diff --git a/kore/kore.cabal b/kore/kore.cabal index 2690a121ef..c223a14f2d 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 @@ -751,6 +752,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/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index a43ed52fc0..009b9c1d37 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/src/Kore/Internal/MultiAnd.hs b/kore/src/Kore/Internal/MultiAnd.hs index b801e33e4a..7b780902ec 100644 --- a/kore/src/Kore/Internal/MultiAnd.hs +++ b/kore/src/Kore/Internal/MultiAnd.hs @@ -20,6 +20,9 @@ module Kore.Internal.MultiAnd ( singleton, map, traverse, + distributeAnd, + traverseOr, + traverseOrAnd, ) where import qualified Data.Functor.Foldable as Recursive @@ -35,6 +38,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 +56,7 @@ import Kore.Internal.Variable import Kore.TopBottom ( TopBottom (..), ) +import qualified Logic import Prelude.Kore hiding ( map, traverse, @@ -251,3 +259,32 @@ 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 #-} + +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 #-} diff --git a/kore/src/Kore/Internal/MultiOr.hs b/kore/src/Kore/Internal/MultiOr.hs index c2ea6fcc03..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 => @@ -343,3 +328,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 #-} 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/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 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 :: 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' = diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index 61012e17dc..ed7ec60e32 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, ) @@ -40,19 +37,21 @@ 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, ) +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 :: @@ -87,8 +86,9 @@ simplify SubstitutionSimplifier{simplifySubstitution} sideCondition = predicate' = Predicate.substitute substitution' predicate simplified <- - simplifyPredicate sideCondition predicate' - >>= simplifyPredicates sideCondition . from @_ @(MultiAnd _) + Predicate.simplify sideCondition predicate' + >>= Logic.scatter + >>= simplifyPredicates sideCondition TopBottom.guardAgainstBottom simplified let merged = simplified <> Condition.fromSubstitution substitution normalized <- normalize merged @@ -118,8 +118,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' @@ -168,58 +168,37 @@ simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do simplifyWithAssumptions predicatesWithUnsimplified ) - Condition.top + MultiAnd.top + & fmap (foldMap mkCondition) 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 + result <- + Predicate.simplify otherSideConds predicate >>= Logic.scatter + & lift State.put (simplifiedSideCond <> result) -{- | Simplify the 'Predicate' once. - -@simplifyPredicate@ does not attempt to apply the resulting substitution and -re-simplify the result. - -See also: 'simplify' --} -simplifyPredicate :: - ( HasCallStack - , MonadSimplify simplifier - ) => - SideCondition RewritingVariableName -> - Predicate RewritingVariableName -> - LogicT simplifier (Condition RewritingVariableName) -simplifyPredicate sideCondition predicate = do - patternOr <- - lift $ - simplifyTermLike sideCondition $ - 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) - where - eraseTerm conditional - | TopBottom.isTop (Pattern.term conditional) = - Conditional.withoutTerm conditional - | otherwise = - (error . show . Pretty.vsep) - [ "Expecting a \\top term, but found:" - , unparse conditional - ] +mkCondition :: + InternalVariable variable => + Predicate variable -> + Condition variable +mkCondition predicate = + maybe + (from @(Predicate _) predicate) + (from @(Assignment _)) + (Substitution.retractAssignment predicate) simplifyConjunctions :: Predicate RewritingVariableName -> 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/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs new file mode 100644 index 0000000000..be9fdb777e --- /dev/null +++ b/kore/src/Kore/Step/Simplification/Predicate.hs @@ -0,0 +1,330 @@ +{- | +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.From +import Kore.Internal.MultiAnd ( + MultiAnd, + ) +import qualified Kore.Internal.MultiAnd as 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, + ) +import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.Predicate ( + Predicate, + PredicateF (..), + ) +import qualified Kore.Internal.Predicate as Predicate +import Kore.Internal.SideCondition ( + SideCondition, + ) +import Kore.Rewriting.RewritingVariable ( + RewritingVariableName, + ) +import Kore.Step.Simplification.Simplify +import Kore.Syntax ( + And (..), + Bottom (..), + Iff (..), + Implies (..), + Not (..), + Or (..), + Top (..), + ) +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 + ] + +{- | @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. + ( HasCallStack + , MonadSimplify simplifier + ) => + SideCondition RewritingVariableName -> + Predicate RewritingVariableName -> + simplifier NormalForm +simplify sideCondition = + loop . MultiOr.singleton . MultiAnd.singleton + where + loop :: NormalForm -> simplifier NormalForm + loop input = do + output <- MultiAnd.traverseOrAnd worker input + (if input == output then pure else loop) output + + worker :: + Predicate RewritingVariableName -> + simplifier NormalForm + worker predicate = + case predicateF of + 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 + ImpliesF impliesF -> simplifyImplies =<< traverse worker impliesF + IffF iffF -> simplifyIff =<< traverse worker iffF + _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT + where + _ :< predicateF = Recursive.project predicate + +-- | See 'normalizeMultiAnd'. +normalizeAnd :: + Applicative simplifier => + 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 <- MultiAnd.traverse Logic.scatter 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] + @ +-} +normalizeOr :: + Applicative simplifier => + Or sort NormalForm -> + simplifier NormalForm +normalizeOr = pure . fold +{-# INLINE normalizeOr #-} + +-- | 'Bottom' is regarded as trivially-normalizable. +normalizeBottom :: + Applicative simplifier => + Bottom sort NormalForm -> + simplifier NormalForm +normalizeBottom _ = pure MultiOr.bottom +{-# INLINE normalizeBottom #-} + +-- | 'Top' is regarded as trivially-normalizable. +normalizeTop :: + Applicative simplifier => + Top sort NormalForm -> + simplifier NormalForm +normalizeTop _ = pure (MultiOr.singleton MultiAnd.top) +{-# INLINE normalizeTop #-} + +{- | @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 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) + +normalizeNotAnd :: + forall simplifier sort. + Monad simplifier => + 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 + fallback = + -- \not(\and(_, ...)) + MultiAnd.toPredicate predicates + & fromNot + & Predicate.markSimplified + & MultiAnd.singleton + & MultiOr.singleton + & 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. +-} +simplifyImplies :: + Monad simplifier => + Implies sort NormalForm -> + simplifier NormalForm +simplifyImplies Implies{impliesFirst, impliesSecond, impliesSort} = do + 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]) = \\or(\\and(\\not(P[1]), \\not(P[2])), \\and(P[1], P[2])) + @ +-} +simplifyIff :: + Monad simplifier => + Iff sort NormalForm -> + simplifier NormalForm +simplifyIff Iff{iffFirst, iffSecond, iffSort} = do + orFirst <- do + andFirst <- mkNotSimplified iffFirst + andSecond <- mkNotSimplified iffSecond + mkAndSimplified andFirst andSecond + orSecond <- mkAndSimplified iffFirst iffSecond + 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} 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" 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" ] 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 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 () 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 = diff --git a/kore/test/Test/Kore/Step/Simplification/Integration.hs b/kore/test/Test/Kore/Step/Simplification/Integration.hs index 7b96c55538..4b6f8d4aee 100644 --- a/kore/test/Test/Kore/Step/Simplification/Integration.hs +++ b/kore/test/Test/Kore/Step/Simplification/Integration.hs @@ -21,6 +21,9 @@ import Kore.Equation ( mkEquation, ) 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, ) @@ -32,6 +35,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,7 +55,9 @@ import qualified Kore.Step.Simplification.Pattern as Pattern ( makeEvaluate, ) import Kore.Step.Simplification.Simplify +import Kore.Unparser import Prelude.Kore +import qualified Pretty import Test.Kore import Test.Kore.Equation.Common ( functionAxiomUnification, @@ -542,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 @@ -575,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 @@ -782,9 +796,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 diff --git a/kore/test/Test/Kore/Step/Simplification/Pattern.hs b/kore/test/Test/Kore/Step/Simplification/Pattern.hs index 3973e44ce0..6516a1fb37 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 @@ -396,6 +423,7 @@ simplifyAndRemoveTopExists = . Pattern.simplifyTopConfiguration assertBidirectionalEqualityResult :: + HasCallStack => TermLike RewritingVariableName -> TermLike RewritingVariableName -> OrPattern RewritingVariableName -> 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..b94d0e3735 --- /dev/null +++ b/kore/test/Test/Kore/Step/Simplification/Predicate.hs @@ -0,0 +1,191 @@ +module Test.Kore.Step.Simplification.Predicate ( + test_simplify, +) where + +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) +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 +import Test.Tasty.HUnit + +test_simplify :: [TestTree] +test_simplify = + [ 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) + [[]] + ] + , testGroup + "\\bottom" + [ test + "Normalization" + fromBottom_ + [] + ] + , testGroup + "\\top" + [ test + "Normalization" + 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]] + ] + , 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) + [[]] + ] + , 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 :: + TestName -> + Predicate RewritingVariableName -> + [[Predicate RewritingVariableName]] -> + TestTree + test testName input expect = + testCase testName $ do + let expect' = mkDisjunctiveNormalForm expect + actual <- + simplify SideCondition.top input + & Test.runSimplifier Mock.env + 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 + fb = Mock.f Mock.b + ga = Mock.g Mock.a + gb = Mock.g Mock.b + + mkDisjunctiveNormalForm = MultiOr.make . map MultiAnd.make + + unparseDisjunctiveNormalForm = + Pretty.indent 2 + . Pretty.pretty + . map MultiAnd.toPredicate + . toList + + faCeil, fbCeil, gaCeil, gbCeil :: Predicate RewritingVariableName + faCeil = fromCeil_ fa + fbCeil = fromCeil_ fb + gaCeil = fromCeil_ ga + gbCeil = fromCeil_ gb 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 => 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" diff --git a/test/imp/max-inconsistent-prelude-spec.k.out.golden b/test/imp/max-inconsistent-prelude-spec.k.out.golden index 8e0bf9d69f..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: [233424] 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: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.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 { 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") + ) ) ) )