Some tweaks to Leon-era propositional logic benchmark (#1597)

* Some tweaks to propositional logic benchmark * More tweaks for termination
epfl-lara · Oct 28, 2024 · 60a2f19 · 60a2f19
1 parent 2024a36
commit 60a2f19
Showing 1 changed file with 59 additions and 40 deletions.
diff --git a/frontends/benchmarks/verification/valid/PropositionalLogic.scala b/frontends/benchmarks/verification/valid/PropositionalLogic.scala
@@ -1,66 +1,83 @@
-/* Copyright 2009-2021 EPFL, Lausanne */
+/* Copyright 2009-2024 EPFL, Lausanne */
 
-import stainless.lang._
-import stainless.annotation._
+import stainless.lang.*
+import stainless.annotation.*
 
-object PropositionalLogic { 
+object PropositionalLogic:
+
+  sealed abstract class Formula:
+    def size: BigInt = { // just to be clear what measure we are using
+      this match
+        case And(l, r)  => l.size + r.size + 1
+        case Or(l, r)   => l.size + r.size + 1
+        case Not(f)     => f.size + 1
+        case Implies(l, r) => l.size + r.size + 1
+        case Literal(_) => BigInt(1)
+    }.ensuring(res => res >= 1)
 
-  sealed abstract class Formula
   case class And(lhs: Formula, rhs: Formula) extends Formula
   case class Or(lhs: Formula, rhs: Formula) extends Formula
   case class Implies(lhs: Formula, rhs: Formula) extends Formula
   case class Not(f: Formula) extends Formula
   case class Literal(id: Int) extends Formula
 
-  def simplify(f: Formula): Formula = (f match {
-    case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
-    case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
-    case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
-    case Not(f) => Not(simplify(f))
-    case Literal(_) => f
-  }).ensuring(isSimplified(_))
+  def simplify(f: Formula): Formula = {
+    decreases(f.size)
+    f match 
+      case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+      case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
+      case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
+      case Not(f) => Not(simplify(f))
+      case Literal(_) => f
+  }.ensuring(isSimplified(_))
 
-  def isSimplified(f: Formula): Boolean = f match {
-    case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
-    case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
-    case Implies(_,_) => false
-    case Not(f) => isSimplified(f)
-    case Literal(_) => true
+  def isSimplified(f: Formula): Boolean = {
+    decreases(f.size)
+    f match 
+      case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+      case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+      case Implies(_,_) => false
+      case Not(f) => isSimplified(f)
+      case Literal(_) => true
   }
 
-  def nnf(formula: Formula): Formula = (formula match {
-    case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
-    case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
-    case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
-    case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
-    case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
-    case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
-    case Not(Not(f)) => nnf(f)
-    case Not(Literal(_)) => formula
-    case Literal(_) => formula
-  }).ensuring(isNNF(_))
+  def nnf(formula: Formula): Formula = {
+    require(isSimplified(formula))
+    decreases(formula.size)
+    formula match 
+      case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+      case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+      case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+      case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+      case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+      case Not(Not(f)) => nnf(f)
+      case Not(Literal(_)) => formula
+      case Literal(_) => formula
+  }.ensuring(isNNF(_))
 
-  def isNNF(f: Formula): Boolean = f match {
-    case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
-    case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
-    case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
-    case Not(Literal(_)) => true
-    case Not(_) => false
-    case Literal(_) => true
-  }
+  def isNNF(f: Formula): Boolean = {
+    decreases(f.size)
+    f match 
+      case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+      case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+      case Implies(lhs, rhs) => false
+      case Not(Literal(_)) => true
+      case Not(_) => false
+      case Literal(_) => true
+  }.ensuring(res => !res || isSimplified(f))
 
   def vars(f: Formula): Set[Int] = {
     require(isNNF(f))
+    decreases(f.size)
     f match {
       case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
       case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
-      case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
       case Not(Literal(i)) => Set[Int](i)
       case Literal(i) => Set[Int](i)
     }
   }
 
-  def fv(f : Formula) = { vars(nnf(f)) }
+  def fv(f : Formula) = { vars(nnf(simplify(f))) }
 
   @induct
   def nnfIsStable(f: Formula) : Boolean = {
@@ -73,4 +90,6 @@ object PropositionalLogic {
     require(isSimplified(f))
     simplify(f) == f
   }.holds
-}
+
+
+end PropositionalLogic