From ca0e798d9040ec0330112f5159bb4772a0f6ce46 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 15 May 2024 15:34:00 +0200 Subject: [PATCH 1/2] Add syntactic filtering of side conditions after simplification --- booster/library/Booster/Pattern/ApplyEquations.hs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index e979ec80a6..124f4eb2db 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -886,9 +886,17 @@ applyEquation term rule = fmap (either Failure Success) $ runExceptT $ do renderOneLineText $ "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue) + -- unclear conditions may have been simplified and + -- could now be syntactically present in the path constraints, check again + -- FIXME: factor this filtering out into a function ans use above unclearConditions' <- catMaybes <$> mapM (checkConstraint ConditionFalse) toCheck + let (newKnownTrue, stillUnclear) = partition (`Set.member` knownPredicates) unclearConditions' + unless (null newKnownTrue) $ + logMessage $ + renderOneLineText $ + "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue) - case unclearConditions' of + case stillUnclear of [] -> do -- check ensured conditions, filter any -- true ones, prune if any is false From 3203683a5f44211d35e1f86848a0266836809f10 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 21 May 2024 09:22:11 +0200 Subject: [PATCH 2/2] refactor applyEquation --- .../library/Booster/Pattern/ApplyEquations.hs | 70 ++++++++++--------- 1 file changed, 36 insertions(+), 34 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 124f4eb2db..96d1b0d7ae 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -872,7 +872,7 @@ applyEquation term rule = fmap (either Failure Success) $ runExceptT $ do $ "Substitution:" <+> (hsep $ intersperse "," $ map (\(k, v) -> pretty k <+> "->" <+> pretty v) $ Map.toList subst) - -- check required conditions, using substitution + -- instantiate the requires clause with the obtained substitution let required = concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) @@ -880,42 +880,44 @@ applyEquation term rule = fmap (either Failure Success) $ runExceptT $ do -- If the required condition is _syntactically_ present in -- the prior (known constraints), we don't check it. knownPredicates <- (.predicates) <$> lift getState - let (knownTrue, toCheck) = partition (`Set.member` knownPredicates) required - unless (null knownTrue) $ - logMessage $ - renderOneLineText $ - "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue) + toCheck <- lift $ filterOutKnownConstraints knownPredicates required + + -- check the filtered requires clause conditions + unclearConditions <- catMaybes <$> mapM (checkConstraint ConditionFalse) toCheck -- unclear conditions may have been simplified and - -- could now be syntactically present in the path constraints, check again - -- FIXME: factor this filtering out into a function ans use above - unclearConditions' <- catMaybes <$> mapM (checkConstraint ConditionFalse) toCheck - let (newKnownTrue, stillUnclear) = partition (`Set.member` knownPredicates) unclearConditions' - unless (null newKnownTrue) $ - logMessage $ - renderOneLineText $ - "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue) - - case stillUnclear of - [] -> do - -- check ensured conditions, filter any - -- true ones, prune if any is false - let ensured = - concatMap - (splitBoolPredicates . substituteInPredicate subst) - (Set.toList rule.ensures) - ensuredConditions <- - -- throws if an ensured condition found to be false - catMaybes <$> mapM (checkConstraint EnsuresFalse) ensured - lift $ pushConstraints $ Set.fromList ensuredConditions - pure $ substituteInTerm subst rule.rhs - unclearConditions -> do - withContext "failure" $ - logMessage $ - renderOneLineText $ - "Uncertain about a condition(s) in rule:" <+> hsep (intersperse "," $ map pretty unclearConditions) - throwE $ IndeterminateCondition unclearConditions + -- could now be syntactically present in the path constraints, filter again + stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions + + -- abort if any of the conditions is still unclear at that point + unless (null stillUnclear) $ do + withContext "failure" $ + logMessage $ + renderOneLineText $ + "Uncertain about a condition(s) in rule:" <+> hsep (intersperse "," $ map pretty stillUnclear) + throwE $ IndeterminateCondition unclearConditions + + -- check ensured conditions, filter any + -- true ones, prune if any is false + let ensured = + concatMap + (splitBoolPredicates . substituteInPredicate subst) + (Set.toList rule.ensures) + ensuredConditions <- + -- throws if an ensured condition found to be false + catMaybes <$> mapM (checkConstraint EnsuresFalse) ensured + lift $ pushConstraints $ Set.fromList ensuredConditions + pure $ substituteInTerm subst rule.rhs where + filterOutKnownConstraints :: Set Predicate -> [Predicate] -> EquationT io [Predicate] + filterOutKnownConstraints priorKnowledge constraitns = do + let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns + unless (null knownTrue) $ + logMessage $ + renderOneLineText $ + "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue) + pure toCheck + -- Simplify given predicate in a nested EquationT execution. -- Call 'whenBottom' if it is Bottom, return Nothing if it is Top, -- otherwise return the simplified remaining predicate.