diff --git a/booster/library/Booster/Definition/Base.hs b/booster/library/Booster/Definition/Base.hs index 72f557568a..b23230ad7f 100644 --- a/booster/library/Booster/Definition/Base.hs +++ b/booster/library/Booster/Definition/Base.hs @@ -47,6 +47,7 @@ data KoreDefinition = KoreDefinition , rewriteTheory :: Theory (RewriteRule "Rewrite") , functionEquations :: Theory (RewriteRule "Function") , simplifications :: Theory (RewriteRule "Simplification") + , existentialSimplifications :: Theory (RewriteRule "ExistentialSimplification") , ceils :: Theory (RewriteRule "Ceil") } deriving stock (Eq, Show, GHC.Generic) @@ -67,6 +68,7 @@ emptyKoreDefinition attributes = , rewriteTheory = Map.empty , functionEquations = Map.empty , simplifications = Map.empty + , existentialSimplifications = Map.empty , ceils = Map.empty } diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index 39dd2cacc3..9d29a4291e 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/booster/library/Booster/Pattern/Bool.hs @@ -17,6 +17,7 @@ module Booster.Pattern.Bool ( pattern AndBool, pattern EqualsInt, pattern EqualsBool, + pattern LtInt, pattern NEqualsInt, pattern EqualsK, pattern NEqualsK, @@ -102,7 +103,15 @@ pattern NotBool t = [] [t] -pattern EqualsInt, EqualsBool, NEqualsInt, EqualsK, NEqualsK, SetIn :: Term -> Term -> Term +pattern + EqualsInt + , EqualsBool + , LtInt + , NEqualsInt + , EqualsK + , NEqualsK + , SetIn :: + Term -> Term -> Term pattern EqualsInt a b = SymbolApplication ( Symbol @@ -114,6 +123,17 @@ pattern EqualsInt a b = ) [] [a, b] +pattern LtInt a b = + SymbolApplication + ( Symbol + "Lbl'Unds-LT-'Int'Unds'" + [] + [SortInt, SortInt] + SortBool + (HookedTotalFunctionWithSMT "INT.lt" "<") + ) + [] + [a, b] pattern EqualsBool a b = SymbolApplication ( Symbol diff --git a/booster/library/Booster/Pattern/PartialOrder.hs b/booster/library/Booster/Pattern/PartialOrder.hs new file mode 100644 index 0000000000..a01998b7b9 --- /dev/null +++ b/booster/library/Booster/Pattern/PartialOrder.hs @@ -0,0 +1,61 @@ +{-# LANGUAGE PatternSynonyms #-} + +{- | +Copyright : (c) Runtime Verification, 2024 +License : BSD-3-Clause +-} +module Booster.Pattern.PartialOrder (transitiveClosure) where + +import Control.Monad (guard) +import Data.Maybe (mapMaybe) +import Data.Set (Set) +import Data.Set qualified as Set + +import Booster.Pattern.Base + +{- | Given a set of predicates @ps@, construct a syntactic transitive closure of relative to the symbol @sym@. + + This function only returns new predicates (if any). + + If the @ps@ contains application of symbols other than @sym@, they are ignored. +-} +transitiveClosure :: Symbol -> Set Predicate -> Set Predicate +transitiveClosure sym ps = + let attempts = map (\target -> Attempt target (Set.toList (Set.delete target ps))) . Set.toList $ ps + in (Set.fromList . concatMap (makeTransitiveStep sym) $ attempts) + +-- | An @Attempt@ is a target clause and a list of assumption clauses +data Attempt = Attempt + { target :: !Predicate + -- ^ target predicate to eliminate, contains an existential variable + , assumptions :: ![Predicate] + -- ^ predicates that are assume "known", must contain the same existential that the target + } + +{- | Validate a predicate clause. Checks: + * the clause is a symbol application of @sym@ + * the variables have distinct names, i.e. @sym@ is irreflexive +-} +validateClause :: Symbol -> Predicate -> Bool +validateClause sym (Predicate p) = case p of + (SymbolApplication clauseSym _ [(Var Variable{variableName = a}), (Var Variable{variableName = b})]) -> clauseSym == sym && a /= b + _ -> False + +-- | Try solving, return an instantiated target if successful +makeTransitiveStep :: Symbol -> Attempt -> [Predicate] +makeTransitiveStep sym Attempt{target, assumptions} = do + guard (all (validateClause sym) (target : assumptions)) + mapMaybe (matchAndTransit sym target) assumptions + +{- | Try to make strengthen the @left@ predicate using the @right@ predicate, + assuming both are the same *transitive* symbol +-} +matchAndTransit :: Symbol -> Predicate -> Predicate -> Maybe Predicate +matchAndTransit sym (Predicate current) (Predicate next) = + case (current, next) of + (SymbolApplication symbol1 sorts [a, b], SymbolApplication symbol2 _ [c, d]) -> do + guard (symbol1 == symbol2 && b == c) + let newClause = Predicate $ SymbolApplication symbol1 sorts [a, d] + guard (validateClause sym newClause) + pure newClause + _ -> Nothing diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index bb703792fa..0fe5b7958f 100644 --- a/booster/library/Booster/Pattern/Util.hs +++ b/booster/library/Booster/Pattern/Util.hs @@ -30,6 +30,7 @@ module Booster.Pattern.Util ( cellVariableStats, stripMarker, markAsExVar, + isExVar, markAsRuleVar, incrementNameCounter, ) where @@ -125,6 +126,9 @@ markAsRuleVar = ("Rule#" <>) markAsExVar :: VarName -> VarName markAsExVar = ("Ex#" <>) +isExVar :: VarName -> Bool +isExVar = BS.isPrefixOf "Ex#" + {- | Strip variable provenance prefixes introduced using "markAsRuleVar" and "markAsExVar" in "Syntax.ParsedKore.Internalize" -} diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 2171578a16..1078c780e5 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -181,6 +181,7 @@ mergeDefs k1 k2 <*> pure (mergeTheories rewriteTheory k1 k2) <*> pure (mergeTheories functionEquations k1 k2) <*> pure (mergeTheories simplifications k1 k2) + <*> pure (mergeTheories existentialSimplifications k1 k2) <*> pure (mergeTheories ceils k1 k2) where mergeTheories :: @@ -235,6 +236,7 @@ addModule , rewriteTheory = currentRewriteTheory , functionEquations = currentFctEqs , simplifications = currentSimpls + , existentialSimplifications = currentExistentialSimplifications , ceils = currentCeils } ) @@ -296,6 +298,7 @@ addModule , rewriteTheory = currentRewriteTheory -- no rules yet , functionEquations = Map.empty , simplifications = Map.empty + , existentialSimplifications = Map.empty , ceils = Map.empty } @@ -352,6 +355,7 @@ addModule subsortPairs = mapMaybe retractSubsortRule newAxioms newFunctionEquations = mapMaybe retractFunctionRule newAxioms newSimplifications = mapMaybe retractSimplificationRule newAxioms + newExistentialSimplifications = mapMaybe retractExistentialSimplificationRule newAxioms newCeils = mapMaybe retractCeilRule newAxioms let rewriteIndex = if null defAttributes.indexCells @@ -363,6 +367,11 @@ addModule addToTheoryWith (Idx.termTopIndex . (.lhs)) newFunctionEquations currentFctEqs simplifications = addToTheoryWith (Idx.termTopIndex . (.lhs)) newSimplifications currentSimpls + existentialSimplifications = + addToTheoryWith + (Idx.termTopIndex . (.lhs)) + newExistentialSimplifications + currentExistentialSimplifications ceils = addToTheoryWith (Idx.termTopIndex . (.lhs)) newCeils currentCeils sorts = @@ -374,6 +383,7 @@ addModule , rewriteTheory , functionEquations , simplifications + , existentialSimplifications , ceils } where @@ -534,6 +544,8 @@ data AxiomResult FunctionAxiom (RewriteRule "Function") | -- | Simplification SimplificationAxiom (RewriteRule "Simplification") + | -- | Existential simplification + ExistentialSimplificationAxiom (RewriteRule "ExistentialSimplification") | -- | Ceil rule CeilAxiom (RewriteRule "Ceil") @@ -554,6 +566,11 @@ retractSimplificationRule :: AxiomResult -> Maybe (RewriteRule "Simplification") retractSimplificationRule (SimplificationAxiom r) = Just r retractSimplificationRule _ = Nothing +retractExistentialSimplificationRule :: + AxiomResult -> Maybe (RewriteRule "ExistentialSimplification") +retractExistentialSimplificationRule (ExistentialSimplificationAxiom r) = Just r +retractExistentialSimplificationRule _ = Nothing + retractCeilRule :: AxiomResult -> Maybe (RewriteRule "Ceil") retractCeilRule (CeilAxiom r) = Just r retractCeilRule _ = Nothing diff --git a/booster/unit-tests/Test/Booster/Fixture.hs b/booster/unit-tests/Test/Booster/Fixture.hs index d0f527473a..e655150a0c 100644 --- a/booster/unit-tests/Test/Booster/Fixture.hs +++ b/booster/unit-tests/Test/Booster/Fixture.hs @@ -67,6 +67,7 @@ testDefinition = , rewriteTheory = Map.empty , functionEquations = Map.empty , simplifications = Map.empty + , existentialSimplifications = Map.empty , ceils = Map.empty } where diff --git a/booster/unit-tests/Test/Booster/Pattern/PartialOrder.hs b/booster/unit-tests/Test/Booster/Pattern/PartialOrder.hs new file mode 100644 index 0000000000..073a853223 --- /dev/null +++ b/booster/unit-tests/Test/Booster/Pattern/PartialOrder.hs @@ -0,0 +1,77 @@ +module Test.Booster.Pattern.PartialOrder ( + test_transitiveClosure, +) where + +import Data.Set qualified as Set +import Test.Tasty +import Test.Tasty.HUnit + +import Booster.Pattern.Base +import Booster.Pattern.Bool +import Booster.Pattern.PartialOrder + +test_transitiveClosure :: TestTree +test_transitiveClosure = + testGroup + " Symbol -> [Term] -> [Term] -> TestTree +test name sym input expected = + testCase name $ + transitiveClosure sym (Set.fromList $ map Predicate input) + @?= (Set.fromList $ map Predicate expected) + +ltIntSymbol :: Symbol +ltIntSymbol = + case LtInt (var "DUMMY") (var "DUMMY") of + SymbolApplication ltInt _ _ -> ltInt + _ -> error "Impossible" + +someSort :: Sort +someSort = SortApp "SomeSort" [] + +var :: VarName -> Term +var variableName = Var $ Variable{variableSort = someSort, variableName}