rules(minion): add modulo

Add modulo expressions, parsing, and conversion rules to Minion.

The undefinedness semantics for modulo are similar to those for
division: it requires a bubble rule, asserting that for x % y, y!=0, to
make it safe.

Due to their similarity, the test cases for modulo in this patch are
based on the division ones.

See also: conjure-cp#454 (implementation of division rules)

Closes: conjure-cp#456

conjure_oxide/tests/generated_tests.rs

@@ -259,6 +259,9 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model)
             WatchedLiteral(_, _, _) => (),
             Reify(_, _, _) => (),
             AuxDeclaration(_, _, _) => (),
+            UnsafeMod(_, _, _) => (),
+            SafeMod(_, _, _) => (),
+            ModEq(_, _, _, _) => (),
         };
         x.clone()
     }));

conjure_oxide/tests/integration/basic/mod/01/input.essence

@@ -0,0 +1,2 @@
+find a,b : int(0..3)
+such that a % b = 1

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

@@ -0,0 +1,14 @@
+[
+  {
+    "a": 1,
+    "b": 2
+  },
+  {
+    "a": 1,
+    "b": 3
+  },
+  {
+    "a": 3,
+    "b": 2
+  }
+]

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

@@ -0,0 +1,94 @@
+{
+  "constraints": {
+    "Eq": [
+      {
+        "clean": false,
+        "etype": null
+      },
+      {
+        "UnsafeMod": [
+          {
+            "clean": false,
+            "etype": null
+          },
+          {
+            "Atomic": [
+              {
+                "clean": false,
+                "etype": null
+              },
+              {
+                "Reference": {
+                  "UserName": "a"
+                }
+              }
+            ]
+          },
+          {
+            "Atomic": [
+              {
+                "clean": false,
+                "etype": null
+              },
+              {
+                "Reference": {
+                  "UserName": "b"
+                }
+              }
+            ]
+          }
+        ]
+      },
+      {
+        "Atomic": [
+          {
+            "clean": false,
+            "etype": null
+          },
+          {
+            "Literal": {
+              "Int": 1
+            }
+          }
+        ]
+      }
+    ]
+  },
+  "next_var": 0,
+  "variables": [
+    [
+      {
+        "UserName": "a"
+      },
+      {
+        "domain": {
+          "IntDomain": [
+            {
+              "Bounded": [
+                0,
+                3
+              ]
+            }
+          ]
+        }
+      }
+    ],
+    [
+      {
+        "UserName": "b"
+      },
+      {
+        "domain": {
+          "IntDomain": [
+            {
+              "Bounded": [
+                0,
+                3
+              ]
+            }
+          ]
+        }
+      }
+    ]
+  ]
+}

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

@@ -0,0 +1,106 @@
+{
+  "constraints": {
+    "And": [
+      {
+        "clean": false,
+        "etype": null
+      },
+      [
+        {
+          "ModEq": [
+            {
+              "clean": false,
+              "etype": null
+            },
+            {
+              "Reference": {
+                "UserName": "a"
+              }
+            },
+            {
+              "Reference": {
+                "UserName": "b"
+              }
+            },
+            {
+              "Literal": {
+                "Int": 1
+              }
+            }
+          ]
+        },
+        {
+          "Neq": [
+            {
+              "clean": false,
+              "etype": null
+            },
+            {
+              "Atomic": [
+                {
+                  "clean": false,
+                  "etype": null
+                },
+                {
+                  "Reference": {
+                    "UserName": "b"
+                  }
+                }
+              ]
+            },
+            {
+              "Atomic": [
+                {
+                  "clean": false,
+                  "etype": null
+                },
+                {
+                  "Literal": {
+                    "Int": 0
+                  }
+                }
+              ]
+            }
+          ]
+        }
+      ]
+    ]
+  },
+  "next_var": 0,
+  "variables": [
+    [
+      {
+        "UserName": "a"
+      },
+      {
+        "domain": {
+          "IntDomain": [
+            {
+              "Bounded": [
+                0,
+                3
+              ]
+            }
+          ]
+        }
+      }
+    ],
+    [
+      {
+        "UserName": "b"
+      },
+      {
+        "domain": {
+          "IntDomain": [
+            {
+              "Bounded": [
+                0,
+                3
+              ]
+            }
+          ]
+        }
+      }
+    ]
+  ]
+}

conjure_oxide/tests/integration/basic/mod/02/input.essence

@@ -0,0 +1,2 @@
+find a : int(0..3)
+such that a >= 4 % 2 $ should be simplified to constant

conjure_oxide/tests/integration/basic/mod/02/input.expected-minion.solutions.json

@@ -0,0 +1,14 @@
+[
+  {
+    "a": 0
+  },
+  {
+    "a": 1
+  },
+  {
+    "a": 2
+  },
+  {
+    "a": 3
+  }
+]

conjure_oxide/tests/integration/basic/mod/02/input.expected-parse.serialised.json

@@ -0,0 +1,77 @@
+{
+  "constraints": {
+    "Geq": [
+      {
+        "clean": false,
+        "etype": null
+      },
+      {
+        "Atomic": [
+          {
+            "clean": false,
+            "etype": null
+          },
+          {
+            "Reference": {
+              "UserName": "a"
+            }
+          }
+        ]
+      },
+      {
+        "UnsafeMod": [
+          {
+            "clean": false,
+            "etype": null
+          },
+          {
+            "Atomic": [
+              {
+                "clean": false,
+                "etype": null
+              },
+              {
+                "Literal": {
+                  "Int": 4
+                }
+              }
+            ]
+          },
+          {
+            "Atomic": [
+              {
+                "clean": false,
+                "etype": null
+              },
+              {
+                "Literal": {
+                  "Int": 2
+                }
+              }
+            ]
+          }
+        ]
+      }
+    ]
+  },
+  "next_var": 0,
+  "variables": [
+    [
+      {
+        "UserName": "a"
+      },
+      {
+        "domain": {
+          "IntDomain": [
+            {
+              "Bounded": [
+                0,
+                3
+              ]
+            }
+          ]
+        }
+      }
+    ]
+  ]
+}