SMTLIB-CVC4 with define-funs-rec

src/main/scala/leon/purescala/DefOps.scala

@@ -2,6 +2,7 @@ package leon.purescala
 
 import Definitions._
 import Expressions._
+import ExprOps.{preMap, postMap, functionCallsOf}
 
 object DefOps {
 
@@ -262,11 +263,7 @@ object DefOps {
     
   }
   
-  
-  
-  import Expressions.Expr
-  import ExprOps.{preMap, postMap}
-  
+
   /*
    * Apply an expression operation on all expressions contained in a FunDef
    */
@@ -385,4 +382,21 @@ object DefOps {
     }(e)
   }
 
-}
+  /**
+   * Returns a call graph starting from the given sources, taking into account
+   * instantiations of function type parameters,
+   * If given limit of explored nodes reached, it returns a partial set of reached TypedFunDefs
+   * and the boolean set to "false".
+   * Otherwise, it returns the full set of reachable TypedFunDefs and "true"
+   */
+
+  def typedTransitiveCallees(sources: Set[TypedFunDef], limit: Option[Int] = None): (Set[TypedFunDef], Boolean) = {
+    import leon.utils.SearchSpace.reachable
+    reachable(
+      sources,
+      (tfd: TypedFunDef) => functionCallsOf(tfd.fd.fullBody) map { _.tfd },
+      limit
+    )
+  }
+
+}
\ No newline at end of file

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

@@ -437,6 +437,8 @@ object Definitions {
       TypedFunDef(this, tparams.map(_.tp))
     }
 
+    def isRecursive(p: Program) = p.callGraph.transitiveCallees(this) contains this
+
     setSubDefOwners()
     // Deprecated, old API
     @deprecated("Use .body instead", "2.3")

src/main/scala/leon/purescala/ExprOps.scala

@@ -1955,6 +1955,7 @@ object ExprOps {
     case _ => None
   }
 
+
   /**
    * Deprecated API
    * ========

src/main/scala/leon/solvers/SolverFactory.scala

@@ -19,7 +19,7 @@ object SolverFactory {
     }
   }
 
-  val definedSolvers = Set("fairz3", "unrollz3", "enum", "smt", "smt-z3", "smt-cvc4")
+  val definedSolvers = Set("fairz3", "unrollz3", "enum", "smt", "smt-z3", "smt-cvc4", "smt-2.5-cvc4")
 
   def getFromSettings[S](ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
     import combinators._
@@ -42,6 +42,9 @@ object SolverFactory {
       case "smt-cvc4" =>
         SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBSolver(ctx, program) with SMTLIBCVC4Target) with TimeoutSolver)
 
+      case "smt-2.5-cvc4" =>
+        SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBUnrollingCVC4Target with TimeoutSolver)
+
       case _ =>
         ctx.reporter.fatalError("Unknown solver "+name)
     }

src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers.smtlib
+
+import purescala.Definitions.TypedFunDef
+import purescala.DefOps.typedTransitiveCallees
+import purescala.ExprOps.matchToIfThenElse
+import smtlib.parser.Commands._
+import smtlib.parser.Terms._
+
+trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
+  this: SMTLIBSolver =>
+
+  private val typedFunDefExplorationLimit = 10000
+
+  override def targetName = "2.5-cvc4"
+  override def declareFunction(tfd: TypedFunDef): SSymbol = {
+    if (tfd.params.isEmpty) {
+      super[SMTLIBCVC4Target].declareFunction(tfd)
+    } else {
+      val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
+      if (!exploredAll) {
+        reporter.warning(
+          s"Did not manage to explore the space of typed functions called from ${tfd.id}. The solver may fail"
+        )
+      }
+
+      val (smtFunDecls, smtBodies) = funs.toSeq.collect {
+        case tfd if !functions.containsA(tfd) && tfd.params.nonEmpty =>
+          val id = if (tfd.tps.isEmpty) {
+            tfd.id
+          } else {
+            tfd.id.freshen
+          }
+          val sym = id2sym(id)
+          functions +=(tfd, sym)
+          (
+            FunDec(
+              sym,
+              tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
+              declareSort(tfd.returnType)
+            ),
+            toSMT(matchToIfThenElse(tfd.body.get))(tfd.params.map { p =>
+              (p.id, id2sym(p.id): Term)
+            }.toMap)
+            )
+      }.unzip
+
+      if (smtFunDecls.nonEmpty) sendCommand(DefineFunsRec(smtFunDecls, smtBodies))
+      functions.toB(tfd)
+    }
+  }
+
+}

src/main/scala/leon/utils/SearchSpace.scala

+package leon.utils
+
+object SearchSpace {
+
+  def reachable[A](sources: Set[A], generateNeighbors: A => Set[A], limit: Option[Int] = None): (Set[A], Boolean) = {
+    require(limit forall(_ >= 0))
+    def rec(seen: Set[A], toSee: Set[A], limit: Option[Int]): (Set[A], Boolean) = {
+      (toSee.headOption, limit) match {
+        case (None, _) =>
+          (seen, true)
+        case (_, Some(0)) =>
+          (seen, false)
+        case (Some(hd), _) =>
+          val neighbors = generateNeighbors(hd)
+          rec(seen + hd, toSee ++ neighbors -- (seen + hd), limit map {_ - 1})
+      }
+    }
+
+    rec(Set(), sources, limit)
+  }
+
+}