-
Notifications
You must be signed in to change notification settings - Fork 41
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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]>
- Loading branch information
1 parent
cfebf12
commit 3230905
Showing
5 changed files
with
91 additions
and
15 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -569,6 +569,7 @@ library | |
SMT | ||
SMT.AST | ||
SMT.SimpleSMT | ||
SMT.Utils | ||
SQL | ||
SQL.ColumnDef | ||
SQL.Key | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters