From 32309057f2925512ae4da564007f56913b574074 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 21 Aug 2024 17:23:16 +1000 Subject: [PATCH] Jb/trim booster ground truth (#4038) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-authored-by: Georgy Lukyanov Co-authored-by: Petar Maksimovic Co-authored-by: github-actions Co-authored-by: Petar Maksimović --- booster/library/Booster/SMT/Interface.hs | 39 ++++++++++++++++++-- kore/kore.cabal | 1 + kore/src/Kore/Rewrite/SMT/Evaluator.hs | 33 ++++++++++++----- kore/src/SMT/Utils.hs | 30 +++++++++++++++ kore/test/Test/Kore/Rewrite/SMT/Evaluator.hs | 3 +- 5 files changed, 91 insertions(+), 15 deletions(-) create mode 100644 kore/src/SMT/Utils.hs diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 03897a96e5..e131435080 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/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 diff --git a/kore/kore.cabal b/kore/kore.cabal index 235717ccd6..95d877eee4 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -569,6 +569,7 @@ library SMT SMT.AST SMT.SimpleSMT + SMT.Utils SQL SQL.ColumnDef SQL.Key diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs index df714b656c..9419fa4d42 100644 --- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs +++ b/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 diff --git a/kore/src/SMT/Utils.hs b/kore/src/SMT/Utils.hs new file mode 100644 index 0000000000..cb3d5b53b3 --- /dev/null +++ b/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 diff --git a/kore/test/Test/Kore/Rewrite/SMT/Evaluator.hs b/kore/test/Test/Kore/Rewrite/SMT/Evaluator.hs index da11dedecc..4edfbe95eb 100644 --- a/kore/test/Test/Kore/Rewrite/SMT/Evaluator.hs +++ b/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