Skip to content

Commit 3d7e91d

Browse files
geo2ageo2a
authored
Georgy/refactor check requires (#4035)
Refactor `applyRule` and `applyEquation` to check `requires`/`ensures` in separate functions. This will make reviewing #4022 easier.
1 parent 95155fc commit 3d7e91d

File tree

2 files changed

+181
-130
lines changed

2 files changed

+181
-130
lines changed

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

Lines changed: 105 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -839,86 +839,15 @@ applyEquation term rule =
839839
Map.toList subst
840840
)
841841

842-
-- instantiate the requires clause with the obtained substitution
843-
let required =
844-
concatMap
845-
(splitBoolPredicates . coerce . substituteInTerm subst . coerce)
846-
rule.requires
847-
-- If the required condition is _syntactically_ present in
848-
-- the prior (known constraints), we don't check it.
849-
knownPredicates <- (.predicates) <$> lift getState
850-
toCheck <- lift $ filterOutKnownConstraints knownPredicates required
851-
852-
-- check the filtered requires clause conditions
853-
unclearConditions <-
854-
catMaybes
855-
<$> mapM
856-
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p)
857-
)
858-
toCheck
859-
860-
-- unclear conditions may have been simplified and
861-
-- could now be syntactically present in the path constraints, filter again
862-
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
863-
864-
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
865-
866-
-- check any conditions that are still unclear with the SMT solver
867-
-- (or abort if no solver is being used), abort if still unclear after
868-
unless (null stillUnclear) $
869-
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
870-
SMT.IsUnknown{} -> do
871-
-- no solver or still unclear: abort
872-
throwE
873-
( \ctx ->
874-
ctx . logMessage $
875-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
876-
renderOneLineText
877-
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
878-
)
879-
, IndeterminateCondition stillUnclear
880-
)
881-
SMT.IsInvalid -> do
882-
-- actually false given path condition: fail
883-
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
884-
throwE
885-
( \ctx ->
886-
ctx . logMessage $
887-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
888-
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
889-
, ConditionFalse failedP
890-
)
891-
SMT.IsValid{} -> do
892-
-- can proceed
893-
pure ()
842+
-- check required constraints from lhs.
843+
-- Reaction on false/indeterminate varies depending on the equation's type (function/simplification),
844+
-- see @handleSimplificationEquation@ and @handleFunctionEquation@
845+
checkRequires subst
894846

895-
-- check ensured conditions, filter any
896-
-- true ones, prune if any is false
897-
let ensured =
898-
concatMap
899-
(splitBoolPredicates . substituteInPredicate subst)
900-
(Set.toList rule.ensures)
901-
ensuredConditions <-
902-
-- throws if an ensured condition found to be false
903-
catMaybes
904-
<$> mapM
905-
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p)
906-
)
907-
ensured
908-
-- check all ensured conditions together with the path condition
909-
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
910-
SMT.IsInvalid -> do
911-
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
912-
throwE
913-
( \ctx ->
914-
ctx . logMessage $
915-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
916-
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
917-
, EnsuresFalse falseEnsures
918-
)
919-
_ ->
920-
pure ()
847+
-- check ensured conditions, filter any true ones, prune if any is false
848+
ensuredConditions <- checkEnsures subst
921849
lift $ pushConstraints $ Set.fromList ensuredConditions
850+
922851
-- when a new path condition is added, invalidate the equation cache
923852
unless (null ensuredConditions) $ do
924853
withContextFor Equations . logMessage $
@@ -1013,6 +942,104 @@ applyEquation term rule =
1013942
check
1014943
$ Map.lookup Variable{variableSort = SortApp sortName [], variableName} subst
1015944

945+
checkRequires ::
946+
Substitution ->
947+
ExceptT
948+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
949+
(EquationT io)
950+
()
951+
checkRequires matchingSubst = do
952+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
953+
-- instantiate the requires clause with the obtained substitution
954+
let required =
955+
concatMap
956+
(splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce)
957+
rule.requires
958+
-- If the required condition is _syntactically_ present in
959+
-- the prior (known constraints), we don't check it.
960+
knownPredicates <- (.predicates) <$> lift getState
961+
toCheck <- lift $ filterOutKnownConstraints knownPredicates required
962+
963+
-- check the filtered requires clause conditions
964+
unclearConditions <-
965+
catMaybes
966+
<$> mapM
967+
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p)
968+
)
969+
toCheck
970+
971+
-- unclear conditions may have been simplified and
972+
-- could now be syntactically present in the path constraints, filter again
973+
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
974+
975+
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
976+
977+
-- check any conditions that are still unclear with the SMT solver
978+
-- (or abort if no solver is being used), abort if still unclear after
979+
unless (null stillUnclear) $
980+
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
981+
SMT.IsUnknown{} -> do
982+
-- no solver or still unclear: abort
983+
throwE
984+
( \ctx ->
985+
ctx . logMessage $
986+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
987+
renderOneLineText
988+
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
989+
)
990+
, IndeterminateCondition stillUnclear
991+
)
992+
SMT.IsInvalid -> do
993+
-- actually false given path condition: fail
994+
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
995+
throwE
996+
( \ctx ->
997+
ctx . logMessage $
998+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
999+
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
1000+
, ConditionFalse failedP
1001+
)
1002+
SMT.IsValid{} -> do
1003+
-- can proceed
1004+
pure ()
1005+
1006+
checkEnsures ::
1007+
Substitution ->
1008+
ExceptT
1009+
((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure)
1010+
(EquationT io)
1011+
[Predicate]
1012+
checkEnsures matchingSubst = do
1013+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
1014+
let ensured =
1015+
concatMap
1016+
(splitBoolPredicates . substituteInPredicate matchingSubst)
1017+
(Set.toList rule.ensures)
1018+
ensuredConditions <-
1019+
-- throws if an ensured condition found to be false
1020+
catMaybes
1021+
<$> mapM
1022+
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p)
1023+
)
1024+
ensured
1025+
1026+
-- check all ensured conditions together with the path condition
1027+
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
1028+
knownPredicates <- (.predicates) <$> lift getState
1029+
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
1030+
SMT.IsInvalid -> do
1031+
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
1032+
throwE
1033+
( \ctx ->
1034+
ctx . logMessage $
1035+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
1036+
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
1037+
, EnsuresFalse falseEnsures
1038+
)
1039+
_ ->
1040+
pure ()
1041+
pure ensuredConditions
1042+
10161043
--------------------------------------------------------------------
10171044

10181045
{- Simplification for boolean predicates

0 commit comments

Comments
 (0)