diff --git a/prover/README.md b/prover/README.md index a4125e176..fb275b001 100644 --- a/prover/README.md +++ b/prover/README.md @@ -1,39 +1,64 @@ -Build Instructions +Building +======== + +Besides the normal K dependencies, the matching logic prover also depends on +`pandoc-tangle`, `python3` and `ninja-build`. +On an Ubuntu Bionic (18.04) system you can install the following packages: + +``` +apt install autoconf curl flex gcc libffi-dev libmpfr-dev libtool make \ + maven ninja-build opam openjdk-8-jdk pandoc pkg-config python3 \ + time zlib1g-dev +``` + +Source organization +=================== + +The source code is organized under the following directories: + +* `drivers/`: Modules for reading input formats and converting them to the + matching logic `kore` format, and loading them into the configuration. +* `lang/`: Tools for working with the source languages (kore and smtlib) +* `strategies/`: The various proof rules are implemented as "strategies". + + * `strategies/core.md`: Core strategies, such as composition and choice. + * `strategies/knaster-tarski.md`: Strategies relating to using the Knaster Tarki rule + and contexts. + * `strategies/unfolding.md`: Strategies relating to unfolding fixed points. + * `strategies/matching.md`: Strategies relating to pattern matching + * `strategies/smt.md`: Strategies that utilize an SMT solver. + +Tests & Benchmarks ================== -Install these dependencies: +Organization +------------- -* pandoc -* ninja-build -* opam -* maven -* openjdk-11-jdk +The tests and benchmarks are stored under the `t/` directory in the following +subdirectories: -Run `./build` to run all tests. -Run `./build .build/t/TEST-NAME.smt2.prover-smt-krun` to run an individual test. +* `t/ltl`: LTL Tests. +* `t/sl`: Separation Logic tests and benchmarks. + * `t/sl/SL-COMP18/`: This is a git submodule containing all the `SL-COMP` tests. + * `t/sl/SL-COMP18/bench/qf_shid_entl/`: These are the benchmarks we aim to complete. +* `t/fol`: FOL Tests. -Repository Layout -================= +In addition, unit tests are stored under `t/unit/` - * `prover.md` contains the implementation - * `direct-proof.md` contains solutions to domain specific queries that - can be checked against an SMT solver. - * The `t/` directory contains a number of tests and experiments, detailed below. +File formats +------------ -Tests & Experiments -=================== +The prover accepts two file formats: + +1. `.kore`: This is the "native" matching logic based format that the prover accepts. +2. `.smt`: This is the [SMT-LIB 2.6 format] with the [extensions for SL-COMP] + +[SMT-LIB 2.6 format]: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf +[extensions for SL-COMP]: https://sl-comp.github.io/docs/smtlib-sl.pdf + +Running tests +============= -In the `t/` directory, we have a number of tests. Each test consists of a -"claim" (the matching logic pattern that we are trying to prove), and a -strategy. The strategy directs the prover in choosing which axioms to apply. The -`search-bound(N)` strategy causes the prover to begin a bounded depth first -search for a proof of the claim. All lemmas named in the paper except one -(`t/lsegright-list-implies-list`; see below) are proved with a search depth of 5 -or lower. The program verification example is proved with a search up to depth -3. In addition, there is an example of a coninductive proof -(`t/zip-zeros-ones-implies-alters.prover`; see below). - -The `t/zip-zeros-ones-implies-alters.prover` test proof is at a depth of 17, -and so we specify the strategy to reduce the search space. -The `t/lsegright-list-implies-list` test needs some help in instantiating -existential variables, which is done by specifying a strategy as a substitution. +* To run a select group of tests, called the "smoke-tests", run: `./build smoke-tests`. +* To run a single kore test named "t/foo.kore", run `./build .build/t/foo.kore.prover-kore-run` +* To run a single smt test named "t/foo.smt", run `./build .build/t/foo.kore.prover-smt-run` diff --git a/prover/build b/prover/build index f602d28cc..120b19ca0 100755 --- a/prover/build +++ b/prover/build @@ -61,8 +61,9 @@ 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_kore.tests(inputs = glob('t/ltl/*.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' @@ -105,7 +106,7 @@ def make_test(rule, test): def sl_comp_test(test, log_file): global tests_with_timeout - test_no_timeout = make_test(prover_smt.krun(), test) + test_no_timeout = make_test(prover_smt.krun().ext('prover-smt-run'), test) test_with_timeout = make_test(krun_with_timeout(timeout_for_test(test)), test) \ .then(log_on_success(log_file, test)) return (test_no_timeout, test_with_timeout) @@ -131,8 +132,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 +149,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..6f9d931c2 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 @@ -23,11 +23,11 @@ module PROVER-CONFIGURATION 1 - + .K .K + \or(.Patterns) // TODO: make this optional instead? $COMMANDLINE:CommandLine ~> $PGM:Pgm - .K .K .K @@ -91,7 +91,7 @@ module DRIVER-BASE .K .K - .K + .K ... diff --git a/prover/drivers/kore-driver.md b/prover/drivers/kore-driver.md index 3135043be..a8556ca78 100644 --- a/prover/drivers/kore-driver.md +++ b/prover/drivers/kore-driver.md @@ -71,6 +71,7 @@ in the subgoal and the claim of the named goal remains intact. => subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT)) ... + rule (success => .K) ~> D:Declarations ... ``` ```k diff --git a/prover/drivers/smt-driver.md b/prover/drivers/smt-driver.md index 75829bac9..608d48637 100644 --- a/prover/drivers/smt-driver.md +++ b/prover/drivers/smt-driver.md @@ -138,9 +138,10 @@ module DRIVER-SMT ( .Bag => symbol pto(SMTLIB2SortToSort(LOC), SMTLIB2SortToSort(DATA)) : Heap - symbol parameterizedSymbol(nil, SMTLIB2SortToSort(LOC)) ( .Sorts ) : SMTLIB2SortToSort(LOC) + symbol nil { SMTLIB2SortToSort(LOC) } (.Sorts) : SMTLIB2SortToSort(LOC) axiom !N:AxiomName : heap(SMTLIB2SortToSort(LOC), SMTLIB2SortToSort(DATA)) - axiom !N:AxiomName : functional(parameterizedSymbol(nil, SMTLIB2SortToSort(LOC))) + axiom !M:AxiomName : functional(nil { SMTLIB2SortToSort(LOC) }) + axiom !P:AxiomName : constructor(nil { SMTLIB2SortToSort(LOC) }) ) ... @@ -159,6 +160,7 @@ module DRIVER-SMT => sort SMTLIB2SortToSort(SORT1) symbol SMTLIB2SimpleSymbolToSymbol(CTOR)(SelectorDecListToSorts(SELDECs)) : SMTLIB2SortToSort(SORT1) axiom !N:AxiomName : functional(SMTLIB2SimpleSymbolToSymbol(CTOR)) + axiom !M:AxiomName : constructor(SMTLIB2SimpleSymbolToSymbol(CTOR)) ) ... @@ -185,10 +187,10 @@ module DRIVER-SMT ) ... - syntax K ::= #rest(SMTLIB2FunctionDecList, SMTLIB2TermList) + syntax K ::= #mutualRecUnfold(SMTLIB2FunctionDecList, SMTLIB2TermList) rule _:GoalBuilder - ~> ( #rest(_, _) + ~> ( #mutualRecUnfold(_, _) ~> (define-funs-rec ( .SMTLIB2FunctionDecList ) ( .SMTLIB2TermList ) ) => .K ) @@ -196,7 +198,7 @@ module DRIVER-SMT rule #goal( goal: _, strategy: unfold-mut-recs . REST_STRAT, expected: _ ) - ~> (.K => #rest(FDs, BODIEs)) + ~> (.K => #mutualRecUnfold(FDs, BODIEs)) ~> (define-funs-rec ( FDs ) ( BODIEs ) ) ... @@ -217,7 +219,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 @@ -226,7 +228,7 @@ module DRIVER-SMT [owise] rule _:GoalBuilder - ~> #rest(FDALLs, BODYALLs) + ~> #mutualRecUnfold(FDALLs, BODYALLs) ~> ( (define-funs-rec ( (ID (ARGs) RET) FDs ) ( BODY BODIEs ) ) => unfoldMR( SMTLIB2SimpleSymbolToSymbol(ID)(SMTLIB2SortedVarListToPatterns(ARGs)) , SMTLIB2TermToPattern(BODY, SMTLIB2SortedVarListToPatterns(ARGs)) @@ -252,7 +254,7 @@ module DRIVER-SMT ), #gatherRest(FDs, BODIEs) syntax K ::= unfoldMR(Pattern, Pattern, PatternTupleList) - rule _:GoalBuilder ~> #rest(_, _) + rule _:GoalBuilder ~> #mutualRecUnfold(_, _) ~> ( unfoldMR(ID:Symbol(ARGs), BODY, .PatternTupleList) => .K ) @@ -267,14 +269,14 @@ module DRIVER-SMT ) ... - rule _:GoalBuilder ~> #rest(_, _) + rule _:GoalBuilder ~> #mutualRecUnfold(_, _) ~> ( unfoldMR(ID:Symbol(ARGs1), BODY1, ((ID:Symbol(ARGs2), BODY2), REST)) => unfoldMR(ID:Symbol(ARGs1), BODY1, REST) ) ... - rule _:GoalBuilder ~> #rest(_, _) + rule _:GoalBuilder ~> #mutualRecUnfold(_, _) ~> ( unfoldMR(ID1:Symbol(ARGs1), BODY1, ((ID2:Symbol(ARGs2), BODY2), REST)) => unfoldMR(ID1:Symbol(ARGs1), substituteBRPs(BODY1, ID2, ARGs2, BODY2), REST) ) @@ -319,23 +321,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 @@ -404,13 +403,9 @@ Clear the `` cell once we are done: rule #removeExistentialsPatterns(P, Ps) => #removeExistentials(P) ++Patterns #removeExistentialsPatterns(Ps) rule #removeExistentialsPatterns(.Patterns) => .Patterns - syntax Pattern ::= #normalizeQFree(Pattern) [function] - | #normalizeDefinition(Pattern) [function] + syntax Pattern ::= #normalizeDefinition(Pattern) [function] | #pushExistentialsDisjunction(Pattern) [function] - rule #normalizeDefinition(P) => #pushExistentialsDisjunction(\exists { #getExistentialVariables(P) } #normalizeQFree(#removeExistentials(P))) - rule #normalizeQFree(\or(Ps)) => \or(#flattenOrs(#dnfPs(Ps))) - rule #normalizeQFree(P) => #normalizeQFree(\or(P, .Patterns)) - [owise] + rule #normalizeDefinition(P) => #pushExistentialsDisjunction(\exists { #getExistentialVariables(P) } #flattenAssoc(#liftOr(#nnf(\or(\and(#removeExistentials(P))))))) rule #pushExistentialsDisjunction(\exists{Vs} \or(Ps)) => \or(#exists(Ps, Vs)) syntax Strategy ::= #statusToTerminalStrategy(CheckSATResult) [function] @@ -437,7 +432,7 @@ Clear the `` cell once we are done: rule SMTLIB2TermToPattern(I:Int, _) => I rule SMTLIB2TermToPattern(#token("true", "LowerName"), _) => \top() rule SMTLIB2TermToPattern(#token("false", "LowerName"), _) => \bottom() - rule SMTLIB2TermToPattern((as nil SORT), _) => parameterizedSymbol(nil, SMTLIB2SortToSort(SORT))(.Patterns) + rule SMTLIB2TermToPattern((as nil SORT), _) => nil { SMTLIB2SortToSort(SORT) } (.Patterns) rule SMTLIB2TermToPattern((underscore emp _ _), _) => emp(.Patterns) rule SMTLIB2TermToPattern((ID Ts), Vs) => SMTLIB2SimpleSymbolToSymbol(ID)(SMTLIB2TermListToPatterns(Ts, Vs)) diff --git a/prover/drivers/unit-tests.md b/prover/drivers/unit-tests.md index 8cb71d5bf..bd9077245 100644 --- a/prover/drivers/unit-tests.md +++ b/prover/drivers/unit-tests.md @@ -8,11 +8,13 @@ requires "t/unit/match-assoc-comm.k" requires "t/unit/subst.k" requires "t/unit/syntactic-match.k" requires "t/unit/visitor.k" +requires "t/unit/dnf.k" ``` ```k module DRIVER-UNIT-TEST imports TEST-CHECKSAT + imports TEST-DNF imports TEST-MATCH-ASSOC imports TEST-MATCH-ASSOC-COMM imports TEST-SUBST @@ -27,7 +29,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..148e69dc6 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -53,6 +53,7 @@ module TOKENS | "sep" [token] | "nil" [token] | "emp" [token] + syntax Symbol ::= "nil" "{" Sort "}" // Arith syntax LowerName ::= "plus" [token] @@ -132,7 +133,7 @@ module KORE syntax Ints ::= List{Int, ","} ``` -We allow two "variaties" of variables: the first, identified by a String, is for +We allow two "varieties" of variables: the first, identified by a String, is for use in defining claims; the second, identified by a String and an Int subscript is to be used for generating fresh variables. *The second variety must be used only in this scenario*. @@ -140,12 +141,15 @@ only in this scenario*. ```k syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)] syntax SetVariable ::= SharpName [klabel(setVariable)] + syntax Context ::= VariableName "[" Pattern "]" [klabel(context)] syntax Pattern ::= Int | Variable | SetVariable | Symbol | Symbol "(" Patterns ")" [klabel(apply)] + | Context + | "\\top" "(" ")" [klabel(top)] | "\\bottom" "(" ")" [klabel(bottom)] | "\\equals" "(" Pattern "," Pattern ")" [klabel(equals)] @@ -158,6 +162,8 @@ only in this scenario*. | "\\exists" "{" Patterns "}" Pattern [klabel(exists)] | "\\forall" "{" Patterns "}" Pattern [klabel(forall)] + | "\\mu" SetVariable "." Pattern [klabel(mu)] + | "\\nu" SetVariable "." Pattern [klabel(nu)] /* Sugar for \iff, \mu and application */ | "\\iff-lfp" "(" Pattern "," Pattern ")" [klabel(ifflfp)] @@ -167,6 +173,7 @@ only in this scenario*. // sugar for commonly needed axioms | "\\typeof" "(" Pattern "," Sort ")" | "functional" "(" Symbol ")" + | "constructor" "(" Symbol ")" | "partial" "(" Patterns ")" | "heap" "(" Sort "," Sort ")" // Location, Data | "\\hole" "(" ")" [klabel(Phole)] @@ -193,7 +200,7 @@ only in this scenario*. syntax Declarations ::= Declaration Declarations syntax Declarations ::= ".Declarations" [klabel(.Declarations), symbol] - syntax Variable ::= "#hole" + syntax VariableName ::= "#hole" // Sugar for `\exists #hole . #hole /\ floor(Arg1 -> Arg2) syntax Pattern ::= implicationContext(Pattern, Pattern) [klabel(implicationContext)] @@ -218,11 +225,9 @@ module KORE-HELPERS syntax String ::= SortToString(Sort) [function, functional, hook(STRING.token2string)] syntax String ::= SymbolToString(Symbol) [function, functional, hook(STRING.token2string)] + rule SymbolToString(nil { SORT }) => SymbolToString(nil) +String "_" +String SortToString(SORT) syntax LowerName ::= StringToSymbol(String) [function, functional, hook(STRING.string2token)] - syntax Symbol ::= parameterizedSymbol(Symbol, Sort) [function] - rule parameterizedSymbol(SYMBOL, SORT) => StringToSymbol(SymbolToString(SYMBOL) +String "_" +String SortToString(SORT)) - syntax Bool ::= Pattern "in" Patterns [function] rule P in (P, P1s) => true rule P in (P1, P1s) => P in P1s requires P =/=K P1 @@ -296,6 +301,10 @@ module KORE-HELPERS rule areFunctional(GId, P, Ps) => isFunctional(GId, P) andBool areFunctional(GId, Ps) + syntax Bool ::= isConstructor(Pattern) [function] + rule [[ isConstructor(S) => true ]] + axiom _: constructor(S) + syntax Sort ::= getReturnSort(Pattern) [function] rule getReturnSort( I:Int ) => Int rule getReturnSort( _ { S } ) => S @@ -314,6 +323,7 @@ module KORE-HELPERS rule getReturnSort( lte ( ARGS ) ) => Bool rule getReturnSort( gte ( ARGS ) ) => Bool rule getReturnSort( isMember ( _ ) ) => Bool + rule getReturnSort( nil { SORT } ( _ ) ) => SORT rule [[ getReturnSort( R ( ARGS ) ) => S ]] symbol R ( _ ) : S rule [[ getReturnSort( R ( ARGS ) ) => S ]] @@ -344,6 +354,31 @@ module KORE-HELPERS => false requires getReturnSort(P) =/=K S + rule getReturnSort(\mu _ . Phi) => getReturnSort(Phi) + rule getReturnSort(\nu _ . Phi) => getReturnSort(Phi) + rule getReturnSort(\or(P, Ps)) => unionSort(getReturnSort(P), getReturnSort(\or(Ps))) + rule getReturnSort(\or(.Patterns)) => BottomSort + rule getReturnSort(\and(P, Ps)) => intersectSort(getReturnSort(P), getReturnSort(\and(Ps))) + rule getReturnSort(\and(.Patterns)) => TopSort + rule getReturnSort(_:SetVariable) => TopSort + + rule getReturnSort(\exists{Vs} P) => getReturnSort(P) + + syntax UpperName ::= "TopSort" [token] + | "BottomSort" [token] + + syntax Sort ::= unionSort(Sort, Sort) [function] + rule unionSort(TopSort, S) => TopSort + rule unionSort(S, TopSort) => TopSort + rule unionSort(BottomSort, S) => S + rule unionSort(S, BottomSort) => S + + syntax Sort ::= intersectSort(Sort, Sort) [function] + rule intersectSort(TopSort, S) => S + rule intersectSort(S, TopSort) => S + rule intersectSort(BottomSort, S) => BottomSort + rule intersectSort(S, BottomSort) => BottomSort + syntax Bool ::= isUnfoldable(Symbol) [function] rule [[ isUnfoldable(S:Symbol) => true ]] axiom _ : \forall {_} \iff-lfp(S(_), _) @@ -402,6 +437,7 @@ module KORE-HELPERS rule getFreeVariables(N:Int, .Patterns) => .Patterns rule getFreeVariables(X:Variable, .Patterns) => X, .Patterns + rule getFreeVariables(X:SetVariable, .Patterns) => X, .Patterns rule getFreeVariables(S:Symbol, .Patterns) => .Patterns rule getFreeVariables(S:Symbol(ARGS) , .Patterns) => getFreeVariables(ARGS) @@ -424,12 +460,22 @@ module KORE-HELPERS => getFreeVariables(P, .Patterns) -Patterns Vs rule getFreeVariables(\forall { Vs } P, .Patterns) => getFreeVariables(P, .Patterns) -Patterns Vs + rule getFreeVariables(\mu X . P, .Patterns) + => getFreeVariables(P, .Patterns) -Patterns (X, .Patterns) + rule getFreeVariables(\nu X . P, .Patterns) + => getFreeVariables(P, .Patterns) -Patterns (X, .Patterns) + rule getFreeVariables(implicationContext(CONTEXT, P), .Patterns) => (getFreeVariables(CONTEXT, .Patterns) ++Patterns getFreeVariables(P, .Patterns)) - -Patterns #hole, .Patterns + -Patterns #hole { Heap }, #hole { Bool }, #hole { TopSort } rule getFreeVariables(\typeof(P, _)) => getFreeVariables(P) + syntax Patterns ::= filterSetVariables(Patterns) [function] + rule filterSetVariables(.Patterns) => .Patterns + rule filterSetVariables(V:Variable, Vs) => V, filterSetVariables(Vs) + rule filterSetVariables(X:SetVariable, Vs) => filterSetVariables(Vs) + // TODO: These seem specific to implication. Perhaps they need better names? syntax Patterns ::= getUniversalVariables(Pattern) [function] rule getUniversalVariables(GOAL) => getFreeVariables(GOAL, .Patterns) @@ -440,6 +486,17 @@ module KORE-HELPERS => .Patterns ``` +```k + syntax Patterns ::= getImplicationContexts(Patterns) [function] + rule getImplicationContexts(\forall {Vs} implicationContext(LCTX, RCTX), Ps) + => \forall {Vs} implicationContext(LCTX, RCTX), getImplicationContexts(Ps) + rule getImplicationContexts(S:Symbol(ARGs), Ps) + => getImplicationContexts(Ps) + rule getImplicationContexts(V:Variable, Ps) + => getImplicationContexts(Ps) + rule getImplicationContexts(.Patterns) => .Patterns +``` + Filters a list of patterns, returning the ones that are applications of the symbol: ```k @@ -542,6 +599,8 @@ terms. This is very non-standard. This is currently needed because the various unfolding strategies use this function. They should instead generate a context, where the term being unfolded has been replace by `#hole`. +TODO: These need to use alpha equivalence rather than `==K` + ```k syntax PatternOrVarName ::= Pattern | VariableName syntax Pattern ::= subst(Pattern, PatternOrVarName, Pattern) [function, klabel(subst)] @@ -551,6 +610,8 @@ where the term being unfolded has been replace by `#hole`. rule subst(X:Variable,Y:Variable,V) => X requires X =/=K Y rule subst(X:SetVariable,Y:SetVariable,V) => X requires X =/=K Y rule subst(X:Variable,P:Pattern, V) => X requires notBool(isVariable(P) orBool isVariableName(P)) + rule subst(X:SetVariable,P:Pattern, V) => X + requires notBool(isSetVariable(P)) rule subst(I:Int, X, V) => I rule subst(\top(),_,_)=> \top() rule subst(\bottom(),_,_) => \bottom() @@ -574,6 +635,10 @@ where the term being unfolded has been replace by `#hole`. requires X in E orBool X in PatternsToVariableNameSet(E) rule subst(\exists { E } C, X, V) => \exists { E } subst(C, X, V) requires notBool( X in E orBool X in PatternsToVariableNameSet(E) ) + rule subst(\mu Y . P, X, V) => \mu Y . subst(P, X, V) + requires notBool( X ==K Y orBool X ==K \mu Y . P) + rule subst(\nu Y . P, X, V) => \nu Y . subst(P, X, V) + requires notBool( X ==K Y orBool X ==K \nu Y . P) rule subst(S:Symbol, X, V) => S requires S =/=K X rule subst(S:Symbol(ARGS:Patterns) #as T:Pattern, X, V) @@ -626,6 +691,8 @@ Alpha renaming: Rename all bound variables. Free variables are left unchanged. => #fun(RENAMING => \forall { Fs[RENAMING] } alphaRename(substMap(P,RENAMING))) ( makeFreshSubstitution(Fs) ) rule alphaRename(\exists { Fs:Patterns } P:Pattern) => #fun(RENAMING => \exists { Fs[RENAMING] } alphaRename(substMap(P,RENAMING))) ( makeFreshSubstitution(Fs) ) + rule alphaRename(\mu X . P:Pattern) => \mu !X . alphaRename(subst(P, X, !X)) + rule alphaRename(\nu X . P:Pattern) => \nu !X . alphaRename(subst(P, X, !X)) rule alphaRename(\equals(L, R)) => \equals(alphaRename(L), alphaRename(R)) rule alphaRename(\not(Ps)) => \not(alphaRename(Ps)) rule alphaRename(\functionalPattern(Ps)) => \functionalPattern(alphaRename(Ps)) @@ -637,6 +704,7 @@ Alpha renaming: Rename all bound variables. Free variables are left unchanged. rule alphaRename(S:Symbol(ARGs)) => S(alphaRenamePs(ARGs)) rule alphaRename(S:Symbol) => S rule alphaRename(V:Variable) => V + rule alphaRename(X:SetVariable) => X rule alphaRename(I:Int) => I rule alphaRename(implicationContext(P, Qs)) => implicationContext(alphaRename(P), alphaRename(Qs)) @@ -652,105 +720,278 @@ Simplifications syntax Patterns ::= #not(Patterns) [function] rule #not(.Patterns) => .Patterns rule #not(P, Ps) => \not(P), #not(Ps) +``` - syntax Pattern ::= #flattenAnd(Pattern) [function] - rule #flattenAnd(\and(Ps)) => \and(#flattenAnds(Ps)) +`#flattenAssoc` flattens associative binary symbols and connectives to a +single symbol applied to multiple arguments. + +```k + syntax Pattern ::= #flattenAssoc(Pattern) [function] + rule #flattenAssoc(\and(Ps)) => \and(#flattenAnds(Ps)) + rule #flattenAssoc(\or(Ps)) => \or(#flattenOrs(Ps)) + rule #flattenAssoc(sep(Ps)) => sep(#flattenSeps(Ps)) syntax Patterns ::= #flattenAnds(Patterns) [function] + rule #flattenAnds(.Patterns) => .Patterns rule #flattenAnds(\and(Ps1), Ps2) => #flattenAnds(Ps1) ++Patterns #flattenAnds(Ps2) - rule #flattenAnds(sep(Ps1), Ps2) => sep(#flattenSeps(Ps1)) ++Patterns #flattenAnds(Ps2) + rule #flattenAnds(\or(Ps1), Ps2) => \or(#flattenOrs(Ps1)), #flattenAnds(Ps2) + rule #flattenAnds(sep(Ps1), Ps2) => sep(#flattenSeps(Ps1)), #flattenAnds(Ps2) rule #flattenAnds(P, Ps) => P, #flattenAnds(Ps) [owise] - rule #flattenAnds(.Patterns) => .Patterns syntax Patterns ::= #flattenSeps(Patterns) [function] + rule #flattenSeps(.Patterns) => .Patterns rule #flattenSeps(emp(.Patterns), Ps2) => #flattenSeps(Ps2) rule #flattenSeps(sep(Ps1), Ps2) => #flattenSeps(Ps1) ++Patterns #flattenSeps(Ps2) + rule #flattenSeps(\and(Ps1), Ps2) => \and(#flattenAnds(Ps1)), #flattenSeps(Ps2) + rule #flattenSeps(\or(Ps1), Ps2) => \or(#flattenOrs(Ps1)), #flattenSeps(Ps2) rule #flattenSeps(P, Ps) => P, #flattenSeps(Ps) [owise] - rule #flattenSeps(.Patterns) => .Patterns syntax Patterns ::= #flattenOrs(Patterns) [function] - rule #flattenOrs(\or(Ps1), Ps2) => #flattenOrs(Ps1) ++Patterns #flattenOrs(Ps2) - rule #flattenOrs(P, Ps) => P ++Patterns #flattenOrs(Ps) [owise] rule #flattenOrs(.Patterns) => .Patterns + rule #flattenOrs(\or(Ps1), Ps2) => #flattenOrs(Ps1) ++Patterns #flattenOrs(Ps2) + rule #flattenOrs(\and(Ps1), Ps2) => \and(#flattenAnds(Ps1)), #flattenOrs(Ps2) + rule #flattenOrs(sep(Ps1), Ps2) => sep(#flattenSeps(Ps1)), #flattenOrs(Ps2) + rule #flattenOrs(P, Ps) => P, #flattenAnds(Ps) [owise] +``` + +`#nnf` converts a formula into Negation Normal Form: + +```k + syntax Patterns ::= #nnfPs(Patterns) [function] + rule #nnfPs(.Patterns) => .Patterns + rule #nnfPs(P, Ps) => #nnf(P), #nnfPs(Ps) + + syntax Pattern ::= #nnf(Pattern) [function] + rule #nnf(P) => P requires isDnfAtom(P) + rule #nnf(S:Symbol(Args)) => S(#nnfPs(Args)) + rule #nnf( \or(Ps)) => \or(#nnfPs(Ps)) + rule #nnf(\and(Ps)) => \and(#nnfPs(Ps)) + rule #nnf(\implies(L, R)) => #nnf(\or(\not(L), R)) + rule #nnf(\exists { .Patterns } P) => #nnf(P) + + rule #nnf(\not(P)) => \not(P) requires isDnfAtom(P) + rule #nnf(\not(S:Symbol(Args))) => \not(S(#nnfPs(Args))) + rule #nnf(\not( \or(Ps))) => \and(#nnfPs(#not(Ps))) + rule #nnf(\not(\and(Ps))) => \or(#nnfPs(#not(Ps))) + rule #nnf(\not(\not(P))) => #nnf(P) + rule #nnf(\not(\implies(L, R))) => #nnf(\not(\or(\not(L), R))) + rule #nnf(\not(\exists { .Patterns } P)) => #nnf(\not(P)) + + syntax Bool ::= isDnfAtom(Pattern) [function] + rule isDnfAtom(V:Variable) => true + rule isDnfAtom(X:SetVariable) => true + rule isDnfAtom(S:Symbol) => true + rule isDnfAtom(\equals(L, R)) => true + rule isDnfAtom(\exists{Vs}_) => true requires Vs =/=K .Patterns + rule isDnfAtom(\forall{Vs}_) => true + rule isDnfAtom(\mu X . _) => true + rule isDnfAtom(\nu X . _) => true + rule isDnfAtom(implicationContext(_, _)) => true + rule isDnfAtom(\and(_)) => false + rule isDnfAtom(\or(_)) => false + rule isDnfAtom(\implies(_, _)) => false + rule isDnfAtom(S:Symbol(ARGS)) => false + rule isDnfAtom(\not(P)) => false +``` - // TODO: dnf should be greatly refactored. Normalization along with lift-constraints - // should happen likely in the same function, with much fewer ad-hoc rules than we - // have below +```k syntax Pattern ::= #dnf(Pattern) [function] - rule #dnf(\or(Ps)) => \or(#dnfPs(Ps)) + rule #dnf(P) => #flattenAssoc(#liftOr(#liftAnd(#nnf(\or(\and(P)))))) +``` - syntax Patterns ::= #dnfPs(Patterns) [function] +```k + syntax Pattern ::= #liftOr(Pattern) [function] + rule #liftOr(P) => \or(P) requires isDnfAtom(P) + rule #liftOr(\not(P)) => \or(\not(P)) + rule #liftOr(S:Symbol(Args)) + => \or(removeDuplicates(#liftOr_distribute( context: S(.Patterns) + , processed: .Patterns + , remaining: Args + ) ) ) + rule #liftOr(\and(Args)) + => \or(removeDuplicates(#liftOr_distribute( context: \and(.Patterns) + , processed: .Patterns + , remaining: Args + ) ) ) + rule #liftOr(\or(Args)) => \or(removeDuplicates(#liftOrPs(Args))) + + syntax Patterns ::= #liftOrPs(Patterns) [function] + rule #liftOrPs(.Patterns) => .Patterns + rule #liftOrPs(P, Ps) => #liftOr(P), #liftOrPs(Ps) + + syntax Patterns ::= "#liftOr_distribute" "(" "context:" Pattern + "," "processed:" Patterns + "," "remaining:" Patterns + ")" [function] + rule #liftOr_distribute( context: Context + , processed: Processed + , remaining: P, Ps + ) + => #liftOr_distribute( context: Context + , processed: Processed + , or: #flattenAssoc(#liftOr(P)) + , remaining: Ps + ) + rule #liftOr_distribute(context: S:Symbol(.Patterns), processed: Processed, remaining: .Patterns) => S(Processed), .Patterns + rule #liftOr_distribute(context: \and(.Patterns), processed: Processed, remaining: .Patterns) => \and(Processed), .Patterns + + syntax Patterns ::= "#liftOr_distribute" "(" "context:" Pattern + "," "processed:" Patterns + "," "or:" Pattern + "," "remaining:" Patterns + ")" [function] + rule #liftOr_distribute( context: Context + , processed: Processed + , or: \or(Or, Ors) + , remaining: Remaining + ) + => #liftOr_distribute( context: Context + , processed: Processed ++Patterns Or + , remaining: Remaining + ) ++Patterns + #liftOr_distribute( context: Context + , processed: Processed + , or: \or(Ors) + , remaining: Remaining + ) + rule #liftOr_distribute( context: Context + , processed: Processed + , or: \or(.Patterns) + , remaining: Remaining + ) + => .Patterns +``` - rule #dnfPs(.Patterns) => .Patterns - rule #dnfPs(\or(Ps), REST) => #dnfPs(Ps ++Patterns REST) - rule #dnfPs(P, Ps) => \and(P), #dnfPs(Ps) - requires isBasePattern(P) - rule #dnfPs(\not(P), Ps) => \and(\not(P)), #dnfPs(Ps) - requires isBasePattern(P) - rule #dnfPs(\exists{Vs} P, Ps) => #exists(#dnfPs(P, .Patterns), Vs) ++Patterns #dnfPs(Ps) +```k + syntax Pattern ::= #liftAnd(Pattern) [function] + rule #liftAnd(P) => \and(P) requires isDnfAtom(P) + rule #liftAnd(\not(P)) => \and(\not(P)) + rule #liftAnd(S:Symbol(Args)) + => \and(removeDuplicates(#liftAnd_distribute( context: S(.Patterns) + , processed: .Patterns + , predicates: .Patterns + , remaining: Args + ) ) ) + rule #liftAnd(\or(Args)) + => \and(removeDuplicates(#liftAnd_distribute( context: \or(.Patterns) + , processed: .Patterns + , predicates: .Patterns + , remaining: Args + ) ) ) + rule #liftAnd(\and(Args)) => \and(removeDuplicates(#liftAndPs(Args))) + + syntax Patterns ::= #liftAndPs(Patterns) [function] + rule #liftAndPs(.Patterns) => .Patterns + rule #liftAndPs(P, Ps) => #liftAnd(P), #liftAndPs(Ps) + + syntax Patterns ::= "#liftAnd_distribute" "(" "context:" Pattern + "," "processed:" Patterns + "," "predicates:" Patterns + "," "remaining:" Patterns + ")" [function] + rule #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , remaining: P, Ps + ) + => #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , and: #flattenAssoc(#liftAnd(P)) + , remaining: Ps + ) + requires #flattenAssoc(#liftAnd(P)) =/=K \and(.Patterns) + + rule #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , remaining: P, Ps + ) + => #liftAnd_distribute( context: Context + , processed: Processed ++Patterns \and(.Patterns) + , predicates: Preds + , remaining: Ps + ) + requires #flattenAssoc(#liftAnd(P)) ==K \and(.Patterns) + + rule #liftAnd_distribute( context: S:Symbol(.Patterns) + , processed: Processed + , predicates: Preds + , remaining: .Patterns + ) + => S(Processed), removeDuplicates(Preds) + rule #liftAnd_distribute( context: \or(.Patterns) + , processed: Processed + , predicates: Preds + , remaining: .Patterns + ) + => \or(Processed ++Patterns Preds), .Patterns + + syntax Patterns ::= "#liftAnd_distribute" "(" "context:" Pattern + "," "processed:" Patterns + "," "predicates:" Patterns + "," "and:" Pattern + "," "remaining:" Patterns + ")" [function] + rule #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , and: \and(And, Ands) + , remaining: Remaining + ) + => #liftAnd_distribute( context: Context + , processed: Processed ++Patterns And + , predicates: Preds + , remaining: Remaining + ) ++Patterns + #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , and: \and(Ands) + , remaining: Remaining + ) + requires notBool isPredicatePattern(And) + rule #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , and: \and(And, Ands) + , remaining: Remaining + ) + => #liftAnd_distribute( context: Context + , processed: Processed ++Patterns \and(.Patterns) + , predicates: Preds ++Patterns And + , remaining: Remaining + ) ++Patterns + #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , and: \and(Ands) + , remaining: Remaining + ) + requires isPredicatePattern(And) + rule #liftAnd_distribute( context: Context + , processed: Processed + , predicates: Preds + , and: \and(.Patterns) + , remaining: Remaining + ) + => .Patterns +``` + +```k +// TODO: These aren't sound +// rule #dnfPs(\exists{Vs} P, Ps) => #exists(#dnfPs(P, .Patterns), Vs) ++Patterns #dnfPs(Ps) +// rule #dnfPs(\forall{Vs} P, Ps) => #forall(#dnfPs(P, .Patterns), Vs) ++Patterns #dnfPs(Ps) syntax Patterns ::= #exists(Patterns, Patterns) [function] rule #exists(.Patterns, _) => .Patterns rule #exists((\and(Ps1), Ps2), Vs) => \exists{removeDuplicates(Vs intersect getFreeVariables(Ps1))} \and(Ps1), #exists(Ps2, Vs) rule #exists((\exists{Es} P, Ps2), Vs) => \exists{removeDuplicates(Es ++Patterns (Vs intersect getFreeVariables(P)))} P, #exists(Ps2, Vs) - - rule #dnfPs(\not(\and(Ps)), REST) => #dnfPs(#not(Ps)) ++Patterns #dnfPs(REST) - rule #dnfPs(\not(\or(Ps)), REST) => #dnfPs(\and(#not(Ps)), REST) - - // Distribute \or over \and - rule #dnfPs(\and(\or(P, Ps1), Ps2), REST) - => #dnfPs(\and(P, Ps2)) ++Patterns #dnfPs(\and(\or(Ps1), Ps2)) - rule #dnfPs(\and(\or(.Patterns), Ps2), REST) => #dnfPs(REST) - - // \and is assoc - rule #dnfPs(\and(\and(Ps1), Ps2), REST) => #dnfPs(\and(Ps1 ++Patterns Ps2), REST) - - rule #dnfPs(\and(Ps), REST) => \and(Ps), #dnfPs(REST) - requires isBaseConjunction(Ps) - rule #dnfPs(\and(P, Ps), REST) => #dnfPs(\and(Ps ++Patterns P), REST) - requires notBool isBaseConjunction(P, Ps) andBool notBool isConjunction(P) andBool isBasePattern(P) - rule #dnfPs(\and(sep(Ps1), Ps2), REST) => #dnfPs(\and(\or(#dnfPs(sep(Ps1), .Patterns)), Ps2), REST) - requires notBool isBaseConjunction(Ps1) - - // sep is assoc - rule #dnfPs(sep(sep(Ps1), Ps2), REST) => #dnfPs(sep(Ps1 ++Patterns Ps2), REST) - - // sep is commutative - rule #dnfPs(sep(P, Ps), REST) => #dnfPs(sep(Ps ++Patterns P), REST) - requires notBool isBaseConjunction(P, Ps) andBool notBool isConjunction(P) andBool isBasePattern(P) - - // borrowing code from lift-constraints - rule #dnfPs(sep(\and(P, Ps1), Ps2), REST) => #dnfPs(\and(sep(\and(Ps1), Ps2), P)) - requires isPredicatePattern(P) - rule #dnfPs(sep(\and(P, Ps1), Ps2), REST) => #dnfPs(sep(\and(Ps1), P, Ps2)) - requires isSpatialPattern(P) - rule #dnfPs(sep(\and(.Patterns), Ps), REST) => #dnfPs(sep(Ps), REST) - - syntax Patterns ::= #dnfPsNew(Patterns) [function] - - // Distribute \or over sep - rule #dnfPs(sep(\or(P, Ps1), Ps2), REST) - => #dnfPs(sep(P, Ps2)) ++Patterns #dnfPs(sep(\or(Ps1), Ps2)) - rule #dnfPs(sep(\or(.Patterns), Ps2), REST) => #dnfPs(REST) - - syntax Bool ::= isBasePattern(Pattern) [function] - rule isBasePattern(S:Symbol(ARGS)) => true - [owise] - rule isBasePattern(\equals(L, R)) => true - rule isBasePattern(\and(_)) => false - rule isBasePattern(\or(_)) => false - rule isBasePattern(\exists{Vs}_) => false - rule isBasePattern(\not(P)) => isBasePattern(P) - rule isBasePattern(sep(ARGS)) => isBaseConjunction(ARGS) - - syntax Bool ::= isBaseConjunction(Patterns) [function] - rule isBaseConjunction(.Patterns) => true - rule isBaseConjunction(\and(P), Ps) => false - rule isBaseConjunction(P, Ps) => isBasePattern(P) andBool isBaseConjunction(Ps) [owise] - - syntax Bool ::= isConjunction(Pattern) [function] - rule isConjunction(\and(P)) => true - rule isConjunction(_) => false [owise] + + syntax Patterns ::= #forall(Patterns, Patterns) [function] + rule #forall(.Patterns, _) => .Patterns + rule #forall((\and(Ps1), Ps2), Vs) => \forall{removeDuplicates(Vs intersect getFreeVariables(Ps1))} \and(Ps1), #forall(Ps2, Vs) + rule #forall((\forall{Es} P, Ps2), Vs) => \forall{removeDuplicates(Es ++Patterns (Vs intersect getFreeVariables(P)))} P, #forall(Ps2, Vs) ``` ```k @@ -763,17 +1004,23 @@ Simplifications rule isPredicatePattern(\or(.Patterns)) => true rule isPredicatePattern(\or(P, Ps)) => isPredicatePattern(P) andBool isPredicatePattern(\or(Ps)) rule isPredicatePattern(\implies(P1, P2)) => isPredicatePattern(P1) andBool isPredicatePattern(P2) - rule isPredicatePattern(#hole) => false + rule isPredicatePattern(#hole { Bool }) => true + rule isPredicatePattern(V:VariableName { Bool }) => true + rule isPredicatePattern(V:VariableName { SORT }) => false + requires SORT =/=K Bool + rule isPredicatePattern(V:SetVariable) => false // TODO: This should use an axiom, similar to `functional` instead: `axiom predicate(P)` rule isPredicatePattern(S:Symbol(ARGS)) => true requires getReturnSort(S(ARGS)) ==K Bool rule isPredicatePattern(S:Symbol(ARGS)) => false - requires getReturnSort(S(ARGS)) ==K Heap + requires getReturnSort(S(ARGS)) =/=K Bool rule isPredicatePattern(emp(.Patterns)) => false rule isPredicatePattern(\exists{Vs} P) => isPredicatePattern(P) rule isPredicatePattern(\forall{Vs} P) => isPredicatePattern(P) + rule isPredicatePattern(\mu X . P) => false + rule isPredicatePattern(\nu X . P) => false rule isPredicatePattern(implicationContext(\and(sep(_),_),_)) => false rule isPredicatePattern(\typeof(_,_)) => true rule isPredicatePattern(implicationContext(_,_)) => true @@ -790,7 +1037,13 @@ Simplifications rule isSpatialPattern(\or(_)) => false rule isSpatialPattern(S:Symbol(ARGS)) => true requires S =/=K sep andBool getReturnSort(S(ARGS)) ==K Heap - rule isSpatialPattern(#hole) => true + rule isSpatialPattern(S:Symbol(ARGS)) => false + requires getReturnSort(S(ARGS)) =/=K Heap + rule isSpatialPattern(#hole { Bool }) => false + rule isSpatialPattern(#hole { Heap }) => true + rule isSpatialPattern(V:VariableName { Heap }) => true + rule isSpatialPattern(V:SetVariable) => false + rule isSpatialPattern(\mu X . P) => false // TODO: Perhaps normalization should get rid of this? rule isSpatialPattern(\exists{_} implicationContext(\and(sep(_),_),_)) => true @@ -800,6 +1053,19 @@ Simplifications rule isSpatialPattern(\forall{_} implicationContext(_,_)) => false [owise] + syntax Patterns ::= getSpatialPatterns(Patterns) [function] + rule getSpatialPatterns(.Patterns) => .Patterns + rule getSpatialPatterns(P, Ps) => P, getSpatialPatterns(Ps) + requires isSpatialPattern(P) + rule getSpatialPatterns(P, Ps) => getSpatialPatterns(Ps) + requires notBool isSpatialPattern(P) + + syntax Patterns ::= getPredicatePatterns(Patterns) [function] + rule getPredicatePatterns(.Patterns) => .Patterns + rule getPredicatePatterns(P, Ps) => P, getPredicatePatterns(Ps) + requires isPredicatePattern(P) + rule getPredicatePatterns(P, Ps) => getPredicatePatterns(Ps) + requires notBool isPredicatePattern(P) ``` ```k @@ -820,6 +1086,7 @@ Simplifications syntax Bool ::= hasImplicationContext(Pattern) [function] syntax Bool ::= hasImplicationContextPs(Patterns) [function] rule hasImplicationContext(X:Variable) => false + rule hasImplicationContext(X:SetVariable) => false rule hasImplicationContext(X:Int) => false rule hasImplicationContext(S:Symbol) => false rule hasImplicationContext(\implies(LHS, RHS)) @@ -833,6 +1100,7 @@ Simplifications rule hasImplicationContext(\functionalPattern(P)) => hasImplicationContext(P) rule hasImplicationContext(\exists{ _ } P ) => hasImplicationContext(P) rule hasImplicationContext(\forall{ _ } P ) => hasImplicationContext(P) + rule hasImplicationContext(\mu X . P) => hasImplicationContext(P) rule hasImplicationContext(implicationContext(_, _)) => true rule hasImplicationContextPs(.Patterns) => false rule hasImplicationContextPs(P, Ps) @@ -1034,6 +1302,12 @@ assume a pattern of the form: => StringToSymbol( getFreshNameNonum(Base, collectSymbolsS(GId))) + syntax Patterns ::= filterVariablesBySort(Patterns, Sort) [function] + rule filterVariablesBySort(.Patterns, _) => .Patterns + rule filterVariablesBySort(((_ { S } #as V), Vs), S) + => V, filterVariablesBySort(Vs, S) + rule filterVariablesBySort((V, Vs), S) + => filterVariablesBySort(Vs, S) [owise] ``` ```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/lib/render-proof-tree b/prover/lib/render-proof-tree new file mode 100755 index 000000000..df0b9e683 --- /dev/null +++ b/prover/lib/render-proof-tree @@ -0,0 +1,96 @@ +#!/usr/bin/env python3 + +usage = \ +"""Prints the proof tree and either the active goal, or the specified goal. + +Usage: + + lib/render-proof-tree [goal_id] +""" + +import sys +import os +sys.path.append(os.path.join(os.path.dirname(__file__), '../ext/k/k-distribution/target/release/k/lib/')) +import pyk + +from anytree import NodeMixin, Node, RenderTree +from collections import namedtuple +import textwrap +import fileinput +import re + + +# Parse args +# ---------- + +if len(sys.argv) < 2 or len(sys.argv) > 3: print(usage); exit(1) +input_file = sys.argv[1] +selected_id = None +if len(sys.argv) == 3: selected_id = sys.argv[2] + +class Goal(NodeMixin): + def __init__(self, id, parent_id, active): + self.id = id + self.name = id + self.parent_id = parent_id + self.active = active + self.claim = None + self.trace = None + self.strategy = None + +# Parse K output +# -------------- + +nodes = {} +roots = [] +next_line_is_claim = False +next_line_is_trace = False +next_line_is_strategy = False + +with open(input_file) as f: + for line in f: + match = re.search(' *id: (\w*\d*), parent: (\.|\w*\d*)', line) + if match is not None: + active = nodes == {} + id = match.group(1) + parent = match.group(2) + node = Goal(id, parent, active) + nodes[id] = node + if parent == '.': roots += [node] + if next_line_is_claim: node.claim = line.strip(); next_line_is_claim = False + next_line_is_claim = re.search('', line) is not None + if next_line_is_trace: node.trace = line.strip(); next_line_is_trace = False + next_line_is_trace = re.search('', line) is not None + if next_line_is_strategy: node.strategy = line.strip(); next_line_is_strategy = False + next_line_is_strategy = re.search('', line) is not None + +# Build proof tree +# ---------------- + +for id, node in nodes.items(): + if node in roots: continue + node.parent = nodes[node.parent_id] + +# Print proof tree +# ---------------- + +def is_node_selected(node): + if selected_id is None: return node.active + return node.id == selected_id + +term_normal ='\033[0m' +term_bold ='\033[1m' +term_reverse ='\033[7m' +for pre, fill, node in RenderTree(roots[0]): + if is_node_selected(node): + pre += term_reverse + print( pre, 'id: ', node.id, ',' + , 'trace:', node.trace.split('(')[0] + , term_normal + ) + +for pre, fill, node in RenderTree(roots[0]): + if is_node_selected(node): + print('id:', node.id) + print('claim:', node.claim) + print('strategy:', node.strategy) diff --git a/prover/lib/testlists.py b/prover/lib/testlists.py index 6546a6d02..dc72339b6 100644 --- a/prover/lib/testlists.py +++ b/prover/lib/testlists.py @@ -61,6 +61,187 @@ def read_list(file): ) . """.replace('\n',' ') +dll_vc07_strategy = """ + normalize . or-split-rhs + . lift-constraints . instantiate-existentials + . substitute-equals-for-equals + . nullity-analysis + ( abstract-nil + . kt + . ( ( left-unfold-Nth(0) + . normalize . or-split-rhs + . lift-constraints . instantiate-existentials + . instantiate-separation-logic-axioms + . substitute-equals-for-equals + . check-lhs-constraint-unsat + . lift-constraints + . match + . spatial-patterns-equal + . spatial-patterns-match + . smt-cvc4 + ) + | ( search-sl(kt-bound: 1, unfold-bound: 0) ) + ) + ) . +""".replace('\n',' ') + +dll_vc17_strategy = """ + normalize . or-split-rhs + . lift-constraints . instantiate-existentials . substitute-equals-for-equals + . abstract-Nth(0) + . normalize . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . kt + . ( ( right-unfold-Nth(0,1) . right-unfold-Nth(0,1) . right-unfold-Nth(0,0) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . instantiate-separation-logic-axioms + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( kt + . ( ( normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . instantiate-separation-logic-axioms + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . check-lhs-constraint-unsat + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . right-unfold-Nth(0,1) . right-unfold-Nth(0,1) + . right-unfold-Nth(0,1) . right-unfold-Nth(0,0) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . ( left-unfold-Nth(0) | left-unfold-Nth(1) ) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . instantiate-separation-logic-axioms + . check-lhs-constraint-unsat + ) + ) + ) + ) . +""".replace('\n',' ') + +nll_vc03_strategy = """ + normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . right-unfold-Nth(0,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto + . right-unfold-Nth(1,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto + . right-unfold-Nth(1,0) . right-unfold-Nth(0,1) + . right-unfold-Nth(0,1) . right-unfold-Nth(0,0) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto . frame + . right-unfold-Nth(0,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto . +""".replace('\n', ' ') + +nll_vc04_strategy = """ + normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . right-unfold-Nth(0,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto + . right-unfold-Nth(0,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto + . right-unfold-Nth(0,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto + . frame + . right-unfold-Nth(0,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto + . right-unfold-Nth(0,0) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals . +""".replace('\n', ' ') + +nll_vc08_10_strategy = """ + normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . kt + . ( ( right-unfold-Nth(0,1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match-pto + . frame + . search-sl(kt-bound: 2, unfold-bound: 3) + ) + | search-sl(kt-bound: 1, unfold-bound: 0) + ) . +""".replace('\n', ' ') + +lsegex4_slk_1_strategy = """ + normalize . or-split-rhs + . lift-constraints . instantiate-existentials . substitute-equals-for-equals + . left-unfold-Nth(0) + . ( ( normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . check-lhs-constraint-unsat . fail + ) + | ( normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . right-unfold-Nth(0,0) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . remove-constraints + . search-sl(kt-bound: 2, unfold-bound: 2) + ) + ) . +""".replace('\n', ' ') + +skl3_vc10_strategy = """ + normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . kt + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . ( ( right-unfold-Nth(0, 1) + . right-unfold-Nth(0, 1) . right-unfold-Nth(0, 1) . right-unfold-Nth(0, 0) + . right-unfold-Nth(0, 1) + . right-unfold-Nth(0, 1) . right-unfold-Nth(0, 0) + . right-unfold-Nth(0, 0) + . right-unfold-Nth(0, 0) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . instantiate-separation-logic-axioms + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 ) + | ( right-unfold-Nth(0, 1) + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . instantiate-separation-logic-axioms + . normalize . or-split-rhs . lift-constraints + . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + ) . +""".replace('\n', ' ') + # prefix KT RU timeout tests test_lists = [ ('unfold-mut-recs . ', 3, 3, '5m', read_list('t/test-lists/passing-3-3-5')) , ('unfold-mut-recs . ', 5, 12, '40m', read_list('t/test-lists/passing-5-12-40')) @@ -167,6 +348,19 @@ def read_list(file): " ) ." ), 2, 6, '10m', ['t/SL-COMP18/bench/qf_shid_entl/odd-lseg3_slk-5.smt2']) , (tst_22_strategy, 0, 0, '10m', ['t/SL-COMP18/bench/qf_shid_entl/22.tst.smt2']) + , ('footprint-analysis . ', + 2, 1, '10m', ['t/SL-COMP18/bench/qf_shid_entl/dll-vc05.smt2']) + , (dll_vc07_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/dll-vc07.smt2']) + , ('footprint-analysis . abstract-nil . ', + 2, 1, '10m', ['t/SL-COMP18/bench/qf_shid_entl/dll-vc11.smt2']) + , (dll_vc17_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/dll-vc17.smt2']) + , (nll_vc03_strategy, 2, 3, '10m', ['t/SL-COMP18/bench/qf_shid_entl/nll-vc03.smt2']) + , (nll_vc04_strategy, 2, 6, '10m', ['t/SL-COMP18/bench/qf_shid_entl/nll-vc04.smt2']) + , (nll_vc08_10_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/nll-vc08.smt2']) + , (nll_vc08_10_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/nll-vc10.smt2']) + , ('', 3, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/tseg_join_tree_entail_tseg.sb.smt2']) + , (lsegex4_slk_1_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/lsegex4_slk-1.smt2']) + , (skl3_vc10_strategy, 2, 2, '10m', ['t/SL-COMP18/bench/qf_shid_entl/skl3-vc10.smt2']) ] qf_shid_entl_unsat_tests = read_list('t/test-lists/qf_shid_entl.unsat') diff --git a/prover/prover.md b/prover/prover.md index 2ddc9ad15..a88ecea0a 100644 --- a/prover/prover.md +++ b/prover/prover.md @@ -40,11 +40,13 @@ module STRATEGIES-EXPORTED-SYNTAX | "reflexivity" | "alternate-search-sl" "(" "kt-bound" ":" Int "," "unfold-bound" ":" Int ")" | "kt-unfold-search-sl" "(" "kt-bound" ":" Int "," "unfold-bound" ":" Int ")" - | "remove-lhs-existential" | "normalize" | "lift-or" | "purify" | "abstract" - | "simplify" | "instantiate-existentials" | "substitute-equals-for-equals" + | "remove-lhs-existential" | "normalize" | "lift-or" + | "purify" | "abstract" | "abstract-Nth" "(" Int ")" | "abstract-nil" + | "simplify" | "substitute-equals-for-equals" + | "instantiate-existentials" | "instantiate-existentials-implication-context" | "lift-constraints" | "direct-proof" - | "check-lhs-constraint-unsat" + | "check-lhs-constraint-unsat" | "check-lhs-constraint-unsat-debug" | "smt" | "smt-z3" | "smt-cvc4" | "smt-debug" | "left-unfold" | "left-unfold-Nth" "(" Int ")" | "right-unfold" | "right-unfold-Nth" "(" Int "," Int ")" | "right-unfold" "(" Symbol ")" @@ -54,13 +56,16 @@ module STRATEGIES-EXPORTED-SYNTAX | "right-unfold" "(" "symbols" ":" Patterns "," "bound" ":" Int ")" | "kt" | "kt" "#" KTFilter | "kt-unf" | "kt-unf" "#" KTFilter - | "kt-gfp" | "kt-gfp" "#" KTFilter + | "gfp" | "kt-solve-implications" "(" Strategy ")" | "instantiate-universals-with-ground-terms" - | "instantiate-separation-logic-axioms" - | "spatial-patterns-equal" - | "match" | "match-pto" + | "instantiate-separation-logic-axioms" | "pto-is-injective" + | "spatial-patterns-equal" | "patterns-equal" + | "spatial-patterns-match" + | "match" | "match-debug" | "match-pto" | "frame" + | "footprint-analysis" | "nullity-analysis" "(" Strategy ")" + | "remove-constraints" | "unfold-mut-recs" | "apply-equation" RewriteDirection AxiomOrClaimName diff --git a/prover/strategies/apply-equation.md b/prover/strategies/apply-equation.md index 5555f3b86..f310adb4a 100644 --- a/prover/strategies/apply-equation.md +++ b/prover/strategies/apply-equation.md @@ -25,18 +25,18 @@ module STRATEGY-APPLY-EQUATION 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 +57,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 +77,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 +105,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 +120,8 @@ module STRATEGY-APPLY-EQUATION , by: Ss ) ... - - T + + T syntax KItem ::= "#apply-equation3" "(" "hypothesis:" Pattern @@ -130,7 +130,7 @@ module STRATEGY-APPLY-EQUATION "," "by:" Strategies ")" - rule + rule #apply-equation3 ( hypothesis: P , heatResult: heatResult(Heated, Subst) @@ -139,10 +139,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 +150,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 +180,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 +192,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..6272c580d 100644 --- a/prover/strategies/apply.md +++ b/prover/strategies/apply.md @@ -21,11 +21,11 @@ module STRATEGY-APPLY 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 +36,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..5044daa06 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -25,7 +25,8 @@ module PROVER-CORE-SYNTAX | TerminalStrategy | Strategy "&" Strategy [right, format(%1%n%2 %3)] | Strategy "|" Strategy [right, format(%1%n%2 %3)] - syntax Strategy ::= "or-split" | "and-split" | "or-split-rhs" + syntax Strategy ::= "or-split" | "and-split" | "or-split-rhs" | "and-split-rhs" + syntax Strategy ::= "rhs-top" | "contradiction" syntax Strategy ::= "prune" "(" Patterns ")" syntax Strategy ::= Strategy "{" Int "}" @@ -54,7 +55,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 +64,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 +92,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 +108,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 + rule ( .Bag => - ID:Int + ID PARENT - SUBSTRAT - SUBGOAL + SUBSTRAT + SUBGOAL LC TRACE ... @@ -124,13 +125,13 @@ 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 ... ... - + ``` Sometimes, we may need to combine the proofs of two subgoals to construct a proof @@ -138,19 +139,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 +165,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 +189,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 +199,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 +212,11 @@ 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) ... + rule GOALS + or-split => noop ... + requires notBool isDisjunction(GOALS) syntax Strategy ::= "#orSplit" "(" Patterns ")" [function] rule #orSplit(.Patterns) => fail @@ -229,17 +233,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,15 +260,55 @@ 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 + rule #andSplit(.Patterns) => success rule #andSplit(P:Pattern, .Patterns) => replace-goal(P) rule #andSplit(P:Pattern, Ps) => replace-goal(P) & #andSplit(Ps) [owise] ``` +`and-split-rhs`: conjunctions on the RHS, singular implication: + +``` + \implies(LHS, \exists{Vs} GOAL-1) ... \implies(LHS, \exists{Vs} GOAL-N) + ----------------------------------------------------------------------------- + \implies(LHS, \exists{Vs} \and(GOAL-1, ..., GOAL-N)) +``` + +```k + rule \implies(LHS, \exists{Vs} \and(GOALS)) + and-split-rhs => #andSplitImplication(LHS, Vs, GOALS) ... + + syntax Strategy ::= "#andSplitImplication" "(" Pattern "," Patterns "," Patterns ")" [function] + rule #andSplitImplication(P, Vs, .Patterns) => noop + rule #andSplitImplication(P1, Vs, (P2, .Patterns)) => replace-goal(\implies(P1, \exists{Vs} \and(P2, .Patterns))) + rule #andSplitImplication(P1, Vs, (P2, Ps)) => replace-goal(\implies(P1, \exists{Vs} \and(P2, .Patterns))) & #andSplitImplication(P1, Vs, Ps) [owise] +``` + +`rhs-top` evaluates to success if the right hand side is top + +```k + rule \implies(LHS, \exists{.Patterns} \and(.Patterns)) + rhs-top => success ... + rule \implies(LHS, \exists{.Patterns} P) + rhs-top => fail ... + requires P =/=K \and(.Patterns) +``` + +`contradiction` evaluates to success if the LHS includes both a clause and its negation. +TODO: This currently only checks the first two clauses + +```k + rule \implies(\and(P, REST), RHS) + contradiction => success ... + requires \not(P) in REST + rule \implies(\and(P, REST), RHS) + contradiction => fail ... + requires notBool(\not(P) in REST) +``` + If-then-else-fi strategy is useful for implementing other strategies: ```k @@ -278,10 +322,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..fa14b1871 100644 --- a/prover/strategies/duplicate.md +++ b/prover/strategies/duplicate.md @@ -15,14 +15,14 @@ module STRATEGY-DUPLICATE 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..0db317d0c 100644 --- a/prover/strategies/knaster-tarski.md +++ b/prover/strategies/knaster-tarski.md @@ -19,6 +19,8 @@ for guessing an instantiation of the inductive hypothesis. rule getKTUnfoldables(R(ARGS), REST) => R(ARGS), getKTUnfoldables(REST) requires isUnfoldable(R) + rule getKTUnfoldables(\mu X . Phi, REST) + => \mu X . Phi, getKTUnfoldables(REST) rule getKTUnfoldables(S:Symbol, REST) => getKTUnfoldables(REST) requires notBool isUnfoldable(S) @@ -34,6 +36,8 @@ for guessing an instantiation of the inductive hypothesis. => getKTUnfoldables(REST) rule getKTUnfoldables(\and(Ps), REST) => getKTUnfoldables(Ps) ++Patterns getKTUnfoldables(REST) + rule getKTUnfoldables(\or(Ps), REST) + => getKTUnfoldables(Ps) ++Patterns getKTUnfoldables(REST) rule getKTUnfoldables(sep(Ps), REST) => getKTUnfoldables(Ps) ++Patterns getKTUnfoldables(REST) rule getKTUnfoldables(\implies(LHS, RHS), REST) @@ -49,84 +53,100 @@ 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)) - => ( remove-lhs-existential . normalize . or-split-rhs . lift-constraints - . kt-wrap(LRP) . kt-forall-intro - . kt-unfold . lift-or . and-split . remove-lhs-existential + rule ktForEachLRP(.Patterns) => fail ... + rule ( ktForEachLRP((LRP, LRPs)) + => ( kt-wrap(LRP) . kt-forall-intro + . kt-unfold . remove-lhs-existential . kt-unwrap - . simplify . normalize . or-split-rhs. lift-constraints. kt-collapse + . simplify . normalize . or-split-rhs + . ( with-each-implication-context( simplify . normalize . or-split-rhs + . remove-lhs-existential + . normalize-implication-context + . kt-collapse + ) + ) ) | 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 + . kt-unfold . remove-lhs-existential . kt-unwrap . simplify . normalize . or-split-rhs. lift-constraints - . ( ( kt-collapse ) - | ( imp-ctx-unfold . kt-collapse ) + . ( with-each-implication-context( ( normalize-implication-context + . kt-collapse + . remove-lhs-existential + . lift-constraints + ) + | ( normalize-implication-context + . imp-ctx-unfold + . instantiate-existentials-implication-context + . kt-collapse + . remove-lhs-existential + . lift-constraints + ) + ) ) ) | ktUnfForEachLRP(LRPs) ) ~> REST - + ``` > phi(x) -> C'[psi(x)] @@ -135,33 +155,15 @@ for guessing an instantiation of the inductive hypothesis. > > where `C'[psi(x)] ≡ \exists #hole . #hole /\ ⌊C[#hole] -> psi(x)⌋` -## kt-wrap (FOL) +## kt-wrap ```k syntax Strategy ::= "kt-wrap" "(" Pattern ")" - 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 - andBool isPredicatePattern(\and(LHS)) -``` - -## kt-wrap (SL) - -```k - 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 - andBool isSpatialPattern(sep(LSPATIAL)) + rule \implies(LHS, RHS) + => \implies(LRP, implicationContext(subst(LHS, LRP, #hole { getReturnSort(LRP) } ), RHS)) + + kt-wrap(LRP) => noop ... + requires #hole { getReturnSort(LRP) } in getFreeVariables(subst(LHS, LRP, #hole { getReturnSort(LRP) })) ``` > phi(x) -> \forall y. psi(x, y) @@ -170,13 +172,15 @@ 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) } + , \forall { filterSetVariables(getUniversalVariables(GOAL)) + -Patterns getFreeVariables(LHS, .Patterns) + } RHS ) - - kt-forall-intro => noop ... + + kt-forall-intro => noop ... ``` > phi(x) -> psi(x, y) @@ -185,30 +189,72 @@ 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) ``` +## `kt-unfold` -// unfold+lfp +### `kt-unfold` for `\mu` ```k - syntax Strategy ::= "kt-unfold" - rule \implies( LRP(ARGS) #as LHS - => substituteBRPs(unfold(LHS), LRP, ARGS, RHS) - , RHS - ) + // TODO: combine with other kt-unfold rules + rule \implies(\mu X . P, RHS) + => \implies(subst(P, X, alphaRename(RHS)), RHS) + + kt-unfold + => lift-or . and-split + ... + +``` + +### `kt-unfold` for `\iff-lfp` + +```k + syntax Strategy ::= "kt-unfold" | "kt-unfold" "(" Pattern ")" + rule \implies(LRP:Symbol(ARGS) #as LHS, RHS) + kt-unfold => kt-unfold(unfold(LHS)) ... + requires isUnfoldable(LRP) + rule \implies(LRP(ARGS) #as LHS, RHS) + => \implies(UNFOLDED_LHS, RHS) + + kt-unfold(UNFOLDED_LHS) + => lift-or . and-split + . kt-subst(filterByConstructor(getUnfoldables(UNFOLDED_LHS), LRP), ARGS) + ... - 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) + // in LHS, substitute LRP(x') with \and(LRP(x'), RHS[x |-> x']) + syntax Strategy ::= "kt-subst" "(" Patterns "," Patterns ")" + rule \implies(LHS, RHS) + => \implies( subst( LHS + , LRP(UNFOLDED_ARGs) + , \and( LRP(UNFOLDED_ARGs) + , substMap(alphaRename(RHS), zip(ARGs, UNFOLDED_ARGs)) + ) + ) + , RHS + ) + + kt-subst((LRP:Symbol(UNFOLDED_ARGs), RECs), ARGs) + => kt-subst(RECs, ARGs) + ... + + rule kt-subst(.Patterns, ARGs) => noop ... + + // TODO: combine with other kt-unfold rules + rule \implies(LHS, \nu X . P) + => \implies(LHS, subst(P, X, alphaRename(LHS))) + + gfp => noop ... + // unfolded fixed point, HEAD, LRP variables, RHS syntax Pattern ::= substituteBRPs(Pattern, Symbol, Patterns, Pattern) [function] rule substituteBRPs(P:Int, RP, Vs, RHS) => P @@ -245,58 +291,62 @@ 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 ... ``` -### `kt-collapse` +### `with-each-implication-context` ```k - syntax Strategy ::= "kt-collapse" + syntax Strategy ::= "with-each-implication-context" "(" Strategy ")" ``` If there are no implication contexts to collapse, we are done: ```k - rule GOAL - kt-collapse => noop ... - requires notBool(hasImplicationContext(GOAL)) - - rule GOAL - imp-ctx-unfold => noop ... - requires notBool(hasImplicationContext(GOAL)) + rule \implies(LHS, RHS) + with-each-implication-context(S) => noop ... + requires notBool(hasImplicationContext(LHS)) + rule \implies(LHS, RHS) + with-each-implication-context(S) => S . with-each-implication-context(S) ... + requires hasImplicationContext(LHS) ``` -#### Normalizing terms +### `normlize-implication-context` + +This strategy exercises various commutativity axioms and brings an +`implicationContext` and its `#hole` to the first leaf position of the formula. -Bring terms containing the implication context to the front: +```k + syntax Strategy ::= "normalize-implication-context" +``` ```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 ... + + normalize-implication-context ... 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 ... + + normalize-implication-context ... 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,25 +358,51 @@ 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 + + normalize-implication-context ... + requires (P =/=K #hole { Bool } orBool P =/=K #hole { TopSort }) + andBool (#hole { Bool } in Ps orBool #hole { TopSort } 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 + + normalize-implication-context ... + requires notBool(#hole { Heap } in getFreeVariables(P)) + andBool #hole { Heap } in getFreeVariables(Ps) + + rule \implies(\and(sep(\forall { _ } + implicationContext( \and( (sep(P, Ps) => sep(Ps ++Patterns P)) + , _) + , _) + ,_ ), _), _) + + normalize-implication-context ... + requires P =/=K #hole { Heap } + andBool #hole { Heap } in getFreeVariables(Ps) +``` + +```k + rule \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { Bool }, _) , _ ) , _ ) , _ ) + normalize-implication-context => noop ... + rule \implies(\and( S:Symbol(\forall { UNIVs } implicationContext( \and(#hole { TopSort }, _) , _ )) , _ ) , _ ) + normalize-implication-context => noop ... + rule \implies(\and( sep(\forall { UNIVs } implicationContext( \and(sep(#hole { Heap }, _), _) , _ ) , _ ), _ ), _ ) + normalize-implication-context => noop ... +``` + +### `kt-collapse` + + +```k + syntax Strategy ::= "kt-collapse" ``` #### Collapsing contexts (FOL) @@ -335,8 +411,8 @@ 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 } - ( implicationContext( \and(#hole, CTXLHS:Patterns) + rule \implies(\and( \forall { UNIVs } + ( implicationContext( \and(#hole { Bool }, CTXLHS:Patterns) , CTXRHS:Pattern ) => \implies(\and(CTXLHS), CTXRHS) @@ -345,42 +421,151 @@ solver using `kt-solve-implications` ) , RHS:Pattern ) - - kt-collapse ... + + kt-collapse ... ``` #### Collapsing contexts (SL) -In the separation logic case, we must use matching. +In the separation logic case, we must use matching to collapse the implication context.. -First, we use matching to instantiate the quantifiers of the implication context. +First, we use match to instantiate the quantifiers of the implication context. Then we apply the substitution to the context, including the constraints. -Next, duplicate constraints are removed using the ad-hoc rule below until the implication -context has no constraints. + +If matching fails, we replace the implication context with a symbolic heap and +continue (`kt-collapse-no-match`). This allows the proof to proceed even if +we cannot infer any additional information about that part of the heap. + +If we do match, we perform a `case-analsysis` over the constraints on the left-hand-side +of the implication context. + +1. Assuming the constraints on the LHS of the implication context do not hold, prove RHS. + While we still use the `kt-collapse-no-match` strategy, we are have addition information: + that the negation of the constraints in the context left hand side hold. + +2. Assuming the constraints on the LHS of the implication context *do* hold + a. prove that we can collapse the context. Even though we have already matched + this is *not* redundant. Since LCTX may have multiple conjuncted heaps, + and matching only proves that we satisfy one, but not all of them. + b. using the collapsed context we are able to prove the RHS + +Note that in this sense we take advantage of implication contexts being more general +than the magic wand. The magic wand does not let you directly represent patterns of +the form `( [] * a ) /\ b -o psi`. i.e. patterns where the context is a conjunction +of heaps. + +``` +1. LHS[?H] /\ not(LCTXCONSTR) -> RHS +2a. LHS[#hole] /\ LCTXCONSTR -> \exists X . REST[LCTX[#hole]] +2b. REST[RCTX] /\ LCTXCONSTR -> RHS +--------------------------------------------------------------------------- Where X does not occur in RCTX or LCTXCONSTR + LHS[\forall X. \ic(LCTX[#hole], RCTX)] -> RHS +``` + ```k - rule \implies(\and( sep ( \forall { UNIVs } - implicationContext( \and(sep(#hole, CTXLHS:Patterns), CTXLCONSTRAINTS) , _) + rule \implies(\and( sep ( \forall { UNIVs } + implicationContext( \and(sep(#hole { Heap }, CTXLHS:Patterns), CTXLCONSTRAINTS) , _) , LSPATIAL ) , LHS:Patterns ) , RHS:Pattern ) - - kt-collapse + + kt-collapse => with-each-match( #match(terms: LSPATIAL, pattern: CTXLHS, variables: UNIVs) , kt-collapse + , kt-collapse-no-match ) ... - - requires UNIVs =/=K .Patterns + ``` ```k - rule \implies(\and( ( sep ( \forall { UNIVs => .Patterns } - ( implicationContext( \and(sep(_), CTXLCONSTRAINTS), CTXRHS ) #as CTX - => substMap(CTX, SUBST) + rule \implies( \and( ( sep ( \forall { UNIVs => UNIVs -Patterns fst(unzip(SUBST)) } + ( implicationContext( \and(sep(_), CTXLHS), CTXRHS ) #as CTX + => substMap(CTX, SUBST) + ) + , LSPATIAL + ) + ) + , LHS:Patterns + ) + , RHS:Pattern + ) + + ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) + => case-analysis( \and(getPredicatePatterns(substPatternsMap(CTXLHS, SUBST))) + , lift-or . and-split . normalize-implication-context . kt-collapse-no-match + , kt-collapse-matched(rest: REST) + ) + ... + +``` + +```k + syntax UpperName ::= "#rest" [token] + rule \implies( \and( S:Symbol ( \forall { UNIVs } + implicationContext(\and(CTXLHS), CTXRHS) + ) + , LHS:Patterns + ) + , RHS:Pattern + ) + + kt-collapse + => with-each-match( #matchAssoc( terms: S( #hole { TopSort } ) + , pattern: #rest[CTXLHS] + , variables: #rest { TopSort } + , subst: .Map + , rest: .Patterns + ) + , kt-collapse + , kt-collapse-no-match + ) + ... + +``` + +```k + rule \implies( \and( S:Symbol ( \forall { .Patterns } + implicationContext( \and(_), CTXRHS ) + ) + , LHS:Patterns + ) + , RHS:Pattern + ) + => \implies( \and( subst({SUBST[#rest { TopSort }]}:>Pattern, #hole { TopSort }, CTXRHS) + , LHS + ) + , RHS + ) + + ( #matchResult(subst: SUBST, rest: .Patterns) ~> kt-collapse ) + => noop + ... + +``` + +In the context of the heuristics we implement, this becomes the following, where +REST is obtained via matching: + +``` +2a. LSPATIAL[#hole] /\ LHS -> \exists UNIVs . REST[CTXLSPATIAL[#hole] /\ CTXLHS_REST] +2b. REST[CTXRHS] /\ LHS -> RHS +--------------------------------------------------------------------------- + sep(LSPATIAL[\forall X. \ic(CTXLSPATIAL[#hole] /\ CTXLHS_REST, CTXRHS)]) /\ LHS -> RHS +``` + +```k + syntax Strategy ::= "kt-collapse-matched" "(" "rest:" Patterns ")" + rule \implies(\and( ( sep ( ( \forall { UNIVs } + implicationContext( ( \and( sep(#hole { Heap }, CTXLSPATIAL) + , CTXLHS_REST) + #as CTXLHS + ) + , CTXRHS) ) , LSPATIAL ) @@ -389,16 +574,34 @@ context has no constraints. ) , RHS:Pattern ) + + kt-collapse-matched(rest: REST) + => replace-goal( \implies( \and(sep(!HOLE { Heap } + , (LSPATIAL -Patterns getImplicationContexts(LSPATIAL))) + , LHS) + , \exists { UNIVs } + \and( sep(( subst(CTXLHS, #hole { Heap }, !HOLE { Heap }) + , REST + ) -Patterns getImplicationContexts(REST) + ) + ) + ) + ) + & replace-goal( \implies( \and(sep(CTXRHS ++Patterns REST), LHS) + , RHS + ) + ) + ... - ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) - => kt-collapse - ... - - requires UNIVs =/=K .Patterns - andBool UNIVs -Patterns fst(unzip(SUBST)) ==K .Patterns + requires getImplicationContexts(LSPATIAL) ==K getImplicationContexts(CTXLSPATIAL ++Patterns REST) +``` - rule \implies(\and( ( sep ( \forall { UNIVs => .Patterns } - ( implicationContext( \and(sep(_), CTXLCONSTRAINTS), CTXRHS ) #as CTX +```k + syntax Strategy ::= "kt-collapse-no-match" + rule \implies(\and( ( sep ( ( ( \forall { UNIVs } + implicationContext( \and(sep(_), CTXLCONSTRAINTS), CTXRHS ) + ) + => !H { Heap } ) , LSPATIAL ) @@ -407,85 +610,80 @@ context has no constraints. ) , RHS:Pattern ) - - ( #matchResult(subst: SUBST, rest: REST) ~> kt-collapse ) - => fail + + kt-collapse-no-match => noop ... - - requires UNIVs =/=K .Patterns - andBool UNIVs -Patterns fst(unzip(SUBST)) =/=K .Patterns + ``` -Finally, we use matching on the no universal quantifiers case to collapse the context. +### Case analysis + +``` + PHI /\ P -> PSI PHI /\ not(P) -> PSI + ------------------------------------------- case-analsysis(P) + PHI -> PSI +``` ```k - rule \implies(\and( sep ( \forall { .Patterns } - implicationContext( \and(sep(#hole, CTXLHS:Patterns)) , _) - , LSPATIAL - ) - , LHS:Patterns - ) - , RHS:Pattern - ) - - kt-collapse - => with-each-match( #match(terms: LSPATIAL, pattern: CTXLHS, variables: .Patterns) - , kt-collapse - ) - ... - + syntax Strategy ::= "case-analysis" "(" Pattern "," negative: Strategy "," positive: Strategy ")" + rule \implies(\and(LHS), RHS) + ( case-analysis(P, NEG, POS) ~> #hole . REST ) + => subgoal( \implies(\and(\not(P), LHS ), RHS) + , NEG . REST + ) + & subgoal( \implies(\and(#flattenAnds(LHS ++Patterns P)), RHS) + , POS . REST + ) + + rule case-analysis(_, _, _) + ~> ( (#hole . S1 ~> #hole . S2) + => #hole . S1 . S2 + ) + ... + +``` - rule \implies( \and( ( sep ( \forall { .Patterns } - implicationContext( \and(sep(_)) , CTXRHS) +```k + syntax Strategy ::= "kt-collapse-unsat" + rule \implies( \and( sep ( \forall { UNIVs } implicationContext(_, _) , LSPATIAL ) - => sep(substMap(CTXRHS, SUBST) ++Patterns REST) - ) , LHS:Patterns - ) - , RHS:Pattern - ) - - ( #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 + ) + , RHS:Pattern + ) + => \implies( \and( sep(LSPATIAL ++Patterns !H:VariableName { Heap }, .Patterns) + , LHS:Patterns + ) + , RHS:Pattern + ) + + kt-collapse-unsat => noop ... -```k - rule \implies(\and( sep ( \forall { .Patterns } - implicationContext( \and( sep(_) - , ( CTXCONSTRAINT, CTXCONSTRAINTs - => CTXCONSTRAINTs - ) - ) , _) - , LSPATIAL - ) - , LHS:Patterns - ) - , RHS:Pattern - ) - - kt-collapse ... - requires isPredicatePattern(CTXCONSTRAINT) - andBool CTXCONSTRAINT in LHS - - rule \implies(\and( sep ( \forall { .Patterns } - implicationContext( \and( sep(_) - , ( CTXCONSTRAINT, CTXCONSTRAINTs ) - ) , _) - , LSPATIAL - ) - , LHS:Patterns - ) - , RHS:Pattern - ) - - kt-collapse => fail ... - requires isPredicatePattern(CTXCONSTRAINT) - andBool notBool (CTXCONSTRAINT in LHS) + // 2a and 2b in rule above + syntax Strategy ::= "kt-collapse-valid" + rule \implies(\and( sep ( \forall { UNIVs } + implicationContext( LCTX , RCTX ) + , LSPATIAL + ) + , LHS:Patterns + ) + , RHS:Pattern + ) + + ( kt-collapse-valid ~> #hole . REST ) + => subgoal( \implies( \and(sep(LSPATIAL ++Patterns !H:VariableName { Heap }), LHS) + , \exists { UNIVs ++Patterns #hole { Heap } } LCTX + ) + , REST + ) + & subgoal( \implies( \and(sep(RCTX, LSPATIAL), LHS) + , RHS + ) + , REST + ) + + requires getFreeVariables(RCTX) intersect UNIVs ==K .Patterns ``` ### Unfolding within the implication context @@ -495,8 +693,8 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i ``` ```k - rule \implies(\and( sep ( \forall { UNIVs } - implicationContext( \and( sep( #hole + rule \implies(\and( sep ( \forall { UNIVs } + implicationContext( \and( sep( #hole { Heap } , CTXLHS:Patterns ) , CTXLCONSTRAINTS @@ -509,20 +707,20 @@ 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 } - implicationContext( \and(sep(#hole, CTXLHS:Patterns)) , _) + rule \implies(\and( sep ( \forall { .Patterns } + implicationContext( \and(sep(#hole { Heap }, CTXLHS:Patterns)) , _) , LSPATIAL ) , LHS:Patterns ) , RHS:Pattern ) - - imp-ctx-unfold => right-unfold-eachRRP(getUnfoldables(CTXLHS)) ... + + imp-ctx-unfold => right-unfold-eachRRP(getUnfoldables(CTXLHS)) ... ``` #### Infrastructure @@ -534,31 +732,24 @@ TODO: This is pretty adhoc: Remove constraints in the context that are already i rule substituteWithEach(P, V, (I, Is)) => subst(P, V, I), substituteWithEach(P, V, Is) - syntax Patterns ::= filterVariablesBySort(Patterns, Sort) [function] - rule filterVariablesBySort(.Patterns, _) => .Patterns - rule filterVariablesBySort(((_ { S } #as V), Vs), S) - => V, filterVariablesBySort(Vs, S) - rule filterVariablesBySort((V, Vs), S) - => 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 +757,17 @@ 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) - => \and(REST) - , _ - ) + rule \implies( \and(\forall { Us } \implies(LIMPLIES, RIMPLIES), LHS), RHS ) + => \implies( \and(LHS), RHS ) + + kt-solve-implications( STRAT ) + => ( kt-solve-implication( subgoal(\implies(\and(removeImplications(LHS)), \exists { Us } LIMPLIES), STRAT) + , RIMPLIES + ) + . 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 +776,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 +805,64 @@ 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) - => S ~> kt-solve-implication(#hole, 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) - => kt-solve-implication(T, RHS) - ... - - rule kt-solve-implication(fail, RHS) => noop ... - rule kt-solve-implication(success, CONC) => noop ... + + 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) + => \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..8253ed7f2 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -36,15 +36,36 @@ module MATCHING-FUNCTIONAL rule (MR1, MR1s) ++MatchResults MR2s => MR1, (MR1s ++MatchResults MR2s) rule .MatchResults ++MatchResults MR2s => MR2s - rule #match( terms: T, pattern: P, variables: Vs ) - => #filterErrors( #matchAssocComm( terms: T - , pattern: P - , variables: Vs - , results: .MatchResults - , subst: .Map - , rest: .Patterns - ) - ) + rule #match( terms: \and(T, Ts), pattern: P, variables: Vs ) + => #match( terms: T, pattern: P, variables: Vs ) + ++MatchResults #match( terms: \and(Ts), pattern: P, variables: Vs ) + requires \and(_) :/=K P + rule #match( terms: \and(T, .Patterns), pattern: P, variables: Vs ) + => #match( terms: T, pattern: P, variables: Vs ) + requires \and(_) :/=K P + rule #match( terms: \and(.Patterns), pattern: P, variables: Vs ) + => .MatchResults + requires \and(_) :/=K P + + rule #match( terms: sep(Ts), pattern: sep(Ps), variables: Vs ) + => #filterErrors( #matchAssocComm( terms: Ts + , pattern: Ps + , variables: Vs + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + + rule #match( terms: Ts, pattern: Ps, variables: Vs ) + => #filterErrors( #matchAssoc( terms: Ts + , pattern: Ps + , variables: Vs + , subst: .Map + , rest: .Patterns + ) + ) + [owise] syntax MatchResults ::= #filterErrors(MatchResults) [function] rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs) @@ -56,21 +77,23 @@ module MATCHING-FUNCTIONAL Work around OCaml not producing reasonable error messages: ```k + syntax MatchResult ::= MatchStuck + syntax MatchStuck ::= "#matchStuck" "(" K ")" syntax KItem ::= "\\n" [format(%n)] - rule #matchAssocComm(terms: T - , pattern: P + rule #matchAssocComm( terms: T + , pattern: P , variables: Vs , results: MRs , subst: SUBST , rest: REST ) - => #error( "AC" - ~> "terms:" ~> T - ~> "pattern:" ~> P - ~> "variables:" ~> Vs - ~> "subst:" ~> SUBST - ~> "rest:" ~> REST - ~> "MRs:" ~> MRs ) + => #matchStuck( "AC" + ~> "terms:" ~> T + ~> "pattern:" ~> P + ~> "variables:" ~> Vs + ~> "subst:" ~> SUBST + ~> "rest:" ~> REST + ~> "MRs:" ~> MRs ) , .MatchResults [owise] ``` @@ -78,6 +101,19 @@ Work around OCaml not producing reasonable error messages: Recurse over assoc-only constructors (including `pto`): ```k + // TODO: matching over context patterns + rule #matchAssoc( terms: S:Symbol(T), .Patterns + , pattern: V[T], .Patterns + , variables: Vs + , subst: SUBST + , rest: REST + ) + => #matchResult( subst: SUBST V { getReturnSort(S(T)) } |-> S( #hole { getReturnSort(T) }) + , rest: .Patterns + ) + , .MatchResults + requires V { getReturnSort(S(T)) } in Vs + // Base case rule #matchAssoc( terms: .Patterns , pattern: .Patterns @@ -128,26 +164,108 @@ Recurse over assoc-only constructors (including `pto`): ) requires S =/=K sep + rule #matchAssoc( terms: \not(T), Ts + => T, Ts + , pattern: \not(P), Ps + => P, Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + + // TODO: the conjunction/disjunction matching rules should be more general, i.e. aware of commutativity + // Recursive over conjunction + rule #matchAssoc( terms: \and(T_ARGs), Ts + => T_ARGs ++Patterns Ts + , pattern: \and(P_ARGs), Ps + => P_ARGs ++Patterns Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + + // Recursive over disjunction + rule #matchAssoc( terms: \or(T_ARGs), Ts + => T_ARGs ++Patterns Ts + , pattern: \or(P_ARGs), Ps + => P_ARGs ++Patterns Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + + // Recursive over disjunction + rule #matchAssoc( terms: \exists { .Patterns } T, Ts + => T, Ts + , pattern: \exists { .Patterns } P, Ps + => P, Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + + // Both term and pattern are a mu: + // Recurse over pattern with same fresh variable for each mu term + rule #matchAssoc( terms: (\mu X . T), Ts + => subst(#nnf(T), X, !F:SetVariable), Ts + , pattern: (\mu Y . P), Ps + => subst(#nnf(P), Y, !F), Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + + // Both term and pattern are a nu: + // Recurse over pattern with same fresh variable for each nu term + rule #matchAssoc( terms: (\nu X . T), Ts + => subst(#nnf(T), X, !F:SetVariable), Ts + , pattern: (\nu Y . P), Ps + => subst(#nnf(P), Y, !F), Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + // ground variable: identical rule #matchAssoc( terms: P:Variable, Ts => Ts - , pattern: P:Variable, Ps => Ps + , pattern: P, Ps => Ps + , variables: Vs + , subst: _ + , rest: REST + ) + requires notBool P in Vs + + rule #matchAssoc( terms: P:SetVariable, Ts => Ts + , pattern: P, Ps => Ps , variables: Vs , subst: _ , rest: REST ) requires notBool P in Vs + rule #matchAssoc( terms: T, Ts + , pattern: P, Ps + , variables: Vs + , subst: _ + , rest: REST + ) + => #error("Ground term does not match"), .MatchResults + requires T =/=K P + andBool (isSetVariable(T) orBool isVariable(T)) + andBool notBool P in Vs + // ground variable: non-identical rule #matchAssoc( terms: T, Ts - , pattern: P:Variable, Ps + , pattern: P, Ps , variables: Vs , subst: _ , rest: REST ) => #error( "No valid substitution" ), .MatchResults requires T =/=K P + andBool (isSetVariable(P) orBool isVariable(P)) andBool notBool P in Vs - + // free variable: different sorts rule #matchAssoc( terms: T , Ts , pattern: P:Variable, Ps @@ -184,6 +302,7 @@ Recurse over assoc-comm `sep`: , rest: REST ) => #error( "Pattern larger than term" ), .MatchResults + requires notBool P in Vs // Base case: emp matches all heaps rule #matchAssocComm( terms: Ts @@ -195,7 +314,7 @@ Recurse over assoc-comm `sep`: ) => #matchResult(subst: SUBST, rest: REST ++Patterns Ts), .MatchResults -// Base case: If matching a single term, agains an atomic pattern, use Assoc Matching +// Base case: If matching a single term against an atomic pattern, use Assoc Matching rule #matchAssocComm( terms: T, .Patterns , pattern: P, .Patterns , variables: Vs @@ -209,6 +328,7 @@ Recurse over assoc-comm `sep`: , subst: SUBST , rest: REST ) + requires notBool P in Vs ``` Matching an atomic pattern against multiple terms: return a disjunction of the solutions @@ -236,6 +356,7 @@ Matching an atomic pattern against multiple terms: return a disjunction of the s , rest: T, REST ) requires Ts =/=K .Patterns + andBool notBool P in Vs ``` Matching a non-atomic pattern against multiple terms: Match the first @@ -264,6 +385,37 @@ atom in the pattern against any of the terms, and then extend those solutions. ) requires ARGs =/=K .Patterns andBool P_ARGs =/=K .Patterns + andBool notBool P_ARG in Vs +``` + +Base case: If matching a single term against a heap variable, return REST +TODO: if there are multiple heap variables, we need to return all possible partitions. +Currently, the entire REST is constrained to a single heap variable +TODO: other corner cases probably + +```k + rule #matchAssocComm( terms: Ts + , pattern: (H:Variable, P, Ps) + => ((P, Ps) ++Patterns H) + , variables: Vs + , results: .MatchResults + , subst: SUBST + , rest: .Patterns + ) + requires notBool isVariable(P) + + rule #matchAssocComm( terms: Ts + , pattern: H:Variable, .Patterns + , variables: Vs + , results: .MatchResults + , subst: SUBST + , rest: .Patterns + ) + => #matchResult( subst: SUBST H |-> sep(Ts) + , rest: .Patterns + ) + , .MatchResults + requires H in Vs ``` With each returned result, we apply the substitution and continue matching over @@ -271,16 +423,21 @@ the unmatched part of the term: ```k // TODO: don't want to call substUnsafe directly (obviously) - rule #matchAssocComm( terms: Ts => REST - , pattern: P => substPatternsMap(P, SUBST1) - , variables: Vs => Vs -Patterns fst(unzip(SUBST1)) - , results: #matchResult(subst: SUBST1, rest: REST), .MatchResults - => .MatchResults - , subst: SUBST2 - => (SUBST1 SUBST2) - , rest: _ + rule #matchAssocComm( terms: Ts + , pattern: P + , variables: Vs + , results: #matchResult(subst: SUBST_INNER, rest: REST_INNER), .MatchResults + , subst: SUBST + , rest: REST + ) + => #matchAssocComm( terms: REST_INNER + , pattern: substPatternsMap(P, SUBST_INNER) + , variables: Vs -Patterns fst(unzip(SUBST_INNER)) + , results: .MatchResults + , subst: SUBST_INNER SUBST + , rest: REST ) - requires intersectSet(keys(SUBST1), keys(SUBST2)) ==K .Set + requires intersectSet(keys(SUBST_INNER), keys(SUBST)) ==K .Set ``` Failures are propagated: @@ -341,86 +498,105 @@ 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 - => with-each-match(#match( terms: LSPATIAL + rule \implies(\and(LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) + match + => with-each-match(#match( terms: \and(getSpatialPatterns(LHS)) , pattern: RSPATIAL , variables: Vs - ) - , match ) - ... - - requires isSpatialPattern(sep(LSPATIAL)) - andBool isSpatialPattern(sep(RSPATIAL)) - rule \implies( \and( LSPATIAL, LHS) - , \exists { Vs } \and( RHS ) - => \exists { Vs -Patterns fst(unzip(SUBST)) } substMap(\and(RHS), SUBST) + , match + ) + ... + + requires isSpatialPattern(sep(RSPATIAL)) + andBool getFreeVariables(getSpatialPatterns(sep(RSPATIAL), RHS)) intersect Vs =/=K .Patterns + + rule \implies(\and(LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) + match-debug => wait ... + _ + => #match( terms: \and(getSpatialPatterns(LHS)) + , pattern: RSPATIAL + , variables: Vs + ) + + requires isSpatialPattern(sep(RSPATIAL)) + + rule \implies(\and(LHS) , \exists { Vs } \and(RHS)) + match => noop ... + requires getFreeVariables(getSpatialPatterns(RHS)) intersect Vs ==K .Patterns + rule \implies( \and( LSPATIAL, LHS) + , \exists { Vs } \and(sep(RSPATIAL), RHS) + => \exists { Vs -Patterns fst(unzip(SUBST)) } + #flattenAssoc(substMap( \and(getSpatialPatterns(RHS) ++Patterns (sep(RSPATIAL), (RHS -Patterns getSpatialPatterns(RHS)))) + , SUBST + ) + ) ) + + ( #matchResult(subst: SUBST, rest: .Patterns) ~> match ) + => 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 => noop ... 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 +607,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) @@ -457,12 +633,13 @@ Instantiate existentials using matching on the spatial part of goals: Instantiate heap axioms: ```k - syntax Strategy ::= "instantiate-axiom" "(" Pattern ")" + syntax Strategy ::= "instantiate-heap-axiom" "(" Pattern ")" | "instantiate-separation-logic-axioms" "(" Patterns ")" - rule instantiate-separation-logic-axioms - => instantiate-separation-logic-axioms(gatherHeapAxioms(.Patterns)) - ... - + | "pto-is-injective" "(" Patterns ")" + rule instantiate-separation-logic-axioms + => instantiate-separation-logic-axioms(gatherHeapAxioms(.Patterns)) + ... + axiom _: heap(LOC, DATA) syntax Patterns ::= gatherHeapAxioms(Patterns) [function] @@ -471,132 +648,366 @@ Instantiate heap axioms: requires notBool(heap(LOC, DATA) in AXs) rule gatherHeapAxioms(AXs) => AXs [owise] - 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 }))) - , \not(\equals( parameterizedSymbol(nil, LOC)(.Patterns), !L { LOC })) - ) - ) - . instantiate-axiom( \forall { !L1 { LOC }, !D1 {DATA}, !L2 { LOC }, !D2 { DATA } } - \implies( \and(sep(pto(!L1 { LOC }, !D1 { DATA }), pto(!L2 { LOC }, !D2 { DATA })) ) - , \not(\equals( !L1 { LOC }, !L2 { LOC }) ) - ) - ) - ... - - rule instantiate-separation-logic-axioms(.Patterns) => noop ... + rule instantiate-separation-logic-axioms(heap(LOC, DATA), AXs) + => instantiate-separation-logic-axioms(AXs) + . instantiate-heap-axiom( \forall { !L { LOC }, !D {DATA} } + \implies( \and(sep(pto(!L { LOC }, !D { DATA }))) + , \not(\equals(nil { LOC }(.Patterns), !L { LOC })) + ) + ) + . instantiate-heap-axiom( \forall { !L1 { LOC }, !D1 { DATA }, !L2 { LOC }, !D2 { DATA } } + \implies( \and(sep(pto(!L1 { LOC }, !D1 { DATA }), pto(!L2 { LOC }, !D2 { DATA })) ) + , \not(\equals( !L1 { LOC }, !L2 { LOC }) ) + ) + ) + ... + + 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 } - \implies( \and(sep(AXIOM_LSPATIAL)) - , AXIOM_RHS - ) - ) #as STRAT - => ( #match( terms: LSPATIAL + rule \implies(\and(LHS), RHS) + instantiate-heap-axiom(\forall { Vs } + \implies( \and(sep(AXIOM_LSPATIAL)) + , AXIOM_RHS + ) + ) #as STRAT + => ( #match( terms: \and(getSpatialPatterns(LHS)) , pattern: AXIOM_LSPATIAL , variables: Vs ) ~> STRAT:Strategy ) ... - + requires isSpatialPattern(sep(AXIOM_LSPATIAL)) - rule \implies(\and((sep(_) #as LSPATIAL), (LCONSTRAINT => substMap(AXIOM_RHS, SUBST), LCONSTRAINT)) - , RHS - ) - - ( #matchResult( subst: SUBST, rest: _ ) , MRs - ~> instantiate-axiom(\forall { Vs } - \implies( _ - , AXIOM_RHS - ) - ) #as STRAT + rule \implies(\and(LHS), RHS) + => \implies(\and(substMap(AXIOM_RHS, SUBST), LHS), RHS) + + ( #matchResult( subst: SUBST, rest: _ ) , MRs + ~> instantiate-heap-axiom(\forall { Vs } + \implies( _ + , AXIOM_RHS + ) + ) #as STRAT ) => ( MRs ~> STRAT:Strategy ) ... - + requires isPredicatePattern(AXIOM_RHS) - rule (.MatchResults ~> instantiate-axiom(_)) => noop ... + rule (.MatchResults ~> instantiate-heap-axiom(_)) => noop ... + + syntax Patterns ::= getLocations(Pattern) [function] + syntax Patterns ::= getLocationsPs(Patterns) [function] + rule getLocationsPs(.Patterns) => .Patterns + rule getLocationsPs(P, Ps) => getLocations(P) ++Patterns getLocationsPs(Ps) + rule getLocations(V:Variable) => .Patterns + rule getLocations(pto(X, Y)) => X, .Patterns + rule getLocations(S:Symbol(_)) => .Patterns + requires S =/=K pto andBool S =/=K sep + rule getLocations(\and(Ps)) => getLocationsPs(Ps) + rule getLocations(sep(Ps)) => getLocationsPs(Ps) + rule getLocations(\or(Ps)) => getLocationsPs(Ps) + rule getLocations(P) => .Patterns + requires isPredicatePattern(P) + + rule \implies(LHS, RHS) + pto-is-injective => pto-is-injective(getLocations(LHS)) ... + + rule pto-is-injective(.Patterns) => noop ... + + // TODO: this should become unification + rule \implies(\and(sep(SPATIAL1), sep(SPATIAL2), LHS), RHS) + pto-is-injective(L { LOC }, LOCs) + => #match( terms: SPATIAL1 + , pattern: pto(L { LOC }, !D1 { DATA }) + , variables: !D1 { DATA } + ) + ~> #match( terms: SPATIAL2 + , pattern: pto(L { LOC }, !D2 { DATA }) + , variables: !D2 { DATA } + ) + ~> pto-is-injective(L { LOC }, LOCs) + ... + + axiom _: heap(LOC, DATA) - rule \implies( \and(sep(LSPATIAL), LCONSTRAINT) - , \exists{ Vs } \and(sep(RSPATIAL), RCONSTRAINT) - ) - => \implies(\and(LCONSTRAINT), \exists { Vs } \and(RCONSTRAINT)) + rule \implies(\and(LHS) , RHS) + => \implies(\and(LHS ++Patterns #destructEquality((D1, .Patterns), (D2, .Patterns))), RHS) + + #matchResult( subst: V1 |-> D1, rest: _ ), .MatchResults + ~> #matchResult( subst: V2 |-> D2, rest: _ ), .MatchResults + ~> pto-is-injective(L { LOC }, LOCs) + => pto-is-injective(LOCs) + ... - spatial-patterns-equal => noop ... - requires LSPATIAL -Patterns RSPATIAL ==K .Patterns - andBool RSPATIAL -Patterns LSPATIAL ==K .Patterns - rule \implies( \and(sep(LSPATIAL), _) - , \exists{ Vs } \and(sep(RSPATIAL), _) - ) + syntax Patterns ::= #destructEquality(Patterns, Patterns) [function] + rule #destructEquality(.Patterns, .Patterns) => .Patterns + rule #destructEquality((P1, Ps1), (P2, Ps2)) + => \equals(P1, P2), #destructEquality(Ps1, Ps2) + requires S:Symbol(_) :/=K P1 + rule #destructEquality((P1, Ps1), (P2, Ps2)) + => \equals(P1, P2), #destructEquality(Ps1, Ps2) + requires S:Symbol(_) :/=K P2 + rule #destructEquality((S:Symbol(ARGs1), Ps1), (S:Symbol(ARGs2), Ps2)) + => #destructEquality(ARGs1, ARGs2) ++Patterns #destructEquality(Ps1, Ps2) + requires isConstructor(S) + rule #destructEquality((S1:Symbol(ARGs1), Ps1), (S2:Symbol(ARGs2), Ps2)) + => \equals(S1(ARGs1), S2(ARGs2)), #destructEquality(Ps1, Ps2) + requires S1 =/=K S2 orBool notBool isConstructor(S1) +``` + +If the RHS is empty, we have nothing to do + +```k + rule \implies(LHS, \exists { Vs } \and(.Patterns)) + patterns-equal => noop ... +``` + +Remove any patterns on the RHS that match a pattern on the LHS: + +```k + rule \implies(\and(LHS), \exists{Vs} \and(RHS, REST)) + patterns-equal + => with-each-match( #match( terms: \and(LHS) + , pattern: RHS + , variables: .Patterns + ) + , patterns-equal + ) + ... + + + rule \implies(LHS, \exists{ Vs } \and(RHS, REST)) + => \implies(LHS, \exists{ Vs } \and(REST)) + + #matchResult(subst: .Map , rest: .Patterns) + ~> patterns-equal + => patterns-equal + ... - spatial-patterns-equal => fail ... - requires LSPATIAL -Patterns RSPATIAL =/=K .Patterns - orBool RSPATIAL -Patterns LSPATIAL =/=K .Patterns + + rule #matchResult(subst: .Map , rest: P, Ps) + ~> patterns-equal + => fail + ... + +``` + +If the RHS has no spatial part, then there is nothing to do: + +```k + rule \implies(LHS, \exists { Vs } RHS) + spatial-patterns-equal => noop ... + requires isPredicatePattern(RHS) ``` +If there is some remaining spatial part, bring it to the front: + +```k + rule \implies(LHS, \exists { Vs } \and(P, RHS)) + => \implies(LHS, \exists { Vs } \and(RHS ++Patterns P)) + + spatial-patterns-equal ... + requires isPredicatePattern(P) + andBool notBool isPredicatePattern(\and(RHS)) +``` + +Remove any spatial pattern on the RHS that matches a spatial pattern on the LHS: + ```k - rule \implies( \and(sep( LSPATIAL ) , _ ) + rule \implies(\and(LHS), \exists{Vs} \and(RSPATIAL, RHS)) + => \implies(\and(LHS), \exists{Vs} \and(sep(RSPATIAL), RHS)) + + spatial-patterns-equal ... + requires isSpatialPattern(RSPATIAL) + andBool sep(_) :/=K RSPATIAL + + rule \implies(\and(LHS), \exists{Vs} \and(sep(RSPATIAL), RHS)) + spatial-patterns-equal + => with-each-match( #match( terms: \and(getSpatialPatterns(LHS)) + , pattern: RSPATIAL + , variables: .Patterns + ) + , spatial-patterns-equal + ) + ... + + rule \implies(LHS, \exists{ Vs } \and(sep(RSPATIAL), RHS)) + => \implies(LHS, \exists{ Vs } \and(RHS)) + + #matchResult(subst: .Map , rest: .Patterns) + ~> spatial-patterns-equal + => spatial-patterns-equal + ... + + + rule #matchResult(subst: .Map , rest: P, Ps) + ~> spatial-patterns-equal + => fail + ... + +``` + +```k + rule \implies(\and(LHS), RHS) + => \implies(\and(LHS -Patterns getSpatialPatterns(LHS)), RHS) + + spatial-patterns-match => noop ... + requires isPredicatePattern(RHS) +``` + +### Footprint Analysis + +``` + REST -> \exists d, H. H * xi |-> d + ----------------------------------- + xi |-> _ * REST -> RHS +``` + +If the left hand side contains a pointer xi |-> _ and a recursive definition, it +is sufficient to prove that the left hand side *without* xi |-> _ implies that +there is a d such that that xi |-> d. If this proof succeeds, then with +instantiate-separation-logic-axioms, we have xi pointing to two different +things, so the LHS becomes unsat. + +```k + syntax Strategy ::= "footprint-analysis" "(" Pattern ")" + + rule \implies(\and(sep(LSPATIAL), LCONSTRAINT), RHS) + footprint-analysis + => with-each-match( #match( terms: LSPATIAL + , pattern: pto(!X:VariableName { LOC }, !Y:VariableName { DATA }) + , variables: !X { LOC }, !Y { DATA } + ) + , footprint-analysis( pto(!X { LOC }, !Y { DATA }) ) + ) + ... + + axiom _: heap(LOC, DATA) + +// TODO: figure out why rule gets stuck when requires clause is uncommented + rule \implies(\and(sep(LSPATIAL), LCONSTRAINT), RHS) + => \implies( \and(sep(REST), LCONSTRAINT), + \exists { !D:VariableName { DATA }, !H:VariableName { Heap } } + \and(sep(pto(XMATCH, !D:VariableName { DATA }), !H { Heap })) + ) + + #matchResult( subst: X { LOC } |-> XMATCH + Y { DATA } |-> YMATCH + , rest: REST + ) + ~> footprint-analysis( pto(X { LOC }, Y { DATA }) ) + => noop + ... + +// requires LSPATIAL -Patterns REST ==K pto(XMATCH, YMATCH) +``` + +### Nullity Analysis + +``` + LHS -> \exists d, H. xi |-> d * H LHS /\ xi =/= nil -> RHS + --------------------------------------------------------------- + LHS -> RHS +``` + +```k + + syntax Strategy ::= "nullity-analysis" "(" Patterns "," Strategy ")" + + rule \implies(LHS, RHS) + nullity-analysis(S) + => nullity-analysis(filterVariablesBySort(getFreeVariables(LHS), LOC), S) + ... + + axiom _: heap(LOC, DATA) + + rule \implies(LHS, RHS) + nullity-analysis(.Patterns, S) => fail ... + + rule \implies( \and( sep(LSPATIAL), LCONSTRAINT), RHS) + => \implies( \and( \forall { !D:VariableName { DATA }, !H:VariableName { Heap } } + \implies( \and(sep(pto(V, !D:VariableName { DATA }), !H { Heap })) + , \not(\equals( V + , nil { LOC }(.Patterns) + ) + ) + ) + , sep(LSPATIAL) + , LCONSTRAINT + ) + , RHS + ) + + nullity-analysis((V, Vs), S) + => kt-solve-implications(S) + | nullity-analysis(Vs, S) + ... + + axiom _: heap(LOC, DATA) +``` + +```k + 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)) ) , normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals . ( noop | left-unfold-Nth(0) | left-unfold-Nth(1) | left-unfold-Nth(2) ) . normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals - . instantiate-separation-logic-axioms . subsume-spatial . (smt-cvc4) + . instantiate-separation-logic-axioms . spatial-patterns-match . (smt-cvc4) ) ~> 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 ... + rule frame(#hole { Heap }, _) => fail ... syntax Patterns ::= filterClausesInvolvingVariable(Variable, Patterns) [function] rule filterClausesInvolvingVariable(V, (P, Ps)) @@ -609,19 +1020,18 @@ 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)) ``` ```k endmodule ``` - 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..46192d6b7 100644 --- a/prover/strategies/search-bound.md +++ b/prover/strategies/search-bound.md @@ -8,60 +8,61 @@ 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) - => normalize . or-split-rhs - . lift-constraints . instantiate-existentials . substitute-equals-for-equals - . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat - . ( right-unfold-all(bound: UNFOLDBOUND) ) - . normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals - . match . spatial-patterns-equal . smt-cvc4 - ) - | ( kt . search-sl(kt-bound: KTBOUND -Int 1, unfold-bound: UNFOLDBOUND) ) - ) - ... - + rule search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... + rule search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) + => remove-lhs-existential . normalize . or-split-rhs + . instantiate-existentials . substitute-equals-for-equals + . check-lhs-constraint-unsat + . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat + . ( right-unfold-all(bound: UNFOLDBOUND) ) + . normalize . or-split-rhs . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( 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) - => normalize . or-split-rhs - . lift-constraints . instantiate-existentials . substitute-equals-for-equals - . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat - . ( right-unfold { UNFOLDBOUND } ) - . normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals - . match . spatial-patterns-equal . smt-cvc4 - ) - | ( kt . alternate-search-sl(kt-bound: KTBOUND -Int 1, unfold-bound: UNFOLDBOUND) ) - ) - ... - + rule alternate-search-sl(kt-bound: 0, unfold-bound: UNFOLDBOUND) => fail ... + rule alternate-search-sl(kt-bound: KTBOUND, unfold-bound: UNFOLDBOUND) + => remove-lhs-existential . normalize . or-split-rhs + . instantiate-existentials . substitute-equals-for-equals + . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat + . ( right-unfold { UNFOLDBOUND } ) + . normalize . or-split-rhs . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( 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) - => normalize . or-split-rhs - . lift-constraints . instantiate-existentials . substitute-equals-for-equals - . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat - . ( right-unfold-all(bound: UNFOLDBOUND) ) - . normalize . or-split-rhs . lift-constraints . instantiate-existentials . substitute-equals-for-equals - . match . spatial-patterns-equal . smt-cvc4 - ) - | ( kt-unf . kt-unfold-search-sl(kt-bound: KTBOUND -Int 1, 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) + => remove-lhs-existential . normalize . or-split-rhs + . instantiate-existentials . substitute-equals-for-equals + . ( ( instantiate-separation-logic-axioms . check-lhs-constraint-unsat + . ( right-unfold-all(bound: UNFOLDBOUND) ) + . normalize . or-split-rhs . instantiate-existentials . substitute-equals-for-equals + . match . spatial-patterns-equal . spatial-patterns-match . smt-cvc4 + ) + | ( 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..e4ed62cd6 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] @@ -58,47 +58,40 @@ Normalize: - All \ands are flattened ```k - - rule P::Pattern => \and(P) - normalize ... - requires \and(...) :/=K P andBool \implies(...) :/=K P - - rule \and(P) => \implies(\and(.Patterns), \and(P)) - normalize ... - - rule \implies(LHS, \and(RHS)) + rule P::Pattern => \and(P) + normalize ... + requires \and(...) :/=K P andBool \implies(...) :/=K P + + rule \and(P) => \implies(\and(.Patterns), \and(P)) + normalize ... + + rule \implies(LHS, RHS) => \implies(LHS, \and(RHS)) + normalize ... + requires \and(...) :/=K RHS + andBool \exists { _ } \and(_) :/=K RHS + + rule \implies(LHS, RHS) => \implies(\and(LHS), RHS) + normalize ... + requires \and(...) :/=K LHS + + rule \implies(LHS, \and(RHS)) => \implies(LHS, \exists { .Patterns } \and(RHS)) - - normalize ... + + normalize ... - rule \implies(\and(LHS), \exists { Es } \and(RHS)) - => \implies( \and(#normalizePs(#flattenAnds(#lhsRemoveExistentialsPs(LHS)))) - , \exists { Es } \and(#normalizePs(#flattenAnds(RHS))) - ) - - normalize => noop ... + rule \implies(LHS, \exists { Es } RHS) + => \implies( #normalize(#dnf(#lhsRemoveExistentials(LHS))) + , \exists { Es } #normalize(#dnf(RHS)) + ) + + 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] - - rule #normalizePs(.Patterns) => .Patterns - rule #normalizePs(P, Ps) => #normalize(P), #normalizePs(Ps) - - // TODO: normalize on LHS and RHS? - rule #normalize(\implies(LHS, RHS)) - => \forall { .Patterns } \implies(LHS, RHS) - rule #normalize(\exists{.Patterns} P) - => #normalize(P) - - rule #normalize(\not(\exists{Vs} P)) => \forall{Vs} #normalize(\not(P)) - rule #normalize(\not(\and(Ps))) => #normalize(\or(#not(Ps))) - rule #normalize(\not(\not(P))) => #normalize(P) - rule #normalize(\or(Ps)) => \or(#normalizePs(Ps)) - rule #normalize(P) => P - [owise] + rule #normalize(\or(P, .Patterns)) => P + rule #normalize(\or(Ps)) => \or(Ps) requires getLength(Ps) =/=Int 1 ``` ### purify @@ -106,8 +99,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,37 +143,60 @@ 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 - => #getNewVariables(LHS, .Patterns) - ~> #getNewVariables(RHS, .Patterns) - ~> abstract - ... - + syntax Strategy ::= "abstract-vars" "(" Patterns "," Patterns ")" + rule \implies(LHS, \exists{_} RHS) + abstract + => abstract-vars(#getNewVariablesForNil(LHS), #getNewVariablesForNil(RHS)) + ... + + + rule \implies(LHS, \exists{_} RHS) + abstract-Nth(M) + => abstract-vars(#makeNils(#getNewVariablesForNil(LHS), M), #getNewVariablesForNil(RHS)) + ... + + + syntax Patterns ::= #makeNils(Patterns, Int) [function] + rule #makeNils(.Patterns, _) => .Patterns + rule #makeNils((V, Vs), 0) => V, #makeNils(Vs, -1) + rule #makeNils((V, Vs), I) => nil { getReturnSort(V) }(.Patterns), #makeNils(Vs, I -Int 1) + requires I =/=Int 0 - rule \implies(LHS, \and(\or(RHS))) - => \implies( #abstract(LHS, VsLHS) + rule \implies(LHS, \exists{_} \and(RHS)) + => \implies( \and(#abstract(LHS, VsLHS)) , \exists{ VsRHS } \and( #dnf(\or(\and(#createEqualities(VsLHS, VsRHS)))) , #abstract(RHS, VsRHS) ) ) + + abstract-vars(VsLHS, VsRHS) + => normalize . or-split-rhs . lift-constraints + . instantiate-separation-logic-axioms + . create-disequalities(VsLHS) + ... - (VsLHS:Patterns ~> VsRHS:Patterns ~> abstract) => noop ... - - syntax Patterns ::= #getNewVariables(Pattern, Patterns) [function] - syntax Patterns ::= #getNewVariablesPs(Patterns, Patterns) [function] - rule #getNewVariables(\and(Ps), Vs) => #getNewVariablesPs(Ps, Vs) - rule #getNewVariables(\or(Ps), Vs) => #getNewVariablesPs(Ps, Vs) - rule #getNewVariables(\not(P), Vs) => #getNewVariablesPs(P, Vs) - rule #getNewVariables(sep(Ps), Vs) => #getNewVariablesPs(Ps, Vs) - rule #getNewVariables(S(ARGs), Ps) - => (makePureVariables(ARGs) -Patterns ARGs) ++Patterns Ps - requires isUnfoldable(S) - rule #getNewVariables(pto(_), Ps) => Ps - rule #getNewVariables(\equals(_, _), Ps) => Ps - rule #getNewVariablesPs(.Patterns, _) => .Patterns - rule #getNewVariablesPs((P, Ps), Vs) => #getNewVariables(P, Vs) ++Patterns #getNewVariablesPs(Ps, Vs) + syntax Strategy ::= "create-disequalities" "(" Patterns ")" + rule \implies(\and(LHS), RHS) + => \implies(\and(LHS ++Patterns #createDisequalities(\and(LHS), VsLHS)), RHS) + + create-disequalities(VsLHS) => noop ... + + syntax Patterns ::= #getNewVariablesForNil(Pattern) [function] + syntax Patterns ::= #getNewVariablesForNilPs(Patterns) [function] + rule #getNewVariablesForNil(\and(Ps)) => #getNewVariablesForNilPs(Ps) + rule #getNewVariablesForNil(\or(Ps)) => #getNewVariablesForNilPs(Ps) + rule #getNewVariablesForNil(\not(P)) => #getNewVariablesForNil(P) + rule #getNewVariablesForNil(sep(Ps)) => #getNewVariablesForNilPs(Ps) + rule #getNewVariablesForNil(S:Symbol(ARGs)) => #getNewVariablesForNilPs(ARGs) + requires nil { _ } :/=K S + andBool S =/=K sep + rule #getNewVariablesForNil(\equals(L, R)) => .Patterns + rule #getNewVariablesForNil(V:Variable) => .Patterns + rule #getNewVariablesForNil(nil { LOC }(.Patterns)) => !V:VariableName { LOC }, .Patterns + + rule #getNewVariablesForNilPs(.Patterns) => .Patterns + rule #getNewVariablesForNilPs(P, Ps) => #getNewVariablesForNil(P) ++Patterns #getNewVariablesForNilPs(Ps) syntax Pattern ::= #abstract(Pattern, Patterns) [function] syntax Patterns ::= #abstractPs(Patterns, Patterns) [function] @@ -188,14 +204,57 @@ R(V, Vs) => exists V', R(V', Vs') and V = V' rule #abstract(\or(Ps), Vs) => \or(#abstractPs(Ps, Vs)) rule #abstract(\not(P), Vs) => \not(#abstract(P, Vs)) rule #abstract(sep(Ps), Vs) => sep(#abstractPs(Ps, Vs)) - rule #abstract(S(ARGs), Vs) - => S(#replaceNewVariables(ARGs, Vs)) - requires isUnfoldable(S) - rule #abstract(pto(ARGs), Vs) => pto(ARGs) - rule #abstract(\equals(L, R), Vs) => \equals(L, R) + rule #abstract(S:Symbol(ARGs), Vs) => S(#abstractArgs(ARGs, Vs)) + requires nil { _ } :/=K S + andBool S =/=K sep + rule #abstract(V:Variable, Vs) => V + rule #abstract(nil{_}(.Patterns), (V, Vs)) => V + rule #abstract(\equals(L, R), Vs) + => \equals( #abstract(L, Vs) + , #abstract(R, #chopPs(Vs, #countNils(L))) + ) + + syntax Patterns ::= #abstractArgs(Patterns, Patterns) [function] + rule #abstractArgs(.Patterns, Vs) => .Patterns + rule #abstractArgs((V:Variable, Ps), Vs) => V, #abstractArgs(Ps, Vs) + rule #abstractArgs((nil{_}(.Patterns), Ps), (V, Vs)) => V, #abstractArgs(Ps, Vs) + rule #abstractArgs((S:Symbol(ARGs), Ps), Vs) + => (S(#abstractArgs(ARGs, Vs)), .Patterns) ++Patterns #abstractArgs(Ps, #chopPs(Vs, #countNils(ARGs))) + requires nil { _ } :/=K S + + syntax Int ::= #countNils(Patterns) [function] + rule #countNils(.Patterns) => 0 + rule #countNils(nil{_}(.Patterns), Ps) => 1 +Int #countNils(Ps) + rule #countNils(S:Symbol(ARGs), Ps) => #countNils(ARGs) + requires nil { _ } :/=K S + rule #countNils(V:Variable, Ps) => #countNils(Ps) + rule #countNils(\not(P), Ps) => #countNils(P, Ps) + rule #countNils(\equals(L, R), Ps) => #countNils(L) +Int #countNils(R) +Int #countNils(Ps) + + syntax Patterns ::= #chopPs(Patterns, Int) [function] + rule #chopPs(Ps, M) => Ps + requires M <=Int 0 + rule #chopPs(.Patterns, M) => .Patterns + rule #chopPs((P, Ps), M) => #chopPs(Ps, M -Int 1) + requires M >Int 0 rule #abstractPs(.Patterns, _) => .Patterns - rule #abstractPs((P, Ps), Vs) => #abstract(P, Vs), #abstractPs(Ps, Vs) + rule #abstractPs((P, Ps), Vs) => #abstract(P, Vs) ++Patterns #abstractPs(Ps, #chopPs(Vs, #countNils(P))) + + // syntax Pattern ::= #abstractNth(Pattern, Patterns, Int) [function] + // syntax Patterns ::= #abstractNthPs(Patterns, Patterns) [function] + // rule #abstractNth(\and(Ps), Vs) => \and(#abstractNthPs(Ps, Vs)) + // rule #abstractNth(\or(Ps), Vs) => \or(#abstractNthPs(Ps, Vs)) + // rule #abstractNth(\not(P), Vs) => \not(#abstractNth(P, Vs)) + // rule #abstractNth(sep(Ps), Vs) => sep(#abstractNthPs(Ps, Vs)) + // rule #abstractNth(S(ARGs), Vs) => + // => S(#replaceNewVariables(ARGs, Vs)) + // requires isUnfoldable(S) + // rule #abstractNth(pto(ARGs), Vs) => pto(ARGs) + // rule #abstractNth(\equals(L, R), Vs) => \equals(L, R) + + // rule #abstractNthPs(.Patterns, _) => .Patterns + // rule #abstractNthPs((P, Ps), Vs) => #abstractNth(P, Vs), #abstractNthPs(Ps, Vs) syntax Patterns ::= #replaceNewVariables(Patterns, Patterns) [function] rule #replaceNewVariables((V1:Variable, Ps), Vs) => V1, #replaceNewVariables(Ps, Vs) @@ -209,6 +268,50 @@ R(V, Vs) => exists V', R(V', Vs') and V = V' rule #createEqualities(VsLHS, (VRHS, VsRHS)) => \or(#createEqualitiesVar(VsLHS, VRHS)), #createEqualities(VsLHS, VsRHS) rule #createEqualitiesVar(.Patterns, VRHS) => .Patterns rule #createEqualitiesVar((VLHS, VsLHS), VRHS) => \equals(VRHS, VLHS), #createEqualitiesVar(VsLHS, VRHS) + + syntax Patterns ::= #createDisequalities(Pattern, Patterns) [function] + syntax Patterns ::= #createDisequalitiesPs(Patterns, Patterns) [function] + rule #createDisequalities(\and(Ps), Vs) => #createDisequalitiesPs(Ps, Vs) + rule #createDisequalities(\or(Ps), Vs) => #createDisequalitiesPs(Ps, Vs) + rule #createDisequalities(sep(Ps), Vs) => #createDisequalitiesPs(Ps, Vs) + rule #createDisequalities(S:Symbol(ARGs), Vs) => .Patterns + rule #createDisequalities(\equals(_, _), Vs) => .Patterns + rule #createDisequalities(\not(\equals(nil{_}(.Patterns), V:Variable)), Vs) => #makeDisequalities(V, Vs) + rule #createDisequalities(\not(\equals(V:Variable, nil{_}(.Patterns))), Vs) => #makeDisequalities(V, Vs) + rule #createDisequalities(\not(P), Vs) => .Patterns + [owise] + + rule #createDisequalitiesPs(.Patterns, _) => .Patterns + rule #createDisequalitiesPs((P, Ps), Vs) => #createDisequalities(P, Vs) ++Patterns #createDisequalitiesPs(Ps, Vs) + + syntax Patterns ::= #makeDisequalities(Variable, Patterns) [function] + rule #makeDisequalities(V, .Patterns) => .Patterns + rule #makeDisequalities(V1, (V2, Vs)) => \not(\equals(V1, V2)), #makeDisequalities(V1, Vs) +``` + +abstracting nil + +on the LHS, replace all occurrences of nil with a fresh variable + +```k + rule \implies(LHS, RHS) => \implies(#abstractNil(LHS), RHS) + abstract-nil => noop + ... + + + syntax Pattern ::= #abstractNil(Pattern) [function] + syntax Patterns ::= #abstractNilPs(Patterns) [function] + rule #abstractNil(V { SORT }) => V { SORT } + rule #abstractNil(\and(Ps)) => \and(#abstractNilPs(Ps)) + rule #abstractNil(\or(Ps)) => \or(#abstractNilPs(Ps)) + rule #abstractNil(\not(P)) => \not(#abstractNil(P)) + rule #abstractNil(sep(Ps)) => sep(#abstractNilPs(Ps)) + rule #abstractNil(nil { LOC }(.Patterns)) => !V:VariableName { LOC } + rule #abstractNil(S:Symbol(ARGs)) => S(#abstractNilPs(ARGs)) + requires nil { _ } :/=K S + rule #abstractNil(\equals(L, R)) => \equals(#abstractNil(L), #abstractNil(R)) + rule #abstractNilPs(.Patterns) => .Patterns + rule #abstractNilPs(P, Ps) => #abstractNil(P), #abstractNilPs(Ps) ``` ### lift-constraints @@ -216,47 +319,81 @@ 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))) - , \exists { _ } (\and(Rs) => #flattenAnd(#liftConstraints(\and(Rs)))) + rule \implies(\and(Ps) => #flattenAssoc(#liftConstraints(#flattenAssoc(\and(Ps)))) + , \exists { _ } (\and(Rs) => #flattenAssoc(#liftConstraints(#flattenAssoc(\and(Rs))))) ) - - lift-constraints => noop ... + + lift-constraints => noop ... syntax Pattern ::= #liftConstraints(Pattern) [function] - rule #liftConstraints(P) => P requires isPredicatePattern(P) - rule #liftConstraints(S) => sep(S) requires isSpatialPattern(S) - - rule #liftConstraints(sep(\and(.Patterns), REST)) => #liftConstraints(sep(REST)) - - rule #liftConstraints(sep(\and(P, Ps:Patterns), REST:Patterns)) - => #liftConstraints(\and(sep(\and(Ps), REST), P, .Patterns)) + syntax Patterns ::= #liftConstraintsPs(Patterns) [function] + // rule #liftConstraints(S:Symbol(\and(P1, P2, Ps), ARGs)) => #liftConstraints(\and(S(P1, ARGs), S(\and(P2, Ps), ARGs))) + // rule #liftConstraints(S:Symbol(\and(P, .Patterns), ARGs)) => #liftConstraints(\and(S(P, ARGs))) + rule #liftConstraints(\and(Ps)) => \and(#liftConstraintsPs(Ps)) + rule #liftConstraintsPs(.Patterns) => .Patterns + rule #liftConstraintsPs(sep(\and(.Patterns), .Patterns), REST) => #liftConstraintsPs(REST) + rule #liftConstraintsPs(P, REST) => #liftConstraintsPs(REST) ++Patterns P requires isPredicatePattern(P) - rule #liftConstraints(sep(\and(P, Ps), REST)) - => #liftConstraints(sep(\and(Ps), P, REST)) + rule #liftConstraintsPs(P, REST) => sep(P), #liftConstraintsPs(REST) requires isSpatialPattern(P) - rule #liftConstraints(sep(\and(P, Ps), REST)) - => #liftConstraints(sep(\and(#flattenAnds(#liftConstraints(P), Ps)), REST)) - requires notBool isPredicatePattern(P) andBool notBool isSpatialPattern(P) - - // Rotate - rule #liftConstraints(sep(S, Ps)) - => #liftConstraints(sep(Ps ++Patterns S)) - requires isSpatialPattern(S) andBool notBool isSpatialPattern(sep(S, Ps)) - - rule #liftConstraints(\and(sep(Ss), Ps)) - => #liftConstraints(\and(#flattenAnds(#liftConstraints(sep(Ss)), .Patterns) ++Patterns Ps)) - requires notBool isSpatialPattern(sep(Ss)) - - rule #liftConstraints(\and(S, Ps)) - => \and(sep(S), #flattenAnds(#liftConstraints(\and(Ps)), .Patterns)) - requires isSpatialPattern(S) - - rule #liftConstraints(\and(\and(Ps), REST)) - => #liftConstraints(\and(Ps ++Patterns REST)) + rule #liftConstraintsPs(V:SetVariable, REST) => V, #liftConstraintsPs(REST) + rule #liftConstraintsPs(\mu X . P, REST) => \mu X . P, #liftConstraintsPs(REST) + // TODO: should handle symbols the same as sep + rule #liftConstraintsPs(S:Symbol(ARGs), REST) => S(ARGs), #liftConstraintsPs(REST) + requires S =/=K sep + andBool notBool isSpatialPattern(S(ARGs)) + rule #liftConstraintsPs(\and(Ps), REST) => #liftConstraintsPs(Ps ++Patterns REST) + requires notBool isPredicatePattern(\and(Ps)) + // note the rule below assumes we hever have a pure predicate pattern inside a sep + rule #liftConstraintsPs(sep((P, Ps) #as SEPs), REST) + => #liftConstraintsPs( sep( (SEPs -Patterns #getSpatialPatterns(SEPs)) + ++Patterns #getSpatialPatterns(SEPs) + ) + , REST + ) + requires isSpatialPattern(P) andBool #getSpatialPatterns(SEPs) =/=K SEPs + rule #liftConstraintsPs(sep(\and(Ps), REST_SEP), REST) + => #liftConstraintsPs( sep( \and(Ps -Patterns #getPredicatePatterns(Ps)) + , REST_SEP + ) + , REST + ) + ++Patterns #getPredicatePatterns(Ps) + requires #getPredicatePatterns(Ps) =/=K .Patterns + rule #liftConstraintsPs(sep(\and(P, .Patterns), REST_SEP), REST) + => #liftConstraintsPs(sep(P, REST_SEP), REST) + requires isSpatialPattern(P) + rule #liftConstraintsPs(sep(\and(P, Ps), REST_SEP), REST) + => #liftConstraintsPs(sep(P, REST_SEP), sep(\and(Ps), REST_SEP), REST) + requires #getPredicatePatterns(P, Ps) ==K .Patterns + andBool isSpatialPattern(P) + andBool Ps =/=K .Patterns + rule #liftConstraintsPs(sep(\and(P, Ps), REST_SEP), REST) + => #liftConstraintsPs(sep(\and(#liftConstraintsPs(P, Ps)), REST_SEP), REST) + requires #getPredicatePatterns(P, Ps) ==K .Patterns + andBool notBool isSpatialPattern(P) + + syntax Patterns ::= #getPredicatePatterns(Patterns) [function] + syntax Patterns ::= #getSpatialPatterns(Patterns) [function] + rule #getPredicatePatterns(.Patterns) => .Patterns + rule #getPredicatePatterns(P, Ps) => P, #getPredicatePatterns(Ps) + requires isPredicatePattern(P) + rule #getPredicatePatterns(P, Ps) => #getPredicatePatterns(Ps) + requires notBool isPredicatePattern(P) + rule #getSpatialPatterns(.Patterns) => .Patterns + rule #getSpatialPatterns(P, Ps) => P, #getSpatialPatterns(Ps) + requires isSpatialPattern(P) + rule #getSpatialPatterns(P, Ps) => #getSpatialPatterns(Ps) + requires notBool isSpatialPattern(P) - rule #liftConstraints(\and(P, Ps)) - => #liftConstraints(\and(Ps ++Patterns P)) - requires isPredicatePattern(P) andBool notBool isPredicatePattern(\and(P, Ps)) + // test cases: + // \and(.Patterns) => \and(.Patterns) + // \and(sep(\and(.Patterns))) => \and(.Patterns) + // \and( dll(..), pto(..) ) => \and( sep( dll ), sep( pto ) ) + // \and(sep(\and(H1, P1, H2, P2))) + // => \and(sep(H1), sep(H2), P1, P2) + // \and(sep(\and(H1, H2, x=y), H3), H4, w=z) + // => \and(sep(H1, H3), sep(H2, H3), sep(H4), x=y, w=z) ``` ### lift-or @@ -270,8 +407,20 @@ 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(\and(\not(\and(Ps)), LHS), RHS) + => \implies(\and(\or(#not(Ps)), LHS), RHS) + + lift-or ... + rule \implies(\and(\or(Ps), LHS), RHS) + => \implies(\or(#liftOr-in-And(Ps, LHS)), RHS) + + lift-or ... + syntax Patterns ::= "#liftOr-in-And" "(" Patterns "," Patterns ")" [function] + rule #liftOr-in-And(.Patterns, LHS) => .Patterns + rule #liftOr-in-And((P, Ps), LHS) => \and(P, LHS), #liftOr-in-And(Ps, LHS) + + 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 +434,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 +443,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 +452,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,23 +465,47 @@ 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 ... +``` + +We define a similar strategy for quantified implication contexts: - rule (.Patterns ~> instantiate-existentials) => noop ... +```k + rule \implies( \and(sep(\forall { Vs } implicationContext(\and(LCTX), RCTX), _), LHS) , _ ) + (. => getAtomForcingInstantiation(LCTX, Vs)) + ~> instantiate-existentials-implication-context + ... + + rule \implies( \and( sep( \forall { Vs } implicationContext(\and(LCTX), RCTX), LSPATIAL), LHS) , RHS ) + => \implies( \and( sep( \forall { Vs -Patterns getFreeVariables(INSTANTIATION) } + implicationContext(\and(LCTX -Patterns INSTANTIATION), RCTX) + , LSPATIAL + ) + , (LHS ++Patterns INSTANTIATION) + ) + , RHS + ) + + (INSTANTIATION => .) ~> instantiate-existentials-implication-context ... + requires INSTANTIATION =/=K .Patterns + rule (.Patterns ~> instantiate-existentials-implication-context) => noop ... +``` +```k syntax Patterns ::= getAtomForcingInstantiation(Patterns, Patterns) [function] rule getAtomForcingInstantiation((\equals(X:Variable, P), Ps), EXISTENTIALS) => \equals(X:Variable, P), .Patterns @@ -357,34 +530,32 @@ Lift `\or`s on the left hand sides of implications ``` ```k - rule \implies(\and(LHS), _) - substitute-equals-for-equals - => (makeEqualitySubstitution(LHS) ~> substitute-equals-for-equals) - ... - + syntax Strategy ::= "substitute-equals-for-equals" "(" Map ")" + rule \implies(\and(LHS), _) + substitute-equals-for-equals + => substitute-equals-for-equals(makeEqualitySubstitution(LHS)) + ... + - rule (SUBST:Map ~> substitute-equals-for-equals) - => noop - ... - - requires SUBST ==K .Map + rule substitute-equals-for-equals(.Map) + => noop + ... + - rule \implies( \and(LHS => removeTrivialEqualities(substPatternsMap(LHS, SUBST))) - , \exists { _ } - ( \and(RHS => removeTrivialEqualities(substPatternsMap(RHS, SUBST))) ) - ) + rule \implies( LHS, \exists{Vs} RHS ) + => \implies( subst(LHS, X, T), \exists{Vs} subst(RHS, X, T) ) + + substitute-equals-for-equals((X |-> T):Map) + => substitute-equals-for-equals + ... - (SUBST:Map ~> substitute-equals-for-equals) - => substitute-equals-for-equals - ... - - requires SUBST =/=K .Map syntax Map ::= makeEqualitySubstitution(Patterns) [function] rule makeEqualitySubstitution(.Patterns) => .Map rule makeEqualitySubstitution(\equals(X:Variable, T), Ps) => (X |-> T) .Map + requires X =/=K T rule makeEqualitySubstitution(\equals(T, X:Variable), Ps) => (X |-> T) .Map - requires notBool(isVariable(T)) + requires notBool(isVariable(T)) andBool X =/=K T rule makeEqualitySubstitution((P, Ps:Patterns)) => makeEqualitySubstitution(Ps) [owise] syntax Patterns ::= removeTrivialEqualities(Patterns) [function] @@ -393,7 +564,6 @@ Lift `\or`s on the left hand sides of implications rule removeTrivialEqualities(P, Ps) => P, removeTrivialEqualities(Ps) [owise] ``` - ### Universal generalization ``` @@ -404,8 +574,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 +593,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 +662,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 +808,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) @@ -696,6 +866,21 @@ Gamma |- C[\exists X. Pi /\ Psi] ``` +### Remove constraints + +``` + PHI /\ C => PSI + ----------------- where C is a predicate pattern + PHI -> PSI +``` + +```k + rule \implies(\and(LHS), RHS) + => \implies(\and(LHS -Patterns getPredicatePatterns(LHS)), RHS) + + remove-constraints => noop ... +``` + ```k endmodule ``` diff --git a/prover/strategies/smt.md b/prover/strategies/smt.md index bfb84e10a..beaa2b86a 100644 --- a/prover/strategies/smt.md +++ b/prover/strategies/smt.md @@ -198,51 +198,58 @@ 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(LHS), _) GId - check-lhs-constraint-unsat - => if CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(LCONSTRAINTS), collectDeclarations(GId))) ==K unsat + check-lhs-constraint-unsat + => if CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(getPredicatePatterns(LHS)), collectDeclarations(GId))) ==K unsat then success else noop fi ... - + .K => check-lhs-constraint-unsat ... - requires isPredicatePattern(\and(LCONSTRAINTS)) +// If the constraints are unsatisfiable, the entire term is unsatisfiable + rule \implies(\and(LHS), _) + GId + check-lhs-constraint-unsat-debug + => wait ~> CVC4CheckSAT(CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(getPredicatePatterns(LHS)), collectDeclarations(GId))) + ... + + .K => check-lhs-constraint-unsat-debug ~> CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(getPredicatePatterns(LHS)), collectDeclarations(GId)) ... ``` 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 +261,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 +295,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..fa65ded06 100644 --- a/prover/strategies/unfolding.md +++ b/prover/strategies/unfolding.md @@ -12,6 +12,8 @@ module STRATEGY-UNFOLDING rule [[ unfold(S:Symbol(ARGs)) => {("ifflfp axiom has free variables!" ~> S ~> (getFreeVariables(DEF) -Patterns Vs))}:>Pattern ]] axiom _: \forall { Vs } \iff-lfp(S(Vs), DEF) requires getFreeVariables(DEF) -Patterns Vs =/=K .Patterns + rule unfold(\mu X . P) => subst(P, X, alphaRename(\mu X . P)) + rule unfold(\nu X . P) => subst(P, X, alphaRename(\nu X . P)) syntax SymbolDeclaration ::= getSymbolDeclaration(Symbol) [function] rule [[ getSymbolDeclaration(S) => DECL ]] @@ -30,6 +32,10 @@ module STRATEGY-UNFOLDING => R(ARGS), (getUnfoldables(ARGS) ++Patterns getUnfoldables(REST)) requires isUnfoldable(R) + rule getUnfoldables(\mu X . P, REST) + => \mu X . P, getUnfoldables(REST) + rule getUnfoldables(\nu X . P, REST) + => \nu X . P, getUnfoldables(REST) rule getUnfoldables(S:Symbol, REST) => getUnfoldables(REST) requires notBool isUnfoldable(S) @@ -41,6 +47,8 @@ module STRATEGY-UNFOLDING => getUnfoldables(REST) rule getUnfoldables(V:Variable, REST) => getUnfoldables(REST) + rule getUnfoldables(X:SetVariable, REST) + => getUnfoldables(REST) rule getUnfoldables(\not(Ps), REST) => getUnfoldables(Ps) ++Patterns getUnfoldables(REST) rule getUnfoldables(\and(Ps), REST) @@ -69,32 +77,23 @@ 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) - => \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))) ) - , _ - ) - , RHS - ) - - left-unfold-oneBody(LRP, \exists { _ } \and(BODY)) => noop ... +// TODO: left-unfold should take a context as a parameter as well in the future + rule \implies(LHS, RHS) + => \implies(subst(LHS, LRP, \and(BODY)), RHS) + + left-unfold-oneBody(LRP, \exists { _ } \and(BODY)) => noop ... .K => left-unfold-oneBody(LRP, \and(BODY)) ... - requires LRP in LHS + requires #hole { TopSort } in getFreeVariables(subst(LHS, LRP, #hole { TopSort })) ``` ### Left Unfold Nth @@ -107,28 +106,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,66 +141,66 @@ 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 ) + . ( ( noop ) | ( right-unfold(P) . right-unfold(symbols: P, Ps, bound: N -Int 1) ) | ( 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 +221,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))) @@ -235,20 +234,20 @@ rule addPattern(P, ListItem(Ps:Patterns) L) => ListItem(P, Ps) addPattern(P, L) requires notBool hasImplicationContext(LHS) syntax Pattern ::= #moveHoleToFront(Pattern) [function] - rule #moveHoleToFront(\and(sep(#hole, REST_SEP), REST_AND)) => \and(sep(#hole, REST_SEP), REST_AND) + rule #moveHoleToFront(\and(sep(#hole { Heap }, REST_SEP), REST_AND)) => \and(sep(#hole { Heap }, REST_SEP), REST_AND) rule #moveHoleToFront(\and(sep(P, REST_SEP), REST_AND)) => #moveHoleToFront(\and(sep(REST_SEP ++Patterns P), REST_AND)) - requires P =/=K #hole:Variable + requires P =/=K #hole { Heap } // right unfolding within an implication context - rule \implies(\and( sep ( \forall { UNIVs => UNIVs ++Patterns E2 } - implicationContext( ( \and( sep( #hole + rule \implies(\and( sep ( \forall { UNIVs => UNIVs ++Patterns E2 } + implicationContext( ( \and( sep( #hole { Heap } , CTXLHS ) , CTXLCONSTRAINTS ) ) - => #moveHoleToFront(#flattenAnd( - #liftConstraints( \and( sep( #hole + => #moveHoleToFront(#flattenAssoc( + #liftConstraints( \and( sep( #hole { Heap } , substPatternsMap(CTXLHS, zip((RRP, .Patterns), (\and(BODY), .Patterns))) ) , CTXLCONSTRAINTS @@ -263,8 +262,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 +283,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 ... - requires (M 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/apply-equation.kore.expected b/prover/t/apply-equation.kore.expected new file mode 100644 index 000000000..e69de29bb diff --git a/prover/t/apply.kore b/prover/t/apply.kore deleted file mode 100644 index 394983dcf..000000000 --- a/prover/t/apply.kore +++ /dev/null @@ -1,15 +0,0 @@ -symbol foo() : Bool -symbol goo() : Bool -symbol bar() : Bool - -axiom foo_holds: foo() -axiom goo_holds: goo() -axiom foo_and_goo_implies_bar: - \implies(foo(), \implies(goo(), bar())) - -claim bar() -strategy - apply( - foo_and_goo_implies_bar, - apply(foo_holds, fail) | apply(goo_holds, fail) - ) diff --git a/prover/t/duplicate.kore.expected b/prover/t/duplicate.kore.expected new file mode 100644 index 000000000..e69de29bb diff --git a/prover/t/inst-exists.kore b/prover/t/inst-exists.kore deleted file mode 100644 index b59ad874b..000000000 --- a/prover/t/inst-exists.kore +++ /dev/null @@ -1,5 +0,0 @@ -axiom f5: \functionalPattern(5) - -claim \exists{I{Int}} gte(I{Int}, 3) -strategy inst-exists(I{Int}, 5, apply(f5, fail)) - . smt-cvc4 diff --git a/prover/t/instantiate-universals.kore.expected b/prover/t/instantiate-universals.kore.expected new file mode 100644 index 000000000..e69de29bb diff --git a/prover/t/ltl/always-propagates.kore b/prover/t/ltl/always-propagates.kore new file mode 100644 index 000000000..bd4c99217 --- /dev/null +++ b/prover/t/ltl/always-propagates.kore @@ -0,0 +1,19 @@ +symbol next(TopSort) : TopSort + +// there is always a next state +axiom inf: next(\top()) + +// one-path next implies all-path next +axiom lin: \implies(next(#X), \not(next(\not(#X)))) + +// IND: phi /\ [](phi -> next(phi)) -> []phi +claim \implies( \and( \nu #X . \or(\exists { } \and(#PHI1, next(#X))) + , \nu #Y . \or(\exists { } \and(\implies(#PHI1, #PHI2), next(#Y))) + ) + , \nu #Z . \or(\exists { } \and(#PHI2, next(#Z))) + ) + +strategy gfp . normalize . left-unfold-Nth(1) . normalize . lift-or . and-split . normalize + . ( ( left-unfold-Nth(0) . normalize . contradiction ) + | ( left-unfold-Nth(0) . normalize . patterns-equal . rhs-top ) + ) diff --git a/prover/t/ltl/always-propagates.kore.expected b/prover/t/ltl/always-propagates.kore.expected new file mode 100644 index 000000000..8b1378917 --- /dev/null +++ b/prover/t/ltl/always-propagates.kore.expected @@ -0,0 +1 @@ + diff --git a/prover/t/ltl/ind.kore b/prover/t/ltl/ind.kore new file mode 100644 index 000000000..3e35dbfc4 --- /dev/null +++ b/prover/t/ltl/ind.kore @@ -0,0 +1,19 @@ +symbol next(TopSort) : TopSort + +// there is always a next state +axiom inf: next(\top()) + +// one-path next implies all-path next +axiom lin: \implies(next(#X), \not(next(\not(#X)))) + +// IND: phi /\ [](phi -> next(phi)) -> []phi +claim \implies( \and( #PHI + , \nu #X . \or(\exists { } \and(\implies(#PHI, next(#PHI)), next(#X))) + ) + , \nu #Y . \or(\exists { } \and(#PHI, next(#Y))) + ) + +strategy gfp . normalize . left-unfold-Nth(0) . normalize . lift-or . and-split . normalize + . ( ( contradiction ) + | ( patterns-equal . rhs-top ) + ) diff --git a/prover/t/ltl/until-implies-eventually.kore b/prover/t/ltl/until-implies-eventually.kore new file mode 100644 index 000000000..818b2f2b9 --- /dev/null +++ b/prover/t/ltl/until-implies-eventually.kore @@ -0,0 +1,42 @@ +symbol next(TopSort) : TopSort + +// there is always a next state +axiom inf: next(\top()) + +// one-path next implies all-path next +axiom lin: \implies(next(#X), \not(next(\not(#X)))) + +// phi1 U phi2 => []phi2 +claim \implies( \mu #X . \or(\exists { } \and(#PHI2), \exists { } \and(#PHI1, next(#X))) + , \mu #X . \or(\exists { } \and(#PHI2), \exists { } \and(next(#X))) + ) + +/* +kt: \implies( \or(PHI2, \and(PHI1, next(\mu #Y . \or(PHI2, next(#Y)))) + , \mu #X . \or(PHI2, next(#X)) + ) + +lift-or, and-spplit +(1) \implies( PHI2 , \mu #X . \or(PHI2, next(#X)) ) +right-unfold-Nth(0, 0) + \implies( PHI2 , PHI2 ) +phi-implies-phi + success + +(2) \implies( next(\mu #Y . \or(PHI2, next(#Y))) + , \mu #X . \or(PHI2, next(#X)) + ) +right-unfold-Nth(0, 1) + \implies( next(\mu #Y . \or(PHI2, next(#Y))) + , next(\mu #X . \or(PHI2, next(#X))) + ) +"alpha-rename" + \implies( next(\mu #Y . \or(PHI2, next(#Y))) + , next(\mu #Y . \or(PHI2, next(#Y))) + ) +phi-implies-phi +*/ + +strategy normalize . kt . ( ( right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top ) + | ( right-unfold-Nth(0, 1) . normalize . lift-constraints . patterns-equal . rhs-top ) + ) diff --git a/prover/t/replace-evar-with-func-constant.kore.expected b/prover/t/replace-evar-with-func-constant.kore.expected new file mode 100644 index 000000000..e69de29bb diff --git a/prover/t/unit/dnf.k b/prover/t/unit/dnf.k new file mode 100644 index 000000000..f6532d91e --- /dev/null +++ b/prover/t/unit/dnf.k @@ -0,0 +1,81 @@ +module TEST-DNF + imports UNIT-TEST + imports KORE-HELPERS + + syntax LowerName ::= "c" [token] + | "f" [token] + + syntax SharpName ::= "#X0" [token] + | "#PHI1" [token] | "#PHI2" [token] + + rule test("dnf", 0) + => assert( \or(\and(.Patterns)) + == #nnf(\not(\and(\or(.Patterns)))) + ) + .Declarations + rule test("dnf", 1) + => assert( \and(\or(\not(c(f, f)), \or(c, f))) + == #nnf(\not(\or(\and(c(f, f), \not(\or(c, f)))))) + ) + .Declarations + + rule test("dnf", 2) + => assert( \or(\and(.Patterns)) + == #dnf(\not(\and(\or(.Patterns)))) + ) + .Declarations + rule test("dnf", 3) + => assert( \or(\and(\not(c(f, f))), \and(c), \and(f)) + == #dnf(\not(\or(\and(c(f, f), \not(\or(c, f)))))) + ) + .Declarations + + rule test("dnf", 4) + => assert( \or(\and((c(f, f)), \not(c), \not(f))) + == #dnf(\or(\and(\and(c(\or(f), \and(\and(f))), \not(\or(c, f)))))) + ) + .Declarations + + rule test("dnf", 5) + => assert( \or(\and(f)) == #dnf(\or(f))) + .Declarations + + rule test("dnf", 6) + => assert( \or(\and(sep(f), sep(c))) + == #dnf(\or(sep(\and(f, c)))) + ) + .Declarations + +// sep(\and(sep(H), \equals(x, y))) +// => \and(sep(H), sep(\equal(x, y))) + + rule test("dnf", 7) + => assert( \or(\and(sep(f), sep(\equals(1, 2)))) + == #dnf(\or(sep(\and(f, \equals(1, 2))))) + ) + .Declarations + + rule test("dnf", 8) + => assert( \or(\and(c(\mu #X0 . \or(\and(#PHI2), \and(c(#X0)))), #PHI1)) + == #dnf(\and(c(\and(\mu #X0 . \or(\and(#PHI2), \and(c(#X0))))), #PHI1)) + ) + .Declarations + + rule test("dnf", 9) + => assert( \or(\and(c(#PHI1), c(#PHI2))) + == #dnf(\and(c(\and(#PHI1, #PHI2)))) + ) + .Declarations + + rule test("dnf", 10) + => assert( \or(\and(c(\and(.Patterns)))) + == #dnf(c(\and(.Patterns))) + ) + .Declarations + +// rule test("dnf", 4) +// => assert( +// == #flattenAnds(\and(\and(\or(\and(\and(\not(c(f, \and(\and(f)))))), \and(c), \and(f))))) +// ) +// .Declarations +endmodule diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k index 2ecba9bed..b1cf226d5 100644 --- a/prover/t/unit/match-assoc-comm.k +++ b/prover/t/unit/match-assoc-comm.k @@ -1,15 +1,17 @@ module TEST-MATCH-ASSOC-COMM imports UNIT-TEST - syntax LowerName ::= "c" [token] - | "d" [token] - syntax UpperName ::= "Data" [token] - | "Loc" [token] - | "W" [token] | "W1" [token] | "W2" [token] - | "X0" [token] | "X1" [token] | "X2" [token] - | "Y0" [token] | "Y1" [token] | "Y2" [token] - | "Z" [token] | "Z1" [token] | "Z2" [token] - | "H0" [token] + syntax LowerName ::= "c" [token] | "d" [token] + | "heap1" [token] | "heap2" [token] + syntax UpperName ::= "Data" [token] + | "Loc" [token] + | "W" [token] | "W0" [token] | "W1" [token] | "W2" [token] + | "X0" [token] | "X1" [token] | "X2" [token] + | "Y0" [token] | "Y1" [token] | "Y2" [token] + | "Z" [token] | "Z1" [token] | "Z2" [token] + | "H0" [token] | "H1" [token] + syntax SharpName ::= "#X0" [token] | "#X1" [token] + | "#PHI1" [token] rule test("match-assoc-comm", 1) => assert( #matchResult( subst: .Map , rest: pto( Z { Loc }, W { Data })) @@ -133,4 +135,171 @@ module TEST-MATCH-ASSOC-COMM ) ) .Declarations + + // Matching within a conjunction of multiple seps + // rule test("match-assoc-comm", 7) + // => assert( #error( "No valid substitution" ) + // , #matchResult( subst: X0 { Loc } |-> W0 { Loc } + // Y0 { Loc } |-> Z0 { Loc } + // X1 { Loc } |-> W1 { Loc } + // Y1 { Loc } |-> Z1 { Loc } + // H0 { Heap } |-> heap1 + // H1 { Heap } |-> heap2 + // , rest: .Patterns + // ) + // , #matchResult( subst: X0 { Loc } |-> W1 { Loc } + // Y0 { Loc } |-> Z1 { Loc } + // X1 { Loc } |-> W0 { Loc } + // Y1 { Loc } |-> Z0 { Loc } + // H0 { Heap } |-> heap2 + // H1 { Heap } |-> heap1 + // , rest: .Patterns + // ) + // , .MatchResults + // == #matchAssocComm( terms: \and( sep( pto ( W0 { Loc } , Z0 { Data } ), heap1 ) + // , sep( pto ( W1 { Loc } , Z1 { Data } ), heap2 ) + // , pattern: \and( sep( pto ( X0 { Loc } , Y0 { Data } ), H0 { Heap } ) + // , sep( pto ( X1 { Loc } , Y1 { Data } ), H1 { Heap } ) + // , variables: X0 { Loc }, Y0 { DATA }, H0 { Heap } + // , X1 { Loc }, Y1 { DATA }, H1 { Heap } + // , results: .MatchResults + // , subst: .Map + // , rest: .Patterns + // ) + // ) + // .Declarations + + rule test("match-assoc-comm", 9) + => assert( #matchResult( subst: Y2 { Data } |-> Y1 { Data } + H1 { Heap } |-> sep( pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) ), H0 { Heap } ) + , rest: .Patterns + ) + , .MatchResults + == #filterErrors( #matchAssocComm( terms: H0 { Heap } + , pto ( X1 { Loc } , Y1 { Data } ) + , pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) ) + , pattern: pto ( X1 { Loc } , Y2 { Data } ) + , H1 { Heap } + , variables: Y2 { Data } + , H1 { Heap } + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + ) + .Declarations + + rule test("match-assoc-comm", 10) + => assert( #error( "Heap variable must be at end of pattern" ) + , .MatchResults + == #matchAssocComm( terms: H0 { Heap } + , pto ( X1 { Loc } , Y1 { Data } ) + , pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) ) + , pattern: H1 { Heap } + , pto ( X1 { Loc } , Y2 { Data } ) + , variables: Y2 { Data } + , H1 { Heap } + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations + + // Matching on a symbolic heap + rule test("match-assoc-comm", 11) + => assert( #matchResult( subst: H0 { Heap } |-> pto ( X1 { Loc } , Y1 { Data } ) + W { Loc } |-> X2 { Loc } + Z { Data } |-> Y2 { Data } + , rest: .Patterns + ) + , #matchResult( subst: H0 { Heap } |-> pto ( X2 { Loc } , Y2 { Data } ) + W { Loc } |-> X1 { Loc } + Z { Data } |-> Y1 { Data } + , rest: .Patterns + ) + , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns ) + W { Loc } |-> X1 { Loc } + Z { Data } |-> Y1 { Data } + , rest: pto ( X2 { Loc } , Y2 { Data } ) + ) + , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns ) + W { Loc } |-> X1 { Loc } + Z { Data } |-> Y1 { Data } + , rest: pto ( X1 { Loc } , Y1 { Data } ) + ) + , .MatchResults + == #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } ) + , pto ( X2 { Loc } , Y2 { Data } ) + , pattern: H0 { Heap } + , pto ( W { Loc } , Z { Data } ) + , variables: H0 { Heap }, W { Loc }, Z { Data } + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations + + // Matching on a symbolic heap + rule test("match-assoc-comm", 12) + => assert( #matchResult( subst: H0 { Heap } |-> pto ( X1 { Loc } , Y1 { Data } ) + W { Loc } |-> X2 { Loc } + Z { Data } |-> Y2 { Data } + , rest: .Patterns + ) + , #matchResult( subst: H0 { Heap } |-> pto ( X2 { Loc } , Y2 { Data } ) + W { Loc } |-> X1 { Loc } + Z { Data } |-> Y1 { Data } + , rest: .Patterns + ) + , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns ) + W { Loc } |-> X1 { Loc } + Z { Data } |-> Y1 { Data } + , rest: pto ( X2 { Loc } , Y2 { Data } ) + ) + , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns ) + W { Loc } |-> X1 { Loc } + Z { Data } |-> Y1 { Data } + , rest: pto ( X1 { Loc } , Y1 { Data } ) + ) + , .MatchResults + == #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } ) + , pto ( X2 { Loc } , Y2 { Data } ) + , pattern: H0 { Heap } + , pto ( W { Loc } , Z { Data } ) + , variables: H0 { Heap }, W { Loc }, Z { Data } + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations + + rule test("match-assoc-comm", 13) + => assert( #error( "???" ), .MatchResults + == #match( terms: \and(sep( pto ( Y0 { Loc } , c ( Z { Loc })) + , pto ( X0 { Loc } , c ( Y0 { Loc })) + ) ) + , pattern: pto ( X0 { Loc } , c ( W0 { Loc })) + , pto ( W0 { Loc } , c ( Z { Loc })) + , variables: W0 { Loc } + ) + ) + .Declarations + + // matching on mu terms with different binders + rule test("match-assoc-comm", 14) + => assert( #matchResult( subst: .Map , rest: .Patterns ) + , .MatchResults + == #matchAssocComm( terms: \mu #X0 . \and(#X0, #PHI1) + , pattern: \mu #X1 . \and(#X1, #PHI1) + , variables: .Patterns + , results: .MatchResults + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations endmodule diff --git a/prover/t/unit/match-assoc.k b/prover/t/unit/match-assoc.k index 6696afbb9..b00e7453f 100644 --- a/prover/t/unit/match-assoc.k +++ b/prover/t/unit/match-assoc.k @@ -110,6 +110,7 @@ module TEST-MATCH-ASSOC // Match constructor against variable rule test("match-assoc", 9) => symbol pto ( Loc, Data ) : Heap + symbol c ( Data ) : Data assert( #error("Constructors do not match") , .MatchResults == #matchAssoc( terms: X0 { Loc }, Y0 { Data } @@ -120,4 +121,20 @@ module TEST-MATCH-ASSOC ) ) .Declarations + + // Match multiple occurances of a variable + rule test("match-assoc", 10) + => symbol c ( Data ) : Data + assert( #matchResult( subst: X0 { Data } |-> c( #hole { Data } ) + , rest: .Patterns + ) + , .MatchResults + == #matchAssoc( terms: c( W { Data } ) + , pattern: X0[W { Data }] + , variables: X0 { Data } + , subst: .Map + , rest: .Patterns + ) + ) + .Declarations endmodule diff --git a/prover/t/unit/unit-tests b/prover/t/unit/unit-tests index 6ef3c9895..70b29e88f 100644 --- a/prover/t/unit/unit-tests +++ b/prover/t/unit/unit-tests @@ -10,4 +10,6 @@ suite "syntactic-match" suite "visitor" +suite "dnf" + .Declarations diff --git a/prover/utils/load-named.md b/prover/utils/load-named.md index f3c9d9a9b..507b6cef9 100644 --- a/prover/utils/load-named.md +++ b/prover/utils/load-named.md @@ -10,19 +10,19 @@ module LOAD-NAMED-RULES imports LOAD-NAMED-SYNTAX imports PROVER-CORE - rule loadNamed(Name) => P ... + rule loadNamed(Name) => P ... ... Name - P - success + P + success ... - rule loadNamed(Name) => P ... + rule loadNamed(Name) => P ... axiom Name : P - rule loadNamed(Name) => P ... + rule loadNamed(Name) => P ... axiom Name : P endmodule