Skip to content

Commit

Permalink
Fix bug in BottomUpSubsumption
Browse files Browse the repository at this point in the history
relates to Issue Paradoxika#77
  • Loading branch information
AFellner committed Aug 6, 2013
1 parent a147710 commit eccd727
Showing 1 changed file with 2 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -63,8 +63,8 @@ abstract class BottomUpSubsumption extends AbstractSubsumption {
val subsMap = subsumed.map(a => a._2)
subsMap.foreach(u => {
replaceNodes.get(u) match {
case Some(v) => if (v.conclusion.size > node.conclusion.size) replaceNodes(u) = node
case None => replaceNodes += (u -> node)
case Some(v) => if (v.conclusion.size > node.conclusion.size) replaceNodes(node) = u
case None => replaceNodes += (node -> u)
}})

node match {
Expand Down

2 comments on commit eccd727

@AFellner
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I found the dirty little bug.
The compression ratios for the first 9 diamond proofs are amazing:
Cumulative stats for BURLSt: 20.2%, 31.7%, 26.4%

I will try to compute more proofs on the cluster

@AFellner
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok I was happy a little too early. This change is not correct I think.

Please sign in to comment.