refactor: make all Minion expressions flat

Change the type signature of Minion constraints to use `Atom`, `Literal` and `Name` instead of recursive `Expressions`. This enforces flatness through typing. Give these expressions the Flat or Minion prefixes to better reflect the fact that they are solver-level expressions only. This commit also contains the following refactors: * Simplified and rewrote much of the Minion solver adaptor `load_model` code, and moved it to a separate file. * Improve documentation of Minion expressions, and add links to their Minion documentation * Rename some Minion rules to be more consistent, and update their doc strings. * Remove `use Expr::*` from the Minion rules. Apart from the rule name changes, these refactors do not change functionality. DETAILS The idea of encoding flatness as types originated in a872e12 (rules(minion): add flattening rules for division, 2024-11-16). This commit adds this strong typing to the rest of the Minion constraints. Minion takes flat constraints as input. Encoding this limitation in the type signature guarantees that our rules obey this, and that nothing is converted into Minion constraints until it is flat. Keeping expressions in a solver-generic, higher-level form until they can be directly converted to a Minion valid constraint is desirable as they can be rewritten by solver-generic rules (such as normalisation) for longer. The prefix used to rename an expression depends on how Minion specific they are: constraints that could be found in other solvers, such as SumGeq, are called Flat. Constraints with more Minion specific semantics, such as DivEqUndefZero, are prefixed with Minion instead.
conjure-cp · Jan 2, 2025 · 6ce102d · 6ce102d
1 parent 77b03db
commit 6ce102d
Show file tree

Hide file tree

Showing 84 changed files with 1,548 additions and 3,502 deletions.
diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs
@@ -328,9 +328,6 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model)
             Max(_, ref vec) => assert_constants_leq_one(&node, vec),
             Or(_, ref vec) => assert_constants_leq_one(&node, vec),
             And(_, ref vec) => assert_constants_leq_one(&node, vec),
-            SumEq(_, ref vec, _) => assert_constants_leq_one(&node, vec),
-            SumGeq(_, ref vec, _) => assert_constants_leq_one(&node, vec),
-            SumLeq(_, ref vec, _) => assert_constants_leq_one(&node, vec),
             _ => (),
         };
     }

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
@@ -8,7 +8,7 @@
         },
         [
           {
-            "DivEqUndefZero": [
+            "MinionDivEqUndefZero": [
               {
                 "clean": false,
                 "etype": null

diff --git a/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/02/input.expected-rewrite.serialised.json
@@ -1,49 +1,23 @@
 {
   "constraints": [
     {
-      "Ineq": [
+      "FlatIneq": [
         {
           "clean": false,
           "etype": null
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Literal": {
-                "Int": 2
-              }
-            }
-          ]
+          "Literal": {
+            "Int": 2
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Reference": {
-                "UserName": "a"
-              }
-            }
-          ]
+          "Reference": {
+            "UserName": "a"
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Literal": {
-                "Int": 0
-              }
-            }
-          ]
+          "Int": 0
         }
       ]
     }

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
@@ -8,7 +8,7 @@
         },
         [
           {
-            "DivEqUndefZero": [
+            "MinionDivEqUndefZero": [
               {
                 "clean": false,
                 "etype": null

diff --git a/conjure_oxide/tests/integration/basic/div/04/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/04/input.expected-rewrite.serialised.json
@@ -79,7 +79,7 @@
       ]
     },
     {
-      "DivEqUndefZero": [
+      "MinionDivEqUndefZero": [
         {
           "clean": false,
           "etype": null

diff --git a/conjure_oxide/tests/integration/basic/div/05/div-05.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/05/div-05.expected-rewrite.serialised.json
@@ -79,7 +79,7 @@
       ]
     },
     {
-      "DivEqUndefZero": [
+      "MinionDivEqUndefZero": [
         {
           "clean": false,
           "etype": null

diff --git a/conjure_oxide/tests/integration/basic/div/06/div-06.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/div/06/div-06.expected-rewrite.serialised.json
@@ -79,7 +79,7 @@
       ]
     },
     {
-      "DivEqUndefZero": [
+      "MinionDivEqUndefZero": [
         {
           "clean": false,
           "etype": null

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,15 +1,15 @@
-(Max([2, a]) <= 2), 
-   ~~> leq_to_ineq ([("Minion", 4100)]) 
-Ineq(Max([2, a]), 2, 0) 
-
---
-
 Max([2, a]), 
    ~~> max_to_var ([("Base", 100)]) 
 __0 
 
 --
 
+(__0 <= 2), 
+   ~~> leq_to_ineq ([("Minion", 4100)]) 
+Ineq(__0, 2, 0) 
+
+--
+
 (__0 >= 2), 
    ~~> geq_to_ineq ([("Minion", 4100)]) 
 Ineq(2, __0, 0) 

diff --git a/conjure_oxide/tests/integration/basic/max/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/max/02/input.expected-rewrite.serialised.json
@@ -1,143 +1,65 @@
 {
   "constraints": [
     {
-      "Ineq": [
+      "FlatIneq": [
         {
           "clean": false,
           "etype": null
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Reference": {
-                "MachineName": 0
-              }
-            }
-          ]
+          "Reference": {
+            "MachineName": 0
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Literal": {
-                "Int": 2
-              }
-            }
-          ]
+          "Literal": {
+            "Int": 2
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Literal": {
-                "Int": 0
-              }
-            }
-          ]
+          "Int": 0
         }
       ]
     },
     {
-      "Ineq": [
+      "FlatIneq": [
         {
           "clean": false,
           "etype": null
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Literal": {
-                "Int": 2
-              }
-            }
-          ]
+          "Literal": {
+            "Int": 2
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Reference": {
-                "MachineName": 0
-              }
-            }
-          ]
+          "Reference": {
+            "MachineName": 0
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Literal": {
-                "Int": 0
-              }
-            }
-          ]
+          "Int": 0
         }
       ]
     },
     {
-      "Ineq": [
+      "FlatIneq": [
         {
           "clean": false,
           "etype": null
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Reference": {
-                "UserName": "a"
-              }
-            }
-          ]
+          "Reference": {
+            "UserName": "a"
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Reference": {
-                "MachineName": 0
-              }
-            }
-          ]
+          "Reference": {
+            "MachineName": 0
+          }
         },
         {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Literal": {
-                "Int": 0
-              }
-            }
-          ]
+          "Int": 0
         }
       ]
     },

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,15 +1,15 @@
-(Min([a, b]) >= 3), 
-   ~~> geq_to_ineq ([("Minion", 4100)]) 
-Ineq(3, Min([a, b]), 0) 
-
---
-
 Min([a, b]), 
    ~~> min_to_var ([("Base", 2000)]) 
 __0 
 
 --
 
+(__0 >= 3), 
+   ~~> geq_to_ineq ([("Minion", 4100)]) 
+Ineq(3, __0, 0) 
+
+--
+
 (__0 <= a), 
    ~~> leq_to_ineq ([("Minion", 4100)]) 
 Ineq(__0, a, 0)