checkpoint

test.exs

@@ -296,26 +296,64 @@ defmodule Tdd do
     # Check 1: Primary type mutual exclusivity
     primary_true_predicates =
       Enum.reduce(assumptions_map, MapSet.new(), fn
+        # A variable like {0, :is_atom} is a primary type predicate
         {{0, predicate_name}, true}, acc_set -> MapSet.put(acc_set, predicate_name)
         _otherwise, acc_set -> acc_set
       end)
 
     if MapSet.size(primary_true_predicates) > 1 do
-      IO.inspect(assumptions_map, label: "Contradiction: Primary Types")
+      # IO.inspect(assumptions_map, label: "Contradiction: Primary Types")
       :contradiction
     else
-      # Check 2: Specific atom value conflicts, e.g. {1, :value, :foo} == true AND {1, :value, :bar} == true
+      # --- Atom-specific checks ---
+      # Check if any atom-specific predicate (category 1) is asserted as true.
+      has_true_atom_specific_pred =
+        Enum.any?(assumptions_map, fn {var_id, truth_value} ->
+          elem(var_id, 0) == 1 && truth_value == true
+        end)
+
+      # Check if the type is explicitly NOT an atom, or if a different primary type is asserted.
+      is_explicitly_not_atom_or_different_primary =
+        Map.get(assumptions_map, @v_is_atom) == false ||
+          (MapSet.size(primary_true_predicates) == 1 &&
+             !MapSet.member?(primary_true_predicates, :is_atom))
+
+      cond do
+        has_true_atom_specific_pred && is_explicitly_not_atom_or_different_primary ->
+          # Atom-specific predicate asserted on a confirmed non-atom type.
+          :contradiction
+
+        # Proceed with internal atom value checks if relevant.
+        true ->
           atom_value_trues =
             Enum.reduce(assumptions_map, MapSet.new(), fn
+              # An atom value predicate is like {1, :value, :some_atom}
               {{1, :value, atom_val}, true}, acc_set -> MapSet.put(acc_set, atom_val)
               _otherwise, acc_set -> acc_set
             end)
 
           if MapSet.size(atom_value_trues) > 1 do
-        IO.inspect(assumptions_map, label: "Contradiction: Atom Values")
+            # IO.inspect(assumptions_map, label: "Contradiction: Atom Values")
             :contradiction
           else
