Skip to content

Commit 7cbf5f9

Browse files
nishantjrnishantjr
committed
configuration: strategies are now in the <k> cell. goals in <claim>
This fixes issues in the various drivers. This logically makes more sense since it is the strategy cell that controls the execution.
1 parent 0ba6ffa commit 7cbf5f9

21 files changed

Lines changed: 519 additions & 520 deletions

‎prover/drivers/base.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ Configuration
22
=============
33

44
The configuration consists of a list of goals. The first goal is considered
5-
active. The `<k>` cell contains the Matching Logic Pattern for which we are
6-
searching for a proof. The `<strategy>` cell contains an imperative language
5+
active. The `<claim>` cell contains the Matching Logic Pattern for which we are
6+
searching for a proof. The `<k>` cell contains an imperative language
77
that controls which (high-level) proof rules are used to complete the goal. The
88
`<trace>` cell stores a log of the strategies used in the search of a proof and
99
other debug information. Eventually, this could be used for constructing a proof
@@ -26,8 +26,8 @@ module PROVER-CONFIGURATION
2626
<goal multiplicity="*" type="List" format="%1%i%n%2, %3%n%4%n%5n%6%n%7%n%d%8">
2727
<id format="id: %2"> .K </id>
2828
<parent format="parent: %2"> .K </parent>
29+
<claim> \and(.Patterns) </claim> // TODO: make this optional instead?
2930
<k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>
30-
<strategy> .K </strategy>
3131
<expected> .K </expected>
3232
<local-context>
3333
<local-decl multiplicity="*" type="Set"> .K </local-decl>
@@ -91,7 +91,7 @@ module DRIVER-BASE
9191
<goal>
9292
<id> .K </id>
9393
<expected> .K </expected>
94-
<strategy> .K </strategy>
94+
<k> .K </k>
9595
...
9696
</goal>
9797
</goals>

‎prover/drivers/kore-driver.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,7 @@ in the subgoal and the claim of the named goal remains intact.
7171
=> subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT))
7272
...
7373
</k>
74+
rule <k> (success => .K) ~> D:Declarations ... </k>
7475
```
7576

7677
```k

‎prover/drivers/smt-driver.md‎

