Safer transitiveCall*, implement isInductive check

src/main/scala/leon/purescala/Definitions.scala

@@ -51,8 +51,8 @@ object Definitions {
     def callees(f1: FunDef) = mainObject.callees(f1)
     def transitiveCallGraph = mainObject.transitiveCallGraph
     def transitivelyCalls(f1: FunDef, f2: FunDef) = mainObject.transitivelyCalls(f1, f2)
-    def transitiveCallers(f1: FunDef) = mainObject.transitiveCallers(f1)
-    def transitiveCallees(f1: FunDef) = mainObject.transitiveCallees(f1)
+    def transitiveCallers(f1: FunDef) = mainObject.transitiveCallers.getOrElse(f1, Set())
+    def transitiveCallees(f1: FunDef) = mainObject.transitiveCallees.getOrElse(f1, Set())
     def isRecursive(f1: FunDef) = mainObject.isRecursive(f1)
     def isCatamorphism(f1: FunDef) = mainObject.isCatamorphism(f1)
     def caseClassDef(name: String) = mainObject.caseClassDef(name)

src/main/scala/leon/purescala/TreeOps.scala

@@ -681,22 +681,36 @@ object TreeOps {
     toRet
   }
 
-  def conditionForPattern(in: Expr, pattern: Pattern) : Expr = pattern match {
-    case WildcardPattern(_) => BooleanLiteral(true)
-    case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
-    case CaseClassPattern(_, ccd, subps) => {
-      assert(ccd.fields.size == subps.size)
-      val pairs = ccd.fields.map(_.id).toList zip subps.toList
-      val subTests = pairs.map(p => conditionForPattern(CaseClassSelector(ccd, in, p._1), p._2))
-      val together = And(subTests)
-      And(CaseClassInstanceOf(ccd, in), together)
+  def conditionForPattern(in: Expr, pattern: Pattern, includeBinders: Boolean = false) : Expr = {
+    def bind(ob: Option[Identifier], to: Expr): Expr = {
+      if (!includeBinders) {
+        BooleanLiteral(true)
+      } else {
+        ob.map(id => Equals(Variable(id), to)).getOrElse(BooleanLiteral(true))
+      }
     }
-    case TuplePattern(_, subps) => {
-      val TupleType(tpes) = in.getType
-      assert(tpes.size == subps.size)
-      val subTests = subps.zipWithIndex.map{case (p, i) => conditionForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
-      And(subTests)
+
+    def rec(in: Expr, pattern: Pattern): Expr = {
+      pattern match {
+        case WildcardPattern(ob) => bind(ob, in)
+        case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
+        case CaseClassPattern(ob, ccd, subps) => {
+          assert(ccd.fields.size == subps.size)
+          val pairs = ccd.fields.map(_.id).toList zip subps.toList
+          val subTests = pairs.map(p => rec(CaseClassSelector(ccd, in, p._1), p._2))
+          val together = And(bind(ob, in) +: subTests)
+          And(CaseClassInstanceOf(ccd, in), together)
+        }
+        case TuplePattern(ob, subps) => {
+          val TupleType(tpes) = in.getType
+          assert(tpes.size == subps.size)
+          val subTests = subps.zipWithIndex.map{case (p, i) => rec(TupleSelect(in, i+1).setType(tpes(i)), p)}
+          And(bind(ob, in) +: subTests)
+        }
+      }
     }
+
+    rec(in, pattern)
   }
 
   private def convertMatchToIfThenElse(expr: Expr) : Expr = {
@@ -734,7 +748,7 @@ object TreeOps {
 
         val condsAndRhs = for(cse <- cases) yield {
           val map = mapForPattern(scrut, cse.pattern)
-          val patCond = conditionForPattern(scrut, cse.pattern)
+          val patCond = conditionForPattern(scrut, cse.pattern, includeBinders = false)
           val realCond = cse.theGuard match {
             case Some(g) => And(patCond, replaceFromIDs(map, g))
             case None => patCond
@@ -1204,7 +1218,7 @@ object TreeOps {
         var soFar = path
 
         MatchExpr(rs, cases.map { c =>
-          val patternExpr = conditionForPattern(rs, c.pattern)
+          val patternExpr = conditionForPattern(rs, c.pattern, includeBinders = true)
 
           val subPath = register(patternExpr, soFar)
           soFar = register(Not(patternExpr), soFar)
@@ -1326,7 +1340,7 @@ object TreeOps {
           e
         } else {
           MatchExpr(rs, cases.flatMap { c =>
-            val patternExpr = conditionForPattern(rs, c.pattern)
+            val patternExpr = conditionForPattern(rs, c.pattern, includeBinders = true)
 
             if (stillPossible && !contradictedBy(patternExpr, path)) {
 
@@ -1745,4 +1759,36 @@ object TreeOps {
     case e => (None, e)
   }
 
+  def isInductiveOn(solver: Solver)(expr: Expr, on: Identifier): Boolean = on match {
+    case IsTyped(origId, AbstractClassType(cd)) =>
+      def isAlternativeRecursive(cd: CaseClassDef): Boolean = {
+        cd.fieldsIds.exists(_.getType == origId.getType)
+      }
+
+      val toCheck = cd.knownDescendents.collect {
+        case ccd: CaseClassDef =>
+          val isType = CaseClassInstanceOf(ccd, Variable(on))
+
+            val recSelectors = ccd.fieldsIds.filter(_.getType == on.getType)
+
+            if (recSelectors.isEmpty) {
+              None
+            } else {
+              val v = Variable(on)
+              Some(And(And(isType, expr), Not(replace(recSelectors.map(s => v -> CaseClassSelector(ccd, v, s)).toMap, expr))))
+            }
+      }.flatten
+
+      toCheck.forall { cond =>
+        solver.solveSAT(cond) match {
+            case (Some(false), _)  =>
+              true
+            case (_, model)  =>
+              false
+        }
+      }
+    case _ =>
+      false
+  }
+
 }

src/main/scala/leon/purescala/Trees.scala

@@ -466,7 +466,10 @@ object Trees {
   }
 
   /* Set expressions */
-  case class FiniteSet(elements: Seq[Expr]) extends Expr 
+  case class FiniteSet(elements: Seq[Expr]) extends Expr {
+    val tpe = if (elements.isEmpty) None else leastUpperBound(elements.map(_.getType))
+    tpe.foreach(t => setType(SetType(t)))
+  }
   // TODO : Figure out what evaluation order is, for this.
   // Perhaps then rewrite as "contains".
   case class ElementOfSet(element: Expr, set: Expr) extends Expr with FixedType {