Implement ForwardAxiomSubsumption and move fixNodes to algorithm/comp…

…ressor/package.scala

Relates to Issues Paradoxika#79 and Paradoxika#76

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

@@ -9,15 +9,10 @@ import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent}
 import scala.collection.mutable.{HashMap => MMap}
 import scala.collection.mutable.{HashSet => MSet}
 
-object RecycleUnits extends (Proof[SequentProofNode] => Proof[SequentProofNode]) {
+object RecycleUnits extends (Proof[SequentProofNode] => Proof[SequentProofNode]) with fixNodes {
 
   def isUnit[P <: ProofNode[Sequent,P]](n: P) = n.conclusion.width == 1
 
-  def fixNode[P <: ProofNode[Sequent,P]](node: SequentProofNode, pivot: E, left: P, right: P, fixedLeft: SequentProofNode, fixedRight: SequentProofNode):SequentProofNode = {
-    if ((left eq fixedLeft) && (right eq fixedRight)) node 
-    else R(fixedLeft,fixedRight,pivot,true)
-  }
-
   def apply(proof: Proof[SequentProofNode]) = {
     //stores the unit descendend unit nodes of all proof nodes
     val descUnits = new MMap[SequentProofNode,MSet[SequentProofNode]]

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

@@ -1,6 +1,7 @@
 package at.logic.skeptik.algorithm.compressor
 
-import at.logic.skeptik.proof.Proof
+import at.logic.skeptik.expression.E
+import at.logic.skeptik.proof._
 import at.logic.skeptik.proof.sequent._
 import at.logic.skeptik.proof.sequent.lk._
 import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent}
@@ -10,7 +11,7 @@ import scala.collection.mutable.{HashSet => MSet}
 import scala.collection.immutable.{HashSet => ISet}
 
 abstract class AbstractSubsumption 
-extends (Proof[SequentProofNode] => Proof[SequentProofNode])
+extends (Proof[SequentProofNode] => Proof[SequentProofNode]) with fixNodes
 
 object TopDownLeftRightSubsumption extends AbstractSubsumption {
 
@@ -25,16 +26,12 @@ object TopDownLeftRightSubsumption extends AbstractSubsumption {
           node match {
             case Axiom(conclusion) => nodeMap += (conclusion -> node) ; node
             case R(left, right, pivot, _) => {
-  	          val fixedLeft  = fixedPremises.head
-              val fixedRight = fixedPremises.last
-              val newNode = 
-    		        if ((left eq fixedLeft) && (right eq fixedRight)) node 
-    		        else R(fixedLeft,fixedRight,pivot,true)
+  	          val newNode = fixNode(node,pivot,left,right,fixedPremises)
   		        nodeMap += (newNode.conclusion -> newNode)
   		        newNode
   	        }
-              case _ => node
-            }
+            case _ => node
+          }
         })
       })
     })
@@ -70,14 +67,7 @@ abstract class BottomUpRightLeftSubsumption extends AbstractSubsumption {
 
       replaceNodes.getOrElse(node,{
         node match {
-          case R(left, right, pivot, _) => {
-            val fixedLeft  = fixedPremises.head
-	        val fixedRight = fixedPremises.last
-	        val newNode = 
-	          if ((left eq fixedLeft) && (right eq fixedRight)) node 
-	          else R(fixedLeft,fixedRight,pivot,true)
-	          newNode
-          }
+          case R(left, right, pivot, _) => fixNode(node,pivot,left,right,fixedPremises)
           case _ => node
         }
       })
@@ -104,3 +94,18 @@ object BottomUpRightLeftSubsumptionMemory extends BottomUpRightLeftSubsumption {
     !(node existsAmongAncestors {_ eq ancestor})
   }
 }
+
+object ForwardAxiomSubsumption extends AbstractSubsumption {
+  def apply(proof: Proof[SequentProofNode]) = {
+    val axioms = MMap[Sequent,SequentProofNode]()
+    proof foldDown { (node: SequentProofNode, fixedPremises: Seq[SequentProofNode]) => node match {
+      case Axiom(conclusion) => {
+        val subsumed = axioms.find(A => A._1 subsequentOf conclusion)
+        val subsMap = subsumed.map(A => A._2)
+        subsMap.getOrElse({axioms += (conclusion -> node); node})
+      }
+      case R(left, right, pivot, _) => fixNode(node,pivot,left,right,fixedPremises)
+      case _ => node
+    }}
+  }
+}

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

@@ -1,6 +1,11 @@
 package at.logic.skeptik.algorithm
 
 import at.logic.skeptik.algorithm.compressor.split._
+import at.logic.skeptik.expression.E
+import at.logic.skeptik.proof.ProofNode
+import at.logic.skeptik.proof.sequent.SequentProofNode
+import at.logic.skeptik.judgment.Sequent
+import at.logic.skeptik.proof.sequent.lk.R
 
 // Algorithm names should contain only alphanumeric characters
 
@@ -30,6 +35,20 @@ package object compressor {
     "MSplit4" -> new TimeoutMultiSplit(4,5000),
     "TDLRS" -> TopDownLeftRightSubsumption,
     "BURLSt" -> BottomUpRightLeftSubsumptionTime,
-    "BURLSm" -> BottomUpRightLeftSubsumptionMemory
+    "BURLSm" -> BottomUpRightLeftSubsumptionMemory,
+    "FAS" -> ForwardAxiomSubsumption
   )
+  trait fixNodes {
+    def fixNode[P <: ProofNode[Sequent,P]](node: SequentProofNode, pivot: E, left: P, right: P, fixedLeft: SequentProofNode, fixedRight: SequentProofNode):SequentProofNode = {
+      if ((left eq fixedLeft) && (right eq fixedRight)) node 
+      else R(fixedLeft,fixedRight,pivot,true)
+    }
+      def fixNode[P <: ProofNode[Sequent,P]](node: SequentProofNode, pivot: E, left: P, right: P, fixedPremises: Seq[SequentProofNode]):SequentProofNode = {
+        val fixedLeft  = fixedPremises.head
+        val fixedRight = fixedPremises.last
+        fixNode(node,pivot,left,right,fixedLeft,fixedRight)
+    }
+  }
 }
+
+

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

@@ -50,11 +50,11 @@ class ForwardSubsumptionSpecification extends SpecificationWithJUnit {
 
     "Forward Subsumption" should {
       "compress the proof" in {
-        val compproof = FWS.apply(r6)
+        val compproof = TopDownLeftRightSubsumption.apply(r6)
         proof.size must beGreaterThan(compproof.size)
       }
       "conclude the empty clause" in {
-        val compproof = FWS.apply(r6)
+        val compproof = TopDownLeftRightSubsumption.apply(r6)
         compproof.root.conclusion.isEmpty must beTrue
       }
 	}