From ac2950e8370056bf324c787a28dd069d15195b8b Mon Sep 17 00:00:00 2001 From: Steve_Freecastler Date: Sun, 23 Jan 2022 15:46:59 +0100 Subject: [PATCH 1/3] proof visualizer / proof tree with proof text samples to test it. Manual is in the README.md --- Webinterface/doc/README.md | 40 ++ .../src/main/visualizer/smt-beweis-kopie.txt | 55 +++ .../visualizer/smtinterpol-beweise-02.txt | 146 ++++++ .../visualizer/textparser_and_resolver.js | 455 ++++++++++++++++++ Webinterface/src/main/visualizer/tree.css | 110 +++++ Webinterface/src/main/visualizer/tree.html | 46 ++ 6 files changed, 852 insertions(+) create mode 100644 Webinterface/doc/README.md create mode 100644 Webinterface/src/main/visualizer/smt-beweis-kopie.txt create mode 100644 Webinterface/src/main/visualizer/smtinterpol-beweise-02.txt create mode 100644 Webinterface/src/main/visualizer/textparser_and_resolver.js create mode 100644 Webinterface/src/main/visualizer/tree.css create mode 100644 Webinterface/src/main/visualizer/tree.html diff --git a/Webinterface/doc/README.md b/Webinterface/doc/README.md new file mode 100644 index 000000000..04545481f --- /dev/null +++ b/Webinterface/doc/README.md @@ -0,0 +1,40 @@ +# SMT-Beweisvisualisierung +Beweisvisualisierung für vorhandenen SMT-Solver + +Manual: + +When executing the visualize_proof() function by pushing the "Start SMT proof" button the proof text +that was put or copied into the the responding field will be split through the smt_parser() function. + +In addition the class Node is created whose objects later contain following information: +unique IDs, arrays containing the children, ID of the parent node, complete text part of the node or leaf, +the filtered literals, pivots and resolved intermediate results for nodes that have children. + +The smt_parser() function differentiates between inner nodes, starting with "(! (@res" or "(@res" and leafs, +starting with "(! (@clause", "(@clause)", "(! (@lemma", or "(@lemma". +Both will then be edited again with separate parsers (parseNode and parseLeaf), turned into a object of +the Node class and receive following information: +- unique IDs (starting at "0") +- an array with the responding kids (if present) +- ID of the parent node (root node keeps the parent ID "-1") +- a boolean "is_leaf" which will be set to "true" if it is a leaf and has no children +- a set with literals (sets being used so there are no duplicates) +- the pivot (if present) +and inner nodes will also receives a set of intermediate results of the resolved children. + +Therefore the literals will be extracted with the extract_literals() function and then saved in node_literals. +This function calls the extract_literals_lemma() function on leafs containing the string "lemma" and the +extract_literals_clause() function on those containing the string "clause". +During this process the literals with parenthesis as well as those without are being considered. + +If the string ":pivot" is also contained after these steps, the extract_pivot() function will be +executed to extract the corresponding pivot. + +For the inner nodes these steps will be executed recursively and the compute_literals_res_node() function will +be executed which calculates and returns the resolved result of all children and saves it in node_literals. +In this function the compute_res() function always computes a resolve step from the children and saves +it in these children nodes as intermediate_result. + +When resolving, the given pivot will be checked in normal and negated version. + +In the end the proof tree results in an empty set. diff --git a/Webinterface/src/main/visualizer/smt-beweis-kopie.txt b/Webinterface/src/main/visualizer/smt-beweis-kopie.txt new file mode 100644 index 000000000..cf14f3f74 --- /dev/null +++ b/Webinterface/src/main/visualizer/smt-beweis-kopie.txt @@ -0,0 +1,55 @@ +//// Eingabeskript für SMTInterpol + +(set-option :print-success false) +(set-option :produce-interpolants true) +(set-info :status unsat) +(set-logic QF_UFLIA) +(declare-fun f (Int) Int) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (and (= x (f x)) (= x y) (= (f y) (+ x 1)))) +(check-sat) +(get-proof) +(exit) + +//// Beweis mit Umschreibschritten der Eingabeformel + +(@res (@res (@lemma (! (or (not (! (= (f y) (+ x 1)) :quotedCC)) (not (! (= x (f x)) :quotedCC)) (not (! (= (f y) (f x)) :quotedCC))) :CC ((! (= (+ x 1) x) :quotedCC) :subpath ((+ x 1) (f y) (f x) x)))) (! (@lemma (! (or (! (= (f y) (f x)) :quotedCC) (not (! (= x y) :quotedCC))) :CC ((! (= (f y) (f x)) :quotedCC) :subpath ((f y) (f x))))) :pivot (! (= (f y) (f x)) :quotedCC))) (! (@clause (@eq (@eq (@split (! (@eq (@asserted (and (= x (f x)) (= x y) (= (f y) (+ x 1)))) (@rewrite (! (= (and (= x (f x)) (= x y) (= (f y) (+ x 1))) (not (or (not (= x (f x))) (not (= x y)) (not (= (f y) (+ x 1)))))) :andToOr))) :notOr) (not (not (= (f y) (+ x 1))))) (@rewrite (! (= (not (not (= (f y) (+ x 1)))) (= (f y) (+ x 1))) :notSimp))) (@rewrite (! (= (= (f y) (+ x 1)) (! (= (f y) (+ x 1)) :quotedCC)) :intern))) (! (! (= (f y) (+ x 1)) :quotedCC) :input)) :pivot (! (= (f y) (+ x 1)) :quotedCC)) (! (@clause (@eq (@eq (@split (! (@eq (@asserted (and (= x (f x)) (= x y) (= (f y) (+ x 1)))) (@rewrite (! (= (and (= x (f x)) (= x y) (= (f y) (+ x 1))) (not (or (not (= x (f x))) (not (= x y)) (not (= (f y) (+ x 1)))))) :andToOr))) :notOr) (not (not (= x y)))) (@rewrite (! (= (not (not (= x y))) (= x y)) :notSimp))) (@rewrite (! (= (= x y) (! (= x y) :quotedCC)) :intern))) (! (! (= x y) :quotedCC) :input)) :pivot (! (= x y) :quotedCC)) (! (@clause (@eq (@eq (@split (! (@eq (@asserted (and (= x (f x)) (= x y) (= (f y) (+ x 1)))) (@rewrite (! (= (and (= x (f x)) (= x y) (= (f y) (+ x 1))) (not (or (not (= x (f x))) (not (= x y)) (not (= (f y) (+ x 1)))))) :andToOr))) :notOr) (not (not (= x (f x))))) (@rewrite (! (= (not (not (= x (f x)))) (= x (f x))) :notSimp))) (@rewrite (! (= (= x (f x)) (! (= x (f x)) :quotedCC)) :intern))) (! (! (= x (f x)) :quotedCC) :input)) :pivot (! (= x (f x)) :quotedCC))) + +//// Resolutionsbeweis (ohne Umschreibschritte) + +(@res (@res (@lemma (! (or (not (! (= (f y) (+ x 1)) :quotedCC)) (not (! (= x (f x)) :quotedCC)) (not (! (= (f y) (f x)) :quotedCC))) :CC ((! (= (+ x 1) x) :quotedCC) :subpath ((+ x 1) (f y) (f x) x)))) (! (@lemma (! (or (! (= (f y) (f x)) :quotedCC) (not (! (= x y) :quotedCC))) :CC ((! (= (f y) (f x)) :quotedCC) :subpath ((f y) (f x))))) :pivot (! (= (f y) (f x)) :quotedCC))) (! (@clause (@asserted (! (= (f y) (+ x 1)) :quotedCC)) (! (! (= (f y) (+ x 1)) :quotedCC) :input)) :pivot (! (= (f y) (+ x 1)) :quotedCC)) (! (@clause (@asserted (! (= x y) :quotedCC)) (! (! (= x y) :quotedCC) :input)) :pivot (! (= x y) :quotedCC)) (! (@clause (@asserted (! (= x (f x)) :quotedCC)) (! (! (= x (f x)) :quotedCC) :input)) :pivot (! (= x (f x)) :quotedCC))) + +//// Beweis lesbarer formatiert mit allen Klauseln + +(@res + (@res + (@lemma (! (or (not (! (= (f y) (+ x 1)) :quotedCC)) (not (! (= x (f x)) :quotedCC)) (not (! (= (f y) (f x)) :quotedCC))) :CC ((! (= (+ x 1) x) :quotedCC) :subpath ((+ x 1) (f y) (f x) x)))) + // != f(y)=x+1 \/ != x=f(x) \/ != f(x)=f(y) + + (! (@lemma (! (or (! (= (f y) (f x)) :quotedCC) (not (! (= x y) :quotedCC))) :CC ((! (= (f y) (f x)) :quotedCC) :subpath ((f y) (f x))))) + // f(x)=f(y) \/ != x=y + :pivot (! (= (f y) (f x)) :quotedCC))) + // != f(y)=x+1 \/ != x=f(x) \/ != x=y + + (! (@clause (@asserted (! (= (f y) (+ x 1)) :quotedCC)) (! (! (= (f y) (+ x 1)) :quotedCC) :input)) + // f(y)=x+1 + :pivot (! (= (f y) (+ x 1)) :quotedCC)) + // != x=f(x) \/ != x=y + + (! (@clause (@asserted (! (= x y) :quotedCC)) (! (! (= x y) :quotedCC) :input)) + // x=y + :pivot (! (= x y) :quotedCC)) + // != x=f(x) + + (! (@clause (@asserted (! (= x (f x)) :quotedCC)) (! (! (= x (f x)) :quotedCC) :input)) + // x=f(x) + :pivot (! (= x (f x)) :quotedCC))) + // {} + + +/// Resolutionsregel + +C_1 \/ ~l C_2 \/ l +-------------------- + C_1 \/ C_2 diff --git a/Webinterface/src/main/visualizer/smtinterpol-beweise-02.txt b/Webinterface/src/main/visualizer/smtinterpol-beweise-02.txt new file mode 100644 index 000000000..bc49fead8 --- /dev/null +++ b/Webinterface/src/main/visualizer/smtinterpol-beweise-02.txt @@ -0,0 +1,146 @@ +Trivialer Beweis - ohne "@res"! + +(@clause (@asserted false) (! false :input)) + +-------------------------------------------------------------------------------- + +Beweis mit Literalen ohne ":quoted" + +Proof text: + +(@res (@clause (@asserted (not p)) (! (not p) :input)) (! (@clause (@asserted p) (! p :input)) :pivot p)) + +Structured: + +(@res + (@clause (@asserted (not p)) (! (not p) :input)) + (! (@clause (@asserted p) (! p :input)) + :pivot p)) + +-------------------------------------------------------------------------------- + +Beweis mit weiterer Art von Literalen und weiterer Art von Lemmas (nicht ":CC", aber immer gleicher Aufbau) + +Proof text: + +(@res (@clause (@asserted (! (<= (+ b (- a) 1) 0) :quotedLA)) (! (! (<= (+ b (- a) 1) 0) :quotedLA) :input)) (! (@res (@lemma (! (or (! (<= (+ b (- a)) 0) :quotedLA) (not (! (<= (+ b (- a) 1) 0) :quotedLA))) :LA ((- 1) 1))) (! (@clause (@asserted (not (! (<= (+ b (- a)) 0) :quotedLA))) (! (not (! (<= (+ b (- a)) 0) :quotedLA)) :input)) :pivot (not (! (<= (+ b (- a)) 0) :quotedLA)))) :pivot (not (! (<= (+ b (- a) 1) 0) :quotedLA)))) + +Structured: + +(@res + (@clause (@asserted (! (<= (+ b (- a) 1) 0) :quotedLA)) (! (! (<= (+ b (- a) 1) 0) :quotedLA) :input)) + (! (@res + (@lemma (! (or (! (<= (+ b (- a)) 0) :quotedLA) (not (! (<= (+ b (- a) 1) 0) :quotedLA))) :LA ((- 1) 1))) + (! (@clause (@asserted (not (! (<= (+ b (- a)) 0) :quotedLA))) (! (not (! (<= (+ b (- a)) 0) :quotedLA)) :input)) + :pivot (not (! (<= (+ b (- a)) 0) :quotedLA)))) + :pivot (not (! (<= (+ b (- a) 1) 0) :quotedLA)))) + +-------------------------------------------------------------------------------- + +Beweis mit "@clause" mit "or", sowie mit tiefer verschachtelten "@res" + +Proof text: + +(@res (@clause (@asserted (or (not (! (= a c) :quotedCC)) p)) (! (or (not (! (= a c) :quotedCC)) p) :input right)) (! (@res (@lemma (! (or (! (= a c) :quotedCC) (not (! (= a b) :quotedCC)) (not (! (= b c) :quotedCC))) :CC ((! (= a c) :quotedCC) :subpath (a b c)))) (! (@clause (@asserted (! (= b c) :quotedCC)) (! (! (= b c) :quotedCC) :input right)) :pivot (! (= b c) :quotedCC)) (! (@clause (@asserted (! (= a b) :quotedCC)) (! (! (= a b) :quotedCC) :input left)) :pivot (! (= a b) :quotedCC))) :pivot (! (= a c) :quotedCC)) (! (@res (@clause (@asserted (or (not (! (= a c) :quotedCC)) (not p))) (! (or (not (! (= a c) :quotedCC)) (not p)) :input left)) (! (@res (@lemma (! (or (! (= a c) :quotedCC) (not (! (= a b) :quotedCC)) (not (! (= b c) :quotedCC))) :CC ((! (= a c) :quotedCC) :subpath (a b c)))) (! (@clause (@asserted (! (= b c) :quotedCC)) (! (! (= b c) :quotedCC) :input right)) :pivot (! (= b c) :quotedCC)) (! (@clause (@asserted (! (= a b) :quotedCC)) (! (! (= a b) :quotedCC) :input left)) :pivot (! (= a b) :quotedCC))) :pivot (! (= a c) :quotedCC))) :pivot (not p))) + +Structured: + +(@res + (@clause (@asserted (or (not (! (= a c) :quotedCC)) p)) (! (or (not (! (= a c) :quotedCC)) p) :input right)) + (! (@res + (@lemma (! (or (! (= a c) :quotedCC) (not (! (= a b) :quotedCC)) (not (! (= b c) :quotedCC))) :CC ((! (= a c) :quotedCC) :subpath (a b c)))) + (! (@clause (@asserted (! (= b c) :quotedCC)) (! (! (= b c) :quotedCC) :input right)) + :pivot (! (= b c) :quotedCC)) + (! (@clause (@asserted (! (= a b) :quotedCC)) (! (! (= a b) :quotedCC) :input left)) + :pivot (! (= a b) :quotedCC))) + :pivot (! (= a c) :quotedCC)) + (! (@res + (@clause (@asserted (or (not (! (= a c) :quotedCC)) (not p))) (! (or (not (! (= a c) :quotedCC)) (not p)) :input left)) + (! (@res + (@lemma (! (or (! (= a c) :quotedCC) (not (! (= a b) :quotedCC)) (not (! (= b c) :quotedCC))) :CC ((! (= a c) :quotedCC) :subpath (a b c)))) + (! (@clause (@asserted (! (= b c) :quotedCC)) (! (! (= b c) :quotedCC) :input right)) + :pivot (! (= b c) :quotedCC)) + (! (@clause (@asserted (! (= a b) :quotedCC)) (! (! (= a b) :quotedCC) :input left)) + :pivot (! (= a b) :quotedCC))) + :pivot (! (= a c) :quotedCC))) + :pivot (not p))) + +-------------------------------------------------------------------------------- + +Langer Beweis (auch ausführliches Format) + +Proof text: + +(@res (@lemma (! (or (! (= (select a i) (select b j)) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= b (store s2 k3 v3)) :quotedCC)) (! (= j k3) :quotedCC) (! (= j k2) :quotedCC) (not (! (= s1 (store s2 k2 v2)) :quotedCC)) (! (= j k1) :quotedCC) (not (! (= a (store s1 k1 v1)) :quotedCC))) :read-over-weakeq ((! (= (select a i) (select b j)) :quotedCC) :weakpath (j (b (store s2 k3 v3) s2 (store s2 k2 v2) s1 (store s1 k1 v1) a))))) (! (@res (@lemma (! (or (! (= i k1) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= j k1) :quotedCC))) :CC ((! (= i k1) :quotedCC) :subpath (i j k1)))) (! (@clause (@mp (@split (! (@mp (@asserted (! (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2)))) :named A)) (@trans (@rewrite (! (= (! (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2)))) :named A) (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2))))) (@cong (@rewrite (! (= (and (not (= i k2)) (= s1 (store s2 k2 v2))) (not (or (not (not (= i k2))) (not (= s1 (store s2 k2 v2)))))) :andToOr)) (@cong (@refl (or (not (not (= i k2))) (not (= s1 (store s2 k2 v2))))) (@rewrite (! (= (not (not (= i k2))) (= i k2)) :notSimp))))) (@rewrite (! (= (and (not (= i k1)) (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) (not (or (not (not (= i k1))) (not (not (or (= i k2) (not (= s1 (store s2 k2 v2))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k1))) (not (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))))) (@rewrite (! (= (not (not (= i k1))) (= i k1)) :notSimp)) (@rewrite (! (= (not (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) (or (= i k2) (not (= s1 (store s2 k2 v2))))) :notSimp)))))) :notOr) (not (= i k1))) (@cong (@refl (not (= i k1))) (@rewrite (! (= (= i k1) (! (= i k1) :quotedCC)) :intern)))) (! (not (! (= i k1) :quotedCC)) :input A)) :pivot (not (! (= i k1) :quotedCC))) (! (@clause (@mp (@mp (@split (! (@split (! (@split (! (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) :notOr) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notOr) (not (or (not (= i j)) (= (select a i) (select b j))))) :notOr) (not (not (= i j)))) (@rewrite (! (= (not (not (= i j))) (= i j)) :notSimp))) (@rewrite (! (= (= i j) (! (= i j) :quotedCC)) :intern))) (! (! (= i j) :quotedCC) :input B)) :pivot (! (= i j) :quotedCC))) :pivot (not (! (= j k1) :quotedCC))) (! (@clause (@mp (@mp (@split (! (@split (! (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) :notOr) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notOr) (not (not (= b (store s2 k3 v3))))) (@rewrite (! (= (not (not (= b (store s2 k3 v3)))) (= b (store s2 k3 v3))) :notSimp))) (@rewrite (! (= (= b (store s2 k3 v3)) (! (= b (store s2 k3 v3)) :quotedCC)) :intern))) (! (! (= b (store s2 k3 v3)) :quotedCC) :input B)) :pivot (! (= b (store s2 k3 v3)) :quotedCC)) (! (@clause (@mp (@mp (@split (! (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) :notOr) (not (not (= a (store s1 k1 v1))))) (@rewrite (! (= (not (not (= a (store s1 k1 v1)))) (= a (store s1 k1 v1))) :notSimp))) (@rewrite (! (= (= a (store s1 k1 v1)) (! (= a (store s1 k1 v1)) :quotedCC)) :intern))) (! (! (= a (store s1 k1 v1)) :quotedCC) :input B)) :pivot (! (= a (store s1 k1 v1)) :quotedCC)) (! (@res (@lemma (! (or (! (= i k2) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= j k2) :quotedCC))) :CC ((! (= i k2) :quotedCC) :subpath (i j k2)))) (! (@clause (@mp (@split (! (@split (! (@mp (@asserted (! (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2)))) :named A)) (@trans (@rewrite (! (= (! (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2)))) :named A) (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2))))) (@cong (@rewrite (! (= (and (not (= i k2)) (= s1 (store s2 k2 v2))) (not (or (not (not (= i k2))) (not (= s1 (store s2 k2 v2)))))) :andToOr)) (@cong (@refl (or (not (not (= i k2))) (not (= s1 (store s2 k2 v2))))) (@rewrite (! (= (not (not (= i k2))) (= i k2)) :notSimp))))) (@rewrite (! (= (and (not (= i k1)) (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) (not (or (not (not (= i k1))) (not (not (or (= i k2) (not (= s1 (store s2 k2 v2))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k1))) (not (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))))) (@rewrite (! (= (not (not (= i k1))) (= i k1)) :notSimp)) (@rewrite (! (= (not (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) (or (= i k2) (not (= s1 (store s2 k2 v2))))) :notSimp)))))) :notOr) (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) :notOr) (not (= i k2))) (@cong (@refl (not (= i k2))) (@rewrite (! (= (= i k2) (! (= i k2) :quotedCC)) :intern)))) (! (not (! (= i k2) :quotedCC)) :input A)) :pivot (not (! (= i k2) :quotedCC))) (! (@clause (@mp (@mp (@split (! (@split (! (@split (! (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) :notOr) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notOr) (not (or (not (= i j)) (= (select a i) (select b j))))) :notOr) (not (not (= i j)))) (@rewrite (! (= (not (not (= i j))) (= i j)) :notSimp))) (@rewrite (! (= (= i j) (! (= i j) :quotedCC)) :intern))) (! (! (= i j) :quotedCC) :input B)) :pivot (! (= i j) :quotedCC))) :pivot (not (! (= j k2) :quotedCC))) (! (@clause (@mp (@mp (@split (! (@split (! (@mp (@asserted (! (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2)))) :named A)) (@trans (@rewrite (! (= (! (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2)))) :named A) (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k1)) (and (not (= i k2)) (= s1 (store s2 k2 v2))))) (@cong (@rewrite (! (= (and (not (= i k2)) (= s1 (store s2 k2 v2))) (not (or (not (not (= i k2))) (not (= s1 (store s2 k2 v2)))))) :andToOr)) (@cong (@refl (or (not (not (= i k2))) (not (= s1 (store s2 k2 v2))))) (@rewrite (! (= (not (not (= i k2))) (= i k2)) :notSimp))))) (@rewrite (! (= (and (not (= i k1)) (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) (not (or (not (not (= i k1))) (not (not (or (= i k2) (not (= s1 (store s2 k2 v2))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k1))) (not (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))))) (@rewrite (! (= (not (not (= i k1))) (= i k1)) :notSimp)) (@rewrite (! (= (not (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) (or (= i k2) (not (= s1 (store s2 k2 v2))))) :notSimp)))))) :notOr) (not (or (= i k2) (not (= s1 (store s2 k2 v2)))))) :notOr) (not (not (= s1 (store s2 k2 v2))))) (@rewrite (! (= (not (not (= s1 (store s2 k2 v2)))) (= s1 (store s2 k2 v2))) :notSimp))) (@rewrite (! (= (= s1 (store s2 k2 v2)) (! (= s1 (store s2 k2 v2)) :quotedCC)) :intern))) (! (! (= s1 (store s2 k2 v2)) :quotedCC) :input A)) :pivot (! (= s1 (store s2 k2 v2)) :quotedCC)) (! (@clause (@mp (@mp (@split (! (@split (! (@split (! (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) :notOr) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notOr) (not (or (not (= i j)) (= (select a i) (select b j))))) :notOr) (not (not (= i j)))) (@rewrite (! (= (not (not (= i j))) (= i j)) :notSimp))) (@rewrite (! (= (= i j) (! (= i j) :quotedCC)) :intern))) (! (! (= i j) :quotedCC) :input B)) :pivot (! (= i j) :quotedCC)) (! (@res (@lemma (! (or (! (= i k3) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= j k3) :quotedCC))) :CC ((! (= i k3) :quotedCC) :subpath (i j k3)))) (! (@clause (@mp (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (= i k3))) (@cong (@refl (not (= i k3))) (@rewrite (! (= (= i k3) (! (= i k3) :quotedCC)) :intern)))) (! (not (! (= i k3) :quotedCC)) :input B)) :pivot (not (! (= i k3) :quotedCC))) (! (@clause (@mp (@mp (@split (! (@split (! (@split (! (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) :notOr) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notOr) (not (or (not (= i j)) (= (select a i) (select b j))))) :notOr) (not (not (= i j)))) (@rewrite (! (= (not (not (= i j))) (= i j)) :notSimp))) (@rewrite (! (= (= i j) (! (= i j) :quotedCC)) :intern))) (! (! (= i j) :quotedCC) :input B)) :pivot (! (= i j) :quotedCC))) :pivot (not (! (= j k3) :quotedCC))) (! (@clause (@mp (@split (! (@split (! (@split (! (@split (! (@mp (@asserted (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B)) (@trans (@rewrite (! (= (! (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) :named B) (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) :strip)) (@cong (@trans (@cong (@refl (and (not (= i k3)) (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))))) (@cong (@trans (@cong (@refl (and (= a (store s1 k1 v1)) (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j))))))) (@cong (@trans (@cong (@refl (and (= b (store s2 k3 v3)) (and (= i j) (not (= (select a i) (select b j)))))) (@cong (@rewrite (! (= (and (= i j) (not (= (select a i) (select b j)))) (not (or (not (= i j)) (not (not (= (select a i) (select b j))))))) :andToOr)) (@cong (@refl (or (not (= i j)) (not (not (= (select a i) (select b j)))))) (@rewrite (! (= (not (not (= (select a i) (select b j)))) (= (select a i) (select b j))) :notSimp))))) (@rewrite (! (= (and (= b (store s2 k3 v3)) (not (or (not (= i j)) (= (select a i) (select b j))))) (not (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j)))))))) :andToOr))) (@cong (@refl (or (not (= b (store s2 k3 v3))) (not (not (or (not (= i j)) (= (select a i) (select b j))))))) (@rewrite (! (= (not (not (or (not (= i j)) (= (select a i) (select b j))))) (or (not (= i j)) (= (select a i) (select b j)))) :notSimp))))) (@rewrite (! (= (and (= a (store s1 k1 v1)) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (not (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) :andToOr))) (@cong (@refl (or (not (= a (store s1 k1 v1))) (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))) (@rewrite (! (= (not (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))) :notSimp))))) (@rewrite (! (= (and (not (= i k3)) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (not (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))))))) :andToOr))) (@cong (@refl (or (not (not (= i k3))) (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))))) (@rewrite (! (= (not (not (= i k3))) (= i k3)) :notSimp)) (@rewrite (! (= (not (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notSimp)))))) :notOr) (not (or (not (= a (store s1 k1 v1))) (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j))))))) :notOr) (not (or (not (= b (store s2 k3 v3))) (or (not (= i j)) (= (select a i) (select b j)))))) :notOr) (not (or (not (= i j)) (= (select a i) (select b j))))) :notOr) (not (= (select a i) (select b j)))) (@cong (@refl (not (= (select a i) (select b j)))) (@rewrite (! (= (= (select a i) (select b j)) (! (= (select a i) (select b j)) :quotedCC)) :intern)))) (! (not (! (= (select a i) (select b j)) :quotedCC)) :input B)) :pivot (not (! (= (select a i) (select b j)) :quotedCC)))) + +Simplified and structured: + +(@res + (@lemma (! (or (! (= (select a i) (select b j)) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= b (store s2 k3 v3)) :quotedCC)) (! (= j k3) :quotedCC) (! (= j k2) :quotedCC) (not (! (= s1 (store s2 k2 v2)) :quotedCC)) (! (= j k1) :quotedCC) (not (! (= a (store s1 k1 v1)) :quotedCC))) :read-over-weakeq ( ... ))) + (! (@res + (@lemma (! (or (! (= i k1) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= j k1) :quotedCC))) :CC ( ... ))) + (! (@clause ( ... ) (! (not (! (= i k1) :quotedCC)) :input A)) + :pivot (not (! (= i k1) :quotedCC))) + (! (@clause ( ... ) (! (! (= i j) :quotedCC) :input B)) + :pivot (! (= i j) :quotedCC))) + :pivot (not (! (= j k1) :quotedCC))) + (! (@clause ( ... ) (! (! (= b (store s2 k3 v3)) :quotedCC) :input B)) + :pivot (! (= b (store s2 k3 v3)) :quotedCC)) + (! (@clause ( ... ) (! (! (= a (store s1 k1 v1)) :quotedCC) :input B)) + :pivot (! (= a (store s1 k1 v1)) :quotedCC)) + (! (@res + (@lemma (! (or (! (= i k2) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= j k2) :quotedCC))) :CC ( ... ))) + (! (@clause ( ... ) (! (not (! (= i k2) :quotedCC)) :input A)) + :pivot (not (! (= i k2) :quotedCC))) + (! (@clause ( ... ) (! (! (= i j) :quotedCC) :input B)) + :pivot (! (= i j) :quotedCC))) + :pivot (not (! (= j k2) :quotedCC))) + (! (@clause ( ... ) (! (! (= s1 (store s2 k2 v2)) :quotedCC) :input A)) + :pivot (! (= s1 (store s2 k2 v2)) :quotedCC)) + (! (@clause ( ... ) (! (! (= i j) :quotedCC) :input B)) + :pivot (! (= i j) :quotedCC)) + (! (@res + (@lemma (! (or (! (= i k3) :quotedCC) (not (! (= i j) :quotedCC)) (not (! (= j k3) :quotedCC))) :CC ( ... ))) + (! (@clause ( ... ) (! (not (! (= i k3) :quotedCC)) :input B)) + :pivot (not (! (= i k3) :quotedCC))) + (! (@clause ( ... ) (! (! (= i j) :quotedCC) :input B)) + :pivot (! (= i j) :quotedCC))) + :pivot (not (! (= j k3) :quotedCC))) + (! (@clause ( ... ) (! (not (! (= (select a i) (select b j)) :quotedCC)) :input B)) + :pivot (not (! (= (select a i) (select b j)) :quotedCC)))) + +-------------------------------------------------------------------------------- + +SMT-LIB für die ersten 3 Beweise + +(set-option :produce-interpolants true) +(set-option :print-terms-cse false) +(set-logic ALL) + +(push 1) +(assert (= 0 1)) +(check-sat) +(get-proof) +(pop 1) + +(push 1) +(declare-fun p () Bool) +(assert p) +(assert (not p)) +(check-sat) +(get-proof) +(pop 1) + +(push 1) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (< a b)) +(assert (< b a)) +(check-sat) +(get-proof) +(pop 1) + +(exit) + +-------------------------------------------------------------------------------- + diff --git a/Webinterface/src/main/visualizer/textparser_and_resolver.js b/Webinterface/src/main/visualizer/textparser_and_resolver.js new file mode 100644 index 000000000..768371e83 --- /dev/null +++ b/Webinterface/src/main/visualizer/textparser_and_resolver.js @@ -0,0 +1,455 @@ +// Set global counters and the global array for the nodes that will be made into a tree. +let root_node; +let all_nodes; +let node_counter; +let text_pos; +let text; + +// Class for nodes and leafs with ids, the text in each node/leaf, ids of parents and children +// (the root node has parent_id = -1) and the info if it is a leaf or not. +class Node { + constructor() { + this.node_id = node_counter; + this.node_text = []; + this.children = []; + this.parent_id = -1; + this.is_leaf = false; + this.node_literals = new Set(); + this.node_pivot = ""; + // Intermediate_result is the resolution of the current nodes children with their literals and pivots. + this.intermediate_result = new Set(); + } + toString() { + return "[" + this.node_id + ", " + this.node_text + ", [" + this.children + "], " + this.parent_id + ", \n" + this.is_leaf + ", {" + Array.from(this.node_literals) + "}, \n" + this.node_pivot + ", " + Array.from(this.intermediate_result) + "]"; + } +} + +// The next extract-functions are for extracting the literals and pivots from their respective node_texts. + +// Extracting the literals from the lemma-string so that they can be +// resolved with the other literals later on. +function extract_literals_lemma(lemma) { + let literals = new Set(); + let pivot = ""; + let lemma_text_pos = 0; + let lemma_literal = ""; + let open = 0; + let close = 0; + while (lemma_text_pos < lemma.length) { + if (lemma.startsWith("or", lemma_text_pos)) { + while (lemma_text_pos < lemma.length) { + if (lemma[lemma_text_pos] == '(') { + open++; + } + if (open > close) { + lemma_literal += lemma[lemma_text_pos]; + } + if (lemma[lemma_text_pos] == ')') { + close++; + } + if (open === close && lemma_literal !== "") { + literals.add(lemma_literal); + lemma_literal = ""; + if (lemma.startsWith(") :", lemma_text_pos + 1)) { + lemma_text_pos = lemma.length; + } + } + lemma_text_pos++; + } + } + lemma_text_pos++; + } + return literals; +} + +// Extracting the pivot from the given clause or lemma +function extract_pivot(text) { + let pivot = ""; + let open = 0; + let close = 0; + let text_pos = 0; + let splitted_text = text.split(":pivot ")[1]; + // If pivot is in parenthesis + if (splitted_text[text_pos] == "(") { + while (text_pos < splitted_text.length) { + if (splitted_text[text_pos] == '(') { + open++; + } + if (open > close) { + pivot += splitted_text[text_pos]; + } + if (splitted_text[text_pos] == ')') { + close++; + } + if (open === close) { + break; + } + text_pos++; + } + } else { // Pivot without parenthesis + while (text_pos < splitted_text.length) { + if (splitted_text[text_pos] == ')') { + break; + } + pivot += splitted_text[text_pos]; + text_pos++; + } + } + return pivot; +} + +function get_parenthesised_clause_literal(clause, text_position) { + let clause_literal = ""; + let open = 0; + let close = 0; + while (text_position < clause.length) { + if (clause[text_position] == '(') { + open++; + } + if (open > close) { + clause_literal += clause[text_position]; + } + if (clause[text_position] == ')') { + close++; + } + if (open === close) { + if (clause_literal == "") { + throw new Error("Literal is empty."); + } + return clause_literal; + } + text_position++ + } +} + +function get_non_parenthesised_clause_literal(clause, text_position) { + let clause_literal = ""; + while (text_position < clause.length) { + if (clause[text_position] == ")" || clause[text_position] == " ") { + if (clause_literal == "") { + throw new Error("Literal is empty."); + } + return clause_literal; + } + if (clause[text_position] !== "") { + clause_literal += clause[text_position]; + } + text_position++; + } +} + +// Extracting the literals from the clause-string so that they can be +// resolved with the other literals later on. +function extract_literals_clause(clause) { + let literals = new Set(); + let pivot = ""; + let clause_text_pos = 0; + let open = 0; + let close = 0; + let is_parenthesis_ignored = false; + while (clause_text_pos < clause.length) { + // Start after "(@clause " or "(! (@clause " + if (clause.startsWith("@clause ", clause_text_pos)) { + clause_text_pos += 8; + // Completely ignore the next parenthesis + if (is_parenthesis_ignored == false) { + if (clause[clause_text_pos] == "(") { + open++; + clause_text_pos++; + while (open > close) { + if (clause[clause_text_pos] == '(') { + open++; + } + if (clause[clause_text_pos] == ')') { + close++; + } + if (open === close) { + break; + } + clause_text_pos++; + } + is_parenthesis_ignored = true; + clause_text_pos += 5; // Ignore " (! " that comes right after the to be ignored parenthesis + } + } + } + if (is_parenthesis_ignored) { + // If there are at least 2 literals then there is alway an "(or " + if (clause.startsWith("(or ", clause_text_pos)) { + clause_text_pos += 4; // Jump behind "(or " + while (clause_text_pos < clause.length) { + if (clause.startsWith(" :input", clause_text_pos)) { + clause_text_pos = clause.length; + break + } + // If the literal is in parenthesis + if (clause[clause_text_pos] == "(") { + let clause_literal = get_parenthesised_clause_literal(clause, clause_text_pos); + literals.add(clause_literal); + clause_text_pos += (clause_literal.length); + } // If the literal is without parenthesis + else if (clause[clause_text_pos] !== "(" && clause[clause_text_pos] !== " ") { + let clause_literal = get_non_parenthesised_clause_literal(clause, clause_text_pos); + literals.add(clause_literal); + clause_text_pos += (clause_literal.length); + } + clause_text_pos++; + } + } + // If there is no "(or " then there is only one literal. + // For a literal with parenthesis: + else if (clause[clause_text_pos] == "(") { + let clause_literal = get_parenthesised_clause_literal(clause, clause_text_pos); + literals.add(clause_literal); + clause_text_pos += (clause_literal.length); + if (clause.startsWith(" :input", clause_text_pos)) { + clause_text_pos = clause.length; + break; + } + } else if (clause[clause_text_pos] !== " " || clause[clause_text_pos] !== "") { + // For a literal without parenthesis: + let clause_literal = get_non_parenthesised_clause_literal(clause, clause_text_pos); + literals.add(clause_literal); + clause_text_pos += (clause_literal.length); + if (clause.startsWith(" :input", clause_text_pos)) { + clause_text_pos = clause.length; + break; + } + } + } + clause_text_pos++; + } + return literals; +} + +function extract_literals(text) { + if (text.includes("lemma")) { + return extract_literals_lemma(text); + } + if (text.includes("clause")) { + return extract_literals_clause(text); + } +} + +// A function for parsing the text for the leafs of the (syntax) tree that will be created later. +function parseLeaf() { + let newStr = [], + open = 0, + close = 0; + // Beginning of new leaf found, so start new "node" with id number and empty text. + // Child and parent ids will be recursively added later. + let node = new Node(); + node.is_leaf = true; + node_counter++; + // Count the brackets to see if the expression is completed and save the text in newStr. + while (text_pos < text.length) { + if (text[text_pos] == '(') { + open++; + } + if (open > close) { + newStr += text[text_pos]; + } + if (text[text_pos] == ')') { + close++; + } + text_pos++; + if (open === close) { + break; + } + } + // Assign the found text to the newly created leaf. + node.node_text = newStr; + node.node_literals = extract_literals(newStr); + if (newStr.includes(":pivot")) { + node.node_pivot = extract_pivot(newStr); + } + all_nodes.push(node); + return node; +} + +// A function for parsing the text for the nodes of the (syntax) tree that will be created later. +function parseNode() { + let newStr = [], + open = 0, + close = 0; + // Beginning of new leaf found, so start new "node" with id number and empty text. + // Child and parent ids will be added later. + let node = new Node(); + node.is_leaf = false; + node_counter++; + // The starting text of the proof, where a node is found can directly be added to the + // created node-object and therefore the found opening brackets can already be counted + // and also the text position needs to be adjusted. + if (text.startsWith('(@res', text_pos)) { + open++; + text_pos += 6; + newStr += "(@res "; + } else if (text.startsWith('(! (@res ', text_pos)) { + open += 2; + text_pos += 9; + newStr += "(! (@res "; + } + while (text_pos < text.length) { + // If another keyword is found inside the res-node (so if there are children) + // we recursively go through these children first and get back to the parent(s) afterwards. + // Here the current node_id needs to be set to the next child's parent_id + // and the child_id of the "node" needs to be filled with the ids of all children. + if (text.startsWith("(! (@res", text_pos) || text.startsWith("(@res", text_pos) || text.startsWith("(! (@clause", text_pos) || text.startsWith("(! (@lemma", text_pos) || text.startsWith("(@clause", text_pos) || text.startsWith("(@lemma", text_pos)) { + let child = smt_parser(); + child.parent_id = node.node_id; + node.children.push(child); + newStr += child.node_id; + } + // Count the brackets to see if the expression is completed and save the text in newStr. + if (text[text_pos] == '(') { + open++; + } + if (open > close) { + newStr += text[text_pos]; + } + if (text[text_pos] == ')') { + close++; + } + text_pos++; + if (open === close) { + break; + } + } + // Save the resolved result of the nodes children in intermediate_result. + // This will be used later for building up our (syntax) tree. + node.node_literals = compute_literals_res_node(node.children); + if (newStr.includes(":pivot ")) { + node.node_pivot = extract_pivot(newStr); + } + // Assign the found text to the newly created node. + node.node_text += newStr; + all_nodes.push(node); + return node; +} + +// The complete parser for leafs and nodes. +function smt_parser() { + for (; text_pos < text.length; text_pos++) { + if (text.startsWith("(! (@res", text_pos) || text.startsWith("(@res", text_pos)) { + return parseNode(); + } else if (text.startsWith("(! (@clause", text_pos) || text.startsWith("(! (@lemma", text_pos) || text.startsWith("(@clause", text_pos) || text.startsWith("(@lemma", text_pos)) { + return parseLeaf(); + } + } + // If there is no proof text, we return an empty node. + let empty_node = new Node(); + return empty_node; +} + +// Recursively compute the literals for the res-nodes and their children. +function compute_literals_res_node(children) { + let left_clause = Array.from(children[0].node_literals); + let right_clause = Array.from(children[1].node_literals); + let child_pivot = children[1].node_pivot; + for (var i = 1; i < children.length; i++) { + children[i].intermediate_result = compute_res(left_clause, right_clause, child_pivot); + left_clause = Array.from(children[i].intermediate_result); + if (children[i + 1]) { + right_clause = Array.from(children[i + 1].node_literals); + child_pivot = children[i + 1].node_pivot; + } + } + return new Set(left_clause); +} + +// Take the given pivot and negate it. +// So either put a "(not )" around the pivot or just take the inner part of the +// "(not (pivot))" string. +function negate_pivot(pivot) { + let negated_pivot; + if (pivot.startsWith("(not")) { + negated_pivot = pivot.slice(5, -1); + } else { + negated_pivot = "(not " + pivot + ")"; + } + return negated_pivot; +} + +// Compute the resolution of 2 clauses and a pivot. +// pivot_found = 0 (pivot not found), = 1 (pivot found), = -1 (negated pivot found) +function compute_res(resolve_literals_1, resolve_literals_2, resolve_pivot) { + let resolution = new Set(); + let pivot_found = 0; + let resolve_literals_1_array = Array.from(resolve_literals_1); + let resolve_literals_2_array = Array.from(resolve_literals_2); + let negated_resolve_pivot = negate_pivot(resolve_pivot) + for (var i = 0; i < resolve_literals_1_array.length; i++) { + if (resolve_literals_1_array[i] === resolve_pivot) { + pivot_found = 1; + } else if (resolve_literals_1_array[i] === negated_resolve_pivot) { + pivot_found = -1; + } else { + resolution.add(resolve_literals_1_array[i]); + } + } + if (pivot_found === 0) { + throw new Error("There is neither a pivot nor a negated pivot found in our left clause."); + } + let opposite_pivot = false; + for (var i = 0; i < resolve_literals_2_array.length; i++) { + if (pivot_found === 1 && resolve_literals_2_array[i] === negated_resolve_pivot) { + opposite_pivot = true; + } else if (pivot_found === -1 && resolve_literals_2_array[i] === resolve_pivot) { + opposite_pivot = true; + } else { + resolution.add(resolve_literals_2_array[i]); + } + } + if (opposite_pivot === false) { + throw new Error("There is no negated pivot found in the right clause."); + } + return resolution; +} + +// This will be the function for the complete visualization proof. +// It will parse through the given proof text and create a (syntax) tree. +function visualize_proof(input) { + text_pos = 0; + node_counter = 0; + all_nodes = []; + text = input; + root_node = smt_parser(); + return all_nodes; // For testing +} + +function create_tree(current_node, parent_id) { + if (current_node.children.length !== 0) { + let node_id = "node" + current_node.node_id; + document.getElementById(parent_id).innerHTML += '
  • {' +Array.from(current_node.node_literals) +'} ' + +current_node.node_pivot+' {'+Array.from(current_node.intermediate_result)+'}
    • '; + for (var i = 0; i < current_node.children.length; i++) { + create_tree(current_node.children[i], node_id); + } + } else if (current_node.children.length === 0) { + let node_id = "node" + current_node.node_id; + document.getElementById(parent_id).innerHTML += '
  • {' + Array.from(current_node.node_literals)+'} ' + +current_node.node_pivot+' {'+Array.from(current_node.intermediate_result)+'}
    • '; + } +} + +// Create a tree with the resolved literals so that the literals, pivots and +// intermediate results before each resolution step will be shown. +window.onload = function() { + var visualize_button = document.getElementById("visualizer"); + visualize_button.addEventListener("click", function() { + document.getElementById("mytree").innerHTML = ''; + document.getElementById("legend").style.display = "inline-block"; + visualize_button.innerHTML = "SMT proof started"; + let proof_input = document.getElementById("input_text").value; + visualize_proof(proof_input); + document.querySelector("button").style.color = "darkred"; + create_tree(root_node, "mytree"); + var toggler = document.getElementsByClassName("arrow"); + for (var i = 0; i < toggler.length; i++) { + toggler[i].addEventListener("click", function() { + this.parentElement.querySelector(".nested").classList.toggle("active"); + this.classList.toggle("arrow-down"); + }); + } + }); +} diff --git a/Webinterface/src/main/visualizer/tree.css b/Webinterface/src/main/visualizer/tree.css new file mode 100644 index 000000000..8bbe5ccba --- /dev/null +++ b/Webinterface/src/main/visualizer/tree.css @@ -0,0 +1,110 @@ +body { + font-family: sans-serif; +} + +ul, .tree { + list-style-type: none; +} + +#input_text{ + border-radius: 5px; + display: inline-block; + padding: 3px 8px; + margin: 10px; +} + +#visualizer { + border-radius: 5px; + display: inline-block; + padding: 3px 8px; + margin: 10px; +} + +.tree { + min-height: 20px; + padding: 19px; + margin-bottom: 20px; +} + +.tree li { + padding: 10px 5px 0 5px; +} + +.tree li span { + border-radius: 5px; + display: inline-block; + padding: 4px 8px; +} + +.box { + cursor: pointer; + -webkit-user-select: none; + /* Safari 3.1+ */ + -moz-user-select: none; + /* Firefox 2+ */ + -ms-user-select: none; + /* IE 10+ */ + user-select: none; +} + +.box::before { + content: "\2610"; + color: black; + display: inline-block; + margin-right: 6px; +} + +.check-box::before { + content: "\2611"; + color: dodgerblue; +} + +.arrow { + cursor: pointer; + user-select: none; +} + +.arrow::before { + content: "\25B6"; + color: black; + display: inline-block; + margin-right: 6px; +} + +.arrow-down::before { + -ms-transform: rotate(90deg); + /* IE 9 */ + -webkit-transform: rotate(90deg); + /* Safari */ + ' +transform: rotate(90deg); +} + +.nested { + display: none; +} + +.active { + display: block; +} + +.node_literals { + color: green; + border: 1px solid green; +} + +.node_pivot { + color: black; + border: 1px solid black; +} + +.intermediate_result { + color: dodgerblue; + border: 1px solid dodgerblue; +} + +#legend { + margin-top: 20px; + margin-left: 20px; + display: none; +} diff --git a/Webinterface/src/main/visualizer/tree.html b/Webinterface/src/main/visualizer/tree.html new file mode 100644 index 000000000..b2f122abb --- /dev/null +++ b/Webinterface/src/main/visualizer/tree.html @@ -0,0 +1,46 @@ + + + + + + + + SMT Proof Tree + + + + +
    + +
    +

    Clause + Pivot + Intermediate result

    + + + + + + From 9af6a6d8847fd88e8e92872e15aa4f41b95b23a1 Mon Sep 17 00:00:00 2001 From: Steve_Freecastler Date: Tue, 25 Jan 2022 14:24:49 +0100 Subject: [PATCH 2/3] English header --- Webinterface/doc/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Webinterface/doc/README.md b/Webinterface/doc/README.md index 04545481f..2742210fa 100644 --- a/Webinterface/doc/README.md +++ b/Webinterface/doc/README.md @@ -1,5 +1,5 @@ -# SMT-Beweisvisualisierung -Beweisvisualisierung für vorhandenen SMT-Solver +# SMT-proof visualisation +Proof visualisation for given SMT-Solver Manual: From e05ebe0e4bff611c9f27847682dec479c85b4b88 Mon Sep 17 00:00:00 2001 From: Steve_Freecastler Date: Sun, 13 Feb 2022 18:15:24 +0100 Subject: [PATCH 3/3] Pivots will only be shown if available. @lemma, @clause and inner node literals will be shown in different colours --- .../visualizer/textparser_and_resolver.js | 54 ++++++++++++++++--- Webinterface/src/main/visualizer/tree.css | 15 ++++-- Webinterface/src/main/visualizer/tree.html | 8 ++- 3 files changed, 66 insertions(+), 11 deletions(-) diff --git a/Webinterface/src/main/visualizer/textparser_and_resolver.js b/Webinterface/src/main/visualizer/textparser_and_resolver.js index 768371e83..c8c39c5b2 100644 --- a/Webinterface/src/main/visualizer/textparser_and_resolver.js +++ b/Webinterface/src/main/visualizer/textparser_and_resolver.js @@ -16,6 +16,8 @@ class Node { this.is_leaf = false; this.node_literals = new Set(); this.node_pivot = ""; + this.is_lemma_node = false; + this.is_clause_node = false; // Intermediate_result is the resolution of the current nodes children with their literals and pivots. this.intermediate_result = new Set(); } @@ -222,11 +224,13 @@ function extract_literals_clause(clause) { return literals; } -function extract_literals(text) { +function extract_literals(text, node) { if (text.includes("lemma")) { + node.is_lemma_node = true; return extract_literals_lemma(text); } if (text.includes("clause")) { + node.is_clause_node = true; return extract_literals_clause(text); } } @@ -259,7 +263,7 @@ function parseLeaf() { } // Assign the found text to the newly created leaf. node.node_text = newStr; - node.node_literals = extract_literals(newStr); + node.node_literals = extract_literals(newStr, node); if (newStr.includes(":pivot")) { node.node_pivot = extract_pivot(newStr); } @@ -420,15 +424,19 @@ function visualize_proof(input) { function create_tree(current_node, parent_id) { if (current_node.children.length !== 0) { let node_id = "node" + current_node.node_id; - document.getElementById(parent_id).innerHTML += '
  • {' +Array.from(current_node.node_literals) +'} ' - +current_node.node_pivot+' {'+Array.from(current_node.intermediate_result)+'}
      • '; + let current_pivot = check_pivot_availability(current_node); + let current_literal = check_node_literal_lemma_clause(current_node); + document.getElementById(parent_id).innerHTML += current_literal+current_pivot+ + ' {'+Array.from(current_node.intermediate_result)+'}
        '; for (var i = 0; i < current_node.children.length; i++) { create_tree(current_node.children[i], node_id); } } else if (current_node.children.length === 0) { let node_id = "node" + current_node.node_id; - document.getElementById(parent_id).innerHTML += '
      • {' + Array.from(current_node.node_literals)+'} ' - +current_node.node_pivot+' {'+Array.from(current_node.intermediate_result)+'}
        • '; + let current_pivot = check_pivot_availability(current_node); + let current_literal = check_leaf_literal_lemma_clause(current_node); + document.getElementById(parent_id).innerHTML += current_literal+current_pivot+ + ' {'+Array.from(current_node.intermediate_result)+'}'; } } @@ -453,3 +461,37 @@ window.onload = function() { } }); } + +// Check if pivot is available and either return it or just the bracket to close +// the node_literals array in the string for the html site +function check_pivot_availability(node) { + if (node.node_pivot) { + let str1 = '} '; + let str2 = node.node_pivot; + return str1+str2; + } else { + return "}"; + } +} + +// Check if literal of the leaf contains @lemma or @clause to highlight it later +function check_leaf_literal_lemma_clause(node) { + if (node.is_lemma_node) { + return '
      • {' + Array.from(node.node_literals); + } else if (node.is_clause_node) { + return '
      • {' + Array.from(node.node_literals); + } else { + return '
      • {' + Array.from(node.node_literals); + } +} + +// Check if literal of the node contains @lemma or @clause to highlight it later +function check_node_literal_lemma_clause(node) { + if (node.is_lemma_node) { + return '
      • {' +Array.from(node.node_literals); + } else if (node.is_clause_node) { + return '
      • {' +Array.from(node.node_literals); + } else { + return '
      • {' +Array.from(node.node_literals); + } +} diff --git a/Webinterface/src/main/visualizer/tree.css b/Webinterface/src/main/visualizer/tree.css index 8bbe5ccba..88d993e55 100644 --- a/Webinterface/src/main/visualizer/tree.css +++ b/Webinterface/src/main/visualizer/tree.css @@ -76,8 +76,7 @@ ul, .tree { /* IE 9 */ -webkit-transform: rotate(90deg); /* Safari */ - ' -transform: rotate(90deg); + transform: rotate(90deg); } .nested { @@ -88,11 +87,21 @@ transform: rotate(90deg); display: block; } -.node_literals { +.inner_node_literals { color: green; border: 1px solid green; } +.clause_literals { + color: purple; + border: 1px solid purple; +} + +.lemma_literals { + color: orange; + border: 1px solid orange; +} + .node_pivot { color: black; border: 1px solid black; diff --git a/Webinterface/src/main/visualizer/tree.html b/Webinterface/src/main/visualizer/tree.html index b2f122abb..77757014d 100644 --- a/Webinterface/src/main/visualizer/tree.html +++ b/Webinterface/src/main/visualizer/tree.html @@ -13,9 +13,13 @@

        -

        Clause +

        + Inner node literals + Clause literals + Lemma literals Pivot - Intermediate result

        + Intermediate result +