Implement possibility to change traversal order when creating a proof…

… from root node and implement corresponding versions of Subsumption algorithms

project/Build.scala

@@ -31,7 +31,7 @@ object SkeptikBuild extends Build {
   val compress = InputKey[Unit]("compress", "bla")
   val compressSettings = Seq(fullRunInputTask(compress,Runtime,"at.logic.skeptik.ProofCompressionCLI"),
                              trapExit in compress := true ,
-                             fork in compress := true, 
+                             fork in compress := false, 
                              traceLevel in compress := 0)
 
 

src/main/scala/at/logic/skeptik/algorithm/compressor/Subsumption.scala

@@ -11,11 +11,21 @@ import scala.collection.mutable.{HashSet => MSet}
 import scala.collection.immutable.{HashSet => ISet}
 
 abstract class AbstractSubsumption 
-extends (Proof[SequentProofNode] => Proof[SequentProofNode]) with fixNodes
+extends (Proof[SequentProofNode] => Proof[SequentProofNode]) with fixNodes {
+  def setTraverseOrder(proof: Proof[SequentProofNode]):Proof[SequentProofNode]
+}
 
-object TopDownLeftRightSubsumption extends AbstractSubsumption {
+trait LeftRight {
+  def setTraverseOrder(proof: Proof[SequentProofNode]):Proof[SequentProofNode] = proof
+}
+trait RightLeft {
+  def setTraverseOrder(proof: Proof[SequentProofNode]):Proof[SequentProofNode] = new Proof(proof.root,false)
+}
+
+abstract class TopDownSubsumption extends AbstractSubsumption {
 
-  def apply(proof: Proof[SequentProofNode]) = {
+  def apply(inputproof: Proof[SequentProofNode]) = {
+    val proof = setTraverseOrder(inputproof)
     val nodeMap = new MMap[Sequent,SequentProofNode]
 
     Proof(proof foldDown { ((node: SequentProofNode, fixedPremises: Seq[SequentProofNode]) => {
@@ -38,7 +48,11 @@ object TopDownLeftRightSubsumption extends AbstractSubsumption {
   }
 }
 
-abstract class BottomUpRightLeftSubsumption extends AbstractSubsumption {
+object TopDownLeftRightSubsumption extends TopDownSubsumption with LeftRight
+
+object TopDownRightLeftSubsumption extends TopDownSubsumption with RightLeft
+
+abstract class BottomUpSubsumption extends AbstractSubsumption {
   val nodeMap = new MMap[Sequent,SequentProofNode]
   val replaceNodes = new MMap[SequentProofNode,SequentProofNode]
 
@@ -60,7 +74,8 @@ abstract class BottomUpRightLeftSubsumption extends AbstractSubsumption {
     }
   }
 
-  def apply(proof: Proof[SequentProofNode]) = {
+  def apply(inputproof: Proof[SequentProofNode]) = {
+    val proof = setTraverseOrder(inputproof)
     proof.foldDown(collect)
 
     Proof(proof foldDown { ((node: SequentProofNode, fixedPremises: Seq[SequentProofNode]) => {
@@ -75,7 +90,7 @@ abstract class BottomUpRightLeftSubsumption extends AbstractSubsumption {
   }
 }
 
-object BottomUpRightLeftSubsumptionTime extends BottomUpRightLeftSubsumption {
+abstract class BottomUpSubsumptionTime extends BottomUpSubsumption {
   val ancestors = new MMap[SequentProofNode,ISet[SequentProofNode]]
   def notAncestor(node: SequentProofNode, ancestor: SequentProofNode):Boolean = {
     !(ancestors.getOrElseUpdate(node, computeAncestors(node)) contains ancestor)
@@ -89,14 +104,21 @@ object BottomUpRightLeftSubsumptionTime extends BottomUpRightLeftSubsumption {
   }
 }
 
-object BottomUpRightLeftSubsumptionMemory extends BottomUpRightLeftSubsumption {
+object BottomUpLeftRightSubsumptionTime extends BottomUpSubsumptionTime with LeftRight
+object BottomUpRightLeftSubsumptionTime extends BottomUpSubsumptionTime with RightLeft
+
+abstract class BottomUpSubsumptionMemory extends BottomUpSubsumption {
   def notAncestor(node: SequentProofNode, ancestor: SequentProofNode):Boolean = {
     !(node existsAmongAncestors {_ eq ancestor})
   }
 }
 
-object ForwardAxiomSubsumption extends AbstractSubsumption {
-  def apply(proof: Proof[SequentProofNode]) = {
+object BottomUpLeftRightSubsumptionMemory extends BottomUpSubsumptionMemory with LeftRight
+object BottomUpRightLeftSubsumptionMemory extends BottomUpSubsumptionMemory with RightLeft
+
+abstract class AxiomSubsumption extends AbstractSubsumption {
+  def apply(inputproof: Proof[SequentProofNode]) = {
+    val proof = setTraverseOrder(inputproof)
     val axioms = MMap[Sequent,SequentProofNode]()
     proof foldDown { (node: SequentProofNode, fixedPremises: Seq[SequentProofNode]) => node match {
       case Axiom(conclusion) => {
@@ -108,4 +130,7 @@ object ForwardAxiomSubsumption extends AbstractSubsumption {
       case _ => node
     }}
   }
-}
+}
+
+object LeftRightAxiomSubsumption extends AxiomSubsumption with LeftRight
+object RightLeftAxiomSubsumption extends AxiomSubsumption with RightLeft

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

@@ -34,9 +34,12 @@ package object compressor {
     "MSplit3" -> new TimeoutMultiSplit(3,5000),
     "MSplit4" -> new TimeoutMultiSplit(4,5000),
     "TDLRS" -> TopDownLeftRightSubsumption,
+    "TDRLS" -> TopDownRightLeftSubsumption,
+    "TDLRS" -> TopDownLeftRightSubsumption,
     "BURLSt" -> BottomUpRightLeftSubsumptionTime,
     "BURLSm" -> BottomUpRightLeftSubsumptionMemory,
-    "FAS" -> ForwardAxiomSubsumption
+    "LRAS" -> LeftRightAxiomSubsumption,
+    "RLAS" -> RightLeftAxiomSubsumption
   )
   trait fixNodes {
     def fixNode[P <: ProofNode[Sequent,P]](node: SequentProofNode, pivot: E, left: P, right: P, fixedLeft: SequentProofNode, fixedRight: SequentProofNode):SequentProofNode = {

src/main/scala/at/logic/skeptik/proof/Proof.scala

@@ -9,16 +9,19 @@ import at.logic.skeptik.judgment.Judgment
 
 // ProofNode tree is rotated clockwise. That means that traversing "left" is bottom-up.
 // Traversing "right" is top-down and we ensure that premises of a proof are processed before that proof.
-class Proof[P <: ProofNode[Judgment,P]](val root: P)
+class Proof[P <: ProofNode[Judgment,P]](val root: P, val leftRight: Boolean)
 extends Iterable[P]
 {
+  def this(root: P) = this(root,true)
+
   def initialize() = {
     val nodes = Stack[P]()
     val children = MMap[P,IndexedSeq[P]](root -> IndexedSeq())
     val visited = MSet[P]()
     def visit(p:P):Unit = if (!visited(p)){
       visited += p
-      p.premises.foreach(premise => {
+      val pr = if (leftRight) p.premises else p.premises.reverse
+      pr.foreach(premise => {
         visit(premise)
         children(premise) = p +: children.getOrElse(premise,IndexedSeq())
       })

src/test/scala/at/logic/skeptik/algorithm/compressor/BackwardSubsumption.scala

@@ -129,7 +129,7 @@ class BackwardSubsumptionSpecification extends SpecificationWithJUnit {
 //    
 //    proof bottomUp(visit)
 //  println(proof)
-   val compproof = BWSm.apply(concseq)
+   val compproof = BottomUpRightLeftSubsumptionMemory(concseq)
 // println(compproof)
 
   "Backward Subsumption" should {