Skip to content

Commit

Permalink
Merge pull request #59 from kframework/list-of-claims
Browse files Browse the repository at this point in the history 
Use  a list of  <goal>s instead of a set
  • Loading branch information
@h0nzZik
h0nzZik authored Apr 29, 2020
2 parents 902b502 + d62cc11 commit ffbb633
Show file tree
Hide file tree
Showing 40 changed files with 250 additions and 269 deletions.
31 changes: 19 additions & 12 deletions prover/drivers/base.md
View file
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
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
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
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
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
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
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
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
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

0 comments on commit ffbb633

Please sign in to comment.