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

checkpoint

Browse Source
This commit is contained in:
Kacper Marzecki 2025-06-16 11:51:38 +02:00
parent de167ff5f3
commit becef5db2f
1 changed files with 28 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
test.exs
View File

@ -130,10 +130,11 @@ defmodule Tdd do
* **Variables**: * **Variables**:
* `@v_is_integer = {0, :is_integer}` (or a new category, e.g., `2` for integer properties). * `@v_is_integer = {0, :is_integer}` (or a new category, e.g., `2` for integer properties).
* `v_int_eq_N = {INT_CAT, :eq, N}`. * INT_CAT variables (names of variables prefixed with `a b c` to force ordering
* `v_int_lt_N = {INT_CAT, :lt, N}` (value < N). * `v_int_lt_N = {INT_CAT, :alt, N}` (value < N).
* `v_int_gt_N = {INT_CAT, :gt, N}` (value > N). * `v_int_eq_N = {INT_CAT, :beq, N}`.
* *(Consider also: `lte` (less than or equal), `gte` (greater than or equal) to simplify some range logic, or derive them).* * `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**: * **Constructors**:
* `type_integer()`: Any integer. * `type_integer()`: Any integer.
* `type_int_eq(n)`: A specific integer value. * `type_int_eq(n)`: A specific integer value.
@ -420,7 +421,7 @@ defmodule Tdd do
assumptions_map, assumptions_map,
initial_bounds_from_true_false, initial_bounds_from_true_false,
fn fn
{{2, :eq, n}, true}, acc -> {{2, :beq, n}, true}, acc ->
cond do cond do
acc.eq_val == :conflict -> acc acc.eq_val == :conflict -> acc
is_nil(acc.eq_val) -> %{acc | eq_val: n} is_nil(acc.eq_val) -> %{acc | eq_val: n}
@ -429,26 +430,26 @@ defmodule Tdd do
end end
# value < n => value <= n-1 # value < n => value <= n-1
{{2, :lt, n}, true}, acc -> {{2, :alt, n}, true}, acc ->
new_max_b = new_max_b =
if is_nil(acc.max_b), do: n - 1, else: min(acc.max_b, n - 1) if is_nil(acc.max_b), do: n - 1, else: min(acc.max_b, n - 1)
%{acc | max_b: new_max_b} %{acc | max_b: new_max_b}
# value > n => value >= n+1 # value > n => value >= n+1
{{2, :gt, n}, true}, acc -> {{2, :cgt, n}, true}, acc ->
new_min_b = new_min_b =
if is_nil(acc.min_b), do: n + 1, else: max(acc.min_b, n + 1) if is_nil(acc.min_b), do: n + 1, else: max(acc.min_b, n + 1)
%{acc | min_b: new_min_b} %{acc | min_b: new_min_b}
# value >= n # 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) new_min_b = if is_nil(acc.min_b), do: n, else: max(acc.min_b, n)
%{acc | min_b: new_min_b} %{acc | min_b: new_min_b}
# value <= n # 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) new_max_b = if is_nil(acc.max_b), do: n, else: min(acc.max_b, n)
%{acc | max_b: new_max_b} %{acc | max_b: new_max_b}
@ -468,17 +469,17 @@ defmodule Tdd do
{{2, pred_type, n_val}, :dc}, _acc_status -> {{2, pred_type, n_val}, :dc}, _acc_status ->
is_implied_true = is_implied_true =
case pred_type do case pred_type do
:eq -> :beq ->
is_integer(current_interval_min) && is_integer(current_interval_min) &&
current_interval_min == n_val && current_interval_min == n_val &&
(is_integer(current_interval_max) && (is_integer(current_interval_max) &&
current_interval_max == n_val) current_interval_max == n_val)
:lt -> :alt ->
is_integer(current_interval_max) && is_integer(current_interval_max) &&
current_interval_max < n_val current_interval_max < n_val
:gt -> :cgt ->
is_integer(current_interval_min) && is_integer(current_interval_min) &&
current_interval_min > n_val current_interval_min > n_val
@ -488,17 +489,17 @@ defmodule Tdd do
is_implied_false = is_implied_false =
case pred_type do case pred_type do
:eq -> :beq ->
(is_integer(current_interval_min) && (is_integer(current_interval_min) &&
current_interval_min > n_val) || current_interval_min > n_val) ||
(is_integer(current_interval_max) && (is_integer(current_interval_max) &&
current_interval_max < n_val) current_interval_max < n_val)
:lt -> :alt ->
is_integer(current_interval_min) && is_integer(current_interval_min) &&
current_interval_min >= n_val current_interval_min >= n_val
:gt -> :cgt ->
is_integer(current_interval_max) && is_integer(current_interval_max) &&
current_interval_max <= n_val 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} def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id}
# Integer Predicates (Category 2) # Integer Predicates (Category 2)
def v_int_eq(n) when is_integer(n), do: {2, :eq, n}
# strictly less than 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 # 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_any, do: @true_node_id
def type_none, do: @false_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.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
) )
Tdd.print_tdd(union_disjoint_ranges)
IO.inspect(Process.get(:test_failures, [])) IO.inspect(Process.get(:test_failures, []))
end end
end end
test_all.() # test_all.()
IntegerTests.run(test) # IntegerTests.run(test)
# tdd_int_gt_10 = Tdd.type_int_gt(10) tdd_int_gt_10 = Tdd.type_int_gt(10)
# tdd_int_gt_3 = Tdd.type_int_gt(3) 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 = Tdd.type_integer()
Tdd.intersect(Tdd.sum(tdd_int_gt_10, tdd_int_gt_3), tdd_int)
|> Tdd.print_tdd(asd)