refactor: simplify naive rewriter using Biplate<Expr>

Simplify the naive rewriter logic by implementing `Biplate<Expression>` for `Model`. Currently, we have two similar functions to rewrite expressions in value lettings and the expression tree. By implementing `Biplate<Expression>` in this commit, the constraints tree and expressions inside the symbol table can be traversed using the same operation. This makes it possible to use a single rewriting loop for both value lettings and the constraints tree. Due to limitations in Uniplate derive (documented in code comments), this commit uses manual implementations for the Uniplate / Biplate traits for `Model` and `SymbolTable`; however, the features needed to make derive work here have been added to the Uniplate issue tracker, so we should be able to remove these in the future.
conjure-cp · Feb 3, 2025 · b06c967 · b06c967
1 parent ea840fb
commit b06c967
Show file tree

Hide file tree

Showing 16 changed files with 217 additions and 282 deletions.
diff --git a/..._oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace-human.txt b/..._oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace-human.txt
@@ -16,27 +16,27 @@ Not(A)
 
 --
 
-A, 
-   ~~> substitute_value_lettings ([("Base", 5000)]) 
-false 
+(b < 3), 
+   ~~> lt_to_leq ([("Minion", 8400)]) 
+(b <= Sum([3, -1])) 
 
 --
 
-Not(false), 
+Sum([3, -1]), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
-true 
+2 
 
 --
 
-(b < 3), 
-   ~~> lt_to_leq ([("Minion", 8400)]) 
-(b <= Sum([3, -1])) 
+A, 
+   ~~> substitute_value_lettings ([("Base", 5000)]) 
+false 
 
 --
 
-Sum([3, -1]), 
+Not(false), 
    ~~> apply_eval_constant ([("Constant", 9001)]) 
-2 
+true 
 
 --
 

diff --git a/conjure_oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace.json b/conjure_oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace.json
@@ -66,84 +66,6 @@
       ]
     }
   },
