checkpoint

test.exs

@@ -45,7 +45,10 @@ defmodule Tdd do
     Process.put(:op_cache, new_state.op_cache)
   end
 
-  def make_node(variable, yes_id, no_id, dc_id) do
+# --- Raw Node Creation (Structural) ---
+  # This is the original make_node, focused on structural uniqueness and basic reduction rule.
+  defp make_node_raw(variable, yes_id, no_id, dc_id) do
+    # Basic reduction: if all children are identical, this node is redundant.
     if yes_id == no_id && yes_id == dc_id do
       yes_id
     else
@@ -53,21 +56,94 @@ defmodule Tdd do
       node_tuple = {variable, yes_id, no_id, dc_id}
 
       if Map.has_key?(state.nodes, node_tuple) do
+        # Node already exists (structural sharing)
         state.nodes[node_tuple]
       else
+        # Create new node
         new_id = state.next_id
-
         update_state(%{
           nodes: Map.put(state.nodes, node_tuple, new_id),
           node_by_id: Map.put(state.node_by_id, new_id, node_tuple),
           next_id: new_id + 1
         })
-
         new_id
       end
     end
   end
 
+  # --- Public Node Creation (Currently same as raw, apply will handle context) ---
+  # The `apply` algorithm inherently creates the necessary structure.
+  # Semantic simplification is applied *after* `apply` completes.
+  def make_node(variable, yes_id, no_id, dc_id) do
+    make_node_raw(variable, yes_id, no_id, dc_id)
+  end
+
+ # --- Semantic Constraint Checking ---
+  defp check_assumptions_consistency(assumptions_map) do
+    # Primary type mutual exclusivity:
+    # Check if more than one primary type (category 0) is assumed to be true.
+    primary_true_predicates =
+      Enum.reduce(assumptions_map, MapSet.new(), fn
+        ({{0, predicate_name}, true}, acc_set) -> MapSet.put(acc_set, predicate_name)
+        # ({var, false}, acc_set) -> # If is_atom is false, that's fine with is_tuple being true.
+        # Check if var is a primary type and its assumed value contradicts another assumed primary type.
+        # E.g. assumptions_map has { {0, :is_atom}, true } and we are checking an assumption for { {0, :is_tuple}, true }
+        # This is implicitly handled by iterating through assumptions_map.
+        _otherwise, acc_set -> acc_set
+      end)
+
+    if MapSet.size(primary_true_predicates) > 1 do
+      # IO.puts "Debug: Contradiction! Assumptions: #{inspect assumptions_map}, True primary types: #{inspect primary_true_predicates}"
+      :contradiction
+    else
+      # Add other semantic checks here, e.g.:
+      # - If assumptions include `{v_int_lt_N, true}` and `{v_int_gt_M, true}` where N <= M.
+      # - If assumptions include `{v_tuple_size_eq_2, true}` and `{v_tuple_size_eq_3, true}`.
+      :consistent
+    end
+  end
+
+  # --- Semantic Simplification ---
+  # Simplifies a TDD given a map of assumptions {variable => value}.
+  # Value can be true, false, or :dc (if we want to model "don't care" assumptions).
+  defp simplify_with_constraints(tdd_id, assumptions_map) do
+    state = get_state()
+    # Canonicalize assumptions_map for cache key: sort map by variable
+    # Convert map to sorted list of tuples for stable cache key
+    sorted_assumptions_list = Enum.sort_by(assumptions_map, fn {var, _val} -> var end)
+    cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list}
+
+    cond do
+      is_terminal_id(tdd_id) ->
+        tdd_id
+      Map.has_key?(state.op_cache, cache_key) ->
+        state.op_cache[cache_key]
+      check_assumptions_consistency(assumptions_map) == :contradiction ->
+        # If assumptions are contradictory, the entire path is impossible.
+        # update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)}) # Cache this finding
+        @false_node_id
+      true ->
+        {var, y, n, d} = get_node_details(tdd_id)
+        result_id =
+          case Map.get(assumptions_map, var) do
+            true -> # Current var is assumed true, follow yes branch with same assumptions
+              simplify_with_constraints(y, assumptions_map)
+            false -> # Current var is assumed false, follow no branch with same assumptions
+              simplify_with_constraints(n, assumptions_map)
+            :dc -> # Current var is assumed don't care, follow dc branch
+              simplify_with_constraints(d, assumptions_map)
+            nil -> # Current var is not in assumptions, so it's a decision point.
+                   # Recursively simplify children by adding this var's assignment to assumptions.
+              simplified_y = simplify_with_constraints(y, Map.put(assumptions_map, var, true))
+              simplified_n = simplify_with_constraints(n, Map.put(assumptions_map, var, false))
+              simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc)) # Assuming :dc can be an assumption value
+              make_node_raw(var, simplified_y, simplified_n, simplified_d) # Use raw, as children are now simplified
+          end
+        update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
+        result_id
+    end
+  end
+
   def get_node_details(id) when is_terminal_id(id) do
     if id == @true_node_id, do: :true_terminal, else: :false_terminal
   end
