drivers: Initial goal is now populated via subgoal strategy

kframework · Apr 15, 2020 · 4eab015 · 4eab015
1 parent d85aa38
commit 4eab015
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 42 deletions.
diff --git a/prover/drivers/base.md b/prover/drivers/base.md
@@ -87,6 +87,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

diff --git a/prover/drivers/kore-driver.md b/prover/drivers/kore-driver.md
@@ -66,34 +66,11 @@ in the subgoal and the claim of the named goal remains intact.
         => claim getFreshClaimName() : PATTERN strategy STRAT
            ...
        </k>
-
-  rule <goals>
-         <k> claim NAME : PATTERN
-             strategy STRAT
-          => .K
-             ...
-         </k>
-         ( .Bag =>
-           <goal>
-             <id> NAME </id>
-             <active> true:Bool </active>
-             <parent> .K </parent>
-             <k> PATTERN </k>
-             <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>
+  rule <k> claim NAME : PATTERN
+           strategy STRAT
+        => subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT))
+           ...
+       </k>
 ```
 
 ```k

diff --git a/prover/drivers/smt-driver.md b/prover/drivers/smt-driver.md
@@ -318,24 +318,21 @@ module DRIVER-SMT
   rule #containsSpatialPatterns(.Patterns, _) => false
   rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S)
 
+  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>
-         ( .Bag =>
-           <goal>
-             <id> !N:ClaimName </id>
-             <active> true:Bool </active>
-             <parent> .K </parent>
-             <k> \implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) </k>
-             <strategy> STRAT </strategy>
-             <expected> EXPECTED </expected>
-             <local-context> .Bag </local-context>
-             <trace> .K </trace>
-           </goal>
-         )
+         <strategy> .K
+                 => subgoal(\implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
+                           , STRAT
+                           )
+                 ~> expect EXPECTED
+         </strategy>
          ...
        </goals>
    requires notBool PATTERN ==K  \exists { .Patterns } \and ( .Patterns )

diff --git a/prover/strategies/core.md b/prover/strategies/core.md
@@ -109,10 +109,13 @@ 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>
+               <id> ID:Int </id>
                <active> true </active>
                <parent> PARENT </parent>
                <strategy> SUBSTRAT </strategy>
@@ -125,7 +128,7 @@ Proving a goal may involve proving other subgoals:
          <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>
            ...