Handle substitution better when simplifying standalone predicates

runtimeverification · Oct 22, 2024 · c73a2c9 · c73a2c9
1 parent f8f956f
commit c73a2c9
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
@@ -68,6 +68,7 @@ import Booster.Syntax.Json.Externalise
 import Booster.Syntax.Json.Internalise (
     InternalisedPredicates (..),
     TermOrPredicates (..),
+    extractSubsitution,
     internalisePattern,
     internaliseTermOrPredicate,
     logPatternError,
@@ -289,16 +290,17 @@ respond stateVar request =
                                     mLlvmLibrary
                                     solver
                                     mempty
-                                    predicates -- TODO include ps.substitution?
+                                    (predicates <> Substitution.asEquations ps.substitution)
                                     >>= \case
-                                        (Right newPreds, _) -> do
+                                        (Right simplified, _) -> do
                                             let predicateSort =
                                                     fromMaybe (error "not a predicate") $
                                                         sortOfJson req.state.term
+                                                (simplifiedSubstitution, simplifiedPredicates) = extractSubsitution simplified
                                                 result =
-                                                    map (externalisePredicate predicateSort) newPreds
+                                                    map (externalisePredicate predicateSort) (Set.toList simplifiedPredicates)
                                                         <> map (externaliseCeil predicateSort) ps.ceilPredicates
-                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
+                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution)
                                                         <> ps.unsupported
 
                                             pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)