Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

booster/library/Booster/SMT/Interface.hs

@@ -434,12 +434,23 @@ checkPredicates ctxt givenPs givenSubst psToCheck
     translated = SMT.runTranslator $ do
         let mkSMTEquation v t =
                 SMT.eq <$> SMT.translateTerm (Var v) <*> SMT.translateTerm t
-        smtSubst <-
-            mapM (\(v, t) -> Assert "Substitution" <$> mkSMTEquation v t) $ Map.assocs givenSubst
-        smtPs <-
-            mapM (\(Predicate p) -> Assert (mkComment p) <$> SMT.translateTerm p) $ Set.toList givenPs
+        substEqs <-
+            mapM (uncurry mkSMTEquation) $ Map.assocs givenSubst
+
+        groundTruth <-
+            mapM (\(Predicate p) -> (p,) <$> SMT.translateTerm p) $ Set.toList givenPs
+
         toCheck <-
             mapM (SMT.translateTerm . coerce) $ Set.toList psToCheck
+
+        let interestingVars = mconcat $ map smtVars toCheck
+            filteredGroundTruth = closureOver interestingVars $ Set.fromList $ map snd groundTruth
+            filteredSubstEqs = closureOver interestingVars $ Set.fromList substEqs
+
+        let mkAssert (p, sexpr) = Assert (mkComment p) sexpr
+            smtPs = map mkAssert $ filter ((`Set.member` filteredGroundTruth) . snd) groundTruth
+            smtSubst = map (Assert "Substitution") $ Set.toList filteredSubstEqs
+
         pure (smtSubst <> smtPs, toCheck)
 
     -- Given the known truth and the expressions to check,
@@ -503,3 +514,23 @@ checkPredicates ctxt givenPs givenSubst psToCheck
                         "Given ∧ P and Given ∧ !P interpreted as "
                             <> pack (show (positive', negative'))
                 pure (positive', negative')
+
+    -- functions for filtering ground truth and substitution equations
+    smtVars :: SMT.SExpr -> Set SMT.SMTId
+    smtVars (Atom smtId@(SMTId bs))
+        | "SMT-" `BS.isPrefixOf` bs = Set.singleton smtId
+        | otherwise = mempty
+    smtVars (List exprs) = mconcat $ map smtVars exprs
+
+    -- filters given 'exprs' to only return those which use any of the
+    -- SMT 'atoms' or from other expressions that are also returned.
+    closureOver :: Set SMT.SMTId -> Set SMT.SExpr -> Set SMT.SExpr
+    closureOver atoms exprs = loop mempty exprs atoms
+      where
+        loop :: Set SMT.SExpr -> Set SMT.SExpr -> Set SMT.SMTId -> Set SMT.SExpr
+        loop acc exprs' currentAtoms =
+            let (rest, addedExprs) = Set.partition (Set.null . Set.intersection currentAtoms . smtVars) exprs'
+                newAtoms = Set.unions $ Set.map smtVars addedExprs
+             in if Set.null addedExprs
+                    then acc
+                    else loop (acc <> addedExprs) rest newAtoms

kore/kore.cabal

@@ -569,6 +569,7 @@ library
     SMT
     SMT.AST
     SMT.SimpleSMT
+    SMT.Utils
     SQL
     SQL.ColumnDef
     SQL.Key

kore/src/Kore/Rewrite/SMT/Evaluator.hs

@@ -94,6 +94,7 @@ import SMT (
  )
 import SMT qualified
 import SMT.SimpleSMT qualified as SimpleSMT
