From fbbca114a8d7af021bc20d677ad2cf0e2e3a411a Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 18 Aug 2016 10:55:08 +0200
Subject: [PATCH] Fixes and preparation for stainless
---
CHANGELOG.md | 64 -------------------
README.md | 8 +--
build.sbt | 7 +-
src/main/scala/inox/ast/ExprOps.scala | 26 ++++----
src/main/scala/inox/ast/Types.scala | 2 +-
.../combinators/SolverPoolFactory.scala | 1 -
.../combinators/TimeoutSolverFactory.scala | 2 -
7 files changed, 20 insertions(+), 90 deletions(-)
delete mode 100644 CHANGELOG.md
diff --git a/CHANGELOG.md b/CHANGELOG.md
deleted file mode 100644
index 9ea1ad0fe..000000000
--- 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 65f322b4e..797af2186 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 9b0df3e32..8de5744b5 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 4f3bf2a7d..c0583c692 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 f6c59d182..92fb6c242 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 ee9a9f749..4f5bb9300 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 51c746358..714e58a27 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 }
--
GitLab