Merge branch 'main' into rule-groups

conjure-cp · Jan 12, 2025 · f6242fc · f6242fc
2 parents c183d89 + e012905
commit f6242fc
Show file tree

Hide file tree

Showing 25 changed files with 57 additions and 154 deletions.
diff --git a/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/01-simple/input-expected-rule-trace-human.txt
@@ -10,7 +10,7 @@ such that
 --
 
 Sum([|x|, |y|]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(0..5)

diff --git a/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/02-neg/input-expected-rule-trace-human.txt
@@ -22,7 +22,7 @@ such that
 --
 
 Sum([|x|, |y|]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(0..5)

diff --git a/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/03-nested/input-expected-rule-trace-human.txt
@@ -155,7 +155,7 @@ And([(Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]) = 10)]),
 --
 
 Sum([|Sum([SafeDiv(x, 2), y, -(z)])|, SafeDiv(|y|, 2)]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(0..10)
@@ -166,7 +166,7 @@ new constraints:
 --
 
 |Sum([SafeDiv(x, 2), y, -(z)])|, 
-   ~~> flatten_unop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 |__2| 
 new variables:
   __2: int(-10..8)
@@ -181,7 +181,7 @@ AbsEq(__0,__2)
 --
 
 SafeDiv(|y|, 2), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__3, 2) 
 new variables:
   __3: int(0..5)
@@ -202,7 +202,7 @@ DivEq(__3, 2, __1)
 --
 
 Sum([SafeDiv(x, 2), y, -(z)]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__4, y, __5]) 
 new variables:
   __4: int(-3..1)

diff --git a/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/abs/04-bounds/input-expected-rule-trace-human.txt
@@ -10,7 +10,7 @@ such that
 --
 
 Product([y, |x|]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Product([y, __0]) 
 new variables:
   __0: int(0..3)

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
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeDiv(b, c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..3)

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
@@ -35,7 +35,7 @@ And([(c != 0)]),
 --
 
 (a != SafeDiv(b, c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..3)

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
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeDiv(b, c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..3)

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
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeMod(b,c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..2)

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
@@ -35,7 +35,7 @@ And([(c != 0)]),
 --
 
 (a != SafeMod(b,c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..2)

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
@@ -53,7 +53,7 @@ Not((c != 0)),
 --
 
 (a != SafeMod(b,c)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (a != __0) 
 new variables:
   __0: int(0..2)

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
@@ -35,7 +35,7 @@ And([(z != 0)]),
 --
 
 SafeDiv(-(y), z), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__0, z) 
 new variables:
   __0: int(-1..1)

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
@@ -46,15 +46,21 @@ And([(z != 0)]),
 
 --
 
-(x = -(SafeDiv(y, z))), 
-   ~~> flatten_minuseq ([("Minion", 4200)]) 
-MinusEq(x,__0) 
+-(SafeDiv(y, z)), 
+   ~~> flatten_generic ([("Minion", 4200)]) 
+-(__0) 
 new variables:
   __0: int(-1..1)
 new constraints:
   __0 =aux SafeDiv(y, z)
 --
 
+(x = -(__0)), 
+   ~~> introduce_minuseq_from_eq ([("Minion", 4400)]) 
+MinusEq(x,__0) 
+
+--
+
 __0 =aux SafeDiv(y, z), 
    ~~> introduce_diveq ([("Minion", 4200)]) 
 DivEq(y, z, __0) 

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
@@ -83,7 +83,7 @@ And([(x = SafeDiv(-(SafeDiv(y, z)), z)), (z != 0), (z != 0)])
 --
 
 SafeDiv(-(SafeDiv(y, z)), z), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__0, z) 
 new variables:
   __0: int(-1..1)
@@ -97,15 +97,21 @@ DivEq(__0, z, x)
 
 --
 
-__0 =aux -(SafeDiv(y, z)), 
-   ~~> flatten_minuseq ([("Minion", 4200)]) 
-MinusEq(__0,__1) 
+-(SafeDiv(y, z)), 
+   ~~> flatten_generic ([("Minion", 4200)]) 
+-(__1) 
 new variables:
   __1: int(-1..1)
 new constraints:
   __1 =aux SafeDiv(y, z)
 --
 
+__0 =aux -(__1), 
+   ~~> introduce_minuseq_from_aux_decl ([("Minion", 4400)]) 
+MinusEq(__0,__1) 
+
+--
+
 __1 =aux SafeDiv(y, z), 
    ~~> introduce_diveq ([("Minion", 4200)]) 
 DivEq(y, z, __1) 

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
@@ -11,7 +11,7 @@ such that
 --
 
 Sum([-(y), z]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, z]) 
 new variables:
   __0: int(-1..1)

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
@@ -55,7 +55,7 @@ a
 --
 
 Sum([-(y), -(z), -1, a, b]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1, -1, a, b]) 
 new variables:
   __0: int(-1..1)

