From 181f71a9551f5a6ea1cfb7260e7e84c924e0bff7 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 19 Jun 2020 13:00:30 +0300 Subject: [PATCH 1/4] Do not rename SideCondition variables when applying equations --- kore/src/Kore/Equation/Application.hs | 24 +++++++++---------- .../src/Kore/Step/Axiom/EvaluationStrategy.hs | 12 ++-------- kore/test/Test/Kore/Equation/Application.hs | 7 +----- 3 files changed, 14 insertions(+), 29 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index cff1f29333..1168b9b297 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -154,7 +154,7 @@ attemptEquation . HasCallStack => MonadSimplify simplifier => InternalVariable variable - => SideCondition (Target variable) + => SideCondition variable -> TermLike (Target variable) -> Equation variable -> simplifier (AttemptEquationResult variable) @@ -228,7 +228,7 @@ attemptEquation sideCondition termLike equation = let toMatchResult Conditional { predicate, substitution } = (predicate, Substitution.toMap substitution) Substitution.mergePredicatesAndSubstitutions - sideCondition + SideCondition.top ([argument, matchPredicate] <> maybeToList antiLeft) [from @_ @(Substitution _) matchSubstitution] & Logic.observeAllT @@ -333,7 +333,7 @@ checkRequires :: forall simplifier variable . MonadSimplify simplifier => InternalVariable variable - => SideCondition (Target variable) + => SideCondition variable -> Predicate variable -- ^ requires from matching -> Predicate variable -- ^ requires from 'Equation' -> ExceptT (CheckRequiresError variable) simplifier () @@ -357,13 +357,7 @@ checkRequires sideCondition predicate requires = -- and the rule will not be applied. & (OrCondition.observeAllT >=> assertBottom) where - simplifyCondition = Simplifier.simplifyCondition sideCondition' - - -- TODO (thomas.tuegel): Do not unwrap sideCondition. - sideCondition' = - SideCondition.mapVariables - (pure Target.unTarget) - sideCondition + simplifyCondition = Simplifier.simplifyCondition sideCondition assertBottom orCondition | isBottom orCondition = done @@ -376,7 +370,7 @@ checkRequires sideCondition predicate requires = } -- Pair a configuration with sideCondition for evaluation by the solver. - withSideCondition = (,) sideCondition' + withSideCondition = (,) sideCondition withoutAxioms = fmap Condition.forgetSimplified @@ -392,7 +386,7 @@ The variables are marked 'Target' and renamed to avoid any variables in the targetEquationVariables :: forall variable . InternalVariable variable - => SideCondition (Target variable) + => SideCondition variable -> TermLike (Target variable) -> Equation variable -> Equation (Target variable) @@ -401,7 +395,11 @@ targetEquationVariables sideCondition initial = . Equation.refreshVariables avoiding . Equation.mapVariables Target.mkUnifiedTarget where - avoiding = freeVariables sideCondition <> freeVariables initial + avoiding = sideConditionVariables <> freeVariables initial + sideConditionVariables = + FreeVariables.mapFreeVariables + Target.mkUnifiedNonTarget + $ freeVariables sideCondition -- * Errors diff --git a/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs b/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs index d9f0f06894..36d5f709f5 100644 --- a/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs +++ b/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs @@ -79,13 +79,9 @@ definitionEvaluation equations = Equation.mapVariables (pure fromVariableName) <$> equations term' = TermLike.mapVariables Target.mkUnifiedNonTarget term - condition' = - SideCondition.mapVariables - Target.mkUnifiedNonTarget - condition let -- Attempt an equation, pairing it with its result, if applicable. attemptEquation equation = - Equation.attemptEquation condition' term' equation + Equation.attemptEquation condition term' equation >>= return . Bifunctor.second apply where apply = Equation.applyEquation condition equation @@ -117,11 +113,7 @@ simplificationEvaluation equation = BuiltinAndAxiomSimplifier $ \term condition -> do let equation' = Equation.mapVariables (pure fromVariableName) equation term' = TermLike.mapVariables Target.mkUnifiedNonTarget term - condition' = - SideCondition.mapVariables - Target.mkUnifiedNonTarget - condition - result <- Equation.attemptEquation condition' term' equation' + result <- Equation.attemptEquation condition term' equation' let apply = Equation.applyEquation condition equation' case result of Right applied -> do diff --git a/kore/test/Test/Kore/Equation/Application.hs b/kore/test/Test/Kore/Equation/Application.hs index 0b75d28363..479cf9a51c 100644 --- a/kore/test/Test/Kore/Equation/Application.hs +++ b/kore/test/Test/Kore/Equation/Application.hs @@ -69,14 +69,9 @@ attemptEquation -> Equation' -> IO AttemptEquationResult' attemptEquation sideCondition termLike equation = - Equation.attemptEquation sideCondition' termLike' equation + Equation.attemptEquation sideCondition termLike' equation & runSimplifier Mock.env where - sideCondition' = - SideCondition.mapVariables - Target.mkUnifiedNonTarget - sideCondition - termLike' = TermLike.mapVariables Target.mkUnifiedNonTarget termLike assertNotMatched :: AttemptEquationError' -> Assertion From c6c157b663f578b09c67071dbe0b08f14980d79a Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 22 Jun 2020 17:44:38 +0300 Subject: [PATCH 2/4] Do not simplify matchPredicate when applying substitution --- kore/src/Kore/Equation/Application.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 1168b9b297..11de624c9e 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -222,14 +222,14 @@ attemptEquation sideCondition termLike equation = simplifyArgumentWithResult argument antiLeft - (matchPredicate, matchSubstitution) + (_, matchSubstitution) = lift $ do let toMatchResult Conditional { predicate, substitution } = (predicate, Substitution.toMap substitution) Substitution.mergePredicatesAndSubstitutions SideCondition.top - ([argument, matchPredicate] <> maybeToList antiLeft) + (argument : maybeToList antiLeft) [from @_ @(Substitution _) matchSubstitution] & Logic.observeAllT & (fmap . fmap) toMatchResult From 8079ac0088b2aa883d93b6b2a72e3f38a81bfbb0 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 23 Jun 2020 11:34:05 +0300 Subject: [PATCH 3/4] Address review comments --- kore/src/Kore/Equation/Application.hs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 11de624c9e..91f8d8b29f 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -41,6 +41,9 @@ import qualified Data.Foldable as Foldable import Data.List.NonEmpty ( NonEmpty (..) ) +import Data.Map.Strict + ( Map + ) import qualified Data.Map.Strict as Map import Data.Set ( Set @@ -170,8 +173,8 @@ attemptEquation sideCondition termLike equation = Just argument' -> do matchResults <- whileMatch - $ match left termLike - >>= simplifyArgumentWithResult argument' antiLeft + $ (match left termLike & fmap snd) + >>= applySubstitutionAndSimplify argument' antiLeft applyAndSelectMatchResult matchResults let Equation { requires } = equation' checkRequires sideCondition predicate requires & whileCheckRequires @@ -210,19 +213,19 @@ attemptEquation sideCondition termLike equation = debugAttemptEquationResult equation result return result - simplifyArgumentWithResult + applySubstitutionAndSimplify :: HasCallStack => Predicate (Target variable) -> Maybe (Predicate (Target variable)) - -> MatchResult (Target variable) + -> Map (SomeVariableName (Target variable)) (TermLike (Target variable)) -> ExceptT (MatchError (Target variable)) simplifier [MatchResult (Target variable)] - simplifyArgumentWithResult + applySubstitutionAndSimplify argument antiLeft - (_, matchSubstitution) + matchSubstitution = lift $ do let toMatchResult Conditional { predicate, substitution } = From f5f755d14352e82e556faf5c777339b58511ac87 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 23 Jun 2020 14:44:23 +0300 Subject: [PATCH 4/4] Use matchPredicate in checkRequires --- kore/src/Kore/Equation/Application.hs | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 91f8d8b29f..926bb2c32d 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -171,11 +171,25 @@ attemptEquation sideCondition termLike equation = applyMatchResult equationRenamed matchResult & whileApplyMatchResult Just argument' -> do + (matchPredicate, matchSubstitution) <- + match left termLike + & whileMatch matchResults <- - whileMatch - $ (match left termLike & fmap snd) - >>= applySubstitutionAndSimplify argument' antiLeft - applyAndSelectMatchResult matchResults + applySubstitutionAndSimplify + argument' + antiLeft + matchSubstitution + & whileMatch + (equation', predicate) <- + applyAndSelectMatchResult matchResults + let matchPredicate' = + Predicate.mapVariables + (pure Target.unTarget) + matchPredicate + return + ( equation' + , makeAndPredicate predicate matchPredicate' + ) let Equation { requires } = equation' checkRequires sideCondition predicate requires & whileCheckRequires let Equation { right, ensures } = equation'