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