Skip to content

Commit a15cbe1

Browse files
geo2ageo2a
committed
Remove the tracing flag from simplifier entry points
1 parent 31bf501 commit a15cbe1

File tree

4 files changed

+17
-30
lines changed

4 files changed

+17
-30
lines changed

‎booster/library/Booster/Definition/Ceil.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ computeCeilRule ::
9696
computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
9797
| null computedAttributes.notPreservesDefinednessReasons = pure Nothing
9898
| otherwise = do
99-
(res, _) <- runEquationT (Flag False) def mllvm Nothing mempty $ do
99+
(res, _) <- runEquationT def mllvm Nothing mempty $ do
100100
lhsCeils <- Set.fromList <$> computeCeil lhs
101101
requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
102102
let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList

‎booster/library/Booster/JsonRpc.hs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -280,7 +280,7 @@ respond stateVar =
280280
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
281281
, ceilConditions = pat.ceilConditions
282282
}
283-
ApplyEquations.evaluatePattern doTracing def mLlvmLibrary solver mempty substPat >>= \case
283+
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
284284
(Right newPattern, _) -> do
285285
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
286286
tSort = externaliseSort (sortOfPattern newPattern)
@@ -313,7 +313,6 @@ respond stateVar =
313313
let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
314314
withContext "constraint" $
315315
ApplyEquations.simplifyConstraints
316-
doTracing
317316
def
318317
mLlvmLibrary
319318
solver
@@ -530,13 +529,12 @@ respond stateVar =
530529
MatchSuccess subst -> do
531530
let filteredConsequentPreds =
532531
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
533-
doTracing = Flag False
534532
solver <- traverse (SMT.initSolver def) mSMTOptions
535533

536534
if null filteredConsequentPreds
537535
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
538536
else
539-
ApplyEquations.evaluateConstraints doTracing def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
537+
ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
540538
(Right newPreds, _) ->
541539
if all (== Pattern.Predicate TrueBool) newPreds
542540
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst

‎booster/library/Booster/Pattern/ApplyEquations.hs

Lines changed: 11 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,6 @@ data EquationConfig = EquationConfig
149149
{ definition :: KoreDefinition
150150
, llvmApi :: Maybe LLVM.API
151151
, smtSolver :: Maybe SMT.SMTContext
152-
, doTracing :: Flag "CollectEquationTraces"
153152
, maxRecursion :: Bound "Recursion"
154153
, maxIterations :: Bound "Iterations"
155154
, logger :: Logger LogMessage
@@ -412,14 +411,13 @@ data EquationPreference = PreferFunctions | PreferSimplifications
412411

413412
runEquationT ::
414413
LoggerMIO io =>
415-
Flag "CollectEquationTraces" ->
416414
KoreDefinition ->
417415
Maybe LLVM.API ->
418416
Maybe SMT.SMTContext ->
419417
SimplifierCache ->
420418
EquationT io a ->
421419
io (Either EquationFailure a, SimplifierCache)
422-
runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do
420+
runEquationT definition llvmApi smtSolver sCache (EquationT m) = do
423421
globalEquationOptions <- liftIO GlobalState.readGlobalEquationOptions
424422
logger <- getLogger
425423
(res, endState) <-
@@ -431,7 +429,6 @@ runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do
431429
{ definition
432430
, llvmApi
433431
, smtSolver
434-
, doTracing
435432
, maxIterations = globalEquationOptions.maxIterations
436433
, maxRecursion = globalEquationOptions.maxRecursion
437434
, logger
@@ -533,15 +530,14 @@ llvmSimplify term = do
533530
-- | Evaluate and simplify a term.
534531
evaluateTerm ::
535532
LoggerMIO io =>
536-
Flag "CollectEquationTraces" ->
537533
Direction ->
538534
KoreDefinition ->
539535
Maybe LLVM.API ->
540536
Maybe SMT.SMTContext ->
541537
Term ->
542538
io (Either EquationFailure Term, SimplifierCache)
543-
evaluateTerm doTracing direction def llvmApi smtSolver =
544-
runEquationT doTracing def llvmApi smtSolver mempty
539+
evaluateTerm direction def llvmApi smtSolver =
540+
runEquationT def llvmApi smtSolver mempty
545541
. evaluateTerm' direction
546542

547543
-- version for internal nested evaluation
@@ -557,15 +553,14 @@ evaluateTerm' direction = iterateEquations direction PreferFunctions
557553
-}
558554
evaluatePattern ::
559555
LoggerMIO io =>
560-
Flag "CollectEquationTraces" ->
561556
KoreDefinition ->
562557
Maybe LLVM.API ->
563558
Maybe SMT.SMTContext ->
564559
SimplifierCache ->
565560
Pattern ->
566561
io (Either EquationFailure Pattern, SimplifierCache)
567-
evaluatePattern doTracing def mLlvmLibrary smtSolver cache =
568-
runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluatePattern'
562+
evaluatePattern def mLlvmLibrary smtSolver cache =
563+
runEquationT def mLlvmLibrary smtSolver cache . evaluatePattern'
569564

570565
-- version for internal nested evaluation
571566
evaluatePattern' ::
@@ -593,15 +588,14 @@ simplifyAssumedPredicate p = do
593588

594589
evaluateConstraints ::
595590
LoggerMIO io =>
596-
Flag "CollectEquationTraces" ->
597591
KoreDefinition ->
598592
Maybe LLVM.API ->
599593
Maybe SMT.SMTContext ->
600594
SimplifierCache ->
601595
Set Predicate ->
602596
io (Either EquationFailure (Set Predicate), SimplifierCache)
603-
evaluateConstraints doTracing def mLlvmLibrary smtSolver cache =
604-
runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluateConstraints'
597+
evaluateConstraints def mLlvmLibrary smtSolver cache =
598+
runEquationT def mLlvmLibrary smtSolver cache . evaluateConstraints'
605599

606600
evaluateConstraints' ::
607601
LoggerMIO io =>
@@ -1071,27 +1065,25 @@ applyEquation term rule = withRuleContext rule $ fmap (either Failure Success) $
10711065
-}
10721066
simplifyConstraint ::
10731067
LoggerMIO io =>
1074-
Flag "CollectEquationTraces" ->
10751068
KoreDefinition ->
10761069
Maybe LLVM.API ->
10771070
Maybe SMT.SMTContext ->
10781071
SimplifierCache ->
10791072
Predicate ->
10801073
io (Either EquationFailure Predicate, SimplifierCache)
1081-
simplifyConstraint doTracing def mbApi mbSMT cache (Predicate p) = do
1082-
runEquationT doTracing def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p
1074+
simplifyConstraint def mbApi mbSMT cache (Predicate p) = do
1075+
runEquationT def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p
10831076

