diff --git a/prover/build b/prover/build index f602d28cc..4927ea8e4 100755 --- a/prover/build +++ b/prover/build @@ -40,7 +40,6 @@ other_md_files = [ 'lang/smt-lang.md' , 'strategies/unfolding.md' , 'utils/error.md' , 'utils/instantiate-assumptions.md' - , 'utils/load-named.md' , 'utils/heatcool.md' , 'utils/syntactic-match.md' , 'utils/visitor.md' @@ -61,8 +60,8 @@ prover_smt = prover('prover-smt', '--main-module DRIVER-SMT --syntax-module D # Functional tests # ---------------- -# prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine') -# prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine') +prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine') +prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine') def log_on_success(file, message): return proj.rule( 'log-to-success' @@ -131,8 +130,11 @@ secondary_tests('qf_shidlia_entl_unsat_tests', 't/test-lists/qf_shidlia_entl.uns secondary_tests('qf_shlid_entl_unsat_tests', 't/test-lists/qf_shlid_entl.unsat') secondary_tests('shid_entl_unsat_tests', 't/test-lists/shid_entl.unsat') +# TODO: Why are smt tests `-krun` and kore tests `-run`? +def test_path(name, type): + return ".build/t/%s.%s" % (name, type) def sl_comp_test_path(name): - return ".build/t/SL-COMP18/bench/qf_shid_entl/%s.prover-smt-krun" % (name) + return test_path("SL-COMP18/bench/qf_shid_entl/%s" % name, 'prover-smt-krun') proj.alias('smoke-tests', list(map( sl_comp_test_path, [ "02.tst.smt2" , # RList trans @@ -145,9 +147,12 @@ proj.alias('smoke-tests', list(map( sl_comp_test_path, [ "skl2-vc03.smt2" , # needs framing but not match-pto "odd-lseg3_slk-5.smt2" , # needs framing and match-pto "nll-vc01.smt2" , # needs large number of unfolding but no kt - "ls_nonrec_entail_ls_07.sb.smt2" , # 6 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5) - needs large number of kts and unfolding + "ls_nonrec_entail_ls_05.sb.smt2" , # 4 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5) - needs large number of kts and unfolding "ls_lsrev_concat_entail_ls_1.sb.smt2" , # need unfolding within implication context - ]))) + ])) + + [ test_path('listSegmentLeft-implies-listSegmentRight.kore', 'prover-kore-run') + ] + ) # Unit Tests # ---------- diff --git a/prover/drivers/base.md b/prover/drivers/base.md index 415e8c9e9..3c313d711 100644 --- a/prover/drivers/base.md +++ b/prover/drivers/base.md @@ -2,8 +2,8 @@ Configuration ============= The configuration consists of a list of goals. The first goal is considered -active. The `` cell contains the Matching Logic Pattern for which we are -searching for a proof. The `` cell contains an imperative language +active. The `` 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 information. Eventually, this could be used for constructing a proof @@ -17,7 +17,7 @@ module PROVER-CONFIGURATION syntax Pgm syntax Strategy syntax CommandLine - syntax GoalId ::= ClaimName | Int + syntax GoalId ::= AxiomName | Int configuration @@ -26,8 +26,8 @@ module PROVER-CONFIGURATION .K .K + \and(.Patterns) // TODO: make this optional instead? $COMMANDLINE:CommandLine ~> $PGM:Pgm - .K .K .K @@ -83,7 +83,6 @@ module DRIVER-BASE imports VISITOR imports PATTERN-LENGTH imports HEATCOOL-RULES - imports LOAD-NAMED-RULES rule .CommandLine => .K ... @@ -91,7 +90,7 @@ module DRIVER-BASE .K .K - .K + .K ... diff --git a/prover/drivers/kore-driver.md b/prover/drivers/kore-driver.md index 3135043be..ddcbc6401 100644 --- a/prover/drivers/kore-driver.md +++ b/prover/drivers/kore-driver.md @@ -58,19 +58,22 @@ Add various standard Kore declarations to the configuration directly: ``` The `claim` Declaration creates a new `` cell. -We create a subgoal, so that all the reasoning happens -in the subgoal and the claim of the named goal remains intact. ```k rule claim PATTERN strategy STRAT - => claim getFreshClaimName() : PATTERN strategy STRAT + => claim getFreshGlobalAxiomName() : PATTERN strategy STRAT ... rule claim NAME : PATTERN strategy STRAT - => subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT)) + => subgoal(NAME, PATTERN, STRAT) + ~> axiom NAME : PATTERN ... + + // the rule above generates `success ~> axiom _ : _ ~> Declarations` + rule (success => .K) ~> D:Declaration ... + rule (success => .K) ~> D:Declarations ... ``` ```k diff --git a/prover/drivers/smt-driver.md b/prover/drivers/smt-driver.md index 75829bac9..b213bbb65 100644 --- a/prover/drivers/smt-driver.md +++ b/prover/drivers/smt-driver.md @@ -217,7 +217,7 @@ module DRIVER-SMT requires notBool #matchesUnfoldMutRecs(STRAT) - rule unfold-mut-recs => noop ... + rule unfold-mut-recs => noop ... syntax Bool ::= #matchesUnfoldMutRecs(Strategy) [function] rule #matchesUnfoldMutRecs(unfold-mut-recs) => true @@ -319,23 +319,20 @@ module DRIVER-SMT rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S) syntax KItem ::= "expect" TerminalStrategy - rule S ~> expect S => .K ... + rule S ~> expect S => .K ... - rule - #goal( goal: (\exists{Vs} \and(Ps)) #as 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) - ... - - .K - => subgoal(\implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) - , STRAT - ) - ~> expect EXPECTED - - ... - - requires notBool PATTERN ==K \exists { .Patterns } \and ( .Patterns ) + ) + => ( subgoal(\implies( \and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) + , STRAT + ) + ~> #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED) + ) + ... + + requires notBool PATTERN ==K \exists { .Patterns } \and ( .Patterns ) + rule (success => .K) ~> #goal( goal: _, strategy: _, expected: _) ... ``` ```k diff --git a/prover/drivers/unit-tests.md b/prover/drivers/unit-tests.md index 8cb71d5bf..022f76ff2 100644 --- a/prover/drivers/unit-tests.md +++ b/prover/drivers/unit-tests.md @@ -27,7 +27,7 @@ module UNIT-TEST syntax Declaration ::= "suite" String rule suite(SUITE) => next-test(SUITE, 1) ... - + syntax Declaration ::= "next-test" "(" String "," Int ")" rule next-test(SUITE, N) => test(SUITE, N) diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md index b24e3bdbe..8cb0baba5 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -182,8 +182,6 @@ only in this scenario*. syntax SymbolDeclaration ::= "symbol" Symbol "(" Sorts ")" ":" Sort syntax SortDeclaration ::= "sort" Sort syntax AxiomName ::= LowerName | UpperName - syntax ClaimName ::= LowerName | UpperName - syntax AxiomOrClaimName ::= AxiomName | ClaimName syntax Declaration ::= "imports" String | "axiom" Pattern @@ -854,21 +852,15 @@ Simplifications rule freshAxiomName(I:Int) => StringToAxiomName("ax" +String Int2String(I)) - syntax String ::= ClaimNameToString(ClaimName) [function, hook(STRING.token2string)] - syntax ClaimName ::= StringToClaimName(String) [function, functional, hook(STRING.string2token)] - | freshClaimName(Int) [freshGenerator, function, functional] - - rule freshClaimName(I:Int) => StringToClaimName("cl" +String Int2String(I)) - syntax Set ::= collectClaimNames() [function] | #collectClaimNames(Set) [function] rule collectClaimNames() => #collectClaimNames(.Set) rule [[ #collectClaimNames(Ns) - => #collectClaimNames(Ns SetItem(ClaimNameToString(N))) ]] - N:ClaimName - requires notBool (ClaimNameToString(N) in Ns) + => #collectClaimNames(Ns SetItem(AxiomNameToString(N))) ]] + N:AxiomName + requires notBool (AxiomNameToString(N) in Ns) rule #collectClaimNames(Ns) => Ns [owise] @@ -1012,10 +1004,6 @@ assume a pattern of the form: rule getFreshAxiomName(GId) => StringToAxiomName(getFreshName("ax", collectNamed(GId))) - syntax ClaimName ::= getFreshClaimName() [function] - rule getFreshClaimName() - => StringToClaimName(getFreshName("cl", collectGlobalNamed())) - syntax Set ::= collectSymbolsS(GoalId) [function] | #collectSymbolsS(Declarations) [function] @@ -1034,6 +1022,14 @@ assume a pattern of the form: => StringToSymbol( getFreshNameNonum(Base, collectSymbolsS(GId))) + syntax KItem ::= loadNamed(AxiomName) + + rule loadNamed(Name) => P ... + axiom Name : P + + rule loadNamed(Name) => P ... + axiom Name : P + ``` ```k diff --git a/prover/lang/smt-lang.md b/prover/lang/smt-lang.md index 15f597d09..11666d602 100644 --- a/prover/lang/smt-lang.md +++ b/prover/lang/smt-lang.md @@ -244,6 +244,7 @@ module SMTLIB2-HELPERS rule CheckSAT.parseResult(#systemResult(0, "sat\n", STDERR)) => sat rule CheckSAT.parseResult(#systemResult(0, "unsat\n", STDERR)) => unsat rule CheckSAT.parseResult(#systemResult(0, "unknown\n", STDERR)) => unknown + rule CheckSAT.parseResult(#systemResult(0, "timeout\n", STDERR)) => unknown rule CheckSAT.parseResult(#systemResult(I, STDOUT, STDERR)) => #error(#systemResult(I, STDOUT, STDERR)) requires I =/=Int 0 endmodule diff --git a/prover/prover.md b/prover/prover.md index 2ddc9ad15..b4a241310 100644 --- a/prover/prover.md +++ b/prover/prover.md @@ -21,7 +21,6 @@ requires "strategies/unfolding.k" requires "utils/error.k" requires "utils/instantiate-assumptions.k" requires "utils/heatcool.k" -requires "utils/load-named.k" requires "utils/syntactic-match.k" requires "utils/visitor.k" ``` @@ -63,7 +62,7 @@ module STRATEGIES-EXPORTED-SYNTAX | "frame" | "unfold-mut-recs" | "apply-equation" - RewriteDirection AxiomOrClaimName + RewriteDirection AxiomName "at" Int "by" "[" Strategies "]" | "apply-equation" "(" "eq:" Pattern @@ -73,7 +72,7 @@ module STRATEGIES-EXPORTED-SYNTAX ")" | "intros" AxiomName | "replace-evar-with-func-constant" Variables - | "duplicate" AxiomOrClaimName "as" AxiomName + | "duplicate" AxiomName "as" AxiomName | "instantiate-universals" "(" "in:" AxiomName "," "vars:" VariableNames "," @@ -82,7 +81,7 @@ module STRATEGIES-EXPORTED-SYNTAX // of the axiom or claim given as the first arg. // Uses the strategy given in second argument // to discharge the axiom's premises. - | "apply" "(" AxiomOrClaimName + | "apply" "(" AxiomName "," Strategy ")" | "inst-exists" "(" Variable "," Pattern "," Strategy ")" diff --git a/prover/strategies/apply-equation.md b/prover/strategies/apply-equation.md index 5555f3b86..911c2a506 100644 --- a/prover/strategies/apply-equation.md +++ b/prover/strategies/apply-equation.md @@ -20,23 +20,22 @@ module STRATEGY-APPLY-EQUATION imports PROVER-CORE imports STRATEGIES-EXPORTED-SYNTAX imports HEATCOOL-SYNTAX - imports LOAD-NAMED-SYNTAX imports INSTANTIATE-ASSUMPTIONS-SYNTAX imports VISITOR-SYNTAX imports SYNTACTIC-MATCH-SYNTAX - rule (.K => loadNamed(Name)) + rule (.K => loadNamed(Name)) ~> apply-equation D Name at _ by[_] ... - + - rule (P:Pattern ~> apply-equation D _ at Idx by[Ss]) + rule (P:Pattern ~> apply-equation D _ at Idx by[Ss]) => #apply-equation1 ( hypothesis: P , direction: D , at: Idx , by: Ss ) - ... + ... syntax KItem ::= "#apply-equation1" @@ -57,7 +56,7 @@ module STRATEGY-APPLY-EQUATION => apply-equation.checkShape(P) rule apply-equation.checkShape(_) => false [owise] - rule + rule #apply-equation1 ( hypothesis: H, direction: D, at: Idx, by: Strats) => @@ -77,7 +76,7 @@ module STRATEGY-APPLY-EQUATION , by: Strats ) ... - + requires apply-equation.checkShape(H) // Gets LHS or RHS of a conclusion that is an equality. @@ -105,7 +104,7 @@ module STRATEGY-APPLY-EQUATION "," "by:" Strategies ")" - rule + rule #apply-equation2(from: L, to: R, hypothesis: H, at: Idx, by: Ss) => #apply-equation3 @@ -120,8 +119,8 @@ module STRATEGY-APPLY-EQUATION , by: Ss ) ... - - T + + T syntax KItem ::= "#apply-equation3" "(" "hypothesis:" Pattern @@ -130,7 +129,7 @@ module STRATEGY-APPLY-EQUATION "," "by:" Strategies ")" - rule + rule #apply-equation3 ( hypothesis: P , heatResult: heatResult(Heated, Subst) @@ -139,10 +138,10 @@ module STRATEGY-APPLY-EQUATION ) => instantiateAssumptions(GId, Subst, P) ~> createSubgoalsWithStrategies(strats: Ss, result: noop) - ... - + ... + _ => cool(heated: Heated, term: substMap(R, Subst)) - + GId syntax KItem ::= "createSubgoalsWithStrategies" @@ -150,18 +149,18 @@ module STRATEGY-APPLY-EQUATION "," "result:" Strategy ")" - rule (#instantiateAssumptionsResult(.Patterns, .Map) + rule (#instantiateAssumptionsResult(.Patterns, .Map) ~> createSubgoalsWithStrategies ( strats: .Strategies , result: R)) => R - ... + ... - rule #instantiateAssumptionsResult(P,Ps => Ps, .Map) + rule #instantiateAssumptionsResult(P,Ps => Ps, .Map) ~> createSubgoalsWithStrategies ( strats: (S, Ss) => Ss , result: R => R & subgoal(P, S)) - ... + ... ``` ### Apply equation in context @@ -180,10 +179,10 @@ Gamma |- C[... /\ A=B /\ ... /\ A /\ ... ] ```k - rule apply-equation(eq: \equals(_,_) #as Eq, idx: Idx, direction: D, at: At) + rule apply-equation(eq: \equals(_,_) #as Eq, idx: Idx, direction: D, at: At) => noop - ... - C + ... + C => visitorResult.getPattern( visitTopDown( applyEquationInContextVisitor(aeicParams( @@ -192,7 +191,7 @@ Gamma |- C[... /\ A=B /\ ... /\ A /\ ... ] C ) ) - + syntax KItem ::= "aeicParams" "(" "eq:" Pattern "," "idx:" Int diff --git a/prover/strategies/apply.md b/prover/strategies/apply.md index e51b4fe93..3145ef567 100644 --- a/prover/strategies/apply.md +++ b/prover/strategies/apply.md @@ -17,15 +17,14 @@ Gamma |- Q module STRATEGY-APPLY imports PROVER-CORE imports STRATEGIES-EXPORTED-SYNTAX - imports LOAD-NAMED-SYNTAX imports SYNTACTIC-MATCH-SYNTAX imports INSTANTIATE-ASSUMPTIONS-SYNTAX - rule (.K => loadNamed(Name)) + rule (.K => loadNamed(Name)) ~> apply(Name, _) ... - + - rule + rule (A:Pattern ~> apply(_, Strat)) => #apply1( A, @@ -36,38 +35,38 @@ module STRATEGY-APPLY ), Strat ) - ... - G + ... + G syntax KItem ::= #apply1(Pattern, MatchResult, Strategy) - rule + rule #apply1(A, #matchResult(subst: Subst), Strat) => #apply2(instantiateAssumptions(GId, Subst, A), Strat, success) - ... + ... GId - rule + rule #apply1(_, #error(_), _) => fail - ... + ... syntax KItem ::= #apply2( InstantiateAssumptionsResult, Strategy, Strategy) - rule + rule #apply2(#instantiateAssumptionsResult(.Patterns, .Map), _, Result) => Result - ... + ... - rule + rule #apply2( #instantiateAssumptionsResult(P, Ps => Ps, .Map), Strat, Result => Result & subgoal(P, Strat) ) - ... + ... endmodule ``` diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 54de8a0ad..d9afd6e9e 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -12,7 +12,7 @@ module PROVER-CORE-SYNTAX imports KORE syntax Declaration ::= "claim" Pattern "strategy" Strategy - | "claim" ClaimName ":" Pattern "strategy" Strategy + | "claim" AxiomName ":" Pattern "strategy" Strategy ``` ```k @@ -54,7 +54,7 @@ module PROVER-CORE `Strategy`s can be sequentially composed via the `.` operator. ```k - rule (S . T) . U => S . (T . U) ... + rule (S . T) . U => S . (T . U) ... ``` Since strategies do not live in the K cell, we must manually heat and cool. @@ -63,23 +63,23 @@ cooled back into the sequence strategy. ```k syntax ResultStrategy ::= "#hole" - rule S1 . S2 => S1 ~> #hole . S2 ... + rule S1 . S2 => S1 ~> #hole . S2 ... requires notBool(isResultStrategy(S1)) andBool notBool(isSequenceStrategy(S1)) - rule S1:ResultStrategy ~> #hole . S2 => S1 . S2 ... + rule S1:ResultStrategy ~> #hole . S2 => S1 . S2 ... ``` The `noop` (no operation) strategy is the unit for sequential composition: ```k - rule noop . T => T ... + rule noop . T => T ... ``` The `success` and `fail` strategy indicate that a goal has been successfully proved, or that constructing a proof has failed. ```k - rule T:TerminalStrategy . S => T ... + rule T:TerminalStrategy . S => T ... ``` The `goalStrat(GoalId)` strategy is used to establish a reference to the result of @@ -91,12 +91,12 @@ completed, its result is replaced in the parent goal and the subgoal is removed. rule ( ID PID - RStrat:TerminalStrategy + RStrat:TerminalStrategy ... => .Bag ) PID - goalStrat(ID) => RStrat ... + goalStrat(ID) => RStrat ... ... ... @@ -107,16 +107,16 @@ Proving a goal may involve proving other subgoals: ```k syntax Strategy ::= "subgoal" "(" Pattern "," Strategy ")" - rule subgoal(GOAL, STRAT) => subgoal(!ID:Int, GOAL, STRAT) ... + rule subgoal(GOAL, STRAT) => subgoal(!ID:Int, GOAL, STRAT) ... syntax Strategy ::= "subgoal" "(" GoalId "," Pattern "," Strategy ")" rule ( .Bag => - ID:Int + ID PARENT - SUBSTRAT - SUBGOAL + SUBSTRAT + SUBGOAL LC TRACE ... @@ -124,7 +124,7 @@ Proving a goal may involve proving other subgoals: ) PARENT - subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID:Int) ... + subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID) ... LC::Bag TRACE ... @@ -138,19 +138,19 @@ of the main goal. The `&` strategy generates subgoals for each child strategy, a all succeed, it succeeds: ```k - rule S & fail => fail ... - rule fail & S => fail ... - rule S & success => S ... - rule success & S => S ... - rule (S1 & S2) . S3 => (S1 . S3) & (S2 . S3) ... - rule T:TerminalStrategy ~> #hole & S2 + rule S & fail => fail ... + rule fail & S => fail ... + rule S & success => S ... + rule success & S => S ... + rule (S1 & S2) . S3 => (S1 . S3) & (S2 . S3) ... + rule T:TerminalStrategy ~> #hole & S2 => T & S2 ... - + rule - ((S1 & S2) => subgoal(GOAL, S1) ~> #hole & S2) - GOAL:Pattern + ((S1 & S2) => subgoal(GOAL, S1) ~> #hole & S2) + GOAL:Pattern ... ... @@ -164,19 +164,19 @@ The `|` strategy lets us try these different approaches, and succeeds if any one approach succeeds: ```k - rule S | fail => S ... - rule fail | S => S ... - rule S | success => success ... - rule success | S => success ... - rule (S1 | S2) . S3 => (S1 . S3) | (S2 . S3) ... - rule T:TerminalStrategy ~> #hole | S2 + rule S | fail => S ... + rule fail | S => S ... + rule S | success => success ... + rule success | S => success ... + rule (S1 | S2) . S3 => (S1 . S3) | (S2 . S3) ... + rule T:TerminalStrategy ~> #hole | S2 => T | S2 ... - + rule - ((S1 | S2) => subgoal(GOAL, S1) ~> #hole | S2 ) - GOAL:Pattern + ((S1 | S2) => subgoal(GOAL, S1) ~> #hole | S2 ) + GOAL:Pattern ... ... @@ -188,9 +188,9 @@ approach succeeds: The S { N } construct allows us to repeat a strategy S N times ```k - rule S { M } => noop ... + rule S { M } => noop ... requires M <=Int 0 - rule S { M } => S . (S { M -Int 1 }) ... + rule S { M } => S . (S { M -Int 1 }) ... requires M >Int 0 ``` @@ -198,8 +198,8 @@ Internal strategy used to implement `or-split` and `and-split`. ```k syntax Strategy ::= "replace-goal" "(" Pattern ")" - rule _ => NEWGOAL - replace-goal(NEWGOAL) => noop ... + rule _ => NEWGOAL + replace-goal(NEWGOAL) => noop ... ``` `or-split`: disjunction of implications: @@ -211,8 +211,8 @@ Internal strategy used to implement `or-split` and `and-split`. ``` ```k - rule \or(GOALS) - or-split => #orSplit(GOALS) ... + rule \or(GOALS) + or-split => #orSplit(GOALS) ... syntax Strategy ::= "#orSplit" "(" Patterns ")" [function] rule #orSplit(.Patterns) => fail @@ -229,17 +229,17 @@ Internal strategy used to implement `or-split` and `and-split`. ``` ```k - rule \implies(LHS, \exists { Vs } \and(\or(RHSs), REST)) - or-split-rhs => #orSplitImplication(LHS, Vs, 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)) - or-split-rhs => noop ... + rule \implies(LHS, \exists { Vs } \and(RHSs, REST)) + or-split-rhs => noop ... requires notBool isDisjunction(RHSs) - rule \implies(LHS, \exists { Vs } \and(.Patterns)) - or-split-rhs => noop ... + rule \implies(LHS, \exists { Vs } \and(.Patterns)) + or-split-rhs => noop ... - rule \implies(LHS, \exists { Vs } \and(.Patterns)) - or-split-rhs => noop ... + rule \implies(LHS, \exists { Vs } \and(.Patterns)) + or-split-rhs => noop ... syntax Strategy ::= "#orSplitImplication" "(" Pattern "," Patterns "," Patterns "," Patterns ")" [function] rule #orSplitImplication(P, Vs, .Patterns, REST) => replace-goal(\implies(P, \exists{Vs} \and(\or(.Patterns)))) @@ -256,8 +256,8 @@ Internal strategy used to implement `or-split` and `and-split`. ``` ```k - rule \and(GOALS) - and-split => #andSplit(GOALS) ... + rule \and(GOALS) + and-split => #andSplit(GOALS) ... syntax Strategy ::= "#andSplit" "(" Patterns ")" [function] rule #andSplit(.Patterns) => noop @@ -278,10 +278,10 @@ is in that list. ```k rule ID - prune(PRUNE_IDs:Patterns) => fail ... + prune(PRUNE_IDs:Patterns) => fail ... requires ID in PRUNE_IDs rule ID - prune(PRUNE_IDs:Patterns) => noop ... + prune(PRUNE_IDs:Patterns) => noop ... requires notBool(ID in PRUNE_IDs) ``` diff --git a/prover/strategies/duplicate.md b/prover/strategies/duplicate.md index f33be3252..5a691f7d3 100644 --- a/prover/strategies/duplicate.md +++ b/prover/strategies/duplicate.md @@ -13,16 +13,15 @@ Gamma, Phi |- Psi module STRATEGY-DUPLICATE imports PROVER-CORE imports STRATEGIES-EXPORTED-SYNTAX - imports LOAD-NAMED-SYNTAX - rule duplicate H as H' + rule duplicate H as H' => loadNamed(H) ~> #nameAs(H') ... - + syntax KItem ::= #nameAs(AxiomName) - rule P ~> #nameAs(H') => noop ... + rule P ~> #nameAs(H') => noop ... (.Bag => axiom H' : P ) ... diff --git a/prover/strategies/inst-exists.md b/prover/strategies/inst-exists.md index dd27f8bde..88ed98779 100644 --- a/prover/strategies/inst-exists.md +++ b/prover/strategies/inst-exists.md @@ -12,13 +12,13 @@ module STRATEGY-INST-EXISTS imports STRATEGIES-EXPORTED-SYNTAX imports KORE-HELPERS - rule + rule 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/instantiate-universals.md b/prover/strategies/instantiate-universals.md index dbb3c3f56..ed4faec40 100644 --- a/prover/strategies/instantiate-universals.md +++ b/prover/strategies/instantiate-universals.md @@ -10,17 +10,17 @@ module STRATEGY-INSTANTIATE-UNIVERSALS imports KORE-HELPERS imports STRATEGIES-EXPORTED-SYNTAX - rule + rule instantiate-universals(in: _, vars: .VariableNames, with: .Patterns) => noop ... - + - rule + rule instantiate-universals(in: H, vars: (V, Vs), with: (T, Ts)) => instantiate-universal V with T in H ~> instantiate-universals(in: H, vars: Vs, with: Ts) ... - + syntax Bool ::= varIsInTopUnivQual(VariableName, Sort, Pattern) [function] @@ -37,28 +37,28 @@ module STRATEGY-INSTANTIATE-UNIVERSALS syntax KItem ::= "instantiate-universal" VariableName "with" Pattern "in" AxiomName - rule + rule (.K => "Error: variable " ~> V ~> " is either not universally quantified in toplevel or has a sort other than " ~> getReturnSort(T)) ~> instantiate-universal V with T in H ... - + axiom H : Phi requires notBool varIsInTopUnivQual(V, getReturnSort(T), Phi) - rule + rule (.K => "The term " ~> T ~> "is not known to be functional.") ~> instantiate-universal _ with T in H ... - + GId requires notBool isFunctional(GId, T) - rule + rule instantiate-universal V with T in H => .K ... - + axiom H : (Phi => #instantiateUniv(Phi, V, T)) diff --git a/prover/strategies/intros.md b/prover/strategies/intros.md index 577c33d9e..79504c256 100644 --- a/prover/strategies/intros.md +++ b/prover/strategies/intros.md @@ -10,8 +10,8 @@ module STRATEGY-INTROS imports STRATEGIES-EXPORTED-SYNTAX imports KORE-HELPERS - rule intros Name => noop ... - \implies(H, G) => G + rule intros Name => noop ... + \implies(H, G) => G (.Bag => axiom Name : H ) ... diff --git a/prover/strategies/knaster-tarski.md b/prover/strategies/knaster-tarski.md index 985de8704..8fb9ce791 100644 --- a/prover/strategies/knaster-tarski.md +++ b/prover/strategies/knaster-tarski.md @@ -49,32 +49,32 @@ for guessing an instantiation of the inductive hypothesis. ``` ```k - rule kt => kt # .KTFilter ... - rule \implies(\and(LHS), RHS) - kt # FILTER + rule kt => kt # .KTFilter ... + rule \implies(\and(LHS), RHS) + kt # FILTER => getKTUnfoldables(LHS) ~> kt # FILTER ... - - rule LRPs:Patterns ~> kt # head(HEAD) + + rule LRPs:Patterns ~> kt # head(HEAD) => filterByConstructor(LRPs, HEAD) ~> kt # .KTFilter ... - - rule LRPs:Patterns ~> kt # index(I:Int) + + rule LRPs:Patterns ~> kt # index(I:Int) => getMember(I, LRPs), .Patterns ~> kt # .KTFilter ... - - rule LRPs:Patterns ~> kt # .KTFilter + + rule LRPs:Patterns ~> kt # .KTFilter => ktForEachLRP(LRPs) ... - + ``` `ktForEachLRP` iterates over the recursive predicates on the LHS of the goal: ```k syntax Strategy ::= ktForEachLRP(Patterns) - rule ktForEachLRP(.Patterns) => noop ... - rule ( ktForEachLRP((LRP, LRPs)) + rule ktForEachLRP(.Patterns) => noop ... + rule ( ktForEachLRP((LRP, LRPs)) => ( remove-lhs-existential . normalize . or-split-rhs . lift-constraints . kt-wrap(LRP) . kt-forall-intro . kt-unfold . lift-or . and-split . remove-lhs-existential @@ -84,36 +84,36 @@ for guessing an instantiation of the inductive hypothesis. | ktForEachLRP(LRPs) ) ~> REST - + ``` ```k - rule kt-unf => kt-unf # .KTFilter ... - rule \implies(\and(LHS), RHS) - kt-unf # FILTER + rule kt-unf => kt-unf # .KTFilter ... + rule \implies(\and(LHS), RHS) + kt-unf # FILTER => getKTUnfoldables(LHS) ~> kt-unf # FILTER ... - - rule LRPs:Patterns ~> kt-unf # head(HEAD) + + rule LRPs:Patterns ~> kt-unf # head(HEAD) => filterByConstructor(LRPs, HEAD) ~> kt-unf # .KTFilter ... - - rule LRPs:Patterns ~> kt-unf # index(I:Int) + + rule LRPs:Patterns ~> kt-unf # index(I:Int) => getMember(I, LRPs), .Patterns ~> kt-unf # .KTFilter ... - - rule LRPs:Patterns ~> kt-unf # .KTFilter + + rule LRPs:Patterns ~> kt-unf # .KTFilter => ktUnfForEachLRP(LRPs) ... - + ``` `ktUnfForEachLRP` iterates over the recursive predicates on the LHS of the goal: ```k syntax Strategy ::= ktUnfForEachLRP(Patterns) - rule ktUnfForEachLRP(.Patterns) => noop ... - rule ( ktUnfForEachLRP((LRP, LRPs)) + rule ktUnfForEachLRP(.Patterns) => noop ... + rule ( ktUnfForEachLRP((LRP, LRPs)) => ( remove-lhs-existential . normalize . or-split-rhs . lift-constraints . kt-wrap(LRP) . kt-forall-intro . kt-unfold . lift-or . and-split . remove-lhs-existential @@ -126,7 +126,7 @@ for guessing an instantiation of the inductive hypothesis. | ktUnfForEachLRP(LRPs) ) ~> REST - + ``` > phi(x) -> C'[psi(x)] @@ -139,10 +139,10 @@ 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 ... + + kt-wrap(LRP) => noop ... .K => kt-wrap(LRP) ... requires LRP in LHS andBool isPredicatePattern(\and(LHS)) @@ -151,14 +151,14 @@ 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 ... + + kt-wrap(LRP) => noop ... .K => kt-wrap(LRP) ... requires LRP in LSPATIAL andBool isSpatialPattern(sep(LSPATIAL)) @@ -170,13 +170,13 @@ 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 ... + + kt-forall-intro => noop ... ``` > phi(x) -> psi(x, y) @@ -185,8 +185,8 @@ for guessing an instantiation of the inductive hypothesis. ```k syntax Strategy ::= "kt-forall-elim" - rule \implies(LHS, \forall { Vs } RHS) => \implies(LHS, RHS) - kt-forall-elim => noop ... + rule \implies(LHS, \forall { Vs } RHS) => \implies(LHS, RHS) + kt-forall-elim => noop ... requires getFreeVariables(LHS) -Patterns Vs ==K getFreeVariables(LHS) ``` @@ -195,17 +195,17 @@ 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 ... + + kt-unfold => noop ... requires removeDuplicates(ARGS) ==K ARGS andBool isUnfoldable(LRP) - rule \implies(LRP(ARGS), RHS) - - kt-unfold => fail ... + rule \implies(LRP(ARGS), RHS) + + kt-unfold => fail ... requires removeDuplicates(ARGS) =/=K ARGS andBool isUnfoldable(LRP) @@ -245,10 +245,10 @@ 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 ... + + kt-unwrap => noop ... ``` @@ -261,12 +261,12 @@ for guessing an instantiation of the inductive hypothesis. If there are no implication contexts to collapse, we are done: ```k - rule GOAL - kt-collapse => noop ... + rule GOAL + kt-collapse => noop ... requires notBool(hasImplicationContext(GOAL)) - rule GOAL - imp-ctx-unfold => noop ... + rule GOAL + imp-ctx-unfold => noop ... requires notBool(hasImplicationContext(GOAL)) ``` @@ -276,27 +276,27 @@ 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 ... + + kt-collapse ... requires notBool hasImplicationContext(P) andBool hasImplicationContext(LHS) ``` ```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 ... + + 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 ... + + imp-ctx-unfold ... requires notBool hasImplicationContext(S) andBool hasImplicationContext(LSPATIAL) ``` @@ -308,23 +308,23 @@ 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 ... + + 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 ... + + 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,8 +345,8 @@ solver using `kt-solve-implications` ) , RHS:Pattern ) - - kt-collapse ... + + kt-collapse ... ``` #### Collapsing contexts (SL) @@ -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,18 +367,18 @@ context has no constraints. ) , RHS:Pattern ) - - kt-collapse + + kt-collapse => with-each-match( #match(terms: LSPATIAL, pattern: CTXLHS, variables: UNIVs) , kt-collapse ) ... - + requires UNIVs =/=K .Patterns ``` ```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,15 +389,15 @@ context has no constraints. ) , RHS:Pattern ) - - ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) + + ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) => kt-collapse ... - + 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,11 +407,11 @@ context has no constraints. ) , RHS:Pattern ) - - ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) + + ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) => fail ... - + requires UNIVs =/=K .Patterns andBool UNIVs -Patterns fst(unzip(SUBST)) =/=K .Patterns ``` @@ -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,15 +427,15 @@ Finally, we use matching on the no universal quantifiers case to collapse the co ) , RHS:Pattern ) - - kt-collapse + + kt-collapse => with-each-match( #match(terms: LSPATIAL, pattern: CTXLHS, variables: .Patterns) , kt-collapse ) ... - + - rule \implies( \and( ( sep ( \forall { .Patterns } + rule \implies( \and( ( sep ( \forall { .Patterns } implicationContext( \and(sep(_)) , CTXRHS) , LSPATIAL ) @@ -445,17 +445,17 @@ Finally, we use matching on the no universal quantifiers case to collapse the co ) , RHS:Pattern ) - - ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) + + ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) => kt-collapse ... - + ``` 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 ... + + 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,8 +482,8 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ) , RHS:Pattern ) - - kt-collapse => fail ... + + 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)) ... + + 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,8 +521,8 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ) , RHS:Pattern ) - - imp-ctx-unfold => right-unfold-eachRRP(getUnfoldables(CTXLHS)) ... + + imp-ctx-unfold => right-unfold-eachRRP(getUnfoldables(CTXLHS)) ... ``` #### Infrastructure @@ -542,23 +542,23 @@ 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 + + kt-collapse ... + rule \implies(\and(_, ( \and(Ps1), Ps2 => Ps1 ++Patterns Ps2)) , RHS) - - kt-collapse ... + + kt-collapse ... - rule \implies(\and( _ + rule \implies(\and( _ , (\exists { _ } P => P) , Ps) , _ ) - - kt-collapse ... + + kt-collapse ... ``` > gamma -> alpha beta /\ gamma -> psi @@ -566,19 +566,19 @@ 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-implications( STRAT) => ( kt-solve-implication( subgoal(\implies(\and(removeImplications(REST)), LHS), STRAT) , \and(LHS, RHS) ) . kt-solve-implications(STRAT) ) ... - + syntax Patterns ::= removeImplications(Patterns) [function] rule removeImplications(P, Ps) => P, removeImplications(Ps) @@ -587,19 +587,19 @@ 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(_) + + kt-solve-implications(_) ... - + requires hasImplication(REST) andBool notBool matchesImplication(P) - rule \implies(\and(LHS), _) - kt-solve-implications(STRAT) => noop ... + rule \implies(\and(LHS), _) + kt-solve-implications(STRAT) => noop ... requires notBool hasImplication(LHS) syntax Bool ::= matchesImplication(Pattern) [function] @@ -616,59 +616,59 @@ If the subgoal in the first argument succeeds add the second argument to the LHS ```k syntax Strategy ::= "kt-solve-implication" "(" Strategy "," Pattern ")" - rule kt-solve-implication(S, RHS) + rule kt-solve-implication(S, RHS) => S ~> kt-solve-implication(#hole, RHS) ... - + requires notBool isTerminalStrategy(S) - rule T:TerminalStrategy ~> kt-solve-implication(#hole, RHS) + rule T:TerminalStrategy ~> kt-solve-implication(#hole, RHS) => kt-solve-implication(T, RHS) ... - - rule kt-solve-implication(fail, RHS) => noop ... - rule kt-solve-implication(success, CONC) => noop ... - \implies(\and(LHS), RHS) - => \implies(\and(CONC, LHS), RHS) + rule kt-solve-implication(fail, RHS) => noop ... + rule kt-solve-implication(success, CONC) => noop ... + \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 - instantiate-universals-with-ground-terms + rule \implies(\and(LHS), RHS) #as GOAL + instantiate-universals-with-ground-terms => instantiate-universals-with-ground-terms(getForalls(LHS), removeDuplicates(getGroundTerms(GOAL))) ... - + - rule instantiate-universals-with-ground-terms( (\forall { (_ { S } #as V:Variable), UNIVs:Patterns } P:Pattern , REST_FORALLs) + rule instantiate-universals-with-ground-terms( (\forall { (_ { S } #as V:Variable), UNIVs:Patterns } P:Pattern , REST_FORALLs) => (substituteWithEach(\forall { UNIVs } P, V, filterBySort(GROUND_TERMS, S)) ++Patterns REST_FORALLs) , GROUND_TERMS ) ... - + - rule \implies(\and(LHS => P, LHS), RHS) - instantiate-universals-with-ground-terms( (\forall { .Patterns } P:Pattern , REST_FORALLs) => REST_FORALLs + 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) - instantiate-universals-with-ground-terms( (\forall { .Patterns } P:Pattern , REST_FORALLs) => REST_FORALLs + rule \implies(\and(LHS), RHS) + instantiate-universals-with-ground-terms( (\forall { .Patterns } P:Pattern , REST_FORALLs) => REST_FORALLs , _ ) ... - + requires P in LHS - rule instantiate-universals-with-ground-terms( .Patterns + rule instantiate-universals-with-ground-terms( .Patterns , _ ) => noop ... - + syntax Patterns ::= getForalls(Patterns) [function] rule getForalls(((\forall { _ } _) #as P), Ps) => P, getForalls(Ps) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index 1e1801139..e9c9a6351 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -341,34 +341,34 @@ The `with-each-match` strategy ```k syntax Strategy ::= "with-each-match" "(" MatchResults "," Strategy ")" - rule with-each-match( MRs, S ) + rule with-each-match( MRs, S ) => with-each-match( MRs, S, fail ) ... - + syntax Strategy ::= "with-each-match" "(" MatchResults "," Strategy "," Strategy ")" - rule with-each-match( (MR, MRs), SUCCESS , FAILURE ) + rule with-each-match( (MR, MRs), SUCCESS , FAILURE ) => with-each-match(MR, SUCCESS, FAILURE) | with-each-match(MRs, SUCCESS, FAILURE) ... - + requires MRs =/=K .MatchResults - rule with-each-match( (MR, .MatchResults), SUCCESS, FAILURE ) + rule with-each-match( (MR, .MatchResults), SUCCESS, FAILURE ) => MR ~> SUCCESS ... - + - rule with-each-match( .MatchResults, SUCCESS, FAILURE ) + rule with-each-match( .MatchResults, SUCCESS, FAILURE ) => FAILURE ... - + ``` Instantiate existentials using matching on the spatial part of goals: ```k - rule \implies(\and(sep(LSPATIAL), LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) - match + rule \implies(\and(sep(LSPATIAL), LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) + match => with-each-match(#match( terms: LSPATIAL , pattern: RSPATIAL , variables: Vs @@ -376,51 +376,51 @@ Instantiate existentials using matching on the spatial part of goals: , match ) ... - + 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 ) + + ( #matchResult(subst: SUBST, rest: .Patterns) ~> match ) => noop ... - + - rule \implies(LHS, \exists { Vs } \and(RSPATIAL, RHS)) - match => fail ... + rule \implies(LHS, \exists { Vs } \and(RSPATIAL, RHS)) + match => fail ... requires isPredicatePattern(LHS) andBool isSpatialPattern(RSPATIAL) - rule \implies(\and(LSPATIAL, LHS), \exists { Vs } RHS) - match => fail ... + rule \implies(\and(LSPATIAL, LHS), \exists { Vs } RHS) + match => fail ... requires isPredicatePattern(RHS) andBool isSpatialPattern(LSPATIAL) - rule ( #matchResult(subst: _, rest: REST) ~> match ) + rule ( #matchResult(subst: _, rest: REST) ~> match ) => fail ... - + requires REST =/=K .Patterns ``` ```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) + + 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) + + match-pto(P, Ps:Patterns) => with-each-match( #match( terms: LSPATIAL:Patterns , pattern: P @@ -431,18 +431,18 @@ 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 ) + + ( #matchResult(subst: SUBST, rest: _) ~> match-pto ) => noop ... - + syntax Patterns ::= getPartiallyInstantiatedPtos(Patterns, Patterns) [function] rule getPartiallyInstantiatedPtos((pto(L, R), Ps), Vs) @@ -459,10 +459,10 @@ Instantiate heap axioms: ```k syntax Strategy ::= "instantiate-axiom" "(" Pattern ")" | "instantiate-separation-logic-axioms" "(" Patterns ")" - rule instantiate-separation-logic-axioms + rule instantiate-separation-logic-axioms => instantiate-separation-logic-axioms(gatherHeapAxioms(.Patterns)) ... - + axiom _: heap(LOC, DATA) syntax Patterns ::= gatherHeapAxioms(Patterns) [function] @@ -471,7 +471,7 @@ Instantiate heap axioms: requires notBool(heap(LOC, DATA) in AXs) rule gatherHeapAxioms(AXs) => AXs [owise] - rule instantiate-separation-logic-axioms(heap(LOC, DATA), AXs) + rule instantiate-separation-logic-axioms(heap(LOC, DATA), AXs) => instantiate-separation-logic-axioms(AXs) . instantiate-axiom( \forall { !L { LOC }, !D {DATA} } \implies( \and(sep(pto(!L { LOC }, !D { DATA }))) @@ -484,15 +484,15 @@ Instantiate heap axioms: ) ) ... - - rule instantiate-separation-logic-axioms(.Patterns) => noop ... + + rule instantiate-separation-logic-axioms(.Patterns) => noop ... ``` Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil ```k - rule \implies(\and((sep(LSPATIAL)), LCONSTRAINT), RHS) - instantiate-axiom(\forall { Vs } + rule \implies(\and((sep(LSPATIAL)), LCONSTRAINT), RHS) + instantiate-axiom(\forall { Vs } \implies( \and(sep(AXIOM_LSPATIAL)) , AXIOM_RHS ) @@ -504,14 +504,14 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil ~> STRAT:Strategy ) ... - + 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 + + ( #matchResult( subst: SUBST, rest: _ ) , MRs ~> instantiate-axiom(\forall { Vs } \implies( _ , AXIOM_RHS @@ -520,46 +520,46 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil ) => ( MRs ~> STRAT:Strategy ) ... - + requires isPredicatePattern(AXIOM_RHS) - rule (.MatchResults ~> instantiate-axiom(_)) => noop ... + 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 ... + + 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 ... + + 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) ... + + 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) + + frame(pto(LOC, VAL), Ps) => subgoal( \implies( LHS , \and(filterClausesInvolvingVariable(LOC, RCONSTRAINTs)) ) @@ -571,32 +571,32 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil ~> frame(pto(LOC, VAL)) ~> frame(Ps) ... - + - 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 + + success ~> frame((pto(LOC, VAL) #as P), .Patterns) => .K ... - + 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) + + frame((S:Symbol(_) #as P), Ps) => frame(Ps) ... - + requires notBool S ==K pto - rule frame(.Patterns) => noop ... + rule frame(.Patterns) => noop ... syntax Patterns ::= filterClausesInvolvingVariable(Variable, Patterns) [function] rule filterClausesInvolvingVariable(V, (P, Ps)) @@ -609,15 +609,15 @@ 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 + + subsume-spatial => noop ... - + requires isPredicatePattern(\and(RHS)) ``` diff --git a/prover/strategies/reflexivity.md b/prover/strategies/reflexivity.md index 920554e51..2e658354d 100644 --- a/prover/strategies/reflexivity.md +++ b/prover/strategies/reflexivity.md @@ -4,11 +4,11 @@ module STRATEGY-REFLEXIVITY imports PROVER-CORE imports STRATEGIES-EXPORTED-SYNTAX - rule reflexivity => success ... - \equals(P, P) + rule reflexivity => success ... + \equals(P, P) - rule reflexivity => fail ... - \equals(P, Q) + rule reflexivity => fail ... + \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 7b0e4d8b0..68d1bbd50 100644 --- a/prover/strategies/replace-evar-with-func-constant.md +++ b/prover/strategies/replace-evar-with-func-constant.md @@ -9,16 +9,16 @@ module STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT imports PROVER-CORE imports STRATEGIES-EXPORTED-SYNTAX - rule + rule replace-evar-with-func-constant V,Vs => #rewfc(V,Vs) - ... + ... - rule + rule replace-evar-with-func-constant .Variables => #rewfc(PatternsToVariables(getFreeVariables(P, .Patterns))) - ... - P + ... + P syntax Variables ::= PatternsToVariables(Patterns) [function] rule PatternsToVariables(.Patterns) => .Variables @@ -28,26 +28,26 @@ module STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT syntax KItem ::= #rewfc(Variables) - rule #rewfc(.Variables) => noop ... + rule #rewfc(.Variables) => noop ... - rule (.K => #rewfc1(V)) + rule (.K => #rewfc1(V)) ~> #rewfc(V,Vs => Vs) - ... + ... syntax KItem ::= #rewfc1(Variable) | #rewfc2(Variable, Symbol) - rule #rewfc1(N{S} #as V) + rule #rewfc1(N{S} #as V) => #rewfc2(V, getFreshSymbol( GId, VariableName2String(N))) - ... + ... GId - P + P requires V in getFreeVariables(P, .Patterns) - rule #rewfc2(N{S}, Sym) => .K ... + 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 @@ -56,9 +56,9 @@ module STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT ... - rule #rewfc1(V) => "No such free variable" - ... - P + rule #rewfc1(V) => "No such free variable" + ... + P requires notBool (V in getFreeVariables(P, .Patterns)) endmodule diff --git a/prover/strategies/search-bound.md b/prover/strategies/search-bound.md index 1c4a34ff1..8bb093c23 100644 --- a/prover/strategies/search-bound.md +++ b/prover/strategies/search-bound.md @@ -8,19 +8,19 @@ module STRATEGY-SEARCH-BOUND imports PROVER-CORE imports STRATEGIES-EXPORTED-SYNTAX - rule search-fol(bound: 0) => fail - rule search-fol(bound: N) + rule search-fol(bound: 0) => fail + rule search-fol(bound: N) => normalize . simplify . ( ( instantiate-existentials . smt-cvc4 ) | (kt . search-fol(bound: N -Int 1)) | (right-unfold . search-fol(bound: N -Int 1)) ) ... - + requires N >Int 0 - rule search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... - rule search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) + rule search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... + rule search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) => normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat @@ -31,11 +31,11 @@ module STRATEGY-SEARCH-BOUND | ( kt . search-sl(kt-bound: KTBOUND -Int 1, unfold-bound: UNFOLDBOUND) ) ) ... - + requires KTBOUND >Int 0 - rule alternate-search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... - rule alternate-search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) + rule alternate-search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... + rule alternate-search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) => normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat @@ -46,11 +46,11 @@ module STRATEGY-SEARCH-BOUND | ( kt . alternate-search-sl(kt-bound: KTBOUND -Int 1, unfold-bound: UNFOLDBOUND) ) ) ... - + requires KTBOUND >Int 0 - rule kt-unfold-search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... - rule kt-unfold-search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) + rule kt-unfold-search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... + rule kt-unfold-search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) => normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat @@ -61,7 +61,7 @@ module STRATEGY-SEARCH-BOUND | ( kt-unf . kt-unfold-search-sl(kt-bound: KTBOUND -Int 1, unfold-bound: UNFOLDBOUND) ) ) ... - + requires KTBOUND >Int 0 endmodule diff --git a/prover/strategies/simplification.md b/prover/strategies/simplification.md index c3a1dac2f..2b887b7a4 100644 --- a/prover/strategies/simplification.md +++ b/prover/strategies/simplification.md @@ -18,8 +18,8 @@ module STRATEGY-SIMPLIFICATION ``` ```k - rule \implies(LHS => #lhsRemoveExistentials(LHS), RHS) - remove-lhs-existential => noop ... + rule \implies(LHS => #lhsRemoveExistentials(LHS), RHS) + remove-lhs-existential => noop ... syntax Pattern ::= #lhsRemoveExistentials(Pattern) [function] syntax Patterns ::= #lhsRemoveExistentialsPs(Patterns) [function] @@ -59,27 +59,27 @@ Normalize: ```k - rule P::Pattern => \and(P) - normalize ... + rule P::Pattern => \and(P) + normalize ... requires \and(...) :/=K P andBool \implies(...) :/=K P - rule \and(P) => \implies(\and(.Patterns), \and(P)) - normalize ... + 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 ... + + 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 ... + + normalize => noop ... - rule \not(_) #as P => #normalize(P) - normalize => noop ... + rule \not(_) #as P => #normalize(P) + normalize => noop ... syntax Pattern ::= #normalize(Pattern) [function] syntax Patterns ::= #normalizePs(Patterns) [function] @@ -106,8 +106,8 @@ Normalize: LHS terms of the form S(T, Vs) become S(V, Vs) /\ V = T ```k - rule \implies(LHS => #purify(LHS), RHS) ... - purify => noop ... + rule \implies(LHS => #purify(LHS), RHS) + purify => noop ... syntax Pattern ::= #purify(Pattern) [function] syntax Patterns ::= #purifyPs(Patterns) [function] @@ -150,22 +150,22 @@ 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) - abstract + rule \implies(LHS, RHS) + abstract => #getNewVariables(LHS, .Patterns) ~> #getNewVariables(RHS, .Patterns) ~> abstract ... - + - 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 ... + + (VsLHS:Patterns ~> VsRHS:Patterns ~> abstract) => noop ... syntax Patterns ::= #getNewVariables(Pattern, Patterns) [function] syntax Patterns ::= #getNewVariablesPs(Patterns, Patterns) [function] @@ -216,11 +216,11 @@ 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 ... + + lift-constraints => noop ... syntax Pattern ::= #liftConstraints(Pattern) [function] rule #liftConstraints(P) => P requires isPredicatePattern(P) @@ -270,8 +270,8 @@ Lift `\or`s on the left hand sides of implications ``` ```k - rule \implies(\or(LHSs), RHS) => \and( #liftOr(LHSs, RHS)) - lift-or => noop ... + rule \implies(\or(LHSs), RHS) => \and( #liftOr(LHSs, RHS)) + lift-or => noop ... syntax Patterns ::= "#liftOr" "(" Patterns "," Pattern ")" [function] rule #liftOr(.Patterns, RHS) => .Patterns @@ -285,8 +285,8 @@ 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) - simplify ... + rule \implies(\forall { .Patterns } \and(LHS) => \and(LHS), RHS) + simplify ... ``` > phi(x, y) -> psi(y) @@ -294,8 +294,8 @@ 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) - simplify ... + rule \implies(\exists { _ } \and(LHS) => \and(LHS), RHS) + simplify ... ``` > LHS /\ phi -> RHS @@ -303,8 +303,8 @@ 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)) - simplify => noop ... + rule \implies(\and(LHS), \exists { _ } \and(RHS => RHS -Patterns LHS)) + simplify => noop ... ``` ### Instantiate Existials @@ -316,22 +316,22 @@ Lift `\or`s on the left hand sides of implications ``` ```k - rule \implies( \and(LHS) , \exists { EXIST } \and(RHS) ) #as GOAL - (. => getAtomForcingInstantiation(RHS, getExistentialVariables(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 ... + + (INSTANTIATION => .) ~> instantiate-existentials ... requires INSTANTIATION =/=K .Patterns - rule (.Patterns ~> instantiate-existentials) => noop ... + rule (.Patterns ~> instantiate-existentials) => noop ... syntax Patterns ::= getAtomForcingInstantiation(Patterns, Patterns) [function] rule getAtomForcingInstantiation((\equals(X:Variable, P), Ps), EXISTENTIALS) @@ -357,27 +357,27 @@ Lift `\or`s on the left hand sides of implications ``` ```k - rule \implies(\and(LHS), _) - substitute-equals-for-equals + rule \implies(\and(LHS), _) + substitute-equals-for-equals => (makeEqualitySubstitution(LHS) ~> substitute-equals-for-equals) ... - + - rule (SUBST:Map ~> substitute-equals-for-equals) + rule (SUBST:Map ~> substitute-equals-for-equals) => noop ... - + 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) + + (SUBST:Map ~> substitute-equals-for-equals) => substitute-equals-for-equals ... - + requires SUBST =/=K .Map syntax Map ::= makeEqualitySubstitution(Patterns) [function] @@ -404,8 +404,8 @@ Lift `\or`s on the left hand sides of implications ```k - rule \forall{_} P => P - universal-generalization => noop ... + rule \forall{_} P => P + universal-generalization => noop ... ``` @@ -423,17 +423,17 @@ Gamma |- C[C_\sigma[\exists X. Phi]] ``` ```k - rule P + rule P => propagateExistsThroughApplicationVisitorResult( visitTopDown( propagateExistsThroughApplicationVisitor(N), P ) ) - - propagate-exists-through-application N + + propagate-exists-through-application N => noop - ... + ... syntax Visitor ::= propagateExistsThroughApplicationVisitor(Int) @@ -492,17 +492,17 @@ Gamma |- C[C_\sigma[P /\ Phi]] ``` ```k - rule T + rule T => pptaVisitorResult( visitTopDown( pptaVisitor(P, N), T ) ) - - propagate-predicate-through-application(P, N) + + propagate-predicate-through-application(P, N) => noop - ... + ... syntax Visitor ::= pptaVisitor(Pattern, Int) @@ -638,17 +638,17 @@ Gamma |- C[\exists X. Pi /\ Psi] ```k - rule T + rule T => visitorResult.getPattern( visitTopDown( pcteVisitor(N, M), T ) ) - - + + propagate-conjunct-through-exists(N, M) => noop - ... + ... syntax Visitor ::= pcteVisitor(Int, Int) diff --git a/prover/strategies/smt.md b/prover/strategies/smt.md index bfb84e10a..f7072d836 100644 --- a/prover/strategies/smt.md +++ b/prover/strategies/smt.md @@ -198,41 +198,41 @@ module STRATEGY-SMT imports STRATEGIES-EXPORTED-SYNTAX imports ML-TO-SMTLIB2 - rule GOAL - smt-z3 + rule GOAL + smt-z3 => if Z3CheckSAT(Z3Prelude ++SMTLIB2Script ML2SMTLIB(\not(GOAL))) ==K unsat then success else fail fi ... - + .K => smt-z3 ... - rule GOAL - smt-z3 => fail + rule GOAL + smt-z3 => fail - rule GOAL + rule GOAL GId - smt-cvc4 + smt-cvc4 => if CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \not(GOAL), collectDeclarations(GId))) ==K unsat then success else fail fi ... - + .K => smt-cvc4 ... 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 + check-lhs-constraint-unsat => if CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(LCONSTRAINTS), collectDeclarations(GId))) ==K unsat then success else noop fi ... - + .K => check-lhs-constraint-unsat ... requires isPredicatePattern(\and(LCONSTRAINTS)) @@ -241,8 +241,8 @@ module STRATEGY-SMT We have an optimized version of trying both: Only call z3 if cvc4 reports unknown. ```k - rule GOAL - smt + rule GOAL + smt => #fun( CVC4RESULT => if CVC4RESULT ==K unsat then success @@ -254,17 +254,17 @@ We have an optimized version of trying both: Only call z3 if cvc4 reports unknow fi ) (CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIB(\not(GOAL))):CheckSATResult) ... - + .K => smt ~> CVC4Prelude ++SMTLIB2Script ML2SMTLIB(GOAL) ... ``` ```k - rule GOAL + rule GOAL GId - smt-debug + smt-debug => wait ~> CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \not(GOAL), collectDeclarations(GId))):CheckSATResult ... - + .K => smt ~> CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \not(GOAL), collectDeclarations(GId)) ... requires isPredicatePattern(GOAL) ``` @@ -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 71b5f853b..8ddad6fd9 100644 --- a/prover/strategies/unfolding.md +++ b/prover/strategies/unfolding.md @@ -69,30 +69,30 @@ module STRATEGY-UNFOLDING syntax Strategy ::= "left-unfold-eachBody" "(" Pattern "," Pattern ")" | "left-unfold-oneBody" "(" Pattern "," Pattern ")" - rule left-unfold-eachBody(LRP, \or(BODY, BODIES)) + rule left-unfold-eachBody(LRP, \or(BODY, BODIES)) => left-unfold-oneBody(LRP, BODY) & left-unfold-eachBody(LRP, \or(BODIES)) ... - - rule left-unfold-eachBody(LRP, \or(.Patterns)) + + rule left-unfold-eachBody(LRP, \or(.Patterns)) => success ... - + - 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 ... + + 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 ... + + left-unfold-oneBody(LRP, \exists { _ } \and(BODY)) => noop ... .K => left-unfold-oneBody(LRP, \and(BODY)) ... requires LRP in LHS ``` @@ -107,28 +107,28 @@ implicatations. The resulting goals are equivalent to the initial goal. | "left-unfold-Nth-eachBody" "(" Int "," Pattern "," Pattern ")" | "left-unfold-Nth-oneBody" "(" Int "," Pattern "," Pattern ")" - rule left-unfold-Nth(M) + rule left-unfold-Nth(M) => left-unfold-Nth-eachLRP(M, getUnfoldables(LHS)) ... - - \implies(\and(LHS), RHS) + + \implies(\and(LHS), RHS) - rule left-unfold-Nth-eachLRP(M, PS) + rule left-unfold-Nth-eachLRP(M, PS) => fail ... - + requires M =Int getLength(PS) - rule left-unfold-Nth-eachLRP(M, PS) + rule left-unfold-Nth-eachLRP(M, PS) => left-unfold-Nth-eachBody(M, getMember(M, PS), unfold(getMember(M, PS))) ... - + requires 0 <=Int M andBool M left-unfold-Nth-eachBody(M, LRP, Bodies) + rule left-unfold-Nth-eachBody(M, LRP, Bodies) => left-unfold-eachBody(LRP, Bodies) ... - + ``` ### Right Unfold @@ -142,39 +142,39 @@ Note that the resulting goals is stonger than the initial goal (i.e. | "right-unfold-eachBody" "(" Pattern "," Pattern ")" | "right-unfold-oneBody" "(" Pattern "," Pattern ")" - rule right-unfold ( SYMBOL ) + rule right-unfold ( SYMBOL ) => right-unfold-eachRRP( filterByConstructor(getUnfoldables(RHS), SYMBOL) ) ... - - \implies(LHS, \exists { _ } \and(RHS)) - rule right-unfold + + \implies(LHS, \exists { _ } \and(RHS)) + rule right-unfold => right-unfold-eachRRP(getUnfoldables(RHS)) ... - - \implies(LHS, \exists { _ } \and(RHS)) - rule right-unfold-all(bound: N) + + \implies(LHS, \exists { _ } \and(RHS)) + rule right-unfold-all(bound: N) => right-unfold-all(symbols: getRecursiveSymbols(.Patterns), bound: N) ... - - rule right-unfold-all(symbols: SYMs, bound: N) + + rule right-unfold-all(symbols: SYMs, bound: N) => right-unfold-perm(permutations: perm(SYMs), bound: N) ... - - rule right-unfold-perm(permutations: .List, bound: _) + + rule right-unfold-perm(permutations: .List, bound: _) => noop ... - - rule right-unfold-perm(permutations: ListItem(Ps) L, bound: N) + + rule right-unfold-perm(permutations: ListItem(Ps) L, bound: N) => right-unfold(symbols: Ps, bound: N) | right-unfold-perm(permutations: L, bound: N) ... - - rule right-unfold(symbols: Ps, bound: N) + + rule right-unfold(symbols: Ps, bound: N) => fail ... - + requires Ps ==K .Patterns orBool N <=Int 0 - rule right-unfold(symbols: P, Ps, bound: N) + rule right-unfold(symbols: P, Ps, bound: N) => normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals . ( ( match . spatial-patterns-equal . smt-cvc4 ) @@ -182,26 +182,26 @@ Note that the resulting goals is stonger than the initial goal (i.e. | ( right-unfold(symbols: Ps, bound: N) ) ) ... - + requires N =/=Int 0 - rule right-unfold-eachRRP(P, PS) + rule right-unfold-eachRRP(P, PS) => right-unfold-eachBody(P, unfold(P)) | right-unfold-eachRRP(PS) ... - - rule right-unfold-eachRRP(.Patterns) + + rule right-unfold-eachRRP(.Patterns) => fail ... - - rule right-unfold-eachBody(RRP, \or(BODY, BODIES)) + + rule right-unfold-eachBody(RRP, \or(BODY, BODIES)) => right-unfold-oneBody(RRP, BODY) | right-unfold-eachBody(RRP, \or(BODIES)) ... - - rule right-unfold-eachBody(RRP, \or(.Patterns)) + + rule right-unfold-eachBody(RRP, \or(.Patterns)) => fail ... - + ``` ### Permuting list of recursive symbols for use in right-unfold-all @@ -222,11 +222,11 @@ 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)) - => \implies(LHS, \exists { E1 ++Patterns E2 } - \and(substPatternsMap(RHS, zip((RRP, .Patterns), (\and(BODY), .Patterns))))) ... - - right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) => noop ... + 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)) ~> RHS ~> substPatternsMap(RHS, zip((RRP, .Patterns), (\and(BODY), .Patterns))) @@ -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,8 +263,8 @@ rule addPattern(P, ListItem(Ps:Patterns) L) => ListItem(P, Ps) addPattern(P, L) ) , RHS:Pattern ) - - right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) => noop ... + + right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) => noop ... .K => right-unfold-oneBody(RRP, \exists { E2 } \and(BODY)) ~> RHS ~> substPatternsMap(RHS, zip((RRP, .Patterns), (\and(BODY), .Patterns))) @@ -284,40 +284,40 @@ or `N` is out of range, `right-unfold(M,N) => fail`. | "right-unfold-Nth-eachBody" "(" Int "," Int "," Pattern "," Pattern ")" | "right-unfold-Nth-oneBody" "(" Int "," Int "," Pattern "," Pattern ")" - rule right-unfold-Nth (M,N) => fail ... + rule right-unfold-Nth (M,N) => fail ... requires (M right-unfold-Nth (M,N) + rule right-unfold-Nth (M,N) => 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 ... + rule right-unfold-Nth-eachRRP(M, N, RRPs) => fail ... requires getLength(RRPs) <=Int M - rule right-unfold-Nth-eachRRP(M, N, RRPs:Patterns) + rule right-unfold-Nth-eachRRP(M, N, RRPs:Patterns) => right-unfold-Nth-eachBody(M, N, getMember(M, RRPs), unfold(getMember(M, RRPs))) ... - + requires getLength(RRPs) >Int M - rule right-unfold-Nth-eachBody(M, N, RRP, \or(Bodies)) + rule right-unfold-Nth-eachBody(M, N, RRP, \or(Bodies)) => fail ... - + requires getLength(Bodies) <=Int N - rule right-unfold-Nth-eachBody(M, N, RRP, \or(Bodies)) + rule right-unfold-Nth-eachBody(M, N, RRP, \or(Bodies)) => right-unfold-Nth-oneBody(M, N, RRP, getMember(N, Bodies)) ... - + requires getLength(Bodies) >Int N - rule right-unfold-Nth-oneBody(M, N, RRP, Body) + rule right-unfold-Nth-oneBody(M, N, RRP, Body) => right-unfold-oneBody(RRP, Body) ... - + ``` ```k diff --git a/prover/t/use-local-axiom.kore b/prover/t/use-local-axiom.kore new file mode 100644 index 000000000..1ea4ca410 --- /dev/null +++ b/prover/t/use-local-axiom.kore @@ -0,0 +1,4 @@ +// Tests that we can use local axioms. +symbol f(Int) : Int +claim \implies(\equals(f(1), 1), \equals(f(1), 1)) +strategy intros H . apply-equation -> H at 0 by [] . reflexivity diff --git a/prover/t/use-proven-claims.kore b/prover/t/use-proven-claims.kore new file mode 100644 index 000000000..accc3cbad --- /dev/null +++ b/prover/t/use-proven-claims.kore @@ -0,0 +1,18 @@ +// Tests that we can reuse proven claims + +symbol f(Int) : Int + +axiom a1: \equals(f(1), 1) + +claim a2: \equals(f(f(1)), 1) + +strategy apply-equation -> a1 at 0 by [] + . apply-equation -> a1 at 0 by [] + . reflexivity + + +claim a3: \equals(f(f(f(1))), 1) +strategy apply-equation -> a1 at 0 by [] + . apply-equation -> a2 at 0 by [] // <- HERE + . reflexivity + diff --git a/prover/t/use-proven-claims.kore.expected b/prover/t/use-proven-claims.kore.expected new file mode 100644 index 000000000..cfd344695 --- /dev/null +++ b/prover/t/use-proven-claims.kore.expected @@ -0,0 +1,34 @@ + + + 0 + + + + id: ., parent: . + + \and ( .Patterns ) + + + . + n + . + + + .LocalDeclCellSet + + + . + + + + + axiom a1 : \equals ( f ( 1 , .Patterns ) , 1 ) + + axiom a2 : \equals ( f ( f ( 1 , .Patterns ) , .Patterns ) , 1 ) + + axiom a3 : \equals ( f ( f ( f ( 1 , .Patterns ) , .Patterns ) , .Patterns ) , 1 ) + + symbol f ( Int , .Sorts ) : Int + + + diff --git a/prover/utils/load-named.md b/prover/utils/load-named.md deleted file mode 100644 index f3c9d9a9b..000000000 --- a/prover/utils/load-named.md +++ /dev/null @@ -1,29 +0,0 @@ -```k -module LOAD-NAMED-SYNTAX - syntax AxiomOrClaimName - - syntax KItem ::= loadNamed(AxiomOrClaimName) - -endmodule - -module LOAD-NAMED-RULES - imports LOAD-NAMED-SYNTAX - imports PROVER-CORE - - rule loadNamed(Name) => P ... - - ... - Name - P - success - ... - - - rule loadNamed(Name) => P ... - axiom Name : P - - rule loadNamed(Name) => P ... - axiom Name : P - -endmodule -```