From 3560caf3c52b7edd4b1b8aa46a0e4230f154e3ee Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 8 Aug 2016 15:45:54 +0200
Subject: [PATCH] GrammarDataGen, EnumerationSolver
---
.../scala/inox/datagen/GrammarDataGen.scala | 9 +-
.../inox/solvers/EnumerationSolver.scala | 87 +++++++++++--------
2 files changed, 55 insertions(+), 41 deletions(-)
diff --git a/src/main/scala/inox/datagen/GrammarDataGen.scala b/src/main/scala/inox/datagen/GrammarDataGen.scala
index 0318f76eb..7b9280831 100644
--- a/src/main/scala/inox/datagen/GrammarDataGen.scala
+++ b/src/main/scala/inox/datagen/GrammarDataGen.scala
@@ -13,13 +13,16 @@ import grammars._
/** Utility functions to generate values of a given type.
* In fact, it could be used to generate *terms* of a given type,
* e.g. by passing trees representing variables for the "bounds". */
-trait GrammarDataGen extends DataGenerator with GrammarsUniverse { self =>
+trait GrammarDataGen extends DataGenerator { self =>
+ val grammars: GrammarsUniverse { val program: self.program.type }
+ import grammars._
val evaluator: DeterministicEvaluator { val program: self.program.type }
val grammar: ExpressionGrammar
import program._
import program.trees._
import program.symbols._
+ import exprOps._
// Assume e contains generic values with index 0.
// Return a series of expressions with all normalized combinations of generic values.
@@ -56,7 +59,7 @@ trait GrammarDataGen extends DataGenerator with GrammarsUniverse { self =>
enum.iterator(Label(tpe)).flatMap(expandGenerics).takeWhile(_ => !interrupted.get)
}
- 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]] = {
def filterCond(vs: Seq[Expr]): Boolean = satisfying match {
case BooleanLiteral(true) =>
@@ -85,7 +88,7 @@ trait GrammarDataGen extends DataGenerator with GrammarsUniverse { self =>
}
}
- def generateMapping(ins: Seq[Variable], satisfying: Expr, maxValid: Int, maxEnumerated: Int) = {
+ def generateMapping(ins: Seq[ValDef], satisfying: Expr, maxValid: Int, maxEnumerated: Int) = {
generateFor(ins, satisfying, maxValid, maxEnumerated) map (ins zip _)
}
diff --git a/src/main/scala/inox/solvers/EnumerationSolver.scala b/src/main/scala/inox/solvers/EnumerationSolver.scala
index 86a3a91f0..4ba5e19db 100644
--- a/src/main/scala/inox/solvers/EnumerationSolver.scala
+++ b/src/main/scala/inox/solvers/EnumerationSolver.scala
@@ -1,32 +1,39 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
package solvers
+import evaluators._
+import SolverResponses._
+import grammars.GrammarsUniverse
import utils._
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Constructors._
-import purescala.Expressions._
-import purescala.ExprOps._
-
import datagen._
-class EnumerationSolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
+trait EnumerationSolver extends Solver { self =>
+
+ val grammars: GrammarsUniverse { val program: self.program.type }
+
+ val evaluator: DeterministicEvaluator { val program: self.program.type }
+
+ import program._
+ import trees._
+ import symbols._
+ import exprOps._
+
def name = "Enum"
val maxTried = 10000
- var datagen: Option[DataGenerator] = None
+ var datagen: Option[DataGenerator { val program: self.program.type }] = None
private var interrupted = false
- val freeVars = new IncrementalSet[Identifier]()
+ val freeVars = new IncrementalSet[ValDef]()
val constraints = new IncrementalSeq[Expr]()
def assertCnstr(expression: Expr): Unit = {
constraints += expression
- freeVars ++= variablesOf(expression)
+ freeVars ++= variablesOf(expression).map(_.toVal)
}
def push() = {
@@ -46,43 +53,49 @@ class EnumerationSolver(val sctx: SolverContext, val program: Program) extends S
datagen = None
}
- private var model = Model.empty
-
- /** @inheritdoc */
- def check: Option[Boolean] = {
- val timer = context.timers.solvers.enum.check.start()
- val res = try {
- datagen = Some(new VanuatooDataGen(context, program, sctx.bank))
+ def check(config: Configuration): config.Response[Model, Cores] = config.cast {
+ val res: SolverResponse[Model, Cores] = try {
+ datagen = Some(new GrammarDataGen {
+ val grammars: self.grammars.type = self.grammars
+ val evaluator: DeterministicEvaluator { val program: self.program.type } = self.evaluator
+ val grammar: grammars.ExpressionGrammar = grammars.ValueGrammar
+ val program: self.program.type = self.program
+ def functionsAvailable(p: Program): Set[FunDef] = Set()
+ })
if (interrupted) {
- None
+ Unknown
} else {
- model = Model.empty
- val allFreeVars = freeVars.toSeq.sortBy(_.name)
+ val allFreeVars = freeVars.toSeq.sortBy(_.id.name)
val allConstraints = constraints.toSeq
- val it = datagen.get.generateFor(allFreeVars, andJoin(allConstraints), 1, maxTried)
+ val it: Iterator[Seq[Expr]] = datagen.get.generateFor(allFreeVars, andJoin(allConstraints), 1, maxTried)
if (it.hasNext) {
- val varModels = it.next
- model = new Model((allFreeVars zip varModels).toMap)
- Some(true)
+ config match {
+ case All | Model =>
+ val varModels = it.next
+ SatWithModel(allFreeVars.zip(varModels).toMap)
+ case _ =>
+ Sat
+ }
} else {
- None
+ config match {
+ case All | Cores =>
+ ??? // TODO
+ case _ =>
+ Unsat
+ }
}
}
} catch {
- case e: codegen.CompilationException =>
- None
+ case e: Throwable =>
+ Unknown
}
datagen = None
- timer.stop()
res
}
- /** @inheritdoc */
- def getModel: Model = {
- model
- }
+ def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Cores] = ??? // TODO
def free() = {
constraints.clear()
@@ -90,13 +103,11 @@ class EnumerationSolver(val sctx: SolverContext, val program: Program) extends S
def interrupt(): Unit = {
interrupted = true
-
- datagen.foreach{ s =>
- s.interrupt
- }
+ datagen.foreach(_.interrupt())
}
def recoverInterrupt(): Unit = {
- datagen.foreach(_.recoverInterrupt)
+ interrupted = false
+ datagen.foreach(_.recoverInterrupt())
}
}
--
GitLab