diff --git a/kore/CHANGELOG.md b/kore/CHANGELOG.md index 5c9e808675..45368caa7e 100644 --- a/kore/CHANGELOG.md +++ b/kore/CHANGELOG.md @@ -8,6 +8,8 @@ All notable changes to this project will be documented in this file. ### Changed +- Execution does not branch when evaluating the hooked `KEQUAL.eq` function. + ### Deprecated ### Removed diff --git a/kore/src/Kore/Builtin/Bool.hs b/kore/src/Kore/Builtin/Bool.hs index 53d23341ea..ff95bece10 100644 --- a/kore/src/Kore/Builtin/Bool.hs +++ b/kore/src/Kore/Builtin/Bool.hs @@ -14,6 +14,8 @@ module Kore.Builtin.Bool , extractBoolDomainValue , parse , termAndEquals + , termNotBool + , matchBool -- * Keys , orKey , andKey @@ -208,7 +210,26 @@ termAndEquals unifyChildren a b = unification2 <- unifyChildren' termLike1 operand2 let conditions = unification1 <> unification2 pure (Pattern.withCondition termLike1 conditions) + worker _ _ = empty +termNotBool + :: forall variable unifier + . InternalVariable variable + => MonadUnify unifier + => TermSimplifier variable unifier + -> TermLike variable + -> TermLike variable + -> MaybeT unifier (Pattern variable) +termNotBool unifyChildren a b = + worker a b <|> worker b a + where + worker termLike1 boolTerm + | Just BoolNot { operand } <- matchBoolNot termLike1 + , isFunctionPattern termLike1 + , Just value <- matchBool boolTerm + = lift $ do + let notValue = asInternal (termLikeSort boolTerm) (not value) + unifyChildren notValue operand worker _ _ = empty {- | Match a @BOOL.Bool@ builtin value. @@ -234,3 +255,20 @@ matchBoolAnd (App_ symbol [operand1, operand2]) = do Monad.guard (hook2 == andKey) return BoolAnd { symbol, operand1, operand2 } matchBoolAnd _ = Nothing + +{- | The @BOOL.not@ hooked symbol applied to a @term@-type argument. + -} +data BoolNot term = + BoolNot + { symbol :: !Symbol + , operand :: !term + } + +{- | Match the @BOOL.not@ hooked symbol. + -} +matchBoolNot :: TermLike variable -> Maybe (BoolNot (TermLike variable)) +matchBoolNot (App_ symbol [operand]) = do + hook2 <- (getHook . symbolHook) symbol + Monad.guard (hook2 == notKey) + return BoolNot { symbol, operand } +matchBoolNot _ = Nothing diff --git a/kore/src/Kore/Builtin/KEqual.hs b/kore/src/Kore/Builtin/KEqual.hs index 36f32440b4..fa3f4ad026 100644 --- a/kore/src/Kore/Builtin/KEqual.hs +++ b/kore/src/Kore/Builtin/KEqual.hs @@ -17,6 +17,9 @@ builtin modules. module Kore.Builtin.KEqual ( verifiers , builtinFunctions + , KEqual (..) + , termKEquals + , unifyIfThenElse -- * keys , eqKey , neqKey @@ -25,6 +28,11 @@ module Kore.Builtin.KEqual import Prelude.Kore +import Control.Error + ( MaybeT + , hoistMaybe + ) +import qualified Control.Monad as Monad import qualified Data.Functor.Foldable as Recursive import qualified Data.HashMap.Strict as HashMap import Data.Map.Strict @@ -38,6 +46,10 @@ import Data.Text ( Text ) +import qualified Branch +import Kore.Attribute.Hook + ( Hook (..) + ) import qualified Kore.Attribute.Pattern as Attribute import qualified Kore.Builtin.Bool as Bool import Kore.Builtin.Builtin @@ -45,21 +57,27 @@ import Kore.Builtin.Builtin ) import qualified Kore.Builtin.Builtin as Builtin import qualified Kore.Error +import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.OrPattern as OrPattern +import Kore.Internal.Pattern + ( Pattern + ) import qualified Kore.Internal.Pattern as Pattern -import qualified Kore.Internal.SideCondition as SideCondition - ( topTODO +import Kore.Internal.Predicate + ( makeCeilPredicate_ ) +import qualified Kore.Internal.SideCondition as SideCondition +import Kore.Internal.Symbol import Kore.Internal.TermLike -import qualified Kore.Step.Simplification.And as And -import qualified Kore.Step.Simplification.Ceil as Ceil -import qualified Kore.Step.Simplification.Equals as Equals -import qualified Kore.Step.Simplification.Not as Not -import qualified Kore.Step.Simplification.Or as Or +import Kore.Step.Simplification.NotSimplifier import Kore.Step.Simplification.Simplify import Kore.Syntax.Definition ( SentenceSymbol (..) ) +import Kore.Unification.Unify as Unify +import Kore.Unification.Unify + ( MonadUnify + ) verifiers :: Builtin.Verifiers verifiers = @@ -125,7 +143,8 @@ builtinFunctions = ] evalKEq - :: (InternalVariable variable, MonadSimplify simplifier) + :: forall variable simplifier + . (InternalVariable variable, MonadSimplify simplifier) => Bool -> CofreeF (Application Symbol) @@ -134,41 +153,24 @@ evalKEq -> simplifier (AttemptedAxiom variable) evalKEq true (valid :< app) = case applicationChildren of - [t1, t2] -> evalEq t1 t2 + [t1, t2] -> Builtin.getAttemptedAxiom (evalEq t1 t2) _ -> Builtin.wrongArity (if true then eqKey else neqKey) where - sideCondition = SideCondition.topTODO - false = not true sort = Attribute.patternSort valid Application { applicationChildren } = app + comparison x y + | true = x == y + | otherwise = x /= y + evalEq + :: TermLike variable + -> TermLike variable + -> MaybeT simplifier (AttemptedAxiom variable) evalEq termLike1 termLike2 = do - let pattern1 = Pattern.fromTermLike termLike1 - pattern2 = Pattern.fromTermLike termLike2 - - defined1 <- Ceil.makeEvaluate sideCondition pattern1 - defined2 <- Ceil.makeEvaluate sideCondition pattern2 - defined <- - And.simplifyEvaluated Not.notSimplifier sideCondition defined1 defined2 - - equalTerms <- - Equals.makeEvaluateTermsToPredicate - termLike1 - termLike2 - sideCondition - let trueTerm = Bool.asInternal sort true - truePatterns = Pattern.withCondition trueTerm <$> equalTerms - - notEqualTerms <- Not.simplifyEvaluatedPredicate equalTerms - let falseTerm = Bool.asInternal sort false - falsePatterns = Pattern.withCondition falseTerm <$> notEqualTerms - - let undefinedResults = Or.simplifyEvaluated truePatterns falsePatterns - results <- - And.simplifyEvaluated Not.notSimplifier sideCondition defined undefinedResults - pure $ Applied AttemptedAxiomResults - { results - , remainders = OrPattern.bottom - } + asConcrete1 <- hoistMaybe $ Builtin.toKey termLike1 + asConcrete2 <- hoistMaybe $ Builtin.toKey termLike2 + Builtin.appliedFunction + $ Bool.asPattern sort + $ comparison asConcrete1 asConcrete2 evalKIte :: forall variable simplifier @@ -208,3 +210,105 @@ neqKey = "KEQUAL.neq" iteKey :: IsString s => s iteKey = "KEQUAL.ite" + +{- | The @KEQUAL.eq@ hooked symbol applied to @term@-type arguments. + -} +data KEqual term = + KEqual + { symbol :: !Symbol + , operand1, operand2 :: !term + } + +{- | Match the @KEQUAL.eq@ hooked symbol. + -} +matchKEqual :: TermLike variable -> Maybe (KEqual (TermLike variable)) +matchKEqual (App_ symbol [operand1, operand2]) = do + hook2 <- (getHook . symbolHook) symbol + Monad.guard (hook2 == eqKey) + return KEqual { symbol, operand1, operand2 } +matchKEqual _ = Nothing + +termKEquals + :: forall variable unifier + . InternalVariable variable + => MonadUnify unifier + => TermSimplifier variable unifier + -> NotSimplifier unifier + -> TermLike variable + -> TermLike variable + -> MaybeT unifier (Pattern variable) +termKEquals unifyChildren (NotSimplifier notSimplifier) a b = + worker a b <|> worker b a + where + eraseTerm = + Pattern.fromCondition . Pattern.withoutTerm + worker termLike1 termLike2 + | Just KEqual { operand1, operand2 } <- matchKEqual termLike1 + , isFunctionPattern termLike1 + , Just value2 <- Bool.matchBool termLike2 + = lift $ do + solution <- + fmap OrPattern.fromPatterns + <$> Unify.gather + $ unifyChildren operand1 operand2 + let solution' = fmap eraseTerm solution + finalSolution <- + if value2 + then return solution' + else notSimplifier SideCondition.top solution' + Unify.scatter finalSolution + worker _ _ = empty + +{- | The @KEQUAL.ite@ hooked symbol applied to @term@-type arguments. + -} +data IfThenElse term = + IfThenElse + { symbol :: !Symbol + , condition :: !term + , branch1, branch2 :: !term + } + +{- | Match the @KEQUAL.eq@ hooked symbol. + -} +matchIfThenElse :: TermLike variable -> Maybe (IfThenElse (TermLike variable)) +matchIfThenElse (App_ symbol [condition, branch1, branch2]) = do + hook' <- (getHook . symbolHook) symbol + Monad.guard (hook' == iteKey) + return IfThenElse { symbol, condition, branch1, branch2 } +matchIfThenElse _ = Nothing + +unifyIfThenElse + :: forall variable unifier + . InternalVariable variable + => MonadUnify unifier + => TermSimplifier variable unifier + -> TermLike variable + -> TermLike variable + -> MaybeT unifier (Pattern variable) +unifyIfThenElse unifyChildren a b = + worker a b <|> worker b a + where + takeCondition value condition' = + makeCeilPredicate_ (mkAnd (Bool.asInternal sort value) condition') + & Condition.fromPredicate + where + sort = termLikeSort condition' + worker termLike1 termLike2 + | Just ifThenElse <- matchIfThenElse termLike1 + = lift (takeBranch1 ifThenElse <|> takeBranch2 ifThenElse) + where + takeBranch1 IfThenElse { condition, branch1 } = do + solution <- unifyChildren branch1 termLike2 + let branchCondition = takeCondition True condition + Pattern.andCondition solution branchCondition + & simplifyCondition SideCondition.top + & Branch.gather + & (>>= Unify.scatter) + takeBranch2 IfThenElse { condition, branch2 } = do + solution <- unifyChildren branch2 termLike2 + let branchCondition = takeCondition False condition + Pattern.andCondition solution branchCondition + & simplifyCondition SideCondition.top + & Branch.gather + & (>>= Unify.scatter) + worker _ _ = empty diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index 441c554889..53cbf641be 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -34,6 +34,7 @@ import qualified Data.Text as Text import qualified Kore.Builtin.Bool as Builtin.Bool import qualified Kore.Builtin.Endianness as Builtin.Endianness +import qualified Kore.Builtin.KEqual as Builtin.KEqual import qualified Kore.Builtin.List as Builtin.List import qualified Kore.Builtin.Map as Builtin.Map import qualified Kore.Builtin.Set as Builtin.Set @@ -230,6 +231,9 @@ andEqualsFunctions notSimplifier = fmap mapEqualsFunctions , (BothT, \_ _ _ -> constructorAndEqualsAssumesDifferentHeads, "constructorAndEqualsAssumesDifferentHeads") , (BothT, \_ _ s -> overloadedConstructorSortInjectionAndEquals s, "overloadedConstructorSortInjectionAndEquals") , (BothT, \_ _ s -> Builtin.Bool.termAndEquals s, "Builtin.Bool.termAndEquals") + , (BothT, \_ _ s -> Builtin.Bool.termNotBool s, "Builtin.Bool.termNotBool") + , (EqualsT, \_ _ s -> Builtin.KEqual.termKEquals s notSimplifier, "Builtin.KEqual.termKEquals") + , (AndT, \_ _ s -> Builtin.KEqual.unifyIfThenElse s, "Builtin.KEqual.unifyIfThenElse") , (BothT, \_ _ _ -> Builtin.Endianness.unifyEquals, "Builtin.Endianness.unifyEquals") , (BothT, \_ _ _ -> Builtin.Signedness.unifyEquals, "Builtin.Signedness.unifyEquals") , (BothT, \_ _ s -> Builtin.Map.unifyEquals s, "Builtin.Map.unifyEquals") diff --git a/kore/test/Test/Kore/Builtin/KEqual.hs b/kore/test/Test/Kore/Builtin/KEqual.hs index ce2d8ec51d..be45c0f55e 100644 --- a/kore/test/Test/Kore/Builtin/KEqual.hs +++ b/kore/test/Test/Kore/Builtin/KEqual.hs @@ -3,6 +3,7 @@ module Test.Kore.Builtin.KEqual , test_kneq , test_KEqual , test_KIte + , test_KEqualSimplification ) where import Prelude.Kore @@ -11,10 +12,33 @@ import Hedgehog import qualified Hedgehog.Gen as Gen import Test.Tasty +import Control.Monad.Trans.Maybe + ( runMaybeT + ) import qualified Data.Text as Text +import qualified Kore.Builtin.KEqual as KEqual +import Kore.Internal.Pattern + ( Pattern + ) import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.TermLike +import Kore.Step.Simplification.AndTerms + ( termUnification + ) +import Kore.Step.Simplification.Data + ( runSimplifierBranch + ) +import qualified Kore.Step.Simplification.Not as Not +import Kore.Unification.Error + ( UnificationError + ) +import Kore.Unification.UnifierT + ( runUnifierT + ) +import SMT + ( SMT + ) import qualified Test.Kore.Builtin.Bool as Test.Bool import Test.Kore.Builtin.Builtin @@ -56,26 +80,38 @@ test_KEqual = assertEqual' "" expect actual , testCaseWithSMT "kseq(x, dotk) equals kseq(x, dotk)" $ do - let expect = Pattern.fromTermLike $ Test.Bool.asInternal True + let expect = Pattern.top original = - keqBool - (kseq - (mkElemVar (elemVarS "x" kItemSort)) - dotk - ) - (kseq - (mkElemVar (elemVarS "x" kItemSort)) - dotk + mkEquals_ + (Test.Bool.asInternal True) + (keqBool + (kseq (mkElemVar (elemVarS "x" kItemSort)) dotk) + (kseq (mkElemVar (elemVarS "x" kItemSort)) dotk) ) actual <- evaluate original assertEqual' "" expect actual , testCaseWithSMT "kseq(inj(x), dotk) equals kseq(inj(x), dotk)" $ do - let expect = Pattern.fromTermLike $ Test.Bool.asInternal True + let expect = Pattern.top original = - keqBool - (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk) - (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk) + mkEquals_ + (Test.Bool.asInternal True) + (keqBool + (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk) + (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk) + ) + actual <- evaluate original + assertEqual' "" expect actual + + , testCaseWithSMT "distinct constructor-like terms" $ do + let expect = Pattern.top + original = + mkEquals_ + (Test.Bool.asInternal False) + (keqBool + (kseq (inj kItemSort dvX) dotk) + (kseq (inj kItemSort dvT) dotk) + ) actual <- evaluate original assertEqual' "" expect actual @@ -102,17 +138,6 @@ test_KEqual = actual <- evaluate original assertEqual' "" expect actual ] - where - dvT = - mkDomainValue DomainValue - { domainValueSort = idSort - , domainValueChild = mkStringLiteral "t" - } - dvX = - mkDomainValue DomainValue - { domainValueSort = idSort - , domainValueChild = mkStringLiteral "x" - } test_KIte :: [TestTree] test_KIte = @@ -140,3 +165,43 @@ test_KIte = actual <- evaluate original assertEqual' "" expect actual ] + +test_KEqualSimplification :: [TestTree] +test_KEqualSimplification = + [ testCaseWithSMT "constructor1 =/=K constructor2" $ do + let term1 = Test.Bool.asInternal False + term2 = + keqBool + (kseq (inj kItemSort dvX) dotk) + (kseq (inj kItemSort dvT) dotk) + expect = [Right [Just Pattern.top]] + actual <- runKEqualSimplification term1 term2 + assertEqual' "" expect actual + + ] + +dvT, dvX :: TermLike Variable +dvT = + mkDomainValue DomainValue + { domainValueSort = idSort + , domainValueChild = mkStringLiteral "t" + } +dvX = + mkDomainValue DomainValue + { domainValueSort = idSort + , domainValueChild = mkStringLiteral "x" + } + +runKEqualSimplification + :: TermLike Variable + -> TermLike Variable + -> SMT [Either UnificationError [Maybe (Pattern Variable)]] +runKEqualSimplification term1 term2 = + runSimplifierBranch testEnv + . runUnifierT Not.notSimplifier + . runMaybeT + $ KEqual.termKEquals + (termUnification Not.notSimplifier) + Not.notSimplifier + term1 + term2 diff --git a/test/not-kequal/Makefile b/test/not-kequal/Makefile new file mode 100644 index 0000000000..310e0746dd --- /dev/null +++ b/test/not-kequal/Makefile @@ -0,0 +1,3 @@ +DEF := test +MODULE := TEST +include $(CURDIR)/../include.mk diff --git a/test/not-kequal/a.test b/test/not-kequal/a.test new file mode 100644 index 0000000000..5c63345a42 --- /dev/null +++ b/test/not-kequal/a.test @@ -0,0 +1 @@ +#changesState(b,123) diff --git a/test/not-kequal/a.test.out.golden b/test/not-kequal/a.test.out.golden new file mode 100644 index 0000000000..937a92cf66 --- /dev/null +++ b/test/not-kequal/a.test.out.golden @@ -0,0 +1,3 @@ + + true + diff --git a/test/not-kequal/test.k b/test/not-kequal/test.k new file mode 100644 index 0000000000..2671411cf5 --- /dev/null +++ b/test/not-kequal/test.k @@ -0,0 +1,15 @@ +module TEST + imports BOOL + imports INT + + syntax OpCode ::= "a" | "b" | "c" | "d" | "e" | "f" | "g" + + syntax Bool ::= #changesState(OpCode, Int) [function] + + rule #changesState(a, VALUE) => VALUE =/=Int 0 + rule #changesState(OP, _) => ( OP ==K b + orBool OP ==K c + ) + requires notBool ( OP ==K a ) + +endmodule