-        # Check 3: Tuple size conflicts, e.g. {4, :size, 2} == true AND {4, :size, 3} == true
+            # --- Tuple-specific checks ---
+            has_true_tuple_specific_pred =
+              Enum.any?(assumptions_map, fn {var_id, truth_value} ->
+                # Category 4 for tuples
+                elem(var_id, 0) == 4 && truth_value == true
+              end)
+
+            is_explicitly_not_tuple_or_different_primary =
+              Map.get(assumptions_map, @v_is_tuple) == false ||
+                (MapSet.size(primary_true_predicates) == 1 &&
+                   !MapSet.member?(primary_true_predicates, :is_tuple))
+
+            cond do
+              has_true_tuple_specific_pred && is_explicitly_not_tuple_or_different_primary ->
+                # Tuple-specific predicate on a confirmed non-tuple type.
+                :contradiction
+
+              true ->
                 tuple_size_trues =
                   Enum.reduce(assumptions_map, MapSet.new(), fn
                     {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val)
@@ -325,54 +363,165 @@ defmodule Tdd do
                 if MapSet.size(tuple_size_trues) > 1 do
                   :contradiction
                 else
-          # Check 4: Integer predicate conflicts (New)
+                  # --- Integer predicate checks (REVISED LOGIC from previous iteration) ---
-          # Collect all integer constraints assumed to be true
+                  has_true_integer_specific_pred =
-          # eq_val stores THE value if an :eq constraint is true. nil otherwise.
+                    Enum.any?(assumptions_map, fn {var_id, truth_value} ->
-          # lt_bound stores the smallest N for which `val < N` is true (upper bound, exclusive). nil if none.
+                      # Category 2 for integers
-          # gt_bound stores the largest N for which `val > N` is true (lower bound, exclusive). nil if none.
+                      elem(var_id, 0) == 2 && truth_value == true
-          constraints =
-            Enum.reduce(assumptions_map, %{eq_val: nil, lt_b: nil, gt_b: nil}, fn
-              {{2, :eq, n}, true}, acc ->
-                %{acc | eq_val: if(is_nil(acc.eq_val) or acc.eq_val == n, do: n, else: :conflict)}
-
-              {{2, :lt, n}, true}, acc ->
-                %{acc | lt_b: min_opt(acc.lt_b, n)}
-
-              {{2, :gt, n}, true}, acc ->
-                %{acc | gt_b: max_opt(acc.gt_b, n)}
-
-              _otherwise, acc ->
-                acc
                     end)
 
+                  is_explicitly_not_integer_or_different_primary =
+                    Map.get(assumptions_map, @v_is_integer) == false ||
+                      (MapSet.size(primary_true_predicates) == 1 &&
+                         !MapSet.member?(primary_true_predicates, :is_integer))
+
+                  # This flag indicates if we should even bother with interval logic.
+                  # We check if there are integer-specific predicates *or* if the primary type is known to be integer.
+                  should_check_integer_logic =
+                    Enum.any?(assumptions_map, fn {var_id, _} -> elem(var_id, 0) == 2 end) ||
+                      MapSet.member?(primary_true_predicates, :is_integer)
+
                   cond do
-            # Multiple different equality constraints
+                    has_true_integer_specific_pred &&
-            constraints.eq_val == :conflict ->
+                        is_explicitly_not_integer_or_different_primary ->
+                      # Integer-specific predicate on a confirmed non-integer type.
                       :contradiction
 
-            # Check eq_val against lt_b and gt_b
+                    should_check_integer_logic ->
-            is_integer(constraints.eq_val) ->
+                      initial_bounds = %{eq_val: nil, min_b: nil, max_b: nil}
-              eq_v = constraints.eq_val
-              lt_ok = is_nil(constraints.lt_b) || eq_v < constraints.lt_b
-              gt_ok = is_nil(constraints.gt_b) || eq_v > constraints.gt_b
-              if lt_ok && gt_ok, do: :consistent, else: :contradiction
 
-            # Check lt_b vs gt_b (if no specific eq_val)
+                      bounds_acc =
-            is_integer(constraints.lt_b) && is_integer(constraints.gt_b) &&
+                        Enum.reduce(
-                constraints.lt_b <= constraints.gt_b + 1 ->
+                          assumptions_map,
-              # e.g., x < 5 AND x > 4 (no integer) OR x < 5 AND x > 3 (only x=4)
+                          initial_bounds,
-              # If lt_b <= gt_b + 1, it means there's no integer space or only one possible integer.
+                          fn
-              # If lt_b == gt_b + 1, it implies x must be that one integer. This isn't a contradiction by itself yet.
+                            # Integer predicates are category 2
-              # If lt_b <= gt_b, it's a definite contradiction e.g. x < 5 and x > 5.
+                            {{2, :eq, n}, true}, acc ->
-              if constraints.lt_b <= constraints.gt_b, do: :contradiction, else: :consistent
+                              cond do
+                                acc.eq_val == :conflict -> acc
+                                is_nil(acc.eq_val) -> %{acc | eq_val: n}
+                                # Different eq values
+                                acc.eq_val != n -> %{acc | eq_val: :conflict}
+                                # Same eq value, no change
+                                true -> acc
+                              end
 
-            # No contradiction found from integer constraints alone
+                            # value < n  =>  value <= n-1
+                            {{2, :lt, n}, true}, acc ->
+                              new_max_b_val = n - 1
+
+                              updated_max_b =
+                                if is_nil(acc.max_b),
+                                  do: new_max_b_val,
+                                  else: min(acc.max_b, new_max_b_val)
+
+                              %{acc | max_b: updated_max_b}
+
+                            # value > n  =>  value >= n+1
+                            {{2, :gt, n}, true}, acc ->
+                              new_min_b_val = n + 1
+
+                              updated_min_b =
+                                if is_nil(acc.min_b),
+                                  do: new_min_b_val,
+                                  else: max(acc.min_b, new_min_b_val)
+
+                              %{acc | min_b: updated_min_b}
+
+                            # value >= n
+                            {{2, :lt, n}, false}, acc ->
+                              new_min_b_val = n
+
+                              updated_min_b =
+                                if is_nil(acc.min_b),
+                                  do: new_min_b_val,
+                                  else: max(acc.min_b, new_min_b_val)
+
+                              %{acc | min_b: updated_min_b}
+
+                            # value <= n
+                            {{2, :gt, n}, false}, acc ->
+                              new_max_b_val = n
+
+                              updated_max_b =
+                                if is_nil(acc.max_b),
+                                  do: new_max_b_val,
+                                  else: min(acc.max_b, new_max_b_val)
+
+                              %{acc | max_b: updated_max_b}
+
+                            # If is_integer is explicitly false, and we have int predicates, it's a conflict
+                            # This is partly covered by the preamble, but good to have in reduction too.
+                            # However, this specific check here might be complex to integrate cleanly
+                            # with the bounds logic. The preamble should suffice.
+
+                            # Non-integer predicates or non-true integer predicates
+                            _otherwise, acc ->
+                              acc
+                          end
+                        )
+
+                      # Stage 1: Initial bounds from <, >, <=, >=
+                      derived_min_b = bounds_acc.min_b
+                      derived_max_b = bounds_acc.max_b
+
+                      # Stage 2: Check for immediate conflict from <, >, <=, >=
+                      if is_integer(derived_min_b) && is_integer(derived_max_b) &&
+                           derived_min_b > derived_max_b do
+                        # IO.inspect({assumptions_map, bounds_acc, derived_min_b, derived_max_b}, label: "CAC Int: Initial min > max")
+                        :contradiction
+                      else
+                        # Stage 3: Incorporate equality constraint
+                        cond do
+                          # e.g. eq(5) and eq(7)
+                          bounds_acc.eq_val == :conflict ->
+                            # IO.inspect({assumptions_map, bounds_acc}, label: "CAC Int: eq_val conflict")
+                            :contradiction
+
+                          is_integer(bounds_acc.eq_val) ->
+                            eq_v = bounds_acc.eq_val
+
+                            # The value must be eq_v. Check if eq_v fits in the derived_min_b/derived_max_b interval.
+                            min_ok = is_nil(derived_min_b) || eq_v >= derived_min_b
+                            max_ok = is_nil(derived_max_b) || eq_v <= derived_max_b
+
+                            if min_ok && max_ok do
+                              # IO.inspect({assumptions_map, bounds_acc, eq_v, derived_min_b, derived_max_b}, label: "CAC Int: eq consistent with interval")
+                              :consistent
+                            else
+                              # IO.inspect({assumptions_map, bounds_acc, eq_v, derived_min_b, derived_max_b}, label: "CAC Int: eq CONTRADICTS interval")
+                              :contradiction
+                            end
+
+                          # No equality constraint, or no conflict from it. The initial interval check (derived_min_b > derived_max_b) suffices.
                           true ->
+                            # IO.inspect({assumptions_map, bounds_acc, derived_min_b, derived_max_b}, label: "CAC Int: consistent (no eq or eq compatible)")
                             :consistent
                         end
                       end
+
+                    # No integer contradictions to check
+                    true ->
+                      :consistent
                   end
+
+                  # End integer checks
                 end
+
+                # End tuple size checks
+            end
+
+            # End tuple preamble
+          end
+
+          # End atom value checks
+      end
+
+      # End atom preamble
+    end
+    |> IO.inspect(
+      label: "check_assumptions_consistency END assumptions_map = #{inspect(assumptions_map)}"
+    )
   end
 
   # Helper for min, treating nil as infinity
@@ -387,59 +536,108 @@ defmodule Tdd do
   # --- Semantic Simplification (Memoized) ---
   defp simplify_with_constraints(tdd_id, assumptions_map) do
     state = get_state()
-    sorted_assumptions_list = Enum.sort_by(assumptions_map, fn {var, _val} -> var end)
+    # Sort assumptions for cache key consistency
+    # Using Map.to_list and then sorting is more robust than Enum.sort_by if keys can be complex
+    sorted_assumptions_list = Enum.sort(Map.to_list(assumptions_map))
     cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list}
 
-    # Order of checks is critical:
+    # 1. Check if the current assumptions_map itself is contradictory
-    # 1. Is the current set of assumptions inherently contradictory? If so, this path is dead.
+    # This initial check is crucial.
-    # 2. Is the TDD itself terminal? (Assumptions are consistent at this point)
+    current_consistency = check_assumptions_consistency(assumptions_map)
-    if check_assumptions_consistency(assumptions_map) == :contradiction do
+
-      # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyContradiction (Early Exit)")
+    if current_consistency == :contradiction do
-      # No need to cache here if it's based purely on assumptions,
+      # update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)}) # Cache if desired
-      # but if tdd_id was involved, caching the result for {tdd_id, assumptions} is good.
-      # Let's cache it for safety, as tdd_id is part of cache_key.
-      update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)})
       @false_node_id
     else