@@ -113,6 +189,7 @@ defmodule Tdd do
     make_node(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
   end
 
+  # --- The APPLY Algorithm (uses make_node, which is currently make_node_raw) ---
   def apply(op_name, op_lambda, u1_id, u2_id) do
     state = get_state()
     cache_key = {op_name, Enum.sort([u1_id, u2_id])}
@@ -125,26 +202,29 @@ defmodule Tdd do
         res_terminal_symbol = op_lambda.(get_node_details(u1_id), get_node_details(u2_id))
         if res_terminal_symbol == :true_terminal, do: @true_node_id, else: @false_node_id
 
-      true ->
+      true -> # Recursive case
         u1_details = get_node_details(u1_id)
         u2_details = get_node_details(u2_id)
 
         result_id =
           cond do
+            # Case: u1 is terminal, u2 is not
             u1_details == :true_terminal or u1_details == :false_terminal ->
               {var2, y2, n2, d2} = u2_details
               res_y = apply(op_name, op_lambda, u1_id, y2)
               res_n = apply(op_name, op_lambda, u1_id, n2)
               res_d = apply(op_name, op_lambda, u1_id, d2)
-              make_node(var2, res_y, res_n, res_d)
+              make_node(var2, res_y, res_n, res_d) # make_node is make_node_raw
 
+            # Case: u2 is terminal, u1 is not
             u2_details == :true_terminal or u2_details == :false_terminal ->
               {var1, y1, n1, d1} = u1_details
               res_y = apply(op_name, op_lambda, y1, u2_id)
               res_n = apply(op_name, op_lambda, n1, u2_id)
               res_d = apply(op_name, op_lambda, d1, u2_id)
-              make_node(var1, res_y, res_n, res_d)
+              make_node(var1, res_y, res_n, res_d) # make_node is make_node_raw
 
+            # Case: Both u1 and u2 are non-terminal nodes
             true ->
               {var1, y1, n1, d1} = u1_details
               {var2, y2, n2, d2} = u2_details
@@ -153,33 +233,30 @@ defmodule Tdd do
                 cond do
                   var1 == var2 -> var1
                   var1 < var2 -> var1
-                  true -> var2
+                  true -> var2 # var2 < var1
                 end
 
+              # Recursive calls based on top_var
               res_y =
                 cond do
                   top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, y1, y2)
-                  top_var == var1 -> apply(op_name, op_lambda, y1, u2_id)
+                  top_var == var1 -> apply(op_name, op_lambda, y1, u2_id) # u2_id passed through
-                  true -> apply(op_name, op_lambda, u1_id, y2)
+                  true -> apply(op_name, op_lambda, u1_id, y2) # u1_id passed through
                 end
-
               res_n =
                 cond do
                   top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, n1, n2)
                   top_var == var1 -> apply(op_name, op_lambda, n1, u2_id)
                   true -> apply(op_name, op_lambda, u1_id, n2)
                 end
-
               res_d =
                 cond do
                   top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, d1, d2)
                   top_var == var1 -> apply(op_name, op_lambda, d1, u2_id)
                   true -> apply(op_name, op_lambda, u1_id, d2)
                 end
-
+              make_node(top_var, res_y, res_n, res_d) # make_node is make_node_raw
-              make_node(top_var, res_y, res_n, res_d)
           end
-
         update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
         result_id
     end