Implement branching on predicates (#484)

* Add ListT

* Add BranchT to Simplifier stack

* Use BranchT on top of Simplifier stack

* Add Test.ListT

* Add Kore.Step.Simplification.Predicate.simplifyPartialBranch

* Add Kore.Step.Simplification.PredicateSubstitution.simplifyBranch

* Kore.Step.Simplification: Branching in PredicateSubstitutionSimplifier

* Remove Kore.Step.Simplification.simplifyPartial

* Rename Kore.Step.Simplification.PredicateSubstitution.simplifyBranch

* Allow branching in Kore.Step.Substitution.normalize

* Kore.Step.Substitution.normalizeSubstitutionAfterMerge: Give a meaningful error

* Kore.Step.Simplification.Data: Collect branching documentation in one place

* Kore.Step.Simplification.Data: Clarify capabilities of BranchT and Simplifier

* Rename Kore.Step.Simplification.Predicate.simplify

* ListT: Describe type more clearly

* Predicate.simplifyPartial: Use straightforward pattern matching

* Kore.Step.Substitution: Reduce duplication and redundant checks

* ListT: Add examples

* Kore.Step.Simplification.Data: Clarify comments around scatter and gather

* Prune branches of Simplifier lifted into BranchT

* normalizeWorker: Cleanup

* Add instance MonadSMT BranchT

Author: ttuegel

kore/src/Kore/Builtin/Map.hs

@@ -91,8 +91,6 @@ import           Kore.Step.Simplification.Data
 import           Kore.Step.StepperAttributes
                  ( StepperAttributes )
 import qualified Kore.Step.StepperAttributes as StepperAttributes
-import           Kore.Step.Substitution
-                 ( normalize )
 import           Kore.Unification.Error
                  ( UnificationOrSubstitutionError (..) )
 import           Kore.Unparser
@@ -573,9 +571,9 @@ unifyEquals
 unifyEquals
     simplificationType
     tools
-    substitutionSimplifier
-    simplifier
-    axiomIdToSimplifier
+    _
+    _
+    _
     unifyEqualsChildren
   =
     unifyEquals0
@@ -717,14 +715,7 @@ unifyEquals
                 -- Elements of map2 missing from map1
                 remainder2 = Map.difference map2 map1
 
-        normalized <- Monad.Trans.lift $
-            normalize
-                tools
-                substitutionSimplifier
-                simplifier
-                axiomIdToSimplifier
-                result
-        return (normalized, SimplificationProof)
+        return (result, SimplificationProof)
       where
         Domain.InternalMap { builtinMapSort } = builtin1
         Domain.InternalMap { builtinMapChild = map1 } = builtin1

kore/src/Kore/Builtin/Set.hs

@@ -96,8 +96,6 @@ import           Kore.Step.Simplification.Data
 import           Kore.Step.StepperAttributes
                  ( StepperAttributes )
 import qualified Kore.Step.StepperAttributes as StepperAttributes
-import           Kore.Step.Substitution
-                 ( normalize )
 import           Kore.Unification.Error
                  ( UnificationOrSubstitutionError (..) )
 import           Kore.Unparser
@@ -531,9 +529,9 @@ unifyEquals
 unifyEquals
     simplificationType
     tools
-    substitutionSimplifier
-    simplifier
-    axiomIdToSimplifier
+    _
+    _
+    _
     unifyEqualsChildren
   =
     unifyEquals0
@@ -635,14 +633,7 @@ unifyEquals
                     -- Return the concrete set, but capture any predicates and
                     -- substitutions from unifying the framing variable.
                     asExpandedPattern builtinSetSort set1 <* remainder
-            normalized <- Monad.Trans.lift $
-                normalize
-                    tools
-                    substitutionSimplifier
-                    simplifier
-                    axiomIdToSimplifier
-                    result
-            return (normalized, SimplificationProof)
+            return (result, SimplificationProof)
 
       | otherwise =
         return (ExpandedPattern.bottom, SimplificationProof)