Fixed some data-type unrolling issues

src/main/scala/leon/solvers/combinators/UnrollingSolver.scala

@@ -268,6 +268,10 @@ trait AbstractUnrollingSolver[T]
   private def getTotalModel: Model = {
     val wrapped = solverGetModel
 
+    templateGenerator.manager.quantifications.map { q =>
+      q.holds
+    }
+
     val typeInsts = templateGenerator.manager.typeInstantiations
     val partialInsts = templateGenerator.manager.partialInstantiations
 

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

@@ -200,7 +200,7 @@ class DatatypeManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(en
       andJoin(inv ++ subtype :+ induct)
 
     case TupleType(tpes) =>
-      andJoin(tpes.zipWithIndex.map(p => typeUnroller(TupleSelect(expr, p._2))))
+      andJoin(tpes.zipWithIndex.map(p => typeUnroller(TupleSelect(expr, p._2 + 1))))
 
     case FunctionType(_, _) =>
       FreshFunction(expr)

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

@@ -211,7 +211,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
 
   def registerFunction(b: T, tpe: FunctionType, f: T): Seq[T] = {
     val ft = bestRealType(tpe).asInstanceOf[FunctionType]
-    val bs = fixpoint((bs: Set[T]) => bs.flatMap(blockerParents))(Set(b))
+    val bs = fixpoint((bs: Set[T]) => bs ++ bs.flatMap(blockerParents))(Set(b))
 
     val (known, neqClauses) = if ((bs intersect typeEnablers).nonEmpty) {
       maybeFree += ft -> (maybeFree(ft) + (b -> f))
@@ -262,10 +262,10 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
         val nextB  = encoder.encodeId(FreshIdentifier("b_or", BooleanType, true))
         freeBlockers += tpe -> (freeBlockers(tpe) + (nextB -> caller))
 
-        val clause = encoder.mkEquals(firstB, encoder.mkOr(
+        val clause = encoder.mkEquals(firstB, encoder.mkAnd(blocker, encoder.mkOr(
           knownFree(tpe).map(idT => encoder.mkEquals(caller, idT)).toSeq ++
           maybeFree(tpe).map { case (b, idT) => encoder.mkAnd(b, encoder.mkEquals(caller, idT)) } :+
-          nextB : _*))
+          nextB : _*)))
         (firstB, Seq(clause))
       }
 

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

@@ -132,7 +132,8 @@ object QuantificationTemplate {
 }
 
 class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManager[T](encoder) {
-  private val quantifications = new IncrementalSeq[MatcherQuantification]
+  private[solvers] val quantifications = new IncrementalSeq[MatcherQuantification]
+
   private val instCtx         = new InstantiationContext
 
   private val ignoredMatchers = new IncrementalSeq[(Int, Set[T], Matcher[T])]
@@ -344,7 +345,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
     }
   }
 
-  private trait MatcherQuantification {
+  private[solvers] trait MatcherQuantification {
+    val holds: T
     val pathVar: (Identifier, T)
     val quantifiers: Seq[(Identifier, T)]
     val matchers: Set[Matcher[T]]
@@ -472,10 +474,9 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
         Instantiation.empty[T]
       } else {
         handledSubsts(this) += enablers -> subst
-        val allEnablers = fixpoint((enablers: Set[T]) => enablers.flatMap(blockerParents))(enablers)
 
         var instantiation = Instantiation.empty[T]
-        val (enabler, optEnabler) = freshBlocker(allEnablers)
+        val (enabler, optEnabler) = freshBlocker(enablers)
         if (optEnabler.isDefined) {
           instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
         }
@@ -539,6 +540,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
     val lambdas: Seq[LambdaTemplate[T]]) extends MatcherQuantification {
 
     var currentQ2Var: T = qs._2
+    val holds = qs._2
 
     protected def instanceSubst(enabler: T): Map[T, T] = {
       val nextQ2Var = encoder.encodeId(q2s._1)
@@ -590,6 +592,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
     val applications: Map[T, Set[App[T]]],
     val lambdas: Seq[LambdaTemplate[T]]) extends MatcherQuantification {
 
+    val holds = start
+
     protected def instanceSubst(enabler: T): Map[T, T] = {
       Map(guardVar -> start, blocker -> enabler)
     }

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

@@ -294,7 +294,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
           // we need to define this defBlocker and link it to definition
           val defBlocker = encoder.encodeId(FreshIdentifier("d", BooleanType))
           defBlockers += info -> defBlocker
-          manager.implies(id, defBlocker)
 
           val template = templateGenerator.mkTemplate(tfd)
           //reporter.debug(template)
@@ -348,7 +347,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
         case None =>
           val lambdaBlocker = encoder.encodeId(FreshIdentifier("d", BooleanType))
           lambdaBlockers += info -> lambdaBlocker
-          manager.implies(b, lambdaBlocker)
 
           val (newExprs, callBlocks, appBlocks) = template.instantiate(lambdaBlocker, args)
           val blockExprs = freshAppBlocks(appBlocks.keys)

testcases/verification/math/RationalProps.scala

@@ -7,63 +7,57 @@ import scala.language.postfixOps
 object RationalProps {
 
   def squarePos(r: Rational): Rational = {
-    require(r.isRational)
     r * r
   } ensuring(_ >= Rational(0))
 
   def additionIsCommutative(p: Rational, q: Rational): Boolean = {
-    require(p.isRational && q.isRational)
     p + q == q + p
   } holds
 
   def multiplicationIsCommutative(p: Rational, q: Rational): Boolean = {
-    require(p.isRational && q.isRational)
     p * q == q * p
   } holds
 
   def lessThanIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
-    require(p.isRational && q.isRational && r.isRational && p < q && q < r)
+    require(p < q && q < r)
     p < r
   } holds
 
   def lessEqualsIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
-    require(p.isRational && q.isRational && r.isRational && p <= q && q <= r)
+    require(p <= q && q <= r)
     p <= r
   } holds
 
   def greaterThanIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
-    require(p.isRational && q.isRational && r.isRational && p > q && q > r)
+    require(p > q && q > r)
     p > r
   } holds
 
   def greaterEqualsIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
-    require(p.isRational && q.isRational && r.isRational && p >= q && q >= r)
+    require(p >= q && q >= r)
     p >= r
   } holds
 
   def distributionMult(p: Rational, q: Rational, r: Rational): Boolean = {
-    require(p.isRational && q.isRational && r.isRational)
     (p*(q + r)) ~ (p*q + p*r)
   } holds
 
   def reciprocalIsCorrect(p: Rational): Boolean = {
-    require(p.isRational && p.nonZero)
+    require(p.nonZero)
     (p * p.reciprocal) ~ Rational(1)
   } holds
 
   def additiveInverseIsCorrect(p: Rational): Boolean = {
-    require(p.isRational)
     (p + (-p)) ~ Rational(0)
   } holds
 
   //should not hold because q could be 0
   def divByZero(p: Rational, q: Rational): Boolean = {
-    require(p.isRational && q.isRational)
     ((p / q) * q) ~ p
   } holds
 
   def divByNonZero(p: Rational, q: Rational): Boolean = {
-    require(p.isRational && q.isRational && q.nonZero)
+    require(q.nonZero)
     ((p / q) * q) ~ p
   } holds
   
@@ -73,17 +67,16 @@ object RationalProps {
    */
 
   def equivalentIsReflexive(p: Rational): Boolean = {
-    require(p.isRational)
     p ~ p
   } holds
 
   def equivalentIsSymmetric(p: Rational, q: Rational): Boolean = {
-    require(p.isRational && q.isRational && p ~ q)
+    require(p ~ q)
     q ~ p
   } holds
 
   def equivalentIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
-    require(p.isRational && q.isRational && r.isRational && p ~ q && q ~ r)
+    require(p ~ q && q ~ r)
     p ~ r
   } holds
 }