checkpoint - int working?
This commit is contained in:
Kacper Marzecki
parent
2ea586c4ad
commit
dddefdb7ac
741
test.exs
741
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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user