rewriter: log new top level constraints and symbol table changes to r…

…ule traces
conjure-cp · Jan 7, 2025 · 6f6ec47 · 6f6ec47
1 parent 1d34710
commit 6f6ec47
Show file tree

Hide file tree

Showing 31 changed files with 315 additions and 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/...ide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt b/...ide/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/...ts/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt b/...ts/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
@@ -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
@@ -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/...ide/tests/integration/basic/sum/02-sum-put-in-aux-var/input-expected-rule-trace-human.txt b/...ide/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/...xide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt b/...xide/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
@@ -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/...ntegration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt b/...ntegration/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/...ration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/...ration/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/...tion/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/...tion/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),