kacper/elipl
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

checkpoint failing test

Browse Source
This commit is contained in:
Kacper Marzecki 2025-06-15 21:04:57 +02:00
parent 6a91950d02
commit 9779fd0328
1 changed files with 51 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

98
test.exs
View File

@ -109,51 +109,56 @@ defmodule Tdd do
sorted_assumptions_list = Enum.sort_by(assumptions_map, fn {var, _val} -> var end)
cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list}
cond do
is_terminal_id(tdd_id) ->
# Order of checks is critical:
# 1. Is the current set of assumptions inherently contradictory? If so, this path is dead.
# 2. Is the TDD itself terminal? (Assumptions are consistent at this point)
if check_assumptions_consistency(assumptions_map) == :contradiction do
# IO.inspect({tdd_id, assumptions_map}, label: "SimplifyContradiction (Early Exit)")
# No need to cache here if it's based purely on assumptions,
# 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
if is_terminal_id(tdd_id) do
# IO.inspect({tdd_id, assumptions_map}, label: "SimplifyTerminal")
# Terminals are not affected by further assumptions if not contradictory
tdd_id
else
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")
result_id =
case Map.get(assumptions_map, var) do
true ->
simplify_with_constraints(y, assumptions_map)
Map.has_key?(state.op_cache, cache_key) ->
state.op_cache[cache_key]
false ->
simplify_with_constraints(n, assumptions_map)
check_assumptions_consistency(assumptions_map) == :contradiction ->
# Path is semantically impossible
# Important
IO.inspect({tdd_id, assumptions_map}, label: "SimplifyContradiction")
update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)})
@false_node_id
:dc ->
simplify_with_constraints(d, assumptions_map)
true ->
{var, y, n, d} = get_node_details(tdd_id)
nil ->
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
result_id =
case Map.get(assumptions_map, var) do
# Current var is assumed true in path, follow yes branch
true ->
simplify_with_constraints(y, assumptions_map)
# Current var is assumed false in path, follow no branch
false ->
simplify_with_constraints(n, assumptions_map)
# Current var is assumed don't care in path, follow dc branch
:dc ->
simplify_with_constraints(d, assumptions_map)
# Current var is not in assumptions, so it's a decision point.
nil ->
# Recursively simplify children by adding this var's assignment to assumptions.
simplified_y = simplify_with_constraints(y, Map.put(assumptions_map, var, true))
simplified_n = simplify_with_constraints(n, Map.put(assumptions_map, var, false))
# Assuming :dc can be an assumption value
simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc))
make_node_raw(var, simplified_y, simplified_n, simplified_d)
end
IO.inspect({tdd_id, assumptions_map, result_id}, label: "SimplifyExit")
update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
result_id
# 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) ---
@ -632,11 +637,10 @@ test_all = fn ->
IO.inspect(Process.get(:test_failures, []))
end
# Should be tdd_none
tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)
test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
IO.inspect("tdd_atom_and_tuple")
Tdd.print_tdd(tdd_atom_and_tuple)
IO.inspect("tdd_none")
Tdd.print_tdd(tdd_none)
# test_all.()
tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))
IO.inspect("tdd_atom_minus_foo")
Tdd.print_tdd(tdd_atom_minus_foo)
IO.inspect("tdd_bar")
Tdd.print_tdd(tdd_bar)