10841077
simplifyConstraints ::
10851078
LoggerMIO io =>
1086-
Flag "CollectEquationTraces" ->
10871079
KoreDefinition ->
10881080
Maybe LLVM.API ->
10891081
Maybe SMT.SMTContext ->
10901082
SimplifierCache ->
10911083
[Predicate] ->
10921084
io (Either EquationFailure [Predicate], SimplifierCache)
1093-
simplifyConstraints doTracing def mbApi mbSMT cache ps =
1094-
runEquationT doTracing def mbApi mbSMT cache $
1085+
simplifyConstraints def mbApi mbSMT cache ps =
1086+
runEquationT def mbApi mbSMT cache $
10951087
concatMap splitAndBools
10961088
<$> mapM ((coerce <$>) . simplifyConstraint' True . coerce) ps
10971089

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -93,9 +93,6 @@ instance MonadLoggerIO io => LoggerMIO (RewriteT io) where
9393
getLogger = RewriteT $ asks logger
9494
withLogger modL (RewriteT m) = RewriteT $ withReaderT (\cfg@RewriteConfig{logger} -> cfg{logger = modL logger}) m
9595

96-
castDoTracingFlag :: Flag "CollectRewriteTraces" -> Flag "CollectEquationTraces"
97-
castDoTracingFlag = coerce
98-
9996
pattern CollectRewriteTraces :: Flag "CollectRewriteTraces"
10097
pattern CollectRewriteTraces = Flag True
10198

@@ -425,11 +422,11 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
425422
Predicate ->
426423
RewriteRuleAppT (RewriteT io) (Maybe a)
427424
checkConstraint onUnclear onBottom p = do
428-
RewriteConfig{definition, llvmApi, smtSolver, doTracing} <- lift $ RewriteT ask
425+
RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask
429426
oldCache <- lift . RewriteT . lift $ get
430427
(simplified, cache) <-
431428
withContext "constraint" $
432-
simplifyConstraint (castDoTracingFlag doTracing) definition llvmApi smtSolver oldCache p
429+
simplifyConstraint definition llvmApi smtSolver oldCache p
433430
-- update cache
434431
lift . RewriteT . lift . modify $ const cache
435432
-- TODO should we keep the traces? Or only on success?
@@ -726,7 +723,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
726723
st <- get
727724
let cache = st.simplifierCache
728725
smt = st.smtSolver
729-
evaluatePattern (castDoTracingFlag doTracing) def mLlvmLibrary smt cache p >>= \(res, newCache) -> do
726+
evaluatePattern def mLlvmLibrary smt cache p >>= \(res, newCache) -> do
730727
updateCache newCache
731728
case res of
732729
Right newPattern -> do

0 commit comments

Comments
 (0)