Jb/trim booster ground truth (#4038)

When `booster` checks predicates with a given ground truth (a
substitution and other predicates assumed true), this change filters the
substitution and the ground truth to only contain predicates using
relevant variables (from the predicates to check, and transitively from
other relevant predicates).

---------

Co-authored-by: Sam Balco <[email protected]>
Co-authored-by: Georgy Lukyanov <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>

Author: 6 people

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