From 7bac10ed77ca976b2dcd7ad445737607a3c54f36 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 12 Feb 2020 02:06:41 +0530 Subject: [PATCH 1/7] core: Sequential composition uses subgoals too --- prover/strategies/core.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 4a5a95ac9..07693e8af 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -63,10 +63,11 @@ cooled back into the sequence strategy. ```k syntax ResultStrategy ::= "#hole" - rule S1 . S2 => S1 ~> #hole . S2 ... + rule S1 . S2 => S1 ~> #hole . S2 requires notBool(isResultStrategy(S1)) andBool notBool(isSequenceStrategy(S1)) - rule S1:ResultStrategy ~> #hole . S2 => S1 . S2 ... + rule GOAL:Pattern + S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) ``` The `noop` (no operation) strategy is the unit for sequential composition: From 018f0f2090508114d4d11b97278dda257b71f327 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 12 Feb 2020 02:42:53 +0530 Subject: [PATCH 2/7] Reap failed goals and children (TODO: This uses `[owise]`) --- prover/strategies/core.md | 43 ++++++++++++++++++++++++++++++++------- 1 file changed, 36 insertions(+), 7 deletions(-) diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 07693e8af..3de608204 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -95,15 +95,44 @@ completed, its result is replaced in the parent goal and the subgoal is removed. goalStrat(ID) => RStrat ... ... - ( ID - true:Bool - PID - RStrat:TerminalStrategy - ... - => .Bag - ) + ID + true:Bool => false + PID + (.K => #reap?) ~> RStrat:TerminalStrategy + ... + ... + + syntax KItem ::= "#reap?" // if goal failed prune goal and children + rule (#reap? => #reap) ~> fail + rule (#reap? => .K ) ~> success + + syntax KItem ::= "#reap" // (always) prune goal and children + rule + PID + #reap ~> RStrat:TerminalStrategy + ... + + + PID + (.K => #reap) ~> Strat:Strategy + ... + + rule + + ID + #reap ~> Strat:Strategy + ... + => .Bag + ... + + requires notBool hasChildren(ID) + + syntax Bool ::= hasChildren(GoalId) [function] + rule [[ hasChildren(ID) => true ]] + ID + rule hasChildren(ID) => false [owise] ``` Proving a goal may involve proving other subgoals: From ec54f3667ae6ca5e47b19f3f6cc8eb43874dbee6 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 12 Feb 2020 03:57:22 +0530 Subject: [PATCH 3/7] lib/render-proof-tree: Small python script for extracting tree structure --- prover/lib/render-proof-tree | 40 ++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100755 prover/lib/render-proof-tree diff --git a/prover/lib/render-proof-tree b/prover/lib/render-proof-tree new file mode 100755 index 000000000..3ae540f5d --- /dev/null +++ b/prover/lib/render-proof-tree @@ -0,0 +1,40 @@ +#!/usr/bin/env python + +from anytree import NodeMixin, Node, RenderTree +from collections import namedtuple +import textwrap +import fileinput +import re + + +class Goal(NodeMixin): + def __init__(self, id, parent_id): + self.id = id + self.name = id + self.parent_id = parent_id + self.claim = None + +nodes = {} +roots = [] + +for line in fileinput.input(): + match = re.search(' *active: \w*, id: (\w*\d*), parent: (\.|\w*\d*)', line) + if not match is None: + id = match.group(1) + parent = match.group(2) + node = Goal(id, parent) + nodes[id] = node + if parent == '.': roots += [node] + match = re.search('implies', line) + if not match is None: + node.claim = line + +for id, node in nodes.items(): + if node in roots: continue + node.parent = nodes[node.parent_id] + +for pre, fill, node in RenderTree(roots[0]): + print(pre, 'id: ', node.id, 'x') + # if not node.claim is None: + # print(('\n' + fill).join(textwrap.wrap('claim: ' + node.claim))) + From 146e6eeee025f09ce15c87a0d5caf9d9ef7b02bc Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 12 Feb 2020 22:44:00 +0530 Subject: [PATCH 4/7] strategies/core: Do not copy the trace to subgoals Since we are not removing subgoals unless they fail this is no longer necessary --- prover/strategies/core.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 3de608204..522adea7d 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -148,7 +148,6 @@ Proving a goal may involve proving other subgoals: SUBSTRAT SUBGOAL LC - TRACE ... ) @@ -157,7 +156,6 @@ Proving a goal may involve proving other subgoals: true => false subgoal(SUBGOAL, SUBSTRAT) => goalStrat(!ID:Int) ... LC::Bag - TRACE ... ... From 8ea3877bd4af3f2db5b6f0bf4cca02ec8da1b76a Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 12 Feb 2020 22:44:40 +0530 Subject: [PATCH 5/7] strategies/smt: Place SMTLIB2Script in trace cell --- prover/strategies/smt.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prover/strategies/smt.md b/prover/strategies/smt.md index fe2491b93..7f1df70e3 100644 --- a/prover/strategies/smt.md +++ b/prover/strategies/smt.md @@ -206,7 +206,7 @@ module STRATEGY-SMT fi ... - .K => smt-z3 ... + .K => smt-z3 ~> (Z3Prelude ++SMTLIB2Script ML2SMTLIB(\not(GOAL))) ... rule GOAL smt-z3 => fail @@ -220,7 +220,7 @@ module STRATEGY-SMT fi ... - .K => smt-cvc4 ... + .K => smt-cvc4 ~> CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \not(GOAL), collectDeclarations(GId)) ... requires isPredicatePattern(GOAL) // If the constraints are unsatisfiable, the entire term is unsatisfiable @@ -233,7 +233,7 @@ module STRATEGY-SMT fi ... - .K => check-lhs-constraint-unsat ... + .K => check-lhs-constraint-unsat ~> CVC4Prelude ++SMTLIB2Script ML2SMTLIBDecls(GId, \and(LCONSTRAINTS), collectDeclarations(GId)) ... requires isPredicatePattern(\and(LCONSTRAINTS)) ``` From 54c028500e65afa5c785d473915c4c6d71555c22 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Mon, 20 Apr 2020 21:58:07 +0530 Subject: [PATCH 6/7] lib/render-proof-tree: Prints prints current goal, and trace cells --- prover/lib/render-proof-tree | 78 ++++++++++++++++++++++++++++++------ prover/strategies/core.md | 1 + 2 files changed, 66 insertions(+), 13 deletions(-) diff --git a/prover/lib/render-proof-tree b/prover/lib/render-proof-tree index 3ae540f5d..e0cdee30c 100755 --- a/prover/lib/render-proof-tree +++ b/prover/lib/render-proof-tree @@ -1,5 +1,18 @@ #!/usr/bin/env python +usage = \ +"""Prints the proof tree and either the active goal, or the specified goal. + +Usage: + + lib/render-proof-tree [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 @@ -7,34 +20,73 @@ 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): + 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 -for line in fileinput.input(): - match = re.search(' *active: \w*, id: (\w*\d*), parent: (\.|\w*\d*)', line) - if not match is None: - id = match.group(1) - parent = match.group(2) - node = Goal(id, parent) +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] - match = re.search('implies', line) - if not match is None: - node.claim = line + 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('', line) is not None + next_line_is_trace = re.search('', 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]): - print(pre, 'id: ', node.id, 'x') - # if not node.claim is None: - # print(('\n' + fill).join(textwrap.wrap('claim: ' + node.claim))) + if is_node_selected(node): + print('id:', node.id) + print('claim:', node.claim) diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 522adea7d..4b330da04 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -64,6 +64,7 @@ cooled back into the sequence strategy. ```k syntax ResultStrategy ::= "#hole" rule S1 . S2 => S1 ~> #hole . S2 + _ => S1 requires notBool(isResultStrategy(S1)) andBool notBool(isSequenceStrategy(S1)) rule GOAL:Pattern From e1dd33a0c022e71debdc961c3c584ea30bfd9de7 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Mon, 20 Apr 2020 23:05:54 +0530 Subject: [PATCH 7/7] core: cool sequences back in, so that subgoals are only generated for a single uncomposed strategy --- prover/strategies/core.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 4b330da04..77878fbb8 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -67,6 +67,8 @@ cooled back into the sequence strategy. _ => S1 requires notBool(isResultStrategy(S1)) andBool notBool(isSequenceStrategy(S1)) + rule GOAL:Pattern + S1:SequenceStrategy ~> #hole . S2 => S1 . S2 rule GOAL:Pattern S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) ```