From f3ac20d2829c28a6ba3dd61dd792b4b0af0bc1d6 Mon Sep 17 00:00:00 2001 From: Ana Pantilie Date: Fri, 17 Feb 2023 13:28:53 +0200 Subject: [PATCH 1/2] WIP: allow certain recursive axioms --- kore/src/Kore/Equation/Application.hs | 28 +++++++++++++------------- kore/src/Kore/Rewrite/SMT/Evaluator.hs | 3 +++ 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 514df02f70..2aaf3ce726 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -22,6 +22,7 @@ import Control.Error ( import Control.Monad ( (>=>), ) +import Data.List (delete) import Data.Map.Strict ( Map, ) @@ -89,6 +90,7 @@ import Kore.Log.DecidePredicateUnknown ( OnDecidePredicateUnknown (..), srcLoc, ) +import Kore.Rewrite.Axiom.Identifier (matchAxiomIdentifier) import Kore.Rewrite.Axiom.Matcher ( MatchResult, patternMatch, @@ -142,7 +144,7 @@ attemptEquation sideCondition termLike equation = do onDecidePredicateUnknown = case simplification of Attribute.NotSimplification -> ErrorDecidePredicateUnknown $srcLoc eqSrc Attribute.IsSimplification _ -> WarnDecidePredicateUnknown $srcLoc eqSrc - checkRequires onDecidePredicateUnknown sideCondition predicate requires + checkRequires equation onDecidePredicateUnknown sideCondition predicate requires & whileCheckRequires return $ Pattern.withCondition right $ from @(Predicate _) ensures @@ -312,14 +314,14 @@ applyMatchResult equation matchResult@(predicate, substitution) = do checkConcreteVariable variable termLike | Set.member variable concretes - , (not . TermLike.isConstructorLike) termLike = + , (not . TermLike.isConstructorLike) termLike = [NotConcrete variable termLike] | otherwise = empty checkSymbolicVariable variable termLike | Set.member variable symbolics - , TermLike.isConstructorLike termLike = + , TermLike.isConstructorLike termLike = [NotSymbolic variable termLike] | otherwise = empty @@ -344,6 +346,8 @@ Throws 'RequiresNotMet' if the 'Predicate's do not hold under the 'SideCondition'. -} checkRequires :: + -- | Original equation + Equation RewritingVariableName -> OnDecidePredicateUnknown -> SideCondition RewritingVariableName -> -- | requires from matching @@ -351,19 +355,16 @@ checkRequires :: -- | requires from 'Equation' Predicate RewritingVariableName -> ExceptT (CheckRequiresError RewritingVariableName) Simplifier () -checkRequires onUnknown sideCondition predicate requires = +checkRequires equation onUnknown sideCondition predicate requires = do let requires' = makeAndPredicate predicate requires -- The condition to refute: condition :: Condition RewritingVariableName condition = from @(Predicate _) (makeNotPredicate requires') return condition - -- First try to refute 'condition' without user-defined axioms: - >>= withoutAxioms . simplifyCondition - -- Next try to refute 'condition' including user-defined axioms: - >>= withAxioms . simplifyCondition - -- Finally, try to refute the simplified 'condition' using the - -- external solver: + >>= Simplifier.localAxiomEquations (removeAxiom equation) . simplifyCondition + >>= filterBranch + >>= simplifyCondition . Condition.forgetSimplified >>= filterBranch -- Collect the simplified results. If they are \bottom, then \and(predicate, @@ -397,10 +398,9 @@ checkRequires onUnknown sideCondition predicate requires = , negatedImplication } - withoutAxioms = - fmap Condition.forgetSimplified - . Simplifier.localAxiomEquations (const mempty) - withAxioms = id + removeAxiom a m = + let iden = matchAxiomIdentifier . left $ a + in Map.adjust (delete a) iden m refreshVariables :: SideCondition RewritingVariableName -> diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs index 2d4aba8b52..ff91ffcba7 100644 --- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs +++ b/kore/src/Kore/Rewrite/SMT/Evaluator.hs @@ -113,6 +113,7 @@ evalPredicate onUnknown predicate sideConditionM = case predicate of condition using an external SMT solver. -} evalConditional :: + HasCallStack => InternalVariable variable => OnDecidePredicateUnknown -> Conditional variable term -> @@ -132,6 +133,7 @@ filterMultiOr :: ( Ord term , TopBottom term , InternalVariable variable + , HasCallStack ) => Loc -> MultiOr (Conditional variable term) -> @@ -141,6 +143,7 @@ filterMultiOr hsLoc multiOr = do return (MultiOr.make (catMaybes elements)) where refute :: + HasCallStack => Conditional variable term -> Simplifier (Maybe (Conditional variable term)) refute p = From 78e47162fbc0ceb396e0d08a66bda342b0572c76 Mon Sep 17 00:00:00 2001 From: github-actions Date: Fri, 17 Feb 2023 11:32:31 +0000 Subject: [PATCH 2/2] Format with fourmolu --- kore/src/Kore/Equation/Application.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 2aaf3ce726..cd8a2b2090 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -314,14 +314,14 @@ applyMatchResult equation matchResult@(predicate, substitution) = do checkConcreteVariable variable termLike | Set.member variable concretes - , (not . TermLike.isConstructorLike) termLike = + , (not . TermLike.isConstructorLike) termLike = [NotConcrete variable termLike] | otherwise = empty checkSymbolicVariable variable termLike | Set.member variable symbolics - , TermLike.isConstructorLike termLike = + , TermLike.isConstructorLike termLike = [NotSymbolic variable termLike] | otherwise = empty