Prettyprint/produce proof tree

prover/lib/render-proof-tree

@@ -0,0 +1,92 @@
+#!/usr/bin/env python
+
+usage = \
+"""Prints the proof tree and either the active goal, or the specified goal.
+
+Usage:
+
+    lib/render-proof-tree <filename> [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
+
+# Parse K output
+# --------------
+
+nodes = {}
+roots = []
+next_line_is_claim = False
+next_line_is_trace = False
+
+with open(input_file) as f:
+  for line in f:
+    match = re.search(' *active: (\w*), id: (\w*\d*), parent: (\.|\w*\d*)', line)
+    if match is not None:
+        active    = match.group(1) == 'true'
+        id        = match.group(2)
+        parent    = match.group(3)
+        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
+    if next_line_is_trace: node.trace = line.strip(); next_line_is_trace = False
+    next_line_is_claim = re.search('<claim>', line) is not None
+    next_line_is_trace = re.search('<trace>', 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
+         , term_normal
+         )
+
+for pre, fill, node in RenderTree(roots[0]):
+    if is_node_selected(node):
+        print('id:', node.id)
+        print('claim:', node.claim)
+

prover/strategies/core.md

@@ -63,10 +63,14 @@ cooled back into the sequence strategy.
 
 ```k
   syntax ResultStrategy ::= "#hole"
-  rule <strategy> S1 . S2 => S1 ~> #hole . S2 ... </strategy>
+  rule <strategy> S1 . S2 => S1 ~> #hole . S2 </strategy>
+       <trace> _ => S1 </trace>
     requires notBool(isResultStrategy(S1))
      andBool notBool(isSequenceStrategy(S1))
-  rule <strategy> S1:ResultStrategy ~> #hole . S2 => S1 . S2 ... </strategy>
+  rule <claim> GOAL:Pattern </claim>
+       <strategy> S1:SequenceStrategy ~> #hole . S2 => S1 . S2 </strategy>
+  rule <claim> GOAL:Pattern </claim>
+       <strategy> S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) </strategy>
 ```
 
 The `noop` (no operation) strategy is the unit for sequential composition:
@@ -94,15 +98,44 @@ completed, its result is replaced in the parent goal and the subgoal is removed.
                 <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> ID </id>
+                <active> true:Bool => false </active>
+                <parent> PID </parent>
+                <strategy> (.K => #reap?) ~> RStrat:TerminalStrategy </strategy>
+                ...
+         </goal>
          ...
        </prover>
+
+  syntax KItem ::= "#reap?" // if goal failed prune goal and children
+  rule <strategy> (#reap? => #reap) ~> fail    </strategy>
+  rule <strategy> (#reap? => .K   ) ~> success </strategy>
+
+  syntax KItem ::= "#reap"  // (always) prune goal and children
+  rule <goal>
+         <id> PID </id>
+         <strategy> #reap ~> RStrat:TerminalStrategy </strategy>
+         ...
+       </goal>
+       <goal>
+         <parent> PID </parent>
+         <strategy> (.K => #reap) ~> Strat:Strategy </strategy>
+         ...
+       </goal>
+  rule <prover>
+         <goal>
+           <id> ID </id>
+           <strategy> #reap ~> Strat:Strategy </strategy>
+           ...
+         </goal> => .Bag
+         ...
+      </prover>
+    requires notBool hasChildren(ID)
+
+  syntax Bool ::= hasChildren(GoalId) [function]
+  rule [[ hasChildren(ID) => true ]]
+       <parent> ID </parent>
+  rule hasChildren(ID) => false [owise]
 ```
 
 Proving a goal may involve proving other subgoals:
@@ -118,7 +151,6 @@ Proving a goal may involve proving other subgoals:
                <strategy> SUBSTRAT </strategy>
                <claim> SUBGOAL </claim>
                <local-context> LC </local-context>
-               <trace> TRACE </trace>
                ...
              </goal>
          )
@@ -127,7 +159,6 @@ Proving a goal may involve proving other subgoals:
            <active> true => false </active>
            <strategy> subgoal(SUBGOAL, SUBSTRAT) => goalStrat(!ID:Int) ... </strategy>
            <local-context> LC::Bag </local-context>
-           <trace> TRACE </trace>
            ...
          </goal>
          ...

prover/strategies/smt.md

@@ -206,7 +206,7 @@ module STRATEGY-SMT
                   fi
                   ...
        </strategy>
-       <trace> .K => smt-z3 ... </trace>
+       <trace> .K => smt-z3 ~> (Z3Prelude ++SMTLIB2Script ML2SMTLIB(\not(GOAL))) ... </trace>
 
   rule <claim> GOAL </claim>
        <strategy> smt-z3 => fail </strategy>
@@ -220,7 +220,7 @@ module STRATEGY-SMT
                   fi
                   ...
        </strategy>
-       <trace> .K => smt-cvc4 ... </trace>
+       <trace> .K => smt-cvc4 ~> CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \not(GOAL), collectDeclarations(GId)) ... </trace>
      requires isPredicatePattern(GOAL)
 
 // If the constraints are unsatisfiable, the entire term is unsatisfiable
@@ -233,7 +233,7 @@ module STRATEGY-SMT
                   fi
                   ...
        </strategy>
-       <trace> .K => check-lhs-constraint-unsat ... </trace>
+       <trace> .K => check-lhs-constraint-unsat ~> CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(LCONSTRAINTS), collectDeclarations(GId)) ... </trace>
      requires isPredicatePattern(\and(LCONSTRAINTS))
 
 ```