refactor(ast): Rename DivEq and ModEq

Rename DivEq to DivEqUndefZero and ModEq to ModulusEqUndefZero. The latter names match more closely to the underlying Minion constraints being used, reflecting that we are using the undefzero variants of both
conjure-cp · Nov 17, 2024 · 77107a0 · 77107a0
1 parent 7579a40
commit 77107a0
Show file tree

Hide file tree

Showing 27 changed files with 61 additions and 48 deletions.
diff --git a/conjure_oxide/tests/generated_tests.rs b/conjure_oxide/tests/generated_tests.rs
@@ -251,7 +251,7 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model)
             SumEq(_, vec, _) => assert_constants_leq_one(&x, vec),
             SumGeq(_, vec, _) => assert_constants_leq_one(&x, vec),
             SumLeq(_, vec, _) => assert_constants_leq_one(&x, vec),
-            DivEq(_, _, _, _) => (),
+            DivEqUndefZero(_, _, _, _) => (),
             Ineq(_, _, _, _) => (),
             // this is a vector operation, but we don't want to fold values into each-other in this
             // one
@@ -261,7 +261,7 @@ fn assert_vector_operators_have_partially_evaluated(model: &conjure_core::Model)
             AuxDeclaration(_, _, _) => (),
             UnsafeMod(_, _, _) => (),
             SafeMod(_, _, _) => (),
