Skip to content

Commit

Permalink
Substitute in the internalisation functions directly
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a committed Oct 23, 2024
1 parent 9bcdc52 commit 58f6402
Show file tree
Hide file tree
Showing 3 changed files with 55 additions and 56 deletions.
14 changes: 4 additions & 10 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,8 @@ respond stateVar request =
[ req.logSuccessfulRewrites
, req.logFailedRewrites
]
-- apply the given substitution before doing anything else
-- apply the given substitution before doing anything else,
-- as internalisePattern does not substitute
let substPat =
Pattern
{ term = Substitution.substituteInTerm substitution term
Expand Down Expand Up @@ -245,19 +246,12 @@ respond stateVar request =
RpcError.CouldNotVerifyPattern $
map patternErrorToRpcError patternErrors
-- term and predicate (pattern)
-- NOTE: the input substitution will have already been applied by internaliseTermOrPredicate
Right (TermAndPredicates pat unsupported) -> do
unless (null unsupported) $ do
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
logMessage ("ignoring unsupported predicate parts" :: Text)
-- apply the given substitution before doing anything else
let substPat =
Pattern
{ term = Substitution.substituteInTerm pat.substitution pat.term
, constraints = Set.map (Substitution.substituteInPredicate pat.substitution) pat.constraints
, ceilConditions = pat.ceilConditions
, substitution = pat.substitution
}
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \case
(Right newPattern, _) -> do
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
tSort = externaliseSort (sortOfPattern newPattern)
Expand Down
59 changes: 20 additions & 39 deletions booster/library/Booster/Pattern/Implies.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ import Booster.Pattern.Base (Pattern (..), Predicate (..))
import Booster.Pattern.Bool (pattern TrueBool)
import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (Implies), matchTerms)
import Booster.Pattern.Pretty (FromModifiersT, ModifiersRep (..), pretty')
import Booster.Pattern.Substitution qualified as Substitution
import Booster.Pattern.Substitution (asEquations)
import Booster.Pattern.Util (freeVariables, sortOfPattern)
import Booster.Prettyprinter (renderDefault)
import Booster.SMT.Interface qualified as SMT
Expand Down Expand Up @@ -107,43 +107,26 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
map (pack . show) $
unsupportedL <> unsupportedR
| otherwise -> do
let
-- apply the given substitution before doing anything else
substPatL =
Pattern
{ term = Substitution.substituteInTerm substitutionL patL.term
, constraints = Set.map (Substitution.substituteInPredicate substitutionL) patL.constraints
, ceilConditions = patL.ceilConditions
, substitution = substitutionL
}
substPatR =
Pattern
{ term = Substitution.substituteInTerm substitutionR patR.term
, constraints = Set.map (Substitution.substituteInPredicate substitutionR) patR.constraints
, ceilConditions = patR.ceilConditions
, substitution = substitutionR
}

SMT.isSat solver (Set.toList substPatL.constraints) substPatL.substitution >>= \case
SMT.isSat solver (Set.toList patL.constraints) patL.substitution >>= \case
SMT.IsUnsat ->
let sort = externaliseSort $ sortOfPattern substPatL
let sort = externaliseSort $ sortOfPattern patL
in implies' (Kore.Syntax.KJBottom sort) sort antecedent.term consequent.term mempty
_ -> checkImpliesMatchTerms existsL substPatL existsR substPatR
_ -> checkImpliesMatchTerms existsL patL existsR patR

checkImpliesMatchTerms existsL substPatL existsR substPatR =
case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of
checkImpliesMatchTerms existsL patL existsR patR =
case matchTerms Booster.Pattern.Match.Implies def patR.term patL.term of
MatchFailed (SubsortingError sortError) ->
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
show sortError
MatchFailed{} ->
doesNotImply
(sortOfPattern substPatL)
(externaliseExistTerm existsL substPatL.term)
(externaliseExistTerm existsR substPatR.term)
(sortOfPattern patL)
(externaliseExistTerm existsL patL.term)
(externaliseExistTerm existsR patR.term)
MatchIndeterminate remainder ->
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty patL >>= \case
(Right simplifedSubstPatL, _) ->
if substPatL == simplifedSubstPatL
if patL == simplifedSubstPatL
then -- we are being conservative here for now and returning an error.
-- since we have already simplified the LHS, we may want to eventually return implise, but the condition
-- will contain the remainder as an equality contraint, predicating the implication on that equality being true.
Expand All @@ -156,32 +139,30 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
NonEmpty.toList remainder
)
else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR
else checkImpliesMatchTerms existsL simplifedSubstPatL existsR patR
(Left err, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
MatchSuccess subst -> do
let filteredConsequentPreds =
Set.map
(Substitution.substituteInPredicate subst)
(substPatR.constraints <> (Set.fromList $ Substitution.asEquations substPatR.substitution))
`Set.difference` (substPatL.constraints <> (Set.fromList $ Substitution.asEquations substPatL.substitution))
(patR.constraints <> (Set.fromList $ asEquations patR.substitution))
`Set.difference` (patL.constraints <> (Set.fromList $ asEquations patL.substitution))

if null filteredConsequentPreds
then
implies
(sortOfPattern substPatL)
(externaliseExistTerm existsL substPatL.term)
(externaliseExistTerm existsR substPatR.term)
(sortOfPattern patL)
(externaliseExistTerm existsL patL.term)
(externaliseExistTerm existsR patR.term)
subst
else
ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
(Right newPreds, _) ->
if all (== Predicate TrueBool) newPreds
then
implies
(sortOfPattern substPatL)
(externaliseExistTerm existsL substPatL.term)
(externaliseExistTerm existsR substPatR.term)
(sortOfPattern patL)
(externaliseExistTerm existsL patL.term)
(externaliseExistTerm existsR patR.term)
subst
else -- here we conservatively abort
-- an anlternative would be to return valid, putting the unknown constraints into the
Expand Down
38 changes: 31 additions & 7 deletions booster/library/Booster/Syntax/Json/Internalise.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,13 @@ retractPattern :: TermOrPredicates -> Maybe Internal.Pattern
retractPattern (TermAndPredicates patt _) = Just patt
retractPattern _ = Nothing

-- main interface functions
{- | Internalise a @'Syntax.KorePattern'@ into the components constituting a @'Internal.Pattern'@
Note: This function will NOT apply the internalised @'Internal.Substitution'@ to the other components.
The callers of this function must decide if it is necessary to substitute.
Use @'internalisePatternOrTopOrBottom'@ or @'internaliseTermOrPredicate'@ that return an already
substituted @'Internal.Pattern'@.
-}
internalisePattern ::
Flag "alias" ->
Flag "subsorts" ->
Expand All @@ -153,7 +159,7 @@ internalisePattern ::
( Internal.Term
, [Internal.Predicate]
, [Internal.Ceil]
, Map Internal.Variable Internal.Term
, Internal.Substitution
, [Syntax.KorePattern]
)
internalisePattern allowAlias checkSubsorts sortVars definition p = do
Expand Down Expand Up @@ -193,7 +199,11 @@ data PatternOrTopOrBottom a
| IsPattern a
deriving (Functor)

-- main interface functions
{- | Internalise a @'Syntax.KorePattern'@ into @'Internal.Pattern'@, detecting and reporting trivial cases.
Note: This function will apply the internalised @'Internal.Substitution'@ part of the pattern's constraints
to the term and constraints (but not the ceils).
-}
internalisePatternOrTopOrBottom ::
Flag "alias" ->
Flag "subsorts" ->
Expand Down Expand Up @@ -223,7 +233,12 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
pure $
IsPattern
( existentialVars
, Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions, substitution = subst}
, Internal.Pattern
{ term = Internal.substituteInTerm subst term
, constraints = Set.map (Internal.substituteInPredicate subst) . Set.fromList $ preds
, ceilConditions
, substitution = subst
}
, unknown
)
where
Expand All @@ -237,6 +252,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
Syntax.KJBottom{sort} : _ -> Just $ IsBottom sort
_ : xs -> isBottom xs

{- | Internalise a @'Syntax.KorePattern'@ into either @'Internal.Pattern'@
or @'[InternalisedPredicates]'@ if only terms of sort bool are present.
Note: If this function successfully internalises a @'Internal.Pattern'@, it will apply the
@'Internal.Substitution'@ part to the term and constraints (but not the ceils).
Otherwise, when we get predicates only, the substitution part
is not applied to the rest of the predicates.
-}
internaliseTermOrPredicate ::
Flag "alias" ->
Flag "subsorts" ->
Expand All @@ -254,10 +278,10 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa
pure $
TermAndPredicates
Internal.Pattern
{ term
, constraints = Set.fromList constrs
{ term = Internal.substituteInTerm substitution term
, constraints = Set.map (Internal.substituteInPredicate substitution) . Set.fromList $ constrs
, ceilConditions
, substitution = substitution
, substitution
}
unsupported
)
Expand Down

0 comments on commit 58f6402

Please sign in to comment.