From 65cb367345792f16ac0c21fced5d25a9bd45e03c Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 15 Jul 2020 14:35:16 -0500 Subject: [PATCH 01/28] inferDefined': mark configuration defined --- kore/src/Kore/Strategies/Goal.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs index 23b84e5132..e89284aee6 100644 --- a/kore/src/Kore/Strategies/Goal.hs +++ b/kore/src/Kore/Strategies/Goal.hs @@ -94,6 +94,7 @@ import Kore.Internal.Symbol ) import Kore.Internal.TermLike ( isFunctionPattern + , mkDefined , mkIn , termLikeSort ) @@ -705,7 +706,7 @@ inferDefined' inferDefined' lensRulePattern = Lens.traverseOf (lensRulePattern . RulePattern.leftPattern) $ \config -> do let definedConfig = - Pattern.andCondition config + Pattern.andCondition (mkDefined <$> config) $ from $ makeCeilPredicate_ (Conditional.term config) configs <- simplifyTopConfiguration definedConfig From 999362d72e66a754ccbd56e0f1d0a7bb44036130 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 16 Jul 2020 09:09:40 -0500 Subject: [PATCH 02/28] transitionRule: Apply InferDefined to all rewritable goals --- kore/src/Kore/Strategies/Goal.hs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs index e89284aee6..623233dd0a 100644 --- a/kore/src/Kore/Strategies/Goal.hs +++ b/kore/src/Kore/Strategies/Goal.hs @@ -516,6 +516,12 @@ transitionRule claims axiomGroups = transitionRuleWorker transitionRuleWorker Simplify (GoalRemainder goal) = GoalRemainder <$> simplify goal + transitionRuleWorker InferDefined (Goal goal) = do + results <- tryTransitionT (inferDefined goal) + case results of + [] -> return Proven + _ -> Goal <$> Transition.scatter results + transitionRuleWorker InferDefined (GoalRemainder goal) = do results <- tryTransitionT (inferDefined goal) case results of From 5bb65b6c04e830ad50dc5e5247977923f0f87aa7 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 16 Jul 2020 09:11:04 -0500 Subject: [PATCH 03/28] AndTerms: Add unifyDefined --- kore/src/Kore/Step/Simplification/AndTerms.hs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index e4b9e19a22..1a2ce4db4a 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -246,6 +246,7 @@ andEqualsFunctions notSimplifier = , (BothT, \_ _ _ -> domainValueAndConstructorErrors) , (BothT, \_ _ _ -> domainValueAndEqualsAssumesDifferent) , (BothT, \_ _ _ -> stringLiteralAndEqualsAssumesDifferent) + , (BothT, \_ _ s -> unifyDefined s) , (AndT, \_ _ _ t1 t2 -> Error.hoistMaybe $ functionAnd t1 t2) ] @@ -723,3 +724,17 @@ bytesDifferent | bytesFirst /= bytesSecond = return Pattern.bottom bytesDifferent _ _ = empty + +{- | Unwrap a 'Defined' term if it is not handled elsewhere. + -} +unifyDefined + :: MonadUnify unifier + => TermSimplifier variable unifier + -> TermLike variable + -> TermLike variable + -> MaybeT unifier (Pattern variable) +unifyDefined unifyChildren (Defined_ term1) term2 = + lift $ unifyChildren term1 term2 +unifyDefined unifyChildren term1 (Defined_ term2) = + lift $ unifyChildren term1 term2 +unifyDefined _ _ _ = empty From 9e17258623a26baa0b1b0daa7cbb3fb4d5d06d62 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 16:06:58 -0500 Subject: [PATCH 04/28] Kore.Internal.TermLike.unDefined --- kore/src/Kore/Internal/TermLike.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index dfb50c2d32..8f818c88bc 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -90,6 +90,7 @@ module Kore.Internal.TermLike , mkEndianness , mkSignedness , mkDefined + , unDefined -- * Predicate constructors , mkBottom_ , mkCeil_ @@ -1557,6 +1558,14 @@ mkDefined = updateCallStack . worker mkDefinedAtTop :: Ord variable => TermLike variable -> TermLike variable mkDefinedAtTop = synthesize . DefinedF . Defined +unDefined :: TermLike variable -> TermLike variable +unDefined = + Recursive.unfold $ \termLike -> + let attrs :< termLikeF = Recursive.project termLike in + case termLikeF of + DefinedF defined -> Recursive.project (getDefined defined) + _ -> attrs :< termLikeF + {- | Construct an 'Endianness' pattern. -} mkEndianness From b3ef4bba4932aa32504cb8c5b5800eba2236b6f5 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 16:06:32 -0500 Subject: [PATCH 05/28] equalAndEquals: Ignore Defined terms --- kore/src/Kore/Step/Simplification/AndTerms.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index 1a2ce4db4a..69f96b0779 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -331,7 +331,7 @@ equalAndEquals -> TermLike variable -> MaybeT unifier (Pattern variable) equalAndEquals first second - | first == second = + | unDefined first == unDefined second = return (Pattern.fromTermLike first) equalAndEquals _ _ = empty From dd674001ababe629ca64a3e6d0420aaadd8497fc Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 16:06:46 -0500 Subject: [PATCH 06/28] unifyDefined --- kore/src/Kore/Step/Simplification/AndTerms.hs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index 69f96b0779..5764ab5731 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -733,8 +733,7 @@ unifyDefined -> TermLike variable -> TermLike variable -> MaybeT unifier (Pattern variable) -unifyDefined unifyChildren (Defined_ term1) term2 = - lift $ unifyChildren term1 term2 -unifyDefined unifyChildren term1 (Defined_ term2) = - lift $ unifyChildren term1 term2 -unifyDefined _ _ _ = empty +unifyDefined unifyChildren term1 term2 + | Defined_ child1 <- term1 = lift $ unifyChildren child1 term2 + | Defined_ child2 <- term2 = lift $ unifyChildren term1 child2 + | otherwise = empty From 435decff1c3a3da7573b822de76508a978bb783c Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 16:06:52 -0500 Subject: [PATCH 07/28] matchDefined --- kore/src/Kore/Step/Axiom/Matcher.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/kore/src/Kore/Step/Axiom/Matcher.hs b/kore/src/Kore/Step/Axiom/Matcher.hs index c51b8db124..3a62546a35 100644 --- a/kore/src/Kore/Step/Axiom/Matcher.hs +++ b/kore/src/Kore/Step/Axiom/Matcher.hs @@ -171,6 +171,7 @@ matchOne pair = <|> matchBuiltinSet pair <|> matchInj pair <|> matchOverload pair + <|> matchDefined pair ) & Error.maybeT (defer pair) return @@ -408,6 +409,15 @@ matchOverload -> MaybeT (MatcherT variable simplifier) () matchOverload termPair = Error.hushT (matchOverloading termPair) >>= push +matchDefined + :: (MatchingVariable variable, MonadSimplify simplifier) + => Pair (TermLike variable) + -> MaybeT (MatcherT variable simplifier) () +matchDefined (Pair term1 term2) + | Defined_ def1 <- term1 = push (Pair def1 term2) + | Defined_ def2 <- term2 = push (Pair term1 def2) + | otherwise = empty + -- * Implementation type MatchingVariable variable = InternalVariable variable From f8a1536f5559257046704f14663a47a8d708daa7 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 21 Jul 2020 11:13:27 -0500 Subject: [PATCH 08/28] equalsAndEquals: Prefer the term which is defined --- kore/src/Kore/Step/Simplification/AndTerms.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index 5764ab5731..a1c250c7f7 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -332,7 +332,7 @@ equalAndEquals -> MaybeT unifier (Pattern variable) equalAndEquals first second | unDefined first == unDefined second = - return (Pattern.fromTermLike first) + return (Pattern.fromTermLike $ if isDefinedPattern second then second else first) equalAndEquals _ _ = empty -- | Unify two patterns where the first is @\\bottom@. From 1d1eb6f5f20853c1616f25c4738ac19a3883c67d Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sat, 25 Jul 2020 15:49:41 -0500 Subject: [PATCH 09/28] functionAnd: Fix predicate sort The predicate sort should be synchronized with the term sort. --- .../Kore/Builtin/AssociativeCommutative.hs | 2 +- kore/src/Kore/Step/Simplification/AndTerms.hs | 18 +- kore/test/Test/Kore/Builtin/Set.hs | 12 +- .../test/Test/Kore/Step/Simplification/And.hs | 17 +- .../Test/Kore/Step/Simplification/AndTerms.hs | 268 ++++++++---------- .../Test/Kore/Step/Simplification/Equals.hs | 18 +- kore/test/Test/Kore/Unification/Unifier.hs | 21 +- 7 files changed, 159 insertions(+), 197 deletions(-) diff --git a/kore/src/Kore/Builtin/AssociativeCommutative.hs b/kore/src/Kore/Builtin/AssociativeCommutative.hs index c44509a064..8dddac3712 100644 --- a/kore/src/Kore/Builtin/AssociativeCommutative.hs +++ b/kore/src/Kore/Builtin/AssociativeCommutative.hs @@ -767,7 +767,7 @@ unifyEqualsNormalized (unzip . Map.toList) (Domain.concreteElements unwrapped) - return (unifierTerm `withCondition` unifierCondition) + return (unifierTerm `Pattern.withCondition` unifierCondition) where sort1 = termLikeSort first diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index a1c250c7f7..54470600b5 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -700,16 +700,14 @@ functionAnd -> Maybe (Pattern variable) functionAnd first second | isFunctionPattern first, isFunctionPattern second = - return Conditional - { term = first -- different for Equals - -- Ceil predicate not needed since first being - -- bottom will make the entire term bottom. However, - -- one must be careful to not just drop the term. - , predicate = - Predicate.markSimplified - $ makeEqualsPredicate_ first second - , substitution = mempty - } + makeEqualsPredicate_ first second + & Predicate.markSimplified + -- Ceil predicate not needed since first being + -- bottom will make the entire term bottom. However, + -- one must be careful to not just drop the term. + & Condition.fromPredicate + & Pattern.withCondition first -- different for Equals + & pure | otherwise = empty bytesDifferent diff --git a/kore/test/Test/Kore/Builtin/Set.hs b/kore/test/Test/Kore/Builtin/Set.hs index 11bc7fa029..5207c80115 100644 --- a/kore/test/Test/Kore/Builtin/Set.hs +++ b/kore/test/Test/Kore/Builtin/Set.hs @@ -120,6 +120,7 @@ import SMT ( SMT ) +import Test.Expect import Test.Kore ( elementVariableGen , standaloneGen @@ -1832,15 +1833,16 @@ unifiedBy -> [(SomeVariable VariableName, TermLike VariableName)] -> TestName -> TestTree -unifiedBy (termLike1, termLike2) substitution testName = +unifiedBy (termLike1, termLike2) (Substitution.unsafeWrap -> expect) testName = testCase testName $ do - actual <- + actuals <- runSimplifier testEnv $ runUnifierT Not.notSimplifier $ termUnification Not.notSimplifier termLike1 termLike2 - liftIO $ assertEqual "" [expect] (Pattern.withoutTerm <$> actual) - where - expect = Condition.fromSubstitution $ Substitution.unsafeWrap substitution + liftIO $ do + actual <- expectOne actuals + assertBool "expected \\top predicate" (isTop $ predicate actual) + assertEqual "" expect (substitution actual) -- | Specialize 'Set.asTermLike' to the builtin sort 'setSort'. asTermLike diff --git a/kore/test/Test/Kore/Step/Simplification/And.hs b/kore/test/Test/Kore/Step/Simplification/And.hs index 073d42a309..fa0ff92a7d 100644 --- a/kore/test/Test/Kore/Step/Simplification/And.hs +++ b/kore/test/Test/Kore/Step/Simplification/And.hs @@ -6,6 +6,7 @@ import Prelude.Kore import Test.Tasty +import qualified Kore.Internal.Condition as Condition import Kore.Internal.MultiOr ( MultiOr (MultiOr) ) @@ -99,11 +100,9 @@ test_andSimplification = , testCase "And function terms" $ do let expect = - Conditional - { term = fOfX - , predicate = makeEqualsPredicate_ fOfX gOfX - , substitution = mempty - } + makeEqualsPredicate_ fOfX gOfX + & Condition.fromPredicate + & Pattern.withCondition fOfX actual <- evaluatePatterns fOfXExpanded gOfXExpanded assertEqual "" (OrPattern.fromPatterns [expect]) actual @@ -332,11 +331,9 @@ test_andSimplification = , testCase "And-Or distribution" $ do let expect = OrPattern.fromPatterns - [ Conditional - { term = fOfX - , predicate = makeEqualsPredicate_ fOfX gOfX - , substitution = mempty - } + [ makeEqualsPredicate_ fOfX gOfX + & Condition.fromPredicate + & Pattern.withCondition fOfX , Conditional { term = fOfX , predicate = makeCeilPredicate Mock.testSort gOfX diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 9a5dec41fc..e94cc1e88b 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -32,7 +32,6 @@ import Kore.Internal.Predicate , makeEqualsPredicate , makeEqualsPredicate_ , makeTruePredicate - , makeTruePredicate_ ) import Kore.Internal.SideCondition ( SideCondition @@ -519,15 +518,12 @@ test_andTermsSimplification = , testCase "not equal values" $ do let expect = - let - expanded = Conditional - { term = fOfA - , predicate = makeEqualsPredicate_ fOfA gOfA - , substitution = mempty - } - in ([expanded], [expanded]) - actual <- simplifyUnify fOfA gOfA - assertEqual "" expect actual + makeEqualsPredicate_ fOfA gOfA + & Condition.fromPredicate + & Pattern.withCondition fOfA + (actualAnd, actualUnify) <- simplifyUnify fOfA gOfA + assertEqual "" [expect] actualAnd + assertEqual "" [expect] actualUnify ] , testGroup "unhandled cases" @@ -597,12 +593,9 @@ test_andTermsSimplification = , testGroup "builtin Map domain" [ testCase "concrete Map, same keys" $ do let expect = - [ Conditional - { term = Mock.builtinMap [(Mock.a, Mock.b)] - , predicate = makeTruePredicate_ - , substitution = - Substitution.unsafeWrap [(inject Mock.x, Mock.b)] - } + [ Pattern.withCondition + (Mock.builtinMap [(Mock.a, Mock.b)]) + (Condition.assign (inject Mock.x) Mock.b) ] actual <- unify @@ -620,16 +613,14 @@ test_andTermsSimplification = , testCase "concrete Map with framed Map" $ do let expect = - [ Conditional - { term = - Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)] - , predicate = makeTruePredicate_ - , substitution = Substitution.wrap - $ Substitution.mkUnwrappedSubstitution - [ (inject Mock.x, fOfA) - , (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)]) + [ Pattern.withCondition + (Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)]) + (mconcat + [ Condition.assign (inject Mock.x) fOfA + , Condition.assign (inject Mock.m) + (Mock.builtinMap [(Mock.b, fOfB)]) ] - } + ) ] actual <- unify @@ -642,16 +633,14 @@ test_andTermsSimplification = , testCase "concrete Map with framed Map" $ do let expect = - [ Conditional - { term = - Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)] - , predicate = makeTruePredicate_ - , substitution = Substitution.wrap - $ Substitution.mkUnwrappedSubstitution - [ (inject Mock.x, fOfA) - , (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)]) + [ Pattern.withCondition + (Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)]) + (mconcat + [ Condition.assign (inject Mock.x) fOfA + , Condition.assign (inject Mock.m) + (Mock.builtinMap [(Mock.b, fOfB)]) ] - } + ) ] actual <- unify @@ -664,16 +653,14 @@ test_andTermsSimplification = , testCase "framed Map with concrete Map" $ do let expect = - [ Conditional - { term = - Mock.builtinMap [(Mock.a, fOfA) , (Mock.b, fOfB)] - , predicate = makeTruePredicate_ - , substitution = Substitution.wrap - $ Substitution.mkUnwrappedSubstitution - [ (inject Mock.x, fOfA) - , (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)]) + [ Pattern.withCondition + (Mock.builtinMap [(Mock.a, fOfA) , (Mock.b, fOfB)]) + (mconcat + [ Condition.assign (inject Mock.x) fOfA + , Condition.assign (inject Mock.m) + (Mock.builtinMap [(Mock.b, fOfB)]) ] - } + ) ] actual <- unify @@ -686,16 +673,14 @@ test_andTermsSimplification = , testCase "framed Map with concrete Map" $ do let expect = - [ Conditional - { term = - Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)] - , predicate = makeTruePredicate_ - , substitution = Substitution.wrap - $ Substitution.mkUnwrappedSubstitution - [ (inject Mock.x, fOfA) - , (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)]) + [ Pattern.withCondition + (Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)]) + (mconcat + [ Condition.assign (inject Mock.x) fOfA + , Condition.assign (inject Mock.m) + (Mock.builtinMap [(Mock.b, fOfB)]) ] - } + ) ] actual <- unify @@ -708,15 +693,13 @@ test_andTermsSimplification = , testCase "concrete Map with element+unit" $ do let expect = - [ Conditional - { term = Mock.builtinMap [ (Mock.a, fOfA) ] - , predicate = makeTruePredicate_ - , substitution = Substitution.wrap - $ Substitution.mkUnwrappedSubstitution - [ (inject Mock.x, Mock.a) - , (inject Mock.y, fOfA) + [ Pattern.withCondition + (Mock.builtinMap [(Mock.a, fOfA)]) + (mconcat + [ Condition.assign (inject Mock.x) Mock.a + , Condition.assign (inject Mock.y) fOfA ] - } + ) ] actual <- unify @@ -729,21 +712,20 @@ test_andTermsSimplification = , testCase "map elem key inj splitting" $ do let expected = - [ Conditional - { term = Mock.builtinMap + [ Pattern.withCondition + (Mock.builtinMap [ ( Mock.sortInjection Mock.testSort Mock.aSubSubsort , fOfA ) ] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ ( inject Mock.xSubSort - , Mock.sortInjectionSubSubToSub Mock.aSubSubsort - ) - , ( inject Mock.y, fOfA ) + ) + (mconcat + [ Condition.assign (inject Mock.xSubSort) + (Mock.sortInjectionSubSubToSub Mock.aSubSubsort) + , Condition.assign (inject Mock.y) fOfA ] - } + ) ] actual <- unify (Mock.builtinMap @@ -765,18 +747,17 @@ test_andTermsSimplification = valueInj = Mock.sortInjection Mock.testSort Mock.aSubSubsort testMapInj = Mock.builtinMap [(key, valueInj)] expected = - [ Conditional - { term = testMapInj - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ ( inject Mock.xSubSort - , Mock.sortInjection + [ Pattern.withCondition + testMapInj + (mconcat + [ Condition.assign (inject Mock.xSubSort) + ( Mock.sortInjection Mock.subSort Mock.aSubSubsort ) - , ( inject Mock.y, Mock.a ) + , Condition.assign (inject Mock.y) Mock.a ] - } + ) ] actual <- unify testMap @@ -788,22 +769,22 @@ test_andTermsSimplification = , testCase "map concat key inj splitting" $ do let expected = - [ Conditional - { term = Mock.builtinMap + [ Pattern.withCondition + (Mock.builtinMap [ ( Mock.sortInjection Mock.testSort Mock.aSubSubsort , fOfA ) ] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ ( inject Mock.xSubSort - , Mock.sortInjectionSubSubToSub Mock.aSubSubsort - ) - , ( inject Mock.y, fOfA ) - , ( inject Mock.m, Mock.builtinMap []) + ) + (mconcat + [ Condition.assign (inject Mock.xSubSort) + (Mock.sortInjectionSubSubToSub Mock.aSubSubsort) + , Condition.assign (inject Mock.y) fOfA + , Condition.assign (inject Mock.m) + (Mock.builtinMap []) ] - } + ) ] actual <- unify (Mock.builtinMap @@ -823,22 +804,21 @@ test_andTermsSimplification = , testCase "map elem value inj splitting" $ do let expected = - [ Conditional - { term = Mock.builtinMap + [ Pattern.withCondition + (Mock.builtinMap [ ( Mock.a , Mock.sortInjection Mock.testSort Mock.aSubSubsort ) ] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ ( inject Mock.xSubSort - , Mock.sortInjectionSubSubToSub Mock.aSubSubsort - ) - , ( inject Mock.y, Mock.a ) - , ( inject Mock.m, Mock.builtinMap []) + ) + (mconcat + [ Condition.assign (inject Mock.xSubSort) + (Mock.sortInjectionSubSubToSub Mock.aSubSubsort) + , Condition.assign (inject Mock.y) Mock.a + , Condition.assign (inject Mock.m) (Mock.builtinMap []) ] - } + ) ] actual <- unify (Mock.builtinMap @@ -948,12 +928,9 @@ test_andTermsSimplification = [ testCase "set singleton + unit" $ do let expected = - [ Conditional - { term = Mock.builtinSet [Mock.a] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ (inject Mock.x, Mock.a) ] - } + [ Pattern.withCondition + (Mock.builtinSet [Mock.a]) + (Condition.assign (inject Mock.x) Mock.a) ] actual <- unify (Mock.concatSet @@ -965,23 +942,21 @@ test_andTermsSimplification = , testCase "handles set ambiguity" $ do let expected1 = - Conditional - { term = Mock.builtinSet [Mock.a, Mock.b] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap + Pattern.withCondition + (Mock.builtinSet [Mock.a, Mock.b]) + (foldMap (uncurry Condition.assign) [ (inject Mock.x, Mock.a) , (inject Mock.xSet, Mock.builtinSet [Mock.b]) ] - } + ) expected2 = - Conditional - { term = Mock.builtinSet [Mock.a, Mock.b] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap + Pattern.withCondition + (Mock.builtinSet [Mock.a, Mock.b]) + (foldMap (uncurry Condition.assign) [ (inject Mock.x, Mock.b) , (inject Mock.xSet, Mock.builtinSet [Mock.a]) ] - } + ) actual <- unify (Mock.concatSet (Mock.elementSet (mkElemVar Mock.x)) @@ -992,16 +967,13 @@ test_andTermsSimplification = , testCase "set elem inj splitting" $ do let expected = - [ Conditional - { term = Mock.builtinSet - [ Mock.sortInjection Mock.testSort Mock.aSubSubsort ] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ ( inject Mock.xSubSort - , Mock.sortInjectionSubSubToSub Mock.aSubSubsort - ) - ] - } + [ Pattern.withCondition + (Mock.builtinSet + [Mock.sortInjection Mock.testSort Mock.aSubSubsort] + ) + (Condition.assign (inject Mock.xSubSort) + (Mock.sortInjectionSubSubToSub Mock.aSubSubsort) + ) ] actual <- unify (Mock.elementSet @@ -1014,11 +986,11 @@ test_andTermsSimplification = , testCase "set concat inj splitting" $ do let expected = - [ Conditional - { term = Mock.builtinSet - [ Mock.sortInjection Mock.testSort Mock.aSubSubsort ] - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap + [ Pattern.withCondition + (Mock.builtinSet + [Mock.sortInjection Mock.testSort Mock.aSubSubsort] + ) + (foldMap (uncurry Condition.assign) [ ( inject Mock.xSubSort , Mock.sortInjectionSubSubToSub Mock.aSubSubsort ) @@ -1026,7 +998,7 @@ test_andTermsSimplification = , Mock.builtinSet [] ) ] - } + ) ] actual <- unify (Mock.concatSet @@ -1047,18 +1019,15 @@ test_andTermsSimplification = , Mock.sortInjection Mock.testSort Mock.aSubSubsort ] expected = - [ Conditional - { term = testSet - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ (inject Mock.x, Mock.a) - , ( inject Mock.xSubSort - , Mock.sortInjectionSubSubToSub - Mock.aSubSubsort - ) - , (inject Mock.xSet, Mock.builtinSet []) - ] - } + [ Pattern.withCondition testSet + (foldMap (uncurry Condition.assign) + [ (inject Mock.x, Mock.a) + , ( inject Mock.xSubSort + , Mock.sortInjectionSubSubToSub Mock.aSubSubsort + ) + , (inject Mock.xSet, Mock.builtinSet []) + ] + ) ] actual <- unify (Mock.concatSet @@ -1207,16 +1176,13 @@ test_equalsTermsSimplification = [ (Mock.a, [Mock.b]) , (Mock.b, [Mock.a]) ] - return Conditional - { term = () - , predicate = makeTruePredicate_ - , substitution = Substitution.unsafeWrap - [ (inject Mock.x, xValue) - , ( inject Mock.xSet - , asInternal (Set.fromList xSetValue) - ) - ] - } + mconcat + [ Condition.assign (inject Mock.x) xValue + , Condition.assign (inject Mock.xSet) + (asInternal $ Set.fromList xSetValue) + ] + & Condition.coerceSort Mock.setSort + & pure actual <- simplifyEquals Map.empty (Mock.concatSet diff --git a/kore/test/Test/Kore/Step/Simplification/Equals.hs b/kore/test/Test/Kore/Step/Simplification/Equals.hs index 29be0cb25a..027e505892 100644 --- a/kore/test/Test/Kore/Step/Simplification/Equals.hs +++ b/kore/test/Test/Kore/Step/Simplification/Equals.hs @@ -704,7 +704,7 @@ test_equalsSimplification_TermLike = (assertTermEquals Conditional { term = () - , predicate = makeTruePredicate_ + , predicate = makeTruePredicate Mock.mapSort , substitution = Substitution.unsafeWrap [(inject Mock.x, Mock.b)] } @@ -723,8 +723,8 @@ test_equalsSimplification_TermLike = { term = () , predicate = makeAndPredicate - (makeCeilPredicate_ fOfB) - (makeCeilPredicate_ fOfA) + (makeCeilPredicate Mock.mapSort fOfB) + (makeCeilPredicate Mock.mapSort fOfA) , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution [ (inject Mock.x, fOfA) @@ -743,8 +743,8 @@ test_equalsSimplification_TermLike = { term = () , predicate = makeAndPredicate - (makeCeilPredicate_ fOfB) - (makeCeilPredicate_ fOfA) + (makeCeilPredicate Mock.mapSort fOfB) + (makeCeilPredicate Mock.mapSort fOfA) , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution [ (inject Mock.x, fOfA) @@ -763,8 +763,8 @@ test_equalsSimplification_TermLike = { term = () , predicate = makeAndPredicate - (makeCeilPredicate_ fOfB) - (makeCeilPredicate_ fOfA) + (makeCeilPredicate Mock.mapSort fOfB) + (makeCeilPredicate Mock.mapSort fOfA) , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution [ (inject Mock.x, fOfA) @@ -783,8 +783,8 @@ test_equalsSimplification_TermLike = { term = () , predicate = makeAndPredicate - (makeCeilPredicate_ fOfB) - (makeCeilPredicate_ fOfA) + (makeCeilPredicate Mock.mapSort fOfB) + (makeCeilPredicate Mock.mapSort fOfA) , substitution = Substitution.wrap $ Substitution.mkUnwrappedSubstitution [ (inject Mock.x, fOfA) diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index 9a0841e688..b8d76d67b4 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -20,6 +20,7 @@ import Data.Text ( Text ) +import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.MultiOr as MultiOr import qualified Kore.Internal.SideCondition as SideCondition ( top @@ -149,13 +150,11 @@ unificationResult :: UnificationResult -> TestPattern unificationResult UnificationResult { term, substitution, predicate } = - Conditional - { term - , predicate - , substitution = - Substitution.unsafeWrapFromAssignments - $ unificationSubstitution substitution - } + unificationSubstitution substitution + & Substitution.unsafeWrapFromAssignments + & Condition.fromSubstitution + & (<>) (Condition.fromPredicate predicate) + & Pattern.withCondition term newtype UnificationTerm = UnificationTerm TestTerm @@ -428,7 +427,7 @@ test_unification = [ UnificationResult { term = dv1 , substitution = [] - , predicate = makeEqualsPredicate_ dv1 a2 + , predicate = Predicate.makeEqualsPredicate Mock.testSort dv1 a2 } ] , testCase "Unmatching nonconstructor constant + domain value" $ @@ -438,7 +437,7 @@ test_unification = [ UnificationResult { term = a2 , substitution = [] - , predicate = makeEqualsPredicate_ a2 dv1 + , predicate = Predicate.makeEqualsPredicate Mock.testSort a2 dv1 } ] , testCase "non-functional pattern" $ @@ -480,7 +479,7 @@ test_unification = [ UnificationResult { term = a , substitution = [] - , predicate = makeEqualsPredicate_ a a2 + , predicate = Predicate.makeEqualsPredicate Mock.testSort a a2 } ] , testCase "non-constructor symbolHead left" $ @@ -490,7 +489,7 @@ test_unification = [ UnificationResult { term = a2 , substitution = [] - , predicate = makeEqualsPredicate_ a2 a + , predicate = Predicate.makeEqualsPredicate Mock.testSort a2 a } ] , testCase "nested a=a1 is bottom" $ From f37f6195a0369f4e8301e74ecb086dc90ad913cd Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 26 Jul 2020 11:15:04 -0500 Subject: [PATCH 10/28] updateConcreteElements: Use separate assertions for clearer errors --- kore/src/Kore/Builtin/AssociativeCommutative.hs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/kore/src/Kore/Builtin/AssociativeCommutative.hs b/kore/src/Kore/Builtin/AssociativeCommutative.hs index 8dddac3712..1c56b4d1f7 100644 --- a/kore/src/Kore/Builtin/AssociativeCommutative.hs +++ b/kore/src/Kore/Builtin/AssociativeCommutative.hs @@ -426,10 +426,9 @@ updateConcreteElements -> [(TermLike Concrete, value)] -> Maybe (Map (TermLike Concrete) value) updateConcreteElements elems newElems = - TermLike.assertConstructorLikeKeys allKeys - $ Foldable.foldrM (uncurry insertMissing) elems newElems - where - allKeys = Map.keys elems <> fmap fst newElems + Foldable.foldrM (uncurry insertMissing) elems newElems + & TermLike.assertConstructorLikeKeys (Map.keys elems) + & TermLike.assertConstructorLikeKeys (fst <$> newElems) {- | Sort the abstract elements. From e6d03d8bca76583c13dcd9e92f99fd7551f8c61b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sat, 25 Jul 2020 20:23:43 -0500 Subject: [PATCH 11/28] test_Defined --- .../Test/Kore/Step/Simplification/AndTerms.hs | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index e94cc1e88b..663c1037b0 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -4,6 +4,7 @@ module Test.Kore.Step.Simplification.AndTerms ( test_andTermsSimplification , test_equalsTermsSimplification , test_functionAnd + , test_Defined ) where import Prelude.Kore @@ -1208,6 +1209,86 @@ test_functionAnd = assertBool "" (Pattern.isSimplified sideRepresentation actual) ] +test_Defined :: [TestTree] +test_Defined = + [ testGroup "exact matching" $ + let partial = Mock.f Mock.a + defined = mkDefined partial + in + [ testCase "\\and" $ do + let expect = [Pattern.fromTermLike defined] + (actualAnd, actualUnify) <- simplifyUnify partial defined + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\equals" $ do + let expect = Just [Condition.topOf Mock.testSort] + actual <- simplifyEquals mempty partial defined + assertEqual "" expect actual + ] + , testGroup "variable with function" $ + let defined = mkDefined (Mock.f Mock.a) + variable = mkElemVar Mock.x + condition = + Condition.assign (inject Mock.x) defined + & Condition.coerceSort Mock.testSort + in + [ testCase "\\and" $ do + let expect = [Pattern.withCondition defined condition] + (actualAnd, actualUnify) <- simplifyUnify defined variable + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\equals" $ do + let expect = Just [condition] + actual <- simplifyEquals mempty defined variable + assertEqual "" expect actual + ] + , testGroup "functions" $ + let function1 = Mock.f Mock.a + function2 = Mock.g Mock.b + defined1 = mkDefined function1 + -- TODO (thomas.tuegel): condition should use defined1 instead of + -- function1. + condition = + makeEqualsPredicate_ function1 function2 + & Condition.fromPredicate + in + [ testCase "\\and" $ do + let expect = [Pattern.withCondition function1 condition] + (actualAnd, actualUnify) <- simplifyUnify defined1 function2 + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\equals" $ do + let expect = Just [condition] + actual <- simplifyEquals mempty defined1 function2 + assertEqual "" expect actual + ] + , testGroup "Sets" $ + let set1 = Mock.builtinSet [fOfA, fOfB] + set2 = Mock.builtinSet [mkElemVar Mock.x, mkElemVar Mock.y] + defined1 = mkDefined set1 + conditions = + [ mconcat + [ Condition.assign (inject Mock.x) fOfA + , Condition.assign (inject Mock.y) fOfB + ] + , mconcat + [ Condition.assign (inject Mock.x) fOfB + , Condition.assign (inject Mock.y) fOfA + ] + ] + in + [ testCase "\\and" $ do + let expect = Pattern.withCondition set1 <$> conditions + (actualAnd, actualUnify) <- simplifyUnify defined1 set2 + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\equals" $ do + let expect = Just conditions + actual <- simplifyEquals mempty defined1 set2 + assertEqual "" expect actual + ] + ] + fOfA :: TermLike VariableName fOfA = Mock.f Mock.a From ddd5ef0fd45e97e7a258ea5a27f9dfbe59537d70 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 12:17:26 -0500 Subject: [PATCH 12/28] RED test_Defined Sets --- .../Test/Kore/Step/Simplification/AndTerms.hs | 61 ++++++++++++++++--- 1 file changed, 52 insertions(+), 9 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 663c1037b0..4c1e5a087c 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1263,29 +1263,72 @@ test_Defined = assertEqual "" expect actual ] , testGroup "Sets" $ - let set1 = Mock.builtinSet [fOfA, fOfB] - set2 = Mock.builtinSet [mkElemVar Mock.x, mkElemVar Mock.y] + let fx = Mock.f (mkElemVar Mock.x) + fy = Mock.f (mkElemVar Mock.y) + set1 = Mock.builtinSet [fx, fy] + set2 = Mock.builtinSet [mkElemVar Mock.t, mkElemVar Mock.u] defined1 = mkDefined set1 conditions = + map (Condition.coerceSort Mock.setSort) [ mconcat - [ Condition.assign (inject Mock.x) fOfA - , Condition.assign (inject Mock.y) fOfB + [ Condition.assign (inject Mock.t) (mkDefined fx) + , Condition.assign (inject Mock.u) (mkDefined fy) ] , mconcat - [ Condition.assign (inject Mock.x) fOfB - , Condition.assign (inject Mock.y) fOfA + [ Condition.assign (inject Mock.t) (mkDefined fy) + , Condition.assign (inject Mock.u) (mkDefined fx) ] ] in - [ testCase "\\and" $ do - let expect = Pattern.withCondition set1 <$> conditions + [ testCase "\\and(defined, _)" $ do + let expect = Pattern.withCondition defined1 <$> conditions (actualAnd, actualUnify) <- simplifyUnify defined1 set2 assertEqual "" expect actualAnd assertEqual "" expect actualUnify - , testCase "\\equals" $ do + , testCase "\\and(_, defined)" $ do + let expect = Pattern.withCondition defined1 <$> conditions + (actualAnd, actualUnify) <- simplifyUnify set2 defined1 + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\equals(defined, _)" $ do let expect = Just conditions actual <- simplifyEquals mempty defined1 set2 assertEqual "" expect actual + , testCase "\\equals(_, defined)" $ do + let expect = Just conditions + actual <- simplifyEquals mempty set2 defined1 + assertEqual "" expect actual + ] + , testGroup "Maps" $ + let map1 = Mock.builtinMap [(mkElemVar Mock.x, fOfA)] + map2 = Mock.builtinMap [(mkElemVar Mock.x, mkElemVar Mock.y)] + defined1 = mkDefined map1 + conditions = + map (Condition.coerceSort Mock.mapSort) + [ mconcat + [ Condition.assign (inject Mock.x) Mock.a + , Condition.assign (inject Mock.y) (mkDefined fOfA) + ] + ] + in + [ testCase "\\and(defined, _)" $ do + let expect = Pattern.withCondition defined1 <$> conditions + (actualAnd, actualUnify) <- simplifyUnify defined1 map2 + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\and(_, defined)" $ do + let expect = Pattern.withCondition defined1 <$> conditions + (actualAnd, actualUnify) <- simplifyUnify map2 defined1 + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\equals(defined, _)" $ do + let expect = Just conditions + actual <- simplifyEquals mempty defined1 map2 + assertEqual "" expect actual + , testCase "\\equals(_, defined)" $ do + let expect = Just conditions + actual <- simplifyEquals mempty map2 defined1 + assertEqual "" expect actual ] ] From 827c5270c600c7c9d2be2aae352e6e2fb981b005 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 13:58:42 -0500 Subject: [PATCH 13/28] GRN test_Defined Sets --- kore/src/Kore/Step/Simplification/AndTerms.hs | 39 ++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index 54470600b5..14d34c68f5 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -241,7 +241,7 @@ andEqualsFunctions notSimplifier = , (BothT, \_ _ _ -> Builtin.Signedness.unifyEquals) , (BothT, \_ _ s -> Builtin.Map.unifyEquals s) , (EqualsT, \_ _ s -> Builtin.Map.unifyNotInKeys s notSimplifier) - , (BothT, \_ _ s -> Builtin.Set.unifyEquals s) + , (BothT, \_ _ s -> unifyDefinedModifier (Builtin.Set.unifyEquals s)) , (BothT, \_ t s -> Builtin.List.unifyEquals t s) , (BothT, \_ _ _ -> domainValueAndConstructorErrors) , (BothT, \_ _ _ -> domainValueAndEqualsAssumesDifferent) @@ -735,3 +735,40 @@ unifyDefined unifyChildren term1 term2 | Defined_ child1 <- term1 = lift $ unifyChildren child1 term2 | Defined_ child2 <- term2 = lift $ unifyChildren term1 child2 | otherwise = empty + +unifyDefinedModifier + :: InternalVariable variable + => Monad monad + => (TermLike variable -> TermLike variable -> monad (Pattern variable)) + -> TermLike variable + -> TermLike variable + -> monad (Pattern variable) +unifyDefinedModifier unify (Defined_ def1) (Defined_ def2) = do + unified <- unify def1 def2 + let Conditional { term } = unified + term' + | term == def1 || term == def2 + = mkDefined term + | otherwise = term + unified' = term' <$ unified + pure unified' +unifyDefinedModifier unify (Defined_ def1) term2 = do + unified <- unify def1 term2 + let Conditional { term } = unified + term' + | unDefined term == unDefined def1 + = mkDefined term + | otherwise = term + unified' = term' <$ unified + pure unified' +unifyDefinedModifier unify term1 (Defined_ def2) = do + unified <- unify term1 def2 + let Conditional { term } = unified + term' + | unDefined term == unDefined def2 + = mkDefined term + | otherwise = term + unified' = term' <$ unified + pure unified' +unifyDefinedModifier unify term1 term2 = + unify term1 term2 From 77888fc644a4f9317131192e2a2bcaa4a00fed2b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 13:59:00 -0500 Subject: [PATCH 14/28] RED test_Defined Maps --- .../Test/Kore/Step/Simplification/AndTerms.hs | 36 +++++++++++++------ 1 file changed, 26 insertions(+), 10 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 4c1e5a087c..8741fb32b0 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -14,6 +14,7 @@ import Test.Tasty import Control.Error ( MaybeT (..) ) +import qualified Data.List as List import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Text @@ -1300,35 +1301,50 @@ test_Defined = assertEqual "" expect actual ] , testGroup "Maps" $ - let map1 = Mock.builtinMap [(mkElemVar Mock.x, fOfA)] - map2 = Mock.builtinMap [(mkElemVar Mock.x, mkElemVar Mock.y)] + let map1 = + Mock.builtinMap + [ (mkElemVar Mock.x, fOfA) + , (mkElemVar Mock.y, fOfB) + ] + map2 = + Mock.framedMap + [(mkElemVar Mock.t, mkElemVar Mock.u)] + [mkElemVar Mock.m] defined1 = mkDefined map1 conditions = map (Condition.coerceSort Mock.mapSort) [ mconcat - [ Condition.assign (inject Mock.x) Mock.a - , Condition.assign (inject Mock.y) (mkDefined fOfA) + [ Condition.assign (inject Mock.t) (mkElemVar Mock.x) + , Condition.assign (inject Mock.u) (mkDefined fOfA) + , Condition.assign (inject Mock.m) + (Mock.builtinMap [(mkElemVar Mock.y, mkDefined fOfB)]) + ] + , mconcat + [ Condition.assign (inject Mock.t) (mkElemVar Mock.y) + , Condition.assign (inject Mock.u) (mkDefined fOfB) + , Condition.assign (inject Mock.m) + (Mock.builtinMap [(mkElemVar Mock.x, mkDefined fOfA)]) ] ] in [ testCase "\\and(defined, _)" $ do let expect = Pattern.withCondition defined1 <$> conditions (actualAnd, actualUnify) <- simplifyUnify defined1 map2 - assertEqual "" expect actualAnd - assertEqual "" expect actualUnify + assertEqual "" (List.sort expect) (List.sort actualAnd) + assertEqual "" (List.sort expect) (List.sort actualUnify) , testCase "\\and(_, defined)" $ do let expect = Pattern.withCondition defined1 <$> conditions (actualAnd, actualUnify) <- simplifyUnify map2 defined1 - assertEqual "" expect actualAnd - assertEqual "" expect actualUnify + assertEqual "" (List.sort expect) (List.sort actualAnd) + assertEqual "" (List.sort expect) (List.sort actualUnify) , testCase "\\equals(defined, _)" $ do let expect = Just conditions actual <- simplifyEquals mempty defined1 map2 - assertEqual "" expect actual + assertEqual "" (List.sort <$> expect) actual , testCase "\\equals(_, defined)" $ do let expect = Just conditions actual <- simplifyEquals mempty map2 defined1 - assertEqual "" expect actual + assertEqual "" (List.sort <$> expect) actual ] ] From 274472fba0d8e1bb88464f42a9070e4c8cdccead Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 13:59:06 -0500 Subject: [PATCH 15/28] GRN test_Defined Maps --- kore/src/Kore/Step/Simplification/AndTerms.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index 14d34c68f5..ac3dfa043e 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -239,7 +239,7 @@ andEqualsFunctions notSimplifier = , (AndT, \_ _ s -> Builtin.KEqual.unifyIfThenElse s) , (BothT, \_ _ _ -> Builtin.Endianness.unifyEquals) , (BothT, \_ _ _ -> Builtin.Signedness.unifyEquals) - , (BothT, \_ _ s -> Builtin.Map.unifyEquals s) + , (BothT, \_ _ s -> unifyDefinedModifier (Builtin.Map.unifyEquals s)) , (EqualsT, \_ _ s -> Builtin.Map.unifyNotInKeys s notSimplifier) , (BothT, \_ _ s -> unifyDefinedModifier (Builtin.Set.unifyEquals s)) , (BothT, \_ t s -> Builtin.List.unifyEquals t s) From 3675ff587b0c58804468a14a990b7eb8b86bfa74 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 15:25:33 -0500 Subject: [PATCH 16/28] Move InferDefined step into Simplify --- kore/src/Kore/Strategies/Goal.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs index 623233dd0a..c9b2223bb2 100644 --- a/kore/src/Kore/Strategies/Goal.hs +++ b/kore/src/Kore/Strategies/Goal.hs @@ -589,7 +589,6 @@ reachabilityFirstStep = , CheckGoalStuck , CheckGoalRemainder , Simplify - , InferDefined , TriviallyValid , CheckImplication , ApplyAxioms @@ -605,7 +604,6 @@ reachabilityNextStep = , CheckGoalStuck , CheckGoalRemainder , Simplify - , InferDefined , TriviallyValid , CheckImplication , ApplyClaims @@ -697,12 +695,14 @@ simplify' -> Strategy.TransitionT (Rule goal) m goal simplify' lensRulePattern = Lens.traverseOf (lensRulePattern . RulePattern.leftPattern) $ \config -> do + let definedConfig = + Pattern.andCondition (mkDefined <$> config) + $ from $ makeCeilPredicate_ (Conditional.term config) configs <- - simplifyTopConfiguration config >>= SMT.Evaluator.filterMultiOr + simplifyTopConfiguration definedConfig + >>= SMT.Evaluator.filterMultiOr & lift - if isBottom configs - then pure Pattern.bottom - else Foldable.asum (pure <$> configs) + Foldable.asum (pure <$> configs) inferDefined' :: MonadSimplify m From aab96520d2e643ca931a478502e6190632116859 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 15:29:54 -0500 Subject: [PATCH 17/28] Remove InferDefined step --- kore/src/Kore/Log/InfoReachability.hs | 1 - kore/src/Kore/Strategies/Goal.hs | 12 ------------ kore/src/Kore/Strategies/ProofState.hs | 6 +----- kore/test/Test/Kore/Strategies/AllPath/AllPath.hs | 14 -------------- 4 files changed, 1 insertion(+), 32 deletions(-) diff --git a/kore/src/Kore/Log/InfoReachability.hs b/kore/src/Kore/Log/InfoReachability.hs index e6a9381b7a..978da480bf 100644 --- a/kore/src/Kore/Log/InfoReachability.hs +++ b/kore/src/Kore/Log/InfoReachability.hs @@ -36,7 +36,6 @@ instance Entry InfoReachability where primDoc :: Prim -> Maybe (Doc ann) primDoc Simplify = Just "simplifying the claim" primDoc CheckImplication = Just "checking the implication" -primDoc InferDefined = Just "inferring that the configuration is defined" primDoc ApplyClaims = Just "applying claims" primDoc ApplyAxioms = Just "applying axioms" primDoc _ = Nothing diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs index c9b2223bb2..5931a1601d 100644 --- a/kore/src/Kore/Strategies/Goal.hs +++ b/kore/src/Kore/Strategies/Goal.hs @@ -516,18 +516,6 @@ transitionRule claims axiomGroups = transitionRuleWorker transitionRuleWorker Simplify (GoalRemainder goal) = GoalRemainder <$> simplify goal - transitionRuleWorker InferDefined (Goal goal) = do - results <- tryTransitionT (inferDefined goal) - case results of - [] -> return Proven - _ -> Goal <$> Transition.scatter results - - transitionRuleWorker InferDefined (GoalRemainder goal) = do - results <- tryTransitionT (inferDefined goal) - case results of - [] -> return Proven - _ -> GoalRemainder <$> Transition.scatter results - transitionRuleWorker CheckImplication (Goal goal) = do result <- checkImplication goal case result of diff --git a/kore/src/Kore/Strategies/ProofState.hs b/kore/src/Kore/Strategies/ProofState.hs index 735629dc93..8c7702ab86 100644 --- a/kore/src/Kore/Strategies/ProofState.hs +++ b/kore/src/Kore/Strategies/ProofState.hs @@ -39,9 +39,6 @@ data Prim | Simplify | CheckImplication -- ^ Check if the claim's implication is valid. - | InferDefined - -- ^ Infer that the left-hand side of the claim is defined. This is related - -- to 'CheckImplication', but separated as an optimization. | TriviallyValid | ApplyClaims | ApplyAxioms @@ -52,9 +49,8 @@ instance Pretty Prim where pretty CheckGoalRemainder = "Transition CheckGoalRemainder." pretty CheckGoalStuck = "Transition CheckGoalStuck." pretty ResetGoal = "Transition ResetGoal." - pretty Simplify = "Transition Simplify." + pretty Simplify = "simplify the claim" pretty CheckImplication = "Transition CheckImplication." - pretty InferDefined = "infer left-hand side is defined" pretty TriviallyValid = "Transition TriviallyValid." pretty ApplyClaims = "apply claims" pretty ApplyAxioms = "apply axioms" diff --git a/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs b/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs index b94430ddc0..9b869b116c 100644 --- a/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs +++ b/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs @@ -3,7 +3,6 @@ module Test.Kore.Strategies.AllPath.AllPath , test_transitionRule_CheckProven , test_transitionRule_CheckGoalRem , test_transitionRule_CheckImplication - , test_transitionRule_InferDefined , test_transitionRule_TriviallyValid , test_transitionRule_ApplyClaims , test_transitionRule_ApplyAxioms @@ -222,19 +221,6 @@ test_transitionRule_ApplyAxioms = -> TestTree derives rules = equals_ (run rules $ ProofState.GoalRemainder (A, C)) -test_transitionRule_InferDefined :: [TestTree] -test_transitionRule_InferDefined = - [ unmodified ProofState.Proven - , unmodified (ProofState.Goal (A, B)) - , unmodified (ProofState.GoalStuck (A, B)) - , ProofState.GoalRemainder (NotDef, B) `becomes` (ProofState.Proven, mempty) - ] - where - run = runTransitionRule [] [] ProofState.InferDefined - unmodified :: HasCallStack => ProofState -> TestTree - unmodified state = run state `equals_` [(state, mempty)] - becomes initial final = run initial `equals_` [final] - test_runStrategy :: [TestTree] test_runStrategy = [ [] `proves` (A, A) From 32b3d0957e7c0f6f68e39bdc9cf630103a77bfa0 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 15:30:28 -0500 Subject: [PATCH 18/28] Goal: Remove method inferDefined --- kore/src/Kore/Strategies/Goal.hs | 33 ------------------- .../Test/Kore/Strategies/AllPath/AllPath.hs | 4 --- 2 files changed, 37 deletions(-) diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs index 5931a1601d..df11770a67 100644 --- a/kore/src/Kore/Strategies/Goal.hs +++ b/kore/src/Kore/Strategies/Goal.hs @@ -203,11 +203,6 @@ class Goal goal where -- checkImplication. isTriviallyValid :: goal -> Bool - inferDefined - :: MonadSimplify m - => goal - -> Strategy.TransitionT (Rule goal) m goal - checkImplication :: MonadSimplify m => goal -> m (CheckImplicationResult goal) @@ -314,8 +309,6 @@ instance Goal OnePathRule where isTriviallyValid = isTriviallyValid' _Unwrapped - inferDefined = inferDefined' _Unwrapped - deriveSeqOnePath :: MonadSimplify simplifier => [Rule OnePathRule] @@ -343,7 +336,6 @@ instance Goal AllPathRule where simplify = simplify' _Unwrapped checkImplication = checkImplication' _Unwrapped isTriviallyValid = isTriviallyValid' _Unwrapped - inferDefined = inferDefined' _Unwrapped applyClaims claims = deriveSeqAllPath (map goalToRule claims) applyAxioms axiomss = \goal -> @@ -419,15 +411,6 @@ instance Goal ReachabilityRule where isTriviallyValid (AllPath goal) = isTriviallyValid goal isTriviallyValid (OnePath goal) = isTriviallyValid goal - inferDefined (AllPath goal) = - inferDefined goal - & fmap AllPath - & allPathTransition - inferDefined (OnePath goal) = - inferDefined goal - & fmap OnePath - & onePathTransition - applyClaims claims (AllPath goal) = applyClaims (mapMaybe maybeAllPath claims) goal & fmap (fmap AllPath) @@ -692,22 +675,6 @@ simplify' lensRulePattern = & lift Foldable.asum (pure <$> configs) -inferDefined' - :: MonadSimplify m - => Lens' goal (RulePattern VariableName) - -> goal - -> Strategy.TransitionT (Rule goal) m goal -inferDefined' lensRulePattern = - Lens.traverseOf (lensRulePattern . RulePattern.leftPattern) $ \config -> do - let definedConfig = - Pattern.andCondition (mkDefined <$> config) - $ from $ makeCeilPredicate_ (Conditional.term config) - configs <- - simplifyTopConfiguration definedConfig - >>= SMT.Evaluator.filterMultiOr - & lift - Foldable.asum (pure <$> configs) - isTriviallyValid' :: Lens' goal (RulePattern variable) -> goal -> Bool isTriviallyValid' lensRulePattern = isBottom . RulePattern.left . Lens.view lensRulePattern diff --git a/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs b/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs index 9b869b116c..cbfb59d236 100644 --- a/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs +++ b/kore/test/Test/Kore/Strategies/AllPath/AllPath.hs @@ -353,10 +353,6 @@ instance Goal.Goal Goal where simplify = return - inferDefined goal@(src, _) - | src == NotDef = empty - | otherwise = pure goal - applyClaims claims = derivePar (map Rule claims) applyAxioms axiomGroups = derivePar (concat axiomGroups) From 7c384848f5218b33833f9682b5f843bf1f1ae73f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 30 Jul 2020 11:17:18 -0500 Subject: [PATCH 19/28] Remove -fno-prof-auto everywhere --- kore/src/Kore/Debug.hs | 1 - kore/src/Kore/Internal/Conditional.hs | 2 -- kore/src/Kore/Step/Simplification/Data.hs | 1 - kore/src/Kore/Step/Transition.hs | 2 -- kore/src/Kore/Unification/UnifierT.hs | 2 -- kore/src/Prof.hs | 2 -- kore/src/SMT.hs | 2 -- 7 files changed, 12 deletions(-) diff --git a/kore/src/Kore/Debug.hs b/kore/src/Kore/Debug.hs index c9cb467328..2bfa2e4dda 100644 --- a/kore/src/Kore/Debug.hs +++ b/kore/src/Kore/Debug.hs @@ -1,5 +1,4 @@ {-# OPTIONS_GHC -Wno-unused-top-binds #-} -{-# OPTIONS_GHC -fno-prof-auto #-} {- | Copyright : (c) Runtime Verification, 2018 diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index cd5e15fee8..727cbb1e67 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -6,8 +6,6 @@ Representation of conditional terms. -} -{-# OPTIONS_GHC -fno-prof-auto #-} - module Kore.Internal.Conditional ( Conditional (..) , withoutTerm diff --git a/kore/src/Kore/Step/Simplification/Data.hs b/kore/src/Kore/Step/Simplification/Data.hs index 33df09949a..cea84e42e6 100644 --- a/kore/src/Kore/Step/Simplification/Data.hs +++ b/kore/src/Kore/Step/Simplification/Data.hs @@ -9,7 +9,6 @@ Portability : portable -} {-# LANGUAGE UndecidableInstances #-} -{-# OPTIONS_GHC -fno-prof-auto #-} module Kore.Step.Simplification.Data ( Simplifier diff --git a/kore/src/Kore/Step/Transition.hs b/kore/src/Kore/Step/Transition.hs index a1258b2a69..3a96c3a3f2 100644 --- a/kore/src/Kore/Step/Transition.hs +++ b/kore/src/Kore/Step/Transition.hs @@ -6,8 +6,6 @@ License : NCSA {-# LANGUAGE UndecidableInstances #-} -{-# OPTIONS_GHC -fno-prof-auto #-} - module Kore.Step.Transition ( TransitionT (..) , runTransitionT diff --git a/kore/src/Kore/Unification/UnifierT.hs b/kore/src/Kore/Unification/UnifierT.hs index 11dae21aab..8499e7559b 100644 --- a/kore/src/Kore/Unification/UnifierT.hs +++ b/kore/src/Kore/Unification/UnifierT.hs @@ -4,8 +4,6 @@ License : NCSA -} -{-# OPTIONS_GHC -fno-prof-auto #-} - module Kore.Unification.UnifierT ( UnifierT (..) , runUnifierT diff --git a/kore/src/Prof.hs b/kore/src/Prof.hs index 97dc5b5997..94b76bdc89 100644 --- a/kore/src/Prof.hs +++ b/kore/src/Prof.hs @@ -4,8 +4,6 @@ License : NCSA -} -{-# OPTIONS_GHC -fno-prof-auto #-} - module Prof ( MonadProf (..) , defaultTraceProf diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index 7be44f79cb..513fa27c8a 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -6,8 +6,6 @@ License : NCSA Maintainer : thomas.tuegel@runtimeverification.com -} -{-# OPTIONS_GHC -fno-prof-auto #-} - module SMT ( SMT, getSMT , Solver From aba09d7be8c19e0ce9ea64da74acc175fce437cf Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 4 Aug 2020 10:44:19 -0500 Subject: [PATCH 20/28] test_Defined: Test equal patterns both ways --- .../Test/Kore/Step/Simplification/AndTerms.hs | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 8741fb32b0..72ab589987 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1216,15 +1216,24 @@ test_Defined = let partial = Mock.f Mock.a defined = mkDefined partial in - [ testCase "\\and" $ do - let expect = [Pattern.fromTermLike defined] + [ testCase "\\and(partial, defined)" $ do + let expect = [Pattern.fromTermLike partial] (actualAnd, actualUnify) <- simplifyUnify partial defined assertEqual "" expect actualAnd assertEqual "" expect actualUnify - , testCase "\\equals" $ do + , testCase "\\and(defined, partial)" $ do + let expect = [Pattern.fromTermLike defined] + (actualAnd, actualUnify) <- simplifyUnify defined partial + assertEqual "" expect actualAnd + assertEqual "" expect actualUnify + , testCase "\\equals(partial, defined)" $ do let expect = Just [Condition.topOf Mock.testSort] actual <- simplifyEquals mempty partial defined assertEqual "" expect actual + , testCase "\\equals(defined, partial)" $ do + let expect = Just [Condition.topOf Mock.testSort] + actual <- simplifyEquals mempty defined partial + assertEqual "" expect actual ] , testGroup "variable with function" $ let defined = mkDefined (Mock.f Mock.a) From 21ee72b6ec48a34865824e1b8d75831667337c49 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 4 Aug 2020 10:44:34 -0500 Subject: [PATCH 21/28] equalAndEquals: Always return first pattern --- kore/src/Kore/Step/Simplification/AndTerms.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index ac3dfa043e..68b72a8d07 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -332,7 +332,8 @@ equalAndEquals -> MaybeT unifier (Pattern variable) equalAndEquals first second | unDefined first == unDefined second = - return (Pattern.fromTermLike $ if isDefinedPattern second then second else first) + -- TODO (thomas.tuegel): Preserve defined and simplified flags. + return (Pattern.fromTermLike first) equalAndEquals _ _ = empty -- | Unify two patterns where the first is @\\bottom@. From 83be04145cbe21ed5b54ac8bb35796ae30636ce7 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 4 Aug 2020 10:44:45 -0500 Subject: [PATCH 22/28] RED test_goTranslatePredicate: Test defined /Int patterns --- kore/test/Test/Kore/Step/MockSymbols.hs | 5 ++++- kore/test/Test/Kore/Step/SMT/Translate.hs | 9 +++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index cb14a21034..5e108d801d 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -593,7 +593,9 @@ greaterEqIntSymbol = tdivIntSymbol :: Symbol tdivIntSymbol = symbol tdivIntId [intSort, intSort] intSort - & function & hook "INT.tdiv" + & function + & hook "INT.tdiv" + & smthook "div" concatListSymbol :: Symbol concatListSymbol = @@ -1544,6 +1546,7 @@ smtUnresolvedDeclarations = SMT.Declarations , ( bSort0Id, smtConstructor bSort0Id [] testSort0) , ( lessIntId, smtBuiltinSymbol "<" [intSort, intSort] boolSort) , ( greaterEqIntId, smtBuiltinSymbol ">=" [intSort, intSort] boolSort) + , ( tdivIntId, smtBuiltinSymbol "div" [intSort, intSort] intSort) , ( sigmaId, smtConstructor sigmaId [testSort, testSort] testSort) ] } diff --git a/kore/test/Test/Kore/Step/SMT/Translate.hs b/kore/test/Test/Kore/Step/SMT/Translate.hs index 9de9a5f1d5..091ecb6ecf 100644 --- a/kore/test/Test/Kore/Step/SMT/Translate.hs +++ b/kore/test/Test/Kore/Step/SMT/Translate.hs @@ -135,6 +135,14 @@ test_goTranslatePredicate = ( exists 0 (exists 1 $ fun 2 [var 0, var 1]) `and` exists 3 (existst 4 $ exists 5 $ fun 2 [var 5, var 3]) ) + , testCase "X:Int = X:Int /Int Y:Int" $ + yields + (translating (peq n (Mock.tdivInt n m))) + (var 0 `eq` (var 0 `sdiv` var 1)) + , testCase "X:Int = \\defined X:Int /Int Y:Int" $ + yields + (translating (peq n (TermLike.mkDefined $ Mock.tdivInt n m))) + (var 0 `eq` (var 0 `sdiv` var 1)) ] where x = TermLike.mkElemVar Mock.x @@ -155,6 +163,7 @@ test_goTranslatePredicate = existsb i p = existsQ [List [var i, Atom "Bool"]] p existst i p = existsQ [List [var i, Atom "|HB_testSort|"]] p fun i p = SMT.SimpleSMT.List (var i : p) + sdiv i j = List [Atom "div", i, j] translating :: HasCallStack => Predicate VariableName -> IO (Maybe SExpr) translating = From fdc14ed293b68789ce8025bdaa3d7bd149ed9f30 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 4 Aug 2020 10:48:40 -0500 Subject: [PATCH 23/28] GRN translatePredicateWith: Remove Defined wrapper from Int and Bool --- kore/src/Kore/Step/SMT/Translate.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kore/src/Kore/Step/SMT/Translate.hs b/kore/src/Kore/Step/SMT/Translate.hs index c31b4ff93e..41cd6a6687 100644 --- a/kore/src/Kore/Step/SMT/Translate.hs +++ b/kore/src/Kore/Step/SMT/Translate.hs @@ -211,6 +211,7 @@ translatePredicateWith translateTerm predicate = (<|>) (translateApplication app) (translateUninterpreted SMT.tInt pat) + DefinedF (Defined child) -> translateInt child _ -> empty -- | Translate a functional pattern in the builtin Bool sort for SMT. @@ -230,6 +231,7 @@ translatePredicateWith translateTerm predicate = (<|>) (translateApplication app) (translateUninterpreted SMT.tBool pat) + DefinedF (Defined child) -> translateBool child _ -> empty translateApplication :: Application Symbol p -> Translator m variable SExpr From b3e15b209038708fd8d5a30845b429fe32981e82 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 4 Aug 2020 10:51:19 -0500 Subject: [PATCH 24/28] test_goTranslatePredicate -> test_translatePredicateWith --- kore/test/Test/Kore/Step/SMT/Translate.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kore/test/Test/Kore/Step/SMT/Translate.hs b/kore/test/Test/Kore/Step/SMT/Translate.hs index 091ecb6ecf..08f1a2d390 100644 --- a/kore/test/Test/Kore/Step/SMT/Translate.hs +++ b/kore/test/Test/Kore/Step/SMT/Translate.hs @@ -1,5 +1,5 @@ module Test.Kore.Step.SMT.Translate - ( test_goTranslatePredicate + ( test_translatePredicateWith ) where import Prelude.Kore hiding @@ -30,8 +30,8 @@ import Kore.Step.SMT.Translate import SMT import qualified SMT.SimpleSMT -test_goTranslatePredicate :: [TestTree] -test_goTranslatePredicate = +test_translatePredicateWith :: [TestTree] +test_translatePredicateWith = [ testCase "true" $ translating true `yields` smtTrue , testCase "n = n" $ From 288cfffbf8c0b83ee87ca1e1d4364f2b84ae647f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 4 Aug 2020 11:32:15 -0500 Subject: [PATCH 25/28] test/imp: make golden --- test/imp/run-stepf-repl-script-spec.k.out.golden | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/imp/run-stepf-repl-script-spec.k.out.golden b/test/imp/run-stepf-repl-script-spec.k.out.golden index 62725d7e52..0d74fe9590 100644 --- a/test/imp/run-stepf-repl-script-spec.k.out.golden +++ b/test/imp/run-stepf-repl-script-spec.k.out.golden @@ -1,8 +1,8 @@ Kore (0)> ProveStepsF 11 Kore (10)> ProveStepsF 4 -Kore (18)> ProveStepsF 1000 +Kore (17)> ProveStepsF 1000 Proof completed on all branches. -Kore (18)> Prove (Left (ClaimIndex {unClaimIndex = 1})) +Kore (17)> Prove (Left (ClaimIndex {unClaimIndex = 1})) Switched to proving claim 1 Kore (0)> ProveStepsF 1000 Proof completed on all branches. From 74de3f72f28f2597c5d31ab6a6e17c65fd7317ee Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 4 Aug 2020 13:26:00 -0500 Subject: [PATCH 26/28] test/map/map-definedness: make golden --- .../map-definedness/test-1-spec.k.out.golden | 29 +----------- .../map-definedness/test-2-spec.k.out.golden | 45 +------------------ .../map-definedness/test-3-spec.k.out.golden | 16 +------ .../map-definedness/test-4-spec.k.out.golden | 39 +--------------- 4 files changed, 4 insertions(+), 125 deletions(-) diff --git a/test/map/map-definedness/test-1-spec.k.out.golden b/test/map/map-definedness/test-1-spec.k.out.golden index e22988260d..e663cb04e1 100644 --- a/test/map/map-definedness/test-1-spec.k.out.golden +++ b/test/map/map-definedness/test-1-spec.k.out.golden @@ -1,28 +1 @@ - #Not ( #Not ( { - X - #Equals - Y - } ) - #And - { - false - #Equals - X:Int in_keys ( M ) - } ) -#And - - - added ~> . - - - M - X:Int |-> 3 - Y:Int |-> 2 - - -#And - { - Y:Int in_keys ( M ) - #Equals - false - } +#True diff --git a/test/map/map-definedness/test-2-spec.k.out.golden b/test/map/map-definedness/test-2-spec.k.out.golden index 2b3a593564..e663cb04e1 100644 --- a/test/map/map-definedness/test-2-spec.k.out.golden +++ b/test/map/map-definedness/test-2-spec.k.out.golden @@ -1,44 +1 @@ - #Ceil ( M - N ) -#And - #Not ( #Not ( { - X - #Equals - 2 - } ) - #And - { - false - #Equals - X:Int in_keys ( M ) - } - #And - { - false - #Equals - X:Int in_keys ( N ) - } ) -#And - - - added ~> . - - - 2 |-> 3 - M - N - X:Int |-> 3 - - -#And - { - false - #Equals - 2 in_keys ( M ) - } -#And - { - false - #Equals - 2 in_keys ( N ) - } +#True diff --git a/test/map/map-definedness/test-3-spec.k.out.golden b/test/map/map-definedness/test-3-spec.k.out.golden index ddb41b6f43..e663cb04e1 100644 --- a/test/map/map-definedness/test-3-spec.k.out.golden +++ b/test/map/map-definedness/test-3-spec.k.out.golden @@ -1,15 +1 @@ - #Not ( { - X:Int in_keys ( M ) - #Equals - false - } ) -#And - - - added ~> . - - - M - X:Int |-> 3 - - +#True diff --git a/test/map/map-definedness/test-4-spec.k.out.golden b/test/map/map-definedness/test-4-spec.k.out.golden index ccbaf31fd1..e663cb04e1 100644 --- a/test/map/map-definedness/test-4-spec.k.out.golden +++ b/test/map/map-definedness/test-4-spec.k.out.golden @@ -1,38 +1 @@ - #Ceil ( f ( 3 ) ) -#And - #Ceil ( f ( X ) ) -#And - #Not ( #Not ( { - 2 - #Equals - f ( X ) - } ) - #And - { - f ( X ) in_keys ( M ) - #Equals - false - } - #And - { - false - #Equals - 2 in_keys ( M ) - } ) -#And - - - added ~> . - - - 2 |-> 3 - M - f ( X ) |-> f ( 3 ) - - -#And - { - 2 in_keys ( M ) - #Equals - false - } +#True From d9368018eff0478cfaa360567ec4d81b4d7536cf Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 Aug 2020 10:25:12 -0500 Subject: [PATCH 27/28] test_Defined: equalAndEquals returns the first argument --- kore/test/Test/Kore/Step/Simplification/AndTerms.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 72ab589987..540baacc06 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1217,11 +1217,13 @@ test_Defined = defined = mkDefined partial in [ testCase "\\and(partial, defined)" $ do + -- equalAndEquals returns the first argument let expect = [Pattern.fromTermLike partial] (actualAnd, actualUnify) <- simplifyUnify partial defined assertEqual "" expect actualAnd assertEqual "" expect actualUnify , testCase "\\and(defined, partial)" $ do + -- equalAndEquals returns the first argument let expect = [Pattern.fromTermLike defined] (actualAnd, actualUnify) <- simplifyUnify defined partial assertEqual "" expect actualAnd From c9c32133da667d2b158bd6fd0dd91a35947bb9e2 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 Aug 2020 10:28:21 -0500 Subject: [PATCH 28/28] Kore.Internal.TermLike.unDefined: Documentation --- kore/src/Kore/Internal/TermLike.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 8f818c88bc..fc7af47f4d 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -1558,6 +1558,8 @@ mkDefined = updateCallStack . worker mkDefinedAtTop :: Ord variable => TermLike variable -> TermLike variable mkDefinedAtTop = synthesize . DefinedF . Defined +{- | Remove (recursively) the 'Defined' wrappers throughout a 'TermLike'. + -} unDefined :: TermLike variable -> TermLike variable unDefined = Recursive.unfold $ \termLike ->