192 lines
8.9 KiB
Elixir
192 lines
8.9 KiB
Elixir
# defmodule Tilly.BDD.OpsTest do
|
|
# use ExUnit.Case, async: true
|
|
#
|
|
# alias Tilly.BDD
|
|
# alias Tilly.BDD.Node
|
|
# alias Tilly.BDD.Ops
|
|
# alias Tilly.BDD.IntegerBoolOps # Using a concrete ops_module for testing
|
|
#
|
|
# setup do
|
|
# typing_ctx = BDD.init_bdd_store(%{})
|
|
# # Pre-intern some common elements for tests if needed, e.g., integers
|
|
# # For now, rely on ops to intern elements as they are used.
|
|
# %{initial_ctx: typing_ctx}
|
|
# end
|
|
#
|
|
# describe "leaf/3" do
|
|
# test "interning an empty leaf value returns predefined false_id", %{initial_ctx: ctx} do
|
|
# {new_ctx, node_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# assert node_id == BDD.false_node_id()
|
|
# assert new_ctx.bdd_store.ops_cache == ctx.bdd_store.ops_cache # Cache not used for this path
|
|
# end
|
|
#
|
|
# test "interning a full leaf value returns predefined true_id", %{initial_ctx: ctx} do
|
|
# {new_ctx, node_id} = Ops.leaf(ctx, true, IntegerBoolOps)
|
|
# assert node_id == BDD.true_node_id()
|
|
# assert new_ctx.bdd_store.ops_cache == ctx.bdd_store.ops_cache
|
|
# end
|
|
#
|
|
# @tag :skip
|
|
# test "interning a new 'other' leaf value returns a new ID", %{initial_ctx: _ctx} do
|
|
# # Assuming IntegerBoolOps.test_leaf_value/1 would return :other for non-booleans
|
|
# # For this test, we'd need an ops_module where e.g. an integer is an :other leaf.
|
|
# # Let's simulate with a mock or by extending IntegerBoolOps if it were not read-only.
|
|
# # For now, this test is conceptual for boolean leaves.
|
|
# # If IntegerBoolOps was extended:
|
|
# # defmodule MockIntegerOps do
|
|
# # defdelegate compare_elements(e1, e2), to: IntegerBoolOps
|
|
# # defdelegate equal_element?(e1, e2), to: IntegerBoolOps
|
|
# # # ... other delegates
|
|
# # def test_leaf_value(10), do: :other # Treat 10 as a specific leaf
|
|
# # def test_leaf_value(true), do: :full
|
|
# # def test_leaf_value(false), do: :empty
|
|
# # end
|
|
# # {ctx_after_intern, node_id} = Ops.leaf(ctx, 10, MockIntegerOps)
|
|
# # assert node_id != BDD.true_node_id() and node_id != BDD.false_node_id()
|
|
# # assert BDD.get_node_data(ctx_after_intern, node_id).structure == Node.mk_leaf(10)
|
|
# # Placeholder for more complex leaf types. Test is skipped.
|
|
# end
|
|
# end
|
|
#
|
|
# describe "split/6 basic simplifications" do
|
|
# test "if i_id is true, returns true_id", %{initial_ctx: ctx} do
|
|
# {_p_ctx, p_id} = Ops.leaf(ctx, false, IntegerBoolOps) # dummy
|
|
# {_n_ctx, n_id} = Ops.leaf(ctx, false, IntegerBoolOps) # dummy
|
|
# true_id = BDD.true_node_id()
|
|
#
|
|
# {new_ctx, result_id} = Ops.split(ctx, 10, p_id, true_id, n_id, IntegerBoolOps)
|
|
# assert result_id == true_id
|
|
# assert new_ctx == ctx # No new nodes or cache entries expected for this rule
|
|
# end
|
|
#
|
|
# test "if p_id == n_id and p_id == i_id, returns p_id", %{initial_ctx: ctx} do
|
|
# {ctx, p_id} = BDD.get_or_intern_node(ctx, Node.mk_leaf(false), IntegerBoolOps) # some leaf
|
|
# i_id = p_id
|
|
# n_id = p_id
|
|
#
|
|
# {_new_ctx, result_id} = Ops.split(ctx, 10, p_id, i_id, n_id, IntegerBoolOps)
|
|
# assert result_id == p_id
|
|
# # Cache might be touched if union_bdds was called, but this rule is direct.
|
|
# # For p_id == i_id, it's direct.
|
|
# end
|
|
#
|
|
# test "if p_id == n_id and p_id != i_id, returns union(p_id, i_id)", %{initial_ctx: ctx} do
|
|
# {ctx, p_id} = BDD.get_or_intern_node(ctx, Node.mk_leaf(false), IntegerBoolOps)
|
|
# {ctx, i_id} = BDD.get_or_intern_node(ctx, Node.mk_leaf(true), IntegerBoolOps) # different leaf
|
|
# n_id = p_id
|
|
#
|
|
# # Expected union of p_id (false_leaf) and i_id (true_leaf) is true_id
|
|
# # This relies on union_bdds working.
|
|
# {_new_ctx, result_id} = Ops.split(ctx, 10, p_id, i_id, n_id, IntegerBoolOps)
|
|
# expected_union_id = BDD.true_node_id() # Union of false_leaf and true_leaf
|
|
# assert result_id == expected_union_id
|
|
# end
|
|
#
|
|
# test "interns a new split node if no simplification rule applies", %{initial_ctx: ctx} do
|
|
# {ctx, p_id} = Ops.leaf(ctx, false, IntegerBoolOps) # false_node_id
|
|
# {ctx, i_id} = Ops.leaf(ctx, false, IntegerBoolOps) # false_node_id
|
|
# {ctx, n_id} = Ops.leaf(ctx, true, IntegerBoolOps) # true_node_id (different from p_id)
|
|
#
|
|
# element = 20
|
|
# {new_ctx, split_node_id} = Ops.split(ctx, element, p_id, i_id, n_id, IntegerBoolOps)
|
|
#
|
|
# assert split_node_id != p_id and split_node_id != i_id and split_node_id != n_id
|
|
# assert split_node_id != BDD.true_node_id() and split_node_id != BDD.false_node_id()
|
|
#
|
|
# node_data = BDD.get_node_data(new_ctx, split_node_id)
|
|
# assert node_data.structure == Node.mk_split(element, p_id, i_id, n_id)
|
|
# assert node_data.ops_module == IntegerBoolOps
|
|
# assert new_ctx.bdd_store.next_node_id > ctx.bdd_store.next_node_id
|
|
# end
|
|
# end
|
|
#
|
|
# describe "union_bdds/3" do
|
|
# test "A U A = A", %{initial_ctx: ctx} do
|
|
# {ctx, a_id} = Ops.leaf(ctx, false, IntegerBoolOps) # false_node_id
|
|
# {new_ctx, result_id} = Ops.union_bdds(ctx, a_id, a_id)
|
|
# assert result_id == a_id
|
|
# assert Map.has_key?(new_ctx.bdd_store.ops_cache, {:union, a_id, a_id})
|
|
# end
|
|
#
|
|
# test "A U True = True", %{initial_ctx: ctx} do
|
|
# {ctx, a_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# true_id = BDD.true_node_id()
|
|
# {_new_ctx, result_id} = Ops.union_bdds(ctx, a_id, true_id)
|
|
# assert result_id == true_id
|
|
# end
|
|
#
|
|
# test "A U False = A", %{initial_ctx: ctx} do
|
|
# {ctx, a_id} = Ops.leaf(ctx, true, IntegerBoolOps) # true_node_id
|
|
# false_id = BDD.false_node_id()
|
|
# {_new_ctx, result_id} = Ops.union_bdds(ctx, a_id, false_id)
|
|
# assert result_id == a_id
|
|
# end
|
|
#
|
|
# test "union of two distinct leaves", %{initial_ctx: ctx} do
|
|
# # leaf(false) U leaf(true) = leaf(true OR false) = leaf(true) -> true_node_id
|
|
# {ctx, leaf_false_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# {ctx, leaf_true_id} = Ops.leaf(ctx, true, IntegerBoolOps) # This is BDD.true_node_id()
|
|
#
|
|
# {_new_ctx, result_id} = Ops.union_bdds(ctx, leaf_false_id, leaf_true_id)
|
|
# assert result_id == BDD.true_node_id()
|
|
# end
|
|
#
|
|
# test "union of two simple split nodes with same element", %{initial_ctx: ctx} do
|
|
# # BDD1: split(10, True, False, False)
|
|
# # BDD2: split(10, False, True, False)
|
|
# # Union: split(10, True U False, False U True, False U False)
|
|
# # = split(10, True, True, False)
|
|
#
|
|
# true_id = BDD.true_node_id()
|
|
# false_id = BDD.false_node_id()
|
|
#
|
|
# {ctx, bdd1_id} = Ops.split(ctx, 10, true_id, false_id, false_id, IntegerBoolOps)
|
|
# {ctx, bdd2_id} = Ops.split(ctx, 10, false_id, true_id, false_id, IntegerBoolOps)
|
|
#
|
|
# {final_ctx, union_id} = Ops.union_bdds(ctx, bdd1_id, bdd2_id)
|
|
#
|
|
# # Expected structure
|
|
# {_final_ctx, expected_bdd_id} = Ops.split(final_ctx, 10, true_id, true_id, false_id, IntegerBoolOps)
|
|
# assert union_id == expected_bdd_id
|
|
# end
|
|
#
|
|
# test "union of two simple split nodes with different elements (x1 < x2)", %{initial_ctx: ctx} do
|
|
# # BDD1: split(10, True, False, False)
|
|
# # BDD2: split(20, False, True, False)
|
|
# # Union (x1 < x2): split(10, p1, i1 U BDD2, n1)
|
|
# # = split(10, True, False U BDD2, False)
|
|
# # = split(10, True, BDD2, False)
|
|
#
|
|
# {ctx, bdd1_p1_id} = Ops.leaf(ctx, true, IntegerBoolOps)
|
|
# {ctx, bdd1_i1_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# {ctx, bdd1_n1_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# {ctx, bdd1_id} = Ops.split(ctx, 10, bdd1_p1_id, bdd1_i1_id, bdd1_n1_id, IntegerBoolOps)
|
|
#
|
|
# {ctx, bdd2_p2_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# {ctx, bdd2_i2_id} = Ops.leaf(ctx, true, IntegerBoolOps)
|
|
# {ctx, bdd2_n2_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# {ctx, bdd2_id} = Ops.split(ctx, 20, bdd2_p2_id, bdd2_i2_id, bdd2_n2_id, IntegerBoolOps)
|
|
#
|
|
# {final_ctx, union_id} = Ops.union_bdds(ctx, bdd1_id, bdd2_id)
|
|
#
|
|
# # Expected structure: split(10, True, BDD2, False)
|
|
# {_final_ctx, expected_bdd_id} = Ops.split(final_ctx, 10, bdd1_p1_id, bdd2_id, bdd1_n1_id, IntegerBoolOps)
|
|
# assert union_id == expected_bdd_id
|
|
# end
|
|
#
|
|
# test "uses cache for repeated union operations", %{initial_ctx: ctx} do
|
|
# {ctx, a_id} = Ops.leaf(ctx, false, IntegerBoolOps)
|
|
# {ctx, b_id} = Ops.leaf(ctx, true, IntegerBoolOps)
|
|
#
|
|
# {ctx_after_first_union, _result1_id} = Ops.union_bdds(ctx, a_id, b_id)
|
|
# cache_after_first = ctx_after_first_union.bdd_store.ops_cache
|
|
#
|
|
# {ctx_after_second_union, _result2_id} = Ops.union_bdds(ctx_after_first_union, a_id, b_id)
|
|
# # The BDD store itself (nodes, next_id) should not change on a cache hit.
|
|
# # The ops_cache map reference will be the same if the result was cached.
|
|
# assert ctx_after_second_union.bdd_store.ops_cache == cache_after_first
|
|
# assert ctx_after_second_union.bdd_store.next_node_id == ctx_after_first_union.bdd_store.next_node_id
|
|
# end
|
|
# end
|
|
# end
|