From f18e636a77a7380e3d4add1f15bcbb2b199ff123 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 8 Aug 2016 11:45:51 +0200
Subject: [PATCH] Better default constructors, added default trees
---
src/main/scala/inox/InoxContext.scala | 4 +-
src/main/scala/inox/InoxOptions.scala | 16 +++-
.../scala/inox/datagen/ModelEnumerator.scala | 17 +++--
.../scala/inox/datagen/SolverDataGen.scala | 9 ++-
.../scala/inox/evaluators/Evaluator.scala | 8 +-
.../inox/evaluators/RecursiveEvaluator.scala | 11 +--
src/main/scala/inox/package.scala | 53 +++++++++++--
.../scala/inox/solvers/GroundSolver.scala | 74 -------------------
.../inox/solvers/NaiveAssumptionSolver.scala | 26 -------
src/main/scala/inox/solvers/Solver.scala | 12 ++-
.../scala/inox/solvers/SolverFactory.scala | 7 +-
11 files changed, 105 insertions(+), 132 deletions(-)
delete mode 100644 src/main/scala/inox/solvers/GroundSolver.scala
delete mode 100644 src/main/scala/inox/solvers/NaiveAssumptionSolver.scala
diff --git a/src/main/scala/inox/InoxContext.scala b/src/main/scala/inox/InoxContext.scala
index f029a985b..fa4910284 100644
--- a/src/main/scala/inox/InoxContext.scala
+++ b/src/main/scala/inox/InoxContext.scala
@@ -12,7 +12,9 @@ case class InoxContext(
reporter: Reporter,
interruptManager: InterruptManager,
options: Seq[InoxOption[Any]] = Seq(),
- timers: TimerStorage = new TimerStorage) extends InoxOptions {
+ timers: TimerStorage = new TimerStorage) extends InoxOptions[InoxContext] {
+
+ def build(opts: Seq[InoxOption[Any]]) = InoxContext(reporter, interruptManager, opts, timers)
def toSolver: solvers.SolverOptions = ???
def toEvaluator: evaluators.EvaluatorOptions = ???
diff --git a/src/main/scala/inox/InoxOptions.scala b/src/main/scala/inox/InoxOptions.scala
index 4ae72dcda..151a60ba9 100644
--- a/src/main/scala/inox/InoxOptions.scala
+++ b/src/main/scala/inox/InoxOptions.scala
@@ -154,14 +154,28 @@ object OptionsHelpers {
}
}
-trait InoxOptions {
+trait InoxOptions[Self <: InoxOptions[Self]] {
val options: Seq[InoxOption[Any]]
+ protected def build(newOpts: Seq[InoxOption[Any]]): Self
+
def findOption[A: ClassTag](optDef: InoxOptionDef[A]): Option[A] = options.collectFirst {
case InoxOption(`optDef`, value: A) => value
}
def findOptionOrDefault[A: ClassTag](optDef: InoxOptionDef[A]): A = findOption(optDef).getOrElse(optDef.default)
+
+ def +(newOpt: InoxOption[Any]): Self = build {
+ options.filter(_.optionDef != newOpt.optionDef) :+ newOpt
+ }
+
+ def ++(newOpts: Seq[InoxOption[Any]]): Self = build {
+ val defs = newOpts.map(_.optionDef).toSet
+ options.filter(opt => !defs(opt.optionDef)) ++ newOpts
+ }
+
+ @inline
+ def ++(that: Self): Self = this ++ that.options
}
object InoxOptions {
diff --git a/src/main/scala/inox/datagen/ModelEnumerator.scala b/src/main/scala/inox/datagen/ModelEnumerator.scala
index 636ff3c16..6cfbc50d8 100644
--- a/src/main/scala/inox/datagen/ModelEnumerator.scala
+++ b/src/main/scala/inox/datagen/ModelEnumerator.scala
@@ -8,17 +8,16 @@ import solvers._
import utils._
trait ModelEnumerator {
- val factory: SolverFactory
- lazy val program: factory.program.type = factory.program
+ val program: Program
+ val factory: SolverFactory { val program: ModelEnumerator.this.program.type }
+ val evaluator: DeterministicEvaluator { val program: ModelEnumerator.this.program.type }
+
import program._
import program.trees._
import program.symbols._
import SolverResponses._
- protected val evaluator: RecursiveEvaluator { val program: ModelEnumerator.this.program.type } =
- RecursiveEvaluator(program)(ctx.toEvaluator, ctx.toSolver)
-
def enumSimple(vs: Seq[ValDef], satisfying: Expr): FreeableIterator[Map[ValDef, Expr]] = {
enumVarying0(vs, satisfying, None, -1)
}
@@ -203,7 +202,11 @@ trait ModelEnumerator {
}
object ModelEnumerator {
- def apply(sf: SolverFactory): ModelEnumerator { val factory: sf.type } = new ModelEnumerator {
+ def apply(p: Program)
+ (sf: SolverFactory { val program: p.type }, ev: DeterministicEvaluator { val program: p.type }):
+ ModelEnumerator { val program: p.type; val factory: sf.type; val evaluator: ev.type } = new {
+ val program: p.type = p
val factory: sf.type = sf
- }
+ val evaluator: ev.type = ev
+ } with ModelEnumerator
}
diff --git a/src/main/scala/inox/datagen/SolverDataGen.scala b/src/main/scala/inox/datagen/SolverDataGen.scala
index 072ec731d..9a530c88b 100644
--- a/src/main/scala/inox/datagen/SolverDataGen.scala
+++ b/src/main/scala/inox/datagen/SolverDataGen.scala
@@ -3,6 +3,7 @@
package inox
package datagen
+import evaluators._
import solvers._
import utils._
@@ -12,6 +13,7 @@ trait SolverDataGen extends DataGenerator { self =>
import program.symbols._
def factory(p: Program { val trees: self.program.trees.type }): SolverFactory { val program: p.type }
+ def evaluator(p: Program { val trees: self.program.trees.type }): DeterministicEvaluator { val program: p.type }
def generate(tpe: Type): FreeableIterator[Expr] = {
generateFor(Seq(ValDef(FreshIdentifier("tmp"), tpe)),
@@ -76,7 +78,7 @@ trait SolverDataGen extends DataGenerator { self =>
// We need to synthesize a size function for ins' types.
val pgm1 = program.extend(functions = fds)
- val modelEnum = ModelEnumerator(factory(pgm1))
+ val modelEnum = ModelEnumerator(pgm1)(factory(pgm1), evaluator(pgm1))
val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
@@ -86,8 +88,9 @@ trait SolverDataGen extends DataGenerator { self =>
}
object SolverDataGen {
- def apply(p: Program): SolverDataGen { val program: p.type } = new SolverDataGen {
+ def apply(p: InoxProgram): SolverDataGen { val program: p.type } = new SolverDataGen {
val program: p.type = p
- def factory(p2: Program { val trees: p.trees.type }): SolverFactory { val program: p2.type } = SolverFactory(p2)
+ def factory(p: InoxProgram): SolverFactory { val program: p.type } = SolverFactory.default(p)
+ def evaluator(p: InoxProgram): RecursiveEvaluator { val program: p.type } = RecursiveEvaluator.default(p)
}
}
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index b9069f65f..c7f271d27 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -3,7 +3,13 @@
package inox
package evaluators
-case class EvaluatorOptions(options: Seq[InoxOption[Any]]) extends InoxOptions
+case class EvaluatorOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[EvaluatorOptions] {
+ protected def build(opts: Seq[InoxOption[Any]]): EvaluatorOptions = EvaluatorOptions(opts)
+}
+
+object EvaluatorOptions {
+ def empty = EvaluatorOptions(Seq())
+}
trait Evaluator {
val program: Program
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index c9f4da8f0..66d4d3e1e 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -529,15 +529,16 @@ trait RecursiveEvaluator
}
object RecursiveEvaluator {
- def apply(p: Program)
- (evOpts: EvaluatorOptions, solverOpts: solvers.SolverOptions):
- RecursiveEvaluator { val program: p.type } = {
+ def apply(p: InoxProgram)(evOpts: EvaluatorOptions, solverOpts: solvers.SolverOptions):
+ RecursiveEvaluator { val program: p.type } = {
new {
val program: p.type = p
} with RecursiveEvaluator with HasDefaultGlobalContext with HasDefaultRecContext {
- val options = evOpts
+ val options = p.ctx.toEvaluator ++ evOpts
val maxSteps = 50000
- def getSolver(opts: InoxOption[Any]*) = solvers.SolverFactory(p)
+ def getSolver(opts: InoxOption[Any]*) = solvers.SolverFactory(p)(p.ctx.toSolver ++ opts, options)
}
}
+
+ def default(p: InoxProgram) = apply(p)(EvaluatorOptions.empty, solvers.SolverOptions.empty)
}
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index ed98affad..a35924d04 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -1,15 +1,56 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-import scala.language.implicitConversions
-
-/** Core package of the Leon system
- *
- * Provides the basic types and definitions for the Leon system.
- */
+/** Core package of the Inox solving interface */
package object inox {
implicit class BooleanToOption(cond: Boolean) {
def option[A](v: => A) = if (cond) Some(v) else None
}
case class FatalError(msg: String) extends Exception(msg)
+
+ type InoxProgram = Program { val trees: inox.trees.type }
+
+ object InoxProgram {
+ def apply(ictx: InoxContext,
+ functions: Seq[inox.trees.FunDef],
+ classes: Seq[inox.trees.ClassDef]) = new Program {
+ val trees = inox.trees
+ val ctx = ictx
+ val symbols = new inox.trees.Symbols(
+ functions.map(fd => fd.id -> fd).toMap,
+ classes.map(cd => cd.id -> cd).toMap)
+ }
+ }
+
+ object trees extends ast.Trees {
+
+ class Symbols(
+ val functions: Map[Identifier, FunDef],
+ val classes: Map[Identifier, ClassDef]
+ ) extends AbstractSymbols {
+
+ def transform(t: TreeTransformer) = new Symbols(
+ functions.mapValues(fd => new FunDef(
+ fd.id,
+ fd.tparams, // type parameters can't be transformed!
+ fd.params.map(vd => t.transform(vd)),
+ t.transform(fd.returnType),
+ fd.body.map(t.transform),
+ fd.flags)),
+ classes.mapValues {
+ case acd: AbstractClassDef => acd
+ case ccd: CaseClassDef => new CaseClassDef(
+ ccd.id,
+ ccd.tparams,
+ ccd.parent,
+ ccd.fields.map(t.transform),
+ ccd.flags)
+ })
+
+ def extend(functions: Seq[FunDef] = Seq.empty, classes: Seq[ClassDef] = Seq.empty) = new Symbols(
+ this.functions ++ functions.map(fd => fd.id -> fd),
+ this.classes ++ classes.map(cd => cd.id -> cd)
+ )
+ }
+ }
}
diff --git a/src/main/scala/inox/solvers/GroundSolver.scala b/src/main/scala/inox/solvers/GroundSolver.scala
deleted file mode 100644
index a50b3f814..000000000
--- a/src/main/scala/inox/solvers/GroundSolver.scala
+++ /dev/null
@@ -1,74 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import evaluators.DefaultEvaluator
-import evaluators.EvaluationResults._
-import purescala.Common.Identifier
-import purescala.Definitions.Program
-import purescala.Expressions.{BooleanLiteral, Expr}
-import purescala.ExprOps.isGround
-import purescala.Constructors.andJoin
-import utils.Interruptible
-import utils.IncrementalSeq
-
-// This solver only "solves" ground terms by evaluating them
-class GroundSolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
-
- context.interruptManager.registerForInterrupts(this)
-
- val evaluator = new DefaultEvaluator(context, program)
- val dbg: Any => Unit = context.reporter.debug(_)
-
- def name: String = "ground"
-
- private val assertions = new IncrementalSeq[Expr]()
-
- // Ground terms will always have the empty model
- def getModel: Model = Model.empty
-
- def assertCnstr(expression: Expr): Unit = {
- assertions += expression
- }
-
- def check: Option[Boolean] = {
- val expr = andJoin(assertions.toSeq)
-
- if (isGround(expr)) {
- evaluator.eval(expr) match {
- case Successful(BooleanLiteral(result)) =>
- Some(result)
- case RuntimeError(message) =>
- dbg(s"Evaluation of $expr resulted in runtime error")
- Some(false)
- case _ =>
- dbg(s"Solver $name encountered error during evaluation.")
- None
- }
- } else {
- dbg(s"Non-ground expression $expr given to solver $name")
- None
- }
- }
-
- def free(): Unit = {
- assertions.clear()
- }
-
- def push() = {
- assertions.push()
- }
-
- def pop() = {
- assertions.pop()
- }
-
- def reset() = {
- assertions.reset()
- }
-
- def interrupt(): Unit = {}
-
- def recoverInterrupt(): Unit = {}
-}
diff --git a/src/main/scala/inox/solvers/NaiveAssumptionSolver.scala b/src/main/scala/inox/solvers/NaiveAssumptionSolver.scala
deleted file mode 100644
index a0dd48a7c..000000000
--- a/src/main/scala/inox/solvers/NaiveAssumptionSolver.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Expressions._
-import purescala.Constructors._
-
-trait NaiveAssumptionSolver {
- self: Solver =>
-
- var lastBs = Set[Expr]()
- def checkAssumptions(bs: Set[Expr]): Option[Boolean] = {
- push()
- lastBs = bs
- assertCnstr(andJoin(bs.toSeq))
- val res = check
- pop()
-
- res
- }
-
- def getUnsatCore: Set[Expr] = {
- lastBs
- }
-}
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index e72533148..5b71c1854 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -6,14 +6,12 @@ package solvers
import utils._
import evaluators._
-case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions {
- def set(opts: Seq[InoxOption[Any]]): SolverOptions = {
- val changed = opts.map(_.optionDef).toSet
- val remainingOpts = options.filter { case InoxOption(optDef, _) => !changed(optDef) }
- copy(options = remainingOpts ++ opts)
- }
+case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[SolverOptions] {
+ def build(opts: Seq[InoxOption[Any]]): SolverOptions = SolverOptions(opts)
+}
- def set(opt: InoxOption[Any], opts: InoxOption[Any]*): SolverOptions = set(opt +: opts)
+object SolverOptions {
+ def empty = SolverOptions(Seq())
}
case object DebugSectionSolver extends DebugSection("solver")
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 6ef8140ac..d15218683 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -33,5 +33,10 @@ object SolverFactory {
}
}
- def apply(p: Program): SolverFactory { val program: p.type } = ???
+ def apply(p: InoxProgram)
+ (solverOpts: SolverOptions, evOpts: evaluators.EvaluatorOptions):
+ SolverFactory { val program: p.type } = ???
+
+ def default(p: InoxProgram): SolverFactory { val program: p.type } =
+ apply(p)(SolverOptions.empty, evaluators.EvaluatorOptions.empty)
}
--
GitLab