Optimization for && and || short-circuiting

src/main/scala/leon/solvers/templates/QuantificationManager.scala

@@ -442,22 +442,24 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
         val lambdaSubstMap = lambdas map (lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
         val substMap = subst.mapValues(Matcher.argValue) ++ baseSubstMap ++ lambdaSubstMap ++ instanceSubst(enablers)
 
-        instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
-          clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
-
-        val msubst = subst.collect { case (c, Right(m)) => c -> m }
-        val substituter = encoder.substitute(substMap)
-
-        for ((b,ms) <- allMatchers; m <- ms) {
-          val sb = enablers ++ (if (b == start) Set.empty else Set(substituter(b)))
-          val sm = m.substitute(substituter, matcherSubst = msubst)
-
-          if (matchers(m)) {
-            handled += sb -> sm
-          } else if (transMatchers(m) && isStrict) {
-            instantiation ++= instCtx.instantiate(sb, sm)(quantifications.toSeq : _*)
-          } else {
-            ignored += sb -> sm
+        if (!skip(substMap)) {
+          instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
+            clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
+
+          val msubst = subst.collect { case (c, Right(m)) => c -> m }
+          val substituter = encoder.substitute(substMap)
+
+          for ((b,ms) <- allMatchers; m <- ms) {
+            val sb = enablers ++ (if (b == start) Set.empty else Set(substituter(b)))
+            val sm = m.substitute(substituter, matcherSubst = msubst)
+
+            if (matchers(m)) {
+              handled += sb -> sm
+            } else if (transMatchers(m) && isStrict) {
+              instantiation ++= instCtx.instantiate(sb, sm)(quantifications.toSeq : _*)
+            } else {
+              ignored += sb -> sm
+            }
           }
         }
       }
@@ -466,6 +468,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
     }
 
     protected def instanceSubst(enablers: Set[T]): Map[T, T]
+
+    protected def skip(subst: Map[T, T]): Boolean = false
   }
 
   private class Quantification (
@@ -515,7 +519,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
       }
   }
 
-  private class Axiom (
+  private class LambdaAxiom (
     val start: T,
     val blocker: T,
     val guardVar: T,
@@ -536,6 +540,13 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
       val guardT = if (optEnabler.isDefined) encoder.mkAnd(start, optEnabler.get) else start
       Map(guardVar -> guardT, blocker -> newBlocker)
     }
+
+    override protected def skip(subst: Map[T, T]): Boolean = {
+      val substituter = encoder.substitute(subst)
+      allMatchers.forall { case (b, ms) =>
+        ms.forall(m => matchers(m) || instCtx(Set(substituter(b)) -> m.substitute(substituter)))
+      }
+    }
   }
 
   private def extractQuorums(
@@ -630,7 +641,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
     var instantiation = Instantiation.empty[T]
 
     for (matchers <- matchQuorums) {
-      val axiom = new Axiom(start, blocker, guardVar, quantified,
+      val axiom = new LambdaAxiom(start, blocker, guardVar, quantified,
         matchers, allMatchers, condVars, exprVars, condTree,
         clauses, blockers, applications, lambdas
       )

src/main/scala/leon/solvers/templates/TemplateGenerator.scala

@@ -311,10 +311,64 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
           }
 
         case a @ And(parts) =>
-          liftToIfExpr(pathVar, parts, andJoin, (a,b) => IfExpr(a, b, BooleanLiteral(false)))
+          val partitions = groupWhile(parts)(!requireDecomposition(_))
+          partitions.map(andJoin) match {
+            case Seq(e) => e
+            case seq =>
+              val newExpr : Identifier = FreshIdentifier("e", BooleanType, true)
+              storeExpr(newExpr)
+
+              def recAnd(pathVar: Identifier, partitions: Seq[Expr]): Unit = partitions match {
+                case x :: Nil if !requireDecomposition(x) =>
+                  storeGuarded(pathVar, Equals(Variable(newExpr), x))
+
+                case x :: xs =>
+                  val newBool : Identifier = FreshIdentifier("b", BooleanType, true)
+                  storeCond(pathVar, newBool)
+
+                  val xrec = rec(pathVar, x)
+                  storeGuarded(pathVar, Equals(Variable(newBool), xrec))
+                  storeGuarded(pathVar, Implies(Not(Variable(newBool)), Not(Variable(newExpr))))
+
+                  recAnd(newBool, xs)
+
+                case Nil =>
+                  storeGuarded(pathVar, Variable(newExpr))
+              }
+
+              recAnd(pathVar, seq)
+              Variable(newExpr)
+          }
 
         case o @ Or(parts) =>
-          liftToIfExpr(pathVar, parts, orJoin, (a,b) => IfExpr(a, BooleanLiteral(true), b))
+          val partitions = groupWhile(parts)(!requireDecomposition(_))
+          partitions.map(orJoin) match {
+            case Seq(e) => e
+            case seq =>
+              val newExpr : Identifier = FreshIdentifier("e", BooleanType, true)
+              storeExpr(newExpr)
+
+              def recOr(pathVar: Identifier, partitions: Seq[Expr]): Unit = partitions match {
+                case x :: Nil if !requireDecomposition(x) =>
+                  storeGuarded(pathVar, Equals(Variable(newExpr), x))
+
+                case x :: xs =>
+                  val newBool : Identifier = FreshIdentifier("b", BooleanType, true)
+                  storeCond(pathVar, newBool)
+
+                  val xrec = rec(pathVar, x)
+                  storeGuarded(pathVar, Equals(Not(Variable(newBool)), xrec))
+                  storeGuarded(pathVar, Implies(Not(Variable(newBool)), Variable(newExpr)))
+
+                  recOr(newBool, xs)
+
+                case Nil =>
+                  storeGuarded(pathVar, Not(Variable(newExpr)))
+              }
+
+              recOr(pathVar, seq)
+              Variable(newExpr)
+          }
 
         case i @ IfExpr(cond, thenn, elze) => {
           if(!requireDecomposition(i)) {

src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala

@@ -67,7 +67,7 @@ object PropositionalLogic {
   //   nnf(simplify(f)) == simplify(nnf(f))
   // }.holds
 
-  //@induct
+  @induct
   def simplifyBreaksNNF(f: Formula) : Boolean = {
     require(isNNF(f))
     isNNF(simplify(f))

src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala

@@ -66,11 +66,6 @@ class PureScalaValidSuiteCVC4 extends PureScalaValidSuite {
 }
 
 class PureScalaInvalidSuite extends PureScalaVerificationSuite {
-  override val ignored = Seq(
-    "verification/purescala/invalid/PropositionalLogic.scala",
-    "verification/purescala/invalid/InductiveQuantification.scala"
-  )
-
   override def testAll() = testInvalid()
   val optionVariants = opts
 }