From 8a26f025fc96d8902631675b550054ae16f3086d Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 6 May 2020 14:02:26 +0300 Subject: [PATCH 01/25] Keep sideCondition and change andCondition --- kore/src/Kore/Internal/SideCondition.hs | 7 ++++--- kore/src/Kore/Step/Simplification/Pattern.hs | 14 +++++++++----- .../Step/Simplification/SubstitutionSimplifier.hs | 7 ++----- kore/src/Kore/Step/Step.hs | 13 +++++-------- 4 files changed, 20 insertions(+), 21 deletions(-) diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index 45dd1db1f3..9a5fdcb9aa 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -161,12 +161,13 @@ andCondition => SideCondition variable -> Condition variable -> SideCondition variable -andCondition SideCondition {assumedTrue} newCondition = - SideCondition +andCondition initial@SideCondition {assumedTrue} newCondition = + if isNormalized result then result else initial + where + result = SideCondition { representation = toRepresentationCondition merged , assumedTrue = merged } - where merged = assumedTrue `Condition.andCondition` newCondition assumeTrueCondition diff --git a/kore/src/Kore/Step/Simplification/Pattern.hs b/kore/src/Kore/Step/Simplification/Pattern.hs index 46ce171e01..2fb3e3c01e 100644 --- a/kore/src/Kore/Step/Simplification/Pattern.hs +++ b/kore/src/Kore/Step/Simplification/Pattern.hs @@ -24,8 +24,10 @@ import Kore.Internal.SideCondition ( SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition - ( andCondition - , topTODO + ( topTODO + ) +import Kore.Internal.Substitution + ( toMap ) import Kore.Internal.TermLike ( pattern Exists_ @@ -36,6 +38,9 @@ import Kore.Step.Simplification.Simplify , simplifyCondition , simplifyConditionalTermToOr ) +import Kore.Substitute + ( substitute + ) {-| Simplifies the pattern without a side-condition (i.e. it's top) and removes the exists quantifiers at the top. @@ -68,9 +73,8 @@ simplify sideCondition pattern' = withSimplifiedCondition <- simplifyCondition sideCondition pattern' let (term, simplifiedCondition) = Conditional.splitTerm withSimplifiedCondition - termSideCondition = - sideCondition `SideCondition.andCondition` simplifiedCondition - orSimplifiedTerms <- simplifyConditionalTermToOr termSideCondition term + term' = substitute (toMap $ substitution simplifiedCondition) term + orSimplifiedTerms <- simplifyConditionalTermToOr sideCondition term' simplifiedTerm <- Branch.scatter orSimplifiedTerms simplifyCondition sideCondition diff --git a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs index 48fc18bcf7..d7db4b3ada 100644 --- a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs +++ b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs @@ -74,8 +74,7 @@ import Kore.Internal.SideCondition ( SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition - ( andCondition - , toRepresentation + ( toRepresentation , topTODO ) import Kore.Internal.Substitution @@ -195,9 +194,7 @@ simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) = AndF And { andFirst, andSecond } -> foldM simplifyAnds' intermediate [andFirst, andSecond] _ -> do - let sideCondition = - SideCondition.topTODO - `SideCondition.andCondition` intermediateCondition + let sideCondition = SideCondition.topTODO simplified <- makeAnd intermediateTerm diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 91b1103f31..fa19ec55a5 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -67,8 +67,7 @@ import Kore.Internal.SideCondition ( SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition - ( andCondition - , mapVariables + ( mapVariables ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike @@ -151,19 +150,17 @@ unifyRule -- ^ Rule -> BranchT simplifier (UnifiedRule rule variable) unifyRule unificationProcedure sideCondition initial rule = do - let (initialTerm, initialCondition) = Pattern.splitTerm initial - mergedSideCondition = - sideCondition `SideCondition.andCondition` initialCondition + let (initialTerm, _) = Pattern.splitTerm initial -- Unify the left-hand side of the rule with the term of the initial -- configuration. let ruleLeft = matchingPattern rule unification <- - unifyTermLikes mergedSideCondition initialTerm ruleLeft + unifyTermLikes sideCondition initialTerm ruleLeft -- Combine the unification solution with the rule's requirement clause, let ruleRequires = precondition rule requires' = Condition.fromPredicate ruleRequires unification' <- - simplifyPredicate mergedSideCondition Nothing (unification <> requires') + simplifyPredicate sideCondition Nothing (unification <> requires') return (rule `Conditional.withCondition` unification') where unifyTermLikes = runUnificationProcedure unificationProcedure @@ -302,7 +299,7 @@ simplifyPredicate simplifyPredicate sideCondition (Just initialCondition) conditional = do partialResult <- Simplifier.simplifyCondition - (sideCondition `SideCondition.andCondition` initialCondition) + sideCondition conditional -- TODO (virgil): Consider using different simplifyPredicate implementations -- for rewrite rules and equational rules. From a4c006bd2719f4a0bb42ad278faaf2ca8a3570ee Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 6 May 2020 20:21:11 +0300 Subject: [PATCH 02/25] addressed coments more carefully --- kore/src/Kore/Step/Simplification/Pattern.hs | 5 ++++- kore/src/Kore/Unification/Procedure.hs | 7 +------ kore/test/Test/Kore/Strategies/OnePath/Step.hs | 3 ++- 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Pattern.hs b/kore/src/Kore/Step/Simplification/Pattern.hs index 2fb3e3c01e..e57cf73c45 100644 --- a/kore/src/Kore/Step/Simplification/Pattern.hs +++ b/kore/src/Kore/Step/Simplification/Pattern.hs @@ -25,6 +25,7 @@ import Kore.Internal.SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition ( topTODO + , andCondition ) import Kore.Internal.Substitution ( toMap @@ -74,7 +75,9 @@ simplify sideCondition pattern' = let (term, simplifiedCondition) = Conditional.splitTerm withSimplifiedCondition term' = substitute (toMap $ substitution simplifiedCondition) term - orSimplifiedTerms <- simplifyConditionalTermToOr sideCondition term' + termSideCondition = + sideCondition `SideCondition.andCondition` simplifiedCondition + orSimplifiedTerms <- simplifyConditionalTermToOr termSideCondition term' simplifiedTerm <- Branch.scatter orSimplifiedTerms simplifyCondition sideCondition diff --git a/kore/src/Kore/Unification/Procedure.hs b/kore/src/Kore/Unification/Procedure.hs index e5b242881e..794afa1d17 100644 --- a/kore/src/Kore/Unification/Procedure.hs +++ b/kore/src/Kore/Unification/Procedure.hs @@ -26,9 +26,6 @@ import qualified Kore.Internal.Pattern as Conditional import Kore.Internal.SideCondition ( SideCondition ) -import qualified Kore.Internal.SideCondition as SideCondition - ( andCondition - ) import Kore.Internal.TermLike import Kore.Log.InfoAttemptUnification ( infoAttemptUnification @@ -75,9 +72,7 @@ unificationProcedureWorker sideCondition p1 p2 pat <- termUnification Not.notSimplifier p1 p2 TopBottom.guardAgainstBottom pat let (term, conditions) = Conditional.splitTerm pat - mergedSideCondition = - sideCondition `SideCondition.andCondition` conditions - orCeil <- Ceil.makeEvaluateTerm mergedSideCondition term + orCeil <- Ceil.makeEvaluateTerm sideCondition term ceil' <- Monad.Unify.scatter orCeil BranchT.alternate . simplifyCondition sideCondition $ Conditional.andCondition ceil' conditions diff --git a/kore/test/Test/Kore/Strategies/OnePath/Step.hs b/kore/test/Test/Kore/Strategies/OnePath/Step.hs index 2f3038c928..d9f59636c7 100644 --- a/kore/test/Test/Kore/Strategies/OnePath/Step.hs +++ b/kore/test/Test/Kore/Strategies/OnePath/Step.hs @@ -775,7 +775,8 @@ test_onePathStrategy = goal [] [] - assertEqual "" (ProofState.GoalStuck goal) _actual + assertEqual "" (ProofState.GoalStuck goal) + $ trace ("\n\nACTUAL\n\n" <> show _actual) _actual ] simpleRewrite From 672ab1f9aab8e8d0ec599a1c5310ae1dc142c4ba Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 6 May 2020 20:31:59 +0300 Subject: [PATCH 03/25] clean up --- kore/src/Kore/Step/Simplification/Pattern.hs | 4 ++-- kore/test/Test/Kore/Strategies/OnePath/Step.hs | 3 +-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/Pattern.hs b/kore/src/Kore/Step/Simplification/Pattern.hs index e57cf73c45..3e0b50e7f5 100644 --- a/kore/src/Kore/Step/Simplification/Pattern.hs +++ b/kore/src/Kore/Step/Simplification/Pattern.hs @@ -24,8 +24,8 @@ import Kore.Internal.SideCondition ( SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition - ( topTODO - , andCondition + ( andCondition + , topTODO ) import Kore.Internal.Substitution ( toMap diff --git a/kore/test/Test/Kore/Strategies/OnePath/Step.hs b/kore/test/Test/Kore/Strategies/OnePath/Step.hs index d9f59636c7..2f3038c928 100644 --- a/kore/test/Test/Kore/Strategies/OnePath/Step.hs +++ b/kore/test/Test/Kore/Strategies/OnePath/Step.hs @@ -775,8 +775,7 @@ test_onePathStrategy = goal [] [] - assertEqual "" (ProofState.GoalStuck goal) - $ trace ("\n\nACTUAL\n\n" <> show _actual) _actual + assertEqual "" (ProofState.GoalStuck goal) _actual ] simpleRewrite From 4682190194714176bd9ab7b9325e78342b239285 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= <53746396+andreiburdusa@users.noreply.github.com> Date: Wed, 6 May 2020 23:24:21 +0300 Subject: [PATCH 04/25] Update kore/src/Kore/Internal/SideCondition.hs Co-authored-by: Thomas Tuegel --- kore/src/Kore/Internal/SideCondition.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index 9a5fdcb9aa..196436b64b 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -162,7 +162,7 @@ andCondition -> Condition variable -> SideCondition variable andCondition initial@SideCondition {assumedTrue} newCondition = - if isNormalized result then result else initial + assert (isNormalized result) result where result = SideCondition { representation = toRepresentationCondition merged From 92731f6a55629b04b4926736b210deb603f7c7af Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Thu, 7 May 2020 11:29:45 +0300 Subject: [PATCH 05/25] pedantic --- kore/src/Kore/Internal/SideCondition.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index 196436b64b..a4ea6bc931 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -161,7 +161,7 @@ andCondition => SideCondition variable -> Condition variable -> SideCondition variable -andCondition initial@SideCondition {assumedTrue} newCondition = +andCondition SideCondition {assumedTrue} newCondition = assert (isNormalized result) result where result = SideCondition From 3ceb88b884dda0cdad7de10204c3175e2b0f2abe Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 10:09:37 -0500 Subject: [PATCH 06/25] applyInitialConditions: No SideCondition argument --- kore/src/Kore/Step/RewriteStep.hs | 8 ++++---- kore/src/Kore/Step/Step.hs | 11 +++-------- kore/test/Test/Kore/Step/RewriteStep.hs | 2 +- 3 files changed, 8 insertions(+), 13 deletions(-) diff --git a/kore/src/Kore/Step/RewriteStep.hs b/kore/src/Kore/Step/RewriteStep.hs index 6a1fb3421a..e09278e347 100644 --- a/kore/src/Kore/Step/RewriteStep.hs +++ b/kore/src/Kore/Step/RewriteStep.hs @@ -136,10 +136,10 @@ finalizeRule initialVariables initial unifiedRule = Branch.gather $ do let initialCondition = Conditional.withoutTerm initial let unificationCondition = Conditional.withoutTerm unifiedRule - applied <- applyInitialConditions - SideCondition.topTODO - (Just initialCondition) - unificationCondition + applied <- + applyInitialConditions + (Just initialCondition) + unificationCondition checkSubstitutionCoverage initial (RewriteRule <$> unifiedRule) let renamedRule = Conditional.term unifiedRule final <- finalizeAppliedRule renamedRule applied diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 91b1103f31..bcf02561cc 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -67,9 +67,6 @@ import Kore.Internal.SideCondition ( SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition - ( andCondition - , mapVariables - ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( InternalVariable @@ -240,20 +237,18 @@ applyInitialConditions :: forall simplifier variable . InternalVariable variable => MonadSimplify simplifier - => SideCondition variable - -- ^ Top-level conditions - -> Maybe (Condition variable) + => Maybe (Condition variable) -- ^ Initial conditions -> Condition variable -- ^ Unification conditions -> BranchT simplifier (OrCondition variable) -- TODO(virgil): This should take advantage of the BranchT and not return -- an OrCondition. -applyInitialConditions sideCondition initial unification = do +applyInitialConditions initial unification = do -- Combine the initial conditions and the unification conditions. -- The axiom requires clause is included in the unification conditions. applied <- - simplifyPredicate sideCondition initial unification + simplifyPredicate SideCondition.topTODO initial unification & MultiOr.gather evaluated <- SMT.Evaluator.filterMultiOr applied -- If 'evaluated' is \bottom, the rule is considered to not apply and diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 13c2a9aa39..0d753630a5 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -91,7 +91,7 @@ applyInitialConditions -> Condition Variable -> IO [OrCondition Variable] applyInitialConditions initial unification = - Step.applyInitialConditions SideCondition.top (Just initial) unification + Step.applyInitialConditions (Just initial) unification & runSimplifier Mock.env . Branch.gather test_applyInitialConditions :: [TestTree] From 0e65e25d99bef0fa652130f43d325eaac8a0e5cf Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 10:12:32 -0500 Subject: [PATCH 07/25] applyInitialConditions: Initial Condition is not optional --- kore/src/Kore/Step/RewriteStep.hs | 5 +---- kore/src/Kore/Step/Step.hs | 4 ++-- kore/test/Test/Kore/Step/RewriteStep.hs | 2 +- 3 files changed, 4 insertions(+), 7 deletions(-) diff --git a/kore/src/Kore/Step/RewriteStep.hs b/kore/src/Kore/Step/RewriteStep.hs index e09278e347..9bc0c02a1d 100644 --- a/kore/src/Kore/Step/RewriteStep.hs +++ b/kore/src/Kore/Step/RewriteStep.hs @@ -136,10 +136,7 @@ finalizeRule initialVariables initial unifiedRule = Branch.gather $ do let initialCondition = Conditional.withoutTerm initial let unificationCondition = Conditional.withoutTerm unifiedRule - applied <- - applyInitialConditions - (Just initialCondition) - unificationCondition + applied <- applyInitialConditions initialCondition unificationCondition checkSubstitutionCoverage initial (RewriteRule <$> unifiedRule) let renamedRule = Conditional.term unifiedRule final <- finalizeAppliedRule renamedRule applied diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index bcf02561cc..d9922a8150 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -237,7 +237,7 @@ applyInitialConditions :: forall simplifier variable . InternalVariable variable => MonadSimplify simplifier - => Maybe (Condition variable) + => Condition variable -- ^ Initial conditions -> Condition variable -- ^ Unification conditions @@ -248,7 +248,7 @@ applyInitialConditions initial unification = do -- Combine the initial conditions and the unification conditions. -- The axiom requires clause is included in the unification conditions. applied <- - simplifyPredicate SideCondition.topTODO initial unification + simplifyPredicate SideCondition.topTODO (Just initial) unification & MultiOr.gather evaluated <- SMT.Evaluator.filterMultiOr applied -- If 'evaluated' is \bottom, the rule is considered to not apply and diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 0d753630a5..1ca0ef28b5 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -91,7 +91,7 @@ applyInitialConditions -> Condition Variable -> IO [OrCondition Variable] applyInitialConditions initial unification = - Step.applyInitialConditions (Just initial) unification + Step.applyInitialConditions initial unification & runSimplifier Mock.env . Branch.gather test_applyInitialConditions :: [TestTree] From 7237c21cec3fcefe8a803b8ecf9de126182a2df4 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 10:16:30 -0500 Subject: [PATCH 08/25] applyInitialConditions: Inline simplifyPredicate --- kore/src/Kore/Step/Step.hs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index d9922a8150..cfb9b98459 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -245,10 +245,17 @@ applyInitialConditions -- TODO(virgil): This should take advantage of the BranchT and not return -- an OrCondition. applyInitialConditions initial unification = do - -- Combine the initial conditions and the unification conditions. - -- The axiom requires clause is included in the unification conditions. + -- Combine the initial conditions and the unification conditions. The axiom + -- requires clause is already included in the unification conditions. applied <- - simplifyPredicate SideCondition.topTODO (Just initial) unification + do + partial <- + Simplifier.simplifyCondition + SideCondition.topTODO + unification + Simplifier.simplifyCondition + SideCondition.topTODO + (initial <> partial) & MultiOr.gather evaluated <- SMT.Evaluator.filterMultiOr applied -- If 'evaluated' is \bottom, the rule is considered to not apply and From 593675b1f402ede37fa815cc8d82286cda54d841 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 10:21:21 -0500 Subject: [PATCH 09/25] applyInitialConditions: Use initial condition to simplify unification solution --- kore/src/Kore/Step/Step.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index cfb9b98459..dcca3acad3 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -249,10 +249,16 @@ applyInitialConditions initial unification = do -- requires clause is already included in the unification conditions. applied <- do + -- Simplify the unification solution under the initial + -- conditions. We must ensure that functions in the solution are + -- evaluated using the top-level side conditions because we will not + -- re-evaluate them after they are added to the top level. partial <- Simplifier.simplifyCondition - SideCondition.topTODO + (SideCondition.fromCondition initial) unification + -- Add the simplified unification solution to the initial + -- conditions. We must preserve the initial conditions here! Simplifier.simplifyCondition SideCondition.topTODO (initial <> partial) From 2a851c7c3af4960571e1972a7ab174d084fe3c6b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 10:38:42 -0500 Subject: [PATCH 10/25] applyRemainder: No SideCondition argument --- kore/src/Kore/Step/RewriteStep.hs | 8 ++------ kore/src/Kore/Step/Step.hs | 11 ++++++----- 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/kore/src/Kore/Step/RewriteStep.hs b/kore/src/Kore/Step/RewriteStep.hs index 9bc0c02a1d..5f6d97a93b 100644 --- a/kore/src/Kore/Step/RewriteStep.hs +++ b/kore/src/Kore/Step/RewriteStep.hs @@ -158,9 +158,7 @@ finalizeRulesParallel initialVariables initial unifiedRules = do & fmap Foldable.fold let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules) remainder = Condition.fromPredicate (Remainder.remainder' unifications) - remainders' <- - applyRemainder SideCondition.topTODO initial remainder - & Branch.gather + remainders' <- applyRemainder initial remainder & Branch.gather return Step.Results { results = Seq.fromList results , remainders = @@ -173,9 +171,7 @@ finalizeRulesSequence initialVariables initial unifiedRules = do State.runStateT (traverse finalizeRuleSequence' unifiedRules) (Conditional.withoutTerm initial) - remainders' <- - applyRemainder SideCondition.topTODO initial remainder - & Branch.gather + remainders' <- applyRemainder initial remainder & Branch.gather return Step.Results { results = Seq.fromList $ Foldable.fold results , remainders = diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index dcca3acad3..a6a3e3be7c 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -285,17 +285,18 @@ applyRemainder :: forall simplifier variable . InternalVariable variable => MonadSimplify simplifier - => SideCondition variable - -- ^ Top level condition - -> Pattern variable + => Pattern variable -- ^ Initial configuration -> Condition variable -- ^ Remainder -> BranchT simplifier (Pattern variable) -applyRemainder sideCondition initial remainder = do +applyRemainder initial remainder = do let (initialTerm, initialCondition) = Pattern.splitTerm initial normalizedCondition <- - simplifyPredicate sideCondition (Just initialCondition) remainder + simplifyPredicate + SideCondition.topTODO + (Just initialCondition) + remainder return normalizedCondition { Conditional.term = initialTerm } -- | Simplifies the predicate obtained upon matching/unification. From 9973418cb666c042f3435ae1ebb8b3f57c070989 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 10:50:38 -0500 Subject: [PATCH 11/25] applyRemainder: Inline simplifyPredicate --- kore/src/Kore/Step/Step.hs | 10 ++-- kore/test/Test/Kore/Step/RewriteStep.hs | 62 ++++++++++++++----------- 2 files changed, 39 insertions(+), 33 deletions(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index a6a3e3be7c..1852dd860b 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -291,13 +291,13 @@ applyRemainder -- ^ Remainder -> BranchT simplifier (Pattern variable) applyRemainder initial remainder = do - let (initialTerm, initialCondition) = Pattern.splitTerm initial - normalizedCondition <- - simplifyPredicate + partial <- + Simplifier.simplifyCondition SideCondition.topTODO - (Just initialCondition) remainder - return normalizedCondition { Conditional.term = initialTerm } + Simplifier.simplifyCondition + SideCondition.topTODO + (Pattern.andCondition initial partial) -- | Simplifies the predicate obtained upon matching/unification. simplifyPredicate diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 1ca0ef28b5..0508943514 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -850,8 +850,11 @@ test_applyRewriteRulesParallel = , predicate = makeNotPredicate $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) , substitution = mempty } ] @@ -895,11 +898,15 @@ test_applyRewriteRulesParallel = (mkElemVar Mock.x) Mock.cg , predicate = - makeAndPredicate (makeCeilPredicate_ Mock.cf) - $ makeNotPredicate - $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + makeAndPredicate + (makeCeilPredicate Mock.testSort Mock.cf) + (makeNotPredicate $ makeAndPredicate + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) + ) , substitution = mempty } ] @@ -937,7 +944,7 @@ test_applyRewriteRulesParallel = remainders = MultiOr.singleton Conditional { term = Mock.functionalConstr10 (mkElemVar Mock.x) - , predicate = makeNotPredicate requirementUnsorted + , predicate = makeNotPredicate requirement , substitution = mempty } initial = pure (Mock.functionalConstr10 (mkElemVar Mock.x)) @@ -945,8 +952,6 @@ test_applyRewriteRulesParallel = makeEqualsPredicate Mock.testSort (Mock.f (mkElemVar Mock.x)) Mock.b - requirementUnsorted = - makeEqualsPredicate_ (Mock.f (mkElemVar Mock.x)) Mock.b Right actual <- applyRewriteRulesParallel initial [axiomSignum] checkResults results actual checkRemainders remainders actual @@ -980,8 +985,11 @@ test_applyRewriteRulesParallel = { predicate = makeNotPredicate $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) } ] initialTerm = Mock.functionalConstr20 (mkElemVar Mock.x) Mock.cg @@ -1016,10 +1024,6 @@ test_applyRewriteRulesParallel = makeAndPredicate (makeCeilPredicate Mock.testSort Mock.cf) (makeCeilPredicate_ Mock.cg) - definedBranchesUnsorted = - makeAndPredicate - (makeCeilPredicate_ Mock.cf) - (makeCeilPredicate_ Mock.cg) results = OrPattern.fromPatterns [ Conditional @@ -1044,19 +1048,19 @@ test_applyRewriteRulesParallel = [ initial { predicate = Predicate.makeAndPredicate - (Predicate.makeNotPredicate - $ Predicate.makeAndPredicate - definedBranchesUnsorted - $ Predicate.makeEqualsPredicate_ + (makeNotPredicate $ makeAndPredicate + definedBranches + (Predicate.makeEqualsPredicate Mock.testSort (mkElemVar Mock.x) Mock.a + ) ) - (Predicate.makeNotPredicate - $ Predicate.makeAndPredicate - definedBranchesUnsorted - $ Predicate.makeEqualsPredicate_ + (makeNotPredicate $ makeAndPredicate + definedBranches + (Predicate.makeEqualsPredicate Mock.testSort (mkElemVar Mock.x) Mock.b + ) ) } ] @@ -1094,10 +1098,12 @@ test_applyRewriteRulesParallel = OrPattern.fromPatterns [ initial { predicate = - makeNotPredicate - $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + makeNotPredicate $ makeAndPredicate + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) } ] initialTerm = Mock.functionalConstr20 (mkElemVar Mock.x) Mock.cg From b85996b2101aadd69f956fa939b86ed102122bdc Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 10:53:54 -0500 Subject: [PATCH 12/25] applyRemainder: Use initial condition to simplify remainders --- kore/src/Kore/Step/Step.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 1852dd860b..6bf2ebc343 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -291,10 +291,16 @@ applyRemainder -- ^ Remainder -> BranchT simplifier (Pattern variable) applyRemainder initial remainder = do + -- Simplify the remainder predicate under the initial conditions. We must + -- ensure that functions in the remainder are evaluated using the top-level + -- side conditions because we will not re-evaluate them after they are added + -- to the top level. partial <- Simplifier.simplifyCondition - SideCondition.topTODO + (SideCondition.fromCondition $ Pattern.withoutTerm initial) remainder + -- Add the simplified remainder to the initial conditions. We must preserve + -- the initial conditions here! Simplifier.simplifyCondition SideCondition.topTODO (Pattern.andCondition initial partial) From d86613d016178732033029272d08cb5c1a7bee04 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 11:18:51 -0500 Subject: [PATCH 13/25] unifyRule: No SideCondition argument --- kore/src/Kore/Step/Step.hs | 16 ++++++---------- kore/test/Test/Kore/Step/RewriteStep.hs | 9 +-------- 2 files changed, 7 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 6bf2ebc343..cea4dbc001 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -117,10 +117,10 @@ unifyRules -> [rule RewritingVariable] -- ^ Rule -> simplifier [UnifiedRule rule RewritingVariable] -unifyRules unificationProcedure sideCondition initial rules = +unifyRules unificationProcedure _ initial rules = Branch.gather $ do rule <- Branch.scatter rules - unifyRule unificationProcedure sideCondition initial rule + unifyRule unificationProcedure initial rule {- | Attempt to unify a rule with the initial configuration. @@ -140,27 +140,23 @@ unifyRule => MonadSimplify simplifier => UnifyingRule rule => UnificationProcedure simplifier - -> SideCondition variable - -- ^ Top level condition. -> Pattern variable -- ^ Initial configuration -> rule variable -- ^ Rule -> BranchT simplifier (UnifiedRule rule variable) -unifyRule unificationProcedure sideCondition initial rule = do +unifyRule unificationProcedure initial rule = do let (initialTerm, initialCondition) = Pattern.splitTerm initial - mergedSideCondition = - sideCondition `SideCondition.andCondition` initialCondition + sideCondition = SideCondition.fromCondition initialCondition -- Unify the left-hand side of the rule with the term of the initial -- configuration. let ruleLeft = matchingPattern rule - unification <- - unifyTermLikes mergedSideCondition initialTerm ruleLeft + unification <- unifyTermLikes sideCondition initialTerm ruleLeft -- Combine the unification solution with the rule's requirement clause, let ruleRequires = precondition rule requires' = Condition.fromPredicate ruleRequires unification' <- - simplifyPredicate mergedSideCondition Nothing (unification <> requires') + simplifyPredicate sideCondition Nothing (unification <> requires') return (rule `Conditional.withCondition` unification') where unifyTermLikes = runUnificationProcedure unificationProcedure diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 0508943514..e02e2eb768 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -54,9 +54,6 @@ import Kore.Internal.Predicate as Predicate , makeTruePredicate , makeTruePredicate_ ) -import qualified Kore.Internal.SideCondition as SideCondition - ( top - ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike import Kore.Rewriting.RewritingVariable @@ -153,11 +150,7 @@ unifyRule [Conditional Variable (RulePattern Variable)] ) unifyRule initial rule = - Step.unifyRule - Unification.unificationProcedure - SideCondition.top - initial - rule + Step.unifyRule Unification.unificationProcedure initial rule & runExceptT . Branch.gather & runSimplifier Mock.env From 1c7d8169c5ca9af8b426c99c88180b0be7622e24 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 11:19:47 -0500 Subject: [PATCH 14/25] unifyRules: No SideCondition argument --- kore/src/Kore/Step/RewriteStep.hs | 5 ++--- kore/src/Kore/Step/Step.hs | 3 +-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Step/RewriteStep.hs b/kore/src/Kore/Step/RewriteStep.hs index 5f6d97a93b..669a04ca50 100644 --- a/kore/src/Kore/Step/RewriteStep.hs +++ b/kore/src/Kore/Step/RewriteStep.hs @@ -204,10 +204,9 @@ applyRulesWithFinalizer -- ^ Configuration being rewritten -> simplifier (Results RulePattern Variable) applyRulesWithFinalizer finalize unificationProcedure rules initial = do - let sideCondition = SideCondition.topTODO - initialVariables = freeVariables sideCondition <> freeVariables initial - results <- unifyRules unificationProcedure sideCondition initial rules + results <- unifyRules unificationProcedure initial rules debugAppliedRewriteRules initial results + let initialVariables = freeVariables initial finalize initialVariables initial results {-# INLINE applyRulesWithFinalizer #-} diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index cea4dbc001..3913ddbd64 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -111,13 +111,12 @@ unifyRules :: MonadSimplify simplifier => UnifyingRule rule => UnificationProcedure simplifier - -> SideCondition RewritingVariable -> Pattern RewritingVariable -- ^ Initial configuration -> [rule RewritingVariable] -- ^ Rule -> simplifier [UnifiedRule rule RewritingVariable] -unifyRules unificationProcedure _ initial rules = +unifyRules unificationProcedure initial rules = Branch.gather $ do rule <- Branch.scatter rules unifyRule unificationProcedure initial rule From cf227cb46397876edb43b4018490c2b3376901b3 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 14:20:18 -0500 Subject: [PATCH 15/25] applyInitialConditions: Inputs are simplified --- kore/src/Kore/Step/Step.hs | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 3913ddbd64..1c044c9f74 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -227,6 +227,10 @@ checkFunctionLike unifiedRules pat The rule is considered to apply if the result is not @\\bottom@. +@applyInitialConditions@ assumes that the unification solution includes the +@requires@ clause, and that their conjunction has already been simplified with +respect to the initial condition. + -} applyInitialConditions :: forall simplifier variable @@ -241,22 +245,14 @@ applyInitialConditions -- an OrCondition. applyInitialConditions initial unification = do -- Combine the initial conditions and the unification conditions. The axiom - -- requires clause is already included in the unification conditions. + -- requires clause is already included in the unification conditions, and + -- the conjunction has already been simplified with respect to the initial + -- conditions. applied <- - do - -- Simplify the unification solution under the initial - -- conditions. We must ensure that functions in the solution are - -- evaluated using the top-level side conditions because we will not - -- re-evaluate them after they are added to the top level. - partial <- - Simplifier.simplifyCondition - (SideCondition.fromCondition initial) - unification - -- Add the simplified unification solution to the initial - -- conditions. We must preserve the initial conditions here! - Simplifier.simplifyCondition - SideCondition.topTODO - (initial <> partial) + -- Add the simplified unification solution to the initial conditions. We + -- must preserve the initial conditions here, so it cannot be used as + -- the side condition! + Simplifier.simplifyCondition SideCondition.top (initial <> unification) & MultiOr.gather evaluated <- SMT.Evaluator.filterMultiOr applied -- If 'evaluated' is \bottom, the rule is considered to not apply and From 1d9750cf5961411ce9db773286ba1bfd7942059b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 14:30:55 -0500 Subject: [PATCH 16/25] applyRemainder: Inputs are simplified --- kore/src/Kore/Step/Step.hs | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 1c044c9f74..d1a00388d1 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -271,6 +271,11 @@ toConfigurationVariablesCondition = {- | Apply the remainder predicate to the given initial configuration. +@applyRemainder@ assumes that the unification solution used to construct the +remainders was simplified with respect to the initial conditions before the +remainder was constructed, and therefore the remainder does not need to be +re-simplified. + -} applyRemainder :: forall simplifier variable @@ -281,20 +286,12 @@ applyRemainder -> Condition variable -- ^ Remainder -> BranchT simplifier (Pattern variable) -applyRemainder initial remainder = do - -- Simplify the remainder predicate under the initial conditions. We must - -- ensure that functions in the remainder are evaluated using the top-level - -- side conditions because we will not re-evaluate them after they are added - -- to the top level. - partial <- - Simplifier.simplifyCondition - (SideCondition.fromCondition $ Pattern.withoutTerm initial) - remainder +applyRemainder initial remainder = -- Add the simplified remainder to the initial conditions. We must preserve - -- the initial conditions here! + -- the initial conditions here, so it cannot be used as the side condition! Simplifier.simplifyCondition SideCondition.topTODO - (Pattern.andCondition initial partial) + (Pattern.andCondition initial remainder) -- | Simplifies the predicate obtained upon matching/unification. simplifyPredicate From 9fdf8bdbb5076d13ee71d822ffdb7570e4733f0b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 14:31:11 -0500 Subject: [PATCH 17/25] finalizeAppliedRule: Inline simplifyPredicate --- kore/src/Kore/Step/RewriteStep.hs | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Step/RewriteStep.hs b/kore/src/Kore/Step/RewriteStep.hs index 669a04ca50..b88a72ebe1 100644 --- a/kore/src/Kore/Step/RewriteStep.hs +++ b/kore/src/Kore/Step/RewriteStep.hs @@ -38,8 +38,6 @@ import Kore.Internal.OrPattern import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern as Pattern import qualified Kore.Internal.SideCondition as SideCondition - ( topTODO - ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike as TermLike import Kore.Log.DebugAppliedRewriteRules @@ -59,6 +57,7 @@ import Kore.Step.RulePattern import qualified Kore.Step.RulePattern as Rule import Kore.Step.Simplification.Simplify ( MonadSimplify + , simplifyCondition ) import Kore.Step.Step ( Result @@ -69,7 +68,6 @@ import Kore.Step.Step , applyRemainder , assertFunctionLikeResults , mkRewritingPattern - , simplifyPredicate , unifyRules ) @@ -112,8 +110,13 @@ finalizeAppliedRule renamedRule appliedConditions = Conditional { predicate = ensures } = finalPattern ensuresCondition = Condition.fromPredicate ensures finalCondition <- - simplifyPredicate - SideCondition.topTODO (Just appliedCondition) ensuresCondition + do + partial <- + simplifyCondition + (SideCondition.fromCondition appliedCondition) + ensuresCondition + simplifyCondition SideCondition.top + (appliedCondition <> partial) & Branch.alternate -- Apply the normalized substitution to the right-hand side of the -- axiom. From 0191924248d4b13ec252a9edd7b7d774237abe10 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 14:32:40 -0500 Subject: [PATCH 18/25] unifyRule: Inline simplifyPredicate --- kore/src/Kore/Step/Step.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index d1a00388d1..df747f519b 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -155,7 +155,9 @@ unifyRule unificationProcedure initial rule = do let ruleRequires = precondition rule requires' = Condition.fromPredicate ruleRequires unification' <- - simplifyPredicate sideCondition Nothing (unification <> requires') + Simplifier.simplifyCondition + sideCondition + (unification <> requires') return (rule `Conditional.withCondition` unification') where unifyTermLikes = runUnificationProcedure unificationProcedure From 571a23af64bb292e527b9dbda3123cc01ff1f635 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 14:32:59 -0500 Subject: [PATCH 19/25] Remove Kore.Step.Step.simplifyPredicate --- kore/src/Kore/Step/Step.hs | 32 -------------------------------- 1 file changed, 32 deletions(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index df747f519b..dee4e14557 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -16,7 +16,6 @@ module Kore.Step.Step , unifyRule , applyInitialConditions , applyRemainder - , simplifyPredicate , toConfigurationVariablesCondition , assertFunctionLikeResults , checkFunctionLike @@ -294,34 +293,3 @@ applyRemainder initial remainder = Simplifier.simplifyCondition SideCondition.topTODO (Pattern.andCondition initial remainder) - --- | Simplifies the predicate obtained upon matching/unification. -simplifyPredicate - :: forall simplifier variable term - . InternalVariable variable - => MonadSimplify simplifier - => SideCondition variable - -> Maybe (Condition variable) - -> Conditional variable term - -> BranchT simplifier (Conditional variable term) -simplifyPredicate sideCondition (Just initialCondition) conditional = do - partialResult <- - Simplifier.simplifyCondition - (sideCondition `SideCondition.andCondition` initialCondition) - conditional - -- TODO (virgil): Consider using different simplifyPredicate implementations - -- for rewrite rules and equational rules. - -- Right now this double simplification both allows using the same code for - -- both kinds of rules, and allows using the strongest background condition - -- for simplifying the `conditional`. However, it's not obvious that - -- using the strongest background condition actually helps in our - -- use cases, so we may be able to do something better for equations. - Simplifier.simplifyCondition - sideCondition - ( partialResult - `Pattern.andCondition` initialCondition - ) -simplifyPredicate sideCondition Nothing conditional = - Simplifier.simplifyCondition - sideCondition - conditional From 15b1f36a9c957a513e1ced1017cb38178e99ea05 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 15:35:12 -0500 Subject: [PATCH 20/25] Revert "applyRemainder: Inputs are simplified" This reverts commit 1d9750cf5961411ce9db773286ba1bfd7942059b. --- kore/src/Kore/Step/Step.hs | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index dee4e14557..7e8623b5c4 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -272,11 +272,6 @@ toConfigurationVariablesCondition = {- | Apply the remainder predicate to the given initial configuration. -@applyRemainder@ assumes that the unification solution used to construct the -remainders was simplified with respect to the initial conditions before the -remainder was constructed, and therefore the remainder does not need to be -re-simplified. - -} applyRemainder :: forall simplifier variable @@ -287,9 +282,17 @@ applyRemainder -> Condition variable -- ^ Remainder -> BranchT simplifier (Pattern variable) -applyRemainder initial remainder = +applyRemainder initial remainder = do + -- Simplify the remainder predicate under the initial conditions. We must + -- ensure that functions in the remainder are evaluated using the top-level + -- side conditions because we will not re-evaluate them after they are added + -- to the top level. + partial <- + Simplifier.simplifyCondition + (SideCondition.fromCondition $ Pattern.withoutTerm initial) + remainder -- Add the simplified remainder to the initial conditions. We must preserve - -- the initial conditions here, so it cannot be used as the side condition! + -- the initial conditions here! Simplifier.simplifyCondition SideCondition.topTODO - (Pattern.andCondition initial remainder) + (Pattern.andCondition initial partial) From 0a92a831410cc30c54bdf0a8946001d5a7906f4c Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 13 May 2020 13:52:02 -0500 Subject: [PATCH 21/25] Dockerfile: Update Z3 --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index e287c793e5..86e0b47683 100644 --- a/Dockerfile +++ b/Dockerfile @@ -13,7 +13,7 @@ RUN apt update pkg-config python3 python-pygments python-recommonmark python-sphinx \ time zlib1g-dev -RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.6.0 \ +RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.8 \ && cd z3 \ && python scripts/mk_make.py \ && cd build \ From af6f8212ed3e3d5b5c3ad9a67abb11a6d0c45a77 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 14 May 2020 15:50:07 -0500 Subject: [PATCH 22/25] Revert "Dockerfile: Update Z3" This reverts commit 0a92a831410cc30c54bdf0a8946001d5a7906f4c. --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 86e0b47683..e287c793e5 100644 --- a/Dockerfile +++ b/Dockerfile @@ -13,7 +13,7 @@ RUN apt update pkg-config python3 python-pygments python-recommonmark python-sphinx \ time zlib1g-dev -RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.8 \ +RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.6.0 \ && cd z3 \ && python scripts/mk_make.py \ && cd build \ From 42583c5701929dc375569f31042ec5deff1f4d0d Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Mon, 18 May 2020 16:00:21 +0300 Subject: [PATCH 23/25] Line length --- kore/test/Test/Kore/Strategies/OnePath/Step.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Strategies/OnePath/Step.hs b/kore/test/Test/Kore/Strategies/OnePath/Step.hs index d142c368db..1d806cf2fa 100644 --- a/kore/test/Test/Kore/Strategies/OnePath/Step.hs +++ b/kore/test/Test/Kore/Strategies/OnePath/Step.hs @@ -847,7 +847,11 @@ runSteps breadthLimit graphFilter picker configuration strategy' = give metadataTools $ declareSMTLemmas $ indexedModuleWithDefaultImports (ModuleName "TestModule") Nothing - runStrategy breadthLimit transitionRule strategy' (ProofState.Goal configuration) + runStrategy + breadthLimit + transitionRule + strategy' + (ProofState.Goal configuration) where mockEnv = Mock.env Env {metadataTools} = mockEnv From e5c8dbb7c98c19b4b64ba751dc3cd8f0b16f57fe Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 18 May 2020 09:33:54 -0500 Subject: [PATCH 24/25] test_onePathStrategy: removeDestination simplifies stuck configuration --- .../test/Test/Kore/Strategies/OnePath/Step.hs | 46 ++++++++++--------- 1 file changed, 25 insertions(+), 21 deletions(-) diff --git a/kore/test/Test/Kore/Strategies/OnePath/Step.hs b/kore/test/Test/Kore/Strategies/OnePath/Step.hs index 1d806cf2fa..7d46ea107f 100644 --- a/kore/test/Test/Kore/Strategies/OnePath/Step.hs +++ b/kore/test/Test/Kore/Strategies/OnePath/Step.hs @@ -80,6 +80,7 @@ import Kore.Syntax.Module import Kore.Syntax.Variable ( Variable (..) ) +import Kore.Variables.UnifiedVariable import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Simplification @@ -749,34 +750,37 @@ test_onePathStrategy = -- Coinductive axiom: - -- Normal axiom: - -- Expected: stuck, since the terms unify but the conditions do not - let goal = - makeOnePathRuleFromPatterns - ( Conditional - { term = TermLike.mkElemVar Mock.x - , predicate = - makeEqualsPredicate Mock.testSort - (TermLike.mkElemVar Mock.x) - Mock.a - , substitution = mempty - } + let left = + Pattern.withCondition + (TermLike.mkElemVar Mock.x) + (Condition.fromPredicate + (makeEqualsPredicate Mock.testSort + (TermLike.mkElemVar Mock.x) + Mock.a + ) ) - ( Conditional - { term = TermLike.mkElemVar Mock.x - , predicate = - makeNotPredicate - $ makeEqualsPredicate Mock.testSort - (TermLike.mkElemVar Mock.x) - Mock.a - , substitution = mempty - } + left' = + Pattern.withCondition + Mock.a + (Condition.assign (ElemVar Mock.x) Mock.a) + right = + Pattern.withCondition + (TermLike.mkElemVar Mock.x) + (Condition.fromPredicate $ makeNotPredicate + (makeEqualsPredicate Mock.testSort + (TermLike.mkElemVar Mock.x) + Mock.a + ) ) + original = makeOnePathRuleFromPatterns left right + expect = makeOnePathRuleFromPatterns left' right [ _actual ] <- runOnePathSteps Unlimited (Limit 1) - goal + original [] [] - assertEqual "" (ProofState.GoalStuck goal) _actual + assertEqual "" (ProofState.GoalStuck expect) _actual ] simpleRewrite From 2e6ebf6a8177676ebed2ae365762436f47c90919 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Tue, 19 May 2020 21:18:04 +0300 Subject: [PATCH 25/25] rebuild