From becef5db2fd0d57345cdd716b1a4133302b38608 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Mon, 16 Jun 2025 11:51:38 +0200 Subject: [PATCH] checkpoint --- test.exs | 51 ++++++++++++++++++++++++++++----------------------- 1 file changed, 28 insertions(+), 23 deletions(-) diff --git a/test.exs b/test.exs index e225b14..605ab5e 100644 --- a/test.exs +++ b/test.exs @@ -130,10 +130,11 @@ defmodule Tdd do * **Variables**: * `@v_is_integer = {0, :is_integer}` (or a new category, e.g., `2` for integer properties). - * `v_int_eq_N = {INT_CAT, :eq, N}`. - * `v_int_lt_N = {INT_CAT, :lt, N}` (value < N). - * `v_int_gt_N = {INT_CAT, :gt, N}` (value > N). - * *(Consider also: `lte` (less than or equal), `gte` (greater than or equal) to simplify some range logic, or derive them).* + * INT_CAT variables (names of variables prefixed with `a b c` to force ordering + * `v_int_lt_N = {INT_CAT, :alt, N}` (value < N). + * `v_int_eq_N = {INT_CAT, :beq, N}`. + * `v_int_gt_N = {INT_CAT, :cgt, N}` (value > N). + * *(Consider also: `lte` (less than or equal), `gte` (greater than or equal) to simplify some range logic, or derive them).* * **Constructors**: * `type_integer()`: Any integer. * `type_int_eq(n)`: A specific integer value. @@ -420,7 +421,7 @@ defmodule Tdd do assumptions_map, initial_bounds_from_true_false, fn - {{2, :eq, n}, true}, acc -> + {{2, :beq, n}, true}, acc -> cond do acc.eq_val == :conflict -> acc is_nil(acc.eq_val) -> %{acc | eq_val: n} @@ -429,26 +430,26 @@ defmodule Tdd do end # value < n => value <= n-1 - {{2, :lt, n}, true}, acc -> + {{2, :alt, 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 -> + {{2, :cgt, 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 -> + {{2, :alt, 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 -> + {{2, :cgt, 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} @@ -468,17 +469,17 @@ defmodule Tdd do {{2, pred_type, n_val}, :dc}, _acc_status -> is_implied_true = case pred_type do - :eq -> + :beq -> is_integer(current_interval_min) && current_interval_min == n_val && (is_integer(current_interval_max) && current_interval_max == n_val) - :lt -> + :alt -> is_integer(current_interval_max) && current_interval_max < n_val - :gt -> + :cgt -> is_integer(current_interval_min) && current_interval_min > n_val @@ -488,17 +489,17 @@ defmodule Tdd do is_implied_false = case pred_type do - :eq -> + :beq -> (is_integer(current_interval_min) && current_interval_min > n_val) || (is_integer(current_interval_max) && current_interval_max < n_val) - :lt -> + :alt -> is_integer(current_interval_min) && current_interval_min >= n_val - :gt -> + :cgt -> is_integer(current_interval_max) && current_interval_max <= n_val @@ -689,11 +690,11 @@ defmodule Tdd do def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id} # Integer Predicates (Category 2) - def v_int_eq(n) when is_integer(n), do: {2, :eq, n} # strictly less than n - def v_int_lt(n) when is_integer(n), do: {2, :lt, n} + def v_int_lt(n) when is_integer(n), do: {2, :alt, n} + def v_int_eq(n) when is_integer(n), do: {2, :beq, n} # strictly greater than n - def v_int_gt(n) when is_integer(n), do: {2, :gt, n} + def v_int_gt(n) when is_integer(n), do: {2, :cgt, n} def type_any, do: @true_node_id def type_none, do: @false_node_id @@ -1312,14 +1313,18 @@ defmodule IntegerTests do Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges) ) + Tdd.print_tdd(union_disjoint_ranges) IO.inspect(Process.get(:test_failures, [])) 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) + +tdd_int = Tdd.type_integer() +Tdd.intersect(Tdd.sum(tdd_int_gt_10, tdd_int_gt_3), tdd_int) +|> Tdd.print_tdd(asd)