Skip to content

Commit

Permalink
Revert "Remove ML connectives from the predicate type (#155)"
Browse files Browse the repository at this point in the history 
This reverts commit 27ac540.
  • Loading branch information
@geo2a
geo2a committed Nov 21, 2023
1 parent da1e8d2 commit 46a27a5
Show file tree
Hide file tree
Showing 30 changed files with 762 additions and 467 deletions.
14 changes: 13 additions & 1 deletion library/Booster/Definition/Base.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ data KoreDefinition = KoreDefinition
, rewriteTheory :: Theory (RewriteRule "Rewrite")
, functionEquations :: Theory (RewriteRule "Function")
, simplifications :: Theory (RewriteRule "Simplification")
, predicateSimplifications :: Theory PredicateEquation
}
deriving stock (Eq, Show, GHC.Generic)
deriving anyclass (NFData)
Expand All @@ -64,6 +65,7 @@ emptyKoreDefinition attributes =
, rewriteTheory = Map.empty
, functionEquations = Map.empty
, simplifications = Map.empty
, predicateSimplifications = Map.empty
}

data RewriteRule (tag :: k) = RewriteRule
Expand All @@ -82,7 +84,17 @@ data Alias = Alias
{ name :: AliasName
, params :: [Sort]
, args :: [Variable]
, rhs :: Pattern
, rhs :: TermOrPredicate
}
deriving stock (Eq, Ord, Show, GHC.Generic)
deriving anyclass (NFData)

data PredicateEquation = PredicateEquation
{ target :: Predicate
, conditions :: [Predicate]
, rhs :: [Predicate]
, attributes :: AxiomAttributes
, computedAttributes :: ComputedAxiomAttributes
}
deriving stock (Eq, Ord, Show, GHC.Generic)
deriving anyclass (NFData)
8 changes: 8 additions & 0 deletions library/Booster/Definition/Util.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ data Summary = Summary
, rewriteRules :: Map.Map TermIndex [SourceRef]
, functionRules :: Map.Map TermIndex [SourceRef]
, simplifications :: Map.Map TermIndex [SourceRef]
, predicateSimplifications :: Map.Map TermIndex [SourceRef]
}
deriving stock (Eq, Show, Generic)
deriving anyclass (NFData)
Expand Down Expand Up @@ -79,6 +80,7 @@ mkSummary file def =
, rewriteRules = Map.map sourceRefs def.rewriteTheory
, functionRules = Map.map sourceRefs def.functionEquations
, simplifications = Map.map sourceRefs def.simplifications
, predicateSimplifications = Map.map sourceRefs def.predicateSimplifications
}
where
sourceRefs :: HasSourceRef x => Map.Map k [x] -> [SourceRef]
Expand Down Expand Up @@ -109,6 +111,9 @@ instance Pretty Summary where
<> ( "Simplifications by term index:"
: tableView prettyTermIndex pretty summary.simplifications
)
<> ( "Predicate simplifications by term index:"
: tableView prettyTermIndex pretty summary.predicateSimplifications
)
<> [mempty]
where
tableView :: (k -> Doc a) -> (elem -> Doc a) -> Map.Map k [elem] -> [Doc a]
Expand Down Expand Up @@ -159,3 +164,6 @@ instance HasSourceRef AxiomAttributes where

instance HasSourceRef (RewriteRule a) where
sourceRef r = sourceRef r.attributes

