From 4d9f91a035f00b47a67b7c021962752c7fb595d1 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 16 Aug 2021 20:24:05 +0300 Subject: [PATCH 1/6] Add prototype Predicate generator --- kore/test/Test/ConsistentKore.hs | 39 +++++++++++++++++++ .../Test/Kore/Simplify/IntegrationProperty.hs | 8 ++++ 2 files changed, 47 insertions(+) diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs index 6e7c5aac10..59b9db4020 100644 --- a/kore/test/Test/ConsistentKore.hs +++ b/kore/test/Test/ConsistentKore.hs @@ -3,6 +3,8 @@ module Test.ConsistentKore ( Setup (..), runTermGen, termLikeGen, + -- testing + predicateGen, ) where import qualified Control.Arrow as Arrow @@ -24,6 +26,8 @@ import Data.Text ( import qualified Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range +import Kore.Internal.From +import Kore.Internal.Predicate (Predicate) import qualified Kore.Attribute.Constructor as Attribute.Constructor ( Constructor (..), ) @@ -241,6 +245,41 @@ termLikeGen = do | s < 10 = Range.Size s | otherwise = Range.Size 10 +-- TODO: +-- - will need the config for generating terms/variables +-- - make generated predicates smaller +predicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +predicateGen = + Gen.recursive + Gen.choice + [return fromTop_, return fromBottom_] + [ andPredicateGen + , orPredicateGen + , notPredicateGen + , impliesPredicateGen + , iffPredicateGen + ] + +andPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +andPredicateGen = + Gen.subterm2 predicateGen predicateGen fromAnd + +orPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +orPredicateGen = + Gen.subterm2 predicateGen predicateGen fromOr + +impliesPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +impliesPredicateGen = + Gen.subterm2 predicateGen predicateGen fromImplies + +iffPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +iffPredicateGen = + Gen.subterm2 predicateGen predicateGen fromIff + +notPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +notPredicateGen = + Gen.subterm predicateGen fromNot + termLikeGenImpl :: Range.Size -> Sort -> Gen (Maybe (TermLike VariableName)) termLikeGenImpl (Range.Size size) requestedSort = do allGenerators <- termGenerators diff --git a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs index a61ee64839..b08c3b86b3 100644 --- a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs +++ b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs @@ -1,11 +1,13 @@ module Test.Kore.Simplify.IntegrationProperty ( test_simplifiesToSimplified, test_regressionGeneratedTerms, + test_testingPredicateGen, ) where import Control.Exception ( ErrorCall (..), ) +import Pretty (pretty) import Control.Monad.Catch ( MonadThrow, catch, @@ -92,6 +94,12 @@ test_simplifiesToSimplified = traceM ("Error for input: " ++ unparseToString term) throwM err +test_testingPredicateGen :: TestTree +test_testingPredicateGen = + testPropertyWithoutSolver "TESTING" $ do + pred' <- forAll predicateGen + traceM (show . pretty $ pred') + test_regressionGeneratedTerms :: [TestTree] test_regressionGeneratedTerms = [ testCase "Term simplifier should not crash with not simplified error" $ do From 52146377e29150fbdda8d3213ef27a094b6e28c6 Mon Sep 17 00:00:00 2001 From: github-actions Date: Mon, 16 Aug 2021 17:26:37 +0000 Subject: [PATCH 2/6] Format with fourmolu --- kore/test/Test/ConsistentKore.hs | 4 ++-- kore/test/Test/Kore/Simplify/IntegrationProperty.hs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs index 59b9db4020..5bff08ad98 100644 --- a/kore/test/Test/ConsistentKore.hs +++ b/kore/test/Test/ConsistentKore.hs @@ -26,8 +26,6 @@ import Data.Text ( import qualified Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range -import Kore.Internal.From -import Kore.Internal.Predicate (Predicate) import qualified Kore.Attribute.Constructor as Attribute.Constructor ( Constructor (..), ) @@ -71,9 +69,11 @@ import qualified Kore.Internal.Alias as Internal ( import Kore.Internal.ApplicationSorts ( ApplicationSorts (ApplicationSorts), ) +import Kore.Internal.From import Kore.Internal.InternalMap import Kore.Internal.InternalSet import Kore.Internal.InternalString +import Kore.Internal.Predicate (Predicate) import qualified Kore.Internal.Symbol as Internal ( Symbol (Symbol), ) diff --git a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs index b08c3b86b3..e2501c6e1b 100644 --- a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs +++ b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs @@ -7,7 +7,6 @@ module Test.Kore.Simplify.IntegrationProperty ( import Control.Exception ( ErrorCall (..), ) -import Pretty (pretty) import Control.Monad.Catch ( MonadThrow, catch, @@ -57,6 +56,7 @@ import qualified Kore.Simplify.Pattern as Pattern ( import Kore.Simplify.Simplify import Kore.Unparser import Prelude.Kore +import Pretty (pretty) import qualified SMT import Test.ConsistentKore import qualified Test.Kore.Rewrite.MockSymbols as Mock From 7c2c9e0d09a7b5c79682d2714f4514e6efd4e561 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 17 Aug 2021 13:48:50 +0300 Subject: [PATCH 3/6] Implement Predicate generator, clean-up --- kore/test/Test/ConsistentKore.hs | 145 ++++++++---------- .../Test/Kore/Simplify/IntegrationProperty.hs | 22 +-- 2 files changed, 72 insertions(+), 95 deletions(-) diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs index 59b9db4020..a897271d9c 100644 --- a/kore/test/Test/ConsistentKore.hs +++ b/kore/test/Test/ConsistentKore.hs @@ -1,10 +1,8 @@ module Test.ConsistentKore ( CollectionSorts (..), Setup (..), - runTermGen, - termLikeGen, - -- testing - predicateGen, + runKoreGen, + patternGen, ) where import qualified Control.Arrow as Arrow @@ -14,6 +12,8 @@ import Control.Monad.Reader ( ) import qualified Control.Monad.Reader as Reader import qualified Data.Functor.Foldable as Recursive +import Kore.Internal.Pattern (Pattern) +import qualified Kore.Internal.Pattern as Pattern import qualified Data.HashMap.Strict as HashMap import qualified Data.List as List ( foldl', @@ -86,15 +86,11 @@ import Kore.Internal.TermLike ( mkApplyAlias, mkApplySymbol, mkBottom, - mkCeil, mkElemVar, - mkEquals, mkExists, - mkFloor, mkForall, mkIff, mkImplies, - mkIn, mkInternalBool, mkInternalInt, mkInternalList, @@ -190,8 +186,8 @@ data Setup = Setup type Gen = ReaderT (Setup, Context) Hedgehog.Gen -runTermGen :: Setup -> Gen a -> Hedgehog.Gen a -runTermGen +runKoreGen :: Setup -> Gen a -> Hedgehog.Gen a +runKoreGen setup@Setup{freeElementVariables, freeSetVariables} generator = Reader.runReaderT generator (setup, context) @@ -204,6 +200,12 @@ runTermGen , onlyConcrete = False } +patternGen :: Gen (Pattern VariableName) +patternGen = + Pattern.fromTermAndPredicate + <$> termLikeGen + <*> predicateGen + addQuantifiedSetVariable :: SetVariable VariableName -> Context -> Context addQuantifiedSetVariable variable @@ -232,8 +234,11 @@ requestConcrete = localContext (\context -> context{onlyConcrete = True}) termLikeGen :: Gen (TermLike VariableName) -termLikeGen = do - topSort <- sortGen +termLikeGen = + sortGen >>= termLikeGenWithSort + +termLikeGenWithSort :: Sort -> Gen (TermLike VariableName) +termLikeGenWithSort topSort = do maybeResult <- Gen.scale limitTermDepth $ Gen.sized (\size -> termLikeGenImpl size topSort) @@ -246,9 +251,8 @@ termLikeGen = do | otherwise = Range.Size 10 -- TODO: --- - will need the config for generating terms/variables -- - make generated predicates smaller -predicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +predicateGen :: Gen (Predicate VariableName) predicateGen = Gen.recursive Gen.choice @@ -258,28 +262,68 @@ predicateGen = , notPredicateGen , impliesPredicateGen , iffPredicateGen + , ceilGen + , floorGen + , equalsGen + , inGen + , existsPredicateGen + , forallPredicateGen ] -andPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +andPredicateGen :: Gen (Predicate VariableName) andPredicateGen = Gen.subterm2 predicateGen predicateGen fromAnd -orPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +orPredicateGen :: Gen (Predicate VariableName) orPredicateGen = Gen.subterm2 predicateGen predicateGen fromOr -impliesPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +impliesPredicateGen :: Gen (Predicate VariableName) impliesPredicateGen = Gen.subterm2 predicateGen predicateGen fromImplies -iffPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +iffPredicateGen :: Gen (Predicate VariableName) iffPredicateGen = Gen.subterm2 predicateGen predicateGen fromIff -notPredicateGen :: Hedgehog.MonadGen m => m (Predicate VariableName) +notPredicateGen :: Gen (Predicate VariableName) notPredicateGen = Gen.subterm predicateGen fromNot +ceilGen :: Gen (Predicate VariableName) +ceilGen = + fromCeil_ <$> termLikeGen + +floorGen :: Gen (Predicate VariableName) +floorGen = + fromFloor_ <$> termLikeGen + +equalsGen :: Gen (Predicate VariableName) +equalsGen = do + sort' <- sortGen + fromEquals_ + <$> termLikeGenWithSort sort' + <*> termLikeGenWithSort sort' + +inGen :: Gen (Predicate VariableName) +inGen = do + sort' <- sortGen + fromIn_ + <$> termLikeGenWithSort sort' + <*> termLikeGenWithSort sort' + +existsPredicateGen :: Gen (Predicate VariableName) +existsPredicateGen = do + sort' <- sortGen + variable <- elementVariableGen sort' + Gen.subterm predicateGen (fromExists variable) + +forallPredicateGen :: Gen (Predicate VariableName) +forallPredicateGen = do + sort' <- sortGen + variable <- elementVariableGen sort' + Gen.subterm predicateGen (fromForall variable) + termLikeGenImpl :: Range.Size -> Sort -> Gen (Maybe (TermLike VariableName)) termLikeGenImpl (Range.Size size) requestedSort = do allGenerators <- termGenerators @@ -375,19 +419,15 @@ termGenerators = do filterGeneratorsAndGroup [ andGenerator , bottomGenerator - , ceilGenerator - , equalsGenerator , existsGenerator - , floorGenerator , forallGenerator , iffGenerator , impliesGenerator - , inGenerator - , muGenerator , notGenerator - , nuGenerator , orGenerator , topGenerator + , nuGenerator + , muGenerator ] literals <- filterGeneratorsAndGroup @@ -464,27 +504,6 @@ unaryOperatorGenerator builder = return (builder <$> child) -- Maybe functor -unaryFreeSortOperatorGenerator :: - (Sort -> TermLike VariableName -> TermLike VariableName) -> - TermGenerator -unaryFreeSortOperatorGenerator builder = - TermGenerator - { arity = 1 - , sort = AnySort - , attributes = - AttributeRequirements - { isConstructorLike = False - , isConcrete = True - } - , generator = worker - } - where - worker childGenerator resultSort = do - childSort <- sortGen - child <- childGenerator childSort - return - (builder resultSort <$> child) -- Maybe functor - unaryQuantifiedElementOperatorGenerator :: (ElementVariable VariableName -> TermLike VariableName -> TermLike VariableName) -> TermGenerator @@ -534,28 +553,6 @@ muNuOperatorGenerator builder = return (builder quantifiedVariable <$> child) -- Maybe functor -binaryFreeSortOperatorGenerator :: - (Sort -> TermLike VariableName -> TermLike VariableName -> TermLike VariableName) -> - TermGenerator -binaryFreeSortOperatorGenerator builder = - TermGenerator - { arity = 2 - , sort = AnySort - , attributes = - AttributeRequirements - { isConstructorLike = False - , isConcrete = True - } - , generator = worker - } - where - worker childGenerator resultSort = do - childSort <- sortGen - child1 <- childGenerator childSort - child2 <- childGenerator childSort - return - (builder resultSort <$> child1 <*> child2) -- Maybe applicative - binaryOperatorGenerator :: (TermLike VariableName -> TermLike VariableName -> TermLike VariableName) -> TermGenerator @@ -583,18 +580,9 @@ andGenerator = binaryOperatorGenerator mkAnd bottomGenerator :: TermGenerator bottomGenerator = nullaryFreeSortOperatorGenerator mkBottom -ceilGenerator :: TermGenerator -ceilGenerator = unaryFreeSortOperatorGenerator mkCeil - -equalsGenerator :: TermGenerator -equalsGenerator = binaryFreeSortOperatorGenerator mkEquals - existsGenerator :: TermGenerator existsGenerator = unaryQuantifiedElementOperatorGenerator mkExists -floorGenerator :: TermGenerator -floorGenerator = unaryFreeSortOperatorGenerator mkFloor - forallGenerator :: TermGenerator forallGenerator = unaryQuantifiedElementOperatorGenerator mkForall @@ -604,9 +592,6 @@ iffGenerator = binaryOperatorGenerator mkIff impliesGenerator :: TermGenerator impliesGenerator = binaryOperatorGenerator mkImplies -inGenerator :: TermGenerator -inGenerator = binaryFreeSortOperatorGenerator mkIn - muGenerator :: TermGenerator muGenerator = muNuOperatorGenerator mkMu diff --git a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs index b08c3b86b3..629f125e74 100644 --- a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs +++ b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs @@ -1,13 +1,11 @@ module Test.Kore.Simplify.IntegrationProperty ( test_simplifiesToSimplified, test_regressionGeneratedTerms, - test_testingPredicateGen, ) where import Control.Exception ( ErrorCall (..), ) -import Pretty (pretty) import Control.Monad.Catch ( MonadThrow, catch, @@ -48,7 +46,7 @@ import Kore.Rewrite.Axiom.EvaluationStrategy ( ) import Kore.Rewrite.RewritingVariable ( RewritingVariableName, - mkRewritingTerm, + mkRewritingPattern, ) import qualified Kore.Simplify.Data as Simplification import qualified Kore.Simplify.Pattern as Pattern ( @@ -70,20 +68,20 @@ import Test.Tasty.HUnit.Ext test_simplifiesToSimplified :: TestTree test_simplifiesToSimplified = testPropertyWithoutSolver "simplify returns simplified pattern" $ do - term <- forAll (runTermGen Mock.generatorSetup termLikeGen) - let term' = mkRewritingTerm term + patt <- forAll (runKoreGen Mock.generatorSetup patternGen) + let patt' = mkRewritingPattern patt (annotate . unlines) - [" ***** unparsed input =", unparseToString term, " ***** "] + [" ***** unparsed input =", unparseToString patt, " ***** "] simplified <- catch - (evaluateT (Pattern.fromTermLike term')) - (exceptionHandler term) + (evaluateT patt') + (exceptionHandler patt) (===) True (OrPattern.isSimplified sideRepresentation simplified) where -- Discard exceptions that are normal for randomly generated patterns. exceptionHandler :: MonadThrow m => - TermLike VariableName -> + Pattern VariableName -> ErrorCall -> PropertyT m a exceptionHandler term err@(ErrorCallWithLocation message _location) @@ -94,12 +92,6 @@ test_simplifiesToSimplified = traceM ("Error for input: " ++ unparseToString term) throwM err -test_testingPredicateGen :: TestTree -test_testingPredicateGen = - testPropertyWithoutSolver "TESTING" $ do - pred' <- forAll predicateGen - traceM (show . pretty $ pred') - test_regressionGeneratedTerms :: [TestTree] test_regressionGeneratedTerms = [ testCase "Term simplifier should not crash with not simplified error" $ do From 9eed31624f91a2bcf4e28d88a8c033b7b9dddb75 Mon Sep 17 00:00:00 2001 From: github-actions Date: Tue, 17 Aug 2021 10:51:55 +0000 Subject: [PATCH 4/6] Format with fourmolu --- kore/test/Test/ConsistentKore.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs index a993636278..6d55da819e 100644 --- a/kore/test/Test/ConsistentKore.hs +++ b/kore/test/Test/ConsistentKore.hs @@ -12,8 +12,6 @@ import Control.Monad.Reader ( ) import qualified Control.Monad.Reader as Reader import qualified Data.Functor.Foldable as Recursive -import Kore.Internal.Pattern (Pattern) -import qualified Kore.Internal.Pattern as Pattern import qualified Data.HashMap.Strict as HashMap import qualified Data.List as List ( foldl', @@ -73,6 +71,8 @@ import Kore.Internal.From import Kore.Internal.InternalMap import Kore.Internal.InternalSet import Kore.Internal.InternalString +import Kore.Internal.Pattern (Pattern) +import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate (Predicate) import qualified Kore.Internal.Symbol as Internal ( Symbol (Symbol), From 5c88ecbd66e8d6ee5c8e70c79fde68e5db38e09c Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 17 Aug 2021 14:13:18 +0300 Subject: [PATCH 5/6] Remove todo --- kore/test/Test/ConsistentKore.hs | 2 -- 1 file changed, 2 deletions(-) diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs index 6d55da819e..2d92b6b77d 100644 --- a/kore/test/Test/ConsistentKore.hs +++ b/kore/test/Test/ConsistentKore.hs @@ -250,8 +250,6 @@ termLikeGenWithSort topSort = do | s < 10 = Range.Size s | otherwise = Range.Size 10 --- TODO: --- - make generated predicates smaller predicateGen :: Gen (Predicate VariableName) predicateGen = Gen.recursive From eb246e24e3712c2930f32d60d41ab55f85719ad8 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 17 Aug 2021 14:23:52 +0300 Subject: [PATCH 6/6] Remove redundant import --- kore/test/Test/Kore/Simplify/IntegrationProperty.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs index 221800881c..629f125e74 100644 --- a/kore/test/Test/Kore/Simplify/IntegrationProperty.hs +++ b/kore/test/Test/Kore/Simplify/IntegrationProperty.hs @@ -55,7 +55,6 @@ import qualified Kore.Simplify.Pattern as Pattern ( import Kore.Simplify.Simplify import Kore.Unparser import Prelude.Kore -import Pretty (pretty) import qualified SMT import Test.ConsistentKore import qualified Test.Kore.Rewrite.MockSymbols as Mock