Skip to content

Commit

Permalink
Rename Subsumption algorithms
Browse files Browse the repository at this point in the history
  • Loading branch information
AFellner committed Aug 5, 2013
1 parent 6fb9ce6 commit 1daa054
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import scala.collection.immutable.{HashSet => ISet}
abstract class AbstractSubsumption
extends (Proof[SequentProofNode] => Proof[SequentProofNode])

object FWS extends AbstractSubsumption {
object TopDownLeftRightSubsumption extends AbstractSubsumption {

def apply(proof: Proof[SequentProofNode]) = {
val nodeMap = new MMap[Sequent,SequentProofNode]
Expand Down Expand Up @@ -41,7 +41,7 @@ object FWS extends AbstractSubsumption {
}
}

abstract class BWS extends AbstractSubsumption {
abstract class BottomUpRightLeftSubsumption extends AbstractSubsumption {
val nodeMap = new MMap[Sequent,SequentProofNode]
val replaceNodes = new MMap[SequentProofNode,SequentProofNode]

Expand All @@ -58,7 +58,7 @@ abstract class BWS extends AbstractSubsumption {

node match {
case Axiom(conclusion) => nodeMap += (conclusion -> node)
case R(_,_,_,_) => nodeMap += (node.conclusion -> node)
case R(_, _, _, _) => nodeMap += (node.conclusion -> node)
case _ => Unit
}
}
Expand All @@ -85,7 +85,7 @@ abstract class BWS extends AbstractSubsumption {
}
}

object BWSt extends BWS {
object BottomUpRightLeftSubsumptionTime extends BottomUpRightLeftSubsumption {
val ancestors = new MMap[SequentProofNode,ISet[SequentProofNode]]
def notAncestor(node: SequentProofNode, ancestor: SequentProofNode):Boolean = {
!(ancestors.getOrElseUpdate(node, computeAncestors(node)) contains ancestor)
Expand All @@ -99,7 +99,7 @@ object BWSt extends BWS {
}
}

object BWSm extends BWS {
object BottomUpRightLeftSubsumptionMemory extends BottomUpRightLeftSubsumption {
def notAncestor(node: SequentProofNode, ancestor: SequentProofNode):Boolean = {
!(node existsAmongAncestors {_ eq ancestor})
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ package object compressor {
"MSplit2" -> new TimeoutMultiSplit(2,5000),
"MSplit3" -> new TimeoutMultiSplit(3,5000),
"MSplit4" -> new TimeoutMultiSplit(4,5000),
"FWS" -> FWS,
"BWSt" -> BWSt,
"BWSm" -> BWSm
"TDLRS" -> TopDownLeftRightSubsumption,
"BURLSt" -> BottomUpRightLeftSubsumptionTime,
"BURLSm" -> BottomUpRightLeftSubsumptionMemory
)
}

0 comments on commit 1daa054

Please sign in to comment.