diff --git a/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/basic/product/01-simple/input-expected-rule-trace-human.txt
@@ -29,7 +29,7 @@ Sum([15, -1]),
 --
 
 (Product([x, y, z]) <= 14), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 <= 14) 
 new variables:
   __0: int(8..64)

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
@@ -42,7 +42,7 @@ And([(a != 0)]),
 --
 
 SafeDiv(Sum([x, y, z]), a), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(__0, a) 
 new variables:
   __0: int(6..14)

diff --git a/...ide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt b/...ide/tests/integration/basic/weighted-sum/03-simple-eq/input-expected-rule-trace-human.txt
@@ -10,7 +10,7 @@ such that
 --
 
 Sum([Product([2, x]), Product([3, y])]), 
-   ~~> flatten_vecop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 Sum([__0, __1]) 
 new variables:
   __0: int(4..8)

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
@@ -71,7 +71,7 @@ And([(SafeDiv(x, SafeDiv(y, z)) = 10), (SafeDiv(y, z) != 0), (z != 0)])
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(x, __0) 
 new variables:
   __0: int(0..5)
@@ -86,7 +86,7 @@ DivEq(x, __0, 10)
 --
 
 (SafeDiv(y, z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..5)

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
@@ -71,7 +71,7 @@ And([(SafeDiv(x, SafeDiv(y, z)) != 10), (SafeDiv(y, z) != 0), (z != 0)])
 --
 
 (SafeDiv(x, SafeDiv(y, z)) != 10), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 10) 
 new variables:
   __0: int(0..20)
@@ -80,7 +80,7 @@ new constraints:
 --
 
 (SafeDiv(y, z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..5)
@@ -89,7 +89,7 @@ new constraints:
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(x, __2) 
 new variables:
   __2: int(0..5)

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
@@ -95,7 +95,7 @@ Not((z != 0)),
 --
 
 (SafeDiv(x, SafeDiv(y, z)) != 10), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 10) 
 new variables:
   __0: int(0..20)
@@ -110,7 +110,7 @@ DivEq(y, z, 0)
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeDiv(x, __1) 
 new variables:
   __1: int(0..5)

diff --git a/...gration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt b/...gration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt
@@ -71,7 +71,7 @@ And([(SafeMod(x,SafeMod(y,z)) = 3), (SafeMod(y,z) != 0), (z != 0)])
 --
 
 SafeMod(x,SafeMod(y,z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeMod(x,__0) 
 new variables:
   __0: int(0..5)
@@ -86,7 +86,7 @@ ModEq(x, __0, 3)
 --
 
 (SafeMod(y,z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..5)

diff --git a/...ion/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt b/...ion/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt
@@ -71,7 +71,7 @@ And([(SafeMod(x,SafeMod(y,z)) != 3), (SafeMod(y,z) != 0), (z != 0)])
 --
 
 (SafeMod(x,SafeMod(y,z)) != 3), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 3) 
 new variables:
   __0: int(0..2)
@@ -80,7 +80,7 @@ new constraints:
 --
 
 (SafeMod(y,z) != 0), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__1 != 0) 
 new variables:
   __1: int(0..3)
@@ -89,7 +89,7 @@ new constraints:
 --
 
 SafeMod(x,SafeMod(y,z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeMod(x,__2) 
 new variables:
   __2: int(0..3)

diff --git a/...n/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt b/...n/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt
@@ -95,7 +95,7 @@ Not((z != 0)),
 --
 
 (SafeMod(x,SafeMod(y,z)) != 3), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 (__0 != 3) 
 new variables:
   __0: int(0..2)
@@ -110,7 +110,7 @@ ModEq(y, z, 0)
 --
 
 SafeMod(x,SafeMod(y,z)), 
-   ~~> flatten_binop ([("Minion", 4200)]) 
+   ~~> flatten_generic ([("Minion", 4200)]) 
 SafeMod(x,__1) 
 new variables:
   __1: int(0..3)