Consider substitution as constraints in evaluatePattern

Include substitution in known truth when simplifying

Author: geo2a

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -455,21 +455,42 @@ evaluatePattern ::
     Pattern ->
     io (Either EquationFailure Pattern, SimplifierCache)
 evaluatePattern def mLlvmLibrary smtSolver cache pat =
-    runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
+    runEquationT
+        def
+        mLlvmLibrary
+        smtSolver
+        cache
+        -- interpret substitution as additional known constraints
+        (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+        . evaluatePattern'
+        $ pat
 
 -- version for internal nested evaluation
 evaluatePattern' ::
     LoggerMIO io =>
     Pattern ->
     EquationT io Pattern
-evaluatePattern' pat@Pattern{term, ceilConditions, substitution} = withPatternContext pat $ do
+evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
     newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults
     -- after evaluating the term, evaluate all (existing and
     -- newly-acquired) constraints, once
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
-    pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions, substitution}
+    -- The interface-level evaluatePattern puts pat.substitution together with pat.constraints
+    -- into the simplifier state as known truth. Here the substitution will bubble-up as part of
+    -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities
+    -- in pat.predicate and pat.substitution), we discard the old substitution here
+    -- and extract a possible simplified one from evaluatedConstraints.
+    let (simplifiedSubsitution, simplifiedConstraints) = partitionPredicates (Set.toList evaluatedConstraints)
+
+    pure
+        Pattern
+            { constraints = Set.fromList simplifiedConstraints
+            , term = newTerm
+            , ceilConditions
+            , substitution = simplifiedSubsitution
+            }
   where
     -- when TooManyIterations exception occurred while evaluating the top-level term,
     -- i.e. not in a recursive evaluation of a side-condition,

booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json

@@ -126,57 +126,6 @@
                         "value": "42"
                     }
                 }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortBool",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "DV",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortBool",
-                            "args": []
-                        },
-                        "value": "true"
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                },
-                                "value": "42"
-                            }
-                        ]
-                    }
-                }
             }
         }
     }

booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json

@@ -126,57 +126,6 @@
                         "value": "42"
                     }
                 }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortBool",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "DV",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortBool",
-                            "args": []
-                        },
-                        "value": "true"
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                },
-                                "value": "42"
-                            }
-                        ]
-                    }
-                }
             }
         }
     }