diff --git a/src/main/scala/inox/Options.scala b/src/main/scala/inox/Options.scala
index e19fdff3bba2e940172440441a54fffa0ab9bbab..2b06bd4589f1c3e363842cc2dc3b9402a0d53678 100644
--- a/src/main/scala/inox/Options.scala
+++ b/src/main/scala/inox/Options.scala
@@ -62,6 +62,10 @@ case class LongOptionDef(name: String, description: String, default: Long, usage
val parser = longParser
}
+case class IntOptionDef(name: String, description: String, default: Int, usageRhs: String) extends OptionDef[Int] {
+ val parser = intParser
+}
+
class OptionValue[A] private (val optionDef: OptionDef[A], val value: A) {
override def toString = s"--${optionDef.name}=$value"
override def equals(other: Any) = other match {
@@ -82,9 +86,8 @@ object OptionValue {
object OptionParsers {
type OptionParser[A] = String => Option[A]
- val longParser: OptionParser[Long] = { s =>
- Try(s.toLong).toOption
- }
+ val intParser: OptionParser[Int] = { s => Try(s.toInt).toOption }
+ val longParser: OptionParser[Long] = { s => Try(s.toLong).toOption }
val stringParser: OptionParser[String] = Some(_)
val booleanParser: OptionParser[Boolean] = {
case "on" | "true" | "yes" | "" => Some(true)
diff --git a/src/main/scala/inox/ast/CallGraph.scala b/src/main/scala/inox/ast/CallGraph.scala
index eb0c3f0835543f4344a0a5f915611b00f32a3583..047ac4151ee3ba37f5e9e32c38f379fa1c27fc86 100644
--- a/src/main/scala/inox/ast/CallGraph.scala
+++ b/src/main/scala/inox/ast/CallGraph.scala
@@ -32,6 +32,10 @@ trait CallGraph {
graph.transitiveSucc(f) contains f
}
+ def isSelfRecursive(f: FunDef) = {
+ graph.succ(f) contains f
+ }
+
def calls(from: FunDef, to: FunDef) = {
graph.E contains SimpleEdge(from, to)
}
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 3d398cebd409976d07360bee49ee1383b17d69d1..f010ad44f382adeb2a0642ed07ba3a76261b5faa 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -33,7 +33,7 @@ trait Definitions { self: Trees =>
* Both types share much in common and being able to reason about them
* in a uniform manner can be useful in certain cases.
*/
- protected[ast] trait VariableSymbol extends Typed {
+ protected[ast] trait VariableSymbol extends Tree with Typed {
val id: Identifier
val tpe: Type
@@ -59,14 +59,14 @@ trait Definitions { self: Trees =>
implicit def convertToVal = new VariableConverter[ValDef] {
def convert(vs: VariableSymbol): ValDef = vs match {
case v: ValDef => v
- case _ => ValDef(vs.id, vs.tpe)
+ case _ => ValDef(vs.id, vs.tpe).copiedFrom(vs)
}
}
implicit def convertToVariable = new VariableConverter[Variable] {
def convert(vs: VariableSymbol): Variable = vs match {
case v: Variable => v
- case _ => Variable(vs.id, vs.tpe)
+ case _ => Variable(vs.id, vs.tpe).copiedFrom(vs)
}
}
@@ -259,7 +259,7 @@ trait Definitions { self: Trees =>
tparams: Seq[TypeParameterDef] = this.tparams,
cons: Seq[Identifier] = this.cons,
flags: Set[Flag] = this.flags
- ): ADTSort = new ADTSort(id, tparams, cons, flags)
+ ): ADTSort = new ADTSort(id, tparams, cons, flags).copiedFrom(this)
}
/** Case classes/ ADT constructors. For single-case classes these may coincide
@@ -304,7 +304,7 @@ trait Definitions { self: Trees =>
sort: Option[Identifier] = this.sort,
fields: Seq[ValDef] = this.fields,
flags: Set[Flag] = this.flags
- ): ADTConstructor = new ADTConstructor(id, tparams, sort, fields, flags)
+ ): ADTConstructor = new ADTConstructor(id, tparams, sort, fields, flags).copiedFrom(this)
}
/** Represents an [[ADTDefinition]] whose type parameters have been instantiated to ''tps'' */
@@ -334,11 +334,15 @@ trait Definitions { self: Trees =>
/** Represents an [[ADTSort]] whose type parameters have been instantiated to ''tps'' */
case class TypedADTSort(definition: ADTSort, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedADTDefinition {
+ copiedFrom(definition)
+
lazy val constructors: Seq[TypedADTConstructor] = definition.constructors.map(_.typed(tps))
}
/** Represents an [[ADTConstructor]] whose type parameters have been instantiated to ''tps'' */
case class TypedADTConstructor(definition: ADTConstructor, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedADTDefinition {
+ copiedFrom(definition)
+
lazy val fields: Seq[ValDef] = {
val tmap = (definition.typeArgs zip tps).toMap
if (tmap.isEmpty) definition.fields
@@ -401,12 +405,14 @@ trait Definitions { self: Trees =>
returnType: Type = this.returnType,
fullBody: Expr = this.fullBody,
flags: Set[Flag] = this.flags
- ): FunDef = new FunDef(id, tparams, params, returnType, fullBody, flags)
+ ): FunDef = new FunDef(id, tparams, params, returnType, fullBody, flags).copiedFrom(this)
}
/** Represents a [[FunDef]] whose type parameters have been instantiated with the specified types */
case class TypedFunDef(fd: FunDef, tps: Seq[Type])(implicit symbols: Symbols) extends Tree {
+ copiedFrom(fd)
+
val id = fd.id
def signature = {
diff --git a/src/main/scala/inox/ast/Identifier.scala b/src/main/scala/inox/ast/Identifier.scala
index f9f847b80082d85ad00ceea1d395b43f93c01ccb..557de837f7e6ded1fd8fe2cee64a14cf56fcf666 100644
--- a/src/main/scala/inox/ast/Identifier.scala
+++ b/src/main/scala/inox/ast/Identifier.scala
@@ -1,6 +1,6 @@
package inox.ast
-import inox.utils.UniqueCounter
+import inox.utils.{UniqueCounter, Positioned}
/** Represents a unique symbol in Inox.
*
@@ -12,7 +12,7 @@ class Identifier (
val globalId: Int,
private val id: Int,
private val alwaysShowUniqueID: Boolean = false
-) extends Ordered[Identifier] {
+) extends Ordered[Identifier] with Positioned {
override def equals(other: Any): Boolean = other match {
case null => false
diff --git a/src/main/scala/inox/ast/ProgramEncoder.scala b/src/main/scala/inox/ast/ProgramEncoder.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e7cae628d5d925b235dad502bd0fcd32174623c7
--- /dev/null
+++ b/src/main/scala/inox/ast/ProgramEncoder.scala
@@ -0,0 +1,37 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package ast
+
+trait ProgramEncoder extends TreeBijection {
+ val sourceProgram: Program
+ lazy val s: sourceProgram.trees.type = sourceProgram.trees
+ lazy val targetProgram: Program { val trees: t.type } = sourceProgram.transform(encoder)
+
+ /* @nv XXX: ideally, we would want to replace `>>` by `override def andThen`, however this
+ * seems to break the scala compiler for some weird reason... */
+ def >>(that: TreeBijection { val s: ProgramEncoder.this.t.type }): ProgramEncoder {
+ val sourceProgram: ProgramEncoder.this.sourceProgram.type
+ val t: that.t.type
+ } = new ProgramEncoder {
+ val sourceProgram: ProgramEncoder.this.sourceProgram.type = ProgramEncoder.this.sourceProgram
+ val t: that.t.type = that.t
+
+ val encoder = ProgramEncoder.this.encoder andThen that.encoder
+ val decoder = that.decoder andThen ProgramEncoder.this.decoder
+ }
+}
+
+object ProgramEncoder {
+ def empty(p: Program): ProgramEncoder {
+ val sourceProgram: p.type
+ val t: p.trees.type
+ } = new ProgramEncoder {
+ val sourceProgram: p.type = p
+ val t: p.trees.type = p.trees
+
+ object encoder extends p.trees.IdentitySymbolTransformer
+ object decoder extends p.trees.IdentitySymbolTransformer
+ }
+}
+
diff --git a/src/main/scala/inox/evaluators/ContextualEvaluator.scala b/src/main/scala/inox/evaluators/ContextualEvaluator.scala
index fba8ac52dfc68456d48d78747636fe849ba2d15c..3b4380a5f3dcd750376a51b536be960d0ec22bcb 100644
--- a/src/main/scala/inox/evaluators/ContextualEvaluator.scala
+++ b/src/main/scala/inox/evaluators/ContextualEvaluator.scala
@@ -3,11 +3,15 @@
package inox
package evaluators
+object optMaxCalls extends IntOptionDef("maxcalls",
+ "Maximum number of function invocations allowed during evaluation", 50000, "<PosInt> | -1 (for unbounded")
+
trait ContextualEvaluator extends Evaluator {
- val maxSteps: Int
import program._
import program.trees._
+ lazy val maxSteps: Int = options.findOptionOrDefault(optMaxCalls)
+
trait RecContext[RC <: RecContext[RC]] {
def mappings: Map[ValDef, Expr]
def newVars(news: Map[ValDef, Expr]): RC
diff --git a/src/main/scala/inox/evaluators/EncodingEvaluator.scala b/src/main/scala/inox/evaluators/EncodingEvaluator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..97e887d07b75178ab5b9f5adcce39e475cc2c595
--- /dev/null
+++ b/src/main/scala/inox/evaluators/EncodingEvaluator.scala
@@ -0,0 +1,47 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package evaluators
+
+trait EncodingEvaluator extends DeterministicEvaluator { self =>
+ import program.trees._
+
+ protected val encoder: ast.ProgramEncoder { val sourceProgram: program.type }
+
+ protected val underlying: DeterministicEvaluator {
+ val program: encoder.targetProgram.type
+ }
+
+ lazy val options = underlying.options
+
+ def eval(expr: Expr, model: Map[ValDef, Expr]): EvaluationResult = {
+ val res = underlying.eval(
+ encoder.encode(expr),
+ model.map(p => encoder.encode(p._1) -> encoder.encode(p._2))
+ )
+
+ res match {
+ case EvaluationResults.Successful(v) => EvaluationResults.Successful(encoder.decode(v))
+ case EvaluationResults.RuntimeError(msg) => EvaluationResults.RuntimeError(msg)
+ case EvaluationResults.EvaluatorError(msg) => EvaluationResults.EvaluatorError(msg)
+ }
+ }
+}
+
+object EncodingEvaluator {
+ def solving(p: Program)
+ (enc: ast.ProgramEncoder { val sourceProgram: p.type })
+ (ev: DeterministicEvaluator with SolvingEvaluator { val program: enc.targetProgram.type }) = {
+ new {
+ val program: p.type = p
+ } with EncodingEvaluator with SolvingEvaluator {
+ lazy val encoder: enc.type = enc
+ lazy val underlying = ev
+
+ def getSolver(opts: OptionValue[_]*) = {
+ solvers.combinators.EncodingSolverFactory(p)(enc)(underlying.getSolver(opts : _*))
+ }
+ }
+ }
+
+}
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index d3b0e2da23d19456a9333f7c27274f9d17968f40..56ea64bf691e05c52da75c5630468299b2a0b3df 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -513,9 +513,8 @@ object RecursiveEvaluator {
def apply(p: InoxProgram, opts: Options): RecursiveEvaluator { val program: p.type } = {
new {
val program: p.type = p
- } with RecursiveEvaluator with HasDefaultGlobalContext with HasDefaultRecContext {
val options = opts
- val maxSteps = 50000
+ } with RecursiveEvaluator with HasDefaultGlobalContext with HasDefaultRecContext {
def getSolver(moreOpts: OptionValue[_]*) = solvers.SolverFactory(p, opts ++ moreOpts)
}
}
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index dd0e9fa5a6c41413b38f19bc98507db4c25073c6..1a720c78adcaaf8eae5a81f838cc1cb9257590bb 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -4,6 +4,7 @@ package inox
package evaluators
import solvers._
+import solvers.combinators._
import scala.collection.mutable.{Map => MutableMap}
@@ -20,7 +21,10 @@ trait SolvingEvaluator extends Evaluator {
def default = MutableMap.empty
}
- def getSolver(opts: OptionValue[_]*): SolverFactory { val program: SolvingEvaluator.this.program.type }
+ def getSolver(opts: OptionValue[_]*): SolverFactory {
+ val program: SolvingEvaluator.this.program.type
+ type S <: TimeoutSolver { val program: SolvingEvaluator.this.program.type }
+ }
private val chooseCache: MutableMap[Choose, Expr] = MutableMap.empty
private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 3af74feb6e2a68e3ccbfab5e856d082ad3f7f2cc..c02ac30a089c2fbdfeef42c6e4c0511d073ced1d 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -49,66 +49,68 @@ object SolverFactory {
def getFromName(name: String)
(p: Program, opts: Options)
(ev: DeterministicEvaluator with SolvingEvaluator { val program: p.type },
- enc: ProgramEncoder { val sourceProgram: p.type; val t: inox.trees.type }):
- SolverFactory { val program: p.type; type S <: TimeoutSolver } = name match {
- case "nativez3" => create(p)(name, () => new {
- val program: p.type = p
- val options = opts
- val encoder = enc
- } with z3.NativeZ3Solver with TimeoutSolver {
- val evaluator = ev
- })
-
- case "unrollz3" => create(p)(name, () => new {
- val program: p.type = p
- val options = opts
- val encoder = enc
- } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
- val evaluator = ev
+ enc: ast.ProgramEncoder { val sourceProgram: p.type; val t: inox.trees.type }):
+ SolverFactory { val program: p.type; type S <: TimeoutSolver { val program: p.type } } = {
+ name match {
+ case "nativez3" => create(p)(name, () => new {
+ val program: p.type = p
+ val options = opts
+ val encoder = enc
+ } with z3.NativeZ3Solver with TimeoutSolver {
+ val evaluator = ev
+ })
- object underlying extends {
- val program: targetProgram.type = targetProgram
+ case "unrollz3" => create(p)(name, () => new {
+ val program: p.type = p
val options = opts
- } with z3.UninterpretedZ3Solver
- })
+ val encoder = enc
+ } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
+ val evaluator = ev
- case "smt-cvc4" => create(p)(name, () => new {
- val program: p.type = p
- val options = opts
- val encoder = enc
- } with unrolling.UnrollingSolver with theories.CVC4Theories with TimeoutSolver {
- val evaluator = ev
+ object underlying extends {
+ val program: targetProgram.type = targetProgram
+ val options = opts
+ } with z3.UninterpretedZ3Solver
+ })
- object underlying extends {
- val program: targetProgram.type = targetProgram
+ case "smt-cvc4" => create(p)(name, () => new {
+ val program: p.type = p
val options = opts
- } with smtlib.CVC4Solver
- })
+ val encoder = enc
+ } with unrolling.UnrollingSolver with theories.CVC4Theories with TimeoutSolver {
+ val evaluator = ev
- case "smt-z3" => create(p)(name, () => new {
- val program: p.type = p
- val options = opts
- val encoder = enc
- } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
- val evaluator = ev
+ object underlying extends {
+ val program: targetProgram.type = targetProgram
+ val options = opts
+ } with smtlib.CVC4Solver
+ })
- object underlying extends {
- val program: targetProgram.type = targetProgram
+ case "smt-z3" => create(p)(name, () => new {
+ val program: p.type = p
val options = opts
- } with smtlib.Z3Solver
- })
+ val encoder = enc
+ } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
+ val evaluator = ev
- case "enum" => create(p)(name, () => new {
- val program: p.type = p
- val options = opts
- } with EnumerationSolver with TimeoutSolver {
- val evaluator = ev
- val grammars: GrammarsUniverse {val program: p.type} = new GrammarsUniverse {
- val program: p.type = p
- }
- })
+ object underlying extends {
+ val program: targetProgram.type = targetProgram
+ val options = opts
+ } with smtlib.Z3Solver
+ })
- case _ => throw FatalError("Unknown solver: " + name)
+ case "enum" => create(p)(name, () => new {
+ val program: p.type = p
+ val options = opts
+ } with EnumerationSolver with TimeoutSolver {
+ val evaluator = ev
+ val grammars: GrammarsUniverse {val program: p.type} = new GrammarsUniverse {
+ val program: p.type = p
+ }
+ })
+
+ case _ => throw FatalError("Unknown solver: " + name)
+ }
}
val solversPretty = "Available: " + solverNames.toSeq.sortBy(_._1).map {
@@ -117,20 +119,24 @@ object SolverFactory {
val solvers: Set[String] = solverNames.map(_._1).toSet
- def apply(name: String, p: InoxProgram, opts: Options):
- SolverFactory { val program: p.type; type S <: TimeoutSolver } = {
- getFromName(name)(p, opts)(RecursiveEvaluator(p, opts), ProgramEncoder.empty(p))
- }
-
- def apply(p: InoxProgram, opts: Options): SolverFactory { val program: p.type; type S <: TimeoutSolver } =
- opts.findOptionOrDefault(InoxOptions.optSelectedSolvers).toSeq match {
- case Seq() => throw FatalError("No selected solver")
- case Seq(single) => apply(single, p, opts)
- case multiple => PortfolioSolverFactory(p) {
- multiple.map(name => apply(name, p, opts))
- }
+ def apply(name: String, p: InoxProgram, opts: Options): SolverFactory {
+ val program: p.type
+ type S <: TimeoutSolver { val program: p.type }
+ } = getFromName(name)(p, opts)(RecursiveEvaluator(p, opts), ast.ProgramEncoder.empty(p))
+
+ def apply(p: InoxProgram, opts: Options): SolverFactory {
+ val program: p.type
+ type S <: TimeoutSolver { val program: p.type }
+ } = opts.findOptionOrDefault(InoxOptions.optSelectedSolvers).toSeq match {
+ case Seq() => throw FatalError("No selected solver")
+ case Seq(single) => apply(single, p, opts)
+ case multiple => PortfolioSolverFactory(p) {
+ multiple.map(name => apply(name, p, opts))
}
+ }
- def default(p: InoxProgram): SolverFactory { val program: p.type; type S <: TimeoutSolver } =
- apply(p, p.ctx.options)
+ def default(p: InoxProgram): SolverFactory {
+ val program: p.type
+ type S <: TimeoutSolver { val program: p.type }
+ } = apply(p, p.ctx.options)
}
diff --git a/src/main/scala/inox/solvers/combinators/EncodingSolver.scala b/src/main/scala/inox/solvers/combinators/EncodingSolver.scala
index 726cbe8c61138404c6976ff5fef9083ad952023f..c02e32927008aeb6065498a198a070761d18d73d 100644
--- a/src/main/scala/inox/solvers/combinators/EncodingSolver.scala
+++ b/src/main/scala/inox/solvers/combinators/EncodingSolver.scala
@@ -4,54 +4,37 @@ package inox
package solvers
package combinators
-import ast._
-
-trait ProgramEncoder extends TreeBijection {
- val sourceProgram: Program
- lazy val s: sourceProgram.trees.type = sourceProgram.trees
- lazy val targetProgram: Program { val trees: t.type } = sourceProgram.transform(encoder)
-
- /* @nv XXX: ideally, we would want to replace `>>` by `override def andThen`, however this
- * seems to break the scala compiler for some weird reason... */
- def >>(that: TreeBijection { val s: ProgramEncoder.this.t.type }): ProgramEncoder {
- val sourceProgram: ProgramEncoder.this.sourceProgram.type
- val t: that.t.type
- } = new ProgramEncoder {
- val sourceProgram: ProgramEncoder.this.sourceProgram.type = ProgramEncoder.this.sourceProgram
- val t: that.t.type = that.t
-
- val encoder = ProgramEncoder.this.encoder andThen that.encoder
- val decoder = that.decoder andThen ProgramEncoder.this.decoder
- }
-}
+trait EncodingSolver extends Solver {
+ import program.trees._
+ import SolverResponses._
-object ProgramEncoder {
- def empty(p: Program): ProgramEncoder {
- val sourceProgram: p.type
- val t: p.trees.type
- } = new ProgramEncoder {
- val sourceProgram: p.type = p
- val t: p.trees.type = p.trees
+ protected val encoder: ast.ProgramEncoder { val sourceProgram: program.type }
+ protected lazy val t: encoder.t.type = encoder.t
- object encoder extends p.trees.IdentitySymbolTransformer
- object decoder extends p.trees.IdentitySymbolTransformer
+ protected val underlying: Solver {
+ val program: encoder.targetProgram.type
}
-}
-trait EncodingSolver extends Solver {
- import program.trees._
+ lazy val name = "E:" + underlying.name
+ lazy val options = underlying.options
- protected val programEncoder: ProgramEncoder { val sourceProgram: program.type }
+ def assertCnstr(expr: Expr) = underlying.assertCnstr(encoder.encode(expr))
- protected def encode(vd: ValDef): programEncoder.t.ValDef = programEncoder.encode(vd)
- protected def decode(vd: programEncoder.t.ValDef): ValDef = programEncoder.decode(vd)
-
- protected def encode(v: Variable): programEncoder.t.Variable = programEncoder.encode(v)
- protected def decode(v: programEncoder.t.Variable): Variable = programEncoder.decode(v)
+ private def convert(config: Configuration)
+ (resp: config.Response[Map[t.ValDef, t.Expr], Set[t.Expr]]):
+ config.Response[Map[ValDef, Expr], Set[Expr]] = {
+ config.convert(resp,
+ (model: Map[t.ValDef, t.Expr]) => model.map(p => encoder.decode(p._1) -> encoder.decode(p._2)),
+ (assumptions: Set[t.Expr]) => assumptions.map(encoder.decode)
+ )
+ }
- protected def encode(e: Expr): programEncoder.t.Expr = programEncoder.encode(e)
- protected def decode(e: programEncoder.t.Expr): Expr = programEncoder.decode(e)
+ def check(config: CheckConfiguration) = convert(config)(underlying.check(config))
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]) =
+ convert(config)(underlying.checkAssumptions(config)(assumptions.map(encoder.encode)))
- protected def encode(tpe: Type): programEncoder.t.Type = programEncoder.encode(tpe)
- protected def decode(tpe: programEncoder.t.Type): Type = programEncoder.decode(tpe)
+ def free() = underlying.free()
+ def reset() = underlying.reset()
+ def push() = underlying.push()
+ def pop() = underlying.pop()
}
diff --git a/src/main/scala/inox/solvers/combinators/EncodingSolverFactory.scala b/src/main/scala/inox/solvers/combinators/EncodingSolverFactory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0c679eca0aef6dd3a341dc7202fa071905fa17c6
--- /dev/null
+++ b/src/main/scala/inox/solvers/combinators/EncodingSolverFactory.scala
@@ -0,0 +1,28 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+package combinators
+
+object EncodingSolverFactory {
+ def apply(p: Program)
+ (enc: ast.ProgramEncoder { val sourceProgram: p.type })
+ (sf: SolverFactory {
+ val program: enc.targetProgram.type
+ type S <: TimeoutSolver { val program: enc.targetProgram.type }
+ }): SolverFactory {
+ val program: p.type
+ type S <: TimeoutSolver { val program: p.type }
+ } = {
+
+ SolverFactory.create(p)("E:" + sf.name, () => new {
+ val program: p.type = p
+ } with EncodingSolver with TimeoutSolver {
+ val encoder: enc.type = enc
+ val underlying = sf.getNewSolver()
+
+ def interrupt() = underlying.interrupt()
+ def recoverInterrupt() = underlying.recoverInterrupt()
+ })
+ }
+}
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 57daddc41e257a3f5f6c4faa88b8e4524ba14fff..4aaa154b56bf050835b7c68dc1ef557aac809c3a 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -21,7 +21,7 @@ object optFeelingLucky extends FlagOptionDef(
object optUnrollAssumptions extends FlagOptionDef(
"unrollassumptions", "Use unsat-assumptions to drive unfolding while remaining fair", false)
-trait AbstractUnrollingSolver extends Solver with EncodingSolver {
+trait AbstractUnrollingSolver extends Solver {
import program._
import program.trees._
@@ -30,7 +30,7 @@ trait AbstractUnrollingSolver extends Solver with EncodingSolver {
protected type Encoded
- protected val encoder: ProgramEncoder { val sourceProgram: program.type }
+ protected val encoder: ast.ProgramEncoder { val sourceProgram: program.type }
protected val theories: TheoryEncoder { val sourceProgram: AbstractUnrollingSolver.this.encoder.targetProgram.type }
@@ -40,8 +40,19 @@ trait AbstractUnrollingSolver extends Solver with EncodingSolver {
protected lazy val t: programEncoder.t.type = programEncoder.t
protected lazy val targetProgram: programEncoder.targetProgram.type = programEncoder.targetProgram
- protected def encode(tpe: FunctionType): t.FunctionType =
- programEncoder.encode(tpe).asInstanceOf[t.FunctionType]
+ protected final def encode(vd: ValDef): t.ValDef = programEncoder.encode(vd)
+ protected final def decode(vd: t.ValDef): ValDef = programEncoder.decode(vd)
+
+ protected final def encode(v: Variable): t.Variable = programEncoder.encode(v)
+ protected final def decode(v: t.Variable): Variable = programEncoder.decode(v)
+
+ protected final def encode(e: Expr): t.Expr = programEncoder.encode(e)
+ protected final def decode(e: t.Expr): Expr = programEncoder.decode(e)
+
+ protected final def encode(tpe: Type): t.Type = programEncoder.encode(tpe)
+ protected final def decode(tpe: t.Type): Type = programEncoder.decode(tpe)
+ protected final def encode(ft: FunctionType): t.FunctionType =
+ programEncoder.encode(ft).asInstanceOf[t.FunctionType]
protected val templates: Templates {
val program: targetProgram.type
diff --git a/src/main/scala/inox/transformers/Collector.scala b/src/main/scala/inox/transformers/Collector.scala
index 0da53d7668477d58d048443fa3ee0ea794f83a4f..191e3c73ad8bd1e22b85f83a81cfba881beff199 100644
--- a/src/main/scala/inox/transformers/Collector.scala
+++ b/src/main/scala/inox/transformers/Collector.scala
@@ -21,13 +21,16 @@ trait Collector extends Transformer {
super.rec(e, current)
}
- /** Traverses the expression and collects */
- final def collect(e: Expr): List[Result] = {
+ /** Traverses an [[Expr]] with the specified environment and collects */
+ final def collect(e: Expr, init: Env) = {
results = Nil
- transform(e)
+ transform(e, init)
results
}
+ /** Traverses an [[Expr]] with the initial environment and collects */
+ final def collect(e: Expr): List[Result] = collect(e, initEnv)
+
/** Collect the expressions in a [[FunDef]]'s body */
final def collect(fd: FunDef): List[Result] = collect(fd.fullBody)
}