From d8ca961d818b62325b299df28ae88d5fb24c9679 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 14 Jun 2021 13:38:03 -0500 Subject: [PATCH 01/44] Add Kore.Internal.Substitution.retractAssignment --- kore/src/Kore/Internal/Substitution.hs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs index 3b14c0ea6b..97efc0b184 100644 --- a/kore/src/Kore/Internal/Substitution.hs +++ b/kore/src/Kore/Internal/Substitution.hs @@ -13,6 +13,7 @@ module Kore.Internal.Substitution ( assignedVariable, assignedTerm, mapAssignedTerm, + retractAssignment, singleSubstitutionToPredicate, UnwrappedSubstitution, mkUnwrappedSubstitution, @@ -68,6 +69,7 @@ import qualified Kore.Attribute.Pattern.Simplified as Attribute ( import Kore.Debug import Kore.Internal.Predicate ( Predicate, + pattern PredicateEquals, ) import qualified Kore.Internal.Predicate as Predicate import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ( @@ -155,6 +157,20 @@ mkUnwrappedSubstitution :: [Assignment variable] mkUnwrappedSubstitution = fmap (uncurry assign) +{- | Extract an 'Assignment' from a 'Predicate' of the proper form. + +Returns 'Nothing' if the 'Predicate' is not in the correct form. +-} +retractAssignment :: + InternalVariable variable => + Predicate variable -> + Maybe (Assignment variable) +retractAssignment (PredicateEquals (Var_ var) term) = + Just (assign var term) +retractAssignment (PredicateEquals term (Var_ var)) = + Just (assign var term) +retractAssignment _ = Nothing + {- | @Substitution@ represents a collection @[xᵢ=φᵢ]@ of substitutions. Individual substitutions are a pair of type From fe4f054bb2cc040ab11c1643ab9c564137365588 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 28 Apr 2021 16:31:58 -0500 Subject: [PATCH 02/44] [REF] Push MultiAnd change down into simplifyPredicate --- .../src/Kore/Step/Simplification/Condition.hs | 36 ++++++++++++------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index 61012e17dc..6403b8ee26 100644 --- a/kore/src/Kore/Step/Simplification/Condition.hs +++ b/kore/src/Kore/Step/Simplification/Condition.hs @@ -40,6 +40,9 @@ import Kore.Internal.SideCondition ( SideCondition, ) import qualified Kore.Internal.SideCondition as SideCondition +import Kore.Internal.Substitution ( + Assignment, + ) import qualified Kore.Internal.Substitution as Substitution import Kore.Rewriting.RewritingVariable ( RewritingVariableName, @@ -88,7 +91,7 @@ simplify SubstitutionSimplifier{simplifySubstitution} sideCondition = simplified <- simplifyPredicate sideCondition predicate' - >>= simplifyPredicates sideCondition . from @_ @(MultiAnd _) + >>= simplifyPredicates sideCondition TopBottom.guardAgainstBottom simplified let merged = simplified <> Condition.fromSubstitution substitution normalized <- normalize merged @@ -137,16 +140,25 @@ simplifyPredicates sideCondition original = do let predicates = SideCondition.simplifyConjunctionByAssumption original & fst . extract - simplified <- + simplifiedPredicates <- simplifyPredicatesWithAssumptions sideCondition (toList predicates) - let simplifiedPredicates = - from @(Condition _) @(MultiAnd (Predicate _)) simplified + let simplified = foldMap mkCondition simplifiedPredicates if original == simplifiedPredicates then return (Condition.markSimplified simplified) else simplifyPredicates sideCondition simplifiedPredicates +mkCondition :: + InternalVariable variable => + Predicate variable -> + Condition variable +mkCondition predicate + | Just assignment <- Substitution.retractAssignment predicate = + from @(Assignment _) assignment + | otherwise = + from @(Predicate _) predicate + {- | Simplify a conjunction of predicates by simplifying each one under the assumption that the others are true. -} @@ -157,8 +169,8 @@ simplifyPredicatesWithAssumptions :: [Predicate RewritingVariableName] -> LogicT simplifier - (Condition RewritingVariableName) -simplifyPredicatesWithAssumptions _ [] = return Condition.top + (MultiAnd (Predicate RewritingVariableName)) +simplifyPredicatesWithAssumptions _ [] = return MultiAnd.top simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do let predicatesWithUnsimplified = zip predicates $ @@ -168,23 +180,21 @@ simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do simplifyWithAssumptions predicatesWithUnsimplified ) - Condition.top + MultiAnd.top where simplifyWithAssumptions :: ( Predicate RewritingVariableName , MultiAnd (Predicate RewritingVariableName) ) -> StateT - (Condition RewritingVariableName) + (MultiAnd (Predicate RewritingVariableName)) (LogicT simplifier) () simplifyWithAssumptions (predicate, unsimplifiedSideCond) = do simplifiedSideCond <- State.get let otherSideConds = SideCondition.addAssumptions - ( from @_ @(MultiAnd (Predicate _)) simplifiedSideCond - <> unsimplifiedSideCond - ) + (simplifiedSideCond <> unsimplifiedSideCond) sideCondition result <- lift $ simplifyPredicate otherSideConds predicate State.put (simplifiedSideCond <> result) @@ -202,7 +212,7 @@ simplifyPredicate :: ) => SideCondition RewritingVariableName -> Predicate RewritingVariableName -> - LogicT simplifier (Condition RewritingVariableName) + LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) simplifyPredicate sideCondition predicate = do patternOr <- lift $ @@ -210,7 +220,7 @@ simplifyPredicate sideCondition predicate = do Predicate.fromPredicate_ predicate -- Despite using lift above, we do not need to -- explicitly check for \bottom because patternOr is an OrPattern. - scatter (OrPattern.map eraseTerm patternOr) + from @(Condition _) @(MultiAnd (Predicate _)) <$> scatter (OrPattern.map eraseTerm patternOr) where eraseTerm conditional | TopBottom.isTop (Pattern.term conditional) = From 19a210a50aa9cc901f6a9cecd3c718f2362bdc18 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 30 Apr 2021 14:54:31 -0500 Subject: [PATCH 03/44] Update golden files --- ...max-inconsistent-prelude-spec.k.out.golden | 4 +- test/priority/1.merge.out.golden | 38 +++++++++---------- test/priority/2.merge.out.golden | 38 +++++++++---------- 3 files changed, 40 insertions(+), 40 deletions(-) diff --git a/test/imp/max-inconsistent-prelude-spec.k.out.golden b/test/imp/max-inconsistent-prelude-spec.k.out.golden index 8e0bf9d69f..e8c9cd4e7e 100644 --- a/test/imp/max-inconsistent-prelude-spec.k.out.golden +++ b/test/imp/max-inconsistent-prelude-spec.k.out.golden @@ -1,6 +1,6 @@ -kore-exec: [233424] Error (ErrorException): +kore-exec: [593738] Error (ErrorException): The definitions sent to the solver are inconsistent. CallStack (from HasCallStack): - error, called at src/Kore/Step/SMT/Lemma.hs:104:9 in kore-0.40.0.0-CzNxqIvwhPqHJvDm7pwDgz:Kore.Step.SMT.Lemma + error, called at src/Kore/Step/SMT/Lemma.hs:106:9 in kore-0.44.0.0-GXyjcogd7FRExioa8Iqini:Kore.Step.SMT.Lemma [Error] Critical: Haskell Backend execution failed with code 1 and produced no output. diff --git a/test/priority/1.merge.out.golden b/test/priority/1.merge.out.golden index 5a3947b567..1645229612 100644 --- a/test/priority/1.merge.out.golden +++ b/test/priority/1.merge.out.golden @@ -7,17 +7,17 @@ \and{SortGeneratedTopCell{}}( /* Sfa */ \and{SortGeneratedTopCell{}}( + /* Sfa */ + \equals{SortBool{}, SortGeneratedTopCell{}}( + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa */ + Lbl'Unds-GT-'Int'Unds'{}( + /* Fl Fn D Sfa */ VarX0:SortInt{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("8") + ) + ), /* Spa */ \and{SortGeneratedTopCell{}}( - /* Sfa */ - \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* Fl Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("8") - ) - ), /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), @@ -26,17 +26,17 @@ /* Fl Fn D Sfa */ VarX0:SortInt{}, /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("10") ) - ) - ), - /* Sfa */ - \not{SortGeneratedTopCell{}}( + ), /* Sfa */ - \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* Fl Fn D Sfa */ - Lbl'Unds-LT-'Int'Unds'{}( - /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("6") + \not{SortGeneratedTopCell{}}( + /* Sfa */ + \equals{SortBool{}, SortGeneratedTopCell{}}( + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa */ + Lbl'Unds-LT-'Int'Unds'{}( + /* Fl Fn D Sfa */ VarX0:SortInt{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("6") + ) ) ) ) diff --git a/test/priority/2.merge.out.golden b/test/priority/2.merge.out.golden index 23d7f75877..1ac8907ae1 100644 --- a/test/priority/2.merge.out.golden +++ b/test/priority/2.merge.out.golden @@ -7,17 +7,17 @@ \and{SortGeneratedTopCell{}}( /* Sfa */ \and{SortGeneratedTopCell{}}( + /* Sfa */ + \equals{SortBool{}, SortGeneratedTopCell{}}( + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa */ + Lbl'Unds-LT-'Int'Unds'{}( + /* Fl Fn D Sfa */ VarX0:SortInt{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("10") + ) + ), /* Spa */ \and{SortGeneratedTopCell{}}( - /* Sfa */ - \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* Fl Fn D Sfa */ - Lbl'Unds-LT-'Int'Unds'{}( - /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("10") - ) - ), /* Sfa */ \not{SortGeneratedTopCell{}}( /* Sfa */ @@ -29,17 +29,17 @@ /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("8") ) ) - ) - ), - /* Sfa */ - \not{SortGeneratedTopCell{}}( + ), /* Sfa */ - \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* Fl Fn D Sfa */ - Lbl'Unds-LT-'Int'Unds'{}( - /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("6") + \not{SortGeneratedTopCell{}}( + /* Sfa */ + \equals{SortBool{}, SortGeneratedTopCell{}}( + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa */ + Lbl'Unds-LT-'Int'Unds'{}( + /* Fl Fn D Sfa */ VarX0:SortInt{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("6") + ) ) ) ) From 8a8b8f37a1e66dab2a22e66511a0694bca5ae92f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 11:08:18 -0500 Subject: [PATCH 04/44] Clean up simplifyPredicates --- .../src/Kore/Step/Simplification/Condition.hs | 94 +++++++------------ 1 file changed, 33 insertions(+), 61 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index 6403b8ee26..cecf1ae820 100644 --- a/kore/src/Kore/Step/Simplification/Condition.hs +++ b/kore/src/Kore/Step/Simplification/Condition.hs @@ -121,8 +121,8 @@ simplify SubstitutionSimplifier{simplifySubstitution} sideCondition = normalize conditional@Conditional{substitution} = do let conditional' = conditional{substitution = mempty} predicates' <- - lift $ - simplifySubstitution sideCondition substitution + simplifySubstitution sideCondition substitution + & lift predicate' <- scatter predicates' return $ Conditional.andCondition conditional' predicate' @@ -132,72 +132,45 @@ others are true. This procedure is applied until the conjunction stabilizes. -} simplifyPredicates :: + forall simplifier. MonadSimplify simplifier => SideCondition RewritingVariableName -> MultiAnd (Predicate RewritingVariableName) -> LogicT simplifier (Condition RewritingVariableName) -simplifyPredicates sideCondition original = do - let predicates = - SideCondition.simplifyConjunctionByAssumption original - & fst . extract - simplifiedPredicates <- - simplifyPredicatesWithAssumptions - sideCondition - (toList predicates) - let simplified = foldMap mkCondition simplifiedPredicates - if original == simplifiedPredicates - then return (Condition.markSimplified simplified) - else simplifyPredicates sideCondition simplifiedPredicates - -mkCondition :: - InternalVariable variable => - Predicate variable -> - Condition variable -mkCondition predicate - | Just assignment <- Substitution.retractAssignment predicate = - from @(Assignment _) assignment - | otherwise = - from @(Predicate _) predicate - -{- | Simplify a conjunction of predicates by simplifying each one -under the assumption that the others are true. --} -simplifyPredicatesWithAssumptions :: - forall simplifier. - MonadSimplify simplifier => - SideCondition RewritingVariableName -> - [Predicate RewritingVariableName] -> - LogicT - simplifier - (MultiAnd (Predicate RewritingVariableName)) -simplifyPredicatesWithAssumptions _ [] = return MultiAnd.top -simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do - let predicatesWithUnsimplified = - zip predicates $ - scanr ((<>) . MultiAnd.singleton) MultiAnd.top rest - State.execStateT - ( traverse_ - simplifyWithAssumptions - predicatesWithUnsimplified - ) - MultiAnd.top +simplifyPredicates initialSideCondition predicates = do + let predicatesList = toList predicates + unsimplifieds = scanr ((<>) . MultiAnd.singleton) MultiAnd.top predicatesList + simplifieds <- + traverse worker (zip predicatesList unsimplifieds) + & flip State.evalStateT initialSideCondition + markConjunctionSimplified (foldMap mkCondition $ mconcat simplifieds) where - simplifyWithAssumptions :: + worker :: ( Predicate RewritingVariableName , MultiAnd (Predicate RewritingVariableName) ) -> StateT - (MultiAnd (Predicate RewritingVariableName)) + (SideCondition RewritingVariableName) (LogicT simplifier) - () - simplifyWithAssumptions (predicate, unsimplifiedSideCond) = do - simplifiedSideCond <- State.get - let otherSideConds = - SideCondition.addAssumptions - (simplifiedSideCond <> unsimplifiedSideCond) - sideCondition - result <- lift $ simplifyPredicate otherSideConds predicate - State.put (simplifiedSideCond <> result) + (MultiAnd (Predicate RewritingVariableName)) + worker (predicate, unsimplified) = do + sideCondition <- SideCondition.addAssumptions unsimplified <$> State.get + results <- simplifyPredicate sideCondition predicate & lift + State.modify (SideCondition.addAssumptions results) + return results + + markConjunctionSimplified = + return . Lens.over (field @"predicate") Predicate.markSimplified + +mkCondition :: + InternalVariable variable => + Predicate variable -> + Condition variable +mkCondition predicate = + maybe + (from @(Predicate _) predicate) + (from @(Assignment _)) + (Substitution.retractAssignment predicate) {- | Simplify the 'Predicate' once. @@ -215,9 +188,8 @@ simplifyPredicate :: LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) simplifyPredicate sideCondition predicate = do patternOr <- - lift $ - simplifyTermLike sideCondition $ - Predicate.fromPredicate_ predicate + simplifyTermLike sideCondition (Predicate.fromPredicate_ predicate) + & lift -- Despite using lift above, we do not need to -- explicitly check for \bottom because patternOr is an OrPattern. from @(Condition _) @(MultiAnd (Predicate _)) <$> scatter (OrPattern.map eraseTerm patternOr) From a19dcda3e69fc1fcf54ca52ee5e21038a6915d35 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 11:10:10 -0500 Subject: [PATCH 05/44] [REF] Insert indirection before simplifyPredicateTODO --- kore/src/Kore/Step/Simplification/Condition.hs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index cecf1ae820..624da54fbc 100644 --- a/kore/src/Kore/Step/Simplification/Condition.hs +++ b/kore/src/Kore/Step/Simplification/Condition.hs @@ -179,14 +179,14 @@ re-simplify the result. See also: 'simplify' -} -simplifyPredicate :: +simplifyPredicateTODO :: ( HasCallStack , MonadSimplify simplifier ) => SideCondition RewritingVariableName -> Predicate RewritingVariableName -> LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) -simplifyPredicate sideCondition predicate = do +simplifyPredicateTODO sideCondition predicate = do patternOr <- simplifyTermLike sideCondition (Predicate.fromPredicate_ predicate) & lift @@ -203,6 +203,16 @@ simplifyPredicate sideCondition predicate = do , unparse conditional ] +simplifyPredicate :: + ( HasCallStack + , MonadSimplify simplifier + ) => + SideCondition RewritingVariableName -> + Predicate RewritingVariableName -> + LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) +simplifyPredicate sideCondition predicate = + simplifyPredicateTODO sideCondition predicate + simplifyConjunctions :: Predicate RewritingVariableName -> Changed (Predicate RewritingVariableName) From 8ddb8974e8e1683a9841590cf11635829fc6a8f7 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 11:41:39 -0500 Subject: [PATCH 06/44] Factor out Kore.Step.Simplification.Predicate --- kore/kore.cabal | 1 + .../src/Kore/Step/Simplification/Condition.hs | 51 +---------- .../src/Kore/Step/Simplification/Predicate.hs | 90 +++++++++++++++++++ 3 files changed, 94 insertions(+), 48 deletions(-) create mode 100644 kore/src/Kore/Step/Simplification/Predicate.hs diff --git a/kore/kore.cabal b/kore/kore.cabal index 025f95ba25..ac5d306751 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -444,6 +444,7 @@ library Kore.Step.Simplification.Overloading Kore.Step.Simplification.OverloadSimplifier Kore.Step.Simplification.Pattern + Kore.Step.Simplification.Predicate Kore.Step.Simplification.Rewrites Kore.Step.Simplification.Rule Kore.Step.Simplification.SetVariable diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index 624da54fbc..c6b9ae16cb 100644 --- a/kore/src/Kore/Step/Simplification/Condition.hs +++ b/kore/src/Kore/Step/Simplification/Condition.hs @@ -5,7 +5,6 @@ License : NCSA module Kore.Step.Simplification.Condition ( create, simplify, - simplifyPredicate, simplifyCondition, -- For testing simplifyPredicates, @@ -26,12 +25,10 @@ import Kore.Internal.MultiAnd ( MultiAnd, ) import qualified Kore.Internal.MultiAnd as MultiAnd -import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Condition, Conditional (..), ) -import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( Predicate, ) @@ -47,15 +44,14 @@ import qualified Kore.Internal.Substitution as Substitution import Kore.Rewriting.RewritingVariable ( RewritingVariableName, ) +import qualified Kore.Step.Simplification.Predicate as Predicate import Kore.Step.Simplification.Simplify import Kore.Step.Simplification.SubstitutionSimplifier ( SubstitutionSimplifier (..), ) import qualified Kore.TopBottom as TopBottom -import Kore.Unparser import Logic import Prelude.Kore -import qualified Pretty -- | Create a 'ConditionSimplifier' using 'simplify'. create :: @@ -90,7 +86,7 @@ simplify SubstitutionSimplifier{simplifySubstitution} sideCondition = predicate' = Predicate.substitute substitution' predicate simplified <- - simplifyPredicate sideCondition predicate' + Predicate.simplify sideCondition predicate' >>= simplifyPredicates sideCondition TopBottom.guardAgainstBottom simplified let merged = simplified <> Condition.fromSubstitution substitution @@ -155,7 +151,7 @@ simplifyPredicates initialSideCondition predicates = do (MultiAnd (Predicate RewritingVariableName)) worker (predicate, unsimplified) = do sideCondition <- SideCondition.addAssumptions unsimplified <$> State.get - results <- simplifyPredicate sideCondition predicate & lift + results <- Predicate.simplify sideCondition predicate & lift State.modify (SideCondition.addAssumptions results) return results @@ -172,47 +168,6 @@ mkCondition predicate = (from @(Assignment _)) (Substitution.retractAssignment predicate) -{- | Simplify the 'Predicate' once. - -@simplifyPredicate@ does not attempt to apply the resulting substitution and -re-simplify the result. - -See also: 'simplify' --} -simplifyPredicateTODO :: - ( HasCallStack - , MonadSimplify simplifier - ) => - SideCondition RewritingVariableName -> - Predicate RewritingVariableName -> - LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) -simplifyPredicateTODO sideCondition predicate = do - patternOr <- - simplifyTermLike sideCondition (Predicate.fromPredicate_ predicate) - & lift - -- Despite using lift above, we do not need to - -- explicitly check for \bottom because patternOr is an OrPattern. - from @(Condition _) @(MultiAnd (Predicate _)) <$> scatter (OrPattern.map eraseTerm patternOr) - where - eraseTerm conditional - | TopBottom.isTop (Pattern.term conditional) = - Conditional.withoutTerm conditional - | otherwise = - (error . show . Pretty.vsep) - [ "Expecting a \\top term, but found:" - , unparse conditional - ] - -simplifyPredicate :: - ( HasCallStack - , MonadSimplify simplifier - ) => - SideCondition RewritingVariableName -> - Predicate RewritingVariableName -> - LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) -simplifyPredicate sideCondition predicate = - simplifyPredicateTODO sideCondition predicate - simplifyConjunctions :: Predicate RewritingVariableName -> Changed (Predicate RewritingVariableName) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs new file mode 100644 index 0000000000..414b982c9e --- /dev/null +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -0,0 +1,90 @@ +{- | +Copyright : (c) Runtime Verification, 2021 +License : NCSA +-} +module Kore.Step.Simplification.Predicate ( + simplify, +) where + + +import qualified Data.Functor.Foldable as Recursive +import qualified Kore.Internal.Conditional as Conditional +import Kore.Internal.MultiAnd (MultiAnd) +import qualified Kore.Internal.OrPattern as OrPattern +import Kore.Internal.Pattern ( + Condition, + ) +import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.Predicate ( + Predicate, + PredicateF (..) + ) +import Kore.Syntax (And) +import qualified Kore.Internal.Predicate as Predicate +import Kore.Internal.SideCondition ( + SideCondition, + ) +import Kore.Rewriting.RewritingVariable ( + RewritingVariableName, + ) +import Kore.Step.Simplification.Simplify +import qualified Kore.TopBottom as TopBottom +import Kore.Unparser +import Logic +import Prelude.Kore +import qualified Pretty + +{- | Simplify the 'Predicate' once. + +@simplifyPredicate@ does not attempt to apply the resulting substitution and +re-simplify the result. + +See also: 'simplify' +-} +simplifyPredicateTODO :: + ( HasCallStack + , MonadSimplify simplifier + ) => + SideCondition RewritingVariableName -> + Predicate RewritingVariableName -> + LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) +simplifyPredicateTODO sideCondition predicate = do + patternOr <- + simplifyTermLike sideCondition (Predicate.fromPredicate_ predicate) + & lift + -- Despite using lift above, we do not need to + -- explicitly check for \bottom because patternOr is an OrPattern. + from @(Condition _) @(MultiAnd (Predicate _)) <$> scatter (OrPattern.map eraseTerm patternOr) + where + eraseTerm conditional + | TopBottom.isTop (Pattern.term conditional) = + Conditional.withoutTerm conditional + | otherwise = + (error . show . Pretty.vsep) + [ "Expecting a \\top term, but found:" + , unparse conditional + ] + +simplify :: + ( HasCallStack + , MonadSimplify simplifier + ) => + SideCondition RewritingVariableName -> + Predicate RewritingVariableName -> + LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) +simplify sideCondition = + worker + where + worker predicate = + case predicateF of + AndF andF -> do + let andF' = worker <$> andF + distributeAnd andF' + _ -> simplifyPredicateTODO sideCondition predicate + where + _ :< predicateF = Recursive.project predicate + +distributeAnd :: + And sort (LogicT simplifier (MultiAnd (Predicate RewritingVariableName))) -> + LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) +distributeAnd andF = fold <$> sequence andF From aa449de12a63e3cacc0ff5b14ca32d291931b230 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 14:39:13 -0500 Subject: [PATCH 07/44] Add failing tests --- kore/kore.cabal | 1 + .../src/Kore/Step/Simplification/Predicate.hs | 13 +++- .../Kore/Step/Simplification/Predicate.hs | 64 +++++++++++++++++++ 3 files changed, 75 insertions(+), 3 deletions(-) create mode 100644 kore/test/Test/Kore/Step/Simplification/Predicate.hs diff --git a/kore/kore.cabal b/kore/kore.cabal index ac5d306751..70d2ee6d3d 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -751,6 +751,7 @@ test-suite kore-test Test.Kore.Step.Simplification.Or Test.Kore.Step.Simplification.OrPattern Test.Kore.Step.Simplification.Overloading + Test.Kore.Step.Simplification.Predicate Test.Kore.Step.Simplification.Pattern Test.Kore.Step.Simplification.Rule Test.Kore.Step.Simplification.StringLiteral diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 414b982c9e..89a36f8c3a 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -6,7 +6,6 @@ module Kore.Step.Simplification.Predicate ( simplify, ) where - import qualified Data.Functor.Foldable as Recursive import qualified Kore.Internal.Conditional as Conditional import Kore.Internal.MultiAnd (MultiAnd) @@ -17,9 +16,8 @@ import Kore.Internal.Pattern ( import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( Predicate, - PredicateF (..) + PredicateF (..), ) -import Kore.Syntax (And) import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.SideCondition ( SideCondition, @@ -28,6 +26,7 @@ import Kore.Rewriting.RewritingVariable ( RewritingVariableName, ) import Kore.Step.Simplification.Simplify +import Kore.Syntax (And, Or) import qualified Kore.TopBottom as TopBottom import Kore.Unparser import Logic @@ -80,6 +79,9 @@ simplify sideCondition = AndF andF -> do let andF' = worker <$> andF distributeAnd andF' + OrF orF -> do + let orF' = worker <$> orF + distributeOr orF' _ -> simplifyPredicateTODO sideCondition predicate where _ :< predicateF = Recursive.project predicate @@ -88,3 +90,8 @@ distributeAnd :: And sort (LogicT simplifier (MultiAnd (Predicate RewritingVariableName))) -> LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) distributeAnd andF = fold <$> sequence andF + +distributeOr :: + Or sort (LogicT simplifier conjunction) -> + LogicT simplifier conjunction +distributeOr = foldr1 (<|>) diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs new file mode 100644 index 0000000000..66bd6bb311 --- /dev/null +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -0,0 +1,64 @@ +module Test.Kore.Step.Simplification.Predicate ( + test_simplify, +) where + +import Kore.Internal.MultiAnd (MultiAnd) +import qualified Kore.Internal.MultiAnd as MultiAnd +import Kore.Internal.Predicate +import qualified Kore.Internal.SideCondition as SideCondition +import Kore.Internal.TermLike (TermLike) +import Kore.Rewriting.RewritingVariable +import Kore.Step.Simplification.Predicate (simplify) +import Prelude.Kore +import qualified Test.Kore.Step.MockSymbols as Mock +import qualified Test.Kore.Step.Simplification as Test +import Test.Tasty +import Test.Tasty.HUnit + +test_simplify :: [TestTree] +test_simplify = + [ test + "\\and(_, _)" + (makeAndPredicate faCeil fbCeil) + [MultiAnd.make [faCeil, fbCeil]] + , test + "\\and(\\top, _)" + (makeAndPredicate makeTruePredicate faCeil) + [MultiAnd.make [faCeil]] + , test + "\\and(\\bottom, _)" + (makeAndPredicate makeFalsePredicate faCeil) + [] + , test + "\\or(_, _)" + (makeOrPredicate faCeil fbCeil) + [MultiAnd.singleton faCeil, MultiAnd.singleton fbCeil] + , test + "\\or(\\bottom, _)" + (makeOrPredicate makeFalsePredicate faCeil) + [MultiAnd.singleton faCeil] + , test + "\\or(\\top, _)" + (makeOrPredicate makeTruePredicate faCeil) + [MultiAnd.top] + ] + where + test :: + TestName -> + Predicate RewritingVariableName -> + [MultiAnd (Predicate RewritingVariableName)] -> + TestTree + test testName input expect = + testCase testName $ do + actual <- + simplify SideCondition.top input + & Test.runSimplifierBranch Mock.env + assertEqual "" expect actual + + fa, fb :: TermLike RewritingVariableName + fa = Mock.f Mock.a + fb = Mock.f Mock.b + + faCeil, fbCeil :: Predicate RewritingVariableName + faCeil = makeCeilPredicate fa + fbCeil = makeCeilPredicate fb From 2a7a1f04692d49a2c5e8a542b5a72baf3f1f5596 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 14 May 2021 13:23:51 -0500 Subject: [PATCH 08/44] Use Kore.Internal.From --- .../Test/Kore/Step/Simplification/Predicate.hs | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index 66bd6bb311..42b3770f92 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -2,6 +2,7 @@ module Test.Kore.Step.Simplification.Predicate ( test_simplify, ) where +import Kore.Internal.From import Kore.Internal.MultiAnd (MultiAnd) import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.Predicate @@ -19,27 +20,27 @@ test_simplify :: [TestTree] test_simplify = [ test "\\and(_, _)" - (makeAndPredicate faCeil fbCeil) + (fromAnd faCeil fbCeil) [MultiAnd.make [faCeil, fbCeil]] , test "\\and(\\top, _)" - (makeAndPredicate makeTruePredicate faCeil) + (fromAnd fromTop_ faCeil) [MultiAnd.make [faCeil]] , test "\\and(\\bottom, _)" - (makeAndPredicate makeFalsePredicate faCeil) + (fromAnd fromBottom_ faCeil) [] , test "\\or(_, _)" - (makeOrPredicate faCeil fbCeil) + (fromOr faCeil fbCeil) [MultiAnd.singleton faCeil, MultiAnd.singleton fbCeil] , test "\\or(\\bottom, _)" - (makeOrPredicate makeFalsePredicate faCeil) + (fromOr fromBottom_ faCeil) [MultiAnd.singleton faCeil] , test "\\or(\\top, _)" - (makeOrPredicate makeTruePredicate faCeil) + (fromOr fromTop_ faCeil) [MultiAnd.top] ] where @@ -60,5 +61,5 @@ test_simplify = fb = Mock.f Mock.b faCeil, fbCeil :: Predicate RewritingVariableName - faCeil = makeCeilPredicate fa - fbCeil = makeCeilPredicate fb + faCeil = fromCeil_ fa + fbCeil = fromCeil_ fb From 93725c6a1dedc99784364dfc222a4a5b97287a3d Mon Sep 17 00:00:00 2001 From: github-actions Date: Fri, 14 May 2021 19:36:34 +0000 Subject: [PATCH 09/44] Materialize Nix expressions --- nix/kore.nix.d/kore.nix | 2 ++ 1 file changed, 2 insertions(+) diff --git a/nix/kore.nix.d/kore.nix b/nix/kore.nix.d/kore.nix index efefd280d3..5aec38c4b1 100644 --- a/nix/kore.nix.d/kore.nix +++ b/nix/kore.nix.d/kore.nix @@ -365,6 +365,7 @@ "Kore/Step/Simplification/Overloading" "Kore/Step/Simplification/OverloadSimplifier" "Kore/Step/Simplification/Pattern" + "Kore/Step/Simplification/Predicate" "Kore/Step/Simplification/Rewrites" "Kore/Step/Simplification/Rule" "Kore/Step/Simplification/SetVariable" @@ -797,6 +798,7 @@ "Test/Kore/Step/Simplification/Or" "Test/Kore/Step/Simplification/OrPattern" "Test/Kore/Step/Simplification/Overloading" + "Test/Kore/Step/Simplification/Predicate" "Test/Kore/Step/Simplification/Pattern" "Test/Kore/Step/Simplification/Rule" "Test/Kore/Step/Simplification/StringLiteral" From abae992d9edee1f9dabd126d20ce38fb82b0e0a6 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 May 2021 15:37:37 -0500 Subject: [PATCH 10/44] Add docs/simplify-predicate.md --- docs/simplify-predicate.md | 88 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 docs/simplify-predicate.md diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md new file mode 100644 index 0000000000..ca60c2399a --- /dev/null +++ b/docs/simplify-predicate.md @@ -0,0 +1,88 @@ +# Simplifying predicates + +The goals of simplification are: + +1. Transform the predicate into [disjunctive normal form] (normalization). +2. Apply identities to reduce the complexity of the predicate (simplification proper). + +Simplification happens recursively, upward from the bottom. Therefore, we +describe the simplification steps based on the shape of the top-most +unsimplified clause of the predicate. + +## \and + +### Normalization + +Apply this distributive law over both arguments of `\and` until `P[n]` are all +in disjunctive normal form: + +``` kore +\and(\or(P[1], P[2]), P[3]) = \or(\and(P[1], P[3]), \and(P[2], P[3])) +``` + +### Simplification + +#### Identity + +``` kore +\and(\top, P[1]) = P[1] +``` + +#### Annihilation + +``` kore +\and(\bottom, _) = \bottom +``` + +#### Idempotence + +``` kore +\and(P[1], P[1]) = P[1] +``` + +#### Affirmation + +Idempotence is actually a special case of _affirmation_, + +``` kore +\and(P[1], P[2]) = \and(P[1], P[2](P[1] = \top)) +``` + +## \or + +### Normalization + +Assuming the children of `\or` are in disjunctive normal form, then the clause +is already normalized. + +### Simplification + +#### Identity + +``` kore +\or(\bottom, P[1]) = P[1] +``` + +#### Annihilation + +``` kore +\or(\top, _) = \top +``` + +#### Idempotence + +``` kore +\or(P[1], P[1]) = P[1] +``` + +#### Affirmation + +This one is not as useful as the rule for `\and`: + +``` kore +\or(P[1], P[2]) = \not(\and(\not(P[1]), \not(P[2]))) + = \not(\and(\not(P[1]), \not(P[2](P[1] = \bottom)))) + = \or(P[1], P[2](P[1] = \bottom)) +``` + +[disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file From 2fb5ae21cf41810c509cdc2f18dd938ea3d02381 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 May 2021 15:38:14 -0500 Subject: [PATCH 11/44] Distinguish normalization from simplification --- .../src/Kore/Step/Simplification/Predicate.hs | 12 ++-- .../Kore/Step/Simplification/Predicate.hs | 64 ++++++++++--------- 2 files changed, 41 insertions(+), 35 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 89a36f8c3a..6a19a27810 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -78,20 +78,20 @@ simplify sideCondition = case predicateF of AndF andF -> do let andF' = worker <$> andF - distributeAnd andF' + normalizeAnd andF' OrF orF -> do let orF' = worker <$> orF - distributeOr orF' + normalizeOr orF' _ -> simplifyPredicateTODO sideCondition predicate where _ :< predicateF = Recursive.project predicate -distributeAnd :: +normalizeAnd :: And sort (LogicT simplifier (MultiAnd (Predicate RewritingVariableName))) -> LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) -distributeAnd andF = fold <$> sequence andF +normalizeAnd andF = fold <$> sequence andF -distributeOr :: +normalizeOr :: Or sort (LogicT simplifier conjunction) -> LogicT simplifier conjunction -distributeOr = foldr1 (<|>) +normalizeOr = foldr1 (<|>) diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index 42b3770f92..990af4b4f7 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -3,7 +3,6 @@ module Test.Kore.Step.Simplification.Predicate ( ) where import Kore.Internal.From -import Kore.Internal.MultiAnd (MultiAnd) import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.Predicate import qualified Kore.Internal.SideCondition as SideCondition @@ -18,48 +17,55 @@ import Test.Tasty.HUnit test_simplify :: [TestTree] test_simplify = - [ test - "\\and(_, _)" - (fromAnd faCeil fbCeil) - [MultiAnd.make [faCeil, fbCeil]] - , test - "\\and(\\top, _)" - (fromAnd fromTop_ faCeil) - [MultiAnd.make [faCeil]] - , test - "\\and(\\bottom, _)" - (fromAnd fromBottom_ faCeil) - [] - , test - "\\or(_, _)" - (fromOr faCeil fbCeil) - [MultiAnd.singleton faCeil, MultiAnd.singleton fbCeil] - , test - "\\or(\\bottom, _)" - (fromOr fromBottom_ faCeil) - [MultiAnd.singleton faCeil] - , test - "\\or(\\top, _)" - (fromOr fromTop_ faCeil) - [MultiAnd.top] + [ testGroup "\\and" + [ test "Normalization" + (fromAnd (fromOr faCeil fbCeil) (fromOr gaCeil gbCeil)) + [ [faCeil, gaCeil] + , [fbCeil, gaCeil] + , [faCeil, gbCeil] + , [fbCeil, gbCeil] + ] + , test "Identity" + (fromAnd fromTop_ faCeil) + [[faCeil]] + , test "Annihilation" + (fromAnd fromBottom_ faCeil) + [] + ] + , testGroup "\\or" + [ test "Normalization" + (fromOr faCeil fbCeil) + [[faCeil], [fbCeil]] + , test "Identity" + (fromOr fromBottom_ faCeil) + [[faCeil]] + , test + "Annihilation" + (fromOr fromTop_ faCeil) + [[]] + ] ] where test :: TestName -> Predicate RewritingVariableName -> - [MultiAnd (Predicate RewritingVariableName)] -> + [[Predicate RewritingVariableName]] -> TestTree test testName input expect = testCase testName $ do actual <- simplify SideCondition.top input & Test.runSimplifierBranch Mock.env - assertEqual "" expect actual + assertEqual "" (MultiAnd.make <$> expect) actual - fa, fb :: TermLike RewritingVariableName + fa, fb, ga, gb :: TermLike RewritingVariableName fa = Mock.f Mock.a fb = Mock.f Mock.b + ga = Mock.g Mock.a + gb = Mock.g Mock.b - faCeil, fbCeil :: Predicate RewritingVariableName + faCeil, fbCeil, gaCeil, gbCeil :: Predicate RewritingVariableName faCeil = fromCeil_ fa fbCeil = fromCeil_ fb + gaCeil = fromCeil_ ga + gbCeil = fromCeil_ gb From fcd95cbeba395472791ead88d3c4ec2669972dce Mon Sep 17 00:00:00 2001 From: github-actions Date: Tue, 18 May 2021 20:40:30 +0000 Subject: [PATCH 12/44] Format with fourmolu --- .../Kore/Step/Simplification/Predicate.hs | 21 ++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index 990af4b4f7..ade0c0b3eb 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -17,26 +17,33 @@ import Test.Tasty.HUnit test_simplify :: [TestTree] test_simplify = - [ testGroup "\\and" - [ test "Normalization" + [ testGroup + "\\and" + [ test + "Normalization" (fromAnd (fromOr faCeil fbCeil) (fromOr gaCeil gbCeil)) [ [faCeil, gaCeil] , [fbCeil, gaCeil] , [faCeil, gbCeil] , [fbCeil, gbCeil] ] - , test "Identity" + , test + "Identity" (fromAnd fromTop_ faCeil) [[faCeil]] - , test "Annihilation" + , test + "Annihilation" (fromAnd fromBottom_ faCeil) [] ] - , testGroup "\\or" - [ test "Normalization" + , testGroup + "\\or" + [ test + "Normalization" (fromOr faCeil fbCeil) [[faCeil], [fbCeil]] - , test "Identity" + , test + "Identity" (fromOr fromBottom_ faCeil) [[faCeil]] , test From 95a9a8f11107d107df460c84c21fb0872d88e29a Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 May 2021 16:25:55 -0500 Subject: [PATCH 13/44] Run unification tests through OrPattern --- kore/test/Test/Kore/Unification/Unifier.hs | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index d4f9876456..5be09acbbf 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -14,6 +14,7 @@ import Data.Text ( Text, ) import qualified Kore.Internal.Condition as Condition +import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Predicate ( Predicate, ) @@ -187,12 +188,13 @@ andSimplify :: [UnificationResult] -> Assertion andSimplify term1 term2 results = do - let expect = map unificationResult results + let expect = OrPattern.fromPatterns $ map unificationResult results subst' <- - runNoSMT $ - runSimplifier testEnv $ - Monad.Unify.runUnifierT Not.notSimplifier $ - simplifyAnds (unificationProblem term1 term2 :| []) + simplifyAnds (unificationProblem term1 term2 :| []) + & Monad.Unify.runUnifierT Not.notSimplifier + & runSimplifier testEnv + & runNoSMT + & fmap OrPattern.fromPatterns assertEqual (message expect subst') expect subst' where message expected actual = @@ -201,11 +203,12 @@ andSimplify term1 term2 results = do , Pretty.indent 4 (unparse term1) , "with term:" , Pretty.indent 4 (unparse term2) - , "expected=" - , Pretty.indent 4 (foldMap unparse expected) - , "actual=" - , Pretty.indent 4 (foldMap unparse actual) + , "expected:" + , Pretty.indent 4 (unparseOrPattern expected) + , "actual:" + , Pretty.indent 4 (unparseOrPattern actual) ] + unparseOrPattern = Pretty.vsep . map unparse . OrPattern.toPatterns andSimplifyException :: HasCallStack => From d6650530d96b2051745bd0434029a54c2681148a Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 May 2021 16:26:16 -0500 Subject: [PATCH 14/44] Keep predicates in disjunctive normal form --- .../src/Kore/Step/Simplification/Condition.hs | 5 ++- .../src/Kore/Step/Simplification/Predicate.hs | 39 ++++++++++++++----- .../Kore/Step/Simplification/Predicate.hs | 7 +++- 3 files changed, 38 insertions(+), 13 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index c6b9ae16cb..d09c1a2524 100644 --- a/kore/src/Kore/Step/Simplification/Condition.hs +++ b/kore/src/Kore/Step/Simplification/Condition.hs @@ -87,6 +87,7 @@ simplify SubstitutionSimplifier{simplifySubstitution} sideCondition = simplified <- Predicate.simplify sideCondition predicate' + >>= Logic.scatter >>= simplifyPredicates sideCondition TopBottom.guardAgainstBottom simplified let merged = simplified <> Condition.fromSubstitution substitution @@ -151,7 +152,9 @@ simplifyPredicates initialSideCondition predicates = do (MultiAnd (Predicate RewritingVariableName)) worker (predicate, unsimplified) = do sideCondition <- SideCondition.addAssumptions unsimplified <$> State.get - results <- Predicate.simplify sideCondition predicate & lift + results <- + Predicate.simplify sideCondition predicate >>= Logic.scatter + & lift State.modify (SideCondition.addAssumptions results) return results diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 6a19a27810..068a443414 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -9,6 +9,10 @@ module Kore.Step.Simplification.Predicate ( import qualified Data.Functor.Foldable as Recursive import qualified Kore.Internal.Conditional as Conditional import Kore.Internal.MultiAnd (MultiAnd) +import Kore.Internal.MultiOr ( + MultiOr, + ) +import qualified Kore.Internal.MultiOr as MultiOr import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Condition, @@ -64,34 +68,49 @@ simplifyPredicateTODO sideCondition predicate = do , unparse conditional ] +type DisjunctiveNormalForm = + MultiOr (MultiAnd (Predicate RewritingVariableName)) + simplify :: + forall simplifier. ( HasCallStack , MonadSimplify simplifier ) => SideCondition RewritingVariableName -> Predicate RewritingVariableName -> - LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) + simplifier DisjunctiveNormalForm simplify sideCondition = worker where + worker :: + Predicate RewritingVariableName -> + simplifier DisjunctiveNormalForm worker predicate = case predicateF of AndF andF -> do let andF' = worker <$> andF - normalizeAnd andF' + normalizeAnd =<< sequence andF' OrF orF -> do let orF' = worker <$> orF - normalizeOr orF' - _ -> simplifyPredicateTODO sideCondition predicate + normalizeOr =<< sequence orF' + _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate normalizeAnd :: - And sort (LogicT simplifier (MultiAnd (Predicate RewritingVariableName))) -> - LogicT simplifier (MultiAnd (Predicate RewritingVariableName)) -normalizeAnd andF = fold <$> sequence andF + Applicative simplifier => + And sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +normalizeAnd andOr = + pure . MultiOr.observeAll $ do + -- andOr: \and(\or(_, _), \or(_, _)) + andAnd <- traverse Logic.scatter andOr + -- andAnd: \and(\and(_, _), \and(_, _)) + let multiAnd = fold andAnd + pure multiAnd normalizeOr :: - Or sort (LogicT simplifier conjunction) -> - LogicT simplifier conjunction -normalizeOr = foldr1 (<|>) + Applicative simplifier => + Or sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +normalizeOr = pure . fold diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index ade0c0b3eb..68ccb158dd 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -4,6 +4,7 @@ module Test.Kore.Step.Simplification.Predicate ( import Kore.Internal.From import qualified Kore.Internal.MultiAnd as MultiAnd +import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Predicate import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike (TermLike) @@ -62,8 +63,8 @@ test_simplify = testCase testName $ do actual <- simplify SideCondition.top input - & Test.runSimplifierBranch Mock.env - assertEqual "" (MultiAnd.make <$> expect) actual + & Test.runSimplifier Mock.env + assertEqual "" (mkDisjunctiveNormalForm expect) actual fa, fb, ga, gb :: TermLike RewritingVariableName fa = Mock.f Mock.a @@ -71,6 +72,8 @@ test_simplify = ga = Mock.g Mock.a gb = Mock.g Mock.b + mkDisjunctiveNormalForm = MultiOr.make . map MultiAnd.make + faCeil, fbCeil, gaCeil, gbCeil :: Predicate RewritingVariableName faCeil = fromCeil_ fa fbCeil = fromCeil_ fb From 3573e34fddc1d59d5d7336b7eb41d6c67f282f3e Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 May 2021 16:30:29 -0500 Subject: [PATCH 15/44] Normalized \bottom --- docs/simplify-predicate.md | 4 ++++ kore/src/Kore/Step/Simplification/Predicate.hs | 15 ++++++++++++++- .../Test/Kore/Step/Simplification/Predicate.hs | 7 +++++++ 3 files changed, 25 insertions(+), 1 deletion(-) diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md index ca60c2399a..673126f5ee 100644 --- a/docs/simplify-predicate.md +++ b/docs/simplify-predicate.md @@ -85,4 +85,8 @@ This one is not as useful as the rule for `\and`: = \or(P[1], P[2](P[1] = \bottom)) ``` +## \bottom + +`\bottom` is already in disjunctive normal form. + [disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 068a443414..da0dbf244e 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -30,7 +30,11 @@ import Kore.Rewriting.RewritingVariable ( RewritingVariableName, ) import Kore.Step.Simplification.Simplify -import Kore.Syntax (And, Or) +import Kore.Syntax ( + And, + Bottom, + Or, + ) import qualified Kore.TopBottom as TopBottom import Kore.Unparser import Logic @@ -93,6 +97,9 @@ simplify sideCondition = OrF orF -> do let orF' = worker <$> orF normalizeOr =<< sequence orF' + BottomF bottomF -> do + let bottomF' = worker <$> bottomF + normalizeBottom =<< sequence bottomF' _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate @@ -114,3 +121,9 @@ normalizeOr :: Or sort DisjunctiveNormalForm -> simplifier DisjunctiveNormalForm normalizeOr = pure . fold + +normalizeBottom :: + Applicative simplifier => + Bottom sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +normalizeBottom _ = pure MultiOr.bottom diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index 68ccb158dd..30c1739497 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -52,6 +52,13 @@ test_simplify = (fromOr fromTop_ faCeil) [[]] ] + , testGroup + "\\bottom" + [ test + "Normalization" + fromBottom_ + [] + ] ] where test :: From 96e99575cc2ca879a78a29a2751225c78514575c Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 May 2021 16:35:39 -0500 Subject: [PATCH 16/44] Normalize \top --- docs/simplify-predicate.md | 4 ++++ kore/src/Kore/Step/Simplification/Predicate.hs | 15 ++++++++++++++- .../Test/Kore/Step/Simplification/Predicate.hs | 7 +++++++ 3 files changed, 25 insertions(+), 1 deletion(-) diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md index 673126f5ee..0232ecccb8 100644 --- a/docs/simplify-predicate.md +++ b/docs/simplify-predicate.md @@ -89,4 +89,8 @@ This one is not as useful as the rule for `\and`: `\bottom` is already in disjunctive normal form. +## \top + +`\top` is already in disjunctive normal form. + [disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index da0dbf244e..6fdc96b1cf 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -8,7 +8,10 @@ module Kore.Step.Simplification.Predicate ( import qualified Data.Functor.Foldable as Recursive import qualified Kore.Internal.Conditional as Conditional -import Kore.Internal.MultiAnd (MultiAnd) +import Kore.Internal.MultiAnd ( + MultiAnd, + ) +import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.MultiOr ( MultiOr, ) @@ -34,6 +37,7 @@ import Kore.Syntax ( And, Bottom, Or, + Top, ) import qualified Kore.TopBottom as TopBottom import Kore.Unparser @@ -100,6 +104,9 @@ simplify sideCondition = BottomF bottomF -> do let bottomF' = worker <$> bottomF normalizeBottom =<< sequence bottomF' + TopF topF -> do + let topF' = worker <$> topF + normalizeTop =<< sequence topF' _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate @@ -127,3 +134,9 @@ normalizeBottom :: Bottom sort DisjunctiveNormalForm -> simplifier DisjunctiveNormalForm normalizeBottom _ = pure MultiOr.bottom + +normalizeTop :: + Applicative simplifier => + Top sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +normalizeTop _ = pure (MultiOr.singleton MultiAnd.top) diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index 30c1739497..139ad7daf6 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -59,6 +59,13 @@ test_simplify = fromBottom_ [] ] + , testGroup + "\\top" + [ test + "Normalization" + fromTop_ + [[]] + ] ] where test :: From edb3f672089916f54735608c126ccb4dc2f6bb35 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 May 2021 16:54:39 -0500 Subject: [PATCH 17/44] Implement fromNot for Predicate --- kore/src/Kore/Internal/Predicate.hs | 4 ++++ kore/test/Test/Kore/Internal/From.hs | 7 +++++++ 2 files changed, 11 insertions(+) diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs index a57fb38328..a2f56499e2 100644 --- a/kore/src/Kore/Internal/Predicate.hs +++ b/kore/src/Kore/Internal/Predicate.hs @@ -254,6 +254,10 @@ instance From (Iff () child) (PredicateF variable child) where from = IffF {-# INLINE from #-} +instance From (Not () child) (PredicateF variable child) where + from = NotF + {-# INLINE from #-} + newtype Predicate variable = Predicate { getPredicate :: Cofree (PredicateF variable) (PredicatePattern variable) diff --git a/kore/test/Test/Kore/Internal/From.hs b/kore/test/Test/Kore/Internal/From.hs index ac88f97278..bee253548e 100644 --- a/kore/test/Test/Kore/Internal/From.hs +++ b/kore/test/Test/Kore/Internal/From.hs @@ -18,6 +18,7 @@ import Kore.Syntax.Forall import Kore.Syntax.Iff import Kore.Syntax.Implies import Kore.Syntax.In +import Kore.Syntax.Not import Kore.Syntax.Or import Kore.Syntax.Variable import Prelude.Kore @@ -124,4 +125,10 @@ test_Predicate = assertEqual "Expected \\top" fromTop_ iffFirst assertEqual "Expected \\bottom" fromBottom_ iffSecond _ -> assertFailure "Expected IffF" + , testCase "\\not(\\top())" $ do + let actual = fromNot fromTop_ + case fromPredicate actual of + NotF Not{notChild} -> do + assertEqual "Expected \\top" fromTop_ notChild + _ -> assertFailure "Expected NotF" ] From 745e50ad8540aae4b4face74f9fc1e8b7aca8b87 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 19 May 2021 16:17:14 -0500 Subject: [PATCH 18/44] MultiOr: Add traverseOr --- kore/src/Kore/Internal/MultiOr.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/kore/src/Kore/Internal/MultiOr.hs b/kore/src/Kore/Internal/MultiOr.hs index c2ea6fcc03..f95b53579f 100644 --- a/kore/src/Kore/Internal/MultiOr.hs +++ b/kore/src/Kore/Internal/MultiOr.hs @@ -343,3 +343,14 @@ traverse :: f (MultiOr child2) traverse f = fmap make . Traversable.traverse f . toList {-# INLINE traverse #-} + +-- | Traverse a @MultiOr@ using an action that returns a disjunction. +traverseOr :: + Ord child2 => + TopBottom child2 => + Applicative f => + (child1 -> f (MultiOr child2)) -> + MultiOr child1 -> + f (MultiOr child2) +traverseOr f = fmap fold . traverse f +{-# INLINE traverseOr #-} From 2b12a7a3ef0e80cedb4106f899b40797b5530450 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 19 May 2021 16:18:58 -0500 Subject: [PATCH 19/44] Move distributeAnd to MultiAnd --- kore/src/Kore/Internal/MultiAnd.hs | 16 ++++++++++++++++ kore/src/Kore/Internal/MultiOr.hs | 17 +---------------- kore/src/Kore/Step/Simplification/Not.hs | 2 +- kore/test/Test/Kore/Internal/OrPattern.hs | 2 +- 4 files changed, 19 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Internal/MultiAnd.hs b/kore/src/Kore/Internal/MultiAnd.hs index b801e33e4a..05b1d079ee 100644 --- a/kore/src/Kore/Internal/MultiAnd.hs +++ b/kore/src/Kore/Internal/MultiAnd.hs @@ -20,6 +20,7 @@ module Kore.Internal.MultiAnd ( singleton, map, traverse, + distributeAnd, ) where import qualified Data.Functor.Foldable as Recursive @@ -35,6 +36,10 @@ import Kore.Attribute.Pattern.FreeVariables ( import Kore.Internal.Condition ( Condition, ) +import Kore.Internal.MultiOr ( + MultiOr, + ) +import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Predicate ( Predicate, getMultiAndPredicate, @@ -49,6 +54,7 @@ import Kore.Internal.Variable import Kore.TopBottom ( TopBottom (..), ) +import qualified Logic import Prelude.Kore hiding ( map, traverse, @@ -251,3 +257,13 @@ traverse :: f (MultiAnd child2) traverse f = fmap make . Traversable.traverse f . toList {-# INLINE traverse #-} + +distributeAnd :: + Ord term => + TopBottom term => + MultiAnd (MultiOr term) -> + MultiOr (MultiAnd term) +distributeAnd multiAnd = + MultiOr.observeAll $ traverse Logic.scatter multiAnd +{-# INLINE distributeAnd #-} + diff --git a/kore/src/Kore/Internal/MultiOr.hs b/kore/src/Kore/Internal/MultiOr.hs index f95b53579f..f72b66f8f9 100644 --- a/kore/src/Kore/Internal/MultiOr.hs +++ b/kore/src/Kore/Internal/MultiOr.hs @@ -15,7 +15,6 @@ module Kore.Internal.MultiOr ( bottom, filterOr, flatten, - distributeAnd, distributeApplication, gather, observeAllT, @@ -26,6 +25,7 @@ module Kore.Internal.MultiOr ( singleton, map, traverse, + traverseOr, -- * Re-exports Alternative (..), @@ -43,10 +43,6 @@ import GHC.Exts ( import qualified GHC.Generics as GHC import qualified Generics.SOP as SOP import Kore.Debug -import Kore.Internal.MultiAnd ( - MultiAnd, - ) -import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Syntax.Application ( Application (..), ) @@ -162,17 +158,6 @@ singleton term | isBottom term = MultiOr [] | otherwise = MultiOr [term] -distributeAnd :: - Ord term => - TopBottom term => - MultiAnd (MultiOr term) -> - MultiOr (MultiAnd term) -distributeAnd = - foldr (crossProductGeneric and') (singleton MultiAnd.top) - where - and' term ma = - MultiAnd.singleton term <> ma - distributeApplication :: Ord head => Ord term => diff --git a/kore/src/Kore/Step/Simplification/Not.hs b/kore/src/Kore/Step/Simplification/Not.hs index 028551d56d..31366a2b11 100644 --- a/kore/src/Kore/Step/Simplification/Not.hs +++ b/kore/src/Kore/Step/Simplification/Not.hs @@ -218,7 +218,7 @@ scatterAnd :: TopBottom child => MultiAnd (MultiOr child) -> LogicT m (MultiAnd child) -scatterAnd = scatter . MultiOr.distributeAnd +scatterAnd = scatter . MultiAnd.distributeAnd -- | Conjoin and simplify a 'MultiAnd' of 'Pattern'. mkMultiAndPattern :: diff --git a/kore/test/Test/Kore/Internal/OrPattern.hs b/kore/test/Test/Kore/Internal/OrPattern.hs index 8f09094935..b29bf714ae 100644 --- a/kore/test/Test/Kore/Internal/OrPattern.hs +++ b/kore/test/Test/Kore/Internal/OrPattern.hs @@ -19,10 +19,10 @@ import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range import Kore.Internal.MultiAnd ( MultiAnd, + distributeAnd, ) import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.MultiOr ( - distributeAnd, distributeApplication, ) import qualified Kore.Internal.MultiOr as MultiOr From a460f91a9ae1163bc906c6462408fe879a5388cc Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 19 May 2021 16:19:13 -0500 Subject: [PATCH 20/44] AndPredicates: Use scatter --- kore/src/Kore/Step/Simplification/AndPredicates.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/AndPredicates.hs b/kore/src/Kore/Step/Simplification/AndPredicates.hs index d09c60a29a..6b7a4098aa 100644 --- a/kore/src/Kore/Step/Simplification/AndPredicates.hs +++ b/kore/src/Kore/Step/Simplification/AndPredicates.hs @@ -15,6 +15,7 @@ import qualified Kore.Internal.Condition as Condition import Kore.Internal.MultiAnd ( MultiAnd, ) +import qualified Kore.Internal.MultiAnd as MultiAnd import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.OrCondition ( OrCondition, @@ -38,10 +39,9 @@ simplifyEvaluatedMultiPredicate :: SideCondition RewritingVariableName -> MultiAnd (OrCondition RewritingVariableName) -> simplifier (OrCondition RewritingVariableName) -simplifyEvaluatedMultiPredicate sideCondition predicates = do - let crossProduct = MultiOr.distributeAnd predicates +simplifyEvaluatedMultiPredicate sideCondition predicates = MultiOr.observeAllT $ do - element <- LogicT.scatter crossProduct + element <- MultiAnd.traverse LogicT.scatter predicates andConditions element where andConditions predicates' = From 79e71afc7e2e30cd34dce5753124eaf5df691ed8 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 19 May 2021 16:19:29 -0500 Subject: [PATCH 21/44] MultiAnd: Add traverseOr and traverseOrAnd --- kore/src/Kore/Internal/MultiAnd.hs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/kore/src/Kore/Internal/MultiAnd.hs b/kore/src/Kore/Internal/MultiAnd.hs index 05b1d079ee..7b780902ec 100644 --- a/kore/src/Kore/Internal/MultiAnd.hs +++ b/kore/src/Kore/Internal/MultiAnd.hs @@ -21,6 +21,8 @@ module Kore.Internal.MultiAnd ( map, traverse, distributeAnd, + traverseOr, + traverseOrAnd, ) where import qualified Data.Functor.Foldable as Recursive @@ -267,3 +269,22 @@ distributeAnd multiAnd = MultiOr.observeAll $ traverse Logic.scatter multiAnd {-# INLINE distributeAnd #-} +traverseOr :: + Ord child2 => + TopBottom child2 => + Applicative f => + (child1 -> f (MultiOr child2)) -> + MultiAnd child1 -> + f (MultiOr (MultiAnd child2)) +traverseOr f = fmap distributeAnd . traverse f +{-# INLINE traverseOr #-} + +traverseOrAnd :: + Ord child2 => + TopBottom child2 => + Applicative f => + (child1 -> f (MultiOr (MultiAnd child2))) -> + MultiOr (MultiAnd child1) -> + f (MultiOr (MultiAnd child2)) +traverseOrAnd f = MultiOr.traverseOr (fmap (MultiOr.map fold) . traverseOr f) +{-# INLINE traverseOrAnd #-} From 66516986d04d905aed0cdfebf06c46005ae54bad Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 19 May 2021 16:20:12 -0500 Subject: [PATCH 22/44] [RED] Simplify Not predicates --- .../src/Kore/Step/Simplification/Predicate.hs | 62 ++++++++++++++----- 1 file changed, 48 insertions(+), 14 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 6fdc96b1cf..20736970b4 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -35,9 +35,10 @@ import Kore.Rewriting.RewritingVariable ( import Kore.Step.Simplification.Simplify import Kore.Syntax ( And, - Bottom, + Bottom (..), + Not (..), Or, - Top, + Top (..), ) import qualified Kore.TopBottom as TopBottom import Kore.Unparser @@ -95,18 +96,11 @@ simplify sideCondition = simplifier DisjunctiveNormalForm worker predicate = case predicateF of - AndF andF -> do - let andF' = worker <$> andF - normalizeAnd =<< sequence andF' - OrF orF -> do - let orF' = worker <$> orF - normalizeOr =<< sequence orF' - BottomF bottomF -> do - let bottomF' = worker <$> bottomF - normalizeBottom =<< sequence bottomF' - TopF topF -> do - let topF' = worker <$> topF - normalizeTop =<< sequence topF' + AndF andF -> normalizeAnd =<< traverse worker andF + OrF orF -> normalizeOr =<< traverse worker orF + BottomF bottomF -> normalizeBottom =<< traverse worker bottomF + TopF topF -> normalizeTop =<< traverse worker topF + NotF notF -> simplifyNot =<< traverse worker notF _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate @@ -140,3 +134,43 @@ normalizeTop :: Top sort DisjunctiveNormalForm -> simplifier DisjunctiveNormalForm normalizeTop _ = pure (MultiOr.singleton MultiAnd.top) + +simplifyNot :: + Monad simplifier => + Not sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +simplifyNot notF@Not{notChild, notSort} + | TopBottom.isTop notChild = normalizeBottom Bottom{bottomSort = notSort} + | TopBottom.isBottom notChild = normalizeTop Top{topSort = notSort} + | otherwise = normalizeNot notF + +normalizeMultiAnd :: + Applicative simplifier => + MultiAnd DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +normalizeMultiAnd andOr = + pure . MultiOr.observeAll $ do + -- andOr: \and(\or(_, _), \or(_, _)) + andAnd <- MultiAnd.traverse Logic.scatter andOr + -- andAnd: \and(\and(_, _), \and(_, _)) + pure (fold andAnd) + +normalizeNot :: + forall simplifier sort. + Monad simplifier => + Not sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +normalizeNot = normalizeNotOr + where + normalizeNotOr Not{notChild = multiOr, notSort} = do + disjunctiveNormalForms <- Logic.observeAllT $ do + multiAnd <- Logic.scatter multiOr + normalizeNotAnd Not{notSort, notChild = multiAnd} & lift + normalizeMultiAnd (MultiAnd.make disjunctiveNormalForms) + normalizeNotAnd :: + Not sort (MultiAnd (Predicate RewritingVariableName)) -> + simplifier DisjunctiveNormalForm + normalizeNotAnd Not{notChild} = + MultiOr.observeAllT $ do + predicate <- Logic.scatter notChild + pure (MultiAnd.singleton $ fromNot predicate) From 6a4a8dcedfae31768dc9e397e630dfe490f49b12 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 19 May 2021 20:16:25 -0500 Subject: [PATCH 23/44] Fix (some) Not simplifier tests --- docs/simplify-predicate.md | 22 ++++++++++++++ .../src/Kore/Step/Simplification/Predicate.hs | 30 +++++++++++++++---- 2 files changed, 47 insertions(+), 5 deletions(-) diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md index 0232ecccb8..2c5f5b7b24 100644 --- a/docs/simplify-predicate.md +++ b/docs/simplify-predicate.md @@ -93,4 +93,26 @@ This one is not as useful as the rule for `\and`: `\top` is already in disjunctive normal form. +## \not + +### Normalization + +``` kore +\not(\or(P[1], P[2])) = \and(\not(P[1]), \not(P[2])) +``` + +### Simplification + +#### \top + +``` kore +\not(\top) = \bottom +``` + +#### \bottom + +``` kore +\not(\bottom) = \top +``` + [disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 20736970b4..34748e34f6 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -8,6 +8,7 @@ module Kore.Step.Simplification.Predicate ( import qualified Data.Functor.Foldable as Recursive import qualified Kore.Internal.Conditional as Conditional +import Kore.Internal.From import Kore.Internal.MultiAnd ( MultiAnd, ) @@ -29,6 +30,7 @@ import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.SideCondition ( SideCondition, ) +import qualified Kore.Internal.SideCondition as SideCondition import Kore.Rewriting.RewritingVariable ( RewritingVariableName, ) @@ -89,8 +91,22 @@ simplify :: Predicate RewritingVariableName -> simplifier DisjunctiveNormalForm simplify sideCondition = - worker + loop . MultiOr.singleton . MultiAnd.singleton where + loop :: DisjunctiveNormalForm -> simplifier DisjunctiveNormalForm + loop input = do + output <- MultiAnd.traverseOrAnd worker input + if input == output + then return (mark output) + else loop output + + mark :: DisjunctiveNormalForm -> DisjunctiveNormalForm + mark = + (MultiOr.map . MultiAnd.map) + (Predicate.markSimplifiedConditional reprSideCondition) + + reprSideCondition = SideCondition.toRepresentation sideCondition + worker :: Predicate RewritingVariableName -> simplifier DisjunctiveNormalForm @@ -170,7 +186,11 @@ normalizeNot = normalizeNotOr normalizeNotAnd :: Not sort (MultiAnd (Predicate RewritingVariableName)) -> simplifier DisjunctiveNormalForm - normalizeNotAnd Not{notChild} = - MultiOr.observeAllT $ do - predicate <- Logic.scatter notChild - pure (MultiAnd.singleton $ fromNot predicate) + normalizeNotAnd Not{notChild = predicates} + | TopBottom.isTop predicates = + pure MultiOr.bottom + | TopBottom.isBottom predicates = + (pure . MultiOr.singleton) MultiAnd.top + | otherwise = + (pure . MultiOr.singleton . MultiAnd.singleton) + (fromNot $ MultiAnd.toPredicate predicates) From 4c5f6cb585cf9779e14119b7f51edf634639bda8 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 20 May 2021 11:52:40 -0500 Subject: [PATCH 24/44] Simplify double negation --- docs/simplify-predicate.md | 6 +++++ .../src/Kore/Step/Simplification/Predicate.hs | 25 +++++++++++++------ .../Kore/Step/Simplification/Predicate.hs | 19 ++++++++++++++ 3 files changed, 42 insertions(+), 8 deletions(-) diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md index 2c5f5b7b24..df739b3f68 100644 --- a/docs/simplify-predicate.md +++ b/docs/simplify-predicate.md @@ -115,4 +115,10 @@ This one is not as useful as the rule for `\and`: \not(\bottom) = \top ``` +#### \not + +``` kore +\not(\not(P)) = P +``` + [disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 34748e34f6..902ca7ab50 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -186,11 +186,20 @@ normalizeNot = normalizeNotOr normalizeNotAnd :: Not sort (MultiAnd (Predicate RewritingVariableName)) -> simplifier DisjunctiveNormalForm - normalizeNotAnd Not{notChild = predicates} - | TopBottom.isTop predicates = - pure MultiOr.bottom - | TopBottom.isBottom predicates = - (pure . MultiOr.singleton) MultiAnd.top - | otherwise = - (pure . MultiOr.singleton . MultiAnd.singleton) - (fromNot $ MultiAnd.toPredicate predicates) + normalizeNotAnd Not{notChild = predicates} = + normalized + & MultiOr.singleton + & pure + where + fallback = + MultiAnd.singleton (fromNot $ MultiAnd.toPredicate predicates) + normalized = + case toList predicates of + [predicate] -> + case predicateF of + NotF Not{notChild = result} -> + MultiAnd.fromPredicate result + _ -> fallback + where + _ :< predicateF = Recursive.project predicate + _ -> fallback diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index 139ad7daf6..8b368b2dc9 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -66,6 +66,25 @@ test_simplify = fromTop_ [[]] ] + , testGroup + "\\not" + [ test + "Normalization" + (fromNot $ fromOr faCeil fbCeil) + [[fromNot faCeil, fromNot fbCeil]] + , test + "\\top" + (fromNot fromTop_) + [] + , test + "\\bottom" + (fromNot fromBottom_) + [[]] + , test + "\\not" + (fromNot $ fromNot faCeil) + [[faCeil]] + ] ] where test :: From 904c53b24466474dc65c8025e548f5d1762f2ae4 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 20 May 2021 11:52:53 -0500 Subject: [PATCH 25/44] RewriteStep: Update tests --- kore/test/Test/Kore/Step/RewriteStep.hs | 97 ++++++++++++++----------- 1 file changed, 53 insertions(+), 44 deletions(-) diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 5de66a6de6..bc50b43b95 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -21,6 +21,7 @@ import Kore.Attribute.Pattern.FreeVariables ( ) import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import qualified Kore.Internal.Conditional as Conditional +import qualified Kore.Internal.MultiAnd as MultiAnd import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Predicate as Predicate ( makeAndPredicate, @@ -1336,14 +1337,15 @@ test_applyRewriteRulesParallel = -- with ¬(⌈cf⌉ and ⌈cg⌉ and [x=a]) -- and ¬(⌈cf⌉ and ⌈cg⌉ and [x=b]) let definedBranches = - makeAndPredicate - (makeCeilPredicate Mock.cf) - (makeCeilPredicate Mock.cg) + MultiAnd.make + [ makeCeilPredicate Mock.cf + , makeCeilPredicate Mock.cg + ] results = OrPattern.fromPatterns [ Conditional { term = Mock.cf - , predicate = definedBranches + , predicate = MultiAnd.toPredicate definedBranches , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution @@ -1351,34 +1353,37 @@ test_applyRewriteRulesParallel = } , Conditional { term = Mock.cg - , predicate = definedBranches + , predicate = MultiAnd.toPredicate definedBranches , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution [(inject Mock.xConfig, Mock.b)] } ] + aBranch = + Predicate.makeEqualsPredicate + (mkElemVar Mock.xConfig) + Mock.a + & MultiAnd.singleton + & mappend definedBranches + aBranchNot = + MultiAnd.toPredicate aBranch + & makeNotPredicate + bBranch = + Predicate.makeEqualsPredicate + (mkElemVar Mock.xConfig) + Mock.b + & MultiAnd.singleton + & mappend definedBranches + bBranchNot = + MultiAnd.toPredicate bBranch + & makeNotPredicate remainders = OrPattern.fromPatterns [ initial { predicate = - Predicate.makeAndPredicate - ( makeNotPredicate $ - makeAndPredicate - definedBranches - ( Predicate.makeEqualsPredicate - (mkElemVar Mock.xConfig) - Mock.a - ) - ) - ( makeNotPredicate $ - makeAndPredicate - definedBranches - ( Predicate.makeEqualsPredicate - (mkElemVar Mock.xConfig) - Mock.b - ) - ) + (MultiAnd.toPredicate . MultiAnd.make) + [aBranchNot, bBranchNot] } ] initialTerm = @@ -1559,14 +1564,15 @@ test_applyRewriteRulesSequence = -- with ¬(⌈cf⌉ and [x=a]) -- and ¬(⌈cg⌉ and [x=b]) let definedBranches = - makeAndPredicate - (makeCeilPredicate Mock.cf) - (makeCeilPredicate Mock.cg) + MultiAnd.make + [ makeCeilPredicate Mock.cf + , makeCeilPredicate Mock.cg + ] results = OrPattern.fromPatterns [ Conditional { term = Mock.cf - , predicate = definedBranches + , predicate = MultiAnd.toPredicate definedBranches , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution @@ -1574,34 +1580,37 @@ test_applyRewriteRulesSequence = } , Conditional { term = Mock.cg - , predicate = definedBranches + , predicate = MultiAnd.toPredicate definedBranches , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution [(inject Mock.xConfig, Mock.b)] } ] + aBranch = + Predicate.makeEqualsPredicate + (mkElemVar Mock.xConfig) + Mock.a + & MultiAnd.singleton + & mappend definedBranches + aBranchNot = + MultiAnd.toPredicate aBranch + & makeNotPredicate + bBranch = + Predicate.makeEqualsPredicate + (mkElemVar Mock.xConfig) + Mock.b + & MultiAnd.singleton + & mappend definedBranches + bBranchNot = + MultiAnd.toPredicate bBranch + & makeNotPredicate remainders = OrPattern.fromPatterns [ initial { predicate = - Predicate.makeAndPredicate - ( Predicate.makeNotPredicate $ - Predicate.makeAndPredicate - definedBranches - ( Predicate.makeEqualsPredicate - (mkElemVar Mock.xConfig) - Mock.a - ) - ) - ( Predicate.makeNotPredicate $ - Predicate.makeAndPredicate - definedBranches - ( Predicate.makeEqualsPredicate - (mkElemVar Mock.xConfig) - Mock.b - ) - ) + (MultiAnd.toPredicate . MultiAnd.make) + [aBranchNot, bBranchNot] } ] initialTerm = From c880d3df859d44dd574e81735aaabd1526edb397 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 21 May 2021 09:30:01 -0500 Subject: [PATCH 26/44] Recursively mark predicates simplified --- kore/src/Kore/Step/Simplification/Predicate.hs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 902ca7ab50..aa544bb903 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -102,8 +102,13 @@ simplify sideCondition = mark :: DisjunctiveNormalForm -> DisjunctiveNormalForm mark = - (MultiOr.map . MultiAnd.map) - (Predicate.markSimplifiedConditional reprSideCondition) + (MultiOr.map . MultiAnd.map) mark1 + + mark1 :: + Predicate RewritingVariableName -> + Predicate RewritingVariableName + mark1 = + Recursive.fold $ Predicate.markSimplifiedConditional reprSideCondition . Recursive.embed reprSideCondition = SideCondition.toRepresentation sideCondition From 64f6e8b8c610728f43e3991007f9cac2cec1774d Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 21 May 2021 09:30:19 -0500 Subject: [PATCH 27/44] assertEquivalentPatterns: Give a useful error message --- kore/test/Test/Kore/Internal/Pattern.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/kore/test/Test/Kore/Internal/Pattern.hs b/kore/test/Test/Kore/Internal/Pattern.hs index a68551f1bf..c9d3063415 100644 --- a/kore/test/Test/Kore/Internal/Pattern.hs +++ b/kore/test/Test/Kore/Internal/Pattern.hs @@ -401,6 +401,7 @@ assertEquivalentPatterns :: Foldable t => InternalVariable variable => Diff variable => + HasCallStack => t (Pattern variable) -> t (Pattern variable) -> IO () From bd5d33e722ab6361070a1418aba45888a77c10ee Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 21 May 2021 14:04:27 -0500 Subject: [PATCH 28/44] Ignore simplification side condition in Predicate simplifier --- kore/src/Kore/Step/Simplification/Predicate.hs | 6 +----- .../Test/Kore/Step/Simplification/Integration.hs | 13 ++++++++++--- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index aa544bb903..f565cf2e75 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -30,7 +30,6 @@ import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.SideCondition ( SideCondition, ) -import qualified Kore.Internal.SideCondition as SideCondition import Kore.Rewriting.RewritingVariable ( RewritingVariableName, ) @@ -107,10 +106,7 @@ simplify sideCondition = mark1 :: Predicate RewritingVariableName -> Predicate RewritingVariableName - mark1 = - Recursive.fold $ Predicate.markSimplifiedConditional reprSideCondition . Recursive.embed - - reprSideCondition = SideCondition.toRepresentation sideCondition + mark1 = Recursive.fold $ Predicate.markSimplified . Recursive.embed worker :: Predicate RewritingVariableName -> diff --git a/kore/test/Test/Kore/Step/Simplification/Integration.hs b/kore/test/Test/Kore/Step/Simplification/Integration.hs index 7b96c55538..fcb379828f 100644 --- a/kore/test/Test/Kore/Step/Simplification/Integration.hs +++ b/kore/test/Test/Kore/Step/Simplification/Integration.hs @@ -21,6 +21,7 @@ import Kore.Equation ( mkEquation, ) import qualified Kore.Equation as Equation +import qualified Kore.Internal.Condition as Condition import Kore.Internal.SideCondition ( SideCondition, ) @@ -32,6 +33,7 @@ import qualified Kore.Internal.SideCondition as SideCondition ( import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ( Representation, ) +import qualified Kore.Internal.TermLike as TermLike import Kore.Rewriting.RewritingVariable ( RewritingVariableName, mkConfigVariable, @@ -51,6 +53,7 @@ import qualified Kore.Step.Simplification.Pattern as Pattern ( makeEvaluate, ) import Kore.Step.Simplification.Simplify +import Kore.Unparser import Prelude.Kore import Test.Kore import Test.Kore.Equation.Common ( @@ -782,9 +785,13 @@ test_simplificationIntegration = , predicate = makeTruePredicate , substitution = mempty } - assertBool - "Expecting simplification" - (OrPattern.isSimplified sideRepresentation actual) + + for_ (toList actual) $ \pattern' -> do + let message = (show . unparse) pattern' + let (term, condition) = Pattern.splitTerm pattern' + assertBool "Expected simplified term" (TermLike.isSimplified sideRepresentation term) + assertBool (unlines ["Expected simplified condition:", message]) (Condition.isSimplified sideRepresentation condition) + assertBool message (Pattern.isSimplified sideRepresentation pattern') , testCase "Equals-in simplification" $ do let gt = mkSetVariable (testId "gt") Mock.stringSort From ce118cac482db24e239237dee0c563521c406a01 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 21 May 2021 16:43:26 -0500 Subject: [PATCH 29/44] Implement Implies simplification --- docs/simplify-predicate.md | 24 ++++++++ .../src/Kore/Step/Simplification/Predicate.hs | 27 ++++++++- .../Test/Kore/Step/Simplification/Pattern.hs | 57 ++++++++++++++----- .../Kore/Step/Simplification/Predicate.hs | 40 ++++++++++++- 4 files changed, 131 insertions(+), 17 deletions(-) diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md index df739b3f68..6e13bbecdc 100644 --- a/docs/simplify-predicate.md +++ b/docs/simplify-predicate.md @@ -121,4 +121,28 @@ This one is not as useful as the rule for `\and`: \not(\not(P)) = P ``` +## \implies + +### Normalization + +``` kore +normalize(\implies(L, R)) = \or(normalize(\not(L)), normalize(\and(L, R))) +``` + +Note: We carry `L` through to the right-hand side because this maximizes the +information content of the second clause of the disjunction. + +### Simplification + +#### \top + +``` kore +\implies(\top, P) = P +``` + +#### \bottom +``` kore +\implies(\bottom, _) = \top +``` + [disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index f565cf2e75..b4c3760a85 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -35,8 +35,9 @@ import Kore.Rewriting.RewritingVariable ( ) import Kore.Step.Simplification.Simplify import Kore.Syntax ( - And, + And (..), Bottom (..), + Implies (..), Not (..), Or, Top (..), @@ -118,6 +119,7 @@ simplify sideCondition = BottomF bottomF -> normalizeBottom =<< traverse worker bottomF TopF topF -> normalizeTop =<< traverse worker topF NotF notF -> simplifyNot =<< traverse worker notF + ImpliesF impliesF -> simplifyImplies =<< traverse worker impliesF _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate @@ -204,3 +206,26 @@ normalizeNot = normalizeNotOr where _ :< predicateF = Recursive.project predicate _ -> fallback + +simplifyImplies :: + Monad simplifier => + Implies sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} + | TopBottom.isTop impliesFirst = pure impliesSecond + | TopBottom.isBottom impliesFirst = normalizeTop Top{topSort = impliesSort} + | otherwise = do + impliesFirst' <- + simplifyNot + Not + { notSort = impliesSort + , notChild = impliesFirst + } + impliesSecond' <- + normalizeAnd + And + { andSort = impliesSort + , andFirst = impliesFirst + , andSecond = impliesSecond + } + pure (impliesFirst' <> impliesSecond') \ No newline at end of file diff --git a/kore/test/Test/Kore/Step/Simplification/Pattern.hs b/kore/test/Test/Kore/Step/Simplification/Pattern.hs index 3973e44ce0..c70f364b2a 100644 --- a/kore/test/Test/Kore/Step/Simplification/Pattern.hs +++ b/kore/test/Test/Kore/Step/Simplification/Pattern.hs @@ -165,9 +165,10 @@ test_Pattern_simplify = let expect = Pattern.fromTermAndPredicate (Mock.constr10 fOfX) - ( makeAndPredicate - (makeEqualsPredicate fOfX gOfX) - (makeNotPredicate $ makeCeilPredicate fOfX) + ( (MultiAnd.toPredicate . MultiAnd.make) + [ makeEqualsPredicate fOfX gOfX + , makeNotPredicate $ makeCeilPredicate fOfX + ] ) actual <- simplify $ @@ -211,9 +212,17 @@ test_Pattern_simplify_equalityterm = [ makeCeilPredicate Mock.cf , makeCeilPredicate Mock.cg , makeEqualsPredicate Mock.cf Mock.cg - , makeImpliesPredicate - (makeCeilPredicate Mock.ch) - (makeEqualsPredicate Mock.cf Mock.ch) + , makeNotPredicate (makeCeilPredicate Mock.ch) + ] + ) + , Pattern.fromTermAndPredicate + (mkTop Mock.testSort) + ( MultiAnd.toPredicate . MultiAnd.make $ + [ makeCeilPredicate Mock.cf + , makeCeilPredicate Mock.cg + , makeCeilPredicate Mock.ch + , makeEqualsPredicate Mock.cf Mock.cg + , makeEqualsPredicate Mock.cf Mock.ch ] ) , Pattern.fromTermAndPredicate @@ -222,9 +231,17 @@ test_Pattern_simplify_equalityterm = [ makeCeilPredicate Mock.cf , makeCeilPredicate Mock.ch , makeEqualsPredicate Mock.cf Mock.ch - , makeImpliesPredicate - (makeCeilPredicate Mock.cg) - (makeEqualsPredicate Mock.cf Mock.cg) + , makeNotPredicate $ makeCeilPredicate Mock.cg + ] + ) + , Pattern.fromTermAndPredicate + (mkTop Mock.testSort) + ( MultiAnd.toPredicate . MultiAnd.make $ + [ makeCeilPredicate Mock.cf + , makeCeilPredicate Mock.ch + , makeCeilPredicate Mock.cg + , makeEqualsPredicate Mock.cf Mock.ch + , makeEqualsPredicate Mock.cf Mock.cg ] ) , Pattern.fromTermAndPredicate @@ -284,9 +301,21 @@ test_Pattern_simplify_equalityterm = [ definedF , definedG , makeEqualsPredicate Mock.cf Mock.cg - , makeImpliesPredicate - definedH - (makeEqualsPredicate Mock.cf Mock.ch) + , makeNotPredicate definedH + ] + , substitution = + Substitution.unsafeWrap + [(inject Mock.xConfig, Mock.a)] + } + , Conditional + { term = mkTop Mock.testSort + , predicate = + (MultiAnd.toPredicate . MultiAnd.make) + [ definedF + , definedG + , definedH + , makeEqualsPredicate Mock.cf Mock.cg + , makeEqualsPredicate Mock.cf Mock.ch ] , substitution = Substitution.unsafeWrap @@ -298,9 +327,7 @@ test_Pattern_simplify_equalityterm = [ definedF , definedH , makeEqualsPredicate Mock.cf Mock.ch - , makeImpliesPredicate - definedGWithSubstitution - (makeEqualsPredicate Mock.cf Mock.cg) + , makeNotPredicate definedGWithSubstitution ] ) , Pattern.fromTermAndPredicate diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index 8b368b2dc9..a305b0b380 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -11,6 +11,7 @@ import Kore.Internal.TermLike (TermLike) import Kore.Rewriting.RewritingVariable import Kore.Step.Simplification.Predicate (simplify) import Prelude.Kore +import qualified Pretty import qualified Test.Kore.Step.MockSymbols as Mock import qualified Test.Kore.Step.Simplification as Test import Test.Tasty @@ -85,6 +86,29 @@ test_simplify = (fromNot $ fromNot faCeil) [[faCeil]] ] + , testGroup + "\\implies" + [ test + "Normalization" + ( fromImplies + (fromOr faCeil fbCeil) + (fromOr gaCeil gbCeil) + ) + [ [fromNot faCeil, fromNot fbCeil] + , [faCeil, gaCeil] + , [fbCeil, gaCeil] + , [faCeil, gbCeil] + , [fbCeil, gbCeil] + ] + , test + "\\top" + (fromImplies fromTop_ faCeil) + [[faCeil]] + , test + "\\bottom" + (fromImplies fromBottom_ faCeil) + [[]] + ] ] where test :: @@ -94,10 +118,18 @@ test_simplify = TestTree test testName input expect = testCase testName $ do + let expect' = mkDisjunctiveNormalForm expect actual <- simplify SideCondition.top input & Test.runSimplifier Mock.env - assertEqual "" (mkDisjunctiveNormalForm expect) actual + let message = + (show . Pretty.vsep) + [ "Expected:" + , unparseDisjunctiveNormalForm expect' + , "but found:" + , unparseDisjunctiveNormalForm actual + ] + assertEqual message expect' actual fa, fb, ga, gb :: TermLike RewritingVariableName fa = Mock.f Mock.a @@ -107,6 +139,12 @@ test_simplify = mkDisjunctiveNormalForm = MultiOr.make . map MultiAnd.make + unparseDisjunctiveNormalForm = + Pretty.indent 2 + . Pretty.vsep + . map (Pretty.pretty . MultiAnd.toPredicate) + . toList + faCeil, fbCeil, gaCeil, gbCeil :: Predicate RewritingVariableName faCeil = fromCeil_ fa fbCeil = fromCeil_ fb From af66ad30227814f3212ee5f34d6f662e280fa71b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 24 May 2021 09:50:14 -0500 Subject: [PATCH 30/44] assertBidirectionalEqualityResult: Add HasCallStack --- kore/test/Test/Kore/Step/Simplification/Pattern.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/kore/test/Test/Kore/Step/Simplification/Pattern.hs b/kore/test/Test/Kore/Step/Simplification/Pattern.hs index c70f364b2a..6516a1fb37 100644 --- a/kore/test/Test/Kore/Step/Simplification/Pattern.hs +++ b/kore/test/Test/Kore/Step/Simplification/Pattern.hs @@ -423,6 +423,7 @@ simplifyAndRemoveTopExists = . Pattern.simplifyTopConfiguration assertBidirectionalEqualityResult :: + HasCallStack => TermLike RewritingVariableName -> TermLike RewritingVariableName -> OrPattern RewritingVariableName -> From a7b49215ac3864ddb8e90f52c7661380b5b267a7 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 24 May 2021 10:13:30 -0500 Subject: [PATCH 31/44] Predicate: Add missing newline --- kore/src/Kore/Step/Simplification/Predicate.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index b4c3760a85..1592648e26 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -228,4 +228,4 @@ simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} , andFirst = impliesFirst , andSecond = impliesSecond } - pure (impliesFirst' <> impliesSecond') \ No newline at end of file + pure (impliesFirst' <> impliesSecond') From 2c7bbff0b36ed58e2be4d86a4999cf0bed731697 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 24 May 2021 11:51:24 -0500 Subject: [PATCH 32/44] Simplify Iff --- docs/simplify-predicate.md | 25 +++++++++++ .../src/Kore/Step/Simplification/Predicate.hs | 26 ++++++++++- .../Kore/Step/Simplification/Integration.hs | 43 ++++++++++++------- .../Kore/Step/Simplification/Predicate.hs | 43 ++++++++++++++++++- 4 files changed, 118 insertions(+), 19 deletions(-) diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md index 6e13bbecdc..1d082f48ba 100644 --- a/docs/simplify-predicate.md +++ b/docs/simplify-predicate.md @@ -145,4 +145,29 @@ information content of the second clause of the disjunction. \implies(\bottom, _) = \top ``` +## \iff + +### Normalization + +`\iff` is desugared to `\implies`. + +``` kore +normalize(\iff(L, R)) = + \or(normalize(\and(\not(L), \not(R))), normalize(\and(L, R))) +``` + +### Simplification + +#### \top + +``` kore +\iff(\top, P) = \iff(P, \top) = P +``` + +#### \bottom + +``` kore +\iff(\bottom, P) = \iff(P, \bottom) = \not(P) +``` + [disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 1592648e26..180b4f0cce 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -37,9 +37,10 @@ import Kore.Step.Simplification.Simplify import Kore.Syntax ( And (..), Bottom (..), + Iff (..), Implies (..), Not (..), - Or, + Or (..), Top (..), ) import qualified Kore.TopBottom as TopBottom @@ -120,6 +121,7 @@ simplify sideCondition = TopF topF -> normalizeTop =<< traverse worker topF NotF notF -> simplifyNot =<< traverse worker notF ImpliesF impliesF -> simplifyImplies =<< traverse worker impliesF + IffF iffF -> simplifyIff =<< traverse worker iffF _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate @@ -229,3 +231,25 @@ simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} , andSecond = impliesSecond } pure (impliesFirst' <> impliesSecond') + +simplifyIff :: + Monad simplifier => + Iff sort DisjunctiveNormalForm -> + simplifier DisjunctiveNormalForm +simplifyIff Iff{iffFirst, iffSecond, iffSort} + | TopBottom.isTop iffFirst = pure iffSecond + | TopBottom.isBottom iffFirst = mkNotSimplified iffSecond + | TopBottom.isTop iffSecond = pure iffFirst + | TopBottom.isBottom iffSecond = mkNotSimplified iffFirst + | otherwise = do + -- \iff(A, B) = \or( \and(\not(A), \not(B)), \and(A, B) ) + orFirst <- do + andFirst <- mkNotSimplified iffFirst + andSecond <- mkNotSimplified iffSecond + mkAndSimplified andFirst andSecond + orSecond <- mkAndSimplified iffFirst iffSecond + normalizeOr Or{orSort = iffSort, orFirst, orSecond} + where + mkNotSimplified notChild = simplifyNot Not{notSort = iffSort, notChild} + mkAndSimplified andFirst andSecond = + normalizeAnd And{andSort = iffSort, andFirst, andSecond} diff --git a/kore/test/Test/Kore/Step/Simplification/Integration.hs b/kore/test/Test/Kore/Step/Simplification/Integration.hs index fcb379828f..4b6f8d4aee 100644 --- a/kore/test/Test/Kore/Step/Simplification/Integration.hs +++ b/kore/test/Test/Kore/Step/Simplification/Integration.hs @@ -22,6 +22,8 @@ import Kore.Equation ( ) import qualified Kore.Equation as Equation import qualified Kore.Internal.Condition as Condition +import Kore.Internal.From +import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.SideCondition ( SideCondition, ) @@ -55,6 +57,7 @@ import qualified Kore.Step.Simplification.Pattern as Pattern ( import Kore.Step.Simplification.Simplify import Kore.Unparser import Prelude.Kore +import qualified Pretty import Test.Kore import Test.Kore.Equation.Common ( functionAxiomUnification, @@ -545,22 +548,21 @@ test_simplificationIntegration = assertEqual "" expected actual , testCase "Or to pattern" $ do let expected = - OrPattern.fromPatterns - [ Conditional - { term = mkTop Mock.boolSort - , predicate = - makeIffPredicate - ( makeOrPredicate - ( makeAndPredicate - (makeCeilPredicate Mock.cf) - (makeCeilPredicate Mock.cg) - ) - (makeCeilPredicate Mock.cf) - ) - (makeCeilPredicate Mock.ch) - , substitution = mempty - } + ( OrPattern.fromPatterns + . map + ( Pattern.fromCondition Mock.boolSort + . Condition.fromPredicate + . MultiAnd.toPredicate + . MultiAnd.make + ) + ) + [ [fromNot cfCeil, fromNot chCeil] + , [chCeil, cgCeil, cfCeil] + , [chCeil, cfCeil] ] + cfCeil = makeCeilPredicate Mock.cf + cgCeil = makeCeilPredicate Mock.cg + chCeil = makeCeilPredicate Mock.ch actual <- evaluate Conditional @@ -578,7 +580,16 @@ test_simplificationIntegration = , predicate = makeTruePredicate , substitution = mempty } - assertEqual "" expected actual + let message = + (show . Pretty.vsep) + [ "Expected:" + , (Pretty.indent 4 . Pretty.vsep) + (map unparse . toList $ expected) + , "but found:" + , (Pretty.indent 4 . Pretty.vsep) + (map unparse . toList $ actual) + ] + assertEqual message expected actual , testCase "Sort matching" $ do let mx = Variable diff --git a/kore/test/Test/Kore/Step/Simplification/Predicate.hs b/kore/test/Test/Kore/Step/Simplification/Predicate.hs index a305b0b380..b94d0e3735 100644 --- a/kore/test/Test/Kore/Step/Simplification/Predicate.hs +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -109,6 +109,45 @@ test_simplify = (fromImplies fromBottom_ faCeil) [[]] ] + , testGroup + "\\iff" + [ test + "Normalization" + ( fromIff + (fromOr faCeil fbCeil) + (fromOr gaCeil gbCeil) + ) + [ [fromNot faCeil, fromNot fbCeil, fromNot gaCeil, fromNot gbCeil] + , [faCeil, gaCeil] + , [fbCeil, gaCeil] + , [faCeil, gbCeil] + , [fbCeil, gbCeil] + ] + , test + "\\top" + (fromIff fromTop_ faCeil) + [[faCeil]] + , test + "\\bottom" + (fromIff fromBottom_ faCeil) + [[fromNot faCeil]] + ] + , testGroup + "Other" + [ test + "\\iff(\\or(\\and(A, B), A), C)" + ( fromIff + ( fromOr + (fromAnd faCeil fbCeil) + faCeil + ) + gaCeil + ) + [ [fromNot faCeil, fromNot (fromAnd faCeil fbCeil), fromNot gaCeil] + , [faCeil, fbCeil, gaCeil] + , [faCeil, gaCeil] + ] + ] ] where test :: @@ -141,8 +180,8 @@ test_simplify = unparseDisjunctiveNormalForm = Pretty.indent 2 - . Pretty.vsep - . map (Pretty.pretty . MultiAnd.toPredicate) + . Pretty.pretty + . map MultiAnd.toPredicate . toList faCeil, fbCeil, gaCeil, gbCeil :: Predicate RewritingVariableName From 1effc463783c8ba8d8ca28c46bf9351f893f9a02 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 25 May 2021 16:15:36 -0500 Subject: [PATCH 33/44] Predicate: Move markSimplified down --- .../src/Kore/Step/Simplification/Predicate.hs | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 180b4f0cce..7d4e47d6b3 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -102,13 +102,13 @@ simplify sideCondition = else loop output mark :: DisjunctiveNormalForm -> DisjunctiveNormalForm - mark = - (MultiOr.map . MultiAnd.map) mark1 + mark = id + -- (MultiOr.map . MultiAnd.map) mark1 - mark1 :: - Predicate RewritingVariableName -> - Predicate RewritingVariableName - mark1 = Recursive.fold $ Predicate.markSimplified . Recursive.embed + -- mark1 :: + -- Predicate RewritingVariableName -> + -- Predicate RewritingVariableName + -- mark1 = Recursive.fold $ Predicate.markSimplified . Recursive.embed worker :: Predicate RewritingVariableName -> @@ -197,7 +197,9 @@ normalizeNot = normalizeNotOr & pure where fallback = - MultiAnd.singleton (fromNot $ MultiAnd.toPredicate predicates) + (fromNot $ MultiAnd.toPredicate predicates) + & Predicate.markSimplified + & MultiAnd.singleton normalized = case toList predicates of [predicate] -> @@ -250,6 +252,7 @@ simplifyIff Iff{iffFirst, iffSecond, iffSort} orSecond <- mkAndSimplified iffFirst iffSecond normalizeOr Or{orSort = iffSort, orFirst, orSecond} where - mkNotSimplified notChild = simplifyNot Not{notSort = iffSort, notChild} + mkNotSimplified notChild = + simplifyNot Not{notSort = iffSort, notChild} mkAndSimplified andFirst andSecond = normalizeAnd And{andSort = iffSort, andFirst, andSecond} From 10577b9f9a32c483e123c6496c976101997ba078 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 26 May 2021 11:56:36 -0500 Subject: [PATCH 34/44] Clarify recursive nature of normalization --- docs/simplify-predicate.md | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md index 1d082f48ba..70f79a9c76 100644 --- a/docs/simplify-predicate.md +++ b/docs/simplify-predicate.md @@ -17,7 +17,8 @@ Apply this distributive law over both arguments of `\and` until `P[n]` are all in disjunctive normal form: ``` kore -\and(\or(P[1], P[2]), P[3]) = \or(\and(P[1], P[3]), \and(P[2], P[3])) +normalize \and(\or(P[1], P[2]), P[3]) = + normalize \or(normalize \and(P[1], P[3]), normalize \and(P[2], P[3])) ``` ### Simplification @@ -98,7 +99,8 @@ This one is not as useful as the rule for `\and`: ### Normalization ``` kore -\not(\or(P[1], P[2])) = \and(\not(P[1]), \not(P[2])) +normalize \not(\or(P[1], P[2])) = + normalize \and(normalize \not(P[1]), normalize \not(P[2])) ``` ### Simplification @@ -126,7 +128,8 @@ This one is not as useful as the rule for `\and`: ### Normalization ``` kore -normalize(\implies(L, R)) = \or(normalize(\not(L)), normalize(\and(L, R))) +normalize \implies(L, R) = + normalize \or(normalize \not(L), normalize \and(L, R)) ``` Note: We carry `L` through to the right-hand side because this maximizes the @@ -152,8 +155,11 @@ information content of the second clause of the disjunction. `\iff` is desugared to `\implies`. ``` kore -normalize(\iff(L, R)) = - \or(normalize(\and(\not(L), \not(R))), normalize(\and(L, R))) +normalize \iff(L, R) = + normalize \or( + normalize \and(normalize \not(L), normalize \not(R)), + normalize \and(L, R) + ) ``` ### Simplification From daf8be27303c1b1f749d24be52e17eab6f01ca2b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 26 May 2021 11:56:57 -0500 Subject: [PATCH 35/44] Send substitutions to SMT solver Although the substitution is assumed to be applied to the predicate, it may also affect variables in the side condition. --- kore/src/Kore/Step/SMT/Evaluator.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/SMT/Evaluator.hs b/kore/src/Kore/Step/SMT/Evaluator.hs index 9d2978780d..0481ba8085 100644 --- a/kore/src/Kore/Step/SMT/Evaluator.hs +++ b/kore/src/Kore/Step/SMT/Evaluator.hs @@ -33,6 +33,7 @@ import qualified Kore.Attribute.Symbol as Attribute ( import Kore.IndexedModule.MetadataTools ( SmtMetadataTools, ) +import qualified Kore.Internal.Condition as Condition import Kore.Internal.Conditional ( Conditional, ) @@ -120,7 +121,9 @@ instance where evaluate (sideCondition, conditional) = assert (Conditional.isNormalized conditional) $ - evaluate (sideCondition, Conditional.predicate conditional) + evaluate (sideCondition, Condition.toPredicate condition) + where + condition = Conditional.withoutTerm conditional -- | Removes all branches refuted by an external SMT solver. filterBranch :: From 79b7b39a52efdb7dac0b511df81627017d5f7780 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 26 May 2021 16:43:40 -0500 Subject: [PATCH 36/44] CheckRequiresError: Include negated implication --- kore/src/Kore/Equation/Application.hs | 25 ++++++++---- kore/test/Test/Kore/Equation/Application.hs | 42 ++++++++++----------- 2 files changed, 39 insertions(+), 28 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index c5b55b521c..d59dd34b80 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -62,6 +62,9 @@ import Kore.Internal.Condition ( Condition, ) import qualified Kore.Internal.Condition as Condition +import Kore.Internal.OrCondition ( + OrCondition, + ) import qualified Kore.Internal.OrCondition as OrCondition import Kore.Internal.OrPattern ( OrPattern, @@ -382,16 +385,17 @@ checkRequires sideCondition predicate requires = where simplifyCondition = Simplifier.simplifyCondition sideCondition - assertBottom orCondition - | isBottom orCondition = done - | otherwise = requiresNotMet + assertBottom negatedImplication + | isBottom negatedImplication = done + | otherwise = requiresNotMet negatedImplication done = return () - requiresNotMet = + requiresNotMet negatedImplication = throwE CheckRequiresError { matchPredicate = predicate , equationRequires = requires , sideCondition + , negatedImplication } -- Pair a configuration with sideCondition for evaluation by the solver. @@ -530,6 +534,7 @@ data CheckRequiresError variable = CheckRequiresError { matchPredicate :: !(Predicate variable) , equationRequires :: !(Predicate variable) , sideCondition :: !(SideCondition variable) + , negatedImplication :: !(OrCondition variable) } deriving stock (Eq, Ord, Show) deriving stock (GHC.Generic) @@ -539,16 +544,22 @@ data CheckRequiresError variable = CheckRequiresError instance Pretty (CheckRequiresError RewritingVariableName) where pretty checkRequiresError = Pretty.vsep - [ "could not infer the equation requirement:" + [ "Could not infer the equation requirement:" , Pretty.indent 4 (pretty equationRequires) , "and the matching requirement:" , Pretty.indent 4 (pretty matchPredicate) , "from the side condition:" , Pretty.indent 4 (pretty sideCondition) + , "The negated implication is:" + , Pretty.indent 4 (pretty negatedImplication) ] where - CheckRequiresError{matchPredicate, equationRequires, sideCondition} = - checkRequiresError + CheckRequiresError + { matchPredicate + , equationRequires + , sideCondition + , negatedImplication + } = checkRequiresError -- * Logging diff --git a/kore/test/Test/Kore/Equation/Application.hs b/kore/test/Test/Kore/Equation/Application.hs index d928d8cc79..6c61b148e2 100644 --- a/kore/test/Test/Kore/Equation/Application.hs +++ b/kore/test/Test/Kore/Equation/Application.hs @@ -178,16 +178,11 @@ test_attemptEquation = makeEqualsPredicate (Mock.functional10 Mock.a) (Mock.functional11 Mock.a) - expect1 = - WhileCheckRequires - CheckRequiresError - { matchPredicate = makeTruePredicate - , equationRequires = requires1 - , sideCondition = SideCondition.top - } - attemptEquation SideCondition.top initial equation - >>= expectLeft - >>= assertEqual "" expect1 + checkRequiresError <- + attemptEquation SideCondition.top initial equation + >>= expectLeft + >>= expectCheckRequiresError + assertEqual "" requires1 (equationRequires checkRequiresError) let requires2 = makeEqualsPredicate (Mock.functional10 Mock.a) @@ -217,17 +212,12 @@ test_attemptEquation = >>= expectRight >>= assertEqual "" expect , testCase "rule a => b requires \\bottom" $ do - let expect = - WhileCheckRequires - CheckRequiresError - { matchPredicate = makeTruePredicate - , equationRequires = makeFalsePredicate - , sideCondition = SideCondition.top - } - initial = Mock.a - attemptEquation SideCondition.top initial equationRequiresBottom - >>= expectLeft - >>= assertEqual "" expect + let initial = Mock.a + checkRequiresError <- + attemptEquation SideCondition.top initial equationRequiresBottom + >>= expectLeft + >>= expectCheckRequiresError + assertEqual "" makeFalsePredicate (equationRequires checkRequiresError) , testCase "rule a => \\bottom does not apply to c" $ do let initial = Mock.c attemptEquation SideCondition.top initial equationRequiresBottom @@ -716,3 +706,13 @@ requiresNotMet :: TestTree requiresNotMet = withAttemptEquationResult (expectLeft >=> assertRequiresNotMet) + +expectCheckRequiresError :: + AttemptEquationError variable -> + IO (CheckRequiresError variable) +expectCheckRequiresError (WhileCheckRequires checkRequiresError) = + pure checkRequiresError +expectCheckRequiresError (WhileMatch _) = + assertFailure "Expected WhileCheckRequires, but found WhileMatch" +expectCheckRequiresError (WhileApplyMatchResult _) = + assertFailure "Expected WhileCheckRequires, but found WhileApplyMatchResult" From 2daa50f3c2887d645cd7a02507b43a60b18120cf Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 27 May 2021 16:38:08 -0500 Subject: [PATCH 37/44] test: make golden --- test/imp/max-inconsistent-prelude-spec.k.out.golden | 4 ++-- test/map-symbolic/lookup-3-spec.k.out.golden | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/imp/max-inconsistent-prelude-spec.k.out.golden b/test/imp/max-inconsistent-prelude-spec.k.out.golden index e8c9cd4e7e..f5a7dd7d89 100644 --- a/test/imp/max-inconsistent-prelude-spec.k.out.golden +++ b/test/imp/max-inconsistent-prelude-spec.k.out.golden @@ -1,6 +1,6 @@ -kore-exec: [593738] Error (ErrorException): +kore-exec: [10415077] Error (ErrorException): The definitions sent to the solver are inconsistent. CallStack (from HasCallStack): - error, called at src/Kore/Step/SMT/Lemma.hs:106:9 in kore-0.44.0.0-GXyjcogd7FRExioa8Iqini:Kore.Step.SMT.Lemma + error, called at src/Kore/Step/SMT/Lemma.hs:106:9 in kore-0.45.0.0-wxhTBooqYV3YocNuIDw2u:Kore.Step.SMT.Lemma [Error] Critical: Haskell Backend execution failed with code 1 and produced no output. diff --git a/test/map-symbolic/lookup-3-spec.k.out.golden b/test/map-symbolic/lookup-3-spec.k.out.golden index 2f7ede0b79..e4a63b5281 100644 --- a/test/map-symbolic/lookup-3-spec.k.out.golden +++ b/test/map-symbolic/lookup-3-spec.k.out.golden @@ -18,7 +18,7 @@ true #Equals Z:MyId in_keys ( MAP - ( Y:MyId |-> 2 ) ) + ( Y:MyId |-> 1 ) ) } #And { From aa36397cced299b5ae180299585347007adac9c0 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 1 Jun 2021 09:36:55 -0500 Subject: [PATCH 38/44] Predicate.simplify: Mark simplified patterns in delegates --- kore/src/Kore/Step/Simplification/Predicate.hs | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 7d4e47d6b3..3281462363 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -97,18 +97,7 @@ simplify sideCondition = loop :: DisjunctiveNormalForm -> simplifier DisjunctiveNormalForm loop input = do output <- MultiAnd.traverseOrAnd worker input - if input == output - then return (mark output) - else loop output - - mark :: DisjunctiveNormalForm -> DisjunctiveNormalForm - mark = id - -- (MultiOr.map . MultiAnd.map) mark1 - - -- mark1 :: - -- Predicate RewritingVariableName -> - -- Predicate RewritingVariableName - -- mark1 = Recursive.fold $ Predicate.markSimplified . Recursive.embed + (if input == output then pure else loop) output worker :: Predicate RewritingVariableName -> From 4866c434bd8521e4a78d7f36f7435100d43361cf Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 2 Jun 2021 13:39:02 -0500 Subject: [PATCH 39/44] Refactor and add documentation --- docs/simplify-predicate.md | 179 -------------- .../src/Kore/Step/Simplification/Predicate.hs | 219 ++++++++++++------ 2 files changed, 152 insertions(+), 246 deletions(-) delete mode 100644 docs/simplify-predicate.md diff --git a/docs/simplify-predicate.md b/docs/simplify-predicate.md deleted file mode 100644 index 70f79a9c76..0000000000 --- a/docs/simplify-predicate.md +++ /dev/null @@ -1,179 +0,0 @@ -# Simplifying predicates - -The goals of simplification are: - -1. Transform the predicate into [disjunctive normal form] (normalization). -2. Apply identities to reduce the complexity of the predicate (simplification proper). - -Simplification happens recursively, upward from the bottom. Therefore, we -describe the simplification steps based on the shape of the top-most -unsimplified clause of the predicate. - -## \and - -### Normalization - -Apply this distributive law over both arguments of `\and` until `P[n]` are all -in disjunctive normal form: - -``` kore -normalize \and(\or(P[1], P[2]), P[3]) = - normalize \or(normalize \and(P[1], P[3]), normalize \and(P[2], P[3])) -``` - -### Simplification - -#### Identity - -``` kore -\and(\top, P[1]) = P[1] -``` - -#### Annihilation - -``` kore -\and(\bottom, _) = \bottom -``` - -#### Idempotence - -``` kore -\and(P[1], P[1]) = P[1] -``` - -#### Affirmation - -Idempotence is actually a special case of _affirmation_, - -``` kore -\and(P[1], P[2]) = \and(P[1], P[2](P[1] = \top)) -``` - -## \or - -### Normalization - -Assuming the children of `\or` are in disjunctive normal form, then the clause -is already normalized. - -### Simplification - -#### Identity - -``` kore -\or(\bottom, P[1]) = P[1] -``` - -#### Annihilation - -``` kore -\or(\top, _) = \top -``` - -#### Idempotence - -``` kore -\or(P[1], P[1]) = P[1] -``` - -#### Affirmation - -This one is not as useful as the rule for `\and`: - -``` kore -\or(P[1], P[2]) = \not(\and(\not(P[1]), \not(P[2]))) - = \not(\and(\not(P[1]), \not(P[2](P[1] = \bottom)))) - = \or(P[1], P[2](P[1] = \bottom)) -``` - -## \bottom - -`\bottom` is already in disjunctive normal form. - -## \top - -`\top` is already in disjunctive normal form. - -## \not - -### Normalization - -``` kore -normalize \not(\or(P[1], P[2])) = - normalize \and(normalize \not(P[1]), normalize \not(P[2])) -``` - -### Simplification - -#### \top - -``` kore -\not(\top) = \bottom -``` - -#### \bottom - -``` kore -\not(\bottom) = \top -``` - -#### \not - -``` kore -\not(\not(P)) = P -``` - -## \implies - -### Normalization - -``` kore -normalize \implies(L, R) = - normalize \or(normalize \not(L), normalize \and(L, R)) -``` - -Note: We carry `L` through to the right-hand side because this maximizes the -information content of the second clause of the disjunction. - -### Simplification - -#### \top - -``` kore -\implies(\top, P) = P -``` - -#### \bottom -``` kore -\implies(\bottom, _) = \top -``` - -## \iff - -### Normalization - -`\iff` is desugared to `\implies`. - -``` kore -normalize \iff(L, R) = - normalize \or( - normalize \and(normalize \not(L), normalize \not(R)), - normalize \and(L, R) - ) -``` - -### Simplification - -#### \top - -``` kore -\iff(\top, P) = \iff(P, \top) = P -``` - -#### \bottom - -``` kore -\iff(\bottom, P) = \iff(P, \bottom) = \not(P) -``` - -[disjunctive normal form]: https://en.wikipedia.org/wiki/Disjunctive_normal_form \ No newline at end of file diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 3281462363..a12c99c1f0 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -80,8 +80,11 @@ simplifyPredicateTODO sideCondition predicate = do , unparse conditional ] -type DisjunctiveNormalForm = - MultiOr (MultiAnd (Predicate RewritingVariableName)) +-- | @NormalForm@ is the normal form result of simplifying 'Predicate'. +-- The primary purpose of this form is to transmit to the external solver. +-- Note that this is almost, but not quite, disjunctive normal form; see +-- 'simplifyNot' for the most notable exception. +type NormalForm = MultiOr (MultiAnd (Predicate RewritingVariableName)) simplify :: forall simplifier. @@ -90,18 +93,18 @@ simplify :: ) => SideCondition RewritingVariableName -> Predicate RewritingVariableName -> - simplifier DisjunctiveNormalForm + simplifier NormalForm simplify sideCondition = loop . MultiOr.singleton . MultiAnd.singleton where - loop :: DisjunctiveNormalForm -> simplifier DisjunctiveNormalForm + loop :: NormalForm -> simplifier NormalForm loop input = do output <- MultiAnd.traverseOrAnd worker input (if input == output then pure else loop) output worker :: Predicate RewritingVariableName -> - simplifier DisjunctiveNormalForm + simplifier NormalForm worker predicate = case predicateF of AndF andF -> normalizeAnd =<< traverse worker andF @@ -115,95 +118,173 @@ simplify sideCondition = where _ :< predicateF = Recursive.project predicate +-- | See 'normalizeMultiAnd'. normalizeAnd :: Applicative simplifier => - And sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm -normalizeAnd andOr = + And sort NormalForm -> + simplifier NormalForm +normalizeAnd = normalizeMultiAnd . foldMap MultiAnd.singleton + +-- | @normalizeAnd@ obeys these laws: +-- +-- Distribution: +-- +-- @ +-- \\and(\\or(P[1], P[2]), P[3]) = \\or(\\and(P[1], P[3]), \\and(P[2], P[3])) +-- @ +-- +-- Identity: +-- +-- @ +-- \\and(\\top, P[1]) = P[1] +-- @ +-- +-- Annihilation: +-- +-- @ +-- \\and(\\bottom, _) = \\bottom +-- @ +-- +-- Idempotence: +-- +-- @ +-- \\and(P[1], P[1]) = P[1] +-- @ +normalizeMultiAnd :: + Applicative simplifier => + MultiAnd NormalForm -> + simplifier NormalForm +normalizeMultiAnd andOr = pure . MultiOr.observeAll $ do -- andOr: \and(\or(_, _), \or(_, _)) - andAnd <- traverse Logic.scatter andOr + andAnd <- MultiAnd.traverse Logic.scatter andOr -- andAnd: \and(\and(_, _), \and(_, _)) - let multiAnd = fold andAnd - pure multiAnd + pure (fold andAnd) +-- | If the arguments of 'Or' are already in 'NormalForm', then normalization is +-- trivial. +-- +-- @normalizeOr@ obeys these laws: +-- +-- Identity: +-- +-- @ +-- \\or(\\bottom, P[1]) = P[1] +-- @ +-- +-- Annihilation: +-- +-- @ +-- \\or(\\top, _) = \\top +-- @ +-- +-- Idempotence: +-- +-- @ +-- \\or(P[1], P[1]) = P[1] +-- @ normalizeOr :: Applicative simplifier => - Or sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm + Or sort NormalForm -> + simplifier NormalForm normalizeOr = pure . fold +-- | 'Bottom' is regarded as trivially-normalizable. normalizeBottom :: Applicative simplifier => - Bottom sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm + Bottom sort NormalForm -> + simplifier NormalForm normalizeBottom _ = pure MultiOr.bottom +-- | 'Top' is regarded as trivially-normalizable. normalizeTop :: Applicative simplifier => - Top sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm + Top sort NormalForm -> + simplifier NormalForm normalizeTop _ = pure (MultiOr.singleton MultiAnd.top) +-- | @simplifyNot@ obeys these laws: +-- +-- 'Top': +-- +-- @ +-- \\not(\\top) = \\bottom +-- @ +-- +-- 'Bottom': +-- +-- @ +-- \\not(\\bottom) = \\top +-- @ +-- +-- 'Not': +-- +-- @ +-- \\not(\\not(P)) = P +-- @ +-- +-- 'Or': +-- +-- @ +-- \\not(\\or(P[1], P[2])) = \\and(\\not(P[1]), \\not(P[2])) +-- @ +-- +-- @simplifyNot@ does not expand @\not(\and(_, _))@ into @\or(_, _)@, because +-- the purpose of simplification is mostly to prepare 'Predicate' for the +-- external solver or for the user, and the un-expanded form is more compact. simplifyNot :: + forall simplifier sort. Monad simplifier => - Not sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm -simplifyNot notF@Not{notChild, notSort} - | TopBottom.isTop notChild = normalizeBottom Bottom{bottomSort = notSort} - | TopBottom.isBottom notChild = normalizeTop Top{topSort = notSort} - | otherwise = normalizeNot notF + Not sort NormalForm -> + simplifier NormalForm +simplifyNot Not{notChild = multiOr, notSort} = do + disjunctiveNormalForms <- Logic.observeAllT $ do + multiAnd <- Logic.scatter multiOr + normalizeNotAnd Not{notSort, notChild = multiAnd} & lift + normalizeMultiAnd (MultiAnd.make disjunctiveNormalForms) -normalizeMultiAnd :: - Applicative simplifier => - MultiAnd DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm -normalizeMultiAnd andOr = - pure . MultiOr.observeAll $ do - -- andOr: \and(\or(_, _), \or(_, _)) - andAnd <- MultiAnd.traverse Logic.scatter andOr - -- andAnd: \and(\and(_, _), \and(_, _)) - pure (fold andAnd) - -normalizeNot :: +normalizeNotAnd :: forall simplifier sort. Monad simplifier => - Not sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm -normalizeNot = normalizeNotOr + Not sort (MultiAnd (Predicate RewritingVariableName)) -> + simplifier NormalForm +normalizeNotAnd Not{notSort, notChild = predicates} = + case toList predicates of + [] -> + -- \not(\top) + bottom + [predicate] -> + case predicateF of + NotF Not{notChild = result} -> + MultiAnd.fromPredicate result + & MultiOr.singleton + & pure + _ -> fallback + where + _ :< predicateF = Recursive.project predicate + _ -> fallback where - normalizeNotOr Not{notChild = multiOr, notSort} = do - disjunctiveNormalForms <- Logic.observeAllT $ do - multiAnd <- Logic.scatter multiOr - normalizeNotAnd Not{notSort, notChild = multiAnd} & lift - normalizeMultiAnd (MultiAnd.make disjunctiveNormalForms) - normalizeNotAnd :: - Not sort (MultiAnd (Predicate RewritingVariableName)) -> - simplifier DisjunctiveNormalForm - normalizeNotAnd Not{notChild = predicates} = - normalized + fallback = + -- \not(\and(_, ...)) + MultiAnd.toPredicate predicates + & fromNot + & Predicate.markSimplified + & MultiAnd.singleton & MultiOr.singleton & pure - where - fallback = - (fromNot $ MultiAnd.toPredicate predicates) - & Predicate.markSimplified - & MultiAnd.singleton - normalized = - case toList predicates of - [predicate] -> - case predicateF of - NotF Not{notChild = result} -> - MultiAnd.fromPredicate result - _ -> fallback - where - _ :< predicateF = Recursive.project predicate - _ -> fallback + bottom = normalizeBottom Bottom{bottomSort = notSort} +-- | +-- @ +-- \\implies(L, R) = \\or(\\not(L), \\and(L, R)) +-- @ +-- +-- Note: @L@ is carried through to the right-hand side of 'Implies' to maximize +-- the information content of that branch. simplifyImplies :: Monad simplifier => - Implies sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm + Implies sort NormalForm -> + simplifier NormalForm simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} | TopBottom.isTop impliesFirst = pure impliesSecond | TopBottom.isBottom impliesFirst = normalizeTop Top{topSort = impliesSort} @@ -223,10 +304,14 @@ simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} } pure (impliesFirst' <> impliesSecond') +-- | +-- @ +-- \\iff(P[1], P[2]) = \\and(\\implies(P[1], P[2]), \\implies(P[2], P[1])) +-- @ simplifyIff :: Monad simplifier => - Iff sort DisjunctiveNormalForm -> - simplifier DisjunctiveNormalForm + Iff sort NormalForm -> + simplifier NormalForm simplifyIff Iff{iffFirst, iffSecond, iffSort} | TopBottom.isTop iffFirst = pure iffSecond | TopBottom.isBottom iffFirst = mkNotSimplified iffSecond From 5f8c1b604796848481d3e1d3cd2f800316556484 Mon Sep 17 00:00:00 2001 From: github-actions Date: Tue, 8 Jun 2021 22:03:37 +0000 Subject: [PATCH 40/44] Format with fourmolu --- .../src/Kore/Step/Simplification/Predicate.hs | 188 +++++++++--------- 1 file changed, 97 insertions(+), 91 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index a12c99c1f0..587ef5a754 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -80,10 +80,11 @@ simplifyPredicateTODO sideCondition predicate = do , unparse conditional ] --- | @NormalForm@ is the normal form result of simplifying 'Predicate'. --- The primary purpose of this form is to transmit to the external solver. --- Note that this is almost, but not quite, disjunctive normal form; see --- 'simplifyNot' for the most notable exception. +{- | @NormalForm@ is the normal form result of simplifying 'Predicate'. + The primary purpose of this form is to transmit to the external solver. + Note that this is almost, but not quite, disjunctive normal form; see + 'simplifyNot' for the most notable exception. +-} type NormalForm = MultiOr (MultiAnd (Predicate RewritingVariableName)) simplify :: @@ -125,31 +126,32 @@ normalizeAnd :: simplifier NormalForm normalizeAnd = normalizeMultiAnd . foldMap MultiAnd.singleton --- | @normalizeAnd@ obeys these laws: --- --- Distribution: --- --- @ --- \\and(\\or(P[1], P[2]), P[3]) = \\or(\\and(P[1], P[3]), \\and(P[2], P[3])) --- @ --- --- Identity: --- --- @ --- \\and(\\top, P[1]) = P[1] --- @ --- --- Annihilation: --- --- @ --- \\and(\\bottom, _) = \\bottom --- @ --- --- Idempotence: --- --- @ --- \\and(P[1], P[1]) = P[1] --- @ +{- | @normalizeAnd@ obeys these laws: + + Distribution: + + @ + \\and(\\or(P[1], P[2]), P[3]) = \\or(\\and(P[1], P[3]), \\and(P[2], P[3])) + @ + + Identity: + + @ + \\and(\\top, P[1]) = P[1] + @ + + Annihilation: + + @ + \\and(\\bottom, _) = \\bottom + @ + + Idempotence: + + @ + \\and(P[1], P[1]) = P[1] + @ +-} normalizeMultiAnd :: Applicative simplifier => MultiAnd NormalForm -> @@ -161,28 +163,29 @@ normalizeMultiAnd andOr = -- andAnd: \and(\and(_, _), \and(_, _)) pure (fold andAnd) --- | If the arguments of 'Or' are already in 'NormalForm', then normalization is --- trivial. --- --- @normalizeOr@ obeys these laws: --- --- Identity: --- --- @ --- \\or(\\bottom, P[1]) = P[1] --- @ --- --- Annihilation: --- --- @ --- \\or(\\top, _) = \\top --- @ --- --- Idempotence: --- --- @ --- \\or(P[1], P[1]) = P[1] --- @ +{- | If the arguments of 'Or' are already in 'NormalForm', then normalization is + trivial. + + @normalizeOr@ obeys these laws: + + Identity: + + @ + \\or(\\bottom, P[1]) = P[1] + @ + + Annihilation: + + @ + \\or(\\top, _) = \\top + @ + + Idempotence: + + @ + \\or(P[1], P[1]) = P[1] + @ +-} normalizeOr :: Applicative simplifier => Or sort NormalForm -> @@ -203,35 +206,36 @@ normalizeTop :: simplifier NormalForm normalizeTop _ = pure (MultiOr.singleton MultiAnd.top) --- | @simplifyNot@ obeys these laws: --- --- 'Top': --- --- @ --- \\not(\\top) = \\bottom --- @ --- --- 'Bottom': --- --- @ --- \\not(\\bottom) = \\top --- @ --- --- 'Not': --- --- @ --- \\not(\\not(P)) = P --- @ --- --- 'Or': --- --- @ --- \\not(\\or(P[1], P[2])) = \\and(\\not(P[1]), \\not(P[2])) --- @ --- --- @simplifyNot@ does not expand @\not(\and(_, _))@ into @\or(_, _)@, because --- the purpose of simplification is mostly to prepare 'Predicate' for the --- external solver or for the user, and the un-expanded form is more compact. +{- | @simplifyNot@ obeys these laws: + + 'Top': + + @ + \\not(\\top) = \\bottom + @ + + 'Bottom': + + @ + \\not(\\bottom) = \\top + @ + + 'Not': + + @ + \\not(\\not(P)) = P + @ + + 'Or': + + @ + \\not(\\or(P[1], P[2])) = \\and(\\not(P[1]), \\not(P[2])) + @ + + @simplifyNot@ does not expand @\not(\and(_, _))@ into @\or(_, _)@, because + the purpose of simplification is mostly to prepare 'Predicate' for the + external solver or for the user, and the un-expanded form is more compact. +-} simplifyNot :: forall simplifier sort. Monad simplifier => @@ -274,13 +278,14 @@ normalizeNotAnd Not{notSort, notChild = predicates} = & pure bottom = normalizeBottom Bottom{bottomSort = notSort} --- | --- @ --- \\implies(L, R) = \\or(\\not(L), \\and(L, R)) --- @ --- --- Note: @L@ is carried through to the right-hand side of 'Implies' to maximize --- the information content of that branch. +{- | + @ + \\implies(L, R) = \\or(\\not(L), \\and(L, R)) + @ + + Note: @L@ is carried through to the right-hand side of 'Implies' to maximize + the information content of that branch. +-} simplifyImplies :: Monad simplifier => Implies sort NormalForm -> @@ -304,10 +309,11 @@ simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} } pure (impliesFirst' <> impliesSecond') --- | --- @ --- \\iff(P[1], P[2]) = \\and(\\implies(P[1], P[2]), \\implies(P[2], P[1])) --- @ +{- | + @ + \\iff(P[1], P[2]) = \\and(\\implies(P[1], P[2]), \\implies(P[2], P[1])) + @ +-} simplifyIff :: Monad simplifier => Iff sort NormalForm -> From 6a6323e28580a41a907e7ce66f0e19c7ab4a47fc Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 14 Jun 2021 16:47:07 -0500 Subject: [PATCH 41/44] Clean up simplifyImplies --- .../src/Kore/Step/Simplification/Predicate.hs | 27 +++++++------------ 1 file changed, 9 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 587ef5a754..68a1c8ec48 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -290,24 +290,15 @@ simplifyImplies :: Monad simplifier => Implies sort NormalForm -> simplifier NormalForm -simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} - | TopBottom.isTop impliesFirst = pure impliesSecond - | TopBottom.isBottom impliesFirst = normalizeTop Top{topSort = impliesSort} - | otherwise = do - impliesFirst' <- - simplifyNot - Not - { notSort = impliesSort - , notChild = impliesFirst - } - impliesSecond' <- - normalizeAnd - And - { andSort = impliesSort - , andFirst = impliesFirst - , andSecond = impliesSecond - } - pure (impliesFirst' <> impliesSecond') +simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} = do + impliesFirst' <- mkNotSimplified impliesFirst + impliesSecond' <- mkAndSimplified impliesFirst impliesSecond + pure (impliesFirst' <> impliesSecond') + where + mkNotSimplified notChild = + simplifyNot Not{notSort = impliesSort, notChild} + mkAndSimplified andFirst andSecond = + normalizeAnd And{andSort = impliesSort, andFirst, andSecond} {- | @ From 0728d696f25af628455538c932f3df316a14bb89 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 14 Jun 2021 16:54:29 -0500 Subject: [PATCH 42/44] Remove special cases of simplifyIff --- .../src/Kore/Step/Simplification/Predicate.hs | 21 +++++++------------ 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 68a1c8ec48..76bea4012e 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -309,19 +309,14 @@ simplifyIff :: Monad simplifier => Iff sort NormalForm -> simplifier NormalForm -simplifyIff Iff{iffFirst, iffSecond, iffSort} - | TopBottom.isTop iffFirst = pure iffSecond - | TopBottom.isBottom iffFirst = mkNotSimplified iffSecond - | TopBottom.isTop iffSecond = pure iffFirst - | TopBottom.isBottom iffSecond = mkNotSimplified iffFirst - | otherwise = do - -- \iff(A, B) = \or( \and(\not(A), \not(B)), \and(A, B) ) - orFirst <- do - andFirst <- mkNotSimplified iffFirst - andSecond <- mkNotSimplified iffSecond - mkAndSimplified andFirst andSecond - orSecond <- mkAndSimplified iffFirst iffSecond - normalizeOr Or{orSort = iffSort, orFirst, orSecond} +simplifyIff Iff{iffFirst, iffSecond, iffSort} = do + -- \iff(A, B) = \or( \and(\not(A), \not(B)), \and(A, B) ) + orFirst <- do + andFirst <- mkNotSimplified iffFirst + andSecond <- mkNotSimplified iffSecond + mkAndSimplified andFirst andSecond + orSecond <- mkAndSimplified iffFirst iffSecond + normalizeOr Or{orSort = iffSort, orFirst, orSecond} where mkNotSimplified notChild = simplifyNot Not{notSort = iffSort, notChild} From c2bfbd42e5e46783fc490167e80fa0d3926ed095 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 14 Jun 2021 17:03:12 -0500 Subject: [PATCH 43/44] Clean up simplifyImplies and simplifyIff --- kore/src/Kore/Step/Simplification/Predicate.hs | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs index 76bea4012e..be9fdb777e 100644 --- a/kore/src/Kore/Step/Simplification/Predicate.hs +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -191,6 +191,7 @@ normalizeOr :: Or sort NormalForm -> simplifier NormalForm normalizeOr = pure . fold +{-# INLINE normalizeOr #-} -- | 'Bottom' is regarded as trivially-normalizable. normalizeBottom :: @@ -198,6 +199,7 @@ normalizeBottom :: Bottom sort NormalForm -> simplifier NormalForm normalizeBottom _ = pure MultiOr.bottom +{-# INLINE normalizeBottom #-} -- | 'Top' is regarded as trivially-normalizable. normalizeTop :: @@ -205,6 +207,7 @@ normalizeTop :: Top sort NormalForm -> simplifier NormalForm normalizeTop _ = pure (MultiOr.singleton MultiAnd.top) +{-# INLINE normalizeTop #-} {- | @simplifyNot@ obeys these laws: @@ -291,18 +294,20 @@ simplifyImplies :: Implies sort NormalForm -> simplifier NormalForm simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} = do - impliesFirst' <- mkNotSimplified impliesFirst - impliesSecond' <- mkAndSimplified impliesFirst impliesSecond - pure (impliesFirst' <> impliesSecond') + negative <- mkNotSimplified impliesFirst + positive <- mkAndSimplified impliesFirst impliesSecond + mkOrSimplified negative positive where mkNotSimplified notChild = simplifyNot Not{notSort = impliesSort, notChild} mkAndSimplified andFirst andSecond = normalizeAnd And{andSort = impliesSort, andFirst, andSecond} + mkOrSimplified orFirst orSecond = + normalizeOr Or{orSort = impliesSort, orFirst, orSecond} {- | @ - \\iff(P[1], P[2]) = \\and(\\implies(P[1], P[2]), \\implies(P[2], P[1])) + \\iff(P[1], P[2]) = \\or(\\and(\\not(P[1]), \\not(P[2])), \\and(P[1], P[2])) @ -} simplifyIff :: @@ -310,15 +315,16 @@ simplifyIff :: Iff sort NormalForm -> simplifier NormalForm simplifyIff Iff{iffFirst, iffSecond, iffSort} = do - -- \iff(A, B) = \or( \and(\not(A), \not(B)), \and(A, B) ) orFirst <- do andFirst <- mkNotSimplified iffFirst andSecond <- mkNotSimplified iffSecond mkAndSimplified andFirst andSecond orSecond <- mkAndSimplified iffFirst iffSecond - normalizeOr Or{orSort = iffSort, orFirst, orSecond} + mkOrSimplified orFirst orSecond where mkNotSimplified notChild = simplifyNot Not{notSort = iffSort, notChild} mkAndSimplified andFirst andSecond = normalizeAnd And{andSort = iffSort, andFirst, andSecond} + mkOrSimplified orFirst orSecond = + normalizeOr Or{orSort = iffSort, orFirst, orSecond} From a7f0699ee0f4ff495db2b6938ae8d90b15c635c6 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 15 Jun 2021 20:43:20 -0500 Subject: [PATCH 44/44] simplifyPredicates: Revert toward master --- .../src/Kore/Step/Simplification/Condition.hs | 69 +++++++++++++------ 1 file changed, 49 insertions(+), 20 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index d09c1a2524..ed7ec60e32 100644 --- a/kore/src/Kore/Step/Simplification/Condition.hs +++ b/kore/src/Kore/Step/Simplification/Condition.hs @@ -129,37 +129,66 @@ others are true. This procedure is applied until the conjunction stabilizes. -} simplifyPredicates :: - forall simplifier. MonadSimplify simplifier => SideCondition RewritingVariableName -> MultiAnd (Predicate RewritingVariableName) -> LogicT simplifier (Condition RewritingVariableName) -simplifyPredicates initialSideCondition predicates = do - let predicatesList = toList predicates - unsimplifieds = scanr ((<>) . MultiAnd.singleton) MultiAnd.top predicatesList - simplifieds <- - traverse worker (zip predicatesList unsimplifieds) - & flip State.evalStateT initialSideCondition - markConjunctionSimplified (foldMap mkCondition $ mconcat simplifieds) +simplifyPredicates sideCondition original = do + let predicates = + SideCondition.simplifyConjunctionByAssumption original + & fst . extract + simplified <- + simplifyPredicatesWithAssumptions + sideCondition + (toList predicates) + let simplifiedPredicates = + from @(Condition _) @(MultiAnd (Predicate _)) simplified + if original == simplifiedPredicates + then return (Condition.markSimplified simplified) + else simplifyPredicates sideCondition simplifiedPredicates + +{- | Simplify a conjunction of predicates by simplifying each one +under the assumption that the others are true. +-} +simplifyPredicatesWithAssumptions :: + forall simplifier. + MonadSimplify simplifier => + SideCondition RewritingVariableName -> + [Predicate RewritingVariableName] -> + LogicT + simplifier + (Condition RewritingVariableName) +simplifyPredicatesWithAssumptions _ [] = return Condition.top +simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do + let predicatesWithUnsimplified = + zip predicates $ + scanr ((<>) . MultiAnd.singleton) MultiAnd.top rest + State.execStateT + ( traverse_ + simplifyWithAssumptions + predicatesWithUnsimplified + ) + MultiAnd.top + & fmap (foldMap mkCondition) where - worker :: + simplifyWithAssumptions :: ( Predicate RewritingVariableName , MultiAnd (Predicate RewritingVariableName) ) -> StateT - (SideCondition RewritingVariableName) - (LogicT simplifier) (MultiAnd (Predicate RewritingVariableName)) - worker (predicate, unsimplified) = do - sideCondition <- SideCondition.addAssumptions unsimplified <$> State.get - results <- - Predicate.simplify sideCondition predicate >>= Logic.scatter + (LogicT simplifier) + () + simplifyWithAssumptions (predicate, unsimplifiedSideCond) = do + simplifiedSideCond <- State.get + let otherSideConds = + SideCondition.addAssumptions + (simplifiedSideCond <> unsimplifiedSideCond) + sideCondition + result <- + Predicate.simplify otherSideConds predicate >>= Logic.scatter & lift - State.modify (SideCondition.addAssumptions results) - return results - - markConjunctionSimplified = - return . Lens.over (field @"predicate") Predicate.markSimplified + State.put (simplifiedSideCond <> result) mkCondition :: InternalVariable variable =>