From 8cf2104a08c4a6b22bdc0c3d0842e16714303fd2 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 9 Aug 2016 11:44:47 +0200
Subject: [PATCH] checkAssumptions for EnumerationSolver, fixed Unsat case
---
.../inox/solvers/EnumerationSolver.scala | 33 ++++++++++++-------
1 file changed, 21 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/inox/solvers/EnumerationSolver.scala b/src/main/scala/inox/solvers/EnumerationSolver.scala
index 4ba5e19db..c15e09393 100644
--- a/src/main/scala/inox/solvers/EnumerationSolver.scala
+++ b/src/main/scala/inox/solvers/EnumerationSolver.scala
@@ -12,7 +12,6 @@ import datagen._
trait EnumerationSolver extends Solver { self =>
val grammars: GrammarsUniverse { val program: self.program.type }
-
val evaluator: DeterministicEvaluator { val program: self.program.type }
import program._
@@ -62,6 +61,7 @@ trait EnumerationSolver extends Solver { self =>
val program: self.program.type = self.program
def functionsAvailable(p: Program): Set[FunDef] = Set()
})
+
if (interrupted) {
Unknown
} else {
@@ -71,19 +71,22 @@ trait EnumerationSolver extends Solver { self =>
val it: Iterator[Seq[Expr]] = datagen.get.generateFor(allFreeVars, andJoin(allConstraints), 1, maxTried)
if (it.hasNext) {
- config match {
- case All | Model =>
- val varModels = it.next
- SatWithModel(allFreeVars.zip(varModels).toMap)
- case _ =>
- Sat
+ if (config.withModel) {
+ val varModels = it.next
+ SatWithModel(allFreeVars.zip(varModels).toMap)
+ } else {
+ Sat
}
} else {
- config match {
- case All | Cores =>
- ??? // TODO
- case _ =>
+ val cardinalities = allFreeVars.map(vd => typeCardinality(vd.tpe))
+ if (cardinalities.forall(_.isDefined) && cardinalities.flatten.product < maxTried) {
+ if (config.withCores) {
+ UnsatWithCores(Set.empty)
+ } else {
Unsat
+ }
+ } else {
+ Unknown
}
}
}
@@ -95,7 +98,13 @@ trait EnumerationSolver extends Solver { self =>
res
}
- def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Cores] = ??? // TODO
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Cores] = {
+ push()
+ for (c <- assumptions) assertCnstr(c)
+ val res = check(config)
+ pop()
+ res
+ }
def free() = {
constraints.clear()
--
GitLab