diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs index 02302f6460..cdc13e0454 100644 --- a/kore/src/Kore/Builtin/Builtin.hs +++ b/kore/src/Kore/Builtin/Builtin.hs @@ -311,9 +311,8 @@ applicationEvaluator impl = (TermLike variable) -> simplifier (AttemptedAxiom variable) evaluator sideCondition (_ :< app) = do - let app' = fmap TermLike.removeEvaluated app getAttemptedAxiom - (impl sideCondition app' >>= appliedFunction) + (impl sideCondition app >>= appliedFunction) {- | Run a parser on a verified domain value. diff --git a/kore/src/Kore/Builtin/External.hs b/kore/src/Kore/Builtin/External.hs index 17dfbdce17..a28ba46d65 100644 --- a/kore/src/Kore/Builtin/External.hs +++ b/kore/src/Kore/Builtin/External.hs @@ -12,7 +12,6 @@ module Kore.Builtin.External import Prelude.Kore -import qualified Control.Comonad.Trans.Cofree as Cofree import Data.Functor.Const ( Const (..) ) @@ -123,10 +122,6 @@ externalize = TopF topF -> Syntax.TopF topF VariableF variableF -> Syntax.VariableF variableF InhabitantF inhabitantF -> Syntax.InhabitantF inhabitantF - EvaluatedF evaluatedF -> - Cofree.tailF - $ worker - $ getEvaluated evaluatedF EndiannessF endiannessF -> Syntax.ApplicationF $ mapHead Symbol.toSymbolOrAlias diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index cf665ae148..d0db16aab1 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -449,10 +449,7 @@ simplifyConjunctionByAssumption (toList -> andPredicates) = size :: TermLike variable -> Int size = - Recursive.fold $ \(_ :< termLikeF) -> - case termLikeF of - TermLike.EvaluatedF evaluated -> TermLike.getEvaluated evaluated - _ -> 1 + sum termLikeF + Recursive.fold $ \(_ :< termLikeF) -> 1 + sum termLikeF predSize :: Predicate variable -> Int predSize = diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 28f82fe9de..a78ca9d91f 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -10,7 +10,6 @@ License : NCSA module Kore.Internal.TermLike ( TermLikeF (..) , TermLike (..) - , Evaluated (..) , extractAttributes , isSimplified , isSimplifiedSomeCondition @@ -27,7 +26,6 @@ module Kore.Internal.TermLike , hasConstructorLikeTop , freeVariables , refreshVariables - , removeEvaluated , termLikeSort , hasFreeVariable , withoutFreeVariable @@ -89,7 +87,6 @@ module Kore.Internal.TermLike , mkSort , mkSortVariable , mkInhabitant - , mkEvaluated , mkEndianness , mkSignedness -- * Predicate constructors @@ -144,7 +141,6 @@ module Kore.Internal.TermLike , pattern ElemVar_ , pattern SetVar_ , pattern StringLiteral_ - , pattern Evaluated_ , pattern Endianness_ , pattern Signedness_ , pattern Inj_ @@ -652,7 +648,6 @@ forceSortPredicate = case pattern' of -- Recurse - EvaluatedF evaluated -> EvaluatedF (Right <$> evaluated) -- Predicates: Force sort and stop. BottomF bottom' -> BottomF bottom' { bottomSort = forcedSort } TopF top' -> TopF top' { topSort = forcedSort } @@ -791,14 +786,6 @@ forceSorts operandSorts children = , Pretty.indent 4 (Unparser.arguments children) ] -{- | Remove `Evaluated` if it appears on the top of the `TermLike`. --} -removeEvaluated :: TermLike variable -> TermLike variable -removeEvaluated termLike@(Recursive.project -> (_ :< termLikeF)) = - case termLikeF of - EvaluatedF (Evaluated e) -> removeEvaluated e - _ -> termLike - {- | Construct an 'Application' pattern. The result sort of the 'Alias' must be provided. The sorts of arguments @@ -1460,13 +1447,6 @@ mkInhabitant -> TermLike variable mkInhabitant = updateCallStack . synthesize . InhabitantF . Inhabitant -mkEvaluated - :: HasCallStack - => Ord variable - => TermLike variable - -> TermLike variable -mkEvaluated = updateCallStack . synthesize . EvaluatedF . Evaluated - {- | Construct an 'Endianness' pattern. -} mkEndianness @@ -1730,8 +1710,6 @@ pattern SetVar_ :: SetVariable variable -> TermLike variable pattern StringLiteral_ :: Text -> TermLike variable -pattern Evaluated_ :: TermLike variable -> TermLike variable - pattern And_ andSort andFirst andSecond <- (Recursive.project -> _ :< AndF And { andSort, andFirst, andSecond }) @@ -1880,9 +1858,6 @@ pattern ElemVar_ elemVariable <- Var_ (retract -> Just elemVariable) pattern StringLiteral_ str <- (Recursive.project -> _ :< StringLiteralF (Const (StringLiteral str))) -pattern Evaluated_ child <- - (Recursive.project -> _ :< EvaluatedF (Evaluated child)) - pattern Endianness_ :: Endianness -> TermLike child pattern Endianness_ endianness <- (Recursive.project -> _ :< EndiannessF (Const endianness)) diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index a1b06481fc..0d3c03cd0a 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -8,8 +8,7 @@ License : NCSA {-# LANGUAGE UndecidableInstances #-} module Kore.Internal.TermLike.TermLike - ( Evaluated (..) - , TermLike (..) + ( TermLike (..) , TermLikeF (..) , retractKey , extractAttributes @@ -120,34 +119,6 @@ import Kore.Variables.Binding import qualified Pretty import qualified SQL -{- | @Evaluated@ wraps patterns which are fully evaluated. - -Fully-evaluated patterns will not be simplified further because no progress -could be made. - - -} -newtype Evaluated child = Evaluated { getEvaluated :: child } - deriving (Eq, Ord, Show) - deriving (Foldable, Functor, Traversable) - deriving (GHC.Generic) - deriving anyclass (Hashable, NFData) - deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) - deriving anyclass (Debug, Diff) - -instance Unparse child => Unparse (Evaluated child) where - unparse evaluated = - Pretty.vsep ["/* evaluated: */", Unparser.unparseGeneric evaluated] - unparse2 evaluated = - Pretty.vsep ["/* evaluated: */", Unparser.unparse2Generic evaluated] - -instance Synthetic syn Evaluated where - synthetic = getEvaluated - {-# INLINE synthetic #-} - -instance {-# OVERLAPS #-} Synthetic Pattern.Simplified Evaluated where - synthetic = const Pattern.fullySimplified - {-# INLINE synthetic #-} - {- | 'TermLikeF' is the 'Base' functor of internal term-like patterns. -} @@ -174,7 +145,6 @@ data TermLikeF variable child | RewritesF !(Rewrites Sort child) | TopF !(Top Sort child) | InhabitantF !(Inhabitant child) - | EvaluatedF !(Evaluated child) | StringLiteralF !(Const StringLiteral child) | InternalBoolF !(Const InternalBool child) | InternalBytesF !(Const InternalBytes child) @@ -226,7 +196,6 @@ instance RewritesF rewrites -> synthetic rewrites TopF top -> synthetic top InhabitantF inhabitant -> synthetic inhabitant - EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes @@ -264,7 +233,6 @@ instance Synthetic Sort (TermLikeF variable) where RewritesF rewrites -> synthetic rewrites TopF top -> synthetic top InhabitantF inhabitant -> synthetic inhabitant - EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes @@ -302,7 +270,6 @@ instance Synthetic Pattern.Functional (TermLikeF variable) where RewritesF rewrites -> synthetic rewrites TopF top -> synthetic top InhabitantF inhabitant -> synthetic inhabitant - EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes @@ -340,7 +307,6 @@ instance Synthetic Pattern.Function (TermLikeF variable) where RewritesF rewrites -> synthetic rewrites TopF top -> synthetic top InhabitantF inhabitant -> synthetic inhabitant - EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes @@ -378,7 +344,6 @@ instance Synthetic Pattern.Defined (TermLikeF variable) where RewritesF rewrites -> synthetic rewrites TopF top -> synthetic top InhabitantF inhabitant -> synthetic inhabitant - EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes @@ -416,7 +381,6 @@ instance Synthetic Pattern.Simplified (TermLikeF variable) where RewritesF rewrites -> synthetic rewrites TopF top -> synthetic top InhabitantF inhabitant -> synthetic inhabitant - EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes @@ -454,7 +418,6 @@ instance Synthetic Pattern.ConstructorLike (TermLikeF variable) where RewritesF rewrites -> synthetic rewrites TopF top -> synthetic top InhabitantF inhabitant -> synthetic inhabitant - EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes @@ -752,8 +715,6 @@ instance TopF Top { topSort } -> locationFromAst topSort VariableF (Const variable) -> locationFromAst variable InhabitantF Inhabitant { inhSort } -> locationFromAst inhSort - EvaluatedF Evaluated { getEvaluated } -> - locationFromAst getEvaluated InjF Inj { injChild } -> locationFromAst injChild SignednessF (Const signedness) -> locationFromAst signedness EndiannessF (Const endianness) -> locationFromAst endianness @@ -821,7 +782,6 @@ traverseVariablesF adj = InternalSetF setP -> pure (InternalSetF setP) TopF topP -> pure (TopF topP) InhabitantF s -> pure (InhabitantF s) - EvaluatedF childP -> pure (EvaluatedF childP) EndiannessF endianness -> pure (EndiannessF endianness) SignednessF signedness -> pure (SignednessF signedness) InjF inj -> pure (InjF inj) diff --git a/kore/src/Kore/Step/SMT/Translate.hs b/kore/src/Kore/Step/SMT/Translate.hs index 013412a736..0dc98e880d 100644 --- a/kore/src/Kore/Step/SMT/Translate.hs +++ b/kore/src/Kore/Step/SMT/Translate.hs @@ -153,7 +153,6 @@ translatePredicateWith sideCondition translateTerm predicate = translatePredicatePatternWorker :: p -> Translator variable m SExpr translatePredicatePatternWorker pat = case Cofree.tailF (Recursive.project pat) of - EvaluatedF child -> translatePredicatePattern (getEvaluated child) -- Logical connectives: translate as connectives AndF and' -> translatePredicateAnd and' BottomF _ -> return (SMT.bool False) diff --git a/kore/src/Kore/Step/Simplification/Ceil.hs b/kore/src/Kore/Step/Simplification/Ceil.hs index 983cf086a5..0e07cdb9f1 100644 --- a/kore/src/Kore/Step/Simplification/Ceil.hs +++ b/kore/src/Kore/Step/Simplification/Ceil.hs @@ -390,7 +390,6 @@ makeSimplifiedCeil where needsChildCeils = case termLikeF of ApplyAliasF _ -> False - EvaluatedF _ -> False EndiannessF _ -> True SignednessF _ -> True AndF _ -> True diff --git a/kore/src/Kore/Step/Simplification/TermLike.hs b/kore/src/Kore/Step/Simplification/TermLike.hs index 1c0ba0cfcc..056cc5ac85 100644 --- a/kore/src/Kore/Step/Simplification/TermLike.hs +++ b/kore/src/Kore/Step/Simplification/TermLike.hs @@ -369,7 +369,6 @@ simplify sideCondition = \termLike -> -- Unimplemented cases ApplyAliasF _ -> doNotSimplify -- Do not simplify non-simplifiable patterns. - EvaluatedF _ -> doNotSimplify EndiannessF _ -> doNotSimplify SignednessF _ -> doNotSimplify -- diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs index 044a750c0a..f2976c7104 100644 --- a/kore/test/Test/ConsistentKore.hs +++ b/kore/test/Test/ConsistentKore.hs @@ -90,7 +90,6 @@ import Kore.Internal.TermLike , mkCeil , mkElemVar , mkEquals - , mkEvaluated , mkExists , mkFloor , mkForall @@ -332,7 +331,6 @@ _checkTermImplemented term@(Recursive.project -> _ :< termF) = checkTermF (InternalListF _) = term checkTermF (InternalMapF _) = term checkTermF (InternalSetF _) = term - checkTermF (EvaluatedF _) = term checkTermF (InhabitantF _) = term -- Not implemented. checkTermF (EndiannessF _) = term -- Not implemented. checkTermF (SignednessF _) = term -- Not implemented. @@ -358,7 +356,6 @@ termGenerators = do , orGenerator , rewritesGenerator , topGenerator - , evaluatedGenerator ] literals <- filterGeneratorsAndGroup (catMaybes @@ -587,9 +584,6 @@ rewritesGenerator = binaryOperatorGenerator mkRewrites topGenerator :: TermGenerator topGenerator = nullaryFreeSortOperatorGenerator mkTop -evaluatedGenerator :: TermGenerator -evaluatedGenerator = unaryOperatorGenerator mkEvaluated - maybeStringLiteralGenerator :: Setup -> Maybe TermGenerator maybeStringLiteralGenerator Setup {maybeStringLiteralSort} = case maybeStringLiteralSort of diff --git a/kore/test/Test/Kore/Builtin/Int.hs b/kore/test/Test/Kore/Builtin/Int.hs index 7e761d8299..c15117dc71 100644 --- a/kore/test/Test/Kore/Builtin/Int.hs +++ b/kore/test/Test/Kore/Builtin/Int.hs @@ -11,8 +11,6 @@ module Test.Kore.Builtin.Int , test_and, test_or, test_xor, test_not , test_shl, test_shr , test_pow, test_powmod, test_log2 - , test_tdiv_evaluated_arguments - , test_ediv_evaluated_arguments , test_unifyEqual_NotEqual , test_unifyEqual_Equal , test_unifyAnd_NotEqual @@ -57,9 +55,6 @@ import Data.Bits , (.&.) , (.|.) ) -import Data.Semigroup - ( Endo (..) - ) import qualified Data.Text as Text import Kore.Builtin.Int @@ -281,10 +276,6 @@ test_abs = testUnary absIntSymbol abs test_tdiv :: TestTree test_tdiv = testPartialBinary tdivIntSymbol tdiv -test_tdiv_evaluated_arguments :: TestTree -test_tdiv_evaluated_arguments = - testDivEvaluatedArguments tdivIntSymbol tdiv - test_tmod :: TestTree test_tmod = testPartialBinary tmodIntSymbol tmod @@ -297,10 +288,6 @@ test_tmodZero = testPartialBinaryZero tmodIntSymbol tmod test_ediv_property :: TestTree test_ediv_property = testPartialBinary edivIntSymbol ediv -test_ediv_evaluated_arguments :: TestTree -test_ediv_evaluated_arguments = - testDivEvaluatedArguments edivIntSymbol ediv - test_emod_property :: TestTree test_emod_property = testPartialBinary emodIntSymbol emod @@ -400,25 +387,6 @@ test_euclidian_division_theorem = internalIntValue _ -> error "Expecting builtin int." -testDivEvaluatedArguments - :: Symbol - -> (Integer -> Integer -> Maybe Integer) - -> TestTree -testDivEvaluatedArguments symbol expected = - testPropertyWithSolver (Text.unpack name) $ do - a <- forAll genInteger - b <- forAll genInteger - na <- forAll $ Gen.integral (Range.linear 0 5) - nb <- forAll $ Gen.integral (Range.linear 0 5) - let expect = asPartialPattern $ expected a b - actual <- evaluateT - $ mkApplySymbol symbol [evaluated na a, evaluated nb b] - (===) expect actual - where - name = expectHook edivIntSymbol <> " with evaluated arguments" - compose n f = appEndo $ stimes (n :: Integer) (Endo f) - evaluated n x = compose n mkEvaluated $ asInternal x - -- Bitwise operations test_and :: TestTree test_and = testBinary andIntSymbol (.&.) diff --git a/kore/test/Test/Kore/Step/Axiom/EvaluationStrategy.hs b/kore/test/Test/Kore/Step/Axiom/EvaluationStrategy.hs index dd25d47826..d0674aa77d 100644 --- a/kore/test/Test/Kore/Step/Axiom/EvaluationStrategy.hs +++ b/kore/test/Test/Kore/Step/Axiom/EvaluationStrategy.hs @@ -119,43 +119,6 @@ test_definitionEvaluation = ) (Mock.functionalConstr10 Mock.c) assertEqual "" expect actual - {- - Uncomment this if we ever go back to having remainders for functions. - - , testCase "Evaluation with remainder" $ do - let requirement = makeEqualsPredicate - (Mock.f Mock.a) - (Mock.g Mock.b) - expect = - AttemptedAxiom.Applied AttemptedAxiomResults - { results = - OrPattern.fromPattern Conditional - { term = Mock.g Mock.a - , predicate = requirement - , substitution = mempty - } - , remainders = - OrPattern.fromPatterns - $ map (fmap mkEvaluated) - [ Conditional - { term = Mock.functionalConstr10 Mock.a - , predicate = makeNotPredicate requirement - , substitution = mempty - } - ] - } - actual <- - evaluate - (definitionEvaluation - [ axiom - (Mock.functionalConstr10 Mock.a) - (Mock.g Mock.a) - requirement - ] - ) - (Mock.functionalConstr10 Mock.a) - assertEqual "" expect actual - -} , testCase "Failed evaluation" $ do let expect = AttemptedAxiom.NotApplicable actual <- @@ -479,52 +442,6 @@ test_simplifierWithFallback = ) (Mock.functionalConstr10 Mock.a) assertEqual "" expect actual - {- - Uncomment this if we ever go back to having remainders for equality axioms. - - , testCase "Uses first with remainder" $ do - let requirement = makeEqualsPredicate - (Mock.f Mock.a) - (Mock.g Mock.b) - expect = - AttemptedAxiom.Applied AttemptedAxiomResults - { results = OrPattern.fromPatterns - [ Conditional - { term = Mock.g Mock.a - , predicate = requirement - , substitution = mempty - } - ] - , remainders = - OrPattern.fromPatterns $ (map . fmap) mkEvaluated - [ Conditional - { term = Mock.functionalConstr10 Mock.a - , predicate = makeNotPredicate requirement - , substitution = mempty - } - ] - } - actual <- - evaluate - (simplifierWithFallback - (definitionEvaluation - [ axiom - (Mock.functionalConstr10 Mock.a) - (Mock.g Mock.a) - requirement - ] - ) - (definitionEvaluation - [ axiom - (Mock.functionalConstr10 Mock.a) - (Mock.f Mock.a) - (makeNotPredicate requirement) - ] - ) - ) - (Mock.functionalConstr10 Mock.a) - assertEqual "" expect actual - -} , testCase "Falls back to second" $ do let expect = AttemptedAxiom.Applied diff --git a/kore/test/Test/Kore/Step/Axiom/Matcher.hs b/kore/test/Test/Kore/Step/Axiom/Matcher.hs index ecaf587fe9..00400aea95 100644 --- a/kore/test/Test/Kore/Step/Axiom/Matcher.hs +++ b/kore/test/Test/Kore/Step/Axiom/Matcher.hs @@ -355,31 +355,6 @@ test_matcherVariableFunction = (Mock.constr10 Mock.cf) assertEqual "" expect actual ] - , testGroup "Evaluated" - [ testCase "Functional" $ do - let evaluated = mkEvaluated Mock.functional00 - expect = - mkMatchResult - ( makeTruePredicate - , Map.singleton - (inject Mock.xConfig) - evaluated - ) - actual <- matchDefinition (mkElemVar Mock.xConfig) evaluated - assertEqual "" expect actual - - , testCase "Function" $ do - let evaluated = mkEvaluated Mock.cf - expect = - mkMatchResult - ( makeCeilPredicate evaluated - , Map.singleton - (inject Mock.xConfig) - evaluated - ) - actual <- matchDefinition (mkElemVar Mock.xConfig) evaluated - assertEqual "" expect actual - ] ] where aSubSub = Mock.functional00SubSubSort diff --git a/kore/test/Test/Kore/Step/Simplification/Ceil.hs b/kore/test/Test/Kore/Step/Simplification/Ceil.hs index 2c8e00a2e1..804127763a 100644 --- a/kore/test/Test/Kore/Step/Simplification/Ceil.hs +++ b/kore/test/Test/Kore/Step/Simplification/Ceil.hs @@ -293,32 +293,6 @@ test_ceilSimplification = "ceil(functional and eq(f(a), g(a)))" expected actual - , testCase "ceil with evaluated functional terms" $ do - -- if term is functional, then - -- ceil(term and predicate and subst) - -- = top and predicate and subst - let - expected = OrPattern.fromPatterns - [ Conditional - { term = mkTop_ - , predicate = makeEqualsPredicate fOfA gOfA - , substitution = - Substitution.unsafeWrap [(inject Mock.xConfig, fOfB)] - } - ] - actual <- makeEvaluate - Conditional - { term = mkEvaluated Mock.a - , predicate = makeEqualsPredicate fOfA gOfA - , substitution = - Substitution.wrap - $ Substitution.mkUnwrappedSubstitution - [(inject Mock.xConfig, fOfB)] - } - assertEqual - "ceil(functional and eq(f(a), g(a)))" - expected - actual , testCase "ceil with functional composition" $ do -- if term is functional(non-funct, non-funct), then -- ceil(term and predicate and subst) diff --git a/kore/test/Test/Kore/Step/Simplification/Integration.hs b/kore/test/Test/Kore/Step/Simplification/Integration.hs index b37555ccca..de6dd8625f 100644 --- a/kore/test/Test/Kore/Step/Simplification/Integration.hs +++ b/kore/test/Test/Kore/Step/Simplification/Integration.hs @@ -15,13 +15,8 @@ import qualified Control.Lens as Lens import qualified Data.Default as Default import Data.Generics.Product import qualified Data.Map.Strict as Map -import Data.Maybe - ( fromJust - ) -import qualified Data.Set as Set import Test.Tasty -import qualified Kore.Builtin.AssociativeCommutative as Ac import qualified Kore.Builtin.Builtin as Builtin import qualified Kore.Builtin.Int as Int import qualified Kore.Builtin.List as List @@ -32,7 +27,6 @@ import Kore.Equation , mkEquation ) import qualified Kore.Equation as Equation -import Kore.Internal.InternalSet import Kore.Internal.SideCondition ( SideCondition ) @@ -45,7 +39,6 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ) import Kore.Rewriting.RewritingVariable ( RewritingVariableName - , configElementVariableFromId , mkConfigVariable , mkRuleVariable ) @@ -762,150 +755,6 @@ test_simplificationIntegration = assertBool "Expecting simplification" (OrPattern.isSimplified sideRepresentation actual) - , testCase "Forall simplification" $ do - let expected = OrPattern.fromPatterns - [ Conditional - { term = mkTop Mock.otherSort - , predicate = - makeCeilPredicate - (mkEvaluated (mkBottom Mock.mapSort)) - , substitution = mempty - } - ] - actual <- evaluate - Conditional - { term = mkForall - Mock.tConfig - (mkIn - Mock.otherSort - (mkNot (mkBottom Mock.mapSort)) - (mkEvaluated mkBottom_) - ) - , predicate = makeTruePredicate - , substitution = mempty - } - assertEqual "" expected actual - , testCase "Implies simplification" $ do - let zz = configElementVariableFromId (testId "zz") Mock.subOthersort - mci = configElementVariableFromId (testId "mci") Mock.subOthersort - mw = configElementVariableFromId (testId "mw") Mock.subOthersort - k = - mkSetVariable (testId "k") Mock.setSort - & mapSetVariable (pure mkConfigVariable) - - let expects = - [ Conditional - { term = mkTop Mock.stringSort - , predicate = makeAndPredicate - (makeImpliesPredicate - (makeAndPredicate - (makeAndPredicate - (makeCeilPredicate - (mkAnd - (Mock.fSet mkTop_) - (mkMu k - (asInternal (Set.fromList [Mock.a])) - ) - ) - ) - (makeCeilPredicate - (Mock.fSet mkTop_) - ) - ) - (makeCeilPredicate - (mkMu k - (asInternal (Set.fromList [Mock.a])) - ) - ) - ) - (makeIffPredicate - (makeEqualsPredicate Mock.aSubSubsort mkTop_) - (makeFloorPredicate - (mkEvaluated (mkBottom Mock.testSort)) - ) - ) - ) - (makeImpliesPredicate - (makeAndPredicate - (makeAndPredicate - (makeCeilPredicate - (mkAnd - (Mock.fSet mkTop_) - (mkMu k - (mkEvaluated Mock.unitSet) - ) - ) - ) - (makeCeilPredicate - (Mock.fSet mkTop_) - ) - ) - (makeCeilPredicate - (mkMu k - (mkEvaluated Mock.unitSet) - ) - ) - ) - (makeIffPredicate - (makeEqualsPredicate Mock.aSubSubsort mkTop_) - (makeFloorPredicate - (mkEvaluated (mkBottom Mock.testSort)) - ) - ) - ) - , substitution = mempty - } - ] - & OrPattern.fromPatterns - actuals <- evaluate - Conditional - { term = mkImplies - (mkCeil_ - (mkIn Mock.testSort0 - (mkMu k - (mkOr - (mkEvaluated Mock.unitSet) - (mkExists mw (Mock.elementSet Mock.a)) - ) - ) - (Mock.fSet (mkFloor_ (mkTop Mock.mapSort))) - ) - ) - (mkEquals Mock.stringSort - (mkFloor Mock.testSort0 - (mkEvaluated (mkBottom Mock.testSort)) - ) - (mkFloor Mock.testSort0 - (mkExists mci - (mkCeil Mock.setSort - (mkForall - zz - (mkEquals_ Mock.aSubSubsort mkTop_) - ) - ) - ) - ) - ) - - , predicate = makeTruePredicate - , substitution = mempty - } - Pattern.assertEquivalentPatterns expects actuals - , testCase "Ceil simplification" $ do - actual <- evaluate - Conditional - { term = mkCeil Mock.topSort - (mkForall Mock.xConfig - (Mock.concatSet - (mkEvaluated (mkEvaluated (mkTop Mock.setSort))) - (mkEvaluated (mkEvaluated (mkTop Mock.setSort))) - ) - ) - , predicate = makeTruePredicate - , substitution = mempty - } - assertBool "Expecting simplification" - (OrPattern.isSimplified sideRepresentation actual) , testCase "Equals-in simplification" $ do let gt = mkSetVariable (testId "gt") Mock.stringSort @@ -999,25 +848,6 @@ test_simplificationIntegration = } actual <- evaluate patt assertEqual "" (OrPattern.fromPattern expected) actual - , testCase "Not-iff-evaluated simplification" $ do - let patt = Conditional - { term = - mkNot - (mkIff - mkBottom_ - (mkEvaluated Mock.unitMap) - ) - , predicate = makeTruePredicate - , substitution = mempty - } - expected = OrPattern.fromPattern Conditional - { term = mkEvaluated Mock.unitMap - , predicate = makeTruePredicate - , substitution = mempty - } - - actual <- evaluate patt - assertEqual "" expected actual ] test_simplificationIntegrationUnification :: [TestTree] @@ -1544,15 +1374,6 @@ axiom left right requires = , attributes = Default.def } --- | Specialize 'Set.builtinSet' to the builtin sort 'setSort'. -asInternal - :: Set.Set (TermLike Concrete) - -> TermLike RewritingVariableName -asInternal = - Ac.asInternalConcrete Mock.metadataTools Mock.setSort - . Map.fromSet (const SetValue) - . Set.map (retractKey >>> fromJust) - sideRepresentation :: SideCondition.Representation sideRepresentation = SideCondition.toRepresentation (SideCondition.top :: SideCondition') diff --git a/kore/test/Test/Kore/Step/Simplification/Or.hs b/kore/test/Test/Kore/Step/Simplification/Or.hs index 8dd34b25d7..91edd683fa 100644 --- a/kore/test/Test/Kore/Step/Simplification/Or.hs +++ b/kore/test/Test/Kore/Step/Simplification/Or.hs @@ -50,7 +50,7 @@ import Test.Terse {- -`SimplifyEvaluated` is the core function. It converts two `OrPattern` +`simplifyEvaluated` is the core function. It converts two `OrPattern` values into a simplifier that is to produce a single `OrPattern`. We run the simplifier to check correctness. diff --git a/kore/test/Test/Kore/Step/Simplification/TermLike.hs b/kore/test/Test/Kore/Step/Simplification/TermLike.hs index 3f5e88a0d2..599eeef5bf 100644 --- a/kore/test/Test/Kore/Step/Simplification/TermLike.hs +++ b/kore/test/Test/Kore/Step/Simplification/TermLike.hs @@ -1,8 +1,7 @@ {-# LANGUAGE Strict #-} module Test.Kore.Step.Simplification.TermLike - ( test_simplify - , test_simplify_sideConditionReplacements + ( test_simplify_sideConditionReplacements ) where import Prelude.Kore @@ -10,9 +9,6 @@ import Prelude.Kore import Test.Tasty import Test.Tasty.HUnit -import Control.Monad - ( void - ) import Control.Monad.Catch ( MonadThrow ) @@ -31,8 +27,7 @@ import Kore.Internal.SideCondition import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike import Kore.Rewriting.RewritingVariable - ( RewritingVariableName - , getRewritingPattern + ( getRewritingPattern , mkConfigVariable , mkRewritingTerm ) @@ -44,12 +39,6 @@ import qualified Logic import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Simplification -test_simplify :: [TestTree] -test_simplify = - [ testCase "Evaluated" $ void - $ simplifyEvaluated $ mkEvaluated $ Mock.f Mock.a - ] - test_simplify_sideConditionReplacements :: [TestTree] test_simplify_sideConditionReplacements = [ testCase "Replaces top level term" $ do @@ -118,19 +107,6 @@ simplifyWithSideCondition . TermLike.simplify sideCondition . mkRewritingTerm -simplifyEvaluated - :: TermLike RewritingVariableName - -> IO (OrPattern RewritingVariableName) -simplifyEvaluated original = - runSimplifier env . getTestSimplifier - $ TermLike.simplify SideCondition.top original - where - env = Mock.env - { simplifierCondition = - -- Throw an error if any predicate would be simplified. - ConditionSimplifier $ const undefined - } - newtype TestSimplifier a = TestSimplifier { getTestSimplifier :: SimplifierT NoSMT a } deriving newtype (Functor, Applicative, Monad) diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index 5adb34c008..17104fffb1 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -3,7 +3,6 @@ module Test.Kore.Unification.Unifier ( test_unification , test_unsupportedConstructs - , test_evaluated ) where import Prelude.Kore @@ -658,29 +657,6 @@ test_unification = x = mkElemVar Mock.xConfig y = mkElemVar Mock.yConfig -test_evaluated :: [TestTree] -test_evaluated = - [ testCase "variable and functional term" $ do - let evaluated = mkEvaluated a2 - andSimplify - (UnificationTerm (mkElemVar Mock.xConfig)) - (UnificationTerm evaluated) - [ UnificationResult - { term = evaluated - , substitution = [("x", evaluated)] - , predicate = Predicate.makeTruePredicate - } - ] - , unificationProcedureSuccess - "variable and non-functional term" - (UnificationTerm (mkElemVar Mock.xConfig)) - (UnificationTerm (mkEvaluated a5)) - [ ( [("x", mkEvaluated a5)] - , Predicate.makeCeilPredicate (mkEvaluated a5) - ) - ] - ] - test_unsupportedConstructs :: TestTree test_unsupportedConstructs = testCase "Unsupported constructs" $