Remove defined marker (#2380)

* Add HashMap to SideCondition

* Rename assumptions to replacements

* Use simplifyConjunctionWithAssumptions to construct and combine SideCondition

* Hlint

* Use to and from SideCondition to simplify Condition

* Use Changed in simplifyConjunctions again

* Use replacements when simplifying terms, with exception

* Regenerate golden

* Comment out failing test, TODO fix

* Simplify Pattern with SideCondition in only special cases

* Use simplify instead of simplifyTopConfiguration

* Modify test which describes possibly wrong behavior

* Fixed onepath test

* TermLike.simplify unit tests; simplify with all replacements

* Remove unused imports

* Add Pretty instance for SideCondition

* Add documentation

* Add strictness to fields

* Add strict language pragma

* Make lazy binding

* Address review comments

* Clean-up

* Update kore/src/Kore/Step/Simplification/Condition.hs

Co-authored-by: Thomas Tuegel <[email protected]>

* Update Debug.hs

* Modify simplification in checkImplication

* unifyKequalsEq should apply for both \and and \equals

* Tests for KEqual unification

* Add a HashSet of defined TermLikes to SideCondition

* Draft, incomplete implementation of assumeDefined

* Implement assumeDefined for assoc comm collections

* Fix

* Fixes and tests for generateNormalizedAcs

* Tests and fixes

* Keep term and predicate replacements together as terms

* Remove double import

* generateNormalizedAcs: clean-up

* Finish isDefined, add tests and clean-up

* Major test clean-up, include set tests

* Fix functional application case, add tests

* Remove Defined marker

* Materialize Nix expressions

* Propagate side condition in SMT translator

* Use definedness in translatePattern as well

* Add tests for defined SMT translation back

* Remove unused test module

* Get rid of isDefinedPattern in Matcher

* Materialize Nix expressions

* Carry SideCondition in Builtin modules; replace isDefinedPattern

* Remove rest of Defined node

* Fix isDefined case for 1-element, 1-opaque collections

* Add accidentally removed collection unification cases

* Temp: TODO and debugging info

* Fix unit test bugs

* SideCondition, Pattern: clean-up and documentation

* Add unit tests for values definedness

* Update TODO comment

Co-authored-by: Thomas Tuegel <[email protected]>

* Update kore/src/Kore/Step/Simplification/Exists.hs

Co-authored-by: Thomas Tuegel <[email protected]>

* Address review comment

Co-authored-by: Thomas Tuegel <[email protected]>
Co-authored-by: ana-pantilie <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 3 people

kore/kore.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 80d27d36f0343e3b6779aa37ed5fccc747fd7c1b66c7b9bd2fb27c1f6a2d6403
+-- hash: f665c212513ddd12eaa511bf198ce16f125dd902b5b25a656b2fa584d073c5ba
 
 name:           kore
 version:        0.41.0.0
@@ -284,7 +284,6 @@ library
       Kore.Step.Simplification.CeilSimplifier
       Kore.Step.Simplification.Condition
       Kore.Step.Simplification.Data
-      Kore.Step.Simplification.Defined
       Kore.Step.Simplification.DomainValue
       Kore.Step.Simplification.Equals
       Kore.Step.Simplification.Exists
@@ -930,7 +929,6 @@ test-suite kore-test
       Test.Kore.BugReport
       Test.Kore.Builtin
       Test.Kore.Builtin.AssocComm.CeilSimplifier
-      Test.Kore.Builtin.AssociativeCommutative
       Test.Kore.Builtin.Bool
       Test.Kore.Builtin.Builtin
       Test.Kore.Builtin.Definition

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -108,7 +108,6 @@ import Kore.Internal.Symbol
     )
 import Kore.Internal.TermLike
     ( pattern App_
-    , pattern Defined_
     , pattern ElemVar_
     , pattern InternalMap_
     , pattern InternalSet_
@@ -220,7 +219,6 @@ instance TermWrapper NormalizedMap where
 
     matchBuiltin (InternalMap_ internalMap) =
         Just (builtinAcChild internalMap)
-    matchBuiltin (Defined_ child) = matchBuiltin child
     matchBuiltin _ = Nothing
 
     {- |Transforms a @TermLike@ representation into a @NormalizedOrBottom@.
@@ -262,7 +260,6 @@ instance TermWrapper NormalizedMap where
         case args of
             [map1, map2] -> toNormalized map1 <> toNormalized map2
             _ -> Builtin.wrongArity "MAP.concat"
-    toNormalized (Defined_ child) = toNormalized child
     toNormalized patt =
         (Normalized . wrapAc) NormalizedAc
             { elementsWithVariables = []
@@ -357,8 +354,6 @@ toNormalizedInternalMapWorker term@(App_ symbol args)
                     }
             return internal
         _ -> Builtin.wrongArity "MAP.concat"
-toNormalizedInternalMapWorker (Defined_ child) =
-    toNormalizedInternalMapWorker child
 toNormalizedInternalMapWorker term =
     Just (emptyInternalAc @NormalizedMap (termLikeSort term))
         { builtinAcChild = wrapAc emptyNormalizedAc { opaque = [term] }
@@ -386,7 +381,6 @@ instance TermWrapper NormalizedSet where
 
     matchBuiltin (InternalSet_ internalSet) =
         Just (builtinAcChild internalSet)
-    matchBuiltin (Defined_ child) = matchBuiltin child
     matchBuiltin _ = Nothing
 
     {- |Transforms a @TermLike@ representation into a @NormalizedSetOrBottom@.
@@ -427,7 +421,6 @@ instance TermWrapper NormalizedSet where
         case args of
             [set1, set2] -> toNormalized set1 <> toNormalized set2
             _ -> Builtin.wrongArity "SET.concat"
-    toNormalized (Defined_ child) = toNormalized child
     toNormalized patt =
         (Normalized . wrapAc)
         emptyNormalizedAc { opaque = [patt] }
@@ -520,8 +513,6 @@ toNormalizedInternalSetWorker term@(App_ symbol args)
                     }
             return internal
         _ -> Builtin.wrongArity "SET.concat"
-toNormalizedInternalSetWorker (Defined_ child) =
-    toNormalizedInternalSetWorker child
 toNormalizedInternalSetWorker term =
     Just (emptyInternalAc @NormalizedSet (termLikeSort term))
         { builtinAcChild = wrapAc emptyNormalizedAc { opaque = [term] }

kore/src/Kore/Builtin/Builtin.hs

@@ -95,6 +95,9 @@ import Kore.Internal.Predicate
     ( makeEqualsPredicate
     )
 import qualified Kore.Internal.Predicate as Predicate
+import Kore.Internal.SideCondition
+    ( SideCondition
+    )
 import qualified Kore.Internal.SideCondition as SideCondition
     ( topTODO
     )
@@ -180,7 +183,7 @@ unaryOperator extractVal asPattern ctx op =
     get = extractVal ctx
 
     unaryOperator0 :: Function
-    unaryOperator0 resultSort children =
+    unaryOperator0 _ resultSort children =
         case children of
             [termLike]
               | Just a <- get termLike -> do
@@ -220,7 +223,7 @@ binaryOperator extractVal asPattern ctx op =
     get = extractVal ctx
 
     binaryOperator0 :: Function
-    binaryOperator0 resultSort children =
+    binaryOperator0 _ resultSort children =
         case children of
             [get -> Just a, get -> Just b] -> do
                 -- Apply the operator to two domain values
@@ -259,7 +262,7 @@ ternaryOperator extractVal asPattern ctx op =
     get = extractVal ctx
 
     ternaryOperator0 :: Function
-    ternaryOperator0 resultSort children =
+    ternaryOperator0 _ resultSort children =
         case children of
             [get -> Just a, get -> Just b, get -> Just c] -> do
                 -- Apply the operator to three domain values
@@ -273,23 +276,25 @@ type Function
         .  InternalVariable variable
         => HasCallStack
         => MonadSimplify simplifier
-        => Sort
+        => SideCondition variable
+        -> Sort
         -> [TermLike variable]
         -> MaybeT simplifier (Pattern variable)
 
 functionEvaluator :: Function -> BuiltinAndAxiomSimplifier
 functionEvaluator impl =
-    applicationEvaluator $ \app -> do
+    applicationEvaluator $ \sideCondition app -> do
         let Application { applicationSymbolOrAlias = symbol } = app
             Application { applicationChildren = args } = app
             resultSort = symbolSorts symbol & applicationSortsResult
-        impl resultSort args
+        impl sideCondition resultSort args
 
 applicationEvaluator
     ::  ( forall variable simplifier
         .  InternalVariable variable
         => MonadSimplify simplifier
-        => Application Symbol (TermLike variable)
+        => SideCondition variable
+        -> Application Symbol (TermLike variable)
         -> MaybeT simplifier (Pattern variable)
         )
     -> BuiltinAndAxiomSimplifier
@@ -299,14 +304,16 @@ applicationEvaluator impl =
     evaluator
         :: InternalVariable variable
         => MonadSimplify simplifier
-        => CofreeF
+        => SideCondition variable
+        -> CofreeF
             (Application Symbol)
             (Attribute.Pattern variable)
             (TermLike variable)
         -> simplifier (AttemptedAxiom variable)
-    evaluator (_ :< app) = do
+    evaluator sideCondition (_ :< app) = do
         let app' = fmap TermLike.removeEvaluated app
-        getAttemptedAxiom (impl app' >>= appliedFunction)
+        getAttemptedAxiom
+            (impl sideCondition app' >>= appliedFunction)
 
 {- | Run a parser on a verified domain value.
 

kore/src/Kore/Builtin/External.hs

@@ -137,10 +137,6 @@ externalize =
                 $ mapHead Symbol.toSymbolOrAlias
                 $ Signedness.toApplication
                 $ getConst signednessF
-            DefinedF definedF ->
-                Cofree.tailF
-                $ worker
-                $ getDefined definedF
             InjF _ -> error "Unexpected sort injection"
             InternalBoolF _ -> error "Unexpected internal builtin"
             InternalBytesF _ -> error "Unexpected internal builtin"

kore/src/Kore/Builtin/Int.hs

@@ -120,6 +120,7 @@ import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( makeCeilPredicate
     )
+import qualified Kore.Internal.SideCondition as SideCondition
 import Kore.Internal.Symbol
     ( symbolHook
     )
@@ -368,7 +369,7 @@ powmod b e m
     | otherwise = Just (powModInteger b e m)
 
 evalEq :: Builtin.Function
-evalEq resultSort arguments@[_intLeft, _intRight] =
+evalEq sideCondition resultSort arguments@[_intLeft, _intRight] =
     concrete <|> symbolicReflexivity
   where
     concrete = do
@@ -388,13 +389,13 @@ evalEq resultSort arguments@[_intLeft, _intRight] =
             empty
 
     mkCeilUnlessDefined termLike
-      | TermLike.isDefinedPattern termLike = Condition.top
+      | SideCondition.isDefined sideCondition termLike = Condition.top
       | otherwise =
         Condition.fromPredicate (makeCeilPredicate termLike)
     returnPattern = return . flip Pattern.andCondition conditions
     conditions = foldMap mkCeilUnlessDefined arguments
 
-evalEq _ _ = Builtin.wrongArity eqKey
+evalEq _ _ _ = Builtin.wrongArity eqKey
 
 {- | Match the @INT.eq@ hooked symbol.
 -}