-            ModEq(_, _, _, _) => (),
+            ModuloEqUndefZero(_, _, _, _) => (),
         };
         x.clone()
     }));

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

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 @@
       },
       [
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "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
@@ -85,7 +85,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "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
@@ -75,7 +75,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "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
@@ -85,7 +85,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/conjure_oxide/tests/integration/basic/mod/01/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/01/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/conjure_oxide/tests/integration/basic/mod/03/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/03/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/conjure_oxide/tests/integration/basic/mod/04/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/04/input.expected-rewrite.serialised.json
@@ -85,7 +85,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/conjure_oxide/tests/integration/basic/mod/05/mod-05.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/05/mod-05.expected-rewrite.serialised.json
@@ -75,7 +75,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/conjure_oxide/tests/integration/basic/mod/06/mod-06.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/mod/06/mod-06.expected-rewrite.serialised.json
@@ -85,7 +85,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...gration/minion_constraints/div_undefzero-01-simple/input.expected-rewrite.serialised.json b/...gration/minion_constraints/div_undefzero-01-simple/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...tegration/minion_constraints/div_undefzero-02-zero/input.expected-rewrite.serialised.json b/...tegration/minion_constraints/div_undefzero-02-zero/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...gration/minion_constraints/div_undefzero-03-nested/input.expected-rewrite.serialised.json b/...gration/minion_constraints/div_undefzero-03-nested/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -98,7 +98,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -121,7 +121,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...ion/minion_constraints/div_undefzero-04-nested-neq/input.expected-rewrite.serialised.json b/...ion/minion_constraints/div_undefzero-04-nested-neq/input.expected-rewrite.serialised.json
@@ -109,7 +109,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -132,7 +132,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -155,7 +155,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...n/minion_constraints/div_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json b/...n/minion_constraints/div_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json
@@ -48,7 +48,7 @@
                 ]
               },
               {
-                "DivEq": [
+                "DivEqUndefZero": [
                   {
                     "clean": false,
                     "etype": null
@@ -108,7 +108,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -131,7 +131,7 @@
           ]
         },
         {
-          "DivEq": [
+          "DivEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...tion/minion_constraints/modulo_undefzero-01-simple/input.expected-rewrite.serialised.json b/...tion/minion_constraints/modulo_undefzero-01-simple/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...ration/minion_constraints/modulo_undefzero-02-zero/input.expected-rewrite.serialised.json b/...ration/minion_constraints/modulo_undefzero-02-zero/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...tion/minion_constraints/modulo_undefzero-03-nested/input.expected-rewrite.serialised.json b/...tion/minion_constraints/modulo_undefzero-03-nested/input.expected-rewrite.serialised.json
@@ -7,7 +7,7 @@
       },
       [
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -98,7 +98,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -121,7 +121,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/.../minion_constraints/modulo_undefzero-04-nested-neq/input.expected-rewrite.serialised.json b/.../minion_constraints/modulo_undefzero-04-nested-neq/input.expected-rewrite.serialised.json
@@ -109,7 +109,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -132,7 +132,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -155,7 +155,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/...inion_constraints/modulo_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json b/...inion_constraints/modulo_undefzero-05-nested-noteq/input.expected-rewrite.serialised.json
@@ -48,7 +48,7 @@
                 ]
               },
               {
-                "ModEq": [
+                "ModuloEqUndefZero": [
                   {
                     "clean": false,
                     "etype": null
@@ -108,7 +108,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null
@@ -131,7 +131,7 @@
           ]
         },
         {
-          "ModEq": [
+          "ModuloEqUndefZero": [
             {
               "clean": false,
               "etype": null

diff --git a/crates/conjure_core/src/ast/expressions.rs b/crates/conjure_core/src/ast/expressions.rs
@@ -108,11 +108,11 @@ pub enum Expression {
 
     /// `a / b = c`
     #[compatible(Minion)]
-    DivEq(Metadata, Atom, Atom, Atom),
+    DivEqUndefZero(Metadata, Atom, Atom, Atom),
 
     /// `a % b = c`
     #[compatible(Minion)]
-    ModEq(Metadata, Atom, Atom, Atom),
+    ModuloEqUndefZero(Metadata, Atom, Atom, Atom),
 
     #[compatible(Minion)]
     Ineq(Metadata, Box<Expression>, Box<Expression>, Box<Expression>),
@@ -294,7 +294,7 @@ impl Expression {
             Expression::SumEq(_, _, _) => Some(ReturnType::Bool),
             Expression::SumGeq(_, _, _) => Some(ReturnType::Bool),
             Expression::SumLeq(_, _, _) => Some(ReturnType::Bool),
-            Expression::DivEq(_, _, _, _) => Some(ReturnType::Bool),
+            Expression::DivEqUndefZero(_, _, _, _) => Some(ReturnType::Bool),
             Expression::Ineq(_, _, _, _) => Some(ReturnType::Bool),
             Expression::AllDiff(_, _) => Some(ReturnType::Bool),
             Expression::Bubble(_, _, _) => None, // TODO: (flm8) should this be a bool?
@@ -303,7 +303,7 @@ impl Expression {
             Expression::AuxDeclaration(_, _, _) => Some(ReturnType::Bool),
             Expression::UnsafeMod(_, _, _) => Some(ReturnType::Int),
             Expression::SafeMod(_, _, _) => Some(ReturnType::Int),
-            Expression::ModEq(_, _, _, _) => Some(ReturnType::Bool),
+            Expression::ModuloEqUndefZero(_, _, _, _) => Some(ReturnType::Bool),
         }
     }
 
@@ -437,7 +437,7 @@ impl Display for Expression {
             Expression::UnsafeDiv(_, box1, box2) => {
                 write!(f, "UnsafeDiv({}, {})", box1.clone(), box2.clone())
             }
-            Expression::DivEq(_, box1, box2, box3) => {
+            Expression::DivEqUndefZero(_, box1, box2, box3) => {
                 write!(
                     f,
                     "DivEq({}, {}, {})",
@@ -446,7 +446,7 @@ impl Display for Expression {
                     box3.clone()
                 )
             }
-            Expression::ModEq(_, box1, box2, box3) => {
+            Expression::ModuloEqUndefZero(_, box1, box2, box3) => {
                 write!(
                     f,
                     "ModEq({}, {}, {})",

diff --git a/crates/conjure_core/src/rules/base.rs b/crates/conjure_core/src/rules/base.rs
@@ -32,7 +32,10 @@ fn remove_empty_expression(expr: &Expr, _: &Model) -> ApplicationResult {
     // excluded expressions
     if matches!(
         expr,
-        Atomic(_, _) | WatchedLiteral(_, _, _) | DivEq(_, _, _, _) | ModEq(_, _, _, _)
+        Atomic(_, _)
+            | WatchedLiteral(_, _, _)
+            | DivEqUndefZero(_, _, _, _)
+            | ModuloEqUndefZero(_, _, _, _)
     ) {
         return Err(ApplicationError::RuleNotApplicable);
     }

diff --git a/crates/conjure_core/src/rules/constant.rs b/crates/conjure_core/src/rules/constant.rs
@@ -72,7 +72,7 @@ pub fn eval_constant(expr: &Expr) -> Option<Lit> {
             }
             bin_op::<i32, i32>(|a, b| a % b, a, b).map(Lit::Int)
         }
-        Expr::DivEq(_, a, b, c) => {
+        Expr::DivEqUndefZero(_, a, b, c) => {
             let a = unwrap_atom::<i32>(a)?;
             let b = unwrap_atom::<i32>(b)?;
             let c = unwrap_atom::<i32>(c)?;