diff --git a/test.exs b/test.exs index 31178b9..4aceef2 100644 --- a/test.exs +++ b/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) - true -> apply(op_name, op_lambda, u1_id, y2) + top_var == var1 -> apply(op_name, op_lambda, y1, u2_id) # u2_id passed through + 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(top_var, res_y, res_n, res_d) # make_node is make_node_raw end - update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)}) result_id end