-      # 3. Cache lookup
+      # 2. Handle terminal nodes
       if is_terminal_id(tdd_id) do
-        # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyTerminal")
+        # Terminals are final, assumptions (if consistent) don't change them
-        # Terminals are not affected by further assumptions if not contradictory
         tdd_id
       else
+        # 3. Cache lookup for non-terminal nodes
         if Map.has_key?(state.op_cache, cache_key) do
-          # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyFromCache")
           state.op_cache[cache_key]
         else
-          # 4. Not contradictory, not terminal, not in cache: Process the node
           {var, y, n, d} = get_node_details(tdd_id)
-          # IO.inspect({tdd_id, assumptions_map, var}, label: "SimplifyProcessingNode")
+
+          # 4. Determine how to proceed based on 'var' and 'assumptions_map'
           result_id =
             case Map.get(assumptions_map, var) do
+              # 'var' is explicitly assumed true
               true ->
                 simplify_with_constraints(y, assumptions_map)
 
+              # 'var' is explicitly assumed false
               false ->
                 simplify_with_constraints(n, assumptions_map)
 
+              # 'var' is explicitly assumed don't care
               :dc ->
                 simplify_with_constraints(d, assumptions_map)
 
+              # 'var' is NOT explicitly in assumptions_map. Check for implied truth value.
               nil ->