-  {
-    "initial_expression": {
-      "Atomic": [
-        {
-          "Reference": {
-            "UserName": "A"
-          }
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    },
-    "rule_name": "substitute_value_lettings",
-    "rule_set": [
-      [
-        "Base",
-        5000
-      ]
-    ],
-    "transformed _expression": {
-      "Atomic": [
-        {
-          "Literal": {
-            "Bool": false
-          }
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    }
-  },
-  {
-    "initial_expression": {
-      "Not": [
-        {
-          "Atomic": [
-            {
-              "Literal": {
-                "Bool": false
-              }
-            },
-            {
-              "clean": false,
-              "etype": null
-            }
-          ]
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    },
-    "rule_name": "apply_eval_constant",
-    "rule_set": [
-      [
-        "Constant",
-        9001
-      ]
-    ],
-    "transformed _expression": {
-      "Atomic": [
-        {
-          "Literal": {
-            "Bool": true
-          }
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    }
-  },
   {
     "initial_expression": {
       "Lt": [
@@ -302,6 +224,84 @@
       ]
     }
   },
+  {
+    "initial_expression": {
+      "Atomic": [
+        {
+          "Reference": {
+            "UserName": "A"
+          }
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    },
+    "rule_name": "substitute_value_lettings",
+    "rule_set": [
+      [
+        "Base",
+        5000
+      ]
+    ],
+    "transformed _expression": {
+      "Atomic": [
+        {
+          "Literal": {
+            "Bool": false
+          }
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    }
+  },
+  {
+    "initial_expression": {
+      "Not": [
+        {
+          "Atomic": [
+            {
+              "Literal": {
+                "Bool": false
+              }
+            },
+            {
+              "clean": false,
+              "etype": null
+            }
+          ]
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    },
+    "rule_name": "apply_eval_constant",
+    "rule_set": [
+      [
+        "Constant",
+        9001
+      ]
+    ],
+    "transformed _expression": {
+      "Atomic": [
+        {
+          "Literal": {
+            "Bool": true
+          }
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    }
+  },
   {
     "initial_expression": {
       "Atomic": [

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
@@ -143,7 +143,7 @@
     }
   ],
   "symbols": {
-    "next_machine_name": 1,
+    "next_machine_name": 0,
     "table": [
       [
         {

diff --git a/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/01/input.expected-rewrite.serialised.json
@@ -143,7 +143,7 @@
     }
   ],
   "symbols": {
-    "next_machine_name": 1,
+    "next_machine_name": 0,
     "table": [
       [
         {

diff --git a/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/02/input.expected-rewrite.serialised.json
@@ -143,7 +143,7 @@
     }
   ],
   "symbols": {
-    "next_machine_name": 1,
+    "next_machine_name": 0,
     "table": [
       [
         {

diff --git a/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/03/input.expected-rewrite.serialised.json
@@ -143,7 +143,7 @@
     }
   ],
   "symbols": {
-    "next_machine_name": 1,
+    "next_machine_name": 0,
     "table": [
       [
         {

diff --git a/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/04/input.expected-rewrite.serialised.json
@@ -143,7 +143,7 @@
     }
   ],
   "symbols": {
-    "next_machine_name": 1,
+    "next_machine_name": 0,
     "table": [
       [
         {

diff --git a/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json b/conjure_oxide/tests/integration/basic/min/05/input.expected-rewrite.serialised.json
@@ -143,7 +143,7 @@
     }
   ],
   "symbols": {
-    "next_machine_name": 1,
+    "next_machine_name": 0,
     "table": [
       [
         {

diff --git a/...e/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json b/...e/tests/integration/bugs/sm600-non-terminating-min/input.expected-rewrite.serialised.json
@@ -147,7 +147,7 @@
     }
   ],
   "symbols": {
-    "next_machine_name": 1,
+    "next_machine_name": 0,
     "table": [
       [
         {

diff --git a/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt b/conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt
@@ -24,18 +24,17 @@ new constraints:
 
 Max([a, b]), 
    ~~> max_to_var ([("Base", 6000)]) 
-__1 
-new variables:
-  __1: int(1..4)
+__0 
+
 new constraints:
-  (__1 >= a)
-  (__1 >= b)
-  Or([(__1 = a), (__1 = b)])
+  (__0 >= a)
+  (__0 >= b)
+  Or([(__0 = a), (__0 = b)])
 --
 
-(x = Sum([__1, 1])), 
+(x = Sum([__0, 1])), 
    ~~> introduce_weighted_sumleq_sumgeq ([("Minion", 4600)]) 
-And([SumLeq([__1, 1], x), SumGeq([__1, 1], x)]) 
+And([SumLeq([__0, 1], x), SumGeq([__0, 1], x)]) 
 
 --
 
@@ -57,15 +56,15 @@ Ineq(b, __0, 0)
 
 --
 
-(__1 >= a), 
+(__0 >= a), 
    ~~> geq_to_ineq ([("Minion", 4100)]) 
-Ineq(a, __1, 0) 
+Ineq(a, __0, 0) 
 
 --
 
-(__1 >= b), 
+(__0 >= b), 
    ~~> geq_to_ineq ([("Minion", 4100)]) 
-Ineq(b, __1, 0) 
+Ineq(b, __0, 0) 
 
 --
 
@@ -75,16 +74,15 @@ find a: int(1..4)
 find b: int(1..4)
 find x: int(1..4)
 find __0: int(1..4)
-find __1: int(1..4)
 
 such that
 
 Ineq(2, __0, 0),
-And([SumLeq([__1, 1], x), SumGeq([__1, 1], x)]),
+And([SumLeq([__0, 1], x), SumGeq([__0, 1], x)]),
 Ineq(a, __0, 0),
 Ineq(b, __0, 0),
 Or([(__0 = a), (__0 = b)]),
-Ineq(a, __1, 0),
-Ineq(b, __1, 0),
-Or([(__1 = a), (__1 = b)])
+Ineq(a, __0, 0),
+Ineq(b, __0, 0),
+Or([(__0 = a), (__0 = b)])