Revert #1784

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

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

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,28 +46,38 @@ 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
     ( acceptAnySort
     )
 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

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")