Fixes and preparation for stainless

CHANGELOG.md

-Change Log
-----------
-
-#### v?.?
-
-Among the changes are (see the commits for details):
-* Resource bound inference engine Orb, developed by Ravi is now merged into master
-* Leon can now do program repair, thanks to Etienne and Manos
-* Experimental support for first-order quantifiers inside Leon
-* Isabelle proof assistant can now be used as a solver, thanks to Lars Hupel
-* A DSL for writing equational proofs in Leon, thanks to Sandro Stucki and Marco Antognini
-* Leon now uses the improved SMT-LIB library, thanks to the continuous work of Regis Blanc
-* New case studies, including a little robot case study thanks to Etienne
-* Improved termination checker of Nicolas Voirol with additions from Samuel Gruetter
-* Many additions to Leon's library, including the state monad
-* Numerous refactorings and bug fixes thanks to relentless work of Manos
-* Add --watch option to automatically re-run Leon after file modifications, thanks to Etienne
-* Somewhat extended source language that allows for deep type hierarchies (Manos)
-* Synthesis improvements: nore specific grammar for CEGIS and various optimizations, new synthesis rules 
-  and new design of the exploration strategy (Etienne and Manos)
-
-#### v3.0
-*Released 17.02.2015*
-
-* Int is now treated as BitVector(32)
-* Introduce BigInt for natural numbers
-
-#### v2.4
-*Released 10.02.2015*
-
-* Implement support for higher-order functions
-
-#### v2.3
-*Released 03.03.2014*
-
-* Accept multiple files with multiple modules/classes. Support class
-  definitions with methods.
-* Introduce the Leon library with common generic datastructures, List and
-  Option for now.
-* Add PortfolioSolver which tries a list of solvers (--solvers) in parallel.
-* Add EnumerationSolver which uses Vanuatoo to guess models.
-* Add documentation and sbt support for development under Eclipse,
-
-#### v2.2
-*Released 04.02.2014*
-
-* Generics for functions and ADTs
-* Use instantiation-time mixing for timeout sovlers
-* Improve unrolling solvers to use incremental solvers
-
-#### v2.1
-*Released 10.01.2014*
-
-* Reworked TreeOps API
-* Tracing evaluators
-* Support for range positions
-* Support choose() in evaluators
-* Flatten functions in results of synthesis
-* Improved pretty printers with context information
-
-
-#### v2.0
-
-* First release

README.md

-Leon 3.0 [![Build Status](http://laraquad4.epfl.ch:9000/epfl-lara/leon/status/master)](http://laraquad4.epfl.ch:9000/epfl-lara/leon)
+Inox 0.1 [![Build Status](http://laraquad4.epfl.ch:9000/epfl-lara/inox/status/master)](http://laraquad4.epfl.ch:9000/epfl-lara/inox)
 ==========
 
 Getting Started
 ---------------
 
-To build Leon you will need JDK, scala, sbt, and some external solver binaries.
+To build Inox, you will need JDK, scala, sbt, and some external solver binaries.
 On Linux, it should already work out of the box.
 
 To get started, see the documentation chapters, such as
   * [Getting Started](src/sphinx/gettingstarted.rst)
   * [Installation](src/sphinx/installation.rst)
-  * [Introduction to Leon](src/sphinx/intro.rst)
-
-[For change log, see CHANGELOG.md](CHANGELOG.md)
+  * [Introduction to Inox](src/sphinx/intro.rst)

build.sbt

@@ -4,9 +4,7 @@ version := "0.1"
 
 organization := "ch.epfl.lara"
 
-val scalaVer = "2.11.8"
-
-scalaVersion := scalaVer
+scalaVersion := "2.11.8"
 
 scalacOptions ++= Seq(
   "-deprecation",
@@ -39,11 +37,8 @@ resolvers ++= Seq(
 )
 
 libraryDependencies ++= Seq(
-  "org.scala-lang" % "scala-compiler" % scalaVer,
   "org.scalatest" %% "scalatest" % "2.2.4" % "test;it",
   "com.typesafe.akka" %% "akka-actor" % "2.3.4",
-  "org.ow2.asm" % "asm-all" % "5.0.4",
-  "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2",
   "org.apache.commons" % "commons-lang3" % "3.4"
   //"com.regblanc" %% "scala-smtlib" % "0.2"
 )

src/main/scala/inox/ast/ExprOps.scala

@@ -48,19 +48,23 @@ trait ExprOps extends GenTreeOps {
     case _ => None
   } (expr)
 
+  object VariableExtractor {
+    def unapply(e: Expr): Option[(Set[Variable], Set[Variable])] = e match {
+      case v: Variable => Some((Set(v), Set.empty))
+      case Let(vd, _, _) => Some((Set.empty, Set(vd.toVariable)))
+      case Lambda(args, _) => Some((Set.empty, args.map(_.toVariable).toSet))
+      case Forall(args, _) => Some((Set.empty, args.map(_.toVariable).toSet))
+      case Choose(res, _) => Some((Set.empty, Set(res.toVariable)))
+      case _ => Some((Set.empty, Set.empty))
+    }
+  }
+
   /** Returns the set of free variables in an expression */
   def variablesOf(expr: Expr): Set[Variable] = {
-    fold[Set[Variable]] {
-      case (e, subs) =>
-        val subvs = subs.flatten.toSet
-        e match {
-          case v: Variable => subvs + v
-          case Let(vd, _, _) => subvs - vd.toVariable
-          case Lambda(args, _) => subvs -- args.map(_.toVariable)
-          case Forall(args, _) => subvs -- args.map(_.toVariable)
-          case Choose(res, _) => subvs - res.toVariable
-          case _ => subvs
-        }
+    fold[Set[Variable]] { case (e, subs) =>
+      val subvs = subs.flatten.toSet
+      val VariableExtractor(add, remove) = e
+      subvs ++ add -- remove
     }(expr)
   }
 

src/main/scala/inox/ast/Types.scala

@@ -10,7 +10,7 @@ trait Types { self: Trees =>
     def isTyped(implicit s: Symbols): Boolean = getType != Untyped
   }
 
-  private[ast] trait CachingTyped extends Typed {
+  protected trait CachingTyped extends Typed {
     private var lastSymbols: Symbols = null
     private var lastType: Type = null
 

src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala

@@ -5,7 +5,6 @@ package solvers
 package combinators
 
 import scala.collection.mutable.Queue
-import scala.reflect.runtime.universe._
 
 /**
  * This is a straitforward implementation of solver pools. The goal is to avoid

src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala

@@ -4,8 +4,6 @@ package inox
 package solvers
 package combinators
 
-import scala.reflect.runtime.universe._
-
 trait TimeoutSolverFactory extends SolverFactory {
   type S <: TimeoutSolver { val program: TimeoutSolverFactory.this.program.type }