Experimental integration of OL- and OCBSL- based simplifiers

core/src/main/scala/stainless/MainHelpers.scala

@@ -53,6 +53,13 @@ trait MainHelpers extends inox.MainHelpers { self =>
       s"Check arithmetic operations for unintended behavior and overflows (default: true)"),
     verification.optTypeChecker -> Description(Verification, "Use the type-checking rules from the calculus to generate verification conditions"),
     verification.optAdmitVCs -> Description(Verification, "Admit all verification conditions"),
+    verification.optSimplifier -> Description(Verification, "Select which simplifier to use for VC simplification\n" +
+      "Available:\n" +
+      "  vanilla:             : Standard simplifier\n" +
+      "  ol (experimental)    : Leverages ortholattice boolean algebra for simplifying boolean expressions\n" +
+      "  ocbsl (experimental) : Leverages orthocomplemented bisemilattices boolean algebra for simplifying boolean expressions.\n" +
+      "                         Though the name sounds cooler than OL, it is less complete.\n" +
+      "  bland (experimental) : Common simplification logic to OL and OCBSL, but without any boolean algebra flavor"),
     termination.optCheckMeasures -> Description(Termination, "Check that measures are valid (both inferred and user-defined)"),
     termination.optInferMeasures -> Description(Termination, "Automatically infer measures for recursive functions"),
     inox.optTimeout -> Description(General, "Set a timeout n (in sec) such that\n" +

core/src/main/scala/stainless/Report.scala

@@ -123,7 +123,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
       f"valid: ${stats.valid}%-4d (${stats.validFromCache} from cache) " +
       f"invalid: ${stats.invalid}%-4d " +
       f"unknown: ${stats.unknown}%-4d " +
-      f"time: ${stats.time/1000d}%7.1f"
+      f"time: ${stats.time/1000d}%7.2f"
 
     var t = Table(withColor(s"$name summary", color))
     t ++= rows

core/src/main/scala/stainless/extraction/xlang/PartialFunctions.scala

@@ -85,7 +85,7 @@ class PartialFunctions(override val s: Trees)(override val t: s.type)
               "unapply syntactic sugar for partial function creation.")
         }
 
-        ClassConstructor(ct, Seq(pre, body)).setPos(fi)
+        ClassConstructor(ct, Seq(exprOps.freshenLocals(pre), body)).setPos(fi)
 
       case other => other
     }

core/src/main/scala/stainless/transformers/LatticesSimplifier.scala

@@ -0,0 +1,49 @@
+package stainless
+package transformers
+
+import inox.solvers
+
+import java.util.concurrent.atomic.AtomicInteger
+
+// Wrapper that sets up a thread-local algo instance
+trait LatticesSimplifier { self =>
+  import LatticesSimplifier._
+  val trees: ast.Trees
+  val symbols: trees.Symbols
+  val opts: solvers.PurityOptions
+  val algo: UnderlyingAlgo
+
+  import trees._
+  import symbols.{given, _}
+
+  private val coreTL: ThreadLocal[lattices.Core{val trees: self.trees.type; val symbols: self.symbols.type}] =
+    ThreadLocal.withInitial(() => algo match {
+      case UnderlyingAlgo.OCBSL => lattices.OCBSL(trees, symbols, opts)
+      case UnderlyingAlgo.OL => lattices.OL(trees, symbols, opts)
+      case UnderlyingAlgo.Bland => lattices.Bland(trees, symbols, opts)
+    })
+
+  def simplify(e: Expr): Expr = {
+    val core = coreTL.get()
+    given core.Env = core.Env.empty
+    given core.Ctxs = core.Ctxs.empty
+    given core.LetValSubst = core.LetValSubst.empty
+
+    val resE = core.codeOfExpr(e)
+    val codeE = resE.selfPlugged(core.Ctxs.empty)._2
+    core.uncodeOf(codeE).expr.copiedFrom(e)
+  }
+}
+object LatticesSimplifier {
+
+  enum UnderlyingAlgo {
+    case OCBSL
+    case OL
+    case Bland
+  }
+
+  def apply(t: ast.Trees, s: t.Symbols, opts: solvers.PurityOptions, algo: UnderlyingAlgo): LatticesSimplifier{val trees: t.type; val symbols: s.type} = {
+    class Impl(override val trees: t.type, override val symbols: s.type, override val opts: solvers.PurityOptions, override val algo: UnderlyingAlgo) extends LatticesSimplifier
+    new Impl(t, s, opts, algo)
+  }
+}

core/src/main/scala/stainless/transformers/lattices/Bland.scala

@@ -0,0 +1,25 @@
+package stainless
+package transformers
+package lattices
+
+import inox.solvers
+
+trait Bland extends Core {
+  import trees._
+  import symbols.{given, _}
+  import Opaques.{given, _}
+  import Purity._
+
+  override final def impliedImpl(rhs: Code)(using env: Env, ctxs: Ctxs): Boolean = false
+
+  override final def doSimplifyDisjunction(disjs: Seq[Code], polarity: Boolean)(using Env, Ctxs): Seq[Code] = disjs
+
+  override final def checkForDisjunctionContradiction(disjs0: Seq[Code])(using Env, Ctxs): Option[Int] = None
+}
+
+object Bland {
+  def apply(t: ast.Trees, s: t.Symbols, opts: solvers.PurityOptions): Bland{val trees: t.type; val symbols: s.type} = {
+    class Impl(override val trees: t.type, override val symbols: s.type, override val opts: solvers.PurityOptions) extends Bland
+    new Impl(t, s, opts)
+  }
+}