Add implication and convert to Minion

conjure_oxide/tests/integration/basic/bool/04/bool-04-expected-rule-trace-human.txt

@@ -11,6 +11,12 @@ such that
 
 --
 
+(x = true), 
+   ~~> bool_eq_to_reify ([("Minion", 4400)]) 
+Reify(true, x) 
+
+--
+
 Final model:
 
 find x: bool
@@ -19,6 +25,6 @@ find z: int(42)
 
 such that
 
-(x = true),
+Reify(true, x),
 (y != false)
 

conjure_oxide/tests/integration/basic/bool/04/bool-04.expected-rewrite.serialised.json

@@ -1,24 +1,11 @@
 {
   "constraints": [
     {
-      "Eq": [
+      "MinionReify": [
         {
           "clean": false,
           "etype": null
         },
-        {
-          "Atomic": [
-            {
-              "clean": false,
-              "etype": null
-            },
-            {
-              "Reference": {
-                "UserName": "x"
-              }
-            }
-          ]
-        },
         {
           "Atomic": [
             {
@@ -31,6 +18,11 @@
               }
             }
           ]
+        },
+        {
+          "Reference": {
+            "UserName": "x"
+          }
         }
       ]
     },

conjure_oxide/tests/integration/basic/implies/01-basic/config.toml

@@ -0,0 +1,2 @@
+run_solver=true
+use_native_parser=false

conjure_oxide/tests/integration/basic/implies/01-basic/input-expected-rule-trace-human.txt

@@ -0,0 +1,26 @@
+Model before rewriting:
+
+find x: bool
+find y: bool
+
+such that
+
+(x) -> (y)
+
+--
+
+(x) -> (y), 
+   ~~> introduce_reifyimply_ineq_from_imply ([("Minion", 4400)]) 
+Ineq(x, y, 0) 
+
+--
+
+Final model:
+
+find x: bool
+find y: bool
+
+such that
+
+Ineq(x, y, 0)
+

conjure_oxide/tests/integration/basic/implies/01-basic/input.eprime

@@ -0,0 +1,4 @@
+language ESSENCE' 1.0
+find x,y: bool
+
+such that x -> y

conjure_oxide/tests/integration/basic/implies/01-basic/input.expected-minion.solutions.json

@@ -0,0 +1,14 @@
+[
+  {
+    "x": 0,
+    "y": 0
+  },
+  {
+    "x": 0,
+    "y": 1
+  },
+  {
+    "x": 1,
+    "y": 1
+  }
+]

conjure_oxide/tests/integration/basic/implies/01-basic/input.expected-parse.serialised.json

@@ -0,0 +1,57 @@
+{
+  "constraints": [
+    {
+      "Imply": [
+        {
+          "clean": false,
+          "etype": null
+        },
+        {
+          "Atomic": [
+            {
+              "clean": false,
+              "etype": null
+            },
+            {
+              "Reference": {
+                "UserName": "x"
+              }
+            }
+          ]
+        },
+        {
+          "Atomic": [
+            {
+              "clean": false,
+              "etype": null
+            },
+            {
+              "Reference": {
+                "UserName": "y"
+              }
+            }
+          ]
+        }
+      ]
+    }
+  ],
+  "next_var": 0,
+  "variables": [
+    [
+      {
+        "UserName": "x"
+      },
+      {
+        "domain": "BoolDomain"
+      }
+    ],
+    [
+      {
+        "UserName": "y"
+      },
+      {
+        "domain": "BoolDomain"
+      }
+    ]
+  ]
+}

conjure_oxide/tests/integration/basic/implies/01-basic/input.expected-rewrite.serialised.json

@@ -0,0 +1,44 @@
+{
+  "constraints": [
+    {
+      "FlatIneq": [
+        {
+          "clean": false,
+          "etype": null
+        },
+        {
+          "Reference": {
+            "UserName": "x"
+          }
+        },
+        {
+          "Reference": {
+            "UserName": "y"
+          }
+        },
+        {
+          "Int": 0
+        }
+      ]
+    }
+  ],
+  "next_var": 0,
+  "variables": [
+    [
+      {
+        "UserName": "x"
+      },
+      {
+        "domain": "BoolDomain"
+      }
+    ],
+    [
+      {
+        "UserName": "y"
+      },
+      {
+        "domain": "BoolDomain"
+      }
+    ]
+  ]
+}

conjure_oxide/tests/integration/basic/implies/02-flattening/config.toml

@@ -0,0 +1,2 @@
+run_solver=true
+use_native_parser=false

conjure_oxide/tests/integration/basic/implies/02-flattening/input-expected-rule-trace-human.txt

@@ -0,0 +1,130 @@
+Model before rewriting:
+
+find x: int(1..5)
+find y: int(1..5)
+find z: int(1..5)
+
+such that
+
+((x < 3)) -> ((y >= 5)),
+((Sum([y, z]) = 8)) -> ((Sum([x, 2]) = 3))
+
+--
+
+(x < 3), 
+   ~~> lt_to_leq ([("Minion", 8400)]) 
+(x <= Sum([3, -1])) 
+
+--
+
+Sum([3, -1]), 
+   ~~> apply_eval_constant ([("Constant", 9001)]) 
+2 
+
+--
+
+((x <= 2)) -> ((y >= 5)), 
+   ~~> flatten_imply ([("Minion", 4200)]) 
+(__0) -> ((y >= 5)) 
+new variables:
+  __0: bool
+new constraints:
+  __0 =aux (x <= 2)
+--
+
+(__0) -> ((y >= 5)), 
+   ~~> introduce_reifyimply_ineq_from_imply ([("Minion", 4400)]) 
+ReifyImply((y >= 5), __0) 
+
+--
+
+__0 =aux (x <= 2), 
+   ~~> bool_eq_to_reify ([("Minion", 4400)]) 
+Reify((x <= 2), __0) 
+
+--
+
+((Sum([y, z]) = 8)) -> ((Sum([x, 2]) = 3)), 
+   ~~> flatten_imply ([("Minion", 4200)]) 
+(__1) -> ((Sum([x, 2]) = 3)) 
+new variables:
+  __1: bool
+new constraints:
+  __1 =aux (Sum([y, z]) = 8)
+--
+
+(__1) -> ((Sum([x, 2]) = 3)), 
+   ~~> introduce_reifyimply_ineq_from_imply ([("Minion", 4400)]) 
+ReifyImply((Sum([x, 2]) = 3), __1) 
+
+--
+
+__1 =aux (Sum([y, z]) = 8), 
+   ~~> bool_eq_to_reify ([("Minion", 4400)]) 
+Reify((Sum([y, z]) = 8), __1) 
+
+--
+
+(y >= 5), 
+   ~~> geq_to_ineq ([("Minion", 4100)]) 
+Ineq(5, y, 0) 
+
+--
+
+(Sum([x, 2]) = 3), 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([x, 2]) <= 3), (Sum([x, 2]) >= 3)]) 
+
+--
+
+(Sum([x, 2]) >= 3), 
+   ~~> y_plus_k_geq_x_to_ineq ([("Minion", 4500)]) 
+Ineq(3, x, 2) 
+
+--
+
+(Sum([x, 2]) <= 3), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([x, 2], 3) 
+
+--
+
+(x <= 2), 
+   ~~> leq_to_ineq ([("Minion", 4100)]) 
+Ineq(x, 2, 0) 
+
+--
+
+(Sum([y, z]) = 8), 
+   ~~> sum_eq_to_inequalities ([("Minion", 4100)]) 
+And([(Sum([y, z]) <= 8), (Sum([y, z]) >= 8)]) 
+
+--
+
+(Sum([y, z]) <= 8), 
+   ~~> introduce_sumleq ([("Minion", 4400)]) 
+SumLeq([y, z], 8) 
+
+--
+
+(Sum([y, z]) >= 8), 
+   ~~> introduce_sumgeq ([("Minion", 4400)]) 
+SumGeq([y, z], 8) 
+
+--
+
+Final model:
+
+find x: int(1..5)
+find y: int(1..5)
+find z: int(1..5)
+find __0: bool
+find __1: bool
+
+such that
+
+ReifyImply(Ineq(5, y, 0), __0),
+ReifyImply(And([SumLeq([x, 2], 3), Ineq(3, x, 2)]), __1),
+Reify(Ineq(x, 2, 0), __0),
+Reify(And([SumLeq([y, z], 8), SumGeq([y, z], 8)]), __1)
+

conjure_oxide/tests/integration/basic/implies/02-flattening/input.eprime

@@ -0,0 +1,6 @@
+language ESSENCE' 1.0
+find x,y,z: int(1..5) 
+
+such that
+  (x < 3) -> (y >= 5),
+  (y + z = 8) -> (x + 2 = 3)