-                simplified_y = simplify_with_constraints(y, Map.put(assumptions_map, var, true))
+                # If (assumptions_map + var=false) is a contradiction, then var MUST be true.
-                simplified_n = simplify_with_constraints(n, Map.put(assumptions_map, var, false))
+                implies_var_true =
-                simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc))
+                  check_assumptions_consistency(Map.put(assumptions_map, var, false)) ==
+                    :contradiction
+
+                # If (assumptions_map + var=true) is a contradiction, then var MUST be false.
+                implies_var_false =
+                  check_assumptions_consistency(Map.put(assumptions_map, var, true)) ==
+                    :contradiction
+
+                # Note: We don't check for implies_var_dc here, as that's more complex.
+                # The original recursion handles the DC case exploration.
+
+                IO.inspect(
+                  %{
+                    tdd_id: tdd_id,
+                    var: var,
+                    assumptions: assumptions_map,
+                    implies_var_true: implies_var_true,
+                    implies_var_false: implies_var_false
+                  },
+                  label: "Simplify NIL branch"
+                )
+
+                cond do
+                  implies_var_true && implies_var_false ->
+                    # This means assumptions_map itself is contradictory.
+                    # This should ideally be caught by the check at the very top of simplify_with_constraints.
+                    # If reached, it implies an issue or a very complex interaction. Safest is False.
+                    # IO.inspect({assumptions_map, var}, label: "Simplify: Contradiction from implies_var_true/false")
+                    @false_node_id
+
+                  implies_var_true ->
+                    # Var is implied true by other assumptions. Follow the 'yes' branch.
+                    # Pass the original 'assumptions_map' because 'var's truth is derived, not added.
+                    simplify_with_constraints(y, assumptions_map)
+
+                  implies_var_false ->
+                    # Var is implied false. Follow the 'no' branch.
+                    simplify_with_constraints(n, assumptions_map)
+
+                  true ->
+                    # Var's value is not forced by current assumptions. Recurse normally.
+                    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))
+
                     make_node_raw(var, simplified_y, simplified_n, simplified_d)
                 end
+            end
 
-          # IO.inspect({tdd_id, assumptions_map, result_id}, label: "SimplifyExitComputed")
           update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
           result_id
         end
       end
     end
-
-    # End of nested cond/if
   end
 
   # --- Public Node Creation (Used by Type Constructors) ---
@@ -684,10 +882,42 @@ defmodule Tdd do
       true ->
         # A <: B  <=>  A ∩ (¬B) == ∅
         # All operations (intersect, negate) now produce semantically simplified results.
+        IO.puts("\n--- is_subtype debug ---")
+
+        IO.inspect(sub_type_id,
+          label: "is_subtype: sub_type_id (#{inspect(Tdd.get_node_details(sub_type_id))})"
+        )
+
+        IO.inspect(super_type_id,
+          label: "is_subtype: super_type_id (#{inspect(Tdd.get_node_details(super_type_id))})"
+        )
+
+        # Tdd.print_tdd(sub_type_id)
+        # Tdd.print_tdd(super_type_id)
+
         negated_super = negate(super_type_id)
+
+        IO.inspect(negated_super,
+          label: "is_subtype: negated_super_id (#{inspect(Tdd.get_node_details(negated_super))})"
+        )
+
+        # IO.puts("Structure of negated_super:")
+        # Tdd.print_tdd(negated_super)
+
         intersection_result = intersect(sub_type_id, negated_super)