instance HasSourceRef PredicateEquation where
sourceRef r = sourceRef r.attributes
57 changes: 23 additions & 34 deletions library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,7 @@ import Booster.Definition.Base (KoreDefinition (..))
import Booster.Definition.Base qualified as Definition (RewriteRule (..))
import Booster.LLVM.Internal qualified as LLVM
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
import Booster.Pattern.Base (
InternalisedPredicate (..),
Pattern (..),
Term,
TermOrPredicate (..),
Variable,
)
import Booster.Pattern.Base qualified as Pattern
import Booster.Pattern.Base (Pattern (..), TermOrPredicate (..))
import Booster.Pattern.Rewrite (
RewriteFailed (..),
RewriteResult (..),
Expand Down Expand Up @@ -95,7 +88,7 @@ respond stateVar =
Left patternError -> do
Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternError
Right (pat, substitution) -> do
Right pat -> do
let cutPoints = fromMaybe [] req.cutPointRules
terminals = fromMaybe [] req.terminalRules
mbDepth = fmap RpcTypes.getNat req.maxDepth
Expand All @@ -116,7 +109,7 @@ respond stateVar =
Just $
fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
else Nothing
pure $ execResponse duration req result substitution
pure $ execResponse duration req result
RpcTypes.AddModule req -> do
-- block other request executions while modifying the server state
state <- liftIO $ takeMVar stateVar
Expand Down Expand Up @@ -179,11 +172,11 @@ respond stateVar =
Log.logError $ "Error internalising cterm: " <> Text.pack (show patternErrors)
pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors
-- term and predicate (pattern)
Right (TermAndPredicateAndSubstitution pat substitution) -> do
Right (TermAndPredicate pat) -> do
Log.logInfoNS "booster" "Simplifying a pattern"
ApplyEquations.evaluatePattern doTracing def mLlvmLibrary mempty pat >>= \case
(Right newPattern, patternTraces, _) -> do
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
tSort = externaliseSort (sortOfPattern newPattern)
result = case catMaybes [mbPredicate, mbSubstitution] of
[] -> term
Expand All @@ -197,7 +190,7 @@ respond stateVar =
(Left other, _traces, _) ->
pure . Left . RpcError.backendError RpcError.Aborted $ show other -- FIXME
-- predicate only
Right (BoolOrCeilOrSubstitutionPredicate (IsPredicate predicate)) -> do
Right (APredicate predicate) -> do
Log.logInfoNS "booster" "Simplifying a predicate"
ApplyEquations.simplifyConstraint doTracing def mLlvmLibrary mempty predicate >>= \case
(Right newPred, traces, _) -> do
Expand All @@ -208,9 +201,6 @@ respond stateVar =
pure $ Right (addHeader result, traces)
(Left something, _traces, _) ->
pure . Left . RpcError.backendError RpcError.Aborted $ show something -- FIXME
Right (BoolOrCeilOrSubstitutionPredicate _) ->
pure . Left . RpcError.backendError RpcError.Aborted $
("cannot simplify ceil/substitution at the moment" :: String) -- FIXME
stop <- liftIO $ getTime Monotonic

let duration =
Expand Down Expand Up @@ -285,18 +275,17 @@ execResponse ::
Maybe Double ->
RpcTypes.ExecuteRequest ->
(Natural, Seq (RewriteTrace Pattern), RewriteResult Pattern) ->
Map Variable Term ->
Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
execResponse mbDuration req (d, traces, rr) = case rr of
RewriteBranch p nexts ->
Right $
RpcTypes.Execute
RpcTypes.ExecuteResult
{ reason = RpcTypes.Branching
, depth
, logs
, state = toExecState p originalSubstitution
, nextStates = Just $ map (\(_, _, p') -> toExecState p' originalSubstitution) $ toList nexts
, state = toExecState p
, nextStates = Just $ map (\(_, _, p') -> toExecState p') $ toList nexts
, rule = Nothing
}
RewriteStuck p ->
Expand All @@ -306,7 +295,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
{ reason = RpcTypes.Stuck
, depth
, logs
, state = toExecState p originalSubstitution
, state = toExecState p
, nextStates = Nothing
, rule = Nothing
}
Expand All @@ -317,7 +306,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
{ reason = RpcTypes.Vacuous
, depth
, logs
, state = toExecState p originalSubstitution
, state = toExecState p
, nextStates = Nothing
, rule = Nothing
}
Expand All @@ -328,8 +317,8 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
{ reason = RpcTypes.CutPointRule
, depth
, logs
, state = toExecState p originalSubstitution
, nextStates = Just [toExecState next originalSubstitution]
, state = toExecState p
, nextStates = Just [toExecState next]
, rule = Just lbl
}
RewriteTerminal lbl _ p ->
Expand All @@ -339,7 +328,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
{ reason = RpcTypes.TerminalRule
, depth
, logs
, state = toExecState p originalSubstitution
, state = toExecState p
, nextStates = Nothing
, rule = Just lbl
}
Expand All @@ -350,7 +339,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
{ reason = RpcTypes.DepthBound
, depth
, logs
, state = toExecState p originalSubstitution
, state = toExecState p
, nextStates = Nothing
, rule = Nothing
}
Expand All @@ -367,7 +356,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
(logSuccessfulSimplifications, logFailedSimplifications)
(RewriteStepFailed failure)
in logs <|> abortRewriteLog
, state = toExecState p originalSubstitution
, state = toExecState p
, nextStates = Nothing
, rule = Nothing
}
Expand Down Expand Up @@ -396,15 +385,15 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of
(Just t, Nothing) -> Just [t]
(Just t, Just xs) -> Just (t : xs)

toExecState :: Pattern -> Map Variable Term -> RpcTypes.ExecuteState
toExecState pat sub =
toExecState :: Pattern -> RpcTypes.ExecuteState
toExecState pat =
RpcTypes.ExecuteState
{ term = addHeader t
, predicate = fmap addHeader p
, substitution = fmap addHeader s
}
where
(t, p, s) = externalisePattern pat sub
(t, p, s) = externalisePattern pat

mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace -> Maybe LogEntry
mkLogEquationTrace
Expand All @@ -420,7 +409,7 @@ mkLogEquationTrace
, origin
, result =
Success
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ rewrittenTrm) mempty
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState $ Pattern rewrittenTrm mempty
, substitution = Nothing
, ruleId = fromMaybe "UNKNOWN" _ruleId
}
Expand Down Expand Up @@ -485,7 +474,7 @@ mkLogEquationTrace
}
_ -> Nothing
where
originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ subjectTerm) mempty
originalTerm = Just $ execStateToKoreJson $ toExecState $ Pattern subjectTerm mempty
originalTermIndex = Nothing
origin = Booster
_ruleId = fmap getUniqueId uid
Expand All @@ -506,7 +495,7 @@ mkLogRewriteTrace
Rewrite
{ result =
Success
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState res mempty
{ rewrittenTerm = Just $ execStateToKoreJson $ toExecState res
, substitution = Nothing
, ruleId = maybe "UNKNOWN" getUniqueId uid
}
Expand Down Expand Up @@ -558,7 +547,7 @@ mkLogRewriteTrace
let final = singleton $ case failure of
ApplyEquations.IndexIsNone trm ->
Simplification
{ originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty
{ originalTerm = Just $ execStateToKoreJson $ toExecState $ Pattern trm mempty
, originalTermIndex = Nothing
, origin = Booster
, result = Failure{reason = "No index found for term", _ruleId = Nothing}
Expand Down
25 changes: 17 additions & 8 deletions library/Booster/JsonRpc/Utils.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,9 @@ import Data.Aeson as Json
import Data.Aeson.Encode.Pretty (encodePretty')
import Data.Aeson.Types (parseMaybe)
import Data.ByteString.Lazy.Char8 qualified as BS
import Data.Functor.Foldable (Corecursive (embed), cata)
import Data.Maybe (fromMaybe)
import Data.Set qualified as Set
import Network.JSONRPC
import Prettyprinter
import System.Exit (ExitCode (..))
Expand All @@ -34,7 +36,6 @@ import Booster.Definition.Base qualified as Internal
import Booster.Pattern.Base qualified as Internal
import Booster.Prettyprinter
import Booster.Syntax.Json.Internalise
import Data.Map qualified as Map
import Kore.JsonRpc.Types
import Kore.Syntax.Json.Types hiding (Left, Right)

Expand Down Expand Up @@ -234,15 +235,23 @@ diffBy def pat1 pat2 =
renderDiff (internalise pat1) (internalise pat2)
where
renderBS :: Internal.TermOrPredicate -> BS.ByteString
renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsPredicate p)) = BS.pack . renderDefault $ pretty p
renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsCeil c)) = BS.pack . renderDefault $ pretty c
renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsSubstitution k v)) = BS.pack . renderDefault $ pretty k <+> "=" <+> pretty v
renderBS (Internal.TermAndPredicateAndSubstitution p m) =
BS.pack . renderDefault $
pretty p <+> vsep (map (\(k, v) -> pretty k <+> "=" <+> pretty v) (Map.toList m))
renderBS (Internal.APredicate p) = BS.pack . renderDefault $ pretty p
renderBS (Internal.TermAndPredicate p) = BS.pack . renderDefault $ pretty p
internalise =
either
(("Pattern could not be internalised: " <>) . Json.encode)
renderBS
(renderBS . orientEquals)
. runExcept
. internaliseTermOrPredicate DisallowAlias IgnoreSubsorts Nothing def

orientEquals = \case
Internal.APredicate p ->
Internal.APredicate $ orient p
Internal.TermAndPredicate p ->
Internal.TermAndPredicate p{Internal.constraints = Set.map orient p.constraints}
where
orient :: Internal.Predicate -> Internal.Predicate
orient = cata $ \case
Internal.EqualsTermF t1 t2
| t1 > t2 -> Internal.EqualsTerm t2 t1
other -> embed other
Loading

0 comments on commit 46a27a5

Please sign in to comment.