From dfaec82205f343a2b9256c9220b83d7773b48d0e Mon Sep 17 00:00:00 2001 From: AFellner Date: Wed, 7 May 2014 00:13:15 +0200 Subject: [PATCH] Implement different version of proof production with long transitivity chains and experiment with R.apply --- .../algorithm/congruence/Congruence.scala | 31 +- .../congruence/CongruenceCompressor.scala | 63 +- .../skeptik/algorithm/dijkstra/Dijkstra.scala | 6 +- .../skeptik/algorithm/dijkstra/PathTree.scala | 172 ++++- .../skeptik/expression/formula/formulas.scala | 51 +- .../at/logic/skeptik/judgment/Sequent.scala | 1 + .../skeptik/parser/ProofParserVeriT.scala | 61 +- .../skeptik/proof/sequent/lk/Congruence.scala | 42 +- .../at/logic/skeptik/proof/sequent/lk/R.scala | 12 +- .../CongruenceCompressorDebug.scala | 6 +- .../skeptik/congruence/CongruenceDebug.scala | 641 +++++++++--------- .../congruence/EquationsExperiment.scala | 7 +- 12 files changed, 666 insertions(+), 427 deletions(-) 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 a498fdd7..57bbd779 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/congruence/Congruence.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/congruence/Congruence.scala @@ -5,6 +5,7 @@ import at.logic.skeptik.expression.formula._ import at.logic.skeptik.algorithm.dijkstra._ //import scala.collection.mutable.{HashMap => MMap} import scala.collection.immutable.{HashMap => IMap} +import scala.collection.mutable.{HashMap => MMap} import scala.collection.mutable.Stack import scala.collection.immutable.Queue import scala.collection.mutable.ListBuffer @@ -19,9 +20,9 @@ import scala.collection.mutable.ListBuffer //bla[PathTree[E,]] class Congruence( + val eqReferences: MMap[(E,E),App], val find: FindTable = new FindTable(), val sigTable: SignatureTable = new SignatureTable(), - val eqReferences: IMap[(E,E),App] = new IMap[(E,E),App], val deduced: Queue[(E,E)] = Queue[(E,E)](), val g: WGraph[E,EqLabel] = new WGraph[E,EqLabel]()) { @@ -36,19 +37,19 @@ class Congruence( // def copy = def updateFind(newFind: FindTable) = { - new Congruence(newFind, sigTable, eqReferences,deduced,g) + new Congruence(eqReferences, newFind, sigTable,deduced,g) } def updateSigTable(newSigTable: SignatureTable) = { - new Congruence(find, newSigTable, eqReferences,deduced,g) - } - def updateEqReferences(newEqReferences: IMap[(E,E),App]) = { - new Congruence(find, sigTable, newEqReferences,deduced,g) + new Congruence(eqReferences, find, newSigTable,deduced,g) } +// def updateEqReferences(newEqReferences: MMap[(E,E),App]) = { +// new Congruence(find, sigTable, newEqReferences,deduced,g) +// } def updateDeduced(newDeduced: Queue[(E,E)]) = { - new Congruence(find, sigTable, eqReferences,newDeduced,g) + new Congruence(eqReferences, find, sigTable,newDeduced,g) } def updateGraph(newG: WGraph[E,EqLabel]) = { - new Congruence(find, sigTable, eqReferences,deduced,newG) + new Congruence(eqReferences, find, sigTable,deduced,newG) } def addAll(eqs: List[App]): Congruence = { @@ -57,9 +58,9 @@ class Congruence( def addEquality(eq: App): Congruence = { val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument) - val eqRef = eqReferences.updated((l,r), eq) - val c0 = updateEqReferences(eqRef) - val c1 = c0.addNode(l) + val eqRef = eqReferences.update((l,r), eq) +// val c0 = updateEqReferences(eqRef) + val c1 = this.addNode(l) val c2 = c1.addNode(r) val c3 = c2.updateGraph(c2.g.addUndirectedEdge((l,(eq,None),r), 1)) val res = c3.merge(l,r,Some(eq)) @@ -173,7 +174,7 @@ class Congruence( } def resolveDeduced(u: E, v: E): Congruence = { - val dij = new EquationDijkstra + val dij = new EquationDijkstra(eqReferences) // println("resolve deduced: " + (u,v)) u match { case App(u1,u2) => { @@ -197,7 +198,7 @@ class Congruence( // 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) + val x = Eq(u,v,eqReferences) 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)) } @@ -207,10 +208,10 @@ class Congruence( case _ => this } } - + def explain(u: E, v: E): Option[EquationTree] = { // resolveDeduced - val dij = new EquationDijkstra + val dij = new EquationDijkstra(eqReferences) // val tmpEq = Eq(u,v) // val tmpCon = addEquality(tmpEq) // val realG = tmpCon.g.removeUndirectedEdge((u,(tmpEq,None),v)) 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 d611c180..100a1fb6 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceCompressor.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/congruence/CongruenceCompressor.scala @@ -13,6 +13,7 @@ import at.logic.skeptik.algorithm.compressor._ import at.logic.skeptik.exporter.Exporter import at.logic.skeptik.exporter.skeptik.{FileExporter => SkeptikFileExporter} import at.logic.skeptik.exporter.smt.{FileExporter => SMTFileExporter} +import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent} import scala.collection.mutable.{HashMap => MMap} import scala.collection.immutable.{HashMap => IMap} @@ -20,8 +21,12 @@ import scala.collection.immutable.{HashMap => IMap} object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { def apply(proof: Proof[N]): Proof[N] = { - val (con,eqNodesLeft,eqNodesRight,allEqReferences) = buildGlobalCongruence(proof) - + val references = MMap[(E,E),App]() + 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) = { @@ -77,14 +82,47 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { val path = tree.get // println("proofing " + (path.firstVert,path.lastVert) + " from " + path.originalEqs) // println("path: " + path) - val eqRef = con.eqReferences +// val eqRef = con.eqReferences val pathProof = try { - path.toProof(allEqReferences) + println("TO PROOF with " + references + " references") + path.toProof(references) } catch { case e: Exception => { - val exporter = new SMTFileExporter("experiments/congruence/resolveBug4") - exporter.write(Proof(fixedNodeInit)) + 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 res1 = rightSideEq match{ + case Some(eq) => { +// println(eq + " is rsEq") + R(new Axiom(new Sequent(origEqs.toSeq,Seq())),fixedNodeInit) + } + case None => { + val leftSideEq = fixedNodeInit.conclusion.ant.find(expr => if (expr.isInstanceOf[App]) origEqs.contains(expr.asInstanceOf[App]) else false) + leftSideEq match{ + case Some(eq) => { +// println(eq + " is lsEq") + R(new Axiom(new Sequent(Seq(),origEqs.toSeq)),fixedNodeInit) + } + case None => { + throw new Exception("fixedNode empty? " + fixedNodeInit) + } + } + } + } + val res2 = origEqs.foldLeft(res1)({(A,B) => + val ax = new Axiom(new Sequent(Seq(),Seq(B))) + if (A.conclusion.ant.contains(B)) R(A,ax) + else A +// try R(A,ax) +// catch { +// case e: Exception => { +// A +// } +// } + }) + exporter.write(Proof(res2.asInstanceOf[N])) + exporter.flush exporter.close throw(e) @@ -140,10 +178,8 @@ object CongruenceCompressor extends (Proof[N] => Proof[N]) with fixNodes { DAGify(resProof) } - - -def buildGlobalCongruence(proof: Proof[N]): (Congruence,MMap[App,N],MMap[App,N],IMap[(E,E),App]) = { - var con = new Congruence + def buildGlobalCongruence(proof: Proof[N], references: MMap[(E,E),App]): (Congruence,MMap[App,N],MMap[App,N]) = { + var con = new Congruence(references) val eqNodesLeft = MMap[App,N]() val eqNodesRight = MMap[App,N]() @@ -164,6 +200,11 @@ def buildGlobalCongruence(proof: Proof[N]): (Congruence,MMap[App,N],MMap[App,N], val leftEqs = node.conclusion.ant.filter(Eq.?:(_)).map(f => f.asInstanceOf[App]) val bothEqs = rightEqs ++ leftEqs + bothEqs.foreach(eq => { + val (l,r) = (eq.function.asInstanceOf[App].argument,eq.argument) + references += ((l,r) -> eq) + references += ((r,l) -> eq) + }) val eqMap = bothEqs.foldLeft(premiseMap)({(A,B) => A.updated((B.function.asInstanceOf[App].argument,B.argument), B) }) @@ -200,6 +241,6 @@ def buildGlobalCongruence(proof: Proof[N]): (Congruence,MMap[App,N],MMap[App,N], val (_,_,mapRes) = proof foldDown traverse con = con.resolveDeducedQueue println("eqNodesLeft in bGC " + eqNodesLeft.mkString(",")) - (con,eqNodesLeft,eqNodesRight,mapRes) + (con,eqNodesLeft,eqNodesRight) } } \ 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 3c8a10ae..c23068b6 100644 --- a/src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala +++ b/src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala @@ -6,7 +6,7 @@ import at.logic.skeptik.expression._ import scala.collection.mutable.{HashSet => MSet} import at.logic.skeptik.expression.formula._ -class EquationDijkstra extends Dijkstra[E,EqLabel] { +class EquationDijkstra(references: MMap[(E,E),App]) extends Dijkstra[E,EqLabel](references) { def pi(u: E): EquationTree = { pathTrees.getOrElseUpdate(u,new EquationTree(u,None)) @@ -24,7 +24,7 @@ class EquationDijkstra extends Dijkstra[E,EqLabel] { // } } -abstract class Dijkstra[T1,T2] { +abstract class Dijkstra[T1,T2](references: MMap[(E,E),App]) { val distances = MMap[T1,Int]() val pathTrees = MMap[T1,EquationTree]() @@ -52,7 +52,7 @@ abstract class Dijkstra[T1,T2] { if (s == target && s.isInstanceOf[E]) { val sE = s.asInstanceOf[E] val end = new EquationTree(sE,None) - val x = Eq(sE,sE) + val x = Eq(sE,sE,references) 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 580680b2..8edb37db 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.expression.formula._ import at.logic.skeptik.expression._ import at.logic.skeptik.proof._ import at.logic.skeptik.proof.sequent.{SequentProofNode => N} @@ -7,6 +8,7 @@ import at.logic.skeptik.judgment._ import at.logic.skeptik.proof.sequent.lk._ 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) { val eq = label._1 @@ -15,42 +17,102 @@ class EqTreeEdge(val nextTree: EquationTree, val label: EqLabel) extends (Equati case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { - def toProof(eqReferences: IMap[(E,E),App]): Option[Proof[N]] = buildTransChain(eqReferences) match { - case Some((Some(node),deduced,eq)) => { -// println("have " + node) -// println("still have to resolve the following deduced nodes: " + deduced) - val x = Some(Proof(deduced.foldLeft(node)({(A,B) => R(A,B)}))) -// println("results in: " + x) - x - } - case Some((None,ded,_)) if !ded.isEmpty => { - if (ded.size > 1) println("more than one deduced with empty node") - Some(ded.last) - } - case _ => None - } +// def toProof(eqReferences: MMap[(E,E),App]): 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 { +// case Some((Some(node),deduced,eq)) => { +// +// // println(eqReferences.hashCode) +// // println("have " + node) +// // println("still have to resolve the following deduced nodes: " + deduced) +// val x = Some(Proof(deduced.foldLeft(node)({(A,B) => +// try R(A,B) +// catch { +// case e: Exception => { +// println("=================== BUG ================") +// println("trans chain node: " + node) +// println("eqTree: " + this) +// println("deduced:") +// println(deduced.mkString("\n")) +// println("=================== BUG ================") +// throw e +// } +// } +// }))) +// // println("results in: " + x) +// x +// } +// case Some((None,ded,_)) if !ded.isEmpty => { +// if (ded.size > 1) println("more than one deduced with empty node") +// Some(ded.last) +// } +// case _ => None +// } +// } - def buildDeduction(dd1: EquationTree, dd2: EquationTree, eq: E, eqReferences: IMap[(E,E),App]): N = { + def buildDeduction(dd1: EquationTree, dd2: EquationTree, eq: E, eqReferences: MMap[(E,E),App]): 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" val ddEqs = ddProofRoots.map(_.conclusion.suc.last).toSeq - println("deducing " + eq) - println("trees: " + dd1 + " and " + dd2) - println("proofs: " + dd1Opt.isDefined + " and " + dd2Opt.isDefined) +// 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 res = if (ddEqs.isEmpty) { - val x = dd1.originalEqs.map(_.asInstanceOf[E]).toSeq ++: dd2.originalEqs.map(_.asInstanceOf[E]).toSeq - EqCongruent(x,eq) +// 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 { - val congr = EqCongruent(ddEqs) +// 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) } } @@ -59,20 +121,74 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { res } - def transChainProof(eqReferences: IMap[(E,E),App]): Option[Proof[N]] = buildTransChain(eqReferences) match { - case Some((Some(node),_,_)) => Some(Proof(node)) - case Some((_,ded,_)) => Some(ded.last) - case _ => None +// def transChainProof(eqReferences: MMap[(E,E),App]): Option[Proof[N]] = buildTransChain(eqReferences) match { +// case Some((Some(node),_,_)) => Some(Proof(node)) +// case Some((_,ded,_)) => Some(ded.last) +// case _ => None +// } + + def toProof(eqReferences: MMap[(E,E),App]): Option[Proof[N]] = { + val (first,last,equations,deduced) = this.buildTransChain(eqReferences) + if (equations.size > 1) { + val transNode = EqTransitive(equations,first,last,eqReferences) + val res = deduced.foldLeft(transNode.asInstanceOf[N])({(A,B) => + val resEq = B._2 + val resNode = B._1 + try { + R(A,resNode,resEq) + } + catch { + case e:Exception => { + try R(resNode,A,resEq) + 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("trying to resolve upon " + B._2 + B._2.hashCode) +// println(Proof(A)) +// println(Proof(B._1)) + throw e1 + } + } + } + } + }) + Some(res) + } + else if (deduced.size == 1) { + Some(deduced.last._1) + } + 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 buildTransChain(eqReferences: IMap[(E,E),App]): Option[(Option[N],Set[N],E)] = pred match { + 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.buildTransChain(eqReferences) + val resultFromNext = nextTree.buildTransChain1(eqReferences) resultFromNext match { case Some((nodeOpt,deducedRes,eqRes)) => { @@ -214,7 +330,7 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdge]) { } val predLabel = if (labels) eq match { - case Some(e) => "-["+e+"]" + "{"+deducedEqs+"}" + case Some(e) => "{"+deducedEqs+"}"//"-["+e+"]" + "{"+deducedEqs+"}" case None => "" } else "" 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 be270478..34d41322 100644 --- a/src/main/scala/at/logic/skeptik/expression/formula/formulas.scala +++ b/src/main/scala/at/logic/skeptik/expression/formula/formulas.scala @@ -48,10 +48,55 @@ object Or extends BinaryFormula(orC) object Imp extends BinaryFormula(impC) object Eq { - def apply(term1: E, term2: E): App = { +// 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),App]): App = { require(term1.t == term2.t) - val t1Type = term1.t - new Equation(t1Type)(term1,term2) +// 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)) { diff --git a/src/main/scala/at/logic/skeptik/judgment/Sequent.scala b/src/main/scala/at/logic/skeptik/judgment/Sequent.scala index 096e6321..e6b34a86 100644 --- a/src/main/scala/at/logic/skeptik/judgment/Sequent.scala +++ b/src/main/scala/at/logic/skeptik/judgment/Sequent.scala @@ -21,4 +21,5 @@ abstract class Sequent extends Judgment with SequentLike[Sequent] { def canEqual(other: Any) = other.isInstanceOf[Sequent] override def hashCode = 42*ant.hashCode + suc.hashCode override def toString = ant.mkString(", ") + unicodeOrElse(" \u22A2 "," :- ") + suc.mkString(", ") +// override def toString = ant.map(x => x + " ~ " + x.hashCode).mkString(", ") + unicodeOrElse(" \u22A2 "," :- ") + suc.map(x => x + " ~ " + x.hashCode).mkString(", ") } \ No newline at end of file diff --git a/src/main/scala/at/logic/skeptik/parser/ProofParserVeriT.scala b/src/main/scala/at/logic/skeptik/parser/ProofParserVeriT.scala index d7b5fbab..a1f8ffec 100644 --- a/src/main/scala/at/logic/skeptik/parser/ProofParserVeriT.scala +++ b/src/main/scala/at/logic/skeptik/parser/ProofParserVeriT.scala @@ -40,20 +40,20 @@ extends JavaTokenParsers with RegexParsers { def inference: Parser[Node] = (resolution | axiom | unchecked) def resolution: Parser[Node] = "resolution" ~> premises <~ conclusion ^^ { - list => resolveClauses(list) -// list => { -// (list.head /: list.tail) { (left, right) => -// try { -// R(left, right) -// } -// catch { -// case e: Exception => { -// -// throw(e) -// } -// } -// } -// } +// list => resolveClauses(list) + list => { + (list.head /: list.tail) { (left, right) => + try { + R(left, right) + } + catch { + case e: Exception => { + + throw(e) + } + } + } + } } /** @@ -115,19 +115,32 @@ extends JavaTokenParsers with RegexParsers { val negClause = negOc(p).last val newClause = R(posClause,negClause,p,false) newClause.conclusion.suc.foreach(v => { - posOc(v) -= posClause - posOc(v) -= negClause - posOc(v) += newClause + posOc.get(v) match { + case None => posOc += (v -> MSet[Node](newClause)) + case Some(set) => { + set -= posClause + set -= negClause + set += newClause + } + } }) newClause.conclusion.ant.foreach(v => { - negOc(v) -= posClause - negOc(v) -= negClause - negOc(v) += newClause + negOc.get(v) match { + case None => negOc += (v -> MSet[Node](newClause)) + case Some(set) => { + set -= posClause + set -= negClause + set += newClause + } + } }) - val newPOc = posOc - p - val newNegOc = negOc - p - if (newPOc.isEmpty && newNegOc.isEmpty) newClause - else res(newPOc,newNegOc) + if (posOc.contains(p) || negOc.contains(p)) { + val newPOc = posOc - p + val newNegOc = negOc - p + if (newPOc.isEmpty && newNegOc.isEmpty) newClause + else res(newPOc,newNegOc) + } + else newClause } } } 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 cc0e6696..6993b6d4 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 @@ -6,6 +6,7 @@ import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent} import at.logic.skeptik.expression._ import at.logic.skeptik.expression.formula._ import scala.collection.immutable.{HashMap => IMap} +import scala.collection.mutable.{HashMap => MMap} abstract class EqAxiom(override val mainFormulas: Sequent) extends SequentProofNode with Nullary with NoImplicitContraction { @@ -18,12 +19,12 @@ class EqReflexive(override val mainFormulas: Sequent) extends EqAxiom(mainFormul object EqReflexive { def apply(conclusion: Sequent) = new EqReflexive(conclusion) - def apply(expr: E, eqReferences: IMap[(E,E),App]) = { + def apply(expr: E, eqReferences: MMap[(E,E),App]) = { expr match { case App(App(e,t1),t2) if (t1 == t2 && Eq.?:(expr)) => new EqReflexive(new Sequent(Seq(),Seq(expr))) case _ => { if (expr.t == i) { - val x = eqReferences.getOrElse((expr,expr), Eq(expr,expr)) + val x = eqReferences.getOrElse((expr,expr), Eq(expr,expr,eqReferences)) 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))) } @@ -42,8 +43,14 @@ object EqReflexive { class EqTransitive(override val mainFormulas: Sequent) extends EqAxiom(mainFormulas) object EqTransitive { + def apply(conclusion: Sequent) = new EqTransitive(conclusion) - def apply(eq1: E, eq2: E, eqReferences: IMap[(E,E),App]) = { + + 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(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)) => { @@ -53,20 +60,21 @@ object EqTransitive { 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 = 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) - println("Have to create " + y + " myself in EqTransitive") - println("eqs: " + eqReferences.values.mkString(",")) - y - } - } - } - } + 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))) } 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 aa2c1cc8..0cea8561 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 @@ -39,7 +39,16 @@ object R { case (None, Some(auxR)) if returnPremiseOnfailure => leftPremise case (Some(auxL), None) if returnPremiseOnfailure => rightPremise case (None, None) if returnPremiseOnfailure => choosePremise(leftPremise, rightPremise) - case _ => throw new Exception("Auxiliary formulas not found.") +// case (None, None) => { +// (leftPremise.conclusion.ant.find(_ == pivot), rightPremise.conclusion.suc.find(_ == pivot)) match { +// case (Some(auxL), Some(auxR)) => new R(rightPremise, leftPremise, auxR, auxL) +// case (None, Some(auxR)) if returnPremiseOnfailure => leftPremise +// case (Some(auxL), None) if returnPremiseOnfailure => rightPremise +// case (None, None) if returnPremiseOnfailure => choosePremise(leftPremise, rightPremise) +// 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 apply(premise1:SequentProofNode, premise2:SequentProofNode) = { @@ -49,7 +58,6 @@ object R { } findPivots(premise1,premise2) match { case Some((auxL,auxR)) => { - if (auxL.toString == "((f2 c_5 c_2) = c_3)") println("<<<>>>") new R(premise1,premise2,auxL,auxR) } case None => findPivots(premise2,premise1) match { diff --git a/src/test/scala/at/logic/skeptik/congruence/CongruenceCompressorDebug.scala b/src/test/scala/at/logic/skeptik/congruence/CongruenceCompressorDebug.scala index 3063a98a..513b03a0 100644 --- a/src/test/scala/at/logic/skeptik/congruence/CongruenceCompressorDebug.scala +++ b/src/test/scala/at/logic/skeptik/congruence/CongruenceCompressorDebug.scala @@ -1,10 +1,13 @@ package at.logic.skeptik.congruence +import at.logic.skeptik.expression.formula._ +import at.logic.skeptik.expression._ import at.logic.skeptik.algorithm.congruence._ import at.logic.skeptik.parser.ProofParserVeriT import at.logic.skeptik.parser.ProofParserSkeptik import at.logic.skeptik.proof.measure import at.logic.skeptik.util.io.Input +import scala.collection.mutable.{HashMap => MMap} object CongruenceCompressorDebug { @@ -13,7 +16,7 @@ object CongruenceCompressorDebug { val reader = new Input("F:/Proofs/QF_UF/seq_files") // val file = "F:/Proofs/QF_UF/SEQ/SEQ005_size6.smt2" // val file = "experiments/congruence/resolveBug.s" - val file = "experiments/congruence/resolveBug3.smt2" + val file = "experiments/congruence/resolveBug10_1.smtb" val parser = ProofParserVeriT // val parser = ProofParserSkeptik if (multiple) { @@ -32,6 +35,7 @@ object CongruenceCompressorDebug { } else { val proof = parser.read(file) +// println(proof) val newProof = CongruenceCompressor(proof) println(measure(proof)) println(measure(newProof)) diff --git a/src/test/scala/at/logic/skeptik/congruence/CongruenceDebug.scala b/src/test/scala/at/logic/skeptik/congruence/CongruenceDebug.scala index d162b3ca..eb34e199 100644 --- a/src/test/scala/at/logic/skeptik/congruence/CongruenceDebug.scala +++ b/src/test/scala/at/logic/skeptik/congruence/CongruenceDebug.scala @@ -1,326 +1,327 @@ -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.algorithm.congruence._ -import at.logic.skeptik.algorithm.dijkstra._ -import at.logic.skeptik.proof._ - -object CongruenceDebug { - def main(args: Array[String]):Unit = { -// val proof = ProofParserVeriT.read("F:/Proofs/QF_UF/QG-classification/qg6/iso_icl_sk004.smt2") -// CongruenceTest(proof) - val testcase = 5 - - val t = o - - val a = new Var("a",t) - val a1 = new Var("a1",t) - val a2 = new Var("a2",t) - val a3 = new Var("a3",t) - val b = new Var("b",t) - val b1 = new Var("b1",t) - val b2 = new Var("b2",t) - val b3 = new Var("b3",t) - val c = new Var("c",t) - val c1 = new Var("c1",t) - val c2 = new Var("c2",t) - val c3 = new Var("c3",t) - - val d = new Var("d",t) - val e = new Var("e",t) - - val f = new Var("f",Arrow(t,t)) - - val x = new Var("x",Arrow(t,t)) - - val op = new Var("op",Arrow(t,Arrow(t,t))) - val e4 = new Var("e4",t) - val skc1 = new Var("skc1",t) - val e3 = new Var("e3",t) - val e1 = new Var("e1",t) - -// println(App(x,b).t) +//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.algorithm.congruence._ +//import at.logic.skeptik.algorithm.dijkstra._ +//import at.logic.skeptik.proof._ +//import scala.collection.mutable.{HashMap => MMap} +// +//object CongruenceDebug { +// def main(args: Array[String]):Unit = { +//// val proof = ProofParserVeriT.read("F:/Proofs/QF_UF/QG-classification/qg6/iso_icl_sk004.smt2") +//// CongruenceTest(proof) +// val testcase = 5 // -// val z1 = App(f,App(x,b)) -// val z2 = App(f,App(x,c)) +// val t = o // -// println(z1 + " type: " + z1.t) -// println(z2 + " type: " + z2.t+"\n") - -// Eq(App(f,a),App(f,a)) - - var con = new Congruence - - val dij = new EquationDijkstra - - testcase match { - case 0 => { - //a = b; b = c; f(a) = d; f(c) = e; - - val t1 = new App(f,a) - val t2 = new App(f,c) - - val eq1 = Eq(a,b) - val eq2 = Eq(b,c) - - val eq3 = Eq(t1,d) - val eq4 = Eq(t2,e) - - println("Input: " + List(eq1,eq2,eq3,eq4).mkString(",")) - - con = con.addEquality(eq1) - con = con.addEquality(eq2) - con = con.addEquality(eq3) - con = con.addEquality(eq4) - -// con = con.resolveDeducedQueue - - - - println(con.find) - println(con.g) - val path = dij(e,d,con.g) - // println(t1 + " = " + t2 + " because: " + con.explain(t1, t2).collectLabels) - println(path) - println(e + " = " + d + " because: " + path.allEqs) - - val eqRef = con.eqReferences - - println("\n"+path.toProof(eqRef).get) -// println("trans chain?: " + con.pathTreetoProof(path)) - } - case 1 => { - - //a = b1, b1 = b2, b2 = b3, b3 = c, f(a1)=a, f(c1) = c, a1 = c1 -// val t1 = App(App(f,a1),a1) -// val t2 = App(App(f,c1),c1) - - val t1 = App(f,a1) - val t2 = App(f,c1) - - con = con.addEquality(Eq(a,b1)) - con = con.addEquality(Eq(b1,b2)) - con = con.addEquality(Eq(b2,b3)) - con = con.addEquality(Eq(b3,c)) - con = con.addEquality(Eq(t1,a)) - con = con.addEquality(Eq(t2,c)) - con = con.addEquality(Eq(a1,c1)) - -// con.resolveDeduced - - println(con.find) - println(con.g) - - val path = dij(a,c,con.g) - println("distance of " + c + " to " + a + ": " + dij.distances.getOrElse(c,Integer.MAX_VALUE)) - println(a + " = " + c + " because: " + path.collectLabels) - - con = con.resolveDeducedQueue -// con = con.resolveDeduced(t1, t2) - val path2 = dij(a,c,con.g) - println("distance after " + c + " to " + a + ": " + dij.distances.getOrElse(c,Integer.MAX_VALUE)) - println(a + " = " + c + " because: " + path2.collectLabels) - val eqRef = con.eqReferences - println("\n"+path.toProof(eqRef).get) - } - case 2 => { - //a1 = b1, a1 = c1, f(a1) = a, f(b1) = b, f(c1) = c - val t1 = App(f,a1) - val t2 = App(f,b1) - val t3 = App(f,c1) - - con = con.addEquality(Eq(a1,b1)) - con = con.addEquality(Eq(a1,c1)) - con = con.addEquality(Eq(t1,a)) - con = con.addEquality(Eq(t2,b)) - con = con.addEquality(Eq(t3,c)) - -// con.resolveDeduced - - val path = dij(a,c,con.g) - println(con.g) - println(con.sigTable) - println("distance of " + c + " to " + a + ": " + dij.distances.getOrElse(c,Integer.MAX_VALUE)) - println(a + " = " + c + " because: " + path.allEqs) - val eqRef = con.eqReferences - println("\n"+path.toProof(eqRef).get) - } - - case 3 => { - //g(l,h) = d, c = d, g(l,d) = a, e = c, e = b, b = h - - val g = new Var("g",Arrow(t,Arrow(t,t))) - val l = new Var("l",t) -// val i = new Var("i",Arrow(i,i)) - val h = new Var("h",t) - - val t1 = App(App(g,l),h) - val t2 = App(App(g,l),d) - - val eqs = List(Eq(t1,d),Eq(c,d),Eq(t2,a),Eq(e,c),Eq(e,b),Eq(b1,b),Eq(b1,h)) - println("===Input: " + eqs.mkString(",")) - con = eqs.foldLeft(con)({(A,B) => A.addEquality(B)}) -// con = con.addEquality(Eq(t1,d)) -// con = con.addEquality(Eq(c,d)) -// con = con.addEquality(Eq(t2,a)) -// con = con.addEquality(Eq(e,c)) -// con = con.addEquality(Eq(e,b)) -// con = con.addEquality(Eq(b1,b)) -// con = con.addEquality(Eq(b1,h)) - -// con = con.resolveDeducedQueue - - - +// val a = new Var("a",t) +// val a1 = new Var("a1",t) +// val a2 = new Var("a2",t) +// val a3 = new Var("a3",t) +// val b = new Var("b",t) +// val b1 = new Var("b1",t) +// val b2 = new Var("b2",t) +// val b3 = new Var("b3",t) +// val c = new Var("c",t) +// val c1 = new Var("c1",t) +// val c2 = new Var("c2",t) +// val c3 = new Var("c3",t) +// +// val d = new Var("d",t) +// val e = new Var("e",t) +// +// val f = new Var("f",Arrow(t,t)) +// +// val x = new Var("x",Arrow(t,t)) +// +// val op = new Var("op",Arrow(t,Arrow(t,t))) +// val e4 = new Var("e4",t) +// val skc1 = new Var("skc1",t) +// val e3 = new Var("e3",t) +// val e1 = new Var("e1",t) +// +//// println(App(x,b).t) +//// +//// val z1 = App(f,App(x,b)) +//// val z2 = App(f,App(x,c)) +//// +//// println(z1 + " type: " + z1.t) +//// println(z2 + " type: " + z2.t+"\n") +// +//// Eq(App(f,a),App(f,a)) +// +// var con = new Congruence +// +// val dij = new EquationDijkstra +// +// testcase match { +// case 0 => { +// //a = b; b = c; f(a) = d; f(c) = e; +// +// val t1 = new App(f,a) +// val t2 = new App(f,c) +// +// val eq1 = Eq(a,b) +// val eq2 = Eq(b,c) +// +// val eq3 = Eq(t1,d) +// val eq4 = Eq(t2,e) +// +// println("Input: " + List(eq1,eq2,eq3,eq4).mkString(",")) +// +// con = con.addEquality(eq1) +// con = con.addEquality(eq2) +// con = con.addEquality(eq3) +// con = con.addEquality(eq4) +// +//// con = con.resolveDeducedQueue +// +// +// +// println(con.find) +// println(con.g) +// val path = dij(e,d,con.g) +// // println(t1 + " = " + t2 + " because: " + con.explain(t1, t2).collectLabels) +// println(path) +// println(e + " = " + d + " because: " + path.allEqs) +// +// val eqRef = con.eqReferences +// +// println("\n"+path.toProof(MMap[(E,E),App]() ++ eqRef).get) +//// println("trans chain?: " + con.pathTreetoProof(path)) +// } +// case 1 => { +// +// //a = b1, b1 = b2, b2 = b3, b3 = c, f(a1)=a, f(c1) = c, a1 = c1 +//// val t1 = App(App(f,a1),a1) +//// val t2 = App(App(f,c1),c1) +// +// val t1 = App(f,a1) +// val t2 = App(f,c1) +// +// con = con.addEquality(Eq(a,b1)) +// con = con.addEquality(Eq(b1,b2)) +// con = con.addEquality(Eq(b2,b3)) +// con = con.addEquality(Eq(b3,c)) +// con = con.addEquality(Eq(t1,a)) +// con = con.addEquality(Eq(t2,c)) +// con = con.addEquality(Eq(a1,c1)) +// +//// con.resolveDeduced +// +// println(con.find) +// println(con.g) +// +// val path = dij(a,c,con.g) +// println("distance of " + c + " to " + a + ": " + dij.distances.getOrElse(c,Integer.MAX_VALUE)) +// println(a + " = " + c + " because: " + path.collectLabels) +// // con = con.resolveDeducedQueue - - val path = dij(a,b,con.g) - println(con.g) - println("distance of " + a + " to " + b + ": " + dij.distances.getOrElse(b,Integer.MAX_VALUE)) - println(a + " = " + b + " because: " + path.allEqs) - val eqRef = con.eqReferences - - val eqs2 = List(Eq(d,c1),Eq(c1,c2),Eq(c2,c3),Eq(c3,h)) - println("\n\n\n===Input: " + (eqs ++ eqs2).mkString(",")) - con = eqs2.foldLeft(con)({(A,B) => A.addEquality(B)}) -// con = con.addEquality(Eq(d,c1)) +//// con = con.resolveDeduced(t1, t2) +// val path2 = dij(a,c,con.g) +// println("distance after " + c + " to " + a + ": " + dij.distances.getOrElse(c,Integer.MAX_VALUE)) +// println(a + " = " + c + " because: " + path2.collectLabels) +// val eqRef = con.eqReferences +// println("\n"+path.toProof(MMap[(E,E),App]() ++ eqRef).get) +// } +// case 2 => { +// //a1 = b1, a1 = c1, f(a1) = a, f(b1) = b, f(c1) = c +// val t1 = App(f,a1) +// val t2 = App(f,b1) +// val t3 = App(f,c1) +// +// con = con.addEquality(Eq(a1,b1)) +// con = con.addEquality(Eq(a1,c1)) +// con = con.addEquality(Eq(t1,a)) +// con = con.addEquality(Eq(t2,b)) +// con = con.addEquality(Eq(t3,c)) +// +//// con.resolveDeduced +// +// val path = dij(a,c,con.g) +// println(con.g) +// println(con.sigTable) +// println("distance of " + c + " to " + a + ": " + dij.distances.getOrElse(c,Integer.MAX_VALUE)) +// println(a + " = " + c + " because: " + path.allEqs) +// val eqRef = con.eqReferences +// println("\n"+path.toProof(MMap[(E,E),App]() ++ eqRef).get) +// } +// +// case 3 => { +// //g(l,h) = d, c = d, g(l,d) = a, e = c, e = b, b = h +// +// val g = new Var("g",Arrow(t,Arrow(t,t))) +// val l = new Var("l",t) +//// val i = new Var("i",Arrow(i,i)) +// val h = new Var("h",t) +// +// val t1 = App(App(g,l),h) +// val t2 = App(App(g,l),d) +// +// val eqs = List(Eq(t1,d),Eq(c,d),Eq(t2,a),Eq(e,c),Eq(e,b),Eq(b1,b),Eq(b1,h)) +// println("===Input: " + eqs.mkString(",")) +// con = eqs.foldLeft(con)({(A,B) => A.addEquality(B)}) +//// con = con.addEquality(Eq(t1,d)) +//// con = con.addEquality(Eq(c,d)) +//// con = con.addEquality(Eq(t2,a)) +//// con = con.addEquality(Eq(e,c)) +//// con = con.addEquality(Eq(e,b)) +//// con = con.addEquality(Eq(b1,b)) +//// con = con.addEquality(Eq(b1,h)) +// +//// con = con.resolveDeducedQueue +// +// +// +//// con = con.resolveDeducedQueue +// +// val path = dij(a,b,con.g) +// println(con.g) +// println("distance of " + a + " to " + b + ": " + dij.distances.getOrElse(b,Integer.MAX_VALUE)) +// println(a + " = " + b + " because: " + path.allEqs) +// val eqRef = con.eqReferences +// +// val eqs2 = List(Eq(d,c1),Eq(c1,c2),Eq(c2,c3),Eq(c3,h)) +// println("\n\n\n===Input: " + (eqs ++ eqs2).mkString(",")) +// con = eqs2.foldLeft(con)({(A,B) => A.addEquality(B)}) +//// con = con.addEquality(Eq(d,c1)) +////// con = con.addEquality(Eq(c1,c2)) //// con = con.addEquality(Eq(c1,c2)) -// con = con.addEquality(Eq(c1,c2)) -// con = con.addEquality(Eq(c2,c3)) -// con = con.addEquality(Eq(c3,h)) - - con = con.resolveDeducedQueue - - val eqRefs2 = con.eqReferences - - val dij2 = new EquationDijkstra - - val path2 = dij2(a,b,con.g) - println(con.g) - println("distance of " + a + " to " + b + ": " + dij2.distances.getOrElse(b,Integer.MAX_VALUE)) - println(a + " = " + b + " because: " + path2.allEqs) - -// println("trans chain?: " + path2.toProof) - - - println("\n"+path.toProof(eqRef).get) - - println("\n"+path2.toProof(eqRefs2).get) - } - case 4 => { - //(op e4 e3),(op e3 e3) from - //((op (op e4 skc1) (op skc1 e4)) = (op e3 e3)), ((op (op e4 skc1)) = (op e3)), (e4 = (op e4 e3)), (e3 = (op e1 e4)), (e4 = (op (op e4 skc1) (op skc1 e4))), ((op e1 e4) = (op skc1 e4))) - //((op (op e4 skc1)) = (op e3)), (e4 = (op e4 e3)), ((op (op e3 skc1) (op skc1 e3)) = e3), (e3 = (op e1 e4)), ((op (op e3 skc1) (op skc1 e3)) = (op e4 skc1)), (e4 = (op (op e4 skc1) (op skc1 e4))), ((op e1 e4) = (op skc1 e4)) - - - //((op e1 e3) = e1), (e4 = (op e4 e3)), ((op (op e3 skc1) (op skc1 e3)) = e3), (e1 = skc1), (e3 = (op e1 e4)), (e4 = (op e3 e1)), ((op e1 e3) = (op skc1 e3)), (e4 = (op (op e4 skc1) (op skc1 e4))), ((op e1 e4) = (op skc1 e4)) - - val subt1 = App(App(op,e4),skc1) // (op e4 skc1) - val subt2 = App(App(op,skc1),e4) // (op skc1 e4) - val t1 = App(App(op,subt1),subt2) //(op (op e4 skc1) (op skc1 e4)) - val t2 = App(App(op,e3),e3) // (op e3 e3) - val t3 = App(op,subt1) //(op (op e4 skc1)) - val t4 = App(op,e3) //(op e3) - val t5 = App(App(op,e1),e4) //(op e1 e4) - val t6 = App(App(op,e4),e3) //(op e4 e3) - val t7 = App(App(op,e1),skc1) //(op e1 e3) - val subt3 = App(App(op,e3),skc1) //(op e3 skc1) - val subt4 = App(App(op,skc1),e3) //(op skc1 e3) - val t8 = App(App(op,subt3),subt4) // (op (op e3 skc1) (op skc1 e3)) - val t9 = App(App(op,e1),e4) //(op e1 e4) - val t10 = App(App(op,e3),e1) //(op e3 e1) - - val eq1 = Eq(t7,e1) // (op e1 e3) = e1) - val eq2 = Eq(e4,t6) // (e4 = (op e4 e3)) - val eq3 = Eq(t8,e3) // ((op (op e3 skc1) (op skc1 e3)) = e3) - val eq4 = Eq(e1,skc1) // (e1 = skc1) - val eq5 = Eq(e3,t5) // (e3 = (op e1 e4)) - val eq6 = Eq(e4,t10) // (e4 = (op e3 e1)) - val eq7 = Eq(t7,subt4)// ((op e1 e3) = (op skc1 e3)) - val eq8 = Eq(e4,t1) //(e4 = (op (op e4 skc1) (op skc1 e4))) - val eq9 = Eq(t5,subt2) //((op e1 e4) = (op skc1 e4)) - val allEqs = List(eq1,eq2,eq3,eq4,eq5,eq6,eq7,eq8,eq9) - - println(allEqs) - - con = con.addAll(allEqs) - con = con.resolveDeducedQueue - - val eqRef = con.eqReferences - - val path = con.explain(t2,t6) - println(path) - println(path.get.toProof(eqRef)) - } - case 5 => { - //((op e3 e1),(op e3 e3)) - //((e3 = (op e4 e4)), (e4 = skc1), (e4 = (op e3 e1)), ((op e4 e4) = (op skc1 e4)), (e4 = (op (op e4 skc1) (op skc1 e4))) - - val t1 = App(App(op,e4),e4) //(op e4 e4) - val t2 = App(App(op,e3),e1) //(op e3 e1) - val t3 = App(App(op,skc1),e4) // (op skc1 e4) - val subt1 = App(App(op,e4),skc1) // (op e4 skc1) - val t4 = App(App(op,subt1),t3) //(op (op e4 skc1) (op skc1 e4)) - - val t5 = App(App(op,e3),e3) //(op e3 e3) - - val eq1 = Eq(e3,t1) - val eq2 = Eq(e4,skc1) - val eq3 = Eq(e4,t2) - val eq4 = Eq(t1,t3) - val eq5 = Eq(e4,t4) - val allEqs = List(eq1,eq2,eq3,eq4,eq5) - - println(allEqs) - - con = con.addAll(allEqs) - println(con.g) +//// con = con.addEquality(Eq(c2,c3)) +//// con = con.addEquality(Eq(c3,h)) +// +// con = con.resolveDeducedQueue +// +// val eqRefs2 = con.eqReferences +// +// val dij2 = new EquationDijkstra +// +// val path2 = dij2(a,b,con.g) +// println(con.g) +// println("distance of " + a + " to " + b + ": " + dij2.distances.getOrElse(b,Integer.MAX_VALUE)) +// println(a + " = " + b + " because: " + path2.allEqs) +// +//// println("trans chain?: " + path2.toProof) +// +// +// println("\n"+path.toProof(MMap[(E,E),App]() ++ eqRef).get) +// +// println("\n"+path2.toProof(MMap[(E,E),App]() ++ eqRefs2).get) +// } +// case 4 => { +// //(op e4 e3),(op e3 e3) from +// //((op (op e4 skc1) (op skc1 e4)) = (op e3 e3)), ((op (op e4 skc1)) = (op e3)), (e4 = (op e4 e3)), (e3 = (op e1 e4)), (e4 = (op (op e4 skc1) (op skc1 e4))), ((op e1 e4) = (op skc1 e4))) +// //((op (op e4 skc1)) = (op e3)), (e4 = (op e4 e3)), ((op (op e3 skc1) (op skc1 e3)) = e3), (e3 = (op e1 e4)), ((op (op e3 skc1) (op skc1 e3)) = (op e4 skc1)), (e4 = (op (op e4 skc1) (op skc1 e4))), ((op e1 e4) = (op skc1 e4)) +// +// +// //((op e1 e3) = e1), (e4 = (op e4 e3)), ((op (op e3 skc1) (op skc1 e3)) = e3), (e1 = skc1), (e3 = (op e1 e4)), (e4 = (op e3 e1)), ((op e1 e3) = (op skc1 e3)), (e4 = (op (op e4 skc1) (op skc1 e4))), ((op e1 e4) = (op skc1 e4)) +// +// val subt1 = App(App(op,e4),skc1) // (op e4 skc1) +// val subt2 = App(App(op,skc1),e4) // (op skc1 e4) +// val t1 = App(App(op,subt1),subt2) //(op (op e4 skc1) (op skc1 e4)) +// val t2 = App(App(op,e3),e3) // (op e3 e3) +// val t3 = App(op,subt1) //(op (op e4 skc1)) +// val t4 = App(op,e3) //(op e3) +// val t5 = App(App(op,e1),e4) //(op e1 e4) +// val t6 = App(App(op,e4),e3) //(op e4 e3) +// val t7 = App(App(op,e1),skc1) //(op e1 e3) +// val subt3 = App(App(op,e3),skc1) //(op e3 skc1) +// val subt4 = App(App(op,skc1),e3) //(op skc1 e3) +// val t8 = App(App(op,subt3),subt4) // (op (op e3 skc1) (op skc1 e3)) +// val t9 = App(App(op,e1),e4) //(op e1 e4) +// val t10 = App(App(op,e3),e1) //(op e3 e1) +// +// val eq1 = Eq(t7,e1) // (op e1 e3) = e1) +// val eq2 = Eq(e4,t6) // (e4 = (op e4 e3)) +// val eq3 = Eq(t8,e3) // ((op (op e3 skc1) (op skc1 e3)) = e3) +// val eq4 = Eq(e1,skc1) // (e1 = skc1) +// val eq5 = Eq(e3,t5) // (e3 = (op e1 e4)) +// val eq6 = Eq(e4,t10) // (e4 = (op e3 e1)) +// val eq7 = Eq(t7,subt4)// ((op e1 e3) = (op skc1 e3)) +// val eq8 = Eq(e4,t1) //(e4 = (op (op e4 skc1) (op skc1 e4))) +// val eq9 = Eq(t5,subt2) //((op e1 e4) = (op skc1 e4)) +// val allEqs = List(eq1,eq2,eq3,eq4,eq5,eq6,eq7,eq8,eq9) +// +// println(allEqs) +// +// con = con.addAll(allEqs) // con = con.resolveDeducedQueue -// println("XXXXXXXXXXXXXXXXXX BEFORE ADDING") - con = con.addNode(t5) -// println("XXXXXXXXXXXXXXXXXX AFTER ADDING") - val eqRef = con.eqReferences - val path = con.explain(t5,t2) - -// println(path.get.toProof) - - val path2 = con.explain(e3,subt1) - println(path2) -// println(path2.get.toProof) - +// +// val eqRef = con.eqReferences +// +// val path = con.explain(t2,t6) +// println(path) +// println(path.get.toProof(MMap[(E,E),App]() ++ eqRef)) +// } +// case 5 => { +// //((op e3 e1),(op e3 e3)) +// //((e3 = (op e4 e4)), (e4 = skc1), (e4 = (op e3 e1)), ((op e4 e4) = (op skc1 e4)), (e4 = (op (op e4 skc1) (op skc1 e4))) +// +// val t1 = App(App(op,e4),e4) //(op e4 e4) +// val t2 = App(App(op,e3),e1) //(op e3 e1) +// val t3 = App(App(op,skc1),e4) // (op skc1 e4) +// val subt1 = App(App(op,e4),skc1) // (op e4 skc1) +// val t4 = App(App(op,subt1),t3) //(op (op e4 skc1) (op skc1 e4)) +// +// val t5 = App(App(op,e3),e3) //(op e3 e3) +// +// val eq1 = Eq(e3,t1) +// val eq2 = Eq(e4,skc1) +// val eq3 = Eq(e4,t2) +// val eq4 = Eq(t1,t3) +// val eq5 = Eq(e4,t4) +// val allEqs = List(eq1,eq2,eq3,eq4,eq5) +// +// println(allEqs) +// +// con = con.addAll(allEqs) // println(con.g) - -// println(dij(e1,e1,con.g)) - - println(path) -// println("transitivity chain:\n" + path.get.transChainProof.get) - println("BUILDING PROOF") - val x = path.get.toProof(eqRef).get - println("full proof:\n" + x) - } - case 6 => { - val op = new Var("op",Arrow(t,Arrow(t,t))) - val e3 = new Var("e3",t) - val e4 = new Var("e4",t) - val skc1 = new Var("skc1",t) - - val t1 = App(App(op,e4),e4) //(op e4 e4) - val t2 = App(App(op,e4),skc1) // (op e4 skc1) - - val eq1 = Eq(e3,t1) - val eq2 = Eq(e4,skc1) - val allEqs = List(eq1,eq2) - - con = con.addAll(allEqs) - con = con.addNode(t2) - val eqRef = con.eqReferences - val path = con.explain(e3,t2) - println(path.get.toString(false)) - println("transitivity chain:\n" + path.get.toProof(eqRef).get) - } - } - } -} \ No newline at end of file +//// con = con.resolveDeducedQueue +//// println("XXXXXXXXXXXXXXXXXX BEFORE ADDING") +// con = con.addNode(t5) +//// println("XXXXXXXXXXXXXXXXXX AFTER ADDING") +// val eqRef = con.eqReferences +// val path = con.explain(t5,t2) +// +//// println(path.get.toProof) +// +// val path2 = con.explain(e3,subt1) +// println(path2) +//// println(path2.get.toProof) +// +//// println(con.g) +// +//// println(dij(e1,e1,con.g)) +// +// println(path) +//// println("transitivity chain:\n" + path.get.transChainProof.get) +// println("BUILDING PROOF") +// val x = path.get.toProof(MMap[(E,E),App]() ++ eqRef).get +// println("full proof:\n" + x) +// } +// case 6 => { +// val op = new Var("op",Arrow(t,Arrow(t,t))) +// val e3 = new Var("e3",t) +// val e4 = new Var("e4",t) +// val skc1 = new Var("skc1",t) +// +// val t1 = App(App(op,e4),e4) //(op e4 e4) +// val t2 = App(App(op,e4),skc1) // (op e4 skc1) +// +// val eq1 = Eq(e3,t1) +// val eq2 = Eq(e4,skc1) +// val allEqs = List(eq1,eq2) +// +// con = con.addAll(allEqs) +// con = con.addNode(t2) +// val eqRef = con.eqReferences +// val path = con.explain(e3,t2) +// println(path.get.toString(false)) +// println("transitivity chain:\n" + path.get.toProof(MMap[(E,E),App]() ++ eqRef).get) +// } +// } +// } +//} \ 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 190c17c7..845eacae 100644 --- a/src/test/scala/at/logic/skeptik/congruence/EquationsExperiment.scala +++ b/src/test/scala/at/logic/skeptik/congruence/EquationsExperiment.scala @@ -8,6 +8,7 @@ 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 { @@ -79,7 +80,7 @@ object EquationsExperiment { val s = rightEqs.size val twoAndCongruent = if (s > 0) { - val con = new Congruence + val con = new Congruence(MMap[(E,E),App]()) leftEqs.foreach(eq => con.addEquality(eq)) con.resolveDeducedQueue rightEqs.exists(eq => { @@ -211,12 +212,12 @@ object EquationsExperiment { 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)({(A,B) => A.addEquality(B)}).resolveDeducedQueue + 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 + var con = new Congruence(MMap[(E,E),App]()) proof foldDown traverse