diff --git a/CODING_GUIDELINES.md b/CODING_GUIDELINES.md
deleted file mode 100644
index 9f3684519791ed111c19c9e8101b6e0c89a13c90..0000000000000000000000000000000000000000
--- a/CODING_GUIDELINES.md
+++ /dev/null
@@ -1,87 +0,0 @@
-# Leon Coding Guidelines
-
-
-Here are a few coding guidelines that should be followed when introducing new
-code into Leon. Existing code that do not meet these guidelines should
-eventually be fixed.
-
-## Development
-
-#### Global state must be concurrent-friendly
-
-Leon relies on global state at several places, it should be assumed that this
-global state can be accessed concurrently, it is thus necessary to ensure that
-it will behave consistently. Global state should be ```private[this]``` and
-accessor functions **synchronized**. Another possibility for things like
-counters is to rely on Java classes such as ```AtomicInteger```.
-
-Even though most of Leon is sequential, parts of it is concurrent (Portfolio
-Solvers, Web interface, Interrupt threads, ...). It is likely to become more
-concurrent in the future.
-
-#### Code should be predictable
-
-Leon's execution should be predictable and reproducible. Due to the complex
-nature of its inner-working, it is crucial that problematic executions and bug
-reports are consistently reproducible.
-
-One of the main reason behind this unpredictability is the traversal of
-structures that are not explicitly ordered(e.g. ``Set``, ``Map``, ..). Please
-avoid that by either explicitly ordering after ``.toSeq``, or by using
-different datastructures.
-
-
-## Documentation
-
-There are two levels of documentation in Leon. the subdirectory ```/doc```
-contains a user manual intended for end-user of Leon. This documentation
-describes the Leon language and the conceptual algorithms of Leon. It is
-intended for people that wish to use Leon as a tool to help them write better
-software. On the other hand, ScalaDoc is used in the source code of Leon for
-describing the internal structure of Leon.
-
-Ideally, all modules/classes that export some functionalities for other
-modules/classes in Leon (or more broadly) should be documented using the
-ScalaDoc. We follow convention outlined
-[here](http://docs.scala-lang.org/style/scaladoc.html). Existing code is not
-well documentated, but we should strive at improving that whenever we get the
-opportunity.
-
-
-## Testing
-
-Leon tests are currently separated in three layers:
-- unit tests
-- integration tests
-- regression tests
-
-```sbt test``` runs only unit tests. Please do not push changes without testing them with ```sbt test integration:test```.
-
-
-### Unit Tests
-
-Leon should have unit-tests for commonly used functions. Although it is
-convenient to rely on a program extracted from Scalac, it is NOT ok to
-write a unit test that rely on an external system (e.g. scalac).
-A unit test should be fast, predictable, and entirely self contained.
-If an external system is required (parser, solver), the system should be mocked
-and the test should focus on testing the piece of code that interacts with
-that system.
-
-It is understood that some functionalities are extremely difficult to unit
-test properly. Thus it is perfectly ok to leave some complex task to be tested
-by integration tests. A typical example would be ```codegen``` which basically
-relies on the JVM.
-
-New library functions or important changes to library functions warrant unit
-tests.
-
-### Integration Tests
-
-Integration tests rely on one or more components of Leon. For instance, a test might rely on extraction to build a complex ```Program```, which is then used to test DefOps operations. Even though these tests are not self-contained, their dependencies can be assumed correct. This allows us to test parts/features that cannot easily be isolated: functions on large programs, solvers, code-gen evaluators.
-
-### Regression Tests
-
-Regression tests are meant to ensure that Leon behaves consistently as a whole on a large set of source files. Entire features of leon are tested by typically running a full pipeline on several file inputs. These tests are slow and are used by travis-ci to validate builds.
-
-**Important:** If/When an regression test fails, the code fix must be accompanied with unit or integration tests that would have caught the issue. This is a on-demand path to transition from essentially only regression tests to smaller, focused tests.
diff --git a/src/main/scala/inox/InoxOptions.scala b/src/main/scala/inox/InoxOptions.scala
index 8ccdfec4f418208f2e5962d708dd3511256572d4..dee27c9016ad2bc2178b51d19d19d0eed0cba4c0 100644
--- a/src/main/scala/inox/InoxOptions.scala
+++ b/src/main/scala/inox/InoxOptions.scala
@@ -27,7 +27,7 @@ abstract class InoxOptionDef[+A] {
parser(s).getOrElse(
reporter.fatalError(
s"Invalid option usage: --$name\n" +
- "Try 'leon --help' for more information."
+ "Try '--help' for more information."
)
)
}
diff --git a/src/main/scala/inox/Reporter.scala b/src/main/scala/inox/Reporter.scala
index 32347fab9f9a1b539766e7c2e0be13cc4889cfe6..9ad6812867d1bdcafa5864e5a3826bb4973ac59d 100644
--- a/src/main/scala/inox/Reporter.scala
+++ b/src/main/scala/inox/Reporter.scala
@@ -52,7 +52,7 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
final def internalError(pos: Position, msg : Any) : Nothing = {
emit(account(Message(INTERNAL, pos, msg.toString +
- "\nPlease inform the authors of Leon about this message"
+ "\nPlease inform the authors of Inox about this message"
)))
onFatal()
}
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 1a32fb14e163ae524d5e57dc68da9eb648d74880..2a4d6e077f3178cd3393bc71abfe4388ead2fa35 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -5,7 +5,7 @@ package ast
/** Provides functions to manipulate [[Expressions.Expr]].
*
- * This object provides a few generic operations on Leon expressions,
+ * This object provides a few generic operations on Inox expressions,
* as well as some common operations.
*
* The generic operations lets you apply operations on a whole tree
@@ -19,7 +19,7 @@ package ast
*
* These operations usually take a higher order function that gets applied to the
* expression tree in some strategy. They provide an expressive way to build complex
- * operations on Leon expressions.
+ * operations on Inox expressions.
*
*/
trait ExprOps extends GenTreeOps {
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index baf93ab3e368de60584e81ecbf2d75c664c751ee..9b1f8a4f69946a904b91f8ebc5388c4dcd542a23 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -3,7 +3,19 @@
package inox
package ast
-
+/** Meat and bones of tree deconstruction/reconstruction.
+ *
+ * Implementations provide methods to extract all useful subtrees from
+ * a given tree ([[Expressions.Expr]], [[Types.Type]], ...) as well as
+ * a closure that can reconstruct the initial tree based on appropriate
+ * arguments.
+ *
+ * Instances of [[Trees]] must provide a [[TreeDeconstructor]] as a
+ * means of applying generic transformations to arbitrary extensions of
+ * the [[Trees.Tree]] interface.
+ *
+ * @see [[Extractors]] for some interesting use cases
+ */
trait TreeDeconstructor {
protected val s: Trees
protected val t: Trees
@@ -240,6 +252,8 @@ trait TreeDeconstructor {
}
}
+/** Provides extraction capabilities to [[Trees]] based on a
+ * [[TreeDeconstructor]] instance. */
trait Extractors { self: Trees =>
val deconstructor: TreeDeconstructor {
@@ -249,7 +263,7 @@ trait Extractors { self: Trees =>
/** Operator Extractor to extract any Expression in a consistent way.
*
- * You can match on any Leon Expr, and then get both a Seq[Expr] of
+ * You can match on any Inox Expr, and then get both a Seq[Expr] of
* subterms and a builder function that takes a Seq of subterms (of same
* length) and rebuild the original node.
*
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 27e66692b3f1aae900cdb5463d3efbeb5b910784..d019cc30259711806a749d953ca254235f642ed2 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -5,24 +5,9 @@ package ast
import utils._
-/** Provides functions to manipulate [[purescala.Expressions]].
- *
- * This object provides a few generic operations on Leon expressions,
- * as well as some common operations.
- *
- * The generic operations lets you apply operations on a whole tree
- * expression. You can look at:
- * - [[GenTreeOps.fold foldRight]]
- * - [[GenTreeOps.preTraversal preTraversal]]
- * - [[GenTreeOps.postTraversal postTraversal]]
- * - [[GenTreeOps.preMap preMap]]
- * - [[GenTreeOps.postMap postMap]]
- * - [[GenTreeOps.genericTransform genericTransform]]
- *
- * These operations usually take a higher order function that gets applied to the
- * expression tree in some strategy. They provide an expressive way to build complex
- * operations on Leon expressions.
- *
+/** Provides functions to manipulate [[Expressions.Expr]] in cases where
+ * a symbol table is available (and required: see [[ExprOps]] for
+ * simpler tree manipulations).
*/
trait SymbolOps { self: TypeOps =>
import trees._
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 1b40732590cb3ffaa2b2020f5154ac6bae50f043..977158077763f4c4aef865385dc96a99409cdc03 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -76,14 +76,6 @@ trait RecursiveEvaluator
// build a mapping for the function...
val frame = rctx.withNewVars(tfd.paramSubst(evArgs))
- // @nv TODO: choose evaluation
-
- /* @nv TODO: should we do this differently?? lambdas??
- if (!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Evaluation of function with unknown implementation." + expr)
- }
- */
-
e(tfd.fullBody)(frame, gctx)
case And(Seq(e1, e2)) =>
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index c96cc9c351c1f3051d7f58b7cf78e1214851b028..6f0b46875f67abc2028096d0ef773a796f8be633 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -38,7 +38,7 @@ object SolverFactory {
private val solverNames = Map(
"nativez3" -> "Native Z3 with z3-templates for unrolling",
- "unrollz3" -> "Native Z3 with leon-templates for unrolling",
+ "unrollz3" -> "Native Z3 with inox-templates for unrolling",
"smt-cvc4" -> "CVC4 through SMT-LIB",
"smt-z3" -> "Z3 through SMT-LIB",
"enum" -> "Enumeration-based counter-example finder"
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index c07d63da17159368fdf2988211190ce1e8921a77..4502f862c1a4f3c82823ef1317506c21a1d550ce 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -106,7 +106,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
}
/*
- * Translation from Leon Expressions to SMTLIB terms and reverse
+ * Translation from Inox Expressions to SMTLIB terms and reverse
*/
/* Symbol handling */
@@ -219,7 +219,6 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
val cmd = DeclareDatatypes(adts)
emit(cmd)
}
-
}
protected def declareStructuralSort(t: Type): Sort = {
@@ -266,7 +265,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
}
}
- /* Translate a Leon Expr to an SMTLIB term */
+ /* Translate a Inox Expr to an SMTLIB term */
def sortToSMT(s: Sort): SExpr = {
s match {
@@ -477,7 +476,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
}
}
- /* Translate an SMTLIB term back to a Leon Expr */
+ /* Translate an SMTLIB term back to a Inox Expr */
protected def fromSMT(t: Term, otpe: Option[Type] = None)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
object EQ {
diff --git a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
index 65471acbf9948744d73a6831765c47f2aa8f28f6..dd160676e0061e54c96b3a18347ff371ed6dacaa 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -90,7 +90,7 @@ trait AbstractZ3Solver
// ADT Manager
private val adtManager = new ADTManager
- // Bijections between Leon Types/Functions/Ids to Z3 Sorts/Decls/ASTs
+ // Bijections between Inox Types/Functions/Ids to Z3 Sorts/Decls/ASTs
private val functions = new IncrementalBijection[TypedFunDef, Z3FuncDecl]()
private val lambdas = new IncrementalBijection[FunctionType, Z3FuncDecl]()
private val variables = new IncrementalBijection[Variable, Z3AST]()
@@ -225,6 +225,11 @@ trait AbstractZ3Solver
case Int32Type | BooleanType | IntegerType | RealType | CharType =>
sorts(oldtt)
+ case tt @ BVType(i) =>
+ sorts.cached(tt) {
+ z3.mkBVSort(i)
+ }
+
case tpe @ (_: ADTType | _: TupleType | _: TypeParameter | UnitType) =>
sorts.getOrElse(tpe, declareStructuralSort(tpe))
diff --git a/src/main/scala/inox/utils/Bijection.scala b/src/main/scala/inox/utils/Bijection.scala
index ed84073a4088a39ce849dbcfcc930425e9c1b357..7d506a203199e4e30386e9f37d0d399b48b92c1e 100644
--- a/src/main/scala/inox/utils/Bijection.scala
+++ b/src/main/scala/inox/utils/Bijection.scala
@@ -13,7 +13,7 @@ object Bijection {
*
* This basically maintains a bi-directional mapping
* between A and B. This is a common operation throughout
- * Leon, that would be usually done by keeping a mapping and
+ * Inox, that would be usually done by keeping a mapping and
* the corresponding reverse mapping. This class abstracts
* away the details.
*
diff --git a/src/main/scala/inox/utils/InterruptManager.scala b/src/main/scala/inox/utils/InterruptManager.scala
index 5377c0c6c4cbdc00681911f557f36968f84b1c11..f00d1e9a4a9e4fce6930ff20d7ae04cead518a8d 100644
--- a/src/main/scala/inox/utils/InterruptManager.scala
+++ b/src/main/scala/inox/utils/InterruptManager.scala
@@ -21,7 +21,7 @@ class InterruptManager(reporter: Reporter) extends Interruptible {
def now(): Long = System.currentTimeMillis()
reporter.info("")
if (now() - lastTimestamp.get < exitWindow) {
- reporter.warning("Aborting Leon...")
+ reporter.warning("Aborting Inox...")
System.exit(1)
}
else {
diff --git a/unmanaged/64/vanuatoo_2.11-0.1.jar b/unmanaged/64/vanuatoo_2.11-0.1.jar
deleted file mode 100644
index 9550eb732bb464d91853cb6edc5fcedee9f8f481..0000000000000000000000000000000000000000
Binary files a/unmanaged/64/vanuatoo_2.11-0.1.jar and /dev/null differ