-        # Check against canonical false
+
-        intersection_result == @false_node_id
+        IO.inspect(intersection_result,
+          label:
+            "is_subtype: intersection_result_id (#{inspect(Tdd.get_node_details(intersection_result))})"
+        )
+
+        # IO.puts("Structure of intersection_result:")
+        # Tdd.print_tdd(intersection_result)
+
+        result = intersection_result == @false_node_id
+        IO.inspect(result, label: "is_subtype: final result")
+        IO.puts("--- end is_subtype debug ---\n")
+        result
     end
   end
 
@@ -1069,14 +1299,315 @@ end
 # test_all.()
 # IntegerTests.run(test)
 
-# x < 3
-tdd_int_lt_3 = Tdd.type_int_lt(3)
-# x > 10
 tdd_int_gt_10 = Tdd.type_int_gt(10)
-union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)
+tdd_int_gt_3 = Tdd.type_int_gt(3)
+test.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3))
 
-test.(
+# output: 
-  "int_eq(12) <: (int < 3 | int > 10)",
+#
-  true,
+# TDD system initialized.
-  Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
-)
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_atom},
+#   tdd_id: 3,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :foo} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :foo} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {1, :value, :foo},
+#   tdd_id: 2,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_atom} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :foo} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :foo} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :foo} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_atom},
+#   tdd_id: 5,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :bar} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :bar} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {1, :value, :bar},
+#   tdd_id: 4,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_atom} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :bar} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :bar} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :bar} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_atom},
+#   tdd_id: 6,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_tuple},
+#   tdd_id: 8,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 0} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 0} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {4, :size, 0},
+#   tdd_id: 7,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_tuple} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 0} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 0} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 0} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_atom},
+#   tdd_id: 10,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :baz} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :baz} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {1, :value, :baz},
+#   tdd_id: 9,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_atom} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :baz} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :baz} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => true, {1, :value, :baz} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_atom} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_tuple},
+#   tdd_id: 11,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_tuple},
+#   tdd_id: 13,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 2} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 2} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {4, :size, 2},
+#   tdd_id: 12,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_tuple} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 2} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 2} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => true, {4, :size, 2} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_tuple} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_integer},
+#   tdd_id: 15,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 10} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 10} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {2, :gt, 10},
+#   tdd_id: 14,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_integer} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 10} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 10} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 10} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_integer},
+#   tdd_id: 17,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {2, :gt, 3},
+#   tdd_id: 16,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_integer} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => :dc}: :consistent
+#
+# --- is_subtype debug ---
+# is_subtype: sub_type_id ({{0, :is_integer}, 14, 0, 0}): 15
+# is_subtype: super_type_id ({{0, :is_integer}, 16, 0, 0}): 17
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{2, :gt, 3} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {2, :gt, 3},
+#   tdd_id: 18,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{2, :gt, 3} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{2, :gt, 3} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_integer},
+#   tdd_id: 19,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {2, :gt, 3},
+#   tdd_id: 18,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_integer} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => :dc}: :consistent
+# is_subtype: negated_super_id ({{0, :is_integer}, 18, 1, 1}): 19
+# check_assumptions_consistency END assumptions_map = %{}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {0, :is_integer},
+#   tdd_id: 21,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {2, :gt, 3},
+#   tdd_id: 20,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_integer} => true}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false, {2, :gt, 10} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false, {2, :gt, 10} => true}: :contradiction
+# Simplify NIL branch: %{
+#   var: {2, :gt, 10},
+#   tdd_id: 14,
+#   implies_var_true: false,
+#   implies_var_false: true,
+#   assumptions: %{{0, :is_integer} => true, {2, :gt, 3} => false}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc, {2, :gt, 10} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc, {2, :gt, 10} => true}: :consistent
+# Simplify NIL branch: %{
+#   var: {2, :gt, 10},
+#   tdd_id: 14,
+#   implies_var_true: false,
+#   implies_var_false: false,
+#   assumptions: %{{0, :is_integer} => true, {2, :gt, 3} => :dc}
+# }
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc, {2, :gt, 10} => true}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc, {2, :gt, 10} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => true, {2, :gt, 3} => :dc, {2, :gt, 10} => :dc}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => false}: :consistent
+# check_assumptions_consistency END assumptions_map = %{{0, :is_integer} => :dc}: :consistent
+# is_subtype: intersection_result_id ({{0, :is_integer}, 22, 0, 0}): 23
+# is_subtype: final result: false
+# --- end is_subtype debug ---
+#
+# int_gt_10 <: int_gt_3 (Expected: true) -> Result: false - FAILED