From 386e808c82509c939138c7ee3e68d8299a61521d Mon Sep 17 00:00:00 2001
From: SimonGuilloud <simon.guilloud@bluewin.ch>
Date: Tue, 18 Apr 2023 16:01:44 +0200
Subject: [PATCH 1/2] correct issue deep in OL Equivalence checker related to
quantifiers.
---
.../main/scala/lisa/kernel/fol/EquivalenceChecker.scala | 8 +-------
.../lisa/automation/kernel/OLPropositionalSolver.scala | 4 ++++
src/main/scala/lisa/mathematics/SetTheory.scala | 2 +-
3 files changed, 6 insertions(+), 8 deletions(-)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index 70bb9a28..adfeb547 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -108,12 +108,6 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
if (value) lessThanBitSet.update(otherIx + 1, true)
}
- // TODO: Check if needed
- override def equals(obj: Any): Boolean = obj match {
- case f: NormalFormula => eq(f)
- case _ => super.equals(obj)
- }
-
def recoverFormula: Formula = toFormulaAIG(this)
}
sealed abstract class NonTraversable extends NormalFormula
@@ -400,7 +394,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
case (NormalSchemConnector(id1, args1, polarity1), NormalSchemConnector(id2, args2, polarity2)) =>
id1 == id2 && polarity1 == polarity2 && args1.zip(args2).forall(f => latticesEQ(f._1, f._2))
case (NormalForall(x1, inner1, polarity1), NormalForall(x2, inner2, polarity2)) =>
- polarity1 == polarity2 && latticesLEQ(inner1, inner2)
+ polarity1 == polarity2 && (if (polarity1) latticesLEQ(inner1, inner2) else latticesLEQ(inner2, inner1))
case (_: NonTraversable, _: NonTraversable) => false
case (_, NormalAnd(children, true)) =>
diff --git a/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala b/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
index 886216f7..2bf8faeb 100644
--- a/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
+++ b/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
@@ -92,11 +92,15 @@ object OLPropositionalSolver {
// Transform a sequent into a format more adequate for solving
private def augmentSequent(s: Sequent): AugSequent = {
+ import lisa.utils.parsing.FOLPrinter.*
val f = reducedForm(sequentToFormula(s))
val atoms: scala.collection.mutable.Map[Formula, Int] = scala.collection.mutable.Map.empty
AugSequent((Nil, Nil), f)
}
+
+
+
def reduceSequent(s: Sequent): Formula = {
val p = simplify(sequentToFormula(s))
val nf = computeNormalForm(p)
diff --git a/src/main/scala/lisa/mathematics/SetTheory.scala b/src/main/scala/lisa/mathematics/SetTheory.scala
index 7f301e91..fc33f2dd 100644
--- a/src/main/scala/lisa/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/mathematics/SetTheory.scala
@@ -868,7 +868,7 @@ object SetTheory extends lisa.Main {
val exRed = thenHave(exists(b, in(b, x) /\ in(t, b)) |- exists(b, in(b, x))) by LeftExists
have(in(t, union(x)) |- exists(b, in(b, x))) by Cut(unionAx, exRed)
- thenHave(thesis) by Weakening
+ thenHave(thesis) by Tautology
}
val rhs = have(∀(b, in(b, x) ==> in(t, b)) /\ exists(b, in(b, x)) |- (in(t, union(x)) /\ ∀(b, in(b, x) ==> in(t, b)))) subproof {
--
GitLab
From d9f22e59ef42c0da0aef1c3ffe46770d8bfb5550 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <simon.guilloud@bluewin.ch>
Date: Tue, 18 Apr 2023 16:05:42 +0200
Subject: [PATCH 2/2] scalafix
---
.../scala/lisa/automation/kernel/OLPropositionalSolver.scala | 4 ----
1 file changed, 4 deletions(-)
diff --git a/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala b/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
index 2bf8faeb..886216f7 100644
--- a/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
+++ b/src/main/scala/lisa/automation/kernel/OLPropositionalSolver.scala
@@ -92,15 +92,11 @@ object OLPropositionalSolver {
// Transform a sequent into a format more adequate for solving
private def augmentSequent(s: Sequent): AugSequent = {
- import lisa.utils.parsing.FOLPrinter.*
val f = reducedForm(sequentToFormula(s))
val atoms: scala.collection.mutable.Map[Formula, Int] = scala.collection.mutable.Map.empty
AugSequent((Nil, Nil), f)
}
-
-
-
def reduceSequent(s: Sequent): Formula = {
val p = simplify(sequentToFormula(s))
val nf = computeNormalForm(p)
--
GitLab