diff --git a/CHANGELOG.md b/CHANGELOG.md
deleted file mode 100644
index 9ea1ad0fe669f6a4b8b93bced958a9bc8ca81520..0000000000000000000000000000000000000000
--- a/CHANGELOG.md
+++ /dev/null
@@ -1,64 +0,0 @@
-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
diff --git a/README.md b/README.md
index 65f322b4e1efbfebaef80a3a81094bdc2f0c85e8..797af21869afb9a19146139cffaf70534c4145e1 100644
--- a/README.md
+++ b/README.md
@@ -1,15 +1,13 @@
-Leon 3.0 [](http://laraquad4.epfl.ch:9000/epfl-lara/leon)
+Inox 0.1 [](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)
diff --git a/build.sbt b/build.sbt
index 9b0df3e328387f6987f285e165c42f94d3182b07..8de5744b5d20c596cf72c0e87aed0c3726327a36 100644
--- a/build.sbt
+++ b/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"
)
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 4f3bf2a7d390c08b5091093acde71aafbd5c8eee..c0583c6923468b38313e56fdc41a714bdd27d0ec 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/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)
}
diff --git a/src/main/scala/inox/ast/Types.scala b/src/main/scala/inox/ast/Types.scala
index f6c59d18267d48c181ea7172d951f4d0baaecc67..92fb6c242372c5658fd7143d050612d7c91ed8a6 100644
--- a/src/main/scala/inox/ast/Types.scala
+++ b/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
diff --git a/src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala b/src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala
index ee9a9f7492568a3924302757c643ca8e00692695..4f5bb93009b9574e3c27fb25566cca4e3b5dad4c 100644
--- a/src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala
+++ b/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
diff --git a/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala b/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
index 51c746358736ac9390a417f8a1e8397803a38f2d..714e58a27a69e88475da088c5ab78ef222d9016d 100644
--- a/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
+++ b/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 }