From bcdabb4fc4e04754d533c230f31444bd477c0303 Mon Sep 17 00:00:00 2001 From: AFellner Date: Fri, 9 May 2014 22:55:40 +0200 Subject: [PATCH] Introduce EqW class as a wrapper for equalities and add comments to CCR, congruence and CongruenceCompressor --- .../skeptik/algorithm/congruence/CCR.scala | 20 +- .../algorithm/congruence/Congruence.scala | 222 ++++---- .../congruence/CongruenceCompressor.scala | 157 +++--- .../skeptik/algorithm/congruence/EqW.scala | 106 ++++ .../skeptik/algorithm/dijkstra/Dijkstra.scala | 9 +- .../skeptik/algorithm/dijkstra/PathTree.scala | 231 ++++----- .../skeptik/algorithm/dijkstra/package.scala | 6 +- .../skeptik/expression/formula/formulas.scala | 136 +++-- .../skeptik/proof/sequent/lk/Congruence.scala | 76 +-- .../at/logic/skeptik/proof/sequent/lk/R.scala | 6 +- .../skeptik}/congruence/CongruenceTest.scala | 0 .../at/logic/skeptik/congruence/EqWTest.scala | 25 + .../congruence/EquationsExperiment.scala | 478 +++++++++--------- 13 files changed, 786 insertions(+), 686 deletions(-) create mode 100644 src/main/scala/at/logic/skeptik/algorithm/congruence/EqW.scala rename src/{main/scala/at/logic/skeptik/algorithm => test/scala/at/logic/skeptik}/congruence/CongruenceTest.scala (100%) create mode 100644 src/test/scala/at/logic/skeptik/congruence/EqWTest.scala diff --git a/src/main/scala/at/logic/skeptik/algorithm/congruence/CCR.scala b/src/main/scala/at/logic/skeptik/algorithm/congruence/CCR.scala index 2386bfad..878b0f80 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/congruence/CCR.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/congruence/CCR.scala @@ -6,16 +6,22 @@ import scala.collection.mutable.ListBuffer import scala.collection.mutable.{HashSet => MSet} import scala.collection.immutable.{HashSet => ISet} +/** + * Class CCR + * is immutable + * stands for congruence class record - as in Pascal Fontaine's PhD Thesis. + * represents one congruence class + * + * @param initterm initial term of the CCR + * @param s representative of the CCR (not yet used really) + * @param term set of terms in this congruence class + * @param pred set of terms where some term in this congruence class is an argument + * @param rightNeighbours forgot what I used that for, probably can be removed + */ class CCR(val initTerm: E, val s: E, val term: Set[E], val pred: Set[E], val rightNeighbours: Set[E]) { -// var s: E = initTerm -// val term: ListBuffer[E] = ListBuffer(initTerm) -// val pred: ListBuffer[E] = ListBuffer() + def this(initTerm: E) = this(initTerm, initTerm, Set(initTerm), Set[E](), Set[E]()) -// term.+=(initTerm) - override def toString: String = "["+s.toString+"]" + "{"+term+"}" } - -//object DummyCCR extends CCR \ No newline at end of file diff --git a/src/main/scala/at/logic/skeptik/algorithm/congruence/Congruence.scala b/src/main/scala/at/logic/skeptik/algorithm/congruence/Congruence.scala index 57bbd779..7c7975c7 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/congruence/Congruence.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/congruence/Congruence.scala @@ -10,54 +10,52 @@ import scala.collection.mutable.Stack import scala.collection.immutable.Queue import scala.collection.mutable.ListBuffer -//type pT = Option[PathTree[E,Option[PathTree[E]]]] - -//trait recType { -// type X <: PathTree[E,Option[(X,X)]] -// type Z = String -//} - -//bla[PathTree[E,]] +/** + * Class Congruence class is for computing and maintaining the congruence closure of some input equations + * equations can be entered incrementally and on entering an equation CCRs will be created and/or merged + * is immutable + * + * @param eqReferences Map for keeping track of the objects that represent the equalities between tuples of expressions + * @param find Table for relating terms with their CCR + * @param deduced List of deduced equalities, for which new explanations can be computed on demand + * @param g Graph representing the congruence closure + */ class Congruence( - val eqReferences: MMap[(E,E),App], + val eqReferences: MMap[(E,E),EqW], val find: FindTable = new FindTable(), - val sigTable: SignatureTable = new SignatureTable(), val deduced: Queue[(E,E)] = Queue[(E,E)](), val g: WGraph[E,EqLabel] = new WGraph[E,EqLabel]()) { - // val find = new FindTable() -// val sigTable = new SignatureTable() -// val eqTriples = new Map[E,(E,E,App)] //this structure is good for comparing to inequalities -//// val transitivityTripples = new -// val deduce1d = Queue[(E,E)]() -// -// var g = new WGraph[E,Set[App]]() - -// def copy = - + /** + * the following methods are create new Congruence objects, when one of their parameters is changed + */ def updateFind(newFind: FindTable) = { - new Congruence(eqReferences, newFind, sigTable,deduced,g) - } - def updateSigTable(newSigTable: SignatureTable) = { - new Congruence(eqReferences, find, newSigTable,deduced,g) + new Congruence(eqReferences, newFind,deduced,g) } -// def updateEqReferences(newEqReferences: MMap[(E,E),App]) = { -// new Congruence(find, sigTable, newEqReferences,deduced,g) -// } + def updateDeduced(newDeduced: Queue[(E,E)]) = { - new Congruence(eqReferences, find, sigTable,newDeduced,g) + new Congruence(eqReferences, find,newDeduced,g) } def updateGraph(newG: WGraph[E,EqLabel]) = { - new Congruence(eqReferences, find, sigTable,deduced,newG) + new Congruence(eqReferences, find,deduced,newG) } - def addAll(eqs: List[App]): Congruence = { - eqs.foldLeft(this)({(A,B) => A.addEquality(B)}) - } + + /** + * method for adding an equation to the this congruence closure + * calls addNode for both sides of the equality + * calls merge with the two sides + * adds edge labeled with the equality and weight 1 to the graph + * + * see page 188 in Pascal's work + * + * @param eq equality to be added represented as an EqW object + * @result new congruence data structure with eq added + */ - def addEquality(eq: App): Congruence = { - val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument) + def addEquality(eq: EqW): Congruence = { + val (l,r) = (eq.l,eq.r) val eqRef = eqReferences.update((l,r), eq) // val c0 = updateEqReferences(eqRef) val c1 = this.addNode(l) @@ -67,17 +65,26 @@ class Congruence( res } + /** + * method addNode adds a term into the congruence closure structure + * checks the findmap for entry u does nothing when u has an entry + * adds u and all its subterms to the congruence structure + * queries for signature equality and deduces new equalities + * + * see page 189 in Pascal's work + * + * @param u expression to add to the structure + * @result new congruence structure with u an its subterms added + */ //find query creates new CCR before subterms are added //order matters??? def addNode(u: E): Congruence = { val uRepr = find.map.get(u) uRepr match { case Some(_) => { -// println("come here when adding " + u) this } case None => { -// println("come there when adding " + u) val c2 = u match { case App(v1,v2) => { @@ -102,8 +109,7 @@ class Congruence( val nF = newFind.addPred(v1, u) val nF2 = nF.addPred(v2, u) val c4 = c3.updateFind(nF2) - val (finalSig,finalFind) = c4.sigTable.enter(u,c4.find) - c4.updateFind(finalFind).updateSigTable(finalSig) + c4 } } } @@ -113,22 +119,47 @@ class Congruence( } } - def merge(a: E, b: E, eq: Option[App]): Congruence = { + /** + * method for adding lists of equations + */ + def addAll(eqs: List[EqW]): Congruence = { + eqs.foldLeft(this)({(A,B) => A.addEquality(B)}) + } + + /** + * merges the CCRs of two by calling union of these terms + * recursively merges deduced equalities of union + * + * see page 190 in Pascal's work + * + * @param a,b expression to be merged + * @param eq equality as reason for merge + * @result new congruence structure with CCRs merged + + */ + def merge(a: E, b: E, eq: Option[EqW]): Congruence = { val (nF,aF,bF) = find.queryTwo(a, b) val c1 = updateFind(nF) if (aF != bF) { val (c2, deduced) = c1.union(a,b) deduced.foldLeft(c2)({(A,B) => val d = A.resolveDeduced(B._1, B._2) -// println("Deducing " + B._1 + " = " + B._2 + " in merge") d.merge(B._1, B._2, None) }) } else c1 } + /** + * union actually performs the merge by altering CCRs and the findMap + * calls sigQuery to deduce new equalities + * + * see page 191 in Pascal's work + * + * @param u,v expressions which CRRs should be merged + * @res new congruence structure with u,v merged and list of deduced equalities + */ def union(u: E, v: E): (Congruence,ListBuffer[(E,E)]) = { -// println("union: " + (u,v)) val (nF,a) = find.query(u) val (nF2,b) = nF.query(v) @@ -141,7 +172,6 @@ class Congruence( val nF6 = remain.term.foldLeft(nF5)({(A,B) => A.update(B, remain)}) val c1 = updateFind(nF6) -// println("after union of " + (u,v) + " their finds: " + (c1.find.map(u),c1.find.map(v))) val c2 = removeCCR.pred.foldLeft(c1)({(A,B) => val s = A.find.sigQuery(B) s match { @@ -150,32 +180,41 @@ class Congruence( A.addDeduced(B, q) } case None => { - val (finalSig,finalFind) = A.sigTable.enter(B,A.find) - A.updateFind(finalFind).updateSigTable(finalSig) + A } } }) (c2,deduct) } + /** + * adds one deduced equality to the Queue of deduced equalities + */ def addDeduced(u: E, v: E): Congruence = { -// println("adding " + (u,v)) updateDeduced(deduced.enqueue((u,v))) } + /** + * resolves all queued up equalities by finding an explanation for them in the current graph + */ def resolveDeducedQueue: Congruence = { deduced.foldLeft(this)((A,B) => { -// val (pair,newQueue) = A.deduced.dequeue val c = A.resolveDeduced(B._1,B._2) -// c.updateDeduced(newQueue) -// println("resolving " + B) c }) } + /** + * resolves one given equality by finding an explanation for it in the current graph + * and adding an edge labeled with the explanation to the graph + * the weight of the edge is defined as the size of the explanation + * + * creates a EquationDijkstra object to perform the search + * + * @res congruence structure with updated graph + */ def resolveDeduced(u: E, v: E): Congruence = { val dij = new EquationDijkstra(eqReferences) -// println("resolve deduced: " + (u,v)) u match { case App(u1,u2) => { v match { @@ -186,19 +225,12 @@ class Congruence( val path2 = if (u2 == v2) new EquationTree(u2,None) else dij(u2,v2,g) - -// println("path1: " + path1) -// println("path2: " + path2) val eq1 = path1.allEqs val eq2 = path2.allEqs val eqAll = eq1 union eq2 val weight = eqAll.size -// println("resolve deduce: " + (u,v)) -// println("equations: "+ eqAll) - //if (weight > 0) here? -// if (u.t != v.t) println("Types are not the same for " + (u,v)) - val x = Eq(u,v,eqReferences) + val x = EqW(u,v) if (x.toString == "((f2 c_5 c_2) = c_3)" || x.toString == "(c_3 = (f2 c_5 c_2))") println("creating " + x + " when adding an edge to graph") updateGraph(g.addUndirectedEdge((u,(x,Some(path1,path2)),v), weight)) } @@ -209,80 +241,22 @@ class Congruence( } } + /** + * queries an EquationDijkstra object for the explanation of the equality of two terms + * + * @res None if there is no explanation (i.e. the terms are not congruent) + * Some(eqT) where eqT is an EquationTree representing the explanation + */ def explain(u: E, v: E): Option[EquationTree] = { -// resolveDeduced val dij = new EquationDijkstra(eqReferences) -// val tmpEq = Eq(u,v) -// val tmpCon = addEquality(tmpEq) -// val realG = tmpCon.g.removeUndirectedEdge((u,(tmpEq,None),v)) val path = dij(u,v,g) -// if (path.isEmpty) { -// println("trying to explain " + (u,v) + " but got empty path") -// (u,v) match { -// case (App(u1,u2),App(v1,v2)) => { -// val p1Opt = explain(u1,v1) -// val p2Opt = explain(u2,v2) -// println("now trying to explain " + (u1,v1) + " result: " + p1Opt) -// println("now trying to explain " + (u2,v2) + " result: " + p2Opt) -// (p1Opt,p2Opt) match { -// case (Some(p1),Some(p2)) => { -// if (p1.isEmpty || p2.isEmpty) { -// None -// } -// else { -// val end = new EquationTree(v,None) -// val eqTreeEdge = new EqTreeEdgeC(end,(Eq(u,v),Some((p1,p2)))) -// Some(new EquationTree(u,Some(eqTreeEdge))) -// } -// } -// case _ => None -// } -// } -// case _ => None -// } -// } -// else Some(path) if (path.isEmpty) None else Some(path) } + /** + * @res returns true iff u and v are congruent in the current congruence structure + */ def isCongruent(u: E, v: E) = { find.query(u) == find.query(v) } - - -// def pathTreetoProof(path: EquationTree): Boolean = { -// path.pred match { -// case Some((nextPT,label)) => { -// if (label.size == 1) { -// val eq = label.last -// val (u,v) = (path.v,nextPT.v) -// val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument) -// val x = (l==u && r == v)|| (l == v && r == u) && pathTreetoProof(nextPT) -// if (!x) println(eq + " is not an equality of " + (u,v)) -// else println(eq + " is an equality of " + (u,v)) -// x -// } -// else pathTreetoProof(nextPT) -// } -// case None => true -// } -// } - -// def eqTriplesToGraph:WGraph[E,App] = { -// val triples = eqTriples.values -// val (simple,nonSimple) = triples.partition(tr => tr._3 != EmptyEq) -// simple.foreach(tr => { -// g = g.addUndirectedEdge((tr._1,tr._3,tr._2), 1) -// }) -// nonSimple.foreach(tr => { -// g = resolve(tr._1,tr._2,g) -// }) -// g -// } - -// def resolve(tr: (E,E,App), g: WGraph[E,App]): WGraph[E,App] = { -// var g1 = g -// -// g1 -// } } \ No newline at end of file diff --git a/src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceCompressor.scala b/src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceCompressor.scala index 100a1fb6..ffba90a9 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceCompressor.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceCompressor.scala @@ -18,19 +18,54 @@ import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent} import scala.collection.mutable.{HashMap => MMap} import scala.collection.immutable.{HashMap => IMap} +/** + * Object CongruenceCompressor is the actual proof compressing object + * + * it gathers axioms from the whole proof and checks input derived nodes for redundant explanation + * input derived nodes all are recursive children of the single input node in the proof file + * to find redundant explanations for a node global axioms are used and + * axioms that where resolved with some recursive premise of the node are used + * + * first the node is fixed, just like subsumption or other compression algorithms do + * then for redundant fixed nodes new subproofs are generated from the EquationTree corresponding to the new explanation + */ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { + /** + * applies the compression algorithm to a proof + * first it calls the method buildGlobalCongruence with the proof and a newly created equality references object + * the result is a congruence structure with all input axioms + * + * in the traversal of the proof + * it first checks its input derived status + * then it fixes the current node + * all equations split in right (suc) and left (ant) in the fixed node are filtered out + * + * if the fixed node is input derived and there are equations on both sides + * it is checked whether the explanation (the left side) is redundant for some equation of the right side + * + * to do that it adds the left equalities in the (immutable!) congruence structure + * and then for all right equations it queries an EquationDijkstra object for a shorter explanation + * + * shorter here means to compare the length of the explanation with the number of equations on the left + * and the number of axioms that were already resolved away earlier in the subproof + * i am not 100% sure if this is the right way to compare sizes or if other things should be taken into account + * + * if there is a shorter explanation it is transformed into a proof and the node is replaced with the root of this proof + * + * @param proof to be compressed + * @res hopefully shorter proof + */ def apply(proof: Proof[N]): Proof[N] = { - val references = MMap[(E,E),App]() + val references = MMap[(E,E),EqW]() val (con,eqNodesLeft,eqNodesRight) = buildGlobalCongruence(proof,references) -// val allEqReferences: MMap[(E,E),App] = MMap[(E,E),App]() ++ allEqReferencesImmutable println("all references size: " + references.size) -// val istherealready = allEqReferences.values.find(p => {(p.toString == "((f1 c_3 c_3) = (f1 (f3 c6) (f3 c7)))" || p.toString == "((f1 (f3 c6) (f3 c7)) = (f1 c_3 c_3))") }) -// println("is there alreay?: " + istherealready) - val premiseAxiomMap = MMap[N,Set[App]]() -// var first = true - def replaceRedundant(node: N, fromPremises: Seq[(N,Set[App],Boolean)]): (N,Set[App],Boolean) = { -// println("processing " + node) + val premiseAxiomMap = MMap[N,Set[EqW]]() + + /** + * traversal + */ + def replaceRedundant(node: N, fromPremises: Seq[(N,Set[EqW],Boolean)]): (N,Set[EqW],Boolean) = { val inputDerived = if (node.isInstanceOf[Axiom]) true else @@ -40,28 +75,24 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { val fixedNodeInit = fixNode(node,premiseNodes) val premiseAxioms = premiseAxiomMap.getOrElseUpdate(fixedNodeInit, { - val premiseAxiomsTmp = fromPremises.foldLeft(Set[App]())({(A,B) => A union B._2}) + val premiseAxiomsTmp = fromPremises.foldLeft(Set[EqW]())({(A,B) => A union B._2}) if (node == fixedNodeInit) premiseAxiomsTmp else premiseAxiomsTmp.filter(Proof(fixedNodeInit).nodes.contains(_)) }) - val rightEqs = fixedNodeInit.conclusion.suc.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) - val leftEqs = fixedNodeInit.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) - -// val r1 = fixedNodeInit.conclusion.suc.filter(Eq.?:(_)) + val rightEqs = fixedNodeInit.conclusion.suc.filter(EqW.isEq(_)).map(EqW(_)) + val leftEqs = fixedNodeInit.conclusion.ant.filter(EqW.isEq(_)).map(EqW(_)) val rS = rightEqs.size val lS = leftEqs.size - -// println(fixedNodeInit + "\nrS: " + rightEqs + "\nlS " + leftEqs) - + val (resNode,resAxioms) = if (rS > 0 && lS > 0 && inputDerived) { val localCon = leftEqs.foldLeft(con)({(A,B) => A.addEquality(B)}) val localConRes = localCon.resolveDeducedQueue var tree: Option[EquationTree] = None val canBeCompressed = rightEqs.exists(eq => { - val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument) + val (l,r) = (eq.l,eq.r) val localConFinal = localConRes.addNode(l).addNode(r) val path = localConFinal.explain(l,r) path match { @@ -80,38 +111,52 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { if (canBeCompressed) { val path = tree.get -// println("proofing " + (path.firstVert,path.lastVert) + " from " + path.originalEqs) -// println("path: " + path) -// val eqRef = con.eqReferences val pathProof = try { - println("TO PROOF with " + references + " references") path.toProof(references) } catch { + /** + * here comes alot of debug stuff, including the exporting of the current node as a proof + * to also have all them found by this procedure some artificial nodes are added + * one for each used equality as a node with just that equality on the right side + * + * and one with all equalities on the left side + */ case e: Exception => { val exporter = new SMTFileExporter("experiments/congruence/resolveBug11",true) - val origEqs = path.originalEqs - val rightSideEq = fixedNodeInit.conclusion.suc.find(expr => if (Eq.?:(expr)) origEqs.contains(expr.asInstanceOf[App]) else false) + val origEqs = path.originalEqs.toSeq //set produced bugs with EqW contain not delivering correct result + val rightSideEq = fixedNodeInit.conclusion.suc.find(expr => if (EqW.isEq(expr)) origEqs.contains(EqW(expr)) else false) val res1 = rightSideEq match{ case Some(eq) => { // println(eq + " is rsEq") - R(new Axiom(new Sequent(origEqs.toSeq,Seq())),fixedNodeInit) + R(new Axiom(new Sequent(origEqs.map(_.equality).toSeq,Seq())),fixedNodeInit) } case None => { - val leftSideEq = fixedNodeInit.conclusion.ant.find(expr => if (expr.isInstanceOf[App]) origEqs.contains(expr.asInstanceOf[App]) else false) + val leftSideEq = fixedNodeInit.conclusion.ant.find(expr => if (EqW.isEq(expr)) origEqs.contains(EqW(expr)) else false) leftSideEq match{ case Some(eq) => { // println(eq + " is lsEq") - R(new Axiom(new Sequent(Seq(),origEqs.toSeq)),fixedNodeInit) + R(new Axiom(new Sequent(Seq(),origEqs.map(_.equality).toSeq)),fixedNodeInit) } case None => { - throw new Exception("fixedNode empty? " + fixedNodeInit) +// fixedNodeInit.conclusion.ant.foreach(p => { +// println(p + " contained in map? " + origEqs.contains(EqW(p))) +// }) + println(origEqs.mkString(",")) + val c7c3_1 = origEqs.find(_.toString == "(c7 = c_3)").get + val c7c3_2 = EqW(fixedNodeInit.conclusion.ant.find(_.toString == "(c7 = c_3)").get) + println(c7c3_1 + " == " + c7c3_2 + " ~> " + (c7c3_1 == c7c3_2)) + fixedNodeInit.conclusion.ant.map(EqW(_)).foreach(p => { + println(p + " contained in map? " + origEqs.contains(p)) + }) +// println(last + " contained in\n " + origEqs.mkString(",") + "\n" +last) + throw new Exception("fixedNode empty?\n" + fixedNodeInit) } } } } val res2 = origEqs.foldLeft(res1)({(A,B) => - val ax = new Axiom(new Sequent(Seq(),Seq(B))) + val ax = new Axiom(new Sequent(Seq(),Seq(B.equality))) if (A.conclusion.ant.contains(B)) R(A,ax) else A // try R(A,ax) @@ -128,20 +173,18 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { throw(e) } } + /** + * here the actual replacement is done + * if a node is in fact replaced it is also resolved with all the which it can be resolved with + */ val usedEqs = path.originalEqs pathProof match { - case Some(proof) => { //try without the if here ~ maybe reveal more bugs; check is not g - println("before " + fixedNodeInit) -// println(usedEqs.mkString(",") == proof.root.conclusion.ant.mkString(",")) - if (!(usedEqs.toSet.diff(proof.root.conclusion.ant.toSet).isEmpty && proof.root.conclusion.ant.toSet.diff(usedEqs.toSet).isEmpty)) { -// println(usedEqs + " differs from \n" + proof.root.conclusion.ant) - } + case Some(proof) => { if (usedEqs.size > fixedNodeInit.conclusion.ant.size) { -// println("compressing, but producing longer expl") } - val (resNode, resAxioms) = usedEqs.foldLeft((proof.root,Set[App]()))({(A,B) => + val (resNode, resAxioms) = usedEqs.foldLeft((proof.root,Set[EqW]()))({(A,B) => eqNodesRight.get(B) match { - case Some(node) => (R(A._1,node), A._2 + node.conclusion.suc.last.asInstanceOf[App]) + case Some(node) => (R(A._1,node), A._2 + EqW(node.conclusion.suc.last)) case None => A } }) @@ -164,7 +207,7 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { } val (newProof, _,_) = proof foldDown replaceRedundant val resProof = newProof.conclusion.suc.foldLeft(newProof)({(A,B) => - eqNodesLeft.get(B.asInstanceOf[App]) match { + eqNodesLeft.get(EqW(B)) match { case Some(node) => { R(A,node) } @@ -178,17 +221,21 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { DAGify(resProof) } - def buildGlobalCongruence(proof: Proof[N], references: MMap[(E,E),App]): (Congruence,MMap[App,N],MMap[App,N]) = { + /** + * gathers all the input equality and inequality axioms (i.e. single equalities on the right and left respectively) + * + */ + def buildGlobalCongruence(proof: Proof[N], references: MMap[(E,E),EqW]): (Congruence,MMap[EqW,N],MMap[EqW,N]) = { var con = new Congruence(references) - val eqNodesLeft = MMap[App,N]() - val eqNodesRight = MMap[App,N]() + val eqNodesLeft = MMap[EqW,N]() + val eqNodesRight = MMap[EqW,N]() - def traverse(node: N, fromPremises: Seq[(Boolean,Boolean,IMap[(E,E),App])]): (Boolean,Boolean,IMap[(E,E),App]) = { + def traverse(node: N, fromPremises: Seq[(Boolean,Boolean,IMap[(E,E),EqW])]): (Boolean,Boolean,IMap[(E,E),EqW]) = { val premiseMap = - if (fromPremises.isEmpty) IMap[(E,E),App]() + if (fromPremises.isEmpty) IMap[(E,E),EqW]() else { val maps = fromPremises.map(_._3) maps.tail.foldLeft(maps.head)({(A,B) => @@ -196,29 +243,25 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { }) } - val rightEqs = node.conclusion.suc.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) - val leftEqs = node.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) + val rightEqs = node.conclusion.suc.filter(EqW.isEq(_)).map(EqW(_)) + val leftEqs = node.conclusion.ant.filter(EqW.isEq(_)).map(EqW(_)) val bothEqs = rightEqs ++ leftEqs bothEqs.foreach(eq => { - val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument) + val (l,r) = (eq.l,eq.r) references += ((l,r) -> eq) - references += ((r,l) -> eq) +// references += ((r,l) -> eq) }) val eqMap = bothEqs.foldLeft(premiseMap)({(A,B) => - A.updated((B.function.asInstanceOf[App].argument,B.argument), B) + A.updated((B.l,B.r), B) }) - -// val test = (node.conclusion.ant ++ node.conclusion.suc).find(expr => { -// expr.toString == "((f2 c_5 c_2) = c_3)" -// }) -// if (test.isDefined) println("found " + test.get + " in " + node) + val freshLeft = if (fromPremises.size > 0) fromPremises.map(_._1).min else true val freshRight = if (fromPremises.size > 0) fromPremises.map(_._2).min else true val freshLeftOut = if(true) { - val singleLeft = node.conclusion.suc.size == 0 && node.conclusion.ant.size == 1 && node.conclusion.ant.forall(Eq.?:(_)) + val singleLeft = node.conclusion.suc.size == 0 && node.conclusion.ant.size == 1 && node.conclusion.ant.forall(EqW.isEq(_)) if (singleLeft) { - val eq = node.conclusion.ant.last.asInstanceOf[App] + val eq = EqW(node.conclusion.ant.last) eqNodesLeft += (eq -> node) false } @@ -226,9 +269,9 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { } else false val freshRightOut = if (freshRight) { - val singleRight = node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0 && node.conclusion.suc.forall(Eq.?:(_)) + val singleRight = node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0 && node.conclusion.suc.forall(EqW.isEq(_)) if (singleRight) { - val eq = node.conclusion.suc.last.asInstanceOf[App] + val eq = EqW(node.conclusion.suc.last) con = con.addEquality(eq) eqNodesRight += (eq -> node) false diff --git a/src/main/scala/at/logic/skeptik/algorithm/congruence/EqW.scala b/src/main/scala/at/logic/skeptik/algorithm/congruence/EqW.scala new file mode 100644 index 00000000..0239e658 --- /dev/null +++ b/src/main/scala/at/logic/skeptik/algorithm/congruence/EqW.scala @@ -0,0 +1,106 @@ +package at.logic.skeptik.algorithm.congruence + +import at.logic.skeptik.expression._ +import at.logic.skeptik.proof.sequent.{SequentProofNode => N} +import at.logic.skeptik.proof.sequent.lk._ + +class EqW(val equality :E) { + + + + + def reverse = { + val eqVar = new Var("=", (l.t -> (l.t -> o))) with Infix + EqW(App(App(eqVar,r),l)) + } + + def l = equality match { + case App(App(c,u),v) if c.toString == "=" => u + case _ => throw new Exception("eq in Equation is not an equality") + } + + def r = equality match { + case App(App(c,u),v) if c.toString == "=" => v + case _ => throw new Exception("eq in Equation is not an equality") + } + + override def equals(other: Any) = { + val res = other match { + case that: EqW => { + ((this.l == that.l) && (this.r == that.r) || (this.l == that.r) && (this.r == that.l)) + } + case _ => false + } +// println("checking " + this + " == " + other + " ?: " + res) + res + } + + override def toString = equality.toString +} + +object EqW { + + def resolveSymm (premise1:N, premise2:N) = { + def findPivots(p1:N, p2:N): Option[(E,E)] = { + for (auxL <- p1.conclusion.suc; auxR <- p2.conclusion.ant) if (auxL == auxR) return Some(auxL,auxR) + return None + } + findPivots(premise1,premise2) match { + case Some((auxL,auxR)) => { + resolve(premise1,premise2,auxL) + } + case None => findPivots(premise2,premise1) match { + case Some((auxL,auxR)) => resolve(premise2,premise1,auxL) + case None => { +// println("Not resolvable:") +// println(premise1 + " class: " + premise1.getClass) +// println(Proof(premise1)) +// println(premise2 + " class: " + premise2.getClass) + throw new Exception("Resolution: the conclusions of the given premises are not resolvable.") + } + } + } + } + + def resolve(leftPremise: N, rightPremise: N, pivot: E) = { + (leftPremise.conclusion.suc.find(EqW(_) == pivot), rightPremise.conclusion.ant.find(EqW(_) == pivot)) match { + case (Some(auxL), Some(auxR)) => new R(leftPremise, rightPremise, auxL, auxR) + case (None, None) => { + (leftPremise.conclusion.suc.find(EqW(_).reverse.equality == pivot), rightPremise.conclusion.ant.find(EqW(_) == pivot)) match { + case (Some(auxL), Some(auxR)) => new R(leftPremise, rightPremise, EqW(auxL).reverse.equality, auxR) + case (None,None) => (leftPremise.conclusion.ant.find(EqW(_) == pivot), rightPremise.conclusion.suc.find(EqW(_) == pivot)) match { + case (Some(auxL), Some(auxR)) => new R(rightPremise, leftPremise, auxR, auxL) + case (None,None) => (leftPremise.conclusion.ant.find(EqW(_).reverse.equality == pivot), rightPremise.conclusion.suc.find(EqW(_) == pivot)) match { + case (Some(auxL),Some(auxR)) => new R(rightPremise, leftPremise, auxR, EqW(auxL).reverse.equality) + case _ => throw new Exception("Auxiliary formulas not found.\n"+leftPremise.conclusion + "\n" + rightPremise.conclusion + "\n" + pivot) + } + } + } + } + case _ => throw new Exception("Auxiliary formulas not found.\n"+leftPremise.conclusion + "\n" + rightPremise.conclusion + "\n" + pivot) + } + } + + def isEq(f: E) = { + f match { + case App(App(v,_),_) => v.toString == "=" + case _ => false + } + } + + def apply(t1: E, t2: E): EqW = { + require(t1.t == t2.t) + val eqVar = new Var("=", (t1.t -> (t1.t -> o))) with Infix + new EqW(App(App(eqVar,t1),t2)) + } + + def apply(eq: E): EqW = { + if (isEq(eq)) new EqW(eq) + else throw new Exception("eq in Equation is not an equality") + } + + def unapply(e:E) = e match { + case App(App(c,u),v) if c.toString == "=" => Some((u,v)) + case _ => None + } +} \ No newline at end of file diff --git a/src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala b/src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala index c23068b6..5b31c587 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala @@ -5,8 +5,9 @@ import scala.collection.mutable.PriorityQueue import at.logic.skeptik.expression._ import scala.collection.mutable.{HashSet => MSet} import at.logic.skeptik.expression.formula._ +import at.logic.skeptik.algorithm.congruence.EqW -class EquationDijkstra(references: MMap[(E,E),App]) extends Dijkstra[E,EqLabel](references) { +class EquationDijkstra(references: MMap[(E,E),EqW]) extends Dijkstra[E,EqLabel](references) { def pi(u: E): EquationTree = { pathTrees.getOrElseUpdate(u,new EquationTree(u,None)) @@ -24,11 +25,11 @@ class EquationDijkstra(references: MMap[(E,E),App]) extends Dijkstra[E,EqLabel]( // } } -abstract class Dijkstra[T1,T2](references: MMap[(E,E),App]) { +abstract class Dijkstra[T1,T2](references: MMap[(E,E),EqW]) { val distances = MMap[T1,Int]() val pathTrees = MMap[T1,EquationTree]() - val discount = MSet[App]() + val discount = MSet[EqW]() def d(u: T1) = { distances.getOrElse(u, Integer.MAX_VALUE) @@ -52,7 +53,7 @@ abstract class Dijkstra[T1,T2](references: MMap[(E,E),App]) { if (s == target && s.isInstanceOf[E]) { val sE = s.asInstanceOf[E] val end = new EquationTree(sE,None) - val x = Eq(sE,sE,references) + val x = EqW(sE,sE) if (x.toString == "((f2 c_5 c_2) = c_3)" || x.toString == "(c_3 = (f2 c_5 c_2))") println("creating " + x + " when shortest path between two equal expr is asked") val eqTreeEdge = new EqTreeEdge(end,(x,None)) new EquationTree(sE,Some(eqTreeEdge)) diff --git a/src/main/scala/at/logic/skeptik/algorithm/dijkstra/PathTree.scala b/src/main/scala/at/logic/skeptik/algorithm/dijkstra/PathTree.scala index 8edb37db..5799fa28 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/dijkstra/PathTree.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/dijkstra/PathTree.scala @@ -1,5 +1,6 @@ package at.logic.skeptik.algorithm.dijkstra +import at.logic.skeptik.algorithm.congruence.EqW import at.logic.skeptik.expression.formula._ import at.logic.skeptik.expression._ import at.logic.skeptik.proof._ @@ -10,14 +11,14 @@ import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent} import scala.collection.immutable.{HashMap => IMap} import scala.collection.mutable.{HashMap => MMap} -class EqTreeEdge(val nextTree: EquationTree, val label: EqLabel) extends (EquationTree,(App,Option[(EquationTree,EquationTree)]))(nextTree,label) { +class EqTreeEdge(val nextTree: EquationTree, val label: EqLabel) extends (EquationTree,(EqW,Option[(EquationTree,EquationTree)]))(nextTree,label) { val eq = label._1 val deduceTrees = label._2 } case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { -// def toProof(eqReferences: MMap[(E,E),App]): Option[Proof[N]] = { +// def toProof(eqReferences: MMap[(E,E),EqW]): Option[Proof[N]] = { //// val istherestill = eqReferences.values.find(p => {(p.toString == "((f1 c_3 c_3) = (f1 (f3 c6) (f3 c7)))" || p.toString == "((f1 (f3 c6) (f3 c7)) = (f1 c_3 c_3))") }) //// println("is there still?: " + istherestill) // buildTransChain(eqReferences) match { @@ -51,7 +52,26 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { // } // } - def buildDeduction(dd1: EquationTree, dd2: EquationTree, eq: E, eqReferences: MMap[(E,E),App]): N = { + + def buildTransChain(eqReferences: MMap[(E,E),EqW]): (E,E,Seq[EqW],Seq[(N,EqW)]) = pred match { + case Some(pr) => { + val (first,last,equations,deduced) = pr._1.buildTransChain(eqReferences) + val resFirst = v + val resEquations = pr._2._1 +: equations + val resDeduced = pr._2._2 match { + case None => deduced + case Some((dd1,dd2)) => { + (buildDeduction(dd1,dd2,pr._2._1,eqReferences),pr._2._1) +: deduced + } + } + (resFirst,last,resEquations,resDeduced) + } + case None => { + (v,v,Seq(),Seq()) + } + } + + def buildDeduction(dd1: EquationTree, dd2: EquationTree, eq: EqW, eqReferences: MMap[(E,E),EqW]): N = { val (dd1Opt, dd2Opt) = (dd1.toProof(eqReferences),dd2.toProof(eqReferences)) val ddProofs = List(dd1Opt,dd2Opt).filter(_.isDefined).map(_.get) val ddProofRoots = ddProofs.map(_.root) //Check for EqAxiom, because of Axiom "hack" @@ -59,63 +79,37 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { // println("deducing " + eq) // println("trees: " + dd1 + " and " + dd2) // println("proofs: " + dd1Opt.isDefined + " and " + dd2Opt.isDefined) - val congr = eq match { - case App(App(c,t1),t2) => (t1,t2) match { - case (App(u1,u2),App(v1,v2)) => { - val realEq = eqReferences.getOrElseUpdate((t1,t2), { - val x = eqReferences.getOrElse((t2,t1), { - println("no eqRef for " + eq) - eq - }) - x.asInstanceOf[App] - }) - if ((u1 == v1) && (u2 != v2)) EqCongruent(Eq(u2,v2,eqReferences),realEq) - else if ((u1 != v1) && (u2 == v2)) EqCongruent(Eq(u1,v1,eqReferences),realEq) - else if ((u1 != v1) && (u2 != v2)) EqCongruent(Eq(u1,v1,eqReferences),Eq(u2,v2,eqReferences),realEq) - else throw new Exception("Trying to prove the congruence of terms with equal arguments") - } - case _ => throw new Exception("Error when creating congruence node, because equality between wrong kind of expressions") - } - case _ => throw new Exception("Error when creating congruence node, because equality between wrong kind of expressions") + val congr = (eq.l,eq.r) match { + case (App(u1,u2),App(v1,v2)) => { + if ((u1 == v1) && (u2 != v2)) EqCongruent(EqW(u2,v2),eq) + else if ((u1 != v1) && (u2 == v2)) EqCongruent(EqW(u1,v1),eq) + else if ((u1 != v1) && (u2 != v2)) EqCongruent(EqW(u1,v1),EqW(u2,v2),eq) + else throw new Exception("Trying to prove the congruence of terms with equal arguments") + } + case _ => throw new Exception("Error when creating congruence node, because equality between wrong kind of expressions") } val res = if (ddEqs.isEmpty) { -// val x = dd1.originalEqs.map(_.asInstanceOf[E]).toSeq ++: dd2.originalEqs.map(_.asInstanceOf[E]).toSeq -// -// val y = EqCongruent(x,eq) -// println("creating congruence with no deduced Eqs: " + y) -// y congr } else { -// println("ddEqs: " + ddEqs) -// val congr = { -// eq match { -// case App(App(c,App(u1,u2)),App(v1,v2)) => { -// if ((u1 == v1) && (u2 != v2)) EqCongruent(Eq(u2,v2),eq) -// else if ((u1 != v1) && (u2 == v2)) EqCongruent(Eq(u1,v1),eq) -// else if ((u1 != v1) && (u2 != v2)) EqCongruent(Eq(u1,v1),Eq(u2,v2),eq) -// else throw new Exception("Trying to prove the congruence of terms with equal arguments") -// } -// case _ => throw new Exception("Error when creating congruence node, because equality between wrong kind of expressions") -// } -// } -// val congr = EqCongruent(ddEqs) -// println("Congruence: " + congr) - try { - ddProofRoots.foldLeft(congr.asInstanceOf[N])({(A,B) => R(A,B)}) - } - catch { - case e:Exception => { - println("error when building proof for " + eq) - println(dd1) - println(dd1Opt) - println(dd2) - println(dd2Opt) - println(this) - throw(e) + ddProofRoots.foldLeft(congr.asInstanceOf[N])({(A,B) => + try EqW.resolveSymm(A,B) + catch { + case e: Exception => { + val AnewAnt = A.conclusion.ant.map(f => if (EqW.isEq(f)) EqW(f).reverse.equality else f) + val AnewSuc = A.conclusion.suc.map(f => if (EqW.isEq(f)) EqW(f).reverse.equality else f) + val Anew = + println() + println(this) + println(A + " " + A.getClass) + println(B + " " + B.getClass) + println(Proof(A)) + println(Proof(B)) + throw e + } } - } + }) } // println("result:\n"+ Proof(res)) res @@ -127,7 +121,7 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { // case _ => None // } - def toProof(eqReferences: MMap[(E,E),App]): Option[Proof[N]] = { + def toProof(eqReferences: MMap[(E,E),EqW]): Option[Proof[N]] = { val (first,last,equations,deduced) = this.buildTransChain(eqReferences) if (equations.size > 1) { val transNode = EqTransitive(equations,first,last,eqReferences) @@ -135,16 +129,19 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { val resEq = B._2 val resNode = B._1 try { - R(A,resNode,resEq) + R(A,resNode) } catch { case e:Exception => { - try R(resNode,A,resEq) + try R(resNode,A) catch { case e1:Exception => { - val oneSide = (resNode.conclusion.suc.contains(resEq) && resNode.conclusion.ant.contains(resEq)) - val otherSide = (resNode.conclusion.ant.contains(resEq) && resNode.conclusion.suc.contains(resEq)) - println(oneSide || otherSide) + println(this) + println(A + " " + resNode.getClass()) + println(Proof(resNode)+ " " + resNode.getClass()) +// val oneSide = (resNode.conclusion.suc.contains(resEq) && resNode.conclusion.ant.contains(resEq)) +// val otherSide = (resNode.conclusion.ant.contains(resEq) && resNode.conclusion.suc.contains(resEq)) +// println(oneSide || otherSide) // println(this) // println("trying to resolve upon " + B._2 + B._2.hashCode) // println(Proof(A)) @@ -163,77 +160,59 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { else None } - def buildTransChain(eqReferences: MMap[(E,E),App]): (E,E,Seq[App],Seq[(N,App)]) = pred match { - case Some(pr) => { - val (first,last,equations,deduced) = pr._1.buildTransChain(eqReferences) - val resFirst = v - val resEquations = pr._2._1 +: equations - val resDeduced = pr._2._2 match { - case None => deduced - case Some((dd1,dd2)) => { - (buildDeduction(dd1,dd2,pr._2._1,eqReferences),pr._2._1) +: deduced - } - } - (resFirst,last,resEquations,resDeduced) - } - case None => { - (v,v,Seq(),Seq()) - } - } - - def buildTransChain1(eqReferences: MMap[(E,E),App]): Option[(Option[N],Set[N],E)] = pred match { - case Some(pr) => { - val (nextTree, eq, deduceTrees) = (pr.nextTree,pr.eq,pr.deduceTrees) - if (nextTree.v == v) { - Some((Some(EqReflexive(v, eqReferences)),Set[N](),eq)) - } - else { - val resultFromNext = nextTree.buildTransChain1(eqReferences) - - resultFromNext match { - case Some((nodeOpt,deducedRes,eqRes)) => { - val node = nodeOpt match { - case Some(nodeRes) => { - val tr = EqTransitive(eq,nodeRes.conclusion.suc.last,eqReferences) - val res = R(nodeRes,tr) - res - } - case None => EqTransitive(eq,eqRes,eqReferences) - } - val ded = deduceTrees match { - case Some((ddT1,ddT2)) => Set[N](buildDeduction(ddT1,ddT2,eq,eqReferences)) - case None => Set[N]() - } - val dedFinal = ded union deducedRes -// println("passing on: " + deducedRes + " while proving " + eq) - Some((Some(node),dedFinal,eq)) - } - case None => { - val ded = deduceTrees match { - case Some((ddT1,ddT2)) => { - val x = Set[N](buildDeduction(ddT1,ddT2,eq,eqReferences)) -// println("getting the following deduced nodes here: " + x.last + " " + x.last.getClass()) - x - } - case None => Set[N]() - } -// println("I am here for " + this) - Some((None,ded,eq)) - } - } - } - } - case None => None - } +// def buildTransChain1(eqReferences: MMap[(E,E),EqW]): Option[(Option[N],Set[N],E)] = pred match { +// case Some(pr) => { +// val (nextTree, eq, deduceTrees) = (pr.nextTree,pr.eq,pr.deduceTrees) +// if (nextTree.v == v) { +// Some((Some(EqReflexive(v, eqReferences)),Set[N](),eq)) +// } +// else { +// val resultFromNext = nextTree.buildTransChain1(eqReferences) +// +// resultFromNext match { +// case Some((nodeOpt,deducedRes,eqRes)) => { +// val node = nodeOpt match { +// case Some(nodeRes) => { +// val tr = EqTransitive(eq,nodeRes.conclusion.suc.last,eqReferences) +// val res = R(nodeRes,tr) +// res +// } +// case None => EqTransitive(eq,eqRes,eqReferences) +// } +// val ded = deduceTrees match { +// case Some((ddT1,ddT2)) => Set[N](buildDeduction(ddT1,ddT2,eq,eqReferences)) +// case None => Set[N]() +// } +// val dedFinal = ded union deducedRes +//// println("passing on: " + deducedRes + " while proving " + eq) +// Some((Some(node),dedFinal,eq)) +// } +// case None => { +// val ded = deduceTrees match { +// case Some((ddT1,ddT2)) => { +// val x = Set[N](buildDeduction(ddT1,ddT2,eq,eqReferences)) +//// println("getting the following deduced nodes here: " + x.last + " " + x.last.getClass()) +// x +// } +// case None => Set[N]() +// } +//// println("I am here for " + this) +// Some((None,ded,eq)) +// } +// } +// } +// } +// case None => None +// } - def eq: Option[App] = pred match { + def eq: Option[EqW] = pred match { case Some(pr) => { Some(pr._2._1) } case None => None } - def allEqs: Set[App] = pred match { + def allEqs: Set[EqW] = pred match { case Some(pr) => { // println(pr._1.v + " deduced eqs: " +deducedEqs) pr._1.allEqs + pr._2._1 ++ deducedEqs @@ -243,7 +222,7 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { } } - def originalEqs: Set[App] = pred match { + def originalEqs: Set[EqW] = pred match { case Some(pr) => { val predOrig = pr._1.originalEqs val extra = pr._2._2 match { @@ -255,7 +234,7 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { case None => Set() } - def pathEqs: Set[App] = pred match { + def pathEqs: Set[EqW] = pred match { case Some(pr) => { pr._1.pathEqs + pr._2._1 } @@ -264,7 +243,7 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { } } - def deducedEqs: Set[App] = { + def deducedEqs: Set[EqW] = { val lEqs = leftExpl match { case Some(l) => l.originalEqs case None => Set() diff --git a/src/main/scala/at/logic/skeptik/algorithm/dijkstra/package.scala b/src/main/scala/at/logic/skeptik/algorithm/dijkstra/package.scala index 9d7fddc2..09d8da7c 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/dijkstra/package.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/dijkstra/package.scala @@ -1,9 +1,9 @@ package at.logic.skeptik.algorithm -//import at.logic.skeptik.expression.{App => PApp} import at.logic.skeptik.expression._ +import at.logic.skeptik.algorithm.congruence.EqW package object dijkstra { -// type EqTreeEdge = Option[(EquationTree,(App,Option[(EquationTree,EquationTree)]))] - type EqLabel = (App,Option[(EquationTree,EquationTree)]) +// type EqTreeEdge = Option[(EquationTree,(EqW,Option[(EquationTree,EquationTree)]))] + type EqLabel = (EqW,Option[(EquationTree,EquationTree)]) } \ No newline at end of file diff --git a/src/main/scala/at/logic/skeptik/expression/formula/formulas.scala b/src/main/scala/at/logic/skeptik/expression/formula/formulas.scala index 34d41322..d6e9d9f4 100644 --- a/src/main/scala/at/logic/skeptik/expression/formula/formulas.scala +++ b/src/main/scala/at/logic/skeptik/expression/formula/formulas.scala @@ -47,80 +47,76 @@ object Or extends BinaryFormula(orC) object Imp extends BinaryFormula(impC) -object Eq { -// def apply(term1: E, term2: E): App = { +//object Eq { +//// def apply(term1: E, term2: E): App = { +//// require(term1.t == term2.t) +//// val t1Type = term1.t +//// new Equation(t1Type)(term1,term2) +//// } +// /** +// * called in: +// * PathTree line 59 +// * package at.logic.skeptik.proof.sequent.lk.congruence line 27 (EQReflexive), line 57 (EQTransitive) +// * Dijkstra line 55 (only reflexive eq) +// * +// */ +// def apply(term1: E, term2: E, eqReferences: scala.collection.mutable.HashMap[(E,E),at.logic.skeptik.algorithm.congruence.EqW]): App = { // require(term1.t == term2.t) -// val t1Type = term1.t -// new Equation(t1Type)(term1,term2) -// } - /** - * called in: - * PathTree line 59 - * package at.logic.skeptik.proof.sequent.lk.congruence line 27 (EQReflexive), line 57 (EQTransitive) - * Dijkstra line 55 (only reflexive eq) - * - */ - def apply(term1: E, term2: E, eqReferences: scala.collection.mutable.HashMap[(E,E),App]): App = { - require(term1.t == term2.t) -// val istherestill = eqReferences.values.find(p => {(p.toString == "((f1 c_3 c_3) = (f1 (f3 c6) (f3 c7)))" || p.toString == "((f1 (f3 c6) (f3 c7)) = (f1 c_3 c_3))") }) -// println("is there still?: " + istherestill + " ~ " + eqReferences.size) - val thisOne= - ((term1.toString == "(f1 (f3 c_4) c_4)" && term2.toString == "(f1 (f2 c_4 c_4) (f2 c_4 c_4)))") - || ((term2.toString == "(f1 (f3 c_4) c_4)" && term1.toString == "(f1 (f2 c_4 c_4) (f2 c_4 c_4)))"))) - eqReferences.get((term1,term2)) match { - case Some(eq) => { - if (thisOne) println("found eq for " + (term1,term2)) - eq - } - case None => { - eqReferences.get((term2,term1)) match { - case Some(eq2) => { - if (thisOne) println("found eq for " + (term2,term1)) - eq2 - } - case None => { - if (thisOne) println("creating eq for " + (term1,term2)) -// val y = Eq(term1,term2) - val y = new Equation(term1.t)(term1,term2) - val doPrint = (y.toString == "((f1 c_3 c_3) = (f1 (f3 c6) (f3 c7)))" || y.toString == "((f1 (f3 c6) (f3 c7)) = (f1 c_3 c_3))") - if (doPrint) println("eqRef before adding " + y + " : " + eqReferences) - eqReferences += ((term1,term2) -> y) - eqReferences += ((term2,term1) -> y) -// eqReferences.update((term2,term1), y) - if (doPrint) println("eqRef before after " + y + " : " + eqReferences) - if (doPrint) println("Have to create " + y + " myself in Eq, apply (formulas)") - if (doPrint) println("eqs: " + eqReferences.values.mkString(",")) - if (y.toString == "((f1 c_0 c_0) = (f1 c_0 (f2 c_0 c_0)))") println("CREATING THE ONE EQUATION IN EQ()") - if (y.toString == "((f1 c_0 (f2 c_0 c_0)) = (f1 c_0 c_0))") println("CREATING THE OTHER EQUATION IN EQ()") - y - } - } - } - } - } -// def eqEquals(t1: E, t2: E): Boolean = { -// if (Eq.?:(t1) && Eq.?:(t2)) { -// val (u1,u2) = t1 match { -// case App(App(c,f1),f2) => (f1,f2) -// } -// val (v1,v2) = t2 match { -// case App(App(c,f1),f2) => (f1,f2) +//// val istherestill = eqReferences.values.find(p => {(p.toString == "((f1 c_3 c_3) = (f1 (f3 c6) (f3 c7)))" || p.toString == "((f1 (f3 c6) (f3 c7)) = (f1 c_3 c_3))") }) +//// println("is there still?: " + istherestill + " ~ " + eqReferences.size) +// val thisOne= +// ((term1.toString == "(f1 (f3 c_4) c_4)" && term2.toString == "(f1 (f2 c_4 c_4) (f2 c_4 c_4)))") +// || ((term2.toString == "(f1 (f3 c_4) c_4)" && term1.toString == "(f1 (f2 c_4 c_4) (f2 c_4 c_4)))"))) +// eqReferences.get((term1,term2)) match { +// case Some(eq) => { +// if (thisOne) println("found eq for " + (term1,term2)) +// eq.equality.asInstanceOf[App] // } -// ((u1 == v1) && (u2 == v2) || (u1 == v2) && (u2 == v1)) +// case None => { +// eqReferences.get((term2,term1)) match { +// case Some(eq2) => { +// if (thisOne) println("found eq for " + (term2,term1)) +// eq2.equality.asInstanceOf[App] +// } +// case None => { +// if (thisOne) println("creating eq for " + (term1,term2)) +//// val y = Eq(term1,term2) +// val y = new Equation(term1.t)(term1,term2) +// val doPrint = (y.toString == "((f1 c_3 c_3) = (f1 (f3 c6) (f3 c7)))" || y.toString == "((f1 (f3 c6) (f3 c7)) = (f1 c_3 c_3))") +// if (doPrint) println("eqRef before adding " + y + " : " + eqReferences) +// eqReferences += ((term1,term2) -> at.logic.skeptik.algorithm.congruence.EqW(y)) +// eqReferences += ((term2,term1) -> at.logic.skeptik.algorithm.congruence.EqW(y)) +//// eqReferences.update((term2,term1), y) +// if (doPrint) println("eqRef before after " + y + " : " + eqReferences) +// if (doPrint) println("Have to create " + y + " myself in Eq, apply (formulas)") +// if (doPrint) println("eqs: " + eqReferences.values.mkString(",")) +// if (y.toString == "((f1 c_0 c_0) = (f1 c_0 (f2 c_0 c_0)))") println("CREATING THE ONE EQUATION IN EQ()") +// if (y.toString == "((f1 c_0 (f2 c_0 c_0)) = (f1 c_0 c_0))") println("CREATING THE OTHER EQUATION IN EQ()") +// y +// } +// } +// } // } -// else t1 == t2 // } - def ?:(f: E) = { // very hacky! - f match { - case App(App(v,_),_) => v.toString == "=" - case _ => false - } - } - def unapply(e:E) = e match { - case App(q, Abs(v,f)) if v.toString == "=" => Some((v,f)) - case _ => None - } -} +//// def eqEquals(t1: E, t2: E): Boolean = { +//// if (Eq.?:(t1) && Eq.?:(t2)) { +//// val (u1,u2) = t1 match { +//// case App(App(c,f1),f2) => (f1,f2) +//// } +//// val (v1,v2) = t2 match { +//// case App(App(c,f1),f2) => (f1,f2) +//// } +//// ((u1 == v1) && (u2 == v2) || (u1 == v2) && (u2 == v1)) +//// } +//// else t1 == t2 +//// } +// def ?:(f: E) = { // very hacky! +// f match { +// case App(App(v,_),_) => v.toString == "=" +// case _ => false +// } +// } +//} object All extends QuantifierFormula(allC) diff --git a/src/main/scala/at/logic/skeptik/proof/sequent/lk/Congruence.scala b/src/main/scala/at/logic/skeptik/proof/sequent/lk/Congruence.scala index 6993b6d4..9c937155 100644 --- a/src/main/scala/at/logic/skeptik/proof/sequent/lk/Congruence.scala +++ b/src/main/scala/at/logic/skeptik/proof/sequent/lk/Congruence.scala @@ -7,6 +7,7 @@ import at.logic.skeptik.expression._ import at.logic.skeptik.expression.formula._ import scala.collection.immutable.{HashMap => IMap} import scala.collection.mutable.{HashMap => MMap} +import at.logic.skeptik.algorithm.congruence.EqW abstract class EqAxiom(override val mainFormulas: Sequent) extends SequentProofNode with Nullary with NoImplicitContraction { @@ -19,12 +20,12 @@ class EqReflexive(override val mainFormulas: Sequent) extends EqAxiom(mainFormul object EqReflexive { def apply(conclusion: Sequent) = new EqReflexive(conclusion) - def apply(expr: E, eqReferences: MMap[(E,E),App]) = { + def apply(expr: E, eqReferences: MMap[(E,E),EqW]) = { expr match { - case App(App(e,t1),t2) if (t1 == t2 && Eq.?:(expr)) => new EqReflexive(new Sequent(Seq(),Seq(expr))) + case App(App(e,t1),t2) if (t1 == t2 && EqW.isEq(expr)) => new EqReflexive(new Sequent(Seq(),Seq(expr))) case _ => { if (expr.t == i) { - val x = eqReferences.getOrElse((expr,expr), Eq(expr,expr,eqReferences)) + val x = eqReferences.getOrElse((expr,expr), EqW(expr,expr)).equality if (x.toString == "((f2 c_5 c_2) = c_3)" || x.toString == "(c_3 = (f2 c_5 c_2))") println("creating " + x + " while creating EqReflexive node") new EqReflexive(new Sequent(Seq(),Seq(x))) } @@ -46,40 +47,20 @@ object EqTransitive { def apply(conclusion: Sequent) = new EqTransitive(conclusion) - def apply(eqsLeft: Seq[E], t1: E, t2: E, eqReferences: MMap[(E,E),App]) = { - new EqTransitive(new Sequent(eqsLeft,Seq(Eq(t1,t2,eqReferences)))) + def apply(eqsLeft: Seq[EqW], t1: E, t2: E, eqReferences: MMap[(E,E),EqW]) = { // Semantics not checked! + new EqTransitive(new Sequent(eqsLeft.map(_.equality),Seq(EqW(t1,t2).equality))) } - def apply(eq1: E, eq2: E, eqReferences: MMap[(E,E),App]) = { - eq1 match { - case App(App(e,u1),u2) if (Eq.?:(eq1)) => eq2 match { - case App(App(e,v1),v2) if (Eq.?:(eq2)) => { - val (t1,t2) = - if (u1 == v1) (u2,v2) - else if (u1 == v2) (u2,v1) - else if (u2 == v1) (u1,v2) - else if (u2 == v2) (u1,v1) - else throw new Exception("Error occured while creating EQtransitive node: "+ eq1 + " and " + eq2 + " don't form a transitivity chain") - val x = Eq(t1,t2,eqReferences) -// eqReferences.get((t1,t2)) match { -// case Some(eq) => eq -// case None => { -// eqReferences.get((t2,t1)) match { -// case Some(eq2) => eq2 -// case None => { -// val y = Eq(t1,t2,eqReferences) -// println("Have to create " + y + " myself in EqTransitive") -// println("eqs: " + eqReferences.values.mkString(",")) -// y -// } -// } -// } -// } - if (x.toString == "((f2 c_5 c_2) = c_3)" || x.toString == "(c_3 = (f2 c_5 c_2))") println("creating " + x + " while creating EqTransitive node") - new EqTransitive(new Sequent(Seq(eq1,eq2),Seq(x))) - } - } - } + def apply(eq1: EqW, eq2: EqW, eqReferences: MMap[(E,E),EqW] = MMap[(E,E),EqW]()) = { + val (u1,u2,v1,v2) = (eq1.l,eq1.r,eq2.l,eq2.r) + val (t1,t2) = + if (u1 == v1) (u2,v2) + else if (u1 == v2) (u2,v1) + else if (u2 == v1) (u1,v2) + else if (u2 == v2) (u1,v1) + else throw new Exception("Error occured while creating EQtransitive node: "+ eq1 + " and " + eq2 + " don't form a transitivity chain") + val x = EqW(t1,t2).equality + new EqTransitive(new Sequent(Seq(eq1.equality,eq2.equality),Seq(x))) } def unapply(p: SequentProofNode) = p match { case p: EqTransitive => Some(p.conclusion) @@ -91,28 +72,17 @@ class EqCongruent(override val mainFormulas: Sequent) extends EqAxiom(mainFormul object EqCongruent { def apply(conclusion: Sequent) = new EqCongruent(conclusion) - def apply(expl: E, eq: E) = { //Semantics are not checked (yet) - new EqCongruent(new Sequent(Seq(expl),Seq(eq))) + def apply(expl: EqW, eq: EqW) = { //Semantics are not checked (yet) + new EqCongruent(new Sequent(Seq(expl.equality),Seq(eq.equality))) } - def apply(expl1: E, expl2: E, eq: E) = { //Semantics are not checked (yet) - new EqCongruent(new Sequent(Seq(expl1,expl2),Seq(eq))) + def apply(expl1: EqW, expl2: EqW, eq: EqW) = { //Semantics are not checked (yet) + new EqCongruent(new Sequent(Seq(expl1.equality,expl2.equality),Seq(eq.equality))) } - def apply(expls: Seq[E], eq: E) = { //Semantics are not checked (yet) - new EqCongruent(new Sequent(expls,Seq(eq))) + def apply(expls: Seq[EqW], eq: EqW) = { //Semantics are not checked (yet) + new EqCongruent(new Sequent(expls.map(_.equality),Seq(eq.equality))) } def unapply(p: SequentProofNode) = p match { case p: EqCongruent => Some(p.conclusion) case _ => None } -} - -//class Axiom(override val mainFormulas: Sequent) extends SequentProofNode -//with Nullary with NoImplicitContraction -// -//object Axiom { -// def apply(conclusion: Sequent) = new Axiom(conclusion) -// def unapply(p: SequentProofNode) = p match { -// case p: Axiom => Some(p.conclusion) -// case _ => None -// } -//} \ No newline at end of file +} \ No newline at end of file diff --git a/src/main/scala/at/logic/skeptik/proof/sequent/lk/R.scala b/src/main/scala/at/logic/skeptik/proof/sequent/lk/R.scala index 0cea8561..f224005d 100644 --- a/src/main/scala/at/logic/skeptik/proof/sequent/lk/R.scala +++ b/src/main/scala/at/logic/skeptik/proof/sequent/lk/R.scala @@ -63,10 +63,10 @@ object R { case None => findPivots(premise2,premise1) match { case Some((auxL,auxR)) => new R(premise2,premise1,auxL,auxR) case None => { - println("Not resolvable:") - println(premise1 + " class: " + premise1.getClass) +// println("Not resolvable:") +// println(premise1 + " class: " + premise1.getClass) // println(Proof(premise1)) - println(premise2 + " class: " + premise2.getClass) +// println(premise2 + " class: " + premise2.getClass) throw new Exception("Resolution: the conclusions of the given premises are not resolvable.") } } diff --git a/src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceTest.scala b/src/test/scala/at/logic/skeptik/congruence/CongruenceTest.scala similarity index 100% rename from src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceTest.scala rename to src/test/scala/at/logic/skeptik/congruence/CongruenceTest.scala diff --git a/src/test/scala/at/logic/skeptik/congruence/EqWTest.scala b/src/test/scala/at/logic/skeptik/congruence/EqWTest.scala new file mode 100644 index 00000000..65957a35 --- /dev/null +++ b/src/test/scala/at/logic/skeptik/congruence/EqWTest.scala @@ -0,0 +1,25 @@ +package at.logic.skeptik.congruence + +import at.logic.skeptik.expression.formula._ +import at.logic.skeptik.expression._ +import at.logic.skeptik.algorithm.congruence.EqW + +object EqWTest { + def main(args: Array[String]):Unit = { + val t = o + + val a = new Var("a",t) + val b = new Var("b",t) + val c = new Var("c",t) + val d = new Var("d",t) + + val eq = EqW(a,b) + + val eq2 = EqW(b,a) + + val seq = Set(eq) + println(eq == eq) + println(seq.contains(eq2)) + println(EqW.isEq(eq.equality)) + } +} \ No newline at end of file diff --git a/src/test/scala/at/logic/skeptik/congruence/EquationsExperiment.scala b/src/test/scala/at/logic/skeptik/congruence/EquationsExperiment.scala index 845eacae..39ad14a9 100644 --- a/src/test/scala/at/logic/skeptik/congruence/EquationsExperiment.scala +++ b/src/test/scala/at/logic/skeptik/congruence/EquationsExperiment.scala @@ -1,242 +1,242 @@ -package at.logic.skeptik.congruence - -import at.logic.skeptik.parser.ProofParserVeriT -import at.logic.skeptik.algorithm.congruence -import at.logic.skeptik.expression.formula._ -import at.logic.skeptik.expression._ -import at.logic.skeptik.proof.sequent.{SequentProofNode => N} -import at.logic.skeptik.proof._ -import at.logic.skeptik.util.io.Input -import at.logic.skeptik.algorithm.congruence._ -import scala.collection.mutable.{HashMap => MMap} - -object EquationsExperiment { - - def main(args: Array[String]):Unit = { - val reader = new Input("F:/Proofs/QF_UF/QG-classification/QC-classification") -// val reader = new Input("F:/Proofs/QF_UF/seq_files") -// val reader = new Input("D:/Paradoxika/Skeptik/prooflists/diamonds") - val lines = reader.lines - val parser = ProofParserVeriT -// var percentage: Double = - 1 - for (singleFile <- lines) { - val proof = parser.read(singleFile) -// println(proof) -// val axioms = proof.filter(n => n.premises.isEmpty) -// val y = countTwoRightAndCongruent(proof) - val z = checkRedundant(proof) -// val x = countTrueAxioms(axioms) -// if (percentage == -1) percentage = x -// else percentage = (percentage + x)/2 -// println(percentage + " % two right and congruent at: " + singleFile) -// println(x + " of " + axioms.size + " two right and congruent at: " + singleFile) - println(z + " of " + proof.size + " found to be redundant: " + singleFile) - } -// println(percentage) - - -// val proof = ProofParserVeriT.read("D:/Paradoxika/Skeptik/examples/proofs/VeriT/eq_diamond2.smt2") +//package at.logic.skeptik.congruence +// +//import at.logic.skeptik.parser.ProofParserVeriT +//import at.logic.skeptik.algorithm.congruence +//import at.logic.skeptik.expression.formula._ +//import at.logic.skeptik.expression._ +//import at.logic.skeptik.proof.sequent.{SequentProofNode => N} +//import at.logic.skeptik.proof._ +//import at.logic.skeptik.util.io.Input +//import at.logic.skeptik.algorithm.congruence._ +//import scala.collection.mutable.{HashMap => MMap} +// +//object EquationsExperiment { +// +// def main(args: Array[String]):Unit = { +// val reader = new Input("F:/Proofs/QF_UF/QG-classification/QC-classification") +//// val reader = new Input("F:/Proofs/QF_UF/seq_files") +//// val reader = new Input("D:/Paradoxika/Skeptik/prooflists/diamonds") +// val lines = reader.lines +// val parser = ProofParserVeriT +//// var percentage: Double = - 1 +// for (singleFile <- lines) { +// val proof = parser.read(singleFile) +//// println(proof) +//// val axioms = proof.filter(n => n.premises.isEmpty) +//// val y = countTwoRightAndCongruent(proof) +// val z = checkRedundant(proof) +//// val x = countTrueAxioms(axioms) +//// if (percentage == -1) percentage = x +//// else percentage = (percentage + x)/2 +//// println(percentage + " % two right and congruent at: " + singleFile) +//// println(x + " of " + axioms.size + " two right and congruent at: " + singleFile) +// println(z + " of " + proof.size + " found to be redundant: " + singleFile) +// } +//// println(percentage) // -// checkRedundant(proof) - } - - def countTrueAxioms(axioms: Iterable[N]) = { - var count = 0 - axioms.foreach(node => { - if (twoRightAndCongruent(node)) { - count = count + 1 - } - }) - count - } - - def countTwoRightAndCongruent(proof: Proof[N]) = { - var count = 0 - proof.foreach(node => { - if (twoRightAndCongruent(node)) { - count = count + 1 - } - }) -// (count.asInstanceOf[Double] * 100) / proof.size - count - } - - def countTwoRight(proof: Proof[N]) = { - var count = 0 - proof.foreach(node => { - if (hasTwoRight(node)) { -// if (node.conclusion.size < 10) println(node.conclusion) - count = count + 1 - } - }) -// println(count +" of "+ proof.size + " have 2 eq's right") -// (count.asInstanceOf[Double] * 100) / proof.size - count - } - - def twoRightAndCongruent(node: N): Boolean = { - val rightEqs = node.conclusion.suc.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) - val leftEqs = node.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) - val s = rightEqs.size - val twoAndCongruent = - if (s > 0) { - val con = new Congruence(MMap[(E,E),App]()) - leftEqs.foreach(eq => con.addEquality(eq)) - con.resolveDeducedQueue - rightEqs.exists(eq => { - val path = con.explain(eq.function.asInstanceOf[App].argument, eq.argument) - val c = if (path.isDefined) path.get.collectLabels.size else 0 - val out = c > 0 && c < leftEqs.size -// if (out) { -// println(node.conclusion + "\nshorter explanation " + path.collectLabels) -// } -// if (!out) println(node.conclusion) -// println("is congruent: " + eq.function.asInstanceOf[App].argument + ", " + eq.argument + " ? " + c) - out - }) - } - else false -// if (s > 0 && leftEqs.size > 0 && !twoAndCongruent) { -// println(node.conclusion) +// +//// val proof = ProofParserVeriT.read("D:/Paradoxika/Skeptik/examples/proofs/VeriT/eq_diamond2.smt2") +//// +//// checkRedundant(proof) +// } +// +// def countTrueAxioms(axioms: Iterable[N]) = { +// var count = 0 +// axioms.foreach(node => { +// if (twoRightAndCongruent(node)) { +// count = count + 1 +// } +// }) +// count +// } +// +// def countTwoRightAndCongruent(proof: Proof[N]) = { +// var count = 0 +// proof.foreach(node => { +// if (twoRightAndCongruent(node)) { +// count = count + 1 // } - twoAndCongruent - } - - def hasTwoRight(node: N): Boolean = { - val s = node.conclusion.suc.filter(Eq.?:(_)).size -// println(s) - s > 1 - } - - def rightEqs(node: N) = node.conclusion.suc.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) - - def leftEqs(node: N) = node.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) - - - def checkRedundant(proof: Proof[N]) = { - - val con = buildGlobalCongruence2(proof) - -// println("congruence graph built") -// println(con.g) - - var count = 0 - var c = 0 - proof foldDown checkRedundantTraversal - - - - def checkRedundantTraversal(node: N, fromPremises: Seq[(Set[App],Int)]): (Set[App],Int) = { -// println("process " + node.conclusion) - - val r = rightEqs(node) - val l = leftEqs(node) -// println("before flattening " + axiomsUsed) - - val children = proof.childrenOf(node).size - val childrenFromPr = if (fromPremises.isEmpty) 0 else fromPremises.map(_._2).max - - val maxChild = - if (childrenFromPr < children) { - children - } - else { - childrenFromPr - } - if (children > 30) { - -// var c = 0 -// val x = proof.childrenOf(node).forall(ch => { -// println("child " + " " + c + " premise contains node?: " + ch.premises.contains(node) + " " + ch) -// c = c + 1 -// println(" ") -// ch.premises.foreach(println) -// ch.premises.contains(node) +// }) +//// (count.asInstanceOf[Double] * 100) / proof.size +// count +// } +// +// def countTwoRight(proof: Proof[N]) = { +// var count = 0 +// proof.foreach(node => { +// if (hasTwoRight(node)) { +//// if (node.conclusion.size < 10) println(node.conclusion) +// count = count + 1 +// } +// }) +//// println(count +" of "+ proof.size + " have 2 eq's right") +//// (count.asInstanceOf[Double] * 100) / proof.size +// count +// } +// +// def twoRightAndCongruent(node: N): Boolean = { +// val rightEqs = node.conclusion.suc.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) +// val leftEqs = node.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) +// val s = rightEqs.size +// val twoAndCongruent = +// if (s > 0) { +// val con = new Congruence(MMap[(E,E),App]()) +// leftEqs.foreach(eq => con.addEquality(eq)) +// con.resolveDeducedQueue +// rightEqs.exists(eq => { +// val path = con.explain(eq.function.asInstanceOf[App].argument, eq.argument) +// val c = if (path.isDefined) path.get.collectLabels.size else 0 +// val out = c > 0 && c < leftEqs.size +//// if (out) { +//// println(node.conclusion + "\nshorter explanation " + path.collectLabels) +//// } +//// if (!out) println(node.conclusion) +//// println("is congruent: " + eq.function.asInstanceOf[App].argument + ", " + eq.argument + " ? " + c) +// out // }) - println("has 30 or more children: " + node) - println(node.getClass()) -// println("all children contain node as premise: " + x) -// println(node) - } - val axiomsBefore = fromPremises.foldLeft( Set[App]() )( {(A,B) => A union B._1}) -// println(c + " node: " + node + " axioms: " + axiomsBefore) - c = c + 1 - val rSize = r.size - val lSize = l.size - val axiomsAfter = if (rSize > 0) { - if (lSize > 0) { -// println("before build currentExlp") - val currentExpl = axiomsBefore ++ l -// println("after build currentExlp") - if (r.exists(eq => { -// println("before xplain") - //Still have to add left eqns! -> copy con - val newCon = l.foldLeft(con)({(A,B) => A.addEquality(B)}) - val path = newCon.explain(eq.function.asInstanceOf[App].argument, eq.argument) -// println("after xplain") - val c = if (path.isDefined) path.get.collectLabels.size else 0 - val out = c > 0 && c < currentExpl.size - if (out) { -// println("current explanation for " + r.mkString(",") + ": " + currentExpl.size + " ~ " + currentExpl) -// println("new explanation for " + r.mkString(",") + ": " + newExpl.size + " ~ " + newExpl) -// println(node + " ~ " + axiomsBefore) -// println("redundant, maxChild: " + maxChild + " current: " + children) -// println(Proof(node)) - } - out - })) count = count + 1 - axiomsBefore - } - else { - if (axiomsBefore.isEmpty && node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0) { -// println(node + " adds axiom") - axiomsBefore.++:(r) - } - else axiomsBefore - } - } - else { -// println("before flattening") - val x = axiomsBefore -// println("after flattening") - x - } - (axiomsAfter,maxChild) - } - count - } - - def buildGlobalCongruence(proof: Proof[N]) = { -// val con = new Congruence - val inputEqNodes = proof.filter(node => node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0 && node.conclusion.suc.forall(Eq.?:(_))) - val inputEqs = inputEqNodes.map(node => node.conclusion.suc.last.asInstanceOf[App]) - inputEqNodes.foreach(node => println(node.getClass())) -// println("inputEqs: " + inputEqs) - val con = inputEqs.foldLeft(new Congruence(MMap[(E,E),App]()))({(A,B) => A.addEquality(B)}).resolveDeducedQueue - con - } - - def buildGlobalCongruence2(proof: Proof[N]) = { - var con = new Congruence(MMap[(E,E),App]()) - - proof foldDown traverse - - def traverse(node: N, premisesFresh: Seq[Boolean]): Boolean = { -// println(node.conclusion) - val fresh = if (premisesFresh.size > 0) premisesFresh.min else true -// println("fresh? " + fresh) - val singleRight = node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0 && node.conclusion.suc.forall(Eq.?:(_)) -// if (singleRight && !fresh) println(node.conclusion + " denied") - if (fresh && singleRight) { - val eq = node.conclusion.suc.last.asInstanceOf[App] -// println(eq + " is an original axiom") - con = con.addEquality(eq) - false - } - else fresh - } - - con = con.resolveDeducedQueue - con - } -} \ No newline at end of file +// } +// else false +//// if (s > 0 && leftEqs.size > 0 && !twoAndCongruent) { +//// println(node.conclusion) +//// } +// twoAndCongruent +// } +// +// def hasTwoRight(node: N): Boolean = { +// val s = node.conclusion.suc.filter(Eq.?:(_)).size +//// println(s) +// s > 1 +// } +// +// def rightEqs(node: N) = node.conclusion.suc.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) +// +// def leftEqs(node: N) = node.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) +// +// +// def checkRedundant(proof: Proof[N]) = { +// +// val con = buildGlobalCongruence2(proof) +// +//// println("congruence graph built") +//// println(con.g) +// +// var count = 0 +// var c = 0 +// proof foldDown checkRedundantTraversal +// +// +// +// def checkRedundantTraversal(node: N, fromPremises: Seq[(Set[App],Int)]): (Set[App],Int) = { +//// println("process " + node.conclusion) +// +// val r = rightEqs(node) +// val l = leftEqs(node) +//// println("before flattening " + axiomsUsed) +// +// val children = proof.childrenOf(node).size +// val childrenFromPr = if (fromPremises.isEmpty) 0 else fromPremises.map(_._2).max +// +// val maxChild = +// if (childrenFromPr < children) { +// children +// } +// else { +// childrenFromPr +// } +// if (children > 30) { +// +//// var c = 0 +//// val x = proof.childrenOf(node).forall(ch => { +//// println("child " + " " + c + " premise contains node?: " + ch.premises.contains(node) + " " + ch) +//// c = c + 1 +//// println(" ") +//// ch.premises.foreach(println) +//// ch.premises.contains(node) +//// }) +// println("has 30 or more children: " + node) +// println(node.getClass()) +//// println("all children contain node as premise: " + x) +//// println(node) +// } +// val axiomsBefore = fromPremises.foldLeft( Set[App]() )( {(A,B) => A union B._1}) +//// println(c + " node: " + node + " axioms: " + axiomsBefore) +// c = c + 1 +// val rSize = r.size +// val lSize = l.size +// val axiomsAfter = if (rSize > 0) { +// if (lSize > 0) { +//// println("before build currentExlp") +// val currentExpl = axiomsBefore ++ l +//// println("after build currentExlp") +// if (r.exists(eq => { +//// println("before xplain") +// //Still have to add left eqns! -> copy con +// val newCon = l.foldLeft(con)({(A,B) => A.addEquality(B)}) +// val path = newCon.explain(eq.function.asInstanceOf[App].argument, eq.argument) +//// println("after xplain") +// val c = if (path.isDefined) path.get.collectLabels.size else 0 +// val out = c > 0 && c < currentExpl.size +// if (out) { +//// println("current explanation for " + r.mkString(",") + ": " + currentExpl.size + " ~ " + currentExpl) +//// println("new explanation for " + r.mkString(",") + ": " + newExpl.size + " ~ " + newExpl) +//// println(node + " ~ " + axiomsBefore) +//// println("redundant, maxChild: " + maxChild + " current: " + children) +//// println(Proof(node)) +// } +// out +// })) count = count + 1 +// axiomsBefore +// } +// else { +// if (axiomsBefore.isEmpty && node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0) { +//// println(node + " adds axiom") +// axiomsBefore.++:(r) +// } +// else axiomsBefore +// } +// } +// else { +//// println("before flattening") +// val x = axiomsBefore +//// println("after flattening") +// x +// } +// (axiomsAfter,maxChild) +// } +// count +// } +// +// def buildGlobalCongruence(proof: Proof[N]) = { +//// val con = new Congruence +// val inputEqNodes = proof.filter(node => node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0 && node.conclusion.suc.forall(Eq.?:(_))) +// val inputEqs = inputEqNodes.map(node => node.conclusion.suc.last.asInstanceOf[App]) +// inputEqNodes.foreach(node => println(node.getClass())) +//// println("inputEqs: " + inputEqs) +// val con = inputEqs.foldLeft(new Congruence(MMap[(E,E),App]()))({(A,B) => A.addEquality(B)}).resolveDeducedQueue +// con +// } +// +// def buildGlobalCongruence2(proof: Proof[N]) = { +// var con = new Congruence(MMap[(E,E),App]()) +// +// proof foldDown traverse +// +// def traverse(node: N, premisesFresh: Seq[Boolean]): Boolean = { +//// println(node.conclusion) +// val fresh = if (premisesFresh.size > 0) premisesFresh.min else true +//// println("fresh? " + fresh) +// val singleRight = node.conclusion.suc.size == 1 && node.conclusion.ant.size == 0 && node.conclusion.suc.forall(Eq.?:(_)) +//// if (singleRight && !fresh) println(node.conclusion + " denied") +// if (fresh && singleRight) { +// val eq = node.conclusion.suc.last.asInstanceOf[App] +//// println(eq + " is an original axiom") +// con = con.addEquality(eq) +// false +// } +// else fresh +// } +// +// con = con.resolveDeducedQueue +// con +// } +//} \ No newline at end of file