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/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index d0702697ba..5b963179f6 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -26,6 +26,7 @@ module Booster.Pattern.ApplyEquations ( evaluateConstraints, ) where +import Booster.Pattern.Existential (instantiateExistentialsMany) import Control.Exception qualified as Exception (throw) import Control.Monad import Control.Monad.Extra (fromMaybeM, whenJust) @@ -39,7 +40,7 @@ import Data.Bifunctor (bimap) import Data.ByteString.Char8 qualified as BS import Data.Coerce (coerce) import Data.Data (Data, Proxy) -import Data.Foldable (toList, traverse_) +import Data.Foldable (foldl', toList, traverse_) import Data.List (foldl1', intersperse, partition) import Data.List.NonEmpty qualified as NonEmpty import Data.Map (Map) @@ -726,6 +727,7 @@ applyEquation term rule = getPrettyModifiers >>= \case ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do -- ensured by internalisation: no existentials in equations + -- TODO allow existentials, but only in the requires clause unless (null rule.existentials) $ do withContext CtxAbort $ logMessage ("Equation with existentials" :: Text) @@ -804,7 +806,55 @@ applyEquation term rule = -- If the required condition is _syntactically_ present in -- the prior (known constraints), we don't check it. knownPredicates <- (.predicates) <$> lift getState - toCheck <- lift $ filterOutKnownConstraints knownPredicates required + + let partitionExistentialRequires :: [Predicate] -> ([Predicate], [Predicate]) + partitionExistentialRequires = foldl' decide ([], []) + where + decide (hasEx, noHasEx) p + | hasExistentials p = (p : hasEx, noHasEx) + | otherwise = (hasEx, p : noHasEx) + + hasExistentials :: Predicate -> Bool + hasExistentials (Predicate t) = any (isExVar . (.variableName)) (freeVariables t) + + listExistentials :: Predicate -> Set VarName + listExistentials (Predicate t) = Set.filter isExVar . Set.map (.variableName) . freeVariables $ t + + -- If we get an equation with existentials in the requires clause, we must have them all instantiated + let (predicateWithEx, predicatesWithNoEx) = partitionExistentialRequires required + instantiatedExistentialPredicates = instantiateExistentialsMany knownPredicates predicateWithEx + + -- detect if any existentials still remain + when (any hasExistentials instantiatedExistentialPredicates) $ do + -- what to do here? Abort equation or simply throw away the clauses with existentials? + -- Let's abort for now. + let remainingExistentials = + Set.toList . Set.map Text.decodeLatin1 . Set.unions . map listExistentials $ + instantiatedExistentialPredicates + + withContext CtxAbort $ + logMessage $ + "Could not instantiate existentials: " <> (Text.intercalate "," remainingExistentials) + + -- all existentials are instantiated: assemble the requires clause again + let requiredWithInstantiatedExistentials = predicatesWithNoEx <> instantiatedExistentialPredicates + + -- TODO these logs need to either go or be assigned a more specific context + withContext CtxConstraint . withContext CtxDetail $ do + logMessage $ + renderOneLineText $ + "Requires clause after substitution:" + <+> hsep (intersperse "," $ map (pretty' @mods) required) + logMessage $ + renderOneLineText $ + "Known predicates:" + <+> hsep (intersperse "," $ map (pretty' @mods) (Set.toList knownPredicates)) + logMessage $ + renderOneLineText $ + "Requires clause predicate after instantiating existential:" + <+> hsep (intersperse "," $ map (pretty' @mods) requiredWithInstantiatedExistentials) + + toCheck <- lift $ filterOutKnownConstraints knownPredicates requiredWithInstantiatedExistentials -- check the filtered requires clause conditions unclearConditions <- diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index 39dd2cacc3..5162dacbba 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/booster/library/Booster/Pattern/Bool.hs @@ -16,6 +16,7 @@ module Booster.Pattern.Bool ( pattern NotBool, pattern AndBool, pattern EqualsInt, + pattern LtInt, pattern EqualsBool, pattern NEqualsInt, pattern EqualsK, @@ -102,7 +103,7 @@ pattern NotBool t = [] [t] -pattern EqualsInt, EqualsBool, NEqualsInt, EqualsK, NEqualsK, SetIn :: Term -> Term -> Term +pattern EqualsInt, EqualsBool, NEqualsInt, LtInt, EqualsK, NEqualsK, SetIn :: Term -> Term -> Term pattern EqualsInt a b = SymbolApplication ( Symbol @@ -136,6 +137,17 @@ pattern NEqualsInt a b = ) [] [a, b] +pattern LtInt a b = + SymbolApplication + ( Symbol + "Lbl'Unds-LT-'Int'Unds'" + [] + [SortInt, SortInt] + SortBool + (HookedTotalFunctionWithSMT "INT.lt" "<") + ) + [] + [a, b] pattern EqualsK a b = SymbolApplication ( Symbol diff --git a/booster/library/Booster/Pattern/Existential.hs b/booster/library/Booster/Pattern/Existential.hs new file mode 100644 index 0000000000..422b71855b --- /dev/null +++ b/booster/library/Booster/Pattern/Existential.hs @@ -0,0 +1,74 @@ +{- | +Copyright : (c) Runtime Verification, 2024 +License : BSD-3-Clause +-} +module Booster.Pattern.Existential (matchExistential, instantiateExistentials, instantiateExistentialsMany) where + +import Control.Monad (guard, when) +import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.Maybe +import Control.Monad.Trans.State.Strict +import Data.Coerce (coerce) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe (fromJust) +import Data.Set (Set) +import Data.Set qualified as Set + +import Booster.Pattern.Base +import Booster.Pattern.Util + +{- | Given a set of @known@ predicates, which must not contains any existential variables, + attempt to instantiate the existential in the @target@ predicate using the following method: + * generate a list of candidate substitutions by matching with every known predicate individually + * collapse all substitutions into one, resolving any conflicts left-to-right, i.e. if a variable + is bound, it is /not/ updated +-} +instantiateExistentials :: Set Predicate -> Predicate -> (Predicate, Substitution) +instantiateExistentials known target@(Predicate targetTerm) = + let candidates = map (matchExistential target) (Set.toList known) + combinedSubst = Map.unions candidates + in (Predicate $ substituteInTerm combinedSubst targetTerm, combinedSubst) + +type Substitution = Map Variable Term + +{- | Apply @instantiateExistentials@ to a list of predicates: + - apply to the head to instantiate existentials and get the substitution + - apply the substitution to the tail and call recursively +-} +instantiateExistentialsMany :: Set Predicate -> [Predicate] -> [Predicate] +instantiateExistentialsMany known = reverse . go [] + where + go :: [Predicate] -> [Predicate] -> [Predicate] + go acc = \case + [] -> acc + (p : ps) -> + let (p', subst) = instantiateExistentials known p + in go (p' : acc) (map (coerce . substituteInTerm subst . coerce) ps) + +{- | Given a @target@ predicate, which may contain existential variables, + and a @known@ predicate, which must not, attempt to instantiate the first with the second +-} +matchExistential :: Predicate -> Predicate -> Substitution +matchExistential target known = + flip execState Map.empty . runMaybeT $ matchExistentialImpl target known + +matchExistentialImpl :: Predicate -> Predicate -> MaybeT (State Substitution) () +matchExistentialImpl (Predicate target) (Predicate known) = + case (target, known) of + (SymbolApplication symbol1 _ [a, b], SymbolApplication symbol2 _ [c, d]) -> do + guard (symbol1 == symbol2) + tryBindExVar a c + tryBindExVar b d + _ -> fail "Not a symbol application" + where + tryBindExVar :: Term -> Term -> MaybeT (State Substitution) () + tryBindExVar variable term = do + when (isExistentialVariable variable) $ do + let variableVar = fromJust . retractVariable $ variable + lift $ modify (Map.insert variableVar term) + +isExistentialVariable :: Term -> Bool +isExistentialVariable = \case + Var v -> isExVar v.variableName + _ -> False diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index bb703792fa..1cb9278596 100644 --- a/booster/library/Booster/Pattern/Util.hs +++ b/booster/library/Booster/Pattern/Util.hs @@ -13,6 +13,7 @@ module Booster.Pattern.Util ( modifyVarName, modifyVarNameConcreteness, freeVariables, + retractVariable, isConstructorSymbol, isFunctionSymbol, isDefinedSymbol, @@ -30,6 +31,7 @@ module Booster.Pattern.Util ( cellVariableStats, stripMarker, markAsExVar, + isExVar, markAsRuleVar, incrementNameCounter, ) where @@ -125,6 +127,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" -} @@ -200,6 +205,11 @@ modifyVarNameConcreteness f = \case freeVariables :: Term -> Set Variable freeVariables (Term attributes _) = attributes.variables +retractVariable :: Term -> Maybe Variable +retractVariable = \case + (Var v) -> Just v + _ -> Nothing + isConcrete :: Term -> Bool isConcrete = Set.null . freeVariables diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 7f3bda4c3d..34dbd590d7 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -182,6 +182,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 :: @@ -236,6 +237,7 @@ addModule , rewriteTheory = currentRewriteTheory , functionEquations = currentFctEqs , simplifications = currentSimpls + , existentialSimplifications = currentExistentialSimplifications , ceils = currentCeils } ) @@ -297,6 +299,7 @@ addModule , rewriteTheory = currentRewriteTheory -- no rules yet , functionEquations = Map.empty , simplifications = Map.empty + , existentialSimplifications = Map.empty , ceils = Map.empty } @@ -353,6 +356,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 @@ -364,6 +368,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 = @@ -375,6 +384,7 @@ addModule , rewriteTheory , functionEquations , simplifications + , existentialSimplifications , ceils } where @@ -535,6 +545,8 @@ data AxiomResult FunctionAxiom (RewriteRule "Function") | -- | Simplification SimplificationAxiom (RewriteRule "Simplification") + | -- | Existential simplification + ExistentialSimplificationAxiom (RewriteRule "ExistentialSimplification") | -- | Ceil rule CeilAxiom (RewriteRule "Ceil") @@ -555,6 +567,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 @@ -750,11 +767,17 @@ extractExistentials = \case <$> extractExistentials arg other -> (other, []) +-- | Useful for getting the requires clause of a simplification axiom, i.e. throwing away the \in conjuncts +getFirstConjunct :: Syntax.KorePattern -> Syntax.KorePattern +getFirstConjunct = \case + Syntax.KJAnd{patterns = (headConjunct : _)} -> headConjunct + other -> other + internaliseAxiom :: PartialDefinition -> ParsedAxiom -> Except DefinitionError (Maybe AxiomResult) -internaliseAxiom (Partial partialDefinition) parsedAxiom = +internaliseAxiom (Partial partialDefinition) parsedAxiom = do classifyAxiom parsedAxiom >>= maybe (pure Nothing) processAxiom where processAxiom :: AxiomData -> Except DefinitionError (Maybe AxiomResult) @@ -837,7 +860,10 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do -- to avoid name clashes with patterns from the user; -- filter out literal `Top` constraints lhs <- internalisePattern' ref (Util.modifyVarName Util.markAsRuleVar) left - existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs + existentials' <- + fmap Set.fromList $ + withExcept (DefinitionPatternError ref) $ + mapM (mkVar partialDefinition right) exs let renameVariable v | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v @@ -878,10 +904,11 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do DefinitionPatternError ref (NotSupported (head unsupported)) pure $ removeTrueBools $ Util.modifyVariables f pat - mkVar (name, sort) = do - variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort - let variableName = textToBS name.getId - pure $ Variable{variableSort, variableName} +mkVar :: KoreDefinition -> Syntax.KorePattern -> (Id, Sort) -> Except PatternError Variable +mkVar partialDefinition right (name, sort) = do + variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort + let variableName = textToBS name.getId + pure $ Variable{variableSort, variableName} internaliseRewriteRule :: KoreDefinition -> @@ -912,7 +939,10 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu fmap (removeTrueBools . Util.modifyVariables (Util.modifyVarName Util.markAsRuleVar)) $ retractPattern result `orFailWith` DefinitionTermOrPredicateError ref (PatternExpected result) - existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs + existentials' <- + fmap Set.fromList $ + withExcept (DefinitionPatternError ref) $ + mapM (mkVar partialDefinition right) exs let renameVariable v | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v @@ -946,11 +976,6 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu , existentials } where - mkVar (name, sort) = do - variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort - let variableName = textToBS name.getId - pure $ Variable{variableSort, variableName} - internalisePattern' ref f t = do (pat, substitution, unsupported) <- withExcept (DefinitionPatternError ref) $ @@ -1011,8 +1036,18 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs | not (coerce attrs.simplification) = error $ "internaliseSimpleEquation should only be called for simplifications" <> show attrs | Syntax.KJApp{} <- left = do + -- extract the top-level existentials from precond and strip them + let (precondNoExists, existentials) = Debug.trace (show precond) $ extractExistentials (getFirstConjunct precond) + + let ref = Debug.trace (show precondNoExists) $ sourceRef attrs + + existentials' <- + fmap Set.fromList $ + withExcept (DefinitionPatternError ref) $ + mapM (mkVar partialDef left) existentials + -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom) - lhs <- internalisePattern' $ Syntax.KJAnd left.sort [left, precond] + lhs <- internalisePattern' $ Syntax.KJAnd left.sort [left, precondNoExists] rhs <- internalisePattern' right let -- checking the lhs term, too, as a safe approximation @@ -1040,7 +1075,7 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs , ensures = rhs.constraints , attributes , computedAttributes - , existentials = Set.empty + , existentials = existentials' } | otherwise = -- we hit a simplification with top level ML connective or an diff --git a/booster/test/llvm-integration/LLVM.hs b/booster/test/llvm-integration/LLVM.hs index a6b335fa39..59e68610bb 100644 --- a/booster/test/llvm-integration/LLVM.hs +++ b/booster/test/llvm-integration/LLVM.hs @@ -310,6 +310,7 @@ testDef = Map.empty -- no rules Map.empty -- no function equations Map.empty -- no simplifications + Map.empty -- no existential rules Map.empty -- no ceils {- To refresh the definition below, run this using the repl and fix up 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/Existential.hs b/booster/unit-tests/Test/Booster/Pattern/Existential.hs new file mode 100644 index 0000000000..7c4c654699 --- /dev/null +++ b/booster/unit-tests/Test/Booster/Pattern/Existential.hs @@ -0,0 +1,292 @@ +{-# LANGUAGE QuasiQuotes #-} + +module Test.Booster.Pattern.Existential ( + test_matchExistential, + test_instantiateExistentials, + test_instantiateExistentialsMany, + test_applyExSimplification, +) where + +import Control.Monad.Logger (runNoLoggingT, runStderrLoggingT) +import Control.Monad.Trans.Reader (runReaderT) +import Data.Coerce (coerce) +import Data.Map (Map) +import Data.Map qualified as Map +import Data.Proxy (Proxy (..)) +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Text (Text) +import GHC.IO.Unsafe (unsafePerformIO) +import Test.Tasty +import Test.Tasty.HUnit + +import Booster.Definition.Attributes.Base +import Booster.Definition.Base +import Booster.Log +import Booster.Pattern.ApplyEquations (Direction (..), evaluateTerm) +import Booster.Pattern.Base +import Booster.Pattern.Bool +import Booster.Pattern.Existential +import Booster.Pattern.Index (CellIndex (..), TermIndex (..)) +import Booster.Pattern.Pretty +import Booster.Pattern.Util (markAsExVar, modifyVarName, modifyVariablesInT) +import Booster.Syntax.Json.Internalise (trm) +import Booster.Syntax.ParsedKore.Internalise (symb) +import Booster.Util (Flag (..), withFastLogger) +import Test.Booster.Fixture hiding (inj, var) + +test_matchExistential :: TestTree +test_matchExistential = + testGroup + "matchExistential" + [ testGroup + "positive cases -- non-empty substitution" + [ test + "One existential -- one binding, left" + (Predicate $ LtInt (varTerm "Ex#A") (varTerm "B")) + (Predicate $ LtInt (varTerm "C") (varTerm "D")) + ( Map.fromList [(var "Ex#A", varTerm "C")] + ) + , test + "One existential -- one binding, right" + (Predicate $ LtInt (varTerm "A") (varTerm "Ex#B")) + (Predicate $ LtInt (varTerm "C") (varTerm "D")) + ( Map.fromList [(var "Ex#B", varTerm "D")] + ) + , test + "Two existentials -- two bindings" + (Predicate $ LtInt (varTerm "Ex#A") (varTerm "Ex#B")) + (Predicate $ LtInt (varTerm "C") (varTerm "D")) + ( Map.fromList [(var "Ex#A", varTerm "C"), (var "Ex#B", varTerm "D")] + ) + ] + , testGroup + "negative cases -- empty substitution" + [ test + "No existentials" + (Predicate $ LtInt (varTerm "A") (varTerm "B")) + (Predicate $ LtInt (varTerm "C") (varTerm "D")) + (Map.empty) + , test + "Different symbols" + (Predicate $ LtInt (varTerm "Ex#A") (varTerm "Ex#B")) + (Predicate $ EqualsInt (varTerm "C") (varTerm "D")) + (Map.empty) + , test + "Malformed target -- not a symbol application" + (Predicate $ varTerm "A") + (Predicate $ LtInt (varTerm "C") (varTerm "D")) + (Map.empty) + , test + "Malformed known -- not a symbol application" + (Predicate $ LtInt (varTerm "Ex#C") (varTerm "D")) + (Predicate $ varTerm "A") + (Map.empty) + ] + ] + where + test :: String -> Predicate -> Predicate -> Map Variable Term -> TestTree + test name target known expected = + testCase name $ + matchExistential target known + @?= expected + +test_instantiateExistentials :: TestTree +test_instantiateExistentials = + testGroup + "instantiateExistentials" + [ testGroup + "positive cases -- changed predicate" + [ test + "Earlier bindings are preferred" + (Predicate $ LtInt (varTerm "Ex#A") (varTerm "Ex#B")) + [ Predicate $ LtInt (varTerm "C1") (varTerm "D1") + , Predicate $ LtInt (varTerm "C2") (varTerm "D2") + ] + (Predicate $ LtInt (varTerm "C1") (varTerm "D1")) + , test + "Can ignore non-matching known" + (Predicate $ LtInt (varTerm "Ex#A") (varTerm "Ex#B")) + [ Predicate $ EqualsInt (varTerm "C1") (varTerm "D1") + , Predicate $ LtInt (varTerm "C2") (varTerm "D2") + ] + (Predicate $ LtInt (varTerm "C2") (varTerm "D2")) + ] + , testGroup + "negative cases -- same predicate" + [ test + "No matching known" + (Predicate $ LtInt (varTerm "Ex#A") (varTerm "Ex#B")) + [ Predicate $ EqualsInt (varTerm "C1") (varTerm "D1") + , Predicate $ EqualsInt (varTerm "C2") (varTerm "D2") + ] + (Predicate $ LtInt (varTerm "Ex#A") (varTerm "Ex#B")) + , test + "No existentials" + (Predicate $ LtInt (varTerm "A") (varTerm "B")) + [ Predicate $ EqualsInt (varTerm "C1") (varTerm "D1") + , Predicate $ EqualsInt (varTerm "C2") (varTerm "D2") + ] + (Predicate $ LtInt (varTerm "A") (varTerm "B")) + ] + ] + where + test :: String -> Predicate -> [Predicate] -> Predicate -> TestTree + test name target known expected = + testCase name $ + let (actual, _subst) = instantiateExistentials (Set.fromList known) target + in actual @?= expected + +test_instantiateExistentialsMany :: TestTree +test_instantiateExistentialsMany = + testGroup + "instantiateExistentialsMany" + [ testGroup + "positive cases -- changed predicate" + [ test + "Earlier bindings are preferred, learned occurrences in consecrative predicates are substituted" + [Predicate $ LtInt (varTerm "A") (varTerm "Ex#B"), Predicate $ LtInt (varTerm "Ex#B") (varTerm "C")] + [ Predicate $ LtInt (varTerm "A") (varTerm "D") + ] + [Predicate $ LtInt (varTerm "A") (varTerm "D"), Predicate $ LtInt (varTerm "D") (varTerm "C")] + ] + ] + where + test :: String -> [Predicate] -> [Predicate] -> [Predicate] -> TestTree + test name targets known expected = + testCase name $ + let actual = instantiateExistentialsMany (Set.fromList known) targets + in actual @?= expected + +{-# NOINLINE test_applyExSimplification #-} +test_applyExSimplification :: TestTree +test_applyExSimplification = + testGroup + "Applying an existential simplification" + [ testCase "No known predicates, no simplification" $ do + simpl + BottomUp + [trm| rel1{}(ConfX:SomeSort{}, ConfZ:SomeSort{}) |] + [] + @?= Right [trm| rel1{}(ConfX:SomeSort{}, ConfZ:SomeSort{}) |] + , testCase + "Known predicate instantiates the conjuncts, but we don't have reflexivity of rel2, simplification is not applied" + $ do + simpl + BottomUp + [trm| rel1{}(ConfX:SomeSort{}, ConfY:SomeSort{}) |] + [ Predicate [trm| rel2{}(ConfX:SomeSort{}, ConfY:SomeSort{}) |] + ] + @?= Right [trm| rel1{}(ConfX:SomeSort{}, ConfY:SomeSort{}) |] + , testCase + "Known predicate instantiates the conjuncts, simplification is not applied, using the extra known condition" + $ do + simpl + BottomUp + [trm| rel1{}(ConfX:SomeSort{}, ConfY:SomeSort{}) |] + [ Predicate [trm| rel2{}(ConfX:SomeSort{}, ConfY:SomeSort{}) |] + , Predicate [trm| rel2{}(ConfX:SomeSort{}, ConfX:SomeSort{}) |] + ] + @?= Right [trm| rel3{}(ConfX:SomeSort{}, ConfY:SomeSort{}) |] + ] + where + -- FIXME this function logs to stderr. I find it useful to be able to see the logs when debugging unit tests, but we likely need to make it opt-in. + simpl direction x knownPredicates = unsafePerformIO $ + withFastLogger Nothing Nothing $ \stderrLogger _ -> + flip runReaderT (textLogger stderrLogger, ModifiersRep @'[] Proxy) $ + unLoggerT $ + (fst <$>) $ + evaluateTerm direction exSimplDef Nothing Nothing (Set.fromList knownPredicates) x + +---------------------------------------- + +var :: VarName -> Variable +var variableName = Variable{variableSort = someSort, variableName} + +varTerm :: VarName -> Term +varTerm variableName = Var $ Variable{variableSort = someSort, variableName} + +---------------------------------------- + +{- | This is a hacky helper to construct an equation with existentials in the requires clause. + The requires clause is traversed and the the variables given in @exVarNames@ are prefixed with Ex#. + TODO: refactor once we do not need to bypass the internalisation checks. +-} +equationExRequires :: + Maybe Text -> Term -> Term -> [Predicate] -> [VarName] -> Priority -> RewriteRule t +equationExRequires ruleLabel lhs rhs requires exVarNames priority = + RewriteRule + { lhs = lhs + , rhs = rhs + , requires = + Set.fromList $ + map + ( coerce + . modifyVariablesInT + (modifyVarName (\name -> if name `elem` exVarNames then markAsExVar name else name)) + . coerce + ) + requires + , ensures = mempty + , attributes = + AxiomAttributes + { location = Nothing + , priority + , ruleLabel + , simplification = Flag True + , preserving = Flag False + , concreteness = Unconstrained + , uniqueId = maybe mockUniqueId UniqueId ruleLabel + , smtLemma = Flag False + } + , computedAttributes = ComputedAxiomAttributes False [] + , existentials = mempty -- intentionally left blank to bypass the checks in ApplyEquations.hs + } + +exSimplDef :: KoreDefinition +exSimplDef = + defWithSymbols + { simplifications = + mkTheory + [ + ( index "rel1" + , + [ equationExRequires -- rel1(X, Y) => rel3(X, Y) requires [rel2(X,?C), rel2(?C,Y)] + (Just "rel1-rel3-ex") + [trm| rel1{}(EqX:SomeSort{}, EqY:SomeSort{}) |] + [trm| rel3{}(EqX:SomeSort{}, EqY:SomeSort{}) |] + ( [ Predicate [trm| rel2{}(EqX:SomeSort{}, EqC:SomeSort{}) |] + , Predicate [trm| rel2{}(EqC:SomeSort{}, EqY:SomeSort{}) |] + ] + ) + ["EqC"] + 50 + ] + ) + ] + } + where + defWithSymbols = + testDefinition + { symbols = + testDefinition.symbols + <> Map.fromList + [("rel1", rel1)] + } + +rel1, rel2, rel3 :: Symbol +rel1 = [symb| symbol rel1{}(SomeSort{}, SomeSort{}) : SomeSort{} [function{}(), total{}()] |] +rel2 = [symb| symbol rel2{}(SomeSort{}, SomeSort{}) : SomeSort{} [function{}(), total{}()] |] +rel3 = [symb| symbol rel3{}(SomeSort{}, SomeSort{}) : SomeSort{} [function{}(), total{}()] |] + +mkTheory :: [(TermIndex, [RewriteRule t])] -> Theory (RewriteRule t) +mkTheory = Map.map mkPriorityGroups . Map.fromList + where + mkPriorityGroups :: [RewriteRule t] -> Map Priority [RewriteRule t] + mkPriorityGroups rules = + Map.unionsWith + (<>) + [Map.fromList [(r.attributes.priority, [r])] | r <- rules] + +index :: SymbolName -> TermIndex +index = TermIndex . (: []) . TopSymbol