change rule priorities to run simplifiers first; add reify

Create a rule priority taxonomy, and refactor rules to follow this new convention. In particular, ensure that partial and total evaluation and simplification rules happen before representation changes and solver specific rules. DESCRIPTION Simplifying a model before applying representation changes should ensure that nested sums do not get propagated across the model. For example, the transformation for min turns it into many binary constraints. If simplification was not done first, simplification steps would have to be ran on each of these binary constraints, instead of just on the input model. Ensuring that everything is always in canonical forms should stop rules looping, and help with pattern matching. The implementation of canonical forms is incomplete and outside the scope of this patch. These rule changes caused basic-div-04 to fail. To fix this, this patch also does the following: - add reify constraint (reify(X,1) if constraint X is SAT, reify(X,0) if constraint X is UNSAT) - add rule not(X) ~> reify(X,0) (where X is a constraint), allowing negated constraints to be passed to Minion. MOTIVATION The commit c2b7460 (add broken complex partial evaluator test (arithmetic, nesting, min), 2024-10-12) added a test case for the partial evaluator that never terminated. Simplification steps should be ran before the decomposition of the min constraint and the conversion of expressions into more specialised / solver specific forms (such as ineq, sumgeq, etc); however, this was not the case in this test. In this test, ineq / sumgeq were being applied before the sums had been flattened. After this refactor, this test now terminates with failure. A flattening rule for ineq is needed before this test passes and will be added in a later commit.
conjure-cp · Oct 12, 2024 · b25c3bb · b25c3bb
1 parent c2b7460
commit b25c3bb
Show file tree

Hide file tree

Showing 32 changed files with 963 additions and 533 deletions.
diff --git a/.gitignore b/.gitignore
@@ -182,3 +182,5 @@ fabric.properties
 *.eprime.solution
 *.eprime.solution.*
 *.eprime.info
+
+.MINION*
diff --git a/COMMITMSG b/COMMITMSG
@@ -0,0 +1,6 @@
+ - dont want to do ineq of a sum when we can do a leq!
+   before this patch, a leq was being rewritten to ineq(sum(...)) causing
+   partial-eval-03 to fail. Also, this was being done before the sums were
+   flattened.
+ - now have not(X) ~ reify(X,0) where X is a constraint
+
diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs
@@ -174,6 +174,7 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model)
             // one
             AllDiff(_, _) => (),
             WatchedLiteral(_, _, _) => (),
+            Reify(_, _, _) => (),
         };
         x.clone()
     }));

diff --git a/conjure_oxide/tests/integration/basic/div/01/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/div/01/input.expected-minion.solutions.json
@@ -1,21 +1,17 @@
 [
   {
-    "MachineName(0)": 1,
     "UserName(a)": 1,
     "UserName(b)": 1
   },
   {
-    "MachineName(0)": 1,
     "UserName(a)": 2,
     "UserName(b)": 2
   },
   {
-    "MachineName(0)": 1,
     "UserName(a)": 3,
     "UserName(b)": 2
   },
   {
-    "MachineName(0)": 1,
     "UserName(a)": 3,
     "UserName(b)": 3
   }

diff --git a/conjure_oxide/tests/integration/basic/div/01/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/01/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "Eq": [
+          "DivEq": [
             {
               "clean": false,
               "etype": null
@@ -19,28 +19,9 @@
                   "etype": null
                 },
                 {
-                  "MachineName": 0
-                }
-              ]
-            },
-            {
-              "Constant": [
-                {
-                  "clean": false,
-                  "etype": null
-                },
-                {
-                  "Int": 1
+                  "UserName": "a"
                 }
               ]
-            }
-          ]
-        },
-        {
-          "Neq": [
-            {
-              "clean": false,
-              "etype": null
             },
             {
               "Reference": [
@@ -60,29 +41,18 @@
                   "etype": null
                 },
                 {
-                  "Int": 0
+                  "Int": 1
                 }
               ]
             }
           ]
         },
         {
-          "DivEq": [
+          "Neq": [
             {
               "clean": false,
               "etype": null
             },
-            {
-              "Reference": [
-                {
-                  "clean": false,
-                  "etype": null
-                },
-                {
-                  "UserName": "a"
-                }
-              ]
-            },
             {
               "Reference": [
                 {
@@ -95,13 +65,13 @@
               ]
             },
             {
-              "Reference": [
+              "Constant": [
                 {
                   "clean": false,
                   "etype": null
                 },
                 {
-                  "MachineName": 0
+                  "Int": 0
                 }
               ]
             }
@@ -112,23 +82,6 @@
   },
   "next_var": 1,
   "variables": [
-    [
-      {
-        "MachineName": 0
-      },
-      {
-        "domain": {
-          "IntDomain": [
-            {
-              "Bounded": [
-                0,
-                3
-              ]
-            }
-          ]
-        }
-      }
-    ],
     [
       {
         "UserName": "a"

diff --git a/conjure_oxide/tests/integration/basic/div/03/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/div/03/input.expected-minion.solutions.json
@@ -1,10 +1,8 @@
 [
   {
-    "MachineName(0)": 2,
     "UserName(a)": 3
   },
   {
-    "MachineName(0)": 2,
     "UserName(a)": 4
   }
 ]
diff --git a/conjure_oxide/tests/integration/basic/div/03/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/03/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "Eq": [
+          "DivEq": [
             {
               "clean": false,
               "etype": null
@@ -19,29 +19,10 @@
                   "etype": null
                 },
                 {
-                  "Int": 2
+                  "Int": 8
                 }
               ]
             },
-            {
-              "Reference": [
-                {
-                  "clean": false,
-                  "etype": null
-                },
-                {
-                  "MachineName": 0
-                }
-              ]
-            }
-          ]
-        },
-        {
-          "Neq": [
-            {
-              "clean": false,
-              "etype": null
-            },
             {
               "Reference": [
                 {
@@ -60,29 +41,18 @@
                   "etype": null
                 },
                 {
-                  "Int": 0
+                  "Int": 2
                 }
               ]
             }
           ]
         },
         {
-          "DivEq": [
+          "Neq": [
             {
               "clean": false,
               "etype": null
             },
-            {
-              "Constant": [
-                {
-                  "clean": false,
-                  "etype": null
-                },
-                {
-                  "Int": 8
-                }
-              ]
-            },
             {
               "Reference": [
                 {
@@ -95,13 +65,13 @@
               ]
             },
             {
-              "Reference": [
+              "Constant": [
                 {
                   "clean": false,
                   "etype": null
                 },
                 {
-                  "MachineName": 0
+                  "Int": 0
                 }
               ]
             }
@@ -112,23 +82,6 @@
   },
   "next_var": 1,
   "variables": [
-    [
-      {
-        "MachineName": 0
-      },
-      {
-        "domain": {
-          "IntDomain": [
-            {
-              "Bounded": [
-                0,
-                8
-              ]
-            }
-          ]
-        }
-      }
-    ],
     [
       {
         "UserName": "a"