Lines changed: 13 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -217,7 +217,7 @@ module DRIVER-SMT
217217
</k>
218218
requires notBool #matchesUnfoldMutRecs(STRAT)
219219
220-
rule <strategy> unfold-mut-recs => noop ... </strategy>
220+
rule <k> unfold-mut-recs => noop ... </k>
221221
222222
syntax Bool ::= #matchesUnfoldMutRecs(Strategy) [function]
223223
rule #matchesUnfoldMutRecs(unfold-mut-recs) => true
@@ -319,23 +319,20 @@ module DRIVER-SMT
319319
rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S)
320320
321321
syntax KItem ::= "expect" TerminalStrategy
322-
rule <strategy> S ~> expect S => .K ... </strategy>
322+
rule <k> S ~> expect S => .K ... </k>
323323
324-
rule <goals>
325-
<k> #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
324+
rule <k> ( #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
326325
~> (check-sat)
327-
=> #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
328-
...
329-
</k>
330-
<strategy> .K
331-
=> subgoal(\implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
332-
, STRAT
333-
)
334-
~> expect EXPECTED
335-
</strategy>
336-
...
337-
</goals>
338-
requires notBool PATTERN ==K \exists { .Patterns } \and ( .Patterns )
326+
)
327+
=> ( subgoal(\implies( \and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
328+
, STRAT
329+
)
330+
~> #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
331+
)
332+
...
333+
</k>
334+
requires notBool PATTERN ==K \exists { .Patterns } \and ( .Patterns )
335+
rule <k> (success => .K) ~> #goal( goal: _, strategy: _, expected: _) ... </k>
339336
```
340337

341338
```k

‎prover/drivers/unit-tests.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ module UNIT-TEST
2727
2828
syntax Declaration ::= "suite" String
2929
rule <k> suite(SUITE) => next-test(SUITE, 1) ... </k>
30-
30+
3131
syntax Declaration ::= "next-test" "(" String "," Int ")"
3232
rule <k> next-test(SUITE, N)
3333
=> test(SUITE, N)

‎prover/lang/smt-lang.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -244,6 +244,7 @@ module SMTLIB2-HELPERS
244244
rule CheckSAT.parseResult(#systemResult(0, "sat\n", STDERR)) => sat
245245
rule CheckSAT.parseResult(#systemResult(0, "unsat\n", STDERR)) => unsat
246246
rule CheckSAT.parseResult(#systemResult(0, "unknown\n", STDERR)) => unknown
247+
rule CheckSAT.parseResult(#systemResult(0, "timeout\n", STDERR)) => unknown
247248
rule CheckSAT.parseResult(#systemResult(I, STDOUT, STDERR)) => #error(#systemResult(I, STDOUT, STDERR))
248249
requires I =/=Int 0
249250
endmodule

‎prover/strategies/apply-equation.md‎

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -25,18 +25,18 @@ module STRATEGY-APPLY-EQUATION
2525
imports VISITOR-SYNTAX
2626
imports SYNTACTIC-MATCH-SYNTAX
2727
28-
rule <strategy> (.K => loadNamed(Name))
28+
rule <k> (.K => loadNamed(Name))
2929
~> apply-equation D Name at _ by[_] ...
30-
</strategy>
30+
</k>
3131
32-
rule <strategy> (P:Pattern ~> apply-equation D _ at Idx by[Ss])
32+
rule <k> (P:Pattern ~> apply-equation D _ at Idx by[Ss])
3333
=> #apply-equation1
3434
( hypothesis: P
3535
, direction: D
3636
, at: Idx
3737
, by: Ss
3838
)
39-
...</strategy>
39+
...</k>
4040
4141
4242
syntax KItem ::= "#apply-equation1"
@@ -57,7 +57,7 @@ module STRATEGY-APPLY-EQUATION
5757
=> apply-equation.checkShape(P)
5858
rule apply-equation.checkShape(_) => false [owise]
5959
60-
rule <strategy>
60+
rule <k>
6161
#apply-equation1
6262
( hypothesis: H, direction: D, at: Idx, by: Strats)
6363
=>
@@ -77,7 +77,7 @@ module STRATEGY-APPLY-EQUATION
7777
, by: Strats
7878
)
7979
...
80-
</strategy>
80+
</k>
8181
requires apply-equation.checkShape(H)
8282
8383
// Gets LHS or RHS of a conclusion that is an equality.
@@ -105,7 +105,7 @@ module STRATEGY-APPLY-EQUATION
105105
"," "by:" Strategies
106106
")"
107107
108-
rule <strategy>
108+
rule <k>
109109
#apply-equation2(from: L, to: R, hypothesis: H, at: Idx, by: Ss)
110110
=>
111111
#apply-equation3
@@ -120,8 +120,8 @@ module STRATEGY-APPLY-EQUATION
120120
, by: Ss
121121
)
122122
...
123-
</strategy>
124-
<k> T </k>
123+
</k>
124+
<claim> T </claim>
125125
126126
syntax KItem ::= "#apply-equation3"
127127
"(" "hypothesis:" Pattern
@@ -130,7 +130,7 @@ module STRATEGY-APPLY-EQUATION
130130
"," "by:" Strategies
131131
")"
132132
133-
rule <strategy>
133+
rule <k>
134134
#apply-equation3
135135
( hypothesis: P
136136
, heatResult: heatResult(Heated, Subst)
@@ -139,29 +139,29 @@ module STRATEGY-APPLY-EQUATION
139139
)
140140
=> instantiateAssumptions(GId, Subst, P)
141141
~> createSubgoalsWithStrategies(strats: Ss, result: noop)
142-
...</strategy>
143-
<k>
142+
...</k>
143+
<claim>
144144
_ => cool(heated: Heated, term: substMap(R, Subst))
145-
</k>
145+
</claim>
146146
<id> GId </id>
147147
148148
syntax KItem ::= "createSubgoalsWithStrategies"
149149
"(" "strats:" Strategies
150150
"," "result:" Strategy
151151
")"
152152
153-
rule <strategy> (#instantiateAssumptionsResult(.Patterns, .Map)
153+
rule <k> (#instantiateAssumptionsResult(.Patterns, .Map)
154154
~> createSubgoalsWithStrategies
155155
( strats: .Strategies
156156
, result: R))
157157
=> R
158-
...</strategy>
158+
...</k>
159159
160-
rule <strategy> #instantiateAssumptionsResult(P,Ps => Ps, .Map)
160+
rule <k> #instantiateAssumptionsResult(P,Ps => Ps, .Map)
161161
~> createSubgoalsWithStrategies
162162
( strats: (S, Ss) => Ss
163163
, result: R => R & subgoal(P, S))
164-
...</strategy>
164+
...</k>
165165
166166
```
167167
### Apply equation in context
@@ -180,10 +180,10 @@ Gamma |- C[... /\ A=B /\ ... /\ A /\ ... ]
180180

181181
```k
182182
183-
rule <strategy> apply-equation(eq: \equals(_,_) #as Eq, idx: Idx, direction: D, at: At)
183+
rule <k> apply-equation(eq: \equals(_,_) #as Eq, idx: Idx, direction: D, at: At)
184184
=> noop
185-
...</strategy>
186-
<k> C
185+
...</k>
186+
<claim> C
187187
=> visitorResult.getPattern(
188188
visitTopDown(
189189
applyEquationInContextVisitor(aeicParams(
@@ -192,7 +192,7 @@ Gamma |- C[... /\ A=B /\ ... /\ A /\ ... ]
192192
C
193193
)
194194
)
195-
</k>
195+
</claim>
196196
197197
syntax KItem ::= "aeicParams" "(" "eq:" Pattern
198198
"," "idx:" Int

‎prover/strategies/apply.md‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,11 @@ module STRATEGY-APPLY
2121
imports SYNTACTIC-MATCH-SYNTAX
2222
imports INSTANTIATE-ASSUMPTIONS-SYNTAX
2323
24-
rule <strategy> (.K => loadNamed(Name))
24+
rule <k> (.K => loadNamed(Name))
2525
~> apply(Name, _) ...
26-
</strategy>
26+
</k>
2727
28-
rule <strategy>
28+
rule <k>
2929
(A:Pattern ~> apply(_, Strat))
3030
=> #apply1(
3131
A,
@@ -36,38 +36,38 @@ module STRATEGY-APPLY
3636
),
3737
Strat
3838
)
39-
...</strategy>
40-
<k> G </k>
39+
...</k>
40+
<claim> G </claim>
4141
4242
4343
syntax KItem ::= #apply1(Pattern, MatchResult, Strategy)
4444
45-
rule <strategy>
45+
rule <k>
4646
#apply1(A, #matchResult(subst: Subst), Strat)
4747
=> #apply2(instantiateAssumptions(GId, Subst, A), Strat, success)
48-
...</strategy>
48+
...</k>
4949
<id> GId </id>
5050
51-
rule <strategy>
51+
rule <k>
5252
#apply1(_, #error(_), _) => fail
53-
...</strategy>
53+
...</k>
5454
5555
syntax KItem ::= #apply2(
5656
InstantiateAssumptionsResult,
5757
Strategy, Strategy)
5858
59-
rule <strategy>
59+
rule <k>
6060
#apply2(#instantiateAssumptionsResult(.Patterns, .Map), _, Result)
6161
=> Result
62-
...</strategy>
62+
...</k>
6363
64-
rule <strategy>
64+
rule <k>
6565
#apply2(
6666
#instantiateAssumptionsResult(P, Ps => Ps, .Map),
6767
Strat,
6868
Result => Result & subgoal(P, Strat)
6969
)
70-
...</strategy>
70+
...</k>
7171
7272
endmodule
7373
```

0 commit comments

Comments
 (0)