Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use a list of <goal>s instead of a set #59

Merged
merged 4 commits into from
Apr 29, 2020
Merged

Use a list of <goal>s instead of a set #59

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a53bd4a
drivers/base: Merge <claim> and <k> cells
nishantjr Apr 14, 2020
514da68
drivers: Initial goal is now populated via `subgoal` strategy
nishantjr Apr 15, 2020
1e4a72c
configuration: Replace Set of <goal>s with list. Only first goal is a…
nishantjr Apr 20, 2020
d62cc11
Add qf_shid_entl/ls_nonrec_entail_ls_14 to passing list (takes 220 m…
nishantjr Apr 24, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 19 additions & 12 deletions prover/drivers/base.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
Configuration
=============

The configuration consists of a assoc-commutative bag of goals. Only goals
marked `<active>` are executed to control the non-determinism in the system. The
`<claim>` cell contains the Matching Logic Pattern for which we are searching for a
proof. The `<strategy>` cell contains an imperative language that controls which
(high-level) proof rules are used to complete the goal. The `<trace>` 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 object.
The configuration consists of a list of goals. The first goal is considered
active. The `<k>` cell contains the Matching Logic Pattern for which we are
searching for a proof. The `<strategy>` cell contains an imperative language
that controls which (high-level) proof rules are used to complete the goal. The
`<trace>` 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
object.

```k
module PROVER-CONFIGURATION
Expand All @@ -21,20 +21,17 @@ module PROVER-CONFIGURATION

configuration
<prover>
<k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>
<exit-code exit=""> 1 </exit-code>
<goals>
<goal multiplicity="*" type="Set" format="%1%i%n%2, %3, %4%n%5%n%6%n%7%n%8%n%d%9">
<active format="active: %2"> true:Bool </active>
<goal multiplicity="*" type="List" format="%1%i%n%2, %3%n%4%n%5n%6%n%7%n%d%8">
<id format="id: %2"> .K </id>
<parent format="parent: %2"> .K </parent>
<claim> .K </claim>
<k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>
<strategy> .K </strategy>
<expected> .K </expected>
<local-context>
<local-decl multiplicity="*" type="Set"> .K </local-decl>
</local-context>

<trace> .K </trace>
</goal>
</goals>
Expand Down Expand Up @@ -89,6 +86,16 @@ module DRIVER-BASE
imports LOAD-NAMED-RULES

rule <k> .CommandLine => .K ... </k>

rule <goals>
<goal>
<id> .K </id>
<expected> .K </expected>
<strategy> .K </strategy>
...
</goal>
</goals>
<exit-code> 1 => 0 </exit-code>
endmodule

module DRIVER-BASE-SYNTAX
Expand Down
25 changes: 1 addition & 24 deletions prover/drivers/kore-driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,34 +66,11 @@ in the subgoal and the claim of the named goal remains intact.
=> claim getFreshClaimName() : PATTERN strategy STRAT
...
</k>

rule <k> claim NAME : PATTERN
strategy STRAT
=> .K
=> subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT))
...
</k>
<goals>
( .Bag =>
<goal>
<id> NAME </id>
<active> true:Bool </active>
<parent> .K </parent>
<claim> PATTERN </claim>
<strategy> subgoal(PATTERN, STRAT) </strategy>
<expected> success </expected>
<local-context> .Bag </local-context>
<trace> .K </trace>
</goal>
)
...
</goals>
```

```k
rule <id> _:ClaimName </id>
<expected> S:TerminalStrategy </expected>
<strategy> S </strategy>
<exit-code> 1 => 0 </exit-code>
```

```k
Expand Down
33 changes: 15 additions & 18 deletions prover/drivers/smt-driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -318,24 +318,21 @@ module DRIVER-SMT
rule #containsSpatialPatterns(.Patterns, _) => false
rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S)

rule <k> #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
~> (check-sat)
=> #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
...
</k>
<goals>
( .Bag =>
<goal>
<id> !N:ClaimName </id>
<active> true:Bool </active>
<parent> .K </parent>
<claim> \implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) </claim>
<strategy> STRAT </strategy>
<expected> EXPECTED </expected>
<local-context> .Bag </local-context>
<trace> .K </trace>
</goal>
)
syntax KItem ::= "expect" TerminalStrategy
rule <strategy> S ~> expect S => .K ... </strategy>

rule <goals>
<k> #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
~> (check-sat)
=> #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
...
</k>
<strategy> .K
=> subgoal(\implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
, STRAT
)
~> expect EXPECTED
</strategy>
...
</goals>
requires notBool PATTERN ==K \exists { .Patterns } \and ( .Patterns )
Expand Down
1 change: 1 addition & 0 deletions prover/lib/testlists.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ def read_list(file):
, ('unfold-mut-recs . ', 10, 16, '20m', ['t/SL-COMP18/bench/qf_shid_entl/ls_nonrec_entail_ls_11.sb.smt2'])
, ('unfold-mut-recs . ', 6, 16, '10m', ['t/SL-COMP18/bench/qf_shid_entl/ls_nonrec_entail_ls_12.sb.smt2'])
, ('unfold-mut-recs . ', 12, 18, '75m', ['t/SL-COMP18/bench/qf_shid_entl/ls_nonrec_entail_ls_13.sb.smt2'])
, ('unfold-mut-recs . ', 14, 21,'220m', ['t/SL-COMP18/bench/qf_shid_entl/ls_nonrec_entail_ls_14.sb.smt2'])
## these 3 tests should go through with this strategy, but they will need a very high
## time bound (>60m)
# , ('unfold-mut-recs . ', 14, 20, '60m', ['t/SL-COMP18/bench/qf_shid_entl/ls_nonrec_entail_ls_14.sb.smt2'])
Expand Down
6 changes: 3 additions & 3 deletions prover/strategies/apply-equation.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ module STRATEGY-APPLY-EQUATION
)
...
</strategy>
<claim> T </claim>
<k> T </k>

syntax KItem ::= "#apply-equation3"
"(" "hypothesis:" Pattern
Expand All @@ -138,9 +138,9 @@ module STRATEGY-APPLY-EQUATION
=> instantiateAssumptions(Subst, P)
~> createSubgoalsWithStrategies(strats: Ss, result: noop)
...</strategy>
<claim>
<k>
_ => cool(heated: Heated, term: substMap(R, Subst))
</claim>
</k>

syntax KItem ::= "createSubgoalsWithStrategies"
"(" "strats:" Strategies
Expand Down
2 changes: 1 addition & 1 deletion prover/strategies/apply.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ module STRATEGY-APPLY
Strat
)
...</strategy>
<claim> G </claim>
<k> G </k>


syntax KItem ::= #apply1(Pattern, MatchResult, Strategy)
Expand Down
39 changes: 19 additions & 20 deletions prover/strategies/core.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,18 +89,16 @@ completed, its result is replaced in the parent goal and the subgoal is removed.
```k
syntax Strategy ::= goalStrat(GoalId)
rule <prover>
<goal> <id> PID </id>
<active> _ => true </active>
<strategy> goalStrat(ID) => RStrat ... </strategy>
...
</goal>
( <goal> <id> ID </id>
<active> true:Bool </active>
<parent> PID </parent>
<strategy> RStrat:TerminalStrategy </strategy>
...
</goal> => .Bag
)
<goal> <id> PID </id>
<strategy> goalStrat(ID) => RStrat ... </strategy>
...
</goal>
...
</prover>
```
Expand All @@ -109,23 +107,24 @@ Proving a goal may involve proving other subgoals:

```k
syntax Strategy ::= "subgoal" "(" Pattern "," Strategy ")"
rule <strategy> subgoal(GOAL, STRAT) => subgoal(!ID:Int, GOAL, STRAT) ... </strategy>
syntax Strategy ::= "subgoal" "(" GoalId "," Pattern "," Strategy ")"
rule <prover>
( .Bag =>
<goal>
<id> !ID:Int </id>
<active> true </active>
<id> ID:Int </id>
<parent> PARENT </parent>
<strategy> SUBSTRAT </strategy>
<claim> SUBGOAL </claim>
<k> SUBGOAL </k>
<local-context> LC </local-context>
<trace> TRACE </trace>
...
</goal>
)
<goal>
<id> PARENT </id>
<active> true => false </active>
<strategy> subgoal(SUBGOAL, SUBSTRAT) => goalStrat(!ID:Int) ... </strategy>
<strategy> subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID:Int) ... </strategy>
<local-context> LC::Bag </local-context>
<trace> TRACE </trace>
...
Expand All @@ -151,7 +150,7 @@ all succeed, it succeeds:
rule <prover>
<goal>
<strategy> ((S1 & S2) => subgoal(GOAL, S1) ~> #hole & S2) </strategy>
<claim> GOAL:Pattern </claim>
<k> GOAL:Pattern </k>
...
</goal>
...
Expand All @@ -177,7 +176,7 @@ approach succeeds:
rule <prover>
<goal>
<strategy> ((S1 | S2) => subgoal(GOAL, S1) ~> #hole | S2 ) </strategy>
<claim> GOAL:Pattern </claim>
<k> GOAL:Pattern </k>
...
</goal>
...
Expand All @@ -199,7 +198,7 @@ Internal strategy used to implement `or-split` and `and-split`.

```k
syntax Strategy ::= "replace-goal" "(" Pattern ")"
rule <claim> _ => NEWGOAL </claim>
rule <k> _ => NEWGOAL </k>
<strategy> replace-goal(NEWGOAL) => noop ... </strategy>
```

Expand All @@ -212,7 +211,7 @@ Internal strategy used to implement `or-split` and `and-split`.
```

```k
rule <claim> \or(GOALS) </claim>
rule <k> \or(GOALS) </k>
<strategy> or-split => #orSplit(GOALS) ... </strategy>
syntax Strategy ::= "#orSplit" "(" Patterns ")" [function]
Expand All @@ -230,16 +229,16 @@ Internal strategy used to implement `or-split` and `and-split`.
```

```k
rule <claim> \implies(LHS, \exists { Vs } \and(\or(RHSs), REST)) </claim>
rule <k> \implies(LHS, \exists { Vs } \and(\or(RHSs), REST)) </k>
<strategy> or-split-rhs => #orSplitImplication(LHS, Vs, RHSs, REST) ... </strategy>
rule <claim> \implies(LHS, \exists { Vs } \and(RHSs, REST)) </claim>
rule <k> \implies(LHS, \exists { Vs } \and(RHSs, REST)) </k>
<strategy> or-split-rhs => noop ... </strategy>
requires notBool isDisjunction(RHSs)
rule <claim> \implies(LHS, \exists { Vs } \and(.Patterns)) </claim>
rule <k> \implies(LHS, \exists { Vs } \and(.Patterns)) </k>
<strategy> or-split-rhs => noop ... </strategy>
rule <claim> \implies(LHS, \exists { Vs } \and(.Patterns)) </claim>
rule <k> \implies(LHS, \exists { Vs } \and(.Patterns)) </k>
<strategy> or-split-rhs => noop ... </strategy>
syntax Strategy ::= "#orSplitImplication" "(" Pattern "," Patterns "," Patterns "," Patterns ")" [function]
Expand All @@ -257,7 +256,7 @@ Internal strategy used to implement `or-split` and `and-split`.
```

```k
rule <claim> \and(GOALS) </claim>
rule <k> \and(GOALS) </k>
<strategy> and-split => #andSplit(GOALS) ... </strategy>
syntax Strategy ::= "#andSplit" "(" Patterns ")" [function]
Expand Down
4 changes: 2 additions & 2 deletions prover/strategies/inst-exists.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@ module STRATEGY-INST-EXISTS
inst-exists(V, T, Strat)
=> subgoal(\functionalPattern(T), Strat) & noop
...</strategy>
<claim>
<k>
P => instExists(P, V, T)
</claim>
</k>
syntax Pattern ::= instExists(Pattern, Variable, Pattern) [function]
Expand Down
2 changes: 1 addition & 1 deletion prover/strategies/intros.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ module STRATEGY-INTROS
imports KORE-HELPERS

rule <strategy> intros Name => noop ...</strategy>
<claim> \implies(H, G) => G </claim>
<k> \implies(H, G) => G </k>
<local-context> (.Bag =>
<local-decl> axiom Name : H </local-decl>
) ...
Expand Down
Loading