Make ProofParserVeriT's resolution method invariant to clause permuta…

…tions

src/main/scala/at/logic/skeptik/algorithm/dijkstra/Dijkstra.scala

@@ -13,7 +13,7 @@ class EquationDijkstra extends Dijkstra[E,EqLabel] {
   }
 
   def setPi(u: E, l: EqLabel, v: E) = {
-    val eqTreeEdge = new EqTreeEdgeC(pi(v),l)
+    val eqTreeEdge = new EqTreeEdge(pi(v),l)
     val p = new EquationTree(u,Some(eqTreeEdge))
     pathTrees.update(u, p)
   }
@@ -54,7 +54,7 @@ abstract class Dijkstra[T1,T2] {
       val end = new EquationTree(sE,None)
       val x = Eq(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 EqTreeEdgeC(end,(x,None))
+      val eqTreeEdge = new EqTreeEdge(end,(x,None))
       new EquationTree(sE,Some(eqTreeEdge))
     }
     else {

src/main/scala/at/logic/skeptik/algorithm/dijkstra/PathTree.scala

@@ -8,12 +8,12 @@ import at.logic.skeptik.proof.sequent.lk._
 import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent}
 import scala.collection.immutable.{HashMap => IMap}
 
-class EqTreeEdgeC(val nextTree: EquationTree, val label: EqLabel) extends (EquationTree,(App,Option[(EquationTree,EquationTree)]))(nextTree,label) {
+class EqTreeEdge(val nextTree: EquationTree, val label: EqLabel) extends (EquationTree,(App,Option[(EquationTree,EquationTree)]))(nextTree,label) {
   val eq = label._1
   val deduceTrees = label._2
 }
 
-case class EquationTree(val v: E, val pred: Option[EqTreeEdgeC]) {
+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)) => {
@@ -23,7 +23,10 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdgeC]) {
 //      println("results in: " + x)
       x
     }
-    case Some((None,ded,_)) if !ded.isEmpty => Some(ded.last)
+    case Some((None,ded,_)) if !ded.isEmpty => {
+      if (ded.size > 1) println("more than one deduced with empty node")
+      Some(ded.last)
+    }
     case _ => None
   }
 
@@ -32,9 +35,9 @@ case class EquationTree(val v: E, val pred: Option[EqTreeEdgeC]) {
     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 res = 
       if (ddEqs.isEmpty) {
         val x = dd1.originalEqs.map(_.asInstanceOf[E]).toSeq ++: dd2.originalEqs.map(_.asInstanceOf[E]).toSeq

src/main/scala/at/logic/skeptik/algorithm/dijkstra/package.scala

@@ -4,6 +4,6 @@ package at.logic.skeptik.algorithm
 import at.logic.skeptik.expression._
 
 package object dijkstra {
-  type EqTreeEdge = Option[(EquationTree,(App,Option[(EquationTree,EquationTree)]))]
+//  type EqTreeEdge = Option[(EquationTree,(App,Option[(EquationTree,EquationTree)]))]
   type EqLabel = (App,Option[(EquationTree,EquationTree)])
 }

src/main/scala/at/logic/skeptik/parser/ProofParserVeriT.scala

@@ -1,7 +1,7 @@
 package at.logic.skeptik.parser
 
 import scala.util.parsing.combinator._
-import collection.mutable.{HashMap => MMap}
+import collection.mutable.{HashMap => MMap, HashSet => MSet}
 import java.io.FileReader
 import at.logic.skeptik.proof.Proof
 import at.logic.skeptik.proof.sequent.{SequentProofNode => Node}
@@ -40,8 +40,99 @@ extends JavaTokenParsers with RegexParsers {
 
   def inference: Parser[Node] = (resolution | axiom | unchecked)
   def resolution: Parser[Node] = "resolution" ~> premises <~ conclusion ^^ {
-    list => (list.head /: list.tail) { ((left, right) => R(left, right)) }
+    list => resolveClauses(list)
+//    list => {
+//      (list.head /: list.tail) { (left, right) => 
+//        try { 
+//          R(left, right)
+//        }
+//        catch {
+//        	case e: Exception => {
+//        	  
+//        	  throw(e)
+//        	}
+//        }
+//      }
+//    }
   }
+
+    /**
+   * Resolves the clauses represented by a list of indices in the correct order.
+   * 
+   * It does this by keeping track of in which clauses variables occur positively/negatively.
+   * This method only initializes these maps and calls the recursive method res with them.
+   */
+  def resolveClauses(clauses: List[Node]): Node = {
+    //map denoting that variable v occurs in {clause_1,...,clause_n} as a positive literl
+    val posOc = MMap[E,MSet[Node]]()
+    //respective negative version
+    val negOc = MMap[E,MSet[Node]]()
+    //initialize the maps
+    clauses.foreach(clause => {
+      clause.conclusion.suc.foreach(v => {
+//        println(v + " occurs positively in " + clause)
+        if (posOc.isDefinedAt(v)) posOc(v) += clause
+        else posOc += (v -> MSet[Node](clause))
+      })
+      clause.conclusion.ant.foreach(v => {
+//        println(v + " occurs negatively in " + clause)
+        if (negOc.isDefinedAt(v)) negOc(v) += clause
+        else negOc += (v -> MSet[Node](clause))
+      })
+    })
+//    println(clauseNumbers)
+//    println(posOc,negOc)
+    //start recursion
+    res(posOc,negOc)
+  }
+
+  /**
+   * Recursively resolves clauses, given two maps for positive/negative occurances of variables
+   * 
+   * For TraceCheck chains, the following invariant holds:
+   * At every point either 
+   * there exists a literal which occurs exactly once positively and once negatively
+   * or there is only one clause remaining
+   * 
+   * In the first case, this literal is used for resolving the respective clauses and updating the
+   * occurange maps
+   * In the other case, the one clause is returned 
+   * (either when no pivot is found or when the resolved clause is empty)
+   */
+  def res(posOc: MMap[E,MSet[Node]], negOc: MMap[E,MSet[Node]]):Node = {
+    val nextPivot = posOc.find(e => {
+      e._2.size == 1 &&
+      negOc.getOrElse(e._1, MSet[Node]()).size == 1
+    }).map(a => a._1)
+//    println(nextPivot)
+    nextPivot match {
+      //no more pivot means posOc and/or negOc can only contain 1 clause in the sets of occurances
+      case None => 
+        if (posOc.size > 0) posOc.last._2.last 
+        else negOc.last._2.last
+      case Some(p) => {
+        val posClause = posOc(p).last
+        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
+        })
+        newClause.conclusion.ant.foreach(v => {
+          negOc(v) -= posClause
+          negOc(v) -= negClause
+          negOc(v) += newClause
+        })
+        val newPOc = posOc - p
+        val newNegOc = negOc - p
+        if (newPOc.isEmpty && newNegOc.isEmpty) newClause
+        else res(newPOc,newNegOc)
+      }
+    }
+  }
+
+
   def axiom: Parser[Node] = "input" ~> conclusion ^^ {
     list => new Axiom(list)
   }