From 882d567f0376fdfa6091662f87b3f232cf3c4759 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 15 Apr 2020 03:54:03 +0530 Subject: [PATCH 1/3] drivers/base: Merge and cells --- prover/drivers/base.md | 6 +- prover/drivers/kore-driver.md | 14 +- prover/drivers/smt-driver.md | 14 +- prover/strategies/apply-equation.md | 6 +- prover/strategies/apply.md | 2 +- prover/strategies/core.md | 20 +-- prover/strategies/inst-exists.md | 4 +- prover/strategies/intros.md | 2 +- prover/strategies/knaster-tarski.md | 126 +++++++++--------- prover/strategies/matching.md | 56 ++++---- prover/strategies/reflexivity.md | 4 +- .../replace-evar-with-func-constant.md | 8 +- prover/strategies/simplification.md | 48 +++---- prover/strategies/smt.md | 16 +-- prover/strategies/unfolding.md | 24 ++-- prover/t/avl-implies-bst.kore.expected | 4 +- prover/t/bst-implies-bt.kore.expected | 4 +- .../t/emptyset-implies-isempty.kore.expected | 4 +- prover/t/fermat-3.smt2.expected | 4 +- prover/t/isMod4-implies-isEven.smt2.expected | 4 +- ...eft-implies-listSegmentRight.kore.expected | 4 +- ...egmentLeft-list-implies-list.kore.expected | 4 +- ...ortedlist-implies-sortedlist.kore.expected | 4 +- ...ight-implies-listSegmentLeft.kore.expected | 4 +- ...plies-listSegmentRightLength.kore.expected | 4 +- ...tedLength-implies-listLength.kore.expected | 4 +- ...tedLength-implies-listSorted.kore.expected | 4 +- prover/t/pythagoras.smt2.expected | 4 +- prover/t/qf_shid_entl-01.tst.smt2.expected | 4 +- prover/t/qf_shid_entl-02.tst.smt2.expected | 4 +- prover/t/qf_shid_entl-03.tst.smt2.expected | 4 +- prover/t/qf_shid_entl-04.tst.smt2.expected | 4 +- prover/t/qf_shid_entl-05.tst.smt2.expected | 4 +- prover/t/qf_shid_entl-06.tst.smt2.expected | 4 +- .../t/sortedlist-implies-list.kore.expected | 4 +- prover/t/trivial-var.smt2.expected | 4 +- prover/t/trivial.smt2.expected | 4 +- prover/t/zero-iszero.smt2.expected | 4 +- prover/utils/load-named.md | 2 +- 39 files changed, 221 insertions(+), 223 deletions(-) diff --git a/prover/drivers/base.md b/prover/drivers/base.md index 5577e6cdb..9c51d7f5f 100644 --- a/prover/drivers/base.md +++ b/prover/drivers/base.md @@ -3,7 +3,7 @@ Configuration The configuration consists of a assoc-commutative bag of goals. Only goals marked `` are executed to control the non-determinism in the system. The -`` cell contains the Matching Logic Pattern for which we are searching for a +`` cell contains the Matching Logic Pattern for which we are searching for a proof. The `` cell contains an imperative language that controls which (high-level) proof rules are used to complete the goal. The `` cell stores a log of the strategies used in the search of a proof and other debug @@ -21,20 +21,18 @@ module PROVER-CONFIGURATION configuration - $COMMANDLINE:CommandLine ~> $PGM:Pgm 1 true:Bool .K .K - .K + $COMMANDLINE:CommandLine ~> $PGM:Pgm .K .K .K - .K diff --git a/prover/drivers/kore-driver.md b/prover/drivers/kore-driver.md index 73c58efc9..ee24131d5 100644 --- a/prover/drivers/kore-driver.md +++ b/prover/drivers/kore-driver.md @@ -67,18 +67,18 @@ in the subgoal and the claim of the named goal remains intact. ... - rule claim NAME : PATTERN - strategy STRAT - => .K - ... - - + rule + claim NAME : PATTERN + strategy STRAT + => .K + ... + ( .Bag => NAME true:Bool .K - PATTERN + PATTERN subgoal(PATTERN, STRAT) success .Bag diff --git a/prover/drivers/smt-driver.md b/prover/drivers/smt-driver.md index 6e4aef716..5d9323b60 100644 --- a/prover/drivers/smt-driver.md +++ b/prover/drivers/smt-driver.md @@ -318,18 +318,18 @@ module DRIVER-SMT rule #containsSpatialPatterns(.Patterns, _) => false rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S) - rule #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED) - ~> (check-sat) - => #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED) - ... - - + rule + #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED) + ~> (check-sat) + => #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED) + ... + ( .Bag => !N:ClaimName true:Bool .K - \implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) + \implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) STRAT EXPECTED .Bag diff --git a/prover/strategies/apply-equation.md b/prover/strategies/apply-equation.md index ea4bc53b9..0a666c308 100644 --- a/prover/strategies/apply-equation.md +++ b/prover/strategies/apply-equation.md @@ -119,7 +119,7 @@ module STRATEGY-APPLY-EQUATION ) ... - T + T syntax KItem ::= "#apply-equation3" "(" "hypothesis:" Pattern @@ -138,9 +138,9 @@ module STRATEGY-APPLY-EQUATION => instantiateAssumptions(Subst, P) ~> createSubgoalsWithStrategies(strats: Ss, result: noop) ... - + _ => cool(heated: Heated, term: substMap(R, Subst)) - + syntax KItem ::= "createSubgoalsWithStrategies" "(" "strats:" Strategies diff --git a/prover/strategies/apply.md b/prover/strategies/apply.md index 4ffe72f12..81a0a69c9 100644 --- a/prover/strategies/apply.md +++ b/prover/strategies/apply.md @@ -37,7 +37,7 @@ module STRATEGY-APPLY Strat ) ... - G + G syntax KItem ::= #apply1(Pattern, MatchResult, Strategy) diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 4a5a95ac9..f8e6a17c3 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -116,7 +116,7 @@ Proving a goal may involve proving other subgoals: true PARENT SUBSTRAT - SUBGOAL + SUBGOAL LC TRACE ... @@ -151,7 +151,7 @@ all succeed, it succeeds: rule ((S1 & S2) => subgoal(GOAL, S1) ~> #hole & S2) - GOAL:Pattern + GOAL:Pattern ... ... @@ -177,7 +177,7 @@ approach succeeds: rule ((S1 | S2) => subgoal(GOAL, S1) ~> #hole | S2 ) - GOAL:Pattern + GOAL:Pattern ... ... @@ -199,7 +199,7 @@ Internal strategy used to implement `or-split` and `and-split`. ```k syntax Strategy ::= "replace-goal" "(" Pattern ")" - rule _ => NEWGOAL + rule _ => NEWGOAL replace-goal(NEWGOAL) => noop ... ``` @@ -212,7 +212,7 @@ Internal strategy used to implement `or-split` and `and-split`. ``` ```k - rule \or(GOALS) + rule \or(GOALS) or-split => #orSplit(GOALS) ... syntax Strategy ::= "#orSplit" "(" Patterns ")" [function] @@ -230,16 +230,16 @@ Internal strategy used to implement `or-split` and `and-split`. ``` ```k - rule \implies(LHS, \exists { Vs } \and(\or(RHSs), REST)) + rule \implies(LHS, \exists { Vs } \and(\or(RHSs), REST)) or-split-rhs => #orSplitImplication(LHS, Vs, RHSs, REST) ... - rule \implies(LHS, \exists { Vs } \and(RHSs, REST)) + rule \implies(LHS, \exists { Vs } \and(RHSs, REST)) or-split-rhs => noop ... requires notBool isDisjunction(RHSs) - rule \implies(LHS, \exists { Vs } \and(.Patterns)) + rule \implies(LHS, \exists { Vs } \and(.Patterns)) or-split-rhs => noop ... - rule \implies(LHS, \exists { Vs } \and(.Patterns)) + rule \implies(LHS, \exists { Vs } \and(.Patterns)) or-split-rhs => noop ... syntax Strategy ::= "#orSplitImplication" "(" Pattern "," Patterns "," Patterns "," Patterns ")" [function] @@ -257,7 +257,7 @@ Internal strategy used to implement `or-split` and `and-split`. ``` ```k - rule \and(GOALS) + rule \and(GOALS) and-split => #andSplit(GOALS) ... syntax Strategy ::= "#andSplit" "(" Patterns ")" [function] diff --git a/prover/strategies/inst-exists.md b/prover/strategies/inst-exists.md index e1f6da9f9..ba2334732 100644 --- a/prover/strategies/inst-exists.md +++ b/prover/strategies/inst-exists.md @@ -16,9 +16,9 @@ module STRATEGY-INST-EXISTS inst-exists(V, T, Strat) => subgoal(\functionalPattern(T), Strat) & noop ... - + P => instExists(P, V, T) - + syntax Pattern ::= instExists(Pattern, Variable, Pattern) [function] diff --git a/prover/strategies/intros.md b/prover/strategies/intros.md index a7a4f2809..577c33d9e 100644 --- a/prover/strategies/intros.md +++ b/prover/strategies/intros.md @@ -11,7 +11,7 @@ module STRATEGY-INTROS imports KORE-HELPERS rule intros Name => noop ... - \implies(H, G) => G + \implies(H, G) => G (.Bag => axiom Name : H ) ... diff --git a/prover/strategies/knaster-tarski.md b/prover/strategies/knaster-tarski.md index 097b7ce7f..985de8704 100644 --- a/prover/strategies/knaster-tarski.md +++ b/prover/strategies/knaster-tarski.md @@ -50,7 +50,7 @@ for guessing an instantiation of the inductive hypothesis. ```k rule kt => kt # .KTFilter ... - rule \implies(\and(LHS), RHS) + rule \implies(\and(LHS), RHS) kt # FILTER => getKTUnfoldables(LHS) ~> kt # FILTER ... @@ -89,7 +89,7 @@ for guessing an instantiation of the inductive hypothesis. ```k rule kt-unf => kt-unf # .KTFilter ... - rule \implies(\and(LHS), RHS) + rule \implies(\and(LHS), RHS) kt-unf # FILTER => getKTUnfoldables(LHS) ~> kt-unf # FILTER ... @@ -139,9 +139,9 @@ for guessing an instantiation of the inductive hypothesis. ```k syntax Strategy ::= "kt-wrap" "(" Pattern ")" - rule \implies(\and(LHS:Patterns), RHS) + rule \implies(\and(LHS:Patterns), RHS) => \implies(LRP, implicationContext(\and(#hole, (LHS -Patterns LRP)), RHS)) - + kt-wrap(LRP) => noop ... .K => kt-wrap(LRP) ... requires LRP in LHS @@ -151,13 +151,13 @@ for guessing an instantiation of the inductive hypothesis. ## kt-wrap (SL) ```k - rule \implies(\and(sep(LSPATIAL), LCONSTRAINT:Patterns), RHS) + rule \implies(\and(sep(LSPATIAL), LCONSTRAINT:Patterns), RHS) => \implies(LRP, implicationContext(\and( sep(#hole, (LSPATIAL -Patterns LRP)) , LCONSTRAINT ) , RHS) ) - + kt-wrap(LRP) => noop ... .K => kt-wrap(LRP) ... requires LRP in LSPATIAL @@ -170,12 +170,12 @@ for guessing an instantiation of the inductive hypothesis. ```k syntax Strategy ::= "kt-forall-intro" - rule \implies(LHS, RHS) #as GOAL + rule \implies(LHS, RHS) #as GOAL => \implies( LHS , \forall { getUniversalVariables(GOAL) -Patterns getFreeVariables(LHS, .Patterns) } RHS ) - + kt-forall-intro => noop ... ``` @@ -185,7 +185,7 @@ for guessing an instantiation of the inductive hypothesis. ```k syntax Strategy ::= "kt-forall-elim" - rule \implies(LHS, \forall { Vs } RHS) => \implies(LHS, RHS) + rule \implies(LHS, \forall { Vs } RHS) => \implies(LHS, RHS) kt-forall-elim => noop ... requires getFreeVariables(LHS) -Patterns Vs ==K getFreeVariables(LHS) ``` @@ -195,16 +195,16 @@ for guessing an instantiation of the inductive hypothesis. ```k syntax Strategy ::= "kt-unfold" - rule \implies( LRP(ARGS) #as LHS + rule \implies( LRP(ARGS) #as LHS => substituteBRPs(unfold(LHS), LRP, ARGS, RHS) , RHS ) - + kt-unfold => noop ... requires removeDuplicates(ARGS) ==K ARGS andBool isUnfoldable(LRP) - rule \implies(LRP(ARGS), RHS) - + rule \implies(LRP(ARGS), RHS) + kt-unfold => fail ... requires removeDuplicates(ARGS) =/=K ARGS andBool isUnfoldable(LRP) @@ -245,9 +245,9 @@ for guessing an instantiation of the inductive hypothesis. ```k syntax Strategy ::= "kt-unwrap" - rule \implies(LHS, \forall { UNIV } implicationContext(CTX, RHS)) + rule \implies(LHS, \forall { UNIV } implicationContext(CTX, RHS)) => \implies(subst(CTX, #hole, LHS), RHS) - + kt-unwrap => noop ... ``` @@ -261,11 +261,11 @@ for guessing an instantiation of the inductive hypothesis. If there are no implication contexts to collapse, we are done: ```k - rule GOAL + rule GOAL kt-collapse => noop ... requires notBool(hasImplicationContext(GOAL)) - rule GOAL + rule GOAL imp-ctx-unfold => noop ... requires notBool(hasImplicationContext(GOAL)) ``` @@ -276,9 +276,9 @@ Bring terms containing the implication context to the front: ```k // FOL case - rule \implies(\and(P, Ps) #as LHS, RHS) + rule \implies(\and(P, Ps) #as LHS, RHS) => \implies(\and(Ps ++Patterns P), RHS) - + kt-collapse ... requires notBool hasImplicationContext(P) andBool hasImplicationContext(LHS) @@ -286,16 +286,16 @@ Bring terms containing the implication context to the front: ```k // SL case - rule \implies(\and((sep(S, Ss) #as LSPATIAL), Ps), RHS) + rule \implies(\and((sep(S, Ss) #as LSPATIAL), Ps), RHS) => \implies(\and(sep(Ss ++Patterns S), Ps), RHS) - + kt-collapse ... requires notBool hasImplicationContext(S) andBool hasImplicationContext(LSPATIAL) - rule \implies(\and((sep(S, Ss) #as LSPATIAL), Ps), RHS) + rule \implies(\and((sep(S, Ss) #as LSPATIAL), Ps), RHS) => \implies(\and(sep(Ss ++Patterns S), Ps), RHS) - + imp-ctx-unfold ... requires notBool hasImplicationContext(S) andBool hasImplicationContext(LSPATIAL) @@ -308,22 +308,22 @@ Move #holes to the front // be better? ```k - rule \implies(\and(\forall { _ } + rule \implies(\and(\forall { _ } implicationContext( \and(P, Ps) => \and(Ps ++Patterns P) , _) , _), _) - + kt-collapse ... requires P =/=K #hole:Pattern andBool #hole in Ps - rule \implies(\and(sep(\forall { _ } + rule \implies(\and(sep(\forall { _ } implicationContext( \and(P, Ps) => \and(Ps ++Patterns P) , _) ,_ ), _), _) - + kt-collapse ... requires P =/=K #hole:Pattern andBool #hole in Ps @@ -335,7 +335,7 @@ In the FOL case, we create an implication, and dispatch that to the smt solver using `kt-solve-implications` ```k - rule \implies(\and( \forall { UNIVs } + rule \implies(\and( \forall { UNIVs } ( implicationContext( \and(#hole, CTXLHS:Patterns) , CTXRHS:Pattern ) @@ -345,7 +345,7 @@ solver using `kt-solve-implications` ) , RHS:Pattern ) - + kt-collapse ... ``` @@ -359,7 +359,7 @@ Next, duplicate constraints are removed using the ad-hoc rule below until the im context has no constraints. ```k - rule \implies(\and( sep ( \forall { UNIVs } + rule \implies(\and( sep ( \forall { UNIVs } implicationContext( \and(sep(#hole, CTXLHS:Patterns), CTXLCONSTRAINTS) , _) , LSPATIAL ) @@ -367,7 +367,7 @@ context has no constraints. ) , RHS:Pattern ) - + kt-collapse => with-each-match( #match(terms: LSPATIAL, pattern: CTXLHS, variables: UNIVs) , kt-collapse @@ -378,7 +378,7 @@ context has no constraints. ``` ```k - rule \implies(\and( ( sep ( \forall { UNIVs => .Patterns } + rule \implies(\and( ( sep ( \forall { UNIVs => .Patterns } ( implicationContext( \and(sep(_), CTXLCONSTRAINTS), CTXRHS ) #as CTX => substMap(CTX, SUBST) ) @@ -389,7 +389,7 @@ context has no constraints. ) , RHS:Pattern ) - + ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) => kt-collapse ... @@ -397,7 +397,7 @@ context has no constraints. requires UNIVs =/=K .Patterns andBool UNIVs -Patterns fst(unzip(SUBST)) ==K .Patterns - rule \implies(\and( ( sep ( \forall { UNIVs => .Patterns } + rule \implies(\and( ( sep ( \forall { UNIVs => .Patterns } ( implicationContext( \and(sep(_), CTXLCONSTRAINTS), CTXRHS ) #as CTX ) , LSPATIAL @@ -407,7 +407,7 @@ context has no constraints. ) , RHS:Pattern ) - + ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) => fail ... @@ -419,7 +419,7 @@ context has no constraints. Finally, we use matching on the no universal quantifiers case to collapse the context. ```k - rule \implies(\and( sep ( \forall { .Patterns } + rule \implies(\and( sep ( \forall { .Patterns } implicationContext( \and(sep(#hole, CTXLHS:Patterns)) , _) , LSPATIAL ) @@ -427,7 +427,7 @@ Finally, we use matching on the no universal quantifiers case to collapse the co ) , RHS:Pattern ) - + kt-collapse => with-each-match( #match(terms: LSPATIAL, pattern: CTXLHS, variables: .Patterns) , kt-collapse @@ -435,7 +435,7 @@ Finally, we use matching on the no universal quantifiers case to collapse the co ... - rule \implies( \and( ( sep ( \forall { .Patterns } + rule \implies( \and( ( sep ( \forall { .Patterns } implicationContext( \and(sep(_)) , CTXRHS) , LSPATIAL ) @@ -445,7 +445,7 @@ Finally, we use matching on the no universal quantifiers case to collapse the co ) , RHS:Pattern ) - + ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) => kt-collapse ... @@ -455,7 +455,7 @@ Finally, we use matching on the no universal quantifiers case to collapse the co TODO: This is pretty adhoc: Remove constraints in the context that are already in the LHS ```k - rule \implies(\and( sep ( \forall { .Patterns } + rule \implies(\and( sep ( \forall { .Patterns } implicationContext( \and( sep(_) , ( CTXCONSTRAINT, CTXCONSTRAINTs => CTXCONSTRAINTs @@ -467,12 +467,12 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ) , RHS:Pattern ) - + kt-collapse ... requires isPredicatePattern(CTXCONSTRAINT) andBool CTXCONSTRAINT in LHS - rule \implies(\and( sep ( \forall { .Patterns } + rule \implies(\and( sep ( \forall { .Patterns } implicationContext( \and( sep(_) , ( CTXCONSTRAINT, CTXCONSTRAINTs ) ) , _) @@ -482,7 +482,7 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ) , RHS:Pattern ) - + kt-collapse => fail ... requires isPredicatePattern(CTXCONSTRAINT) andBool notBool (CTXCONSTRAINT in LHS) @@ -495,7 +495,7 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ``` ```k - rule \implies(\and( sep ( \forall { UNIVs } + rule \implies(\and( sep ( \forall { UNIVs } implicationContext( \and( sep( #hole , CTXLHS:Patterns ) @@ -509,11 +509,11 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ) , RHS:Pattern ) - + imp-ctx-unfold => right-unfold-eachRRP(getUnfoldables(CTXLHS)) ... requires UNIVs =/=K .Patterns - rule \implies(\and( sep ( \forall { .Patterns } + rule \implies(\and( sep ( \forall { .Patterns } implicationContext( \and(sep(#hole, CTXLHS:Patterns)) , _) , LSPATIAL ) @@ -521,7 +521,7 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ) , RHS:Pattern ) - + imp-ctx-unfold => right-unfold-eachRRP(getUnfoldables(CTXLHS)) ... ``` @@ -542,22 +542,22 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i => filterVariablesBySort(Vs, S) [owise] // TODO: Move to "normalize" strategy - rule \implies(\and(\and(Ps1), Ps2), RHS) + rule \implies(\and(\and(Ps1), Ps2), RHS) => \implies(\and(Ps1 ++Patterns Ps2), RHS) - + kt-collapse ... - rule \implies(\and(_, ( \and(Ps1), Ps2 + rule \implies(\and(_, ( \and(Ps1), Ps2 => Ps1 ++Patterns Ps2)) , RHS) - + kt-collapse ... - rule \implies(\and( _ + rule \implies(\and( _ , (\exists { _ } P => P) , Ps) , _ ) - + kt-collapse ... ``` @@ -566,11 +566,11 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i > (alpha -> beta) /\ gamma -> psi ```k - rule \implies( \and(\forall { .Patterns } \implies(LHS, RHS), REST:Patterns) + rule \implies( \and(\forall { .Patterns } \implies(LHS, RHS), REST:Patterns) => \and(REST) , _ ) - + kt-solve-implications( STRAT) => ( kt-solve-implication( subgoal(\implies(\and(removeImplications(REST)), LHS), STRAT) , \and(LHS, RHS) @@ -587,18 +587,18 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i requires matchesImplication(P) rule removeImplications(.Patterns) => .Patterns - rule \implies( \and(P:Pattern, REST:Patterns) + rule \implies( \and(P:Pattern, REST:Patterns) => \and(REST ++Patterns P) , _ ) - + kt-solve-implications(_) ... requires hasImplication(REST) andBool notBool matchesImplication(P) - rule \implies(\and(LHS), _) + rule \implies(\and(LHS), _) kt-solve-implications(STRAT) => noop ... requires notBool hasImplication(LHS) @@ -628,14 +628,14 @@ If the subgoal in the first argument succeeds add the second argument to the LHS rule kt-solve-implication(fail, RHS) => noop ... rule kt-solve-implication(success, CONC) => noop ... - \implies(\and(LHS), RHS) + \implies(\and(LHS), RHS) => \implies(\and(CONC, LHS), RHS) - + ``` ```k syntax Strategy ::= "instantiate-universals-with-ground-terms" "(" Patterns /* universals */ "," Patterns /* ground terms */ ")" - rule \implies(\and(LHS), RHS) #as GOAL + rule \implies(\and(LHS), RHS) #as GOAL instantiate-universals-with-ground-terms => instantiate-universals-with-ground-terms(getForalls(LHS), removeDuplicates(getGroundTerms(GOAL))) ... @@ -648,14 +648,14 @@ If the subgoal in the first argument succeeds add the second argument to the LHS ... - rule \implies(\and(LHS => P, LHS), RHS) + rule \implies(\and(LHS => P, LHS), RHS) instantiate-universals-with-ground-terms( (\forall { .Patterns } P:Pattern , REST_FORALLs) => REST_FORALLs , _ ) ... requires notBool P in LHS - rule \implies(\and(LHS), RHS) + rule \implies(\and(LHS), RHS) instantiate-universals-with-ground-terms( (\forall { .Patterns } P:Pattern , REST_FORALLs) => REST_FORALLs , _ ) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index d6dcd269e..96c4aae5a 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -378,7 +378,7 @@ The `with-each-match` strategy Instantiate existentials using matching on the spatial part of goals: ```k - rule \implies(\and(sep(LSPATIAL), LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) + rule \implies(\and(sep(LSPATIAL), LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) match => with-each-match(#match( terms: LSPATIAL , pattern: RSPATIAL @@ -390,21 +390,21 @@ Instantiate existentials using matching on the spatial part of goals: requires isSpatialPattern(sep(LSPATIAL)) andBool isSpatialPattern(sep(RSPATIAL)) - rule \implies( \and( LSPATIAL, LHS) + rule \implies( \and( LSPATIAL, LHS) , \exists { Vs } \and( RHS ) => \exists { Vs -Patterns fst(unzip(SUBST)) } substMap(\and(RHS), SUBST) ) - + ( #matchResult(subst: SUBST, rest: .Patterns) ~> match ) => noop ... - rule \implies(LHS, \exists { Vs } \and(RSPATIAL, RHS)) + rule \implies(LHS, \exists { Vs } \and(RSPATIAL, RHS)) match => fail ... requires isPredicatePattern(LHS) andBool isSpatialPattern(RSPATIAL) - rule \implies(\and(LSPATIAL, LHS), \exists { Vs } RHS) + rule \implies(\and(LSPATIAL, LHS), \exists { Vs } RHS) match => fail ... requires isPredicatePattern(RHS) andBool isSpatialPattern(LSPATIAL) @@ -418,19 +418,19 @@ Instantiate existentials using matching on the spatial part of goals: ```k syntax Strategy ::= "match-pto" "(" Patterns ")" - rule \implies( \and(sep(LSPATIAL), LHS) + rule \implies( \and(sep(LSPATIAL), LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS) ) - + match-pto => match-pto(getPartiallyInstantiatedPtos(RSPATIAL, Vs)) ... rule match-pto(.Patterns) => noop ... - rule \implies( \and(sep(LSPATIAL), LHS:Patterns) + rule \implies( \and(sep(LSPATIAL), LHS:Patterns) , \exists { Vs } \and(sep(RSPATIAL), RHS:Patterns)) - + match-pto(P, Ps:Patterns) => with-each-match( #match( terms: LSPATIAL:Patterns @@ -443,13 +443,13 @@ Instantiate existentials using matching on the spatial part of goals: . match-pto(Ps:Patterns) ... - rule \implies( _ + rule \implies( _ , (\exists { Vs } \and( RHS )) => ( \exists { Vs -Patterns fst(unzip(SUBST)) } substMap(\and(RHS), SUBST) ) ) - + ( #matchResult(subst: SUBST, rest: _) ~> match-pto ) => noop ... @@ -502,7 +502,7 @@ Instantiate heap axioms: Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil ```k - rule \implies(\and((sep(LSPATIAL)), LCONSTRAINT), RHS) + rule \implies(\and((sep(LSPATIAL)), LCONSTRAINT), RHS) instantiate-axiom(\forall { Vs } \implies( \and(sep(AXIOM_LSPATIAL)) , AXIOM_RHS @@ -518,10 +518,10 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil requires isSpatialPattern(sep(AXIOM_LSPATIAL)) - rule \implies(\and((sep(_) #as LSPATIAL), (LCONSTRAINT => substMap(AXIOM_RHS, SUBST), LCONSTRAINT)) + rule \implies(\and((sep(_) #as LSPATIAL), (LCONSTRAINT => substMap(AXIOM_RHS, SUBST), LCONSTRAINT)) , RHS ) - + ( #matchResult( subst: SUBST, rest: _ ) , MRs ~> instantiate-axiom(\forall { Vs } \implies( _ @@ -536,40 +536,40 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil rule (.MatchResults ~> instantiate-axiom(_)) => noop ... - rule \implies( \and(sep(LSPATIAL), LCONSTRAINT) + rule \implies( \and(sep(LSPATIAL), LCONSTRAINT) , \exists{ Vs } \and(sep(RSPATIAL), RCONSTRAINT) ) => \implies(\and(LCONSTRAINT), \exists { Vs } \and(RCONSTRAINT)) - + spatial-patterns-equal => noop ... requires LSPATIAL -Patterns RSPATIAL ==K .Patterns andBool RSPATIAL -Patterns LSPATIAL ==K .Patterns - rule \implies( \and(sep(LSPATIAL), _) + rule \implies( \and(sep(LSPATIAL), _) , \exists{ Vs } \and(sep(RSPATIAL), _) ) - + spatial-patterns-equal => fail ... requires LSPATIAL -Patterns RSPATIAL =/=K .Patterns orBool RSPATIAL -Patterns LSPATIAL =/=K .Patterns ``` ```k - rule \implies( \and(sep( LSPATIAL ) , _ ) + rule \implies( \and(sep( LSPATIAL ) , _ ) , \exists {_} \and(sep( RSPATIAL ) , _ ) ) - + frame => frame(LSPATIAL intersect RSPATIAL) ... ``` ```k syntax Strategy ::= "frame" "(" Patterns ")" - rule \implies( LHS + rule \implies( LHS , \exists { .Patterns } \and( sep(_), RCONSTRAINTs ) ) - + frame(pto(LOC, VAL), Ps) => subgoal( \implies( LHS , \and(filterClausesInvolvingVariable(LOC, RCONSTRAINTs)) @@ -584,11 +584,11 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil ... - rule \implies( \and( sep(LSPATIAL => (LSPATIAL -Patterns P)) , LCONSTRAINTs ) + rule \implies( \and( sep(LSPATIAL => (LSPATIAL -Patterns P)) , LCONSTRAINTs ) , \exists { .Patterns } \and( (sep(RSPATIAL => RSPATIAL -Patterns P)) , (RCONSTRAINTs => RCONSTRAINTs -Patterns filterClausesInvolvingVariable(LOC, RCONSTRAINTs)) ) ) - + success ~> frame((pto(LOC, VAL) #as P), .Patterns) => .K @@ -597,11 +597,11 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil requires P in LSPATIAL andBool P in RSPATIAL - rule \implies( \and( sep(LSPATIAL => (LSPATIAL -Patterns P)) , LCONSTRAINTs ) + rule \implies( \and( sep(LSPATIAL => (LSPATIAL -Patterns P)) , LCONSTRAINTs ) , \exists { .Patterns } \and( (sep(RSPATIAL => RSPATIAL -Patterns P)) , RCONSTRAINTs ) ) - + frame((S:Symbol(_) #as P), Ps) => frame(Ps) ... @@ -627,12 +627,12 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil => .Patterns syntax Strategy ::= "subsume-spatial" - rule \implies( \and( sep(LSPATIAL:Patterns) , LCONSTRAINTs:Patterns) + rule \implies( \and( sep(LSPATIAL:Patterns) , LCONSTRAINTs:Patterns) => \and( LCONSTRAINTs:Patterns) , \exists { Vs:Patterns } \and( RHS:Patterns ) ) - + subsume-spatial => noop ... diff --git a/prover/strategies/reflexivity.md b/prover/strategies/reflexivity.md index 9691054cc..920554e51 100644 --- a/prover/strategies/reflexivity.md +++ b/prover/strategies/reflexivity.md @@ -5,10 +5,10 @@ module STRATEGY-REFLEXIVITY imports STRATEGIES-EXPORTED-SYNTAX rule reflexivity => success ... - \equals(P, P) + \equals(P, P) rule reflexivity => fail ... - \equals(P, Q) + \equals(P, Q) requires P =/=K Q diff --git a/prover/strategies/replace-evar-with-func-constant.md b/prover/strategies/replace-evar-with-func-constant.md index c968a64e4..7b0e4d8b0 100644 --- a/prover/strategies/replace-evar-with-func-constant.md +++ b/prover/strategies/replace-evar-with-func-constant.md @@ -18,7 +18,7 @@ module STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT replace-evar-with-func-constant .Variables => #rewfc(PatternsToVariables(getFreeVariables(P, .Patterns))) ... - P + P syntax Variables ::= PatternsToVariables(Patterns) [function] rule PatternsToVariables(.Patterns) => .Variables @@ -42,12 +42,12 @@ module STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT GId, VariableName2String(N))) ... GId - P + P requires V in getFreeVariables(P, .Patterns) rule #rewfc2(N{S}, Sym) => .K ... GId - P => subst(P, N{S}, Sym(.Patterns)) + P => subst(P, N{S}, Sym(.Patterns)) (.Bag => symbol Sym(.Sorts) : S @@ -58,7 +58,7 @@ module STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT rule #rewfc1(V) => "No such free variable" ... - P + P requires notBool (V in getFreeVariables(P, .Patterns)) endmodule diff --git a/prover/strategies/simplification.md b/prover/strategies/simplification.md index fcd4c86c5..a3a328dfb 100644 --- a/prover/strategies/simplification.md +++ b/prover/strategies/simplification.md @@ -16,7 +16,7 @@ module STRATEGY-SIMPLIFICATION ``` ```k - rule \implies(LHS => #lhsRemoveExistentials(LHS), RHS) + rule \implies(LHS => #lhsRemoveExistentials(LHS), RHS) remove-lhs-existential => noop ... syntax Pattern ::= #lhsRemoveExistentials(Pattern) [function] @@ -57,26 +57,26 @@ Normalize: ```k - rule P::Pattern => \and(P) + rule P::Pattern => \and(P) normalize ... requires \and(...) :/=K P andBool \implies(...) :/=K P - rule \and(P) => \implies(\and(.Patterns), \and(P)) + rule \and(P) => \implies(\and(.Patterns), \and(P)) normalize ... - rule \implies(LHS, \and(RHS)) + rule \implies(LHS, \and(RHS)) => \implies(LHS, \exists { .Patterns } \and(RHS)) - + normalize ... - rule \implies(\and(LHS), \exists { Es } \and(RHS)) + rule \implies(\and(LHS), \exists { Es } \and(RHS)) => \implies( \and(#normalizePs(#flattenAnds(#lhsRemoveExistentialsPs(LHS)))) , \exists { Es } \and(#normalizePs(#flattenAnds(RHS))) ) - + normalize => noop ... - rule \not(_) #as P => #normalize(P) + rule \not(_) #as P => #normalize(P) normalize => noop ... syntax Pattern ::= #normalize(Pattern) [function] @@ -104,7 +104,7 @@ Normalize: LHS terms of the form S(T, Vs) become S(V, Vs) /\ V = T ```k - rule \implies(LHS => #purify(LHS), RHS) ... + rule \implies(LHS => #purify(LHS), RHS) ... purify => noop ... syntax Pattern ::= #purify(Pattern) [function] @@ -148,7 +148,7 @@ obligation of the form R(T, Vs) => R(T', Vs') becomes R(V, Vs) => exists V', R(V', Vs') and V = V' ```k - rule \implies(LHS, RHS) + rule \implies(LHS, RHS) abstract => #getNewVariables(LHS, .Patterns) ~> #getNewVariables(RHS, .Patterns) @@ -156,13 +156,13 @@ R(V, Vs) => exists V', R(V', Vs') and V = V' ... - rule \implies(LHS, \and(\or(RHS))) + rule \implies(LHS, \and(\or(RHS))) => \implies( #abstract(LHS, VsLHS) , \exists{ VsRHS } \and( #dnf(\or(\and(#createEqualities(VsLHS, VsRHS)))) , #abstract(RHS, VsRHS) ) ) - + (VsLHS:Patterns ~> VsRHS:Patterns ~> abstract) => noop ... syntax Patterns ::= #getNewVariables(Pattern, Patterns) [function] @@ -214,10 +214,10 @@ R(V, Vs) => exists V', R(V', Vs') and V = V' Bring predicate constraints to the top of a term. ```k - rule \implies(\and(Ps) => #flattenAnd(#liftConstraints(\and(Ps))) + rule \implies(\and(Ps) => #flattenAnd(#liftConstraints(\and(Ps))) , \exists { _ } (\and(Rs) => #flattenAnd(#liftConstraints(\and(Rs)))) ) - + lift-constraints => noop ... syntax Pattern ::= #liftConstraints(Pattern) [function] @@ -268,7 +268,7 @@ Lift `\or`s on the left hand sides of implications ``` ```k - rule \implies(\or(LHSs), RHS) => \and( #liftOr(LHSs, RHS)) + rule \implies(\or(LHSs), RHS) => \and( #liftOr(LHSs, RHS)) lift-or => noop ... syntax Patterns ::= "#liftOr" "(" Patterns "," Pattern ")" [function] @@ -283,7 +283,7 @@ Lift `\or`s on the left hand sides of implications > (\forall .Patterns . phi(x, y)) -> psi(y) ```k - rule \implies(\forall { .Patterns } \and(LHS) => \and(LHS), RHS) + rule \implies(\forall { .Patterns } \and(LHS) => \and(LHS), RHS) simplify ... ``` @@ -292,7 +292,7 @@ Lift `\or`s on the left hand sides of implications > \exists X . phi(x, y) -> psi(y) ```k - rule \implies(\exists { _ } \and(LHS) => \and(LHS), RHS) + rule \implies(\exists { _ } \and(LHS) => \and(LHS), RHS) simplify ... ``` @@ -301,7 +301,7 @@ Lift `\or`s on the left hand sides of implications > LHS /\ phi -> RHS /\ phi ```k - rule \implies(\and(LHS), \exists { _ } \and(RHS => RHS -Patterns LHS)) + rule \implies(\and(LHS), \exists { _ } \and(RHS => RHS -Patterns LHS)) simplify => noop ... ``` @@ -314,18 +314,18 @@ Lift `\or`s on the left hand sides of implications ``` ```k - rule \implies( \and(LHS) , \exists { EXIST } \and(RHS) ) #as GOAL + rule \implies( \and(LHS) , \exists { EXIST } \and(RHS) ) #as GOAL (. => getAtomForcingInstantiation(RHS, getExistentialVariables(GOAL))) ~> instantiate-existentials ... - rule \implies( \and(LHS) , \exists { EXIST } \and(RHS) ) + rule \implies( \and(LHS) , \exists { EXIST } \and(RHS) ) => \implies( \and(LHS ++Patterns INSTANTIATION) , \exists { EXIST -Patterns getFreeVariables(INSTANTIATION) } \and(RHS -Patterns INSTANTIATION) ) - + (INSTANTIATION => .) ~> instantiate-existentials ... requires INSTANTIATION =/=K .Patterns @@ -355,7 +355,7 @@ Lift `\or`s on the left hand sides of implications ``` ```k - rule \implies(\and(LHS), _) + rule \implies(\and(LHS), _) substitute-equals-for-equals => (makeEqualitySubstitution(LHS) ~> substitute-equals-for-equals) ... @@ -367,11 +367,11 @@ Lift `\or`s on the left hand sides of implications requires SUBST ==K .Map - rule \implies( \and(LHS => removeTrivialEqualities(substPatternsMap(LHS, SUBST))) + rule \implies( \and(LHS => removeTrivialEqualities(substPatternsMap(LHS, SUBST))) , \exists { _ } ( \and(RHS => removeTrivialEqualities(substPatternsMap(RHS, SUBST))) ) ) - + (SUBST:Map ~> substitute-equals-for-equals) => substitute-equals-for-equals ... diff --git a/prover/strategies/smt.md b/prover/strategies/smt.md index fe2491b93..bfb84e10a 100644 --- a/prover/strategies/smt.md +++ b/prover/strategies/smt.md @@ -198,7 +198,7 @@ module STRATEGY-SMT imports STRATEGIES-EXPORTED-SYNTAX imports ML-TO-SMTLIB2 - rule GOAL + rule GOAL smt-z3 => if Z3CheckSAT(Z3Prelude ++SMTLIB2Script ML2SMTLIB(\not(GOAL))) ==K unsat then success @@ -208,10 +208,10 @@ module STRATEGY-SMT .K => smt-z3 ... - rule GOAL + rule GOAL smt-z3 => fail - rule GOAL + rule GOAL GId smt-cvc4 => if CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \not(GOAL), collectDeclarations(GId))) ==K unsat @@ -224,7 +224,7 @@ module STRATEGY-SMT requires isPredicatePattern(GOAL) // If the constraints are unsatisfiable, the entire term is unsatisfiable - rule \implies(\and(sep(_), LCONSTRAINTS), _) + rule \implies(\and(sep(_), LCONSTRAINTS), _) GId check-lhs-constraint-unsat => if CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(LCONSTRAINTS), collectDeclarations(GId))) ==K unsat @@ -241,7 +241,7 @@ module STRATEGY-SMT We have an optimized version of trying both: Only call z3 if cvc4 reports unknown. ```k - rule GOAL + rule GOAL smt => #fun( CVC4RESULT => if CVC4RESULT ==K unsat @@ -259,7 +259,7 @@ We have an optimized version of trying both: Only call z3 if cvc4 reports unknow ``` ```k - rule GOAL + rule GOAL GId smt-debug => wait ~> CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \not(GOAL), collectDeclarations(GId))):CheckSATResult @@ -288,12 +288,12 @@ module SMTLIB2-TEST-DRIVER imports Z3 imports CVC4 - configuration $PGM:Pattern + configuration $PGM:Pattern .K .K .K - rule IMPL + rule IMPL .K => ML2SMTLIB(\not(IMPL)) rule SCRIPT:SMTLIB2Script .K => Z3CheckSAT(Z3Prelude ++SMTLIB2Script SCRIPT) diff --git a/prover/strategies/unfolding.md b/prover/strategies/unfolding.md index a7a60dcd9..71b5f853b 100644 --- a/prover/strategies/unfolding.md +++ b/prover/strategies/unfolding.md @@ -79,19 +79,19 @@ module STRATEGY-UNFOLDING ... - rule \implies(\and(LHS), RHS) + rule \implies(\and(LHS), RHS) => \implies(\and((LHS -Patterns (LRP, .Patterns)) ++Patterns BODY), RHS) - + left-unfold-oneBody(LRP, \exists { _ } \and(BODY)) => noop ... .K => left-unfold-oneBody(LRP, \and(BODY)) ... requires LRP in LHS - rule \implies( \and( sep( (LHS => ((LHS -Patterns (LRP, .Patterns)) ++Patterns \and(BODY))) ) + rule \implies( \and( sep( (LHS => ((LHS -Patterns (LRP, .Patterns)) ++Patterns \and(BODY))) ) , _ ) , RHS ) - + left-unfold-oneBody(LRP, \exists { _ } \and(BODY)) => noop ... .K => left-unfold-oneBody(LRP, \and(BODY)) ... requires LRP in LHS @@ -111,7 +111,7 @@ implicatations. The resulting goals are equivalent to the initial goal. => left-unfold-Nth-eachLRP(M, getUnfoldables(LHS)) ... - \implies(\and(LHS), RHS) + \implies(\and(LHS), RHS) rule left-unfold-Nth-eachLRP(M, PS) => fail @@ -146,12 +146,12 @@ Note that the resulting goals is stonger than the initial goal (i.e. => right-unfold-eachRRP( filterByConstructor(getUnfoldables(RHS), SYMBOL) ) ... - \implies(LHS, \exists { _ } \and(RHS)) + \implies(LHS, \exists { _ } \and(RHS)) rule right-unfold => right-unfold-eachRRP(getUnfoldables(RHS)) ... - \implies(LHS, \exists { _ } \and(RHS)) + \implies(LHS, \exists { _ } \and(RHS)) rule right-unfold-all(bound: N) => right-unfold-all(symbols: getRecursiveSymbols(.Patterns), bound: N) ... @@ -222,10 +222,10 @@ rule addPattern(P, ListItem(Ps:Patterns) L) => ListItem(P, Ps) addPattern(P, L) ```k // TODO: -Patterns does not work here. We need to substitute RRP with BODY - rule \implies(LHS, \exists { E1 } \and(RHS)) + rule \implies(LHS, \exists { E1 } \and(RHS)) => \implies(LHS, \exists { E1 ++Patterns E2 } \and(substPatternsMap(RHS, zip((RRP, .Patterns), (\and(BODY), .Patterns))))) ... - + right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) => noop ... .K => right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) @@ -240,7 +240,7 @@ rule addPattern(P, ListItem(Ps:Patterns) L) => ListItem(P, Ps) addPattern(P, L) requires P =/=K #hole:Variable // right unfolding within an implication context - rule \implies(\and( sep ( \forall { UNIVs => UNIVs ++Patterns E2 } + rule \implies(\and( sep ( \forall { UNIVs => UNIVs ++Patterns E2 } implicationContext( ( \and( sep( #hole , CTXLHS ) @@ -263,7 +263,7 @@ rule addPattern(P, ListItem(Ps:Patterns) L) => ListItem(P, Ps) addPattern(P, L) ) , RHS:Pattern ) - + right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) => noop ... .K => right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) @@ -291,7 +291,7 @@ or `N` is out of range, `right-unfold(M,N) => fail`. => right-unfold-Nth-eachRRP(M, N, getUnfoldables(RHS)) ... - \implies(LHS,\exists {_ } \and(RHS)) + \implies(LHS,\exists {_ } \and(RHS)) rule right-unfold-Nth-eachRRP(M, N, RRPs) => fail ... requires getLength(RRPs) <=Int M diff --git a/prover/t/avl-implies-bst.kore.expected b/prover/t/avl-implies-bst.kore.expected index 840713029..919bf1147 100644 --- a/prover/t/avl-implies-bst.kore.expected +++ b/prover/t/avl-implies-bst.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( avl ( H { ArrayIntInt } , X { Int } , F { SetInt } , MIN { Int } , MAX { Int } , Height { Int } , Balance { Int } , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( bst ( H { ArrayIntInt } , X { Int } , F { SetInt } , MIN { Int } , MAX { Int } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/bst-implies-bt.kore.expected b/prover/t/bst-implies-bt.kore.expected index 1ffda42e6..f96177e19 100644 --- a/prover/t/bst-implies-bt.kore.expected +++ b/prover/t/bst-implies-bt.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( bst ( H { ArrayIntInt } , X { Int } , F { SetInt } , MIN { Int } , MAX { Int } , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( bt ( H { ArrayIntInt } , X { Int } , F { SetInt } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/emptyset-implies-isempty.kore.expected b/prover/t/emptyset-implies-isempty.kore.expected index 058e30b7b..6e0c03245 100644 --- a/prover/t/emptyset-implies-isempty.kore.expected +++ b/prover/t/emptyset-implies-isempty.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( \equals ( S { SetInt } , emptyset ) , .Patterns ) , \exists { .Patterns } \and ( isEmpty ( S { SetInt } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/fermat-3.smt2.expected b/prover/t/fermat-3.smt2.expected index ef7d1d445..21cff13c5 100644 --- a/prover/t/fermat-3.smt2.expected +++ b/prover/t/fermat-3.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( \equals ( plus ( mult ( Vx { Int } , mult ( Vx { Int } , Vx { Int } , .Patterns ) , .Patterns ) , mult ( Vy { Int } , mult ( Vy { Int } , Vy { Int } , .Patterns ) , .Patterns ) , .Patterns ) , mult ( Vz { Int } , mult ( Vz { Int } , Vz { Int } , .Patterns ) , .Patterns ) ) , gt ( Vz { Int } , 0 , .Patterns ) , gt ( Vy { Int } , 0 , .Patterns ) , gt ( Vx { Int } , 0 , .Patterns ) , .Patterns ) , \and ( \or ( .Patterns ) , .Patterns ) ) - + fail diff --git a/prover/t/isMod4-implies-isEven.smt2.expected b/prover/t/isMod4-implies-isEven.smt2.expected index b736511b0..6a010078e 100644 --- a/prover/t/isMod4-implies-isEven.smt2.expected +++ b/prover/t/isMod4-implies-isEven.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( isDiv4Pos ( Vx { Int } , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( isEvenPos ( Vx { Int } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/listSegmentLeft-implies-listSegmentRight.kore.expected b/prover/t/listSegmentLeft-implies-listSegmentRight.kore.expected index 8f0c0e73c..eb2249054 100644 --- a/prover/t/listSegmentLeft-implies-listSegmentRight.kore.expected +++ b/prover/t/listSegmentLeft-implies-listSegmentRight.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSegmentLeft ( H { ArrayIntInt } , X { Int } , Y { Int } , F { SetInt } , .Patterns ) , .Patterns ) , \and ( listSegmentRight ( H { ArrayIntInt } , X { Int } , Y { Int } , F { SetInt } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/listSegmentLeft-list-implies-list.kore.expected b/prover/t/listSegmentLeft-list-implies-list.kore.expected index 1319dabf6..f95ca27a4 100644 --- a/prover/t/listSegmentLeft-list-implies-list.kore.expected +++ b/prover/t/listSegmentLeft-list-implies-list.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSegmentLeft ( H { ArrayIntInt } , X { Int } , Y { Int } , F { SetInt } , .Patterns ) , list ( H { ArrayIntInt } , Y { Int } , G { SetInt } , .Patterns ) , \equals ( K { SetInt } , union ( F { SetInt } , G { SetInt } , .Patterns ) ) , disjoint ( F { SetInt } , G { SetInt } , .Patterns ) , .Patterns ) , \and ( list ( H { ArrayIntInt } , X { Int } , K { SetInt } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/listSegmentLeftsorted-sortedlist-implies-sortedlist.kore.expected b/prover/t/listSegmentLeftsorted-sortedlist-implies-sortedlist.kore.expected index b07d2c125..191818d53 100644 --- a/prover/t/listSegmentLeftsorted-sortedlist-implies-sortedlist.kore.expected +++ b/prover/t/listSegmentLeftsorted-sortedlist-implies-sortedlist.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSegmentLeftSorted ( H { ArrayIntInt } , X { Int } , Y { Int } , F { SetInt } , MIN { Int } , MAX { Int } , .Patterns ) , listSorted ( H { ArrayIntInt } , Y { Int } , G { SetInt } , MIN2 { Int } , .Patterns ) , \equals ( K { SetInt } , union ( F { SetInt } , G { SetInt } , .Patterns ) ) , disjoint ( F { SetInt } , G { SetInt } , .Patterns ) , \not ( gt ( MAX { Int } , MIN2 { Int } , .Patterns ) ) , .Patterns ) , \and ( listSorted ( H { ArrayIntInt } , X { Int } , K { SetInt } , MIN { Int } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/listSegmentRight-implies-listSegmentLeft.kore.expected b/prover/t/listSegmentRight-implies-listSegmentLeft.kore.expected index bfaec813a..19455428a 100644 --- a/prover/t/listSegmentRight-implies-listSegmentLeft.kore.expected +++ b/prover/t/listSegmentRight-implies-listSegmentLeft.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSegmentRight ( H { ArrayIntInt } , X { Int } , Y { Int } , F { SetInt } , .Patterns ) , .Patterns ) , \and ( listSegmentLeft ( H { ArrayIntInt } , X { Int } , Y { Int } , F { SetInt } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/listSegmentRightLength-appendone-implies-listSegmentRightLength.kore.expected b/prover/t/listSegmentRightLength-appendone-implies-listSegmentRightLength.kore.expected index 509c2b294..84f567480 100644 --- a/prover/t/listSegmentRightLength-appendone-implies-listSegmentRightLength.kore.expected +++ b/prover/t/listSegmentRightLength-appendone-implies-listSegmentRightLength.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSegmentRightLength ( H { ArrayIntInt } , X { Int } , Y { Int } , FA { SetInt } , LA { Int } , .Patterns ) , \equals ( F { SetInt } , union ( FA { SetInt } , singleton ( Y { Int } , .Patterns ) , .Patterns ) ) , disjoint ( FA { SetInt } , singleton ( Y { Int } , .Patterns ) , .Patterns ) , \equals ( Z { Int } , select ( H { ArrayIntInt } , Y { Int } , .Patterns ) ) , \equals ( LENGTH { Int } , plus ( LA { Int } , 1 , .Patterns ) ) , gt ( Y { Int } , 0 , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( listSegmentRightLength ( H { ArrayIntInt } , X { Int } , Z { Int } , F { SetInt } , LENGTH { Int } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/listSortedLength-implies-listLength.kore.expected b/prover/t/listSortedLength-implies-listLength.kore.expected index fa3a030b7..546a8c6f9 100644 --- a/prover/t/listSortedLength-implies-listLength.kore.expected +++ b/prover/t/listSortedLength-implies-listLength.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSortedLength ( H { ArrayIntInt } , X { Int } , K { SetInt } , MIN { Int } , Length { Int } , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( listLength ( H { ArrayIntInt } , X { Int } , K { SetInt } , Length { Int } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/listSortedLength-implies-listSorted.kore.expected b/prover/t/listSortedLength-implies-listSorted.kore.expected index c7f01f34c..95f7039e9 100644 --- a/prover/t/listSortedLength-implies-listSorted.kore.expected +++ b/prover/t/listSortedLength-implies-listSorted.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSortedLength ( H { ArrayIntInt } , X { Int } , K { SetInt } , MIN { Int } , Length { Int } , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( listSorted ( H { ArrayIntInt } , X { Int } , K { SetInt } , MIN { Int } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/pythagoras.smt2.expected b/prover/t/pythagoras.smt2.expected index d8f2dbec1..753765c3a 100644 --- a/prover/t/pythagoras.smt2.expected +++ b/prover/t/pythagoras.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( \equals ( plus ( mult ( Vx { Int } , Vx { Int } , .Patterns ) , mult ( Vy { Int } , Vy { Int } , .Patterns ) , .Patterns ) , mult ( Vz { Int } , Vz { Int } , .Patterns ) ) , gt ( Vz { Int } , 0 , .Patterns ) , gt ( Vy { Int } , 0 , .Patterns ) , gt ( Vx { Int } , 0 , .Patterns ) , .Patterns ) , \and ( \or ( .Patterns ) , .Patterns ) ) - + fail diff --git a/prover/t/qf_shid_entl-01.tst.smt2.expected b/prover/t/qf_shid_entl-01.tst.smt2.expected index ea05c8c57..32d93ae7b 100644 --- a/prover/t/qf_shid_entl-01.tst.smt2.expected +++ b/prover/t/qf_shid_entl-01.tst.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( sep ( pto ( Vx { RefGTyp } , c_GTyp ( Vy { RefGTyp } , .Patterns ) , .Patterns ) , RList ( Vy { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( sep ( RList ( Vx { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/qf_shid_entl-02.tst.smt2.expected b/prover/t/qf_shid_entl-02.tst.smt2.expected index 99f1dd3a8..c7f001926 100644 --- a/prover/t/qf_shid_entl-02.tst.smt2.expected +++ b/prover/t/qf_shid_entl-02.tst.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( sep ( RList ( Vx { RefGTyp } , Vy { RefGTyp } , .Patterns ) , RList ( Vy { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( sep ( RList ( Vx { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/qf_shid_entl-03.tst.smt2.expected b/prover/t/qf_shid_entl-03.tst.smt2.expected index 6c815a830..82782eda8 100644 --- a/prover/t/qf_shid_entl-03.tst.smt2.expected +++ b/prover/t/qf_shid_entl-03.tst.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( sep ( List ( Vx { RefGTyp } , Vy { RefGTyp } , .Patterns ) , pto ( Vy { RefGTyp } , c_GTyp ( Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( sep ( List ( Vx { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/qf_shid_entl-04.tst.smt2.expected b/prover/t/qf_shid_entl-04.tst.smt2.expected index e9f0e27d4..d95be8a6d 100644 --- a/prover/t/qf_shid_entl-04.tst.smt2.expected +++ b/prover/t/qf_shid_entl-04.tst.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( sep ( List ( Vx { RefGTyp } , Vy { RefGTyp } , .Patterns ) , List ( Vy { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( sep ( List ( Vx { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/qf_shid_entl-05.tst.smt2.expected b/prover/t/qf_shid_entl-05.tst.smt2.expected index da1a8a357..8ed6341e8 100644 --- a/prover/t/qf_shid_entl-05.tst.smt2.expected +++ b/prover/t/qf_shid_entl-05.tst.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( sep ( PeList ( Vx { RefGTyp } , Vy { RefGTyp } , .Patterns ) , pto ( Vy { RefGTyp } , c_GTyp ( Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( sep ( PeList ( Vx { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/qf_shid_entl-06.tst.smt2.expected b/prover/t/qf_shid_entl-06.tst.smt2.expected index e797aaaa2..bd45c985f 100644 --- a/prover/t/qf_shid_entl-06.tst.smt2.expected +++ b/prover/t/qf_shid_entl-06.tst.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( sep ( PeList ( Vx { RefGTyp } , Vy { RefGTyp } , .Patterns ) , PeList ( Vy { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( sep ( PeList ( Vx { RefGTyp } , Vz { RefGTyp } , .Patterns ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/sortedlist-implies-list.kore.expected b/prover/t/sortedlist-implies-list.kore.expected index 601290d3b..e69b8064b 100644 --- a/prover/t/sortedlist-implies-list.kore.expected +++ b/prover/t/sortedlist-implies-list.kore.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( listSorted ( H { ArrayIntInt } , X { Int } , K { SetInt } , MIN { Int } , .Patterns ) , .Patterns ) , \exists { .Patterns } \and ( list ( H { ArrayIntInt } , X { Int } , K { SetInt } , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/trivial-var.smt2.expected b/prover/t/trivial-var.smt2.expected index b464a3b46..4893971d8 100644 --- a/prover/t/trivial-var.smt2.expected +++ b/prover/t/trivial-var.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( .Patterns ) , \and ( \or ( \equals ( Vx { Int } , Vx { Int } ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/trivial.smt2.expected b/prover/t/trivial.smt2.expected index b18d4bf0b..996a73ba5 100644 --- a/prover/t/trivial.smt2.expected +++ b/prover/t/trivial.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( \equals ( 1 , 1 ) , .Patterns ) , \and ( \or ( \equals ( 2 , 2 ) , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/t/zero-iszero.smt2.expected b/prover/t/zero-iszero.smt2.expected index 83e59df0a..516288fdf 100644 --- a/prover/t/zero-iszero.smt2.expected +++ b/prover/t/zero-iszero.smt2.expected @@ -8,9 +8,9 @@ active: true, id: root, parent: . - + \implies ( \and ( .Patterns ) , \exists { .Patterns } \and ( iszero ( 0 , .Patterns ) , .Patterns ) ) - + success diff --git a/prover/utils/load-named.md b/prover/utils/load-named.md index fb6dee665..f3c9d9a9b 100644 --- a/prover/utils/load-named.md +++ b/prover/utils/load-named.md @@ -14,7 +14,7 @@ module LOAD-NAMED-RULES ... Name - P + P success ... From d85aa381f7c7c826a07a0792f38eac4389c79537 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Mon, 13 Apr 2020 22:37:35 +0530 Subject: [PATCH 2/3] t/unit: Use token names that aren't used as variables in the semantics to avoid parsing issues --- prover/t/unit/match-assoc-comm.k | 33 +++++++++++------------ prover/t/unit/match-assoc.k | 45 ++++++++++++++++---------------- 2 files changed, 40 insertions(+), 38 deletions(-) diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 522cabcd5..2ecba9bed 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -6,9 +6,10 @@ module TEST-MATCH-ASSOC-COMM syntax UpperName ::= "Data" [token] | "Loc" [token] | "W" [token] | "W1" [token] | "W2" [token] - | "X" [token] | "X1" [token] | "X2" [token] - | "Y" [token] | "Y1" [token] | "Y2" [token] + | "X0" [token] | "X1" [token] | "X2" [token] + | "Y0" [token] | "Y1" [token] | "Y2" [token] | "Z" [token] | "Z1" [token] | "Z2" [token] + | "H0" [token] rule test("match-assoc-comm", 1) => assert( #matchResult( subst: .Map , rest: pto( Z { Loc }, W { Data })) @@ -24,12 +25,12 @@ module TEST-MATCH-ASSOC-COMM .Declarations rule test("match-assoc-comm", 2) - => assert( #matchResult( subst: Z { Loc } |-> X { Loc } - W { Data } |-> Y { Data } + => assert( #matchResult( subst: Z { Loc } |-> X0 { Loc } + W { Data } |-> Y0 { Data } , rest: .Patterns ) , .MatchResults - == #matchAssocComm( terms: pto( X { Loc }, Y { Data }) + == #matchAssocComm( terms: pto( X0 { Loc }, Y0 { Data }) , pattern: pto( Z { Loc }, W { Data }) , variables: Z { Loc }, W { Data } , results: .MatchResults @@ -91,9 +92,9 @@ module TEST-MATCH-ASSOC-COMM , .MatchResults == #matchAssocComm( terms: pto( X1 { Loc }, Y1 { Loc }) , pto( X2 { Loc }, Y2 { Loc }) - , pattern: pto( X { Loc }, Y { Loc }) - , pto( Y { Loc }, Z { Loc }) - , variables: X { Loc }, Y { Loc }, Z { Loc } + , pattern: pto( X0 { Loc }, Y0 { Loc }) + , pto( Y0 { Loc }, Z { Loc }) + , variables: X0 { Loc }, Y0 { Loc }, Z { Loc } , results: .MatchResults , subst: .Map , rest: .Patterns @@ -103,14 +104,14 @@ module TEST-MATCH-ASSOC-COMM rule test("match-assoc-comm", 7) => assert( #error( "No valid substitution" ) - , #matchResult( subst: W { Loc } |-> Y { Loc } + , #matchResult( subst: W { Loc } |-> Y0 { Loc } , rest: .Patterns ) , .MatchResults - == #matchAssocComm( terms: pto ( Y { Loc } , c(Z { Loc }) ) - , pto ( X { Loc } , c(Y { Loc }) ) - , pattern: pto ( X { Loc } , c(W { Loc }) ) - , pto ( W { Loc } , c(Z { Loc }) ) + == #matchAssocComm( terms: pto ( Y0 { Loc } , c(Z { Loc }) ) + , pto ( X0 { Loc } , c(Y0 { Loc }) ) + , pattern: pto ( X0 { Loc } , c(W { Loc }) ) + , pto ( W { Loc } , c(Z { Loc }) ) , variables: W { Loc } , results: .MatchResults , subst: .Map @@ -123,9 +124,9 @@ module TEST-MATCH-ASSOC-COMM rule test("match-assoc-comm", 8) => assert( #error("Variable sort does not match term") , .MatchResults - == #matchAssocComm( terms: pto ( W { X1 } , c(X { X1 }) ) - , pattern: pto ( Y { X2 } , c(Z { X2 }) ) - , variables: Y { X2 }, Z { X2 } + == #matchAssocComm( terms: pto ( W { X1 } , c(X0 { X1 }) ) + , pattern: pto ( Y0 { X2 } , c(Z { X2 }) ) + , variables: Y0 { X2 }, Z { X2 } , results: .MatchResults , subst: .Map , rest: .Patterns diff --git a/prover/t/unit/match-assoc.k b/prover/t/unit/match-assoc.k index bb0828fe2..6696afbb9 100644 --- a/prover/t/unit/match-assoc.k +++ b/prover/t/unit/match-assoc.k @@ -6,14 +6,14 @@ module TEST-MATCH-ASSOC syntax UpperName ::= "Data" [token] | "Loc" [token] | "W" [token] - | "X" [token] - | "Y" [token] + | "X0" [token] + | "Y0" [token] | "Z" [token] rule test("match-assoc", 1) => assert( #error("No valid substitution"), .MatchResults - == #matchAssoc( terms: pto( X { Loc }, Y { Data }) - , pattern: pto( Z { Loc }, W { Data }) + == #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data }) + , pattern: pto( Z { Loc }, W { Data }) , variables: W { Data } , subst: .Map , rest: .Patterns @@ -22,8 +22,8 @@ module TEST-MATCH-ASSOC .Declarations rule test("match-assoc", 2) => assert( #error("Constructors do not match"), .MatchResults - == #matchAssoc( terms: c( X { Loc }, Y { Data }) - , pattern: d( Z { Loc }, W { Data }) + == #matchAssoc( terms: c( X0 { Loc }, Y0 { Data }) + , pattern: d( Z { Loc }, W { Data }) , variables: Z { Loc }, W { Data } , subst: .Map , rest: .Patterns @@ -32,7 +32,7 @@ module TEST-MATCH-ASSOC .Declarations rule test("match-assoc", 3) => assert( #error( "Mismatch in length of arguments" ), .MatchResults - == #matchAssoc( terms: pto( X { Loc }, Y { Data }) + == #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data }) , pattern: .Patterns , variables: .Patterns , subst: .Map @@ -42,8 +42,8 @@ module TEST-MATCH-ASSOC .Declarations rule test("match-assoc", 4) => assert( #error( "Mismatch in length of arguments" ), .MatchResults - == #matchAssoc( terms: c(X { Loc }, Y { Data }) - , pattern: c(X { Loc }, Y { Data }, Y { Data }) + == #matchAssoc( terms: c(X0 { Loc }, Y0 { Data }) + , pattern: c(X0 { Loc }, Y0 { Data }, Y0 { Data }) , variables: .Patterns , subst: .Map , rest: .Patterns @@ -66,13 +66,13 @@ module TEST-MATCH-ASSOC .Declarations // Basic Matching rule test("match-assoc", 6) - => assert( #matchResult( subst: Z { Loc } |-> X { Loc } - W { Data } |-> Y { Data } + => assert( #matchResult( subst: Z { Loc } |-> X0 { Loc } + W { Data } |-> Y0 { Data } , rest: .Patterns ) , .MatchResults - == #matchAssoc( terms: pto( X { Loc }, Y { Data }) - , pattern: pto( Z { Loc }, W { Data }) + == #matchAssoc( terms: pto( X0 { Loc }, Y0 { Data }) + , pattern: pto( Z { Loc }, W { Data }) , variables: Z { Loc }, W { Data } , subst: .Map , rest: .Patterns @@ -81,13 +81,13 @@ module TEST-MATCH-ASSOC .Declarations // Match multiple occurances of a variable rule test("match-assoc", 7) - => assert( #matchResult( subst: Z { Loc } |-> X { Loc } - W { Data } |-> Y { Data } + => assert( #matchResult( subst: Z { Loc } |-> X0 { Loc } + W { Data } |-> Y0 { Data } , rest: .Patterns ) , .MatchResults - == #matchAssoc( terms: c( X { Loc }, Y { Data }), d( X { Loc }, Y { Data }) - , pattern: c( Z { Loc }, W { Data }), d( Z { Loc }, W { Data }) + == #matchAssoc( terms: c( X0 { Loc }, Y0 { Data }), d( X0 { Loc }, Y0 { Data }) + , pattern: c( Z { Loc }, W { Data }), d( Z { Loc }, W { Data }) , variables: Z { Loc }, W { Data } , subst: .Map , rest: .Patterns @@ -98,8 +98,8 @@ module TEST-MATCH-ASSOC rule test("match-assoc", 8) => assert( #error( "No valid substitution" ) , .MatchResults - == #matchAssoc( terms: c( X { Loc }, Y { Data }), c( X { Loc }, Y { Data }) - , pattern: c( Z { Loc }, W { Data }), c( Y { Loc }, W { Data }) + == #matchAssoc( terms: c( X0 { Loc }, Y0 { Data }), c( X0 { Loc }, Y0 { Data }) + , pattern: c( Z { Loc }, W { Data }), c( Y0 { Loc }, W { Data }) , variables: Z { Loc }, W { Data } , subst: .Map , rest: .Patterns @@ -109,10 +109,11 @@ module TEST-MATCH-ASSOC // Match constructor against variable rule test("match-assoc", 9) - => assert( #error("Constructors do not match") + => symbol pto ( Loc, Data ) : Heap + assert( #error("Constructors do not match") , .MatchResults - == #matchAssoc( terms: X { Loc }, Y { Data } - , pattern: c( Z { Loc }, W { Data }), c( Y { Loc }, W { Data }) + == #matchAssoc( terms: X0 { Loc }, Y0 { Data } + , pattern: c( Z { Loc }, W { Data }), c( Y0 { Loc }, W { Data }) , variables: Z { Loc }, W { Data } , subst: .Map , rest: .Patterns From 4eab0153fc5c25cf075e5134321a15b7baeedf6f Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 15 Apr 2020 06:04:02 +0530 Subject: [PATCH 3/3] drivers: Initial goal is now populated via `subgoal` strategy --- prover/drivers/base.md | 10 ++++++++++ prover/drivers/kore-driver.md | 33 +++++---------------------------- prover/drivers/smt-driver.md | 21 +++++++++------------ prover/strategies/core.md | 7 +++++-- 4 files changed, 29 insertions(+), 42 deletions(-) diff --git a/prover/drivers/base.md b/prover/drivers/base.md index 9c51d7f5f..3c26ac868 100644 --- a/prover/drivers/base.md +++ b/prover/drivers/base.md @@ -87,6 +87,16 @@ module DRIVER-BASE imports LOAD-NAMED-RULES rule .CommandLine => .K ... + + rule + + .K + .K + .K + ... + + + 1 => 0 endmodule module DRIVER-BASE-SYNTAX diff --git a/prover/drivers/kore-driver.md b/prover/drivers/kore-driver.md index ee24131d5..3135043be 100644 --- a/prover/drivers/kore-driver.md +++ b/prover/drivers/kore-driver.md @@ -66,34 +66,11 @@ in the subgoal and the claim of the named goal remains intact. => claim getFreshClaimName() : PATTERN strategy STRAT ... - - rule - claim NAME : PATTERN - strategy STRAT - => .K - ... - - ( .Bag => - - NAME - true:Bool - .K - PATTERN - subgoal(PATTERN, STRAT) - success - .Bag - .K - - ) - ... - -``` - -```k - rule _:ClaimName - S:TerminalStrategy - S - 1 => 0 + rule claim NAME : PATTERN + strategy STRAT + => subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT)) + ... + ``` ```k diff --git a/prover/drivers/smt-driver.md b/prover/drivers/smt-driver.md index 5d9323b60..45c823729 100644 --- a/prover/drivers/smt-driver.md +++ b/prover/drivers/smt-driver.md @@ -318,24 +318,21 @@ module DRIVER-SMT rule #containsSpatialPatterns(.Patterns, _) => false rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S) + syntax KItem ::= "expect" TerminalStrategy + rule S ~> expect S => .K ... + rule #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED) ~> (check-sat) => #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED) ... - ( .Bag => - - !N:ClaimName - true:Bool - .K - \implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) - STRAT - EXPECTED - .Bag - .K - - ) + .K + => subgoal(\implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) + , STRAT + ) + ~> expect EXPECTED + ... requires notBool PATTERN ==K \exists { .Patterns } \and ( .Patterns ) diff --git a/prover/strategies/core.md b/prover/strategies/core.md index f8e6a17c3..d22c677e9 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -109,10 +109,13 @@ Proving a goal may involve proving other subgoals: ```k syntax Strategy ::= "subgoal" "(" Pattern "," Strategy ")" + rule subgoal(GOAL, STRAT) => subgoal(!ID:Int, GOAL, STRAT) ... + + syntax Strategy ::= "subgoal" "(" GoalId "," Pattern "," Strategy ")" rule ( .Bag => - !ID:Int + ID:Int true PARENT SUBSTRAT @@ -125,7 +128,7 @@ Proving a goal may involve proving other subgoals: PARENT true => false - subgoal(SUBGOAL, SUBSTRAT) => goalStrat(!ID:Int) ... + subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID:Int) ... LC::Bag TRACE ...