From 6f6ec4761fc42b876c25df8680e1939c1d100d31 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Mon, 6 Jan 2025 12:15:08 +0000 Subject: [PATCH] rewriter: log new top level constraints and symbol table changes to rule traces --- .../04/input-expected-rule-trace-human.txt | 4 + .../05/div-05-expected-rule-trace-human.txt | 4 + .../06/div-06-expected-rule-trace-human.txt | 4 + .../02/input-expected-rule-trace-human.txt | 6 ++ .../01/input-expected-rule-trace-human.txt | 6 ++ .../02/input-expected-rule-trace-human.txt | 6 ++ .../03/input-expected-rule-trace-human.txt | 6 ++ .../04/input-expected-rule-trace-human.txt | 6 ++ .../05/input-expected-rule-trace-human.txt | 6 ++ .../04/input-expected-rule-trace-human.txt | 4 + .../05/mod-05-expected-rule-trace-human.txt | 4 + .../06/mod-06-expected-rule-trace-human.txt | 4 + .../input-expected-rule-trace-human.txt | 4 + .../input-expected-rule-trace-human.txt | 4 + .../input-expected-rule-trace-human.txt | 8 ++ .../input-expected-rule-trace-human.txt | 4 + .../input-expected-rule-trace-human.txt | 6 ++ .../input-expected-rule-trace-human.txt | 4 + .../input-expected-rule-trace-human.txt | 10 +++ .../max2/input-expected-rule-trace-human.txt | 16 ++++ .../input-expected-rule-trace-human.txt | 8 ++ .../input-expected-rule-trace-human.txt | 12 +++ .../input-expected-rule-trace-human.txt | 8 ++ .../input-expected-rule-trace-human.txt | 8 ++ .../input-expected-rule-trace-human.txt | 12 +++ .../input-expected-rule-trace-human.txt | 8 ++ crates/conjure_core/src/ast/pretty.rs | 33 +++++++- .../conjure_core/src/rule_engine/rewrite.rs | 2 +- .../src/rule_engine/rewrite_naive.rs | 2 +- .../src/rule_engine/rewriter_common.rs | 77 ++++++++++++++++++- crates/conjure_core/src/rule_engine/rule.rs | 37 ++++++++- 31 files changed, 315 insertions(+), 8 deletions(-) diff --git a/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt index f99b574ca1..4e49cdedd3 100644 --- a/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt @@ -43,7 +43,11 @@ Not((c != 0)), (a != SafeDiv(b, c)), ~~> flatten_binop ([("Minion", 4400)]) (a != __0) +with new top level expressions: + __0 =aux SafeDiv(b, c) +with changed declarations: + + __0: int(0..3) -- __0 =aux SafeDiv(b, c), diff --git a/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt index 570ac85a19..758952c5fe 100644 --- a/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt @@ -25,7 +25,11 @@ And([(c != 0)]), (a != SafeDiv(b, c)), ~~> flatten_binop ([("Minion", 4400)]) (a != __0) +with new top level expressions: + __0 =aux SafeDiv(b, c) +with changed declarations: + + __0: int(0..3) -- __0 =aux SafeDiv(b, c), diff --git a/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt index f99b574ca1..4e49cdedd3 100644 --- a/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt @@ -43,7 +43,11 @@ Not((c != 0)), (a != SafeDiv(b, c)), ~~> flatten_binop ([("Minion", 4400)]) (a != __0) +with new top level expressions: + __0 =aux SafeDiv(b, c) +with changed declarations: + + __0: int(0..3) -- __0 =aux SafeDiv(b, c), diff --git a/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt index 5c663c67b8..5b6f1fd7f4 100644 --- a/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt @@ -1,7 +1,13 @@ Max([2, a]), ~~> max_to_var ([("Base", 100)]) __0 +with new top level expressions: + (__0 >= 2) + (__0 >= a) + Or([(__0 = 2), (__0 = a)]) +with changed declarations: + + __0: int(2..3) -- (__0 <= 2), diff --git a/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt index eb3271e88b..ae2f04dc47 100644 --- a/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt @@ -1,7 +1,13 @@ Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 +with new top level expressions: + (__0 <= a) + (__0 <= b) + Or([(__0 = a), (__0 = b)]) +with changed declarations: + + __0: int(1..3) -- (__0 >= 3), diff --git a/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt index 5cec6e6d2e..ab000d0d57 100644 --- a/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt @@ -1,7 +1,13 @@ Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 +with new top level expressions: + (__0 <= a) + (__0 <= b) + Or([(__0 = a), (__0 = b)]) +with changed declarations: + + __0: int(1..3) -- (__0 <= 2), diff --git a/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt index 5cec6e6d2e..ab000d0d57 100644 --- a/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt @@ -1,7 +1,13 @@ Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 +with new top level expressions: + (__0 <= a) + (__0 <= b) + Or([(__0 = a), (__0 = b)]) +with changed declarations: + + __0: int(1..3) -- (__0 <= 2), diff --git a/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt index eb3271e88b..382d04ea10 100644 --- a/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt @@ -1,7 +1,13 @@ Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 +with new top level expressions: + (__0 <= a) + (__0 <= b) + Or([(__0 = a), (__0 = b)]) +with changed declarations: + + __0: int(1..2) -- (__0 >= 3), diff --git a/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt index 5cec6e6d2e..f94cbb52c8 100644 --- a/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt @@ -1,7 +1,13 @@ Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __0 +with new top level expressions: + (__0 <= a) + (__0 <= b) + Or([(__0 = a), (__0 = b)]) +with changed declarations: + + __0: int(1..4) -- (__0 <= 2), diff --git a/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt index 02be22e7a5..6b39eb4f08 100644 --- a/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt @@ -43,7 +43,11 @@ Not((c != 0)), (a != SafeMod(b,c)), ~~> flatten_binop ([("Minion", 4400)]) (a != __0) +with new top level expressions: + __0 =aux SafeMod(b,c) +with changed declarations: + + __0: int(0..2) -- __0 =aux SafeMod(b,c), diff --git a/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt index d27f7bdec7..fdfa0b7c95 100644 --- a/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt @@ -25,7 +25,11 @@ And([(c != 0)]), (a != SafeMod(b,c)), ~~> flatten_binop ([("Minion", 4400)]) (a != __0) +with new top level expressions: + __0 =aux SafeMod(b,c) +with changed declarations: + + __0: int(0..2) -- __0 =aux SafeMod(b,c), diff --git a/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt index 02be22e7a5..6b39eb4f08 100644 --- a/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt @@ -43,7 +43,11 @@ Not((c != 0)), (a != SafeMod(b,c)), ~~> flatten_binop ([("Minion", 4400)]) (a != __0) +with new top level expressions: + __0 =aux SafeMod(b,c) +with changed declarations: + + __0: int(0..2) -- __0 =aux SafeMod(b,c), diff --git a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt index 482ee09f0c..6ffd7397a0 100644 --- a/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt @@ -25,7 +25,11 @@ And([(z != 0)]), SafeDiv(-(y), z), ~~> flatten_binop ([("Minion", 4400)]) SafeDiv(__0, z) +with new top level expressions: + __0 =aux -(y) +with changed declarations: + + __0: int(-1..1) -- __0 =aux -(y), diff --git a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt index 47c29e355a..acca2e5657 100644 --- a/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt @@ -37,7 +37,11 @@ And([(z != 0)]), (x = -(SafeDiv(y, z))), ~~> flatten_minuseq ([("Minion", 4400)]) MinusEq(x,__0) +with new top level expressions: + __0 =aux SafeDiv(y, z) +with changed declarations: + + __0: int(-1..1) -- __0 =aux SafeDiv(y, z), diff --git a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt index e5c2770df7..39f5a5018b 100644 --- a/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt @@ -79,13 +79,21 @@ And([(x = SafeDiv(-(SafeDiv(y, z)), z)), (z != 0), (z != 0)]) SafeDiv(-(SafeDiv(y, z)), z), ~~> flatten_binop ([("Minion", 4400)]) SafeDiv(__0, z) +with new top level expressions: + __0 =aux -(SafeDiv(y, z)) +with changed declarations: + + __0: int(-1..1) -- __0 =aux -(SafeDiv(y, z)), ~~> flatten_minuseq ([("Minion", 4400)]) MinusEq(__0,__1) +with new top level expressions: + __1 =aux SafeDiv(y, z) +with changed declarations: + + __1: int(-1..1) -- (x = SafeDiv(__0, z)), diff --git a/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt index e3ac1726ee..cd34f75bf3 100644 --- a/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt @@ -1,7 +1,11 @@ Sum([-(y), z]), ~~> flatten_vecop ([("Minion", 4400)]) Sum([__0, z]) +with new top level expressions: + __0 =aux -(y) +with changed declarations: + + __0: int(-1..1) -- __0 =aux -(y), diff --git a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt index 77b24b2a2f..64c3d4b3b8 100644 --- a/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt @@ -49,7 +49,13 @@ a Sum([-(y), -(z), -1, a, b]), ~~> flatten_vecop ([("Minion", 4400)]) Sum([__0, __1, -1, a, b]) +with new top level expressions: + __0 =aux -(y) + __1 =aux -(z) +with changed declarations: + + __0: int(-1..1) + + __1: int(-1..1) -- __0 =aux -(y), diff --git a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt index eb7cc185b6..cf4a68db57 100644 --- a/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt @@ -31,7 +31,11 @@ And([(a != 0)]), SafeDiv(Sum([x, y, z]), a), ~~> flatten_binop ([("Minion", 4400)]) SafeDiv(__0, a) +with new top level expressions: + __0 =aux Sum([x, y, z]) +with changed declarations: + + __0: int(6..14) -- (SafeDiv(__0, a) = 3), diff --git a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt index 01e4228bf5..5c528f67e2 100644 --- a/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt @@ -1,7 +1,11 @@ Sum([Min([a, b]), 6]), ~~> flatten_vecop ([("Minion", 4400)]) Sum([__0, 6]) +with new top level expressions: + __0 =aux Min([a, b]) +with changed declarations: + + __0: int(1..7) -- (Sum([__0, 6]) <= 10), @@ -13,7 +17,13 @@ SumLeq([__0, 6], 10) Min([a, b]), ~~> min_to_var ([("Base", 2000)]) __1 +with new top level expressions: + (__1 <= a) + (__1 <= b) + Or([(__1 = a), (__1 = b)]) +with changed declarations: + + __1: int(1..7) -- (__1 <= a), diff --git a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt index 38b2cc8ca4..73f27ece40 100644 --- a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt @@ -1,7 +1,11 @@ Sum([Max([a, b]), 1]), ~~> flatten_vecop ([("Minion", 4400)]) Sum([__0, 1]) +with new top level expressions: + __0 =aux Max([a, b]) +with changed declarations: + + __0: int(1..4) -- (x = Sum([__0, 1])), @@ -19,7 +23,13 @@ And([SumLeq([__0, 1], x), SumGeq([__0, 1], x)]) Max([a, b]), ~~> max_to_var ([("Base", 100)]) __1 +with new top level expressions: + (__1 >= a) + (__1 >= b) + Or([(__1 = a), (__1 = b)]) +with changed declarations: + + __1: int(1..4) -- (__1 >= 2), @@ -43,7 +53,13 @@ Ineq(b, __1, 0) Max([a, b]), ~~> max_to_var ([("Base", 100)]) __2 +with new top level expressions: + (__2 >= a) + (__2 >= b) + Or([(__2 = a), (__2 = b)]) +with changed declarations: + + __2: int(1..4) -- (__2 >= a), diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt index 34d7b5e672..2544c47737 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt @@ -67,13 +67,21 @@ And([(SafeDiv(x, SafeDiv(y, z)) = 10), (SafeDiv(y, z) != 0), (z != 0)]) SafeDiv(x, SafeDiv(y, z)), ~~> flatten_binop ([("Minion", 4400)]) SafeDiv(x, __0) +with new top level expressions: + __0 =aux SafeDiv(y, z) +with changed declarations: + + __0: int(0..5) -- (SafeDiv(y, z) != 0), ~~> flatten_binop ([("Minion", 4400)]) (__1 != 0) +with new top level expressions: + __1 =aux SafeDiv(y, z) +with changed declarations: + + __1: int(0..5) -- (SafeDiv(x, __0) = 10), diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt index 0193bb3251..1ff649a503 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt @@ -67,19 +67,31 @@ And([(SafeDiv(x, SafeDiv(y, z)) != 10), (SafeDiv(y, z) != 0), (z != 0)]) (SafeDiv(x, SafeDiv(y, z)) != 10), ~~> flatten_binop ([("Minion", 4400)]) (__0 != 10) +with new top level expressions: + __0 =aux SafeDiv(x, SafeDiv(y, z)) +with changed declarations: + + __0: int(0..20) -- (SafeDiv(y, z) != 0), ~~> flatten_binop ([("Minion", 4400)]) (__1 != 0) +with new top level expressions: + __1 =aux SafeDiv(y, z) +with changed declarations: + + __1: int(0..5) -- SafeDiv(x, SafeDiv(y, z)), ~~> flatten_binop ([("Minion", 4400)]) SafeDiv(x, __2) +with new top level expressions: + __2 =aux SafeDiv(y, z) +with changed declarations: + + __2: int(0..5) -- __0 =aux SafeDiv(x, __2), diff --git a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt index e5c9223356..a0504d26dd 100644 --- a/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt @@ -97,13 +97,21 @@ Or([(SafeDiv(x, SafeDiv(y, z)) != 10), (SafeDiv(y, z) = 0), (z = 0)]) (SafeDiv(x, SafeDiv(y, z)) != 10), ~~> flatten_binop ([("Minion", 4400)]) (__0 != 10) +with new top level expressions: + __0 =aux SafeDiv(x, SafeDiv(y, z)) +with changed declarations: + + __0: int(0..20) -- SafeDiv(x, SafeDiv(y, z)), ~~> flatten_binop ([("Minion", 4400)]) SafeDiv(x, __1) +with new top level expressions: + __1 =aux SafeDiv(y, z) +with changed declarations: + + __1: int(0..5) -- (SafeDiv(y, z) = 0), diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt index 07540148dd..c12833790e 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt @@ -67,13 +67,21 @@ And([(SafeMod(x,SafeMod(y,z)) = 3), (SafeMod(y,z) != 0), (z != 0)]) SafeMod(x,SafeMod(y,z)), ~~> flatten_binop ([("Minion", 4400)]) SafeMod(x,__0) +with new top level expressions: + __0 =aux SafeMod(y,z) +with changed declarations: + + __0: int(0..5) -- (SafeMod(y,z) != 0), ~~> flatten_binop ([("Minion", 4400)]) (__1 != 0) +with new top level expressions: + __1 =aux SafeMod(y,z) +with changed declarations: + + __1: int(0..5) -- (SafeMod(x,__0) = 3), diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt index 002aab3cae..df4f2dc9ab 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt @@ -67,19 +67,31 @@ And([(SafeMod(x,SafeMod(y,z)) != 3), (SafeMod(y,z) != 0), (z != 0)]) (SafeMod(x,SafeMod(y,z)) != 3), ~~> flatten_binop ([("Minion", 4400)]) (__0 != 3) +with new top level expressions: + __0 =aux SafeMod(x,SafeMod(y,z)) +with changed declarations: + + __0: int(0..2) -- (SafeMod(y,z) != 0), ~~> flatten_binop ([("Minion", 4400)]) (__1 != 0) +with new top level expressions: + __1 =aux SafeMod(y,z) +with changed declarations: + + __1: int(0..3) -- SafeMod(x,SafeMod(y,z)), ~~> flatten_binop ([("Minion", 4400)]) SafeMod(x,__2) +with new top level expressions: + __2 =aux SafeMod(y,z) +with changed declarations: + + __2: int(0..3) -- __0 =aux SafeMod(x,__2), diff --git a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt index 9abfa4a589..a7ad9a8800 100644 --- a/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt +++ b/conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt @@ -97,13 +97,21 @@ Or([(SafeMod(x,SafeMod(y,z)) != 3), (SafeMod(y,z) = 0), (z = 0)]) (SafeMod(x,SafeMod(y,z)) != 3), ~~> flatten_binop ([("Minion", 4400)]) (__0 != 3) +with new top level expressions: + __0 =aux SafeMod(x,SafeMod(y,z)) +with changed declarations: + + __0: int(0..2) -- SafeMod(x,SafeMod(y,z)), ~~> flatten_binop ([("Minion", 4400)]) SafeMod(x,__1) +with new top level expressions: + __1 =aux SafeMod(y,z) +with changed declarations: + + __1: int(0..3) -- (SafeMod(y,z) = 0), diff --git a/crates/conjure_core/src/ast/pretty.rs b/crates/conjure_core/src/ast/pretty.rs index c22ad10ddc..137b48d65b 100644 --- a/crates/conjure_core/src/ast/pretty.rs +++ b/crates/conjure_core/src/ast/pretty.rs @@ -7,7 +7,7 @@ use std::fmt::Display; use itertools::Itertools; -use super::Expression; +use super::{Expression, Name, SymbolTable}; /// Pretty prints a `Vec` as if it were a top level constraint list in a `such that`. /// @@ -59,3 +59,34 @@ pub fn pretty_vec(elems: &[T]) -> String { str } + +/// Pretty prints, in essence syntax, the variable declaration for the given symbol. +/// +/// E.g. +/// +/// ```text +/// a: int(1..5) +/// ``` +/// +/// Returns None if the symbol is not in the symbol table +pub fn pretty_variable_declaration(symbol_table: &SymbolTable, var_name: &Name) -> Option { + let var = symbol_table.get(var_name)?; + match &var.domain { + super::Domain::BoolDomain => Some(format!("{}: bool", var_name)), + super::Domain::IntDomain(domain) => { + let mut domain_ranges: Vec = vec![]; + for range in domain { + domain_ranges.push(match range { + super::Range::Single(a) => a.to_string(), + super::Range::Bounded(a, b) => format!("{}..{}", a, b), + }); + } + + if domain_ranges.is_empty() { + Some(format!("{}: int", var_name)) + } else { + Some(format!("{}: int({})", var_name, domain_ranges.join(","))) + } + } + } +} diff --git a/crates/conjure_core/src/rule_engine/rewrite.rs b/crates/conjure_core/src/rule_engine/rewrite.rs index c050d649e7..3c6f02dd68 100644 --- a/crates/conjure_core/src/rule_engine/rewrite.rs +++ b/crates/conjure_core/src/rule_engine/rewrite.rs @@ -217,7 +217,7 @@ fn rewrite_iteration<'a>( let rule_results = apply_all_rules(&expression, model, rules, stats); if let Some(result) = choose_rewrite(&rule_results, &expression) { // If a rule is applied, mark the expression as dirty - log_rule_application(&result, &expression); + log_rule_application(&result, &expression, model); return Some(result.reduction); } diff --git a/crates/conjure_core/src/rule_engine/rewrite_naive.rs b/crates/conjure_core/src/rule_engine/rewrite_naive.rs index 0cc52a7ade..d9670699f9 100644 --- a/crates/conjure_core/src/rule_engine/rewrite_naive.rs +++ b/crates/conjure_core/src/rule_engine/rewrite_naive.rs @@ -78,7 +78,7 @@ pub fn rewrite_naive<'a>( [(result, priority, expr, ctx), ..] => { // Extract the single applicable rule and apply it - log_rule_application(result, expr); + log_rule_application(result, expr, &model); // Replace expr with new_expression model.set_constraints(ctx(result.reduction.new_expression.clone())); diff --git a/crates/conjure_core/src/rule_engine/rewriter_common.rs b/crates/conjure_core/src/rule_engine/rewriter_common.rs index 20568714c0..65b20d4714 100644 --- a/crates/conjure_core/src/rule_engine/rewriter_common.rs +++ b/crates/conjure_core/src/rule_engine/rewriter_common.rs @@ -1,8 +1,15 @@ //! Common utilities and types for rewriters. use super::{resolve_rules::ResolveRulesError, Reduction, Rule}; -use crate::ast::{pretty::pretty_vec, Expression}; +use crate::{ + ast::{ + pretty::{pretty_variable_declaration, pretty_vec}, + Expression, + }, + Model, +}; +use itertools::Itertools; use thiserror::Error; use tracing::{info, trace}; @@ -14,7 +21,11 @@ pub struct RuleResult<'a> { /// Logs, to the main log, and the human readable traces used by the integration tester, that the /// rule has been applied to the expression -pub fn log_rule_application(result: &RuleResult, initial_expression: &Expression) { +pub fn log_rule_application( + result: &RuleResult, + initial_expression: &Expression, + initial_model: &Model, +) { let red = &result.reduction; let rule = result.rule; let new_top_string = pretty_vec(&red.new_top); @@ -28,13 +39,73 @@ pub fn log_rule_application(result: &RuleResult, initial_expression: &Expression red.new_expression ); + // empty if no top level constraints + let top_level_str = if !red.new_top.is_empty() { + let mut exprs: Vec = vec![]; + + for expr in &red.new_top { + exprs.push(format!(" {}", expr)); + } + + let exprs = exprs.iter().join("\n"); + + format!("with new top level expressions:\n{}\n", exprs) + } else { + String::new() + }; + + let mut symbol_changes: Vec = vec![]; + + // show symbol changes in diff-like format + // + // + some added decl + // - some removed decl + // + // [old] x: someDomain + // [new] x: someNewDomain + + // TODO: when we support them, print removed declarations with a - in-front of them. + + for var_name in red.added_symbols(&initial_model.variables) { + #[allow(clippy::unwrap_used)] + symbol_changes.push(format!( + " + {}", + pretty_variable_declaration(&red.symbols, &var_name).unwrap() + )); + } + + for (var_name, _, _) in red.changed_symbols(&initial_model.variables) { + #[allow(clippy::unwrap_used)] + symbol_changes.push(format!( + " [old] {}", + pretty_variable_declaration(&initial_model.variables, &var_name).unwrap() + )); + + #[allow(clippy::unwrap_used)] + symbol_changes.push(format!( + " [new] {}", + pretty_variable_declaration(&red.symbols, &var_name).unwrap() + )); + } + + let symbol_changes_str = if symbol_changes.is_empty() { + String::new() + } else { + format!( + "with changed declarations:\n{}\n", + symbol_changes.join("\n") + ) + }; + trace!( target: "rule_engine_human", - "{}, \n ~~> {} ({:?}) \n{} \n\n--\n", + "{}, \n ~~> {} ({:?}) \n{} \n{}\n{}--\n", initial_expression, rule.name, rule.rule_sets, red.new_expression, + top_level_str, + symbol_changes_str ); } diff --git a/crates/conjure_core/src/rule_engine/rule.rs b/crates/conjure_core/src/rule_engine/rule.rs index f0edd1feff..410ddf5bbe 100644 --- a/crates/conjure_core/src/rule_engine/rule.rs +++ b/crates/conjure_core/src/rule_engine/rule.rs @@ -1,9 +1,10 @@ +use std::collections::BTreeSet; use std::fmt::{self, Display, Formatter}; use std::hash::Hash; use thiserror::Error; -use crate::ast::{Expression, SymbolTable}; +use crate::ast::{DecisionVariable, Expression, Name, SymbolTable}; use crate::model::Model; #[derive(Debug, Error)] @@ -97,11 +98,43 @@ impl Reduction { } } - // Apply side-effects (e.g. symbol table updates) + /// Applies side-effects (e.g. symbol table updates) pub fn apply(self, model: &mut Model) { model.extend_sym_table(self.symbols); // Add new assignments to the symbol table model.constraints.extend(self.new_top.clone()); } + + /// Gets symbols added by this reduction + pub fn added_symbols(&self, initial_symbols: &SymbolTable) -> BTreeSet { + let initial_symbols_set: BTreeSet = initial_symbols.keys().cloned().collect(); + let new_symbols_set: BTreeSet = self.symbols.keys().cloned().collect(); + + new_symbols_set + .difference(&initial_symbols_set) + .cloned() + .collect() + } + + /// Gets symbols changed by this reduction + /// + /// Returns a list of tuples of (name, domain before reduction, domain after reduction) + pub fn changed_symbols( + &self, + initial_symbols: &SymbolTable, + ) -> Vec<(Name, DecisionVariable, DecisionVariable)> { + let mut changes: Vec<(Name, DecisionVariable, DecisionVariable)> = vec![]; + + for (var_name, initial_value) in initial_symbols { + let Some(new_value) = self.symbols.get(var_name) else { + continue; + }; + + if new_value != initial_value { + changes.push((var_name.clone(), initial_value.clone(), new_value.clone())); + } + } + changes + } } /**