From dddefdb7aca597a62248d151b1bf179fbafe8426 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Sun, 15 Jun 2025 23:51:11 +0200 Subject: [PATCH] checkpoint - int working? --- test.exs | 741 ++++++++++++++++++------------------------------------- 1 file changed, 234 insertions(+), 507 deletions(-) diff --git a/test.exs b/test.exs index 8fb9614..5728c52 100644 --- a/test.exs +++ b/test.exs @@ -291,237 +291,272 @@ defmodule Tdd do end # --- Semantic Constraint Checking --- - # assumptions_map is {variable_id => value (true, false, :dc)} + # Helper function to calculate the final interval from true/false integer predicates + # and check for internal contradictions among them. + defp calculate_final_interval_from_bounds(bounds_acc) do + derived_min_b = bounds_acc.min_b + derived_max_b = bounds_acc.max_b + + # Stage 1: Check for immediate conflict from <, >, <=, >= derived from true/false predicates + if is_integer(derived_min_b) && is_integer(derived_max_b) && + derived_min_b > derived_max_b do + # Invalid interval + {:contradiction, nil, nil} + else + # Stage 2: Incorporate equality constraint + cond do + bounds_acc.eq_val == :conflict -> + # IO.inspect({bounds_acc}, label: "CAC Int Interval: eq_val conflict") + {:contradiction, nil, nil} + + is_integer(bounds_acc.eq_val) -> + eq_v = bounds_acc.eq_val + 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({bounds_acc, eq_v}, label: "CAC Int Interval: eq consistent") + # Interval is a single point + {:consistent, eq_v, eq_v} + else + # IO.inspect({bounds_acc, eq_v, derived_min_b, derived_max_b}, label: "CAC Int Interval: eq contradicts interval") + # Equality conflicts with bounds + {:contradiction, nil, nil} + end + + true -> + # No equality constraint, or no conflict from it. The initial interval check (derived_min_b > derived_max_b) suffices. + # IO.inspect({bounds_acc, derived_min_b, derived_max_b}, label: "CAC Int Interval: consistent (no eq or eq compatible)") + {:consistent, derived_min_b, derived_max_b} + end + end + end + defp check_assumptions_consistency(assumptions_map) 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") - :contradiction - else - # --- 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) + raw_result = + if MapSet.size(primary_true_predicates) > 1 do + :contradiction + else + # --- Atom-specific checks --- + 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)) + 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") + cond do + has_true_atom_specific_pred && is_explicitly_not_atom_or_different_primary -> :contradiction - else - # --- 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 + + true -> + atom_value_trues = + Enum.reduce(assumptions_map, MapSet.new(), fn + {{1, :value, atom_val}, true}, acc_set -> MapSet.put(acc_set, atom_val) + _otherwise, acc_set -> acc_set 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)) + if MapSet.size(atom_value_trues) > 1 do + :contradiction + else + # --- Tuple-specific checks --- + has_true_tuple_specific_pred = + Enum.any?(assumptions_map, fn {var_id, truth_value} -> + elem(var_id, 0) == 4 && truth_value == true + end) - cond do - has_true_tuple_specific_pred && is_explicitly_not_tuple_or_different_primary -> - # Tuple-specific predicate on a confirmed non-tuple type. - :contradiction + 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)) - true -> - tuple_size_trues = - Enum.reduce(assumptions_map, MapSet.new(), fn - {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val) - _otherwise, acc_set -> acc_set - end) - - if MapSet.size(tuple_size_trues) > 1 do + cond do + has_true_tuple_specific_pred && is_explicitly_not_tuple_or_different_primary -> :contradiction - else - # --- Integer predicate checks (REVISED LOGIC from previous iteration) --- - has_true_integer_specific_pred = - Enum.any?(assumptions_map, fn {var_id, truth_value} -> - # Category 2 for integers - elem(var_id, 0) == 2 && truth_value == true + + true -> + tuple_size_trues = + Enum.reduce(assumptions_map, MapSet.new(), fn + {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val) + _otherwise, acc_set -> acc_set 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)) + if MapSet.size(tuple_size_trues) > 1 do + :contradiction + else + # --- Integer predicate checks (REVISED LOGIC) --- + has_true_integer_specific_pred = + Enum.any?(assumptions_map, fn {var_id, truth_value} -> + elem(var_id, 0) == 2 && truth_value == true + end) - # 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) + 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)) - cond do - has_true_integer_specific_pred && - is_explicitly_not_integer_or_different_primary -> - # Integer-specific predicate on a confirmed non-integer type. - :contradiction + should_check_integer_logic = + Enum.any?(assumptions_map, fn {var_id, _} -> elem(var_id, 0) == 2 end) || + MapSet.member?(primary_true_predicates, :is_integer) - should_check_integer_logic -> - initial_bounds = %{eq_val: nil, min_b: nil, max_b: nil} - - bounds_acc = - Enum.reduce( - assumptions_map, - initial_bounds, - fn - # Integer predicates are category 2 - {{2, :eq, n}, true}, acc -> - 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 - - # 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") + cond do + has_true_integer_specific_pred && + is_explicitly_not_integer_or_different_primary -> :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") + + should_check_integer_logic -> + initial_bounds_from_true_false = %{eq_val: nil, min_b: nil, max_b: nil} + + bounds_acc = + Enum.reduce( + assumptions_map, + initial_bounds_from_true_false, + fn + {{2, :eq, n}, true}, acc -> + cond do + acc.eq_val == :conflict -> acc + is_nil(acc.eq_val) -> %{acc | eq_val: n} + acc.eq_val != n -> %{acc | eq_val: :conflict} + true -> acc + end + + # value < n => value <= n-1 + {{2, :lt, n}, true}, acc -> + new_max_b = + if is_nil(acc.max_b), do: n - 1, else: min(acc.max_b, n - 1) + + %{acc | max_b: new_max_b} + + # value > n => value >= n+1 + {{2, :gt, n}, true}, acc -> + new_min_b = + if is_nil(acc.min_b), do: n + 1, else: max(acc.min_b, n + 1) + + %{acc | min_b: new_min_b} + + # value >= n + {{2, :lt, n}, false}, acc -> + new_min_b = if is_nil(acc.min_b), do: n, else: max(acc.min_b, n) + %{acc | min_b: new_min_b} + + # value <= n + {{2, :gt, n}, false}, acc -> + new_max_b = if is_nil(acc.max_b), do: n, else: min(acc.max_b, n) + %{acc | max_b: new_max_b} + + # Ignore non-integer or :dc preds for this pass + _otherwise, acc -> + acc + end + ) + + case calculate_final_interval_from_bounds(bounds_acc) do + {:contradiction, _, _} -> :contradiction - is_integer(bounds_acc.eq_val) -> - eq_v = bounds_acc.eq_val + {:consistent, current_interval_min, current_interval_max} -> + # Interval from true/false preds is consistent. Now check :dc preds against it. + Enum.reduce_while(assumptions_map, :consistent, fn + {{2, pred_type, n_val}, :dc}, _acc_status -> + is_implied_true = + case pred_type do + :eq -> + is_integer(current_interval_min) && + current_interval_min == n_val && + (is_integer(current_interval_max) && + current_interval_max == n_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 + :lt -> + is_integer(current_interval_max) && + current_interval_max < n_val - 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 + :gt -> + is_integer(current_interval_min) && + current_interval_min > n_val - # 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 + _ -> + false + end + + is_implied_false = + case pred_type do + :eq -> + (is_integer(current_interval_min) && + current_interval_min > n_val) || + (is_integer(current_interval_max) && + current_interval_max < n_val) + + :lt -> + is_integer(current_interval_min) && + current_interval_min >= n_val + + :gt -> + is_integer(current_interval_max) && + current_interval_max <= n_val + + _ -> + false + end + + if is_implied_true || is_implied_false do + # IO.inspect({assumptions_map, pred_type, n_val, current_interval_min, current_interval_max, implied_true, implied_false}, label: "CAC Int DC Contradiction") + # :dc assumption contradicted by derived interval + {:halt, :contradiction} + else + {:cont, :consistent} + end + + _other_assumption, acc_status -> + # Continue with current status + {:cont, acc_status} + end) + + # End reduce_while for :dc checks end - end - # No integer contradictions to check - true -> - :consistent + # End case for calculate_final_interval + # No integer specific preds or not relevant to check integer logic + true -> + :consistent + end + + # End cond for integer checks end - # End integer checks - end + # End else for tuple_size_trues + end - # End tuple size checks + # End true for tuple_specific_pred end - # End tuple preamble - end + # End cond for tuple_specific_pred + end - # End atom value checks + # End else for atom_value_trues end - # End atom preamble - end - |> IO.inspect( - label: "check_assumptions_consistency END assumptions_map = #{inspect(assumptions_map)}" - ) + # End true for atom_specific_pred + + # The IO.inspect was here. For clarity, let's assign to result then inspect. + # result |> IO.inspect(label: "check_assumptions_consistency END assumptions_map = #{inspect(assumptions_map)}") + # For testing, you might want to remove or conditionalize this inspect: + # if System.get_env("DEBUG_CAC") do + # raw_result |> IO.inspect(label: "CAC END: #{inspect(assumptions_map)}") + # else + # raw_result + # end + # Return the consistency status + raw_result end # Helper for min, treating nil as infinity @@ -1296,318 +1331,10 @@ defmodule IntegerTests do end end -# test_all.() -# IntegerTests.run(test) +test_all.() +IntegerTests.run(test) -tdd_int_gt_10 = Tdd.type_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)) +# tdd_int_gt_10 = Tdd.type_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)) -# output: -# -# TDD system initialized. -# 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