From 0bf3da198823a72c858700e95f4ecc8a2a620dd4 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Wed, 18 May 2022 19:29:12 +0200
Subject: [PATCH] Corrected a bug in the equivalence checker. Due to small
optimisations, part of checkForContradiction was reversing a list at one
point, and expecting it not reverse at some other point. This made the check
non-sufficient.
---
src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index d652b045..79addcff 100644
--- a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -135,7 +135,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
})
*/
def checkForContradiction(children:List[(NormalFormula, Int)]): Boolean = {
- val (negatives_temp, positives) = children.foldLeft[(List[NormalFormula], List[NormalFormula])]((Nil, Nil))(
+ val (negatives_temp, positives_temp) = children.foldLeft[(List[NormalFormula], List[NormalFormula])]((Nil, Nil))(
(acc, ch) => acc match {
case (negatives, positives) => ch._1 match {
case NNeg(child, c) =>(child::negatives, positives)
@@ -143,7 +143,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
}
}
)
- val negatives = negatives_temp.sortBy(_.code)
+ val (negatives, positives) = (negatives_temp.sortBy(_.code), positives_temp.reverse)
var i, j = 0
while (i<positives.size && j<negatives.size){ //checks if there is a positive and negative nodes with same code.
val (c1, c2) = (positives(i).code, negatives(j).code)
--
GitLab