+import SMT.Utils qualified as SMT
 
 {- | Attempt to evaluate the 'Predicate' argument with an optional side
  condition using an external SMT solver.
@@ -109,11 +110,13 @@ evalPredicate onUnknown predicate sideConditionM = case predicate of
     Predicate.PredicateFalse -> return $ Just False
     _ -> case sideConditionM of
         Nothing ->
-            predicate :| []
-                & decidePredicate onUnknown SideCondition.top
+            decidePredicate onUnknown SideCondition.top [] predicate
         Just sideCondition ->
-            predicate :| [from @_ @(Predicate _) sideCondition]
-                & decidePredicate onUnknown sideCondition
+            decidePredicate
+                onUnknown
+                sideCondition
+                (Predicate.getMultiAndPredicate $ from @_ @(Predicate _) sideCondition)
+                predicate
 
 {- | Attempt to evaluate the 'Conditional' argument with an optional side
  condition using an external SMT solver.
@@ -164,9 +167,10 @@ decidePredicate ::
     InternalVariable variable =>
     OnDecidePredicateUnknown ->
     SideCondition variable ->
-    NonEmpty (Predicate variable) ->
+    [Predicate variable] ->
+    Predicate variable ->
     Simplifier (Maybe Bool)
-decidePredicate onUnknown sideCondition predicates =
+decidePredicate onUnknown sideCondition sideConditionPredicates predicate =
     whileDebugEvaluateCondition predicates $
         do
             result <- query >>= whenUnknown retry
@@ -187,14 +191,23 @@ decidePredicate onUnknown sideCondition predicates =
                     empty
             & runMaybeT
   where
+    predicates = predicate :| sideConditionPredicates
+
     query :: MaybeT Simplifier Result
     query = onErrorUnknown $ SMT.withSolver . evalTranslator $ do
         tools <- Simplifier.askMetadataTools
         Morph.hoist SMT.liftSMT $ do
-            predicates' <-
-                traverse
-                    (translatePredicate sideCondition tools)
-                    predicates
+            sideConditionPredicates' <-
+                concatMap SMT.splitAnd
+                    <$> traverse
+                        (translatePredicate sideCondition tools)
+                        sideConditionPredicates
+            predicate' <- SMT.splitAnd <$> translatePredicate sideCondition tools predicate
+            let predicates' = SMT.transitiveClosure (Set.fromList predicate') $ Set.fromList sideConditionPredicates'
+            -- when (Set.fromList predicate' /= predicates') $ liftIO $ do
+            --     putStrLn $ "predicate: " <> show (Set.fromList predicate')
+            --     putStrLn $ "sideConditionPredicates: " <> show sideConditionPredicates'
+            --     putStrLn $ "pruned to: " <> show predicates'
             traverse_ SMT.assert predicates'
             SMT.check >>= maybe empty return
 

kore/src/SMT/Utils.hs

@@ -0,0 +1,30 @@
+module SMT.Utils (module SMT.Utils) where
+
+import Data.Set (Set)
+import Data.Set qualified as Set
+import Data.Text (Text, isPrefixOf, isSuffixOf)
+
+import Prelude.Kore
+import SMT qualified
+
+splitAnd :: SMT.SExpr -> [SMT.SExpr]
+splitAnd = \case
+    SMT.List (SMT.Atom "and" : xs) -> concatMap splitAnd xs
+    other -> [other]
+
+varAtoms :: SMT.SExpr -> Set Text
+varAtoms = \case
+    SMT.Atom a
+        | "<" `isPrefixOf` a && ">" `isSuffixOf` a -> Set.singleton a
+        | otherwise -> mempty
+    SMT.List xs -> mconcat $ map varAtoms xs
+    _ -> mempty
+
+transitiveClosure :: Set SMT.SExpr -> Set SMT.SExpr -> Set SMT.SExpr
+transitiveClosure cl' rest' = loop (Set.unions (Set.map varAtoms cl')) cl' rest'
+  where
+    loop clVars cl rest =
+        let (nonCommon, common) = Set.partition (null . Set.intersection clVars . varAtoms) rest
+         in if null common
+                then cl
+                else loop (clVars <> Set.unions (Set.map varAtoms common)) (cl <> common) nonCommon

kore/test/Test/Kore/Rewrite/SMT/Evaluator.hs

@@ -243,7 +243,8 @@ assertRefuted prop = do
         SMT.Evaluator.decidePredicate
             (ErrorDecidePredicateUnknown $srcLoc Nothing)
             SideCondition.top
-            (prop :| [])
+            []
+            prop
             & Test.runSimplifierSMT testEnv
     assertEqual "" expect actual