Handle with care

runtimeverification · Oct 18, 2024 · 47326f7 · 47326f7
1 parent 95989c7
commit 47326f7
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
@@ -71,6 +71,7 @@ import Booster.Pattern.Util
 import Booster.Prettyprinter
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
+import Booster.Syntax.Json.Internalise (extractSubsitution)
 import Booster.Util (Flag (..))
 
 newtype RewriteT io a = RewriteT
@@ -367,7 +368,7 @@ applyRule pat@Pattern{ceilConditions} rule =
                     let (newSubsitution, newConstraints) = partitionPredicates ensuredConditions
 
                     -- compose the existing substitution pattern and the newly acquired one
-                    let modifiedPatternSubst = newSubsitution `compose` pat.substitution
+                    let (modifiedPatternSubst, leftoverConstraints) = extractSubsitution . asEquations $ newSubsitution `compose` pat.substitution
 
                     let rewrittenTerm = substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) rule.rhs
                         substitutedNewConstraints =
@@ -379,7 +380,7 @@ applyRule pat@Pattern{ceilConditions} rule =
                             Pattern
                                 rewrittenTerm
                                 -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables
-                                (pat.constraints <> substitutedNewConstraints)
+                                (pat.constraints <> substitutedNewConstraints <> Set.fromList leftoverConstraints)
                                 modifiedPatternSubst -- ruleSubstitution is not needed, do not attach it to the result
                                 ceilConditions
                     withContext CtxSuccess $

diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs
@@ -19,6 +19,7 @@ import Data.Text.Encoding qualified as Text
 import Booster.Pattern.Base (externaliseKmapUnsafe)
 import Booster.Pattern.Base qualified as Internal
 import Booster.Pattern.Bool qualified as Internal
+import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (sortOfTerm)
 import Data.Map (Map)
 import Data.Map qualified as Map
@@ -35,7 +36,7 @@ externalisePattern ::
 externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution = ensuredSubstitution} inputSubstitution =
     -- need a sort for the predicates in external format
     let sort = externaliseSort $ sortOfTerm term
-        substitutions = ensuredSubstitution <> inputSubstitution -- TODO ensuredSubstitution takes priority. Do we even need inputSubstitution?
+        substitutions = inputSubstitution <> (ensuredSubstitution `Substitution.compose` inputSubstitution)
         externalisedSubstitution =
             if null substitutions
                 then Nothing