Proof visualizer

Webinterface/doc/README.md

@@ -0,0 +1,40 @@
+# SMT-proof visualisation
+Proof visualisation for given 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.

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