From 0b108395d330aa459ba55b6ecfbeea13717d7e80 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 6 Aug 2016 14:40:47 +0200
Subject: [PATCH] Finished up SolverDataGen
---
src/main/scala/inox/InoxContext.scala | 6 +-
src/main/scala/inox/Program.scala | 2 +-
src/main/scala/inox/ast/Definitions.scala | 3 +
.../scala/inox/datagen/DataGenerator.scala | 2 +-
.../scala/inox/datagen/ModelEnumerator.scala | 97 ++++++++++---------
.../scala/inox/datagen/SolverDataGen.scala | 23 +++--
.../scala/inox/evaluators/Evaluator.scala | 2 -
.../inox/evaluators/RecursiveEvaluator.scala | 14 ++-
.../inox/evaluators/SolvingEvaluator.scala | 14 +--
.../scala/inox/grammars/AllGrammars.scala | 4 +-
.../inox/grammars/GrammarsUniverse.scala | 20 ++--
.../scala/inox/solvers/SimpleSolverAPI.scala | 5 +-
.../scala/inox/solvers/SolverFactory.scala | 4 +-
13 files changed, 112 insertions(+), 84 deletions(-)
diff --git a/src/main/scala/inox/InoxContext.scala b/src/main/scala/inox/InoxContext.scala
index 6abc7d3e1..f029a985b 100644
--- a/src/main/scala/inox/InoxContext.scala
+++ b/src/main/scala/inox/InoxContext.scala
@@ -12,7 +12,11 @@ case class InoxContext(
reporter: Reporter,
interruptManager: InterruptManager,
options: Seq[InoxOption[Any]] = Seq(),
- timers: TimerStorage = new TimerStorage) extends InoxOptions
+ timers: TimerStorage = new TimerStorage) extends InoxOptions {
+
+ def toSolver: solvers.SolverOptions = ???
+ def toEvaluator: evaluators.EvaluatorOptions = ???
+}
object InoxContext {
def empty = {
diff --git a/src/main/scala/inox/Program.scala b/src/main/scala/inox/Program.scala
index 549c4b22b..7c978b1ca 100644
--- a/src/main/scala/inox/Program.scala
+++ b/src/main/scala/inox/Program.scala
@@ -18,7 +18,7 @@ trait Program {
val ctx = Program.this.ctx
}
- def extend(functions: Seq[FunDef] = Seq.empty, classes: Seq[ClassDef] = Seq.empty):
+ def extend(functions: Seq[trees.FunDef] = Seq.empty, classes: Seq[trees.ClassDef] = Seq.empty):
Program { val trees: Program.this.trees.type } = new Program {
val trees: Program.this.trees.type = Program.this.trees
val symbols = Program.this.symbols.extend(functions, classes)
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 625136266..e29fa2762 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -47,6 +47,9 @@ trait Definitions { self: Trees =>
override def hashCode: Int = 61 * id.hashCode + tpe.hashCode
}
+ implicit def variableSymbolOrdering[VS <: VariableSymbol]: Ordering[VS] =
+ Ordering.by(e => e.id)
+
sealed abstract class VariableConverter[B <: VariableSymbol] {
def convert(a: VariableSymbol): B
}
diff --git a/src/main/scala/inox/datagen/DataGenerator.scala b/src/main/scala/inox/datagen/DataGenerator.scala
index 1b5583fdf..d8a80bed6 100644
--- a/src/main/scala/inox/datagen/DataGenerator.scala
+++ b/src/main/scala/inox/datagen/DataGenerator.scala
@@ -15,7 +15,7 @@ trait DataGenerator extends Interruptible {
implicit val debugSection = DebugSectionDataGen
- def generateFor(ins: Seq[Variable], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]]
+ def generateFor(ins: Seq[ValDef], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]]
protected val interrupted: AtomicBoolean = new AtomicBoolean(false)
diff --git a/src/main/scala/inox/datagen/ModelEnumerator.scala b/src/main/scala/inox/datagen/ModelEnumerator.scala
index 3d433936d..636ff3c16 100644
--- a/src/main/scala/inox/datagen/ModelEnumerator.scala
+++ b/src/main/scala/inox/datagen/ModelEnumerator.scala
@@ -5,17 +5,21 @@ package datagen
import evaluators._
import solvers._
+import utils._
-class ModelEnumerator(factory: SolverFactory[Solver]) {
- val program: factory.program.type = factory.program
+trait ModelEnumerator {
+ val factory: SolverFactory
+ lazy val program: factory.program.type = factory.program
import program._
import program.trees._
import program.symbols._
+ import SolverResponses._
+
protected val evaluator: RecursiveEvaluator { val program: ModelEnumerator.this.program.type } =
- RecursiveEvaluator(program)
+ RecursiveEvaluator(program)(ctx.toEvaluator, ctx.toSolver)
- def enumSimple(vs: Seq[Variable], satisfying: Expr): FreeableIterator[Map[Variable, Expr]] = {
+ def enumSimple(vs: Seq[ValDef], satisfying: Expr): FreeableIterator[Map[ValDef, Expr]] = {
enumVarying0(vs, satisfying, None, -1)
}
@@ -26,52 +30,53 @@ class ModelEnumerator(factory: SolverFactory[Solver]) {
* Note: there is no guarantee that the models enumerated consecutively share the
* same `caracteristic`.
*/
- def enumVarying(ids: Seq[Identifier], satisfying: Expr, measure: Expr, nPerMeasure: Int = 1) = {
- enumVarying0(ids, satisfying, Some(measure), nPerMeasure)
+ def enumVarying(vs: Seq[ValDef], satisfying: Expr, measure: Expr, nPerMeasure: Int = 1) = {
+ enumVarying0(vs, satisfying, Some(measure), nPerMeasure)
}
- private[this] def enumVarying0(ids: Seq[Identifier], satisfying: Expr, measure: Option[Expr], nPerMeasure: Int = 1): FreeableIterator[Map[Identifier, Expr]] = {
+ private[this] def enumVarying0(vs: Seq[ValDef], satisfying: Expr, measure: Option[Expr], nPerMeasure: Int = 1): FreeableIterator[Map[ValDef, Expr]] = {
val s = factory.getNewSolver
s.assertCnstr(satisfying)
val m = measure match {
case Some(ms) =>
- val m = FreshIdentifier("measure", ms.getType)
- s.assertCnstr(Equals(m.toVariable, ms))
+ val m = Variable(FreshIdentifier("measure"), ms.getType)
+ s.assertCnstr(Equals(m, ms))
m
case None =>
- FreshIdentifier("noop", BooleanType)
+ Variable(FreshIdentifier("noop"), BooleanType)
}
var perMeasureRem = Map[Expr, Int]().withDefaultValue(nPerMeasure)
- new FreeableIterator[Map[Identifier, Expr]] {
+ new FreeableIterator[Map[ValDef, Expr]] {
def computeNext() = {
- s.check match {
- case Some(true) =>
- val model = s.getModel
- val idsModel = ids.map { id =>
- id -> model.getOrElse(id, simplestValue(id.getType))
+ s.check(Model) match {
+ case SatWithModel(model) =>
+ val fullModel = vs.map { v =>
+ v -> model.getOrElse(v, simplestValue(v.getType))
}.toMap
// Vary the model
- s.assertCnstr(not(andJoin(idsModel.toSeq.sortBy(_._1).map { case (k, v) => equality(k.toVariable, v) })))
+ s.assertCnstr(not(andJoin(fullModel.toSeq.sortBy(_._1).map {
+ case (k, v) => equality(k.toVariable, v)
+ })))
measure match {
case Some(ms) =>
- val mValue = evaluator.eval(ms, idsModel).result.get
+ val mValue = evaluator.eval(ms, fullModel).result.get
perMeasureRem += (mValue -> (perMeasureRem(mValue) - 1))
if (perMeasureRem(mValue) <= 0) {
- s.assertCnstr(not(equality(m.toVariable, mValue)))
+ s.assertCnstr(not(equality(m, mValue)))
}
case None =>
}
- Some(idsModel)
+ Some(fullModel)
case _ =>
None
@@ -84,27 +89,27 @@ class ModelEnumerator(factory: SolverFactory[Solver]) {
}
}
- def enumMinimizing(ids: Seq[Identifier], cnstr: Expr, measure: Expr) = {
- enumOptimizing(ids, cnstr, measure, Down)
+ def enumMinimizing(vs: Seq[ValDef], cnstr: Expr, measure: Expr) = {
+ enumOptimizing(vs, cnstr, measure, Down)
}
- def enumMaximizing(ids: Seq[Identifier], cnstr: Expr, measure: Expr) = {
- enumOptimizing(ids, cnstr, measure, Up)
+ def enumMaximizing(vs: Seq[ValDef], cnstr: Expr, measure: Expr) = {
+ enumOptimizing(vs, cnstr, measure, Up)
}
abstract class SearchDirection
case object Up extends SearchDirection
case object Down extends SearchDirection
- private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): FreeableIterator[Map[Identifier, Expr]] = {
+ private[this] def enumOptimizing(vs: Seq[ValDef], satisfying: Expr, measure: Expr, dir: SearchDirection): FreeableIterator[Map[ValDef, Expr]] = {
assert(measure.getType == IntegerType)
- val s = sf.getNewSolver
+ val s = factory.getNewSolver
s.assertCnstr(satisfying)
- val mId = FreshIdentifier("measure", measure.getType)
- s.assertCnstr(Equals(mId.toVariable, measure))
+ val m = Variable(FreshIdentifier("measure"), measure.getType)
+ s.assertCnstr(Equals(m, measure))
// Search Range
var ub: Option[BigInt] = None
@@ -130,8 +135,8 @@ class ModelEnumerator(factory: SolverFactory[Solver]) {
case _ => None
}
- new FreeableIterator[Map[Identifier, Expr]] {
- def computeNext(): Option[Map[Identifier, Expr]] = {
+ new FreeableIterator[Map[ValDef, Expr]] {
+ def computeNext(): Option[Map[ValDef, Expr]] = {
if (rangeEmpty()) {
None
} else {
@@ -140,37 +145,35 @@ class ModelEnumerator(factory: SolverFactory[Solver]) {
s.push()
dir match {
case Up =>
- s.assertCnstr(GreaterThan(mId.toVariable, InfiniteIntegerLiteral(t)))
+ s.assertCnstr(GreaterThan(m, IntegerLiteral(t)))
case Down =>
- s.assertCnstr(LessThan(mId.toVariable, InfiniteIntegerLiteral(t)))
+ s.assertCnstr(LessThan(m, IntegerLiteral(t)))
}
t
}
- s.check match {
- case Some(true) =>
- val sm = s.getModel
- val m = ids.map { id =>
- id -> sm.getOrElse(id, simplestValue(id.getType))
+ s.check(Model) match {
+ case SatWithModel(model) =>
+ val fullModel = vs.map { v =>
+ v -> model.getOrElse(v, simplestValue(v.getType))
}.toMap
- evaluator.eval(measure, m).result match {
- case Some(InfiniteIntegerLiteral(measureVal)) =>
+ evaluator.eval(measure, fullModel).result match {
+ case Some(IntegerLiteral(measureVal)) =>
// Positive result
dir match {
case Up => lb = Some(measureVal)
case Down => ub = Some(measureVal)
}
- Some(m)
+ Some(fullModel)
case _ =>
ctx.reporter.warning("Evaluator failed to evaluate measure!")
None
}
-
- case Some(false) =>
+ case Unsat =>
// Negative result
thisTry match {
case Some(t) =>
@@ -186,15 +189,21 @@ class ModelEnumerator(factory: SolverFactory[Solver]) {
None
}
- case None =>
+ case Unknown =>
None
}
}
}
def free() {
- sf.reclaim(s)
+ factory.reclaim(s)
}
}
}
}
+
+object ModelEnumerator {
+ def apply(sf: SolverFactory): ModelEnumerator { val factory: sf.type } = new ModelEnumerator {
+ val factory: sf.type = sf
+ }
+}
diff --git a/src/main/scala/inox/datagen/SolverDataGen.scala b/src/main/scala/inox/datagen/SolverDataGen.scala
index f3eff883b..072ec731d 100644
--- a/src/main/scala/inox/datagen/SolverDataGen.scala
+++ b/src/main/scala/inox/datagen/SolverDataGen.scala
@@ -6,19 +6,19 @@ package datagen
import solvers._
import utils._
-trait SolverDataGen extends DataGenerator {
+trait SolverDataGen extends DataGenerator { self =>
import program._
import program.trees._
import program.symbols._
- def factory(p: Program): SolverFactory { val program: p.type }
+ def factory(p: Program { val trees: self.program.trees.type }): SolverFactory { val program: p.type }
def generate(tpe: Type): FreeableIterator[Expr] = {
- generateFor(Seq(Variable(FreshIdentifier("tmp"), tpe)),
+ generateFor(Seq(ValDef(FreshIdentifier("tmp"), tpe)),
BooleanLiteral(true), 20, 20).map(_.head).takeWhile(_ => !interrupted.get)
}
- def generateFor(ins: Seq[Variable], satisfying: Expr, maxValid: Int, maxEnumerated: Int): FreeableIterator[Seq[Expr]] = {
+ def generateFor(ins: Seq[ValDef], satisfying: Expr, maxValid: Int, maxEnumerated: Int): FreeableIterator[Seq[Expr]] = {
if (ins.isEmpty) {
FreeableIterator.empty
} else {
@@ -31,6 +31,8 @@ trait SolverDataGen extends DataGenerator {
val tcd = ct.tcd
val root = tcd.cd.root
val id = cdToId.getOrElse(root, {
+ import dsl._
+
val id = FreshIdentifier("sizeOf", true)
val tparams = root.tparams.map(_.freshen)
cdToId += root -> id
@@ -41,7 +43,6 @@ trait SolverDataGen extends DataGenerator {
plus(i, sizeFor(expr.getField(f.id)))
}
- import dsl._
val x = Variable(FreshIdentifier("x", true), tcd.root.toType)
fds +:= new FunDef(id, tparams, Seq(x.toVal), IntegerType, Some(root match {
case acd: AbstractClassDef =>
@@ -54,6 +55,8 @@ trait SolverDataGen extends DataGenerator {
case ccd: CaseClassDef =>
sizeOfCaseClass(ccd, x)
}), Set.empty)
+
+ id
})
FunctionInvocation(id, ct.tps, Seq(of))
@@ -69,16 +72,22 @@ trait SolverDataGen extends DataGenerator {
IntegerLiteral(1)
}
- val sizeOf = sizeFor(tupleWrap(ins))
+ val sizeOf = sizeFor(tupleWrap(ins.map(_.toVariable)))
// We need to synthesize a size function for ins' types.
val pgm1 = program.extend(functions = fds)
- val modelEnum = new ModelEnumerator(factory(pgm1))
+ val modelEnum = ModelEnumerator(factory(pgm1))
val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
enum.take(maxValid).map(model => ins.map(model)).takeWhile(_ => !interrupted.get)
}
}
+}
+object SolverDataGen {
+ def apply(p: Program): 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)
+ }
}
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index ab9166748..b9069f65f 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -5,8 +5,6 @@ package evaluators
case class EvaluatorOptions(options: Seq[InoxOption[Any]]) extends InoxOptions
-
-
trait Evaluator {
val program: Program
val options: EvaluatorOptions
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index c62f0cff8..c9f4da8f0 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -529,9 +529,15 @@ trait RecursiveEvaluator
}
object RecursiveEvaluator {
- def apply(p: Program)(opts: EvaluatorOptions): RecursiveEvaluator { val program: p.type } = new {
- val program: p.type = p
- } with RecursiveEvaluator with HasDefaultGlobalContext with HasDefaultRecContext {
- val maxSteps = 50000
+ def apply(p: Program)
+ (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 maxSteps = 50000
+ def getSolver(opts: InoxOption[Any]*) = solvers.SolverFactory(p)
+ }
}
}
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 09a479e94..6b84839cf 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -20,7 +20,7 @@ trait SolvingEvaluator extends Evaluator {
def default = MutableMap.empty
}
- def getSolver(opts: InoxOption[Any]*): Solver { val program: SolvingEvaluator.this.program.type }
+ def getSolver(opts: InoxOption[Any]*): SolverFactory { val program: SolvingEvaluator.this.program.type }
private val specCache: MutableMap[Expr, Expr] = MutableMap.empty
private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
@@ -29,14 +29,14 @@ trait SolvingEvaluator extends Evaluator {
val Lambda(Seq(vd), body) = specs
val timer = ctx.timers.evaluators.specs.start()
- val solver = getSolver(options.options.collect {
+ val sf = getSolver(options.options.collect {
case o @ InoxOption(opt, _) if opt == optForallCache => o
}.toSeq : _*)
import SolverResponses._
- solver.assertCnstr(body)
- val res = solver.check(Model)
+ val api = SimpleSolverAPI(sf)
+ val res = api.solveSAT(body)
timer.stop()
res match {
@@ -56,7 +56,7 @@ trait SolvingEvaluator extends Evaluator {
BooleanLiteral(cache.getOrElse(forall, {
val timer = ctx.timers.evaluators.forall.start()
- val solver = getSolver(
+ val sf = getSolver(
InoxOption(optSilentErrors)(true),
InoxOption(optCheckModels)(false),
InoxOption(optForallCache)(cache)
@@ -64,8 +64,8 @@ trait SolvingEvaluator extends Evaluator {
import SolverResponses._
- solver.assertCnstr(Not(forall.body))
- val res = solver.check(Model)
+ val api = SimpleSolverAPI(sf)
+ val res = api.solveSAT(Not(forall.body))
timer.stop()
res match {
diff --git a/src/main/scala/inox/grammars/AllGrammars.scala b/src/main/scala/inox/grammars/AllGrammars.scala
index 265892bfb..d999404ac 100644
--- a/src/main/scala/inox/grammars/AllGrammars.scala
+++ b/src/main/scala/inox/grammars/AllGrammars.scala
@@ -6,6 +6,6 @@ trait AllGrammars extends ElementaryGrammars
with ConstantGrammars
with ClosureGrammars
with EqualityGrammars
- with FunctionCallsGrammars
-{ self: GrammarsUniverse =>
+ with FunctionCallsGrammars {
+ self: GrammarsUniverse =>
}
diff --git a/src/main/scala/inox/grammars/GrammarsUniverse.scala b/src/main/scala/inox/grammars/GrammarsUniverse.scala
index 74971a28e..961452010 100644
--- a/src/main/scala/inox/grammars/GrammarsUniverse.scala
+++ b/src/main/scala/inox/grammars/GrammarsUniverse.scala
@@ -1,15 +1,15 @@
package inox
package grammars
-trait GrammarsUniverse extends Tags
- with Productions
- with Aspects
- with aspects.PersistentAspects
- with aspects.AllAspects
- with Labels
- with ExpressionGrammars
- with SimpleExpressionGrammars
- with AllGrammars
-{
+trait GrammarsUniverse
+ extends Tags
+ with Productions
+ with Aspects
+ with aspects.PersistentAspects
+ with aspects.AllAspects
+ with Labels
+ with ExpressionGrammars
+ with SimpleExpressionGrammars
+ with AllGrammars {
val program: Program
}
diff --git a/src/main/scala/inox/solvers/SimpleSolverAPI.scala b/src/main/scala/inox/solvers/SimpleSolverAPI.scala
index deb96092b..cd96dca50 100644
--- a/src/main/scala/inox/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/inox/solvers/SimpleSolverAPI.scala
@@ -11,7 +11,6 @@ trait SimpleSolverAPI {
def solveVALID(expression: Expr): Option[Boolean] = {
val s = factory.getNewSolver()
- import s._
try {
s.assertCnstr(Not(expression))
s.check(Simple) match {
@@ -25,7 +24,6 @@ trait SimpleSolverAPI {
def solveSAT(expression: Expr): ResponseWithModel[Map[ValDef, Expr]] = {
val s = factory.getNewSolver()
- import s._
try {
s.assertCnstr(expression)
s.check(Model)
@@ -37,7 +35,6 @@ trait SimpleSolverAPI {
def solveSATWithCores(expression: Expr, assumptions: Set[Expr]):
ResponseWithModelAndCores[Map[ValDef, Expr], Set[Expr]] = {
val s = factory.getNewSolver()
- import s._
try {
s.assertCnstr(expression)
s.checkAssumptions(All)(assumptions)
@@ -48,7 +45,7 @@ trait SimpleSolverAPI {
}
object SimpleSolverAPI {
- def apply(sf: SolverFactory) = new SimpleSolverAPI {
+ def apply(sf: SolverFactory): SimpleSolverAPI { val factory: sf.type } = new SimpleSolverAPI {
val factory: sf.type = sf
}
}
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index fc36dd3ff..6ef8140ac 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -22,7 +22,7 @@ trait SolverFactory {
}
object SolverFactory {
- def apply[S1 <: Solver : TypeTag](p: Program)(nme: String, builder: () => S1 { val program: p.type }):
+ def create[S1 <: Solver : TypeTag](p: Program)(nme: String, builder: () => S1 { val program: p.type }):
SolverFactory { val program: p.type; type S = S1 { val program: p.type } } = {
new SolverFactory {
val program: p.type = p
@@ -32,4 +32,6 @@ object SolverFactory {
def getNewSolver() = builder()
}
}
+
+ def apply(p: Program): SolverFactory { val program: p.type } = ???
}
--
GitLab