From 545b280d03a628c6cfa8458ed3ffe42b4d0d36ae Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 24 Dec 2016 17:45:49 +0100
Subject: [PATCH] Some enhancement to model-finding mode
---
src/main/scala/inox/Main.scala | 2 +-
.../scala/inox/solvers/unrolling/Templates.scala | 3 ++-
.../inox/solvers/unrolling/UnrollingSolver.scala | 13 +++++++++----
3 files changed, 12 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
index aa9be2481..60f4b55bb 100644
--- a/src/main/scala/inox/Main.scala
+++ b/src/main/scala/inox/Main.scala
@@ -64,7 +64,7 @@ trait MainHelpers {
solvers.unrolling.optFeelingLucky -> Description(Solvers, "Use evaluator to find counter-examples early"),
solvers.unrolling.optUnrollAssumptions -> Description(Solvers, "Use unsat-assumptions to drive unfolding while remaining fair"),
solvers.unrolling.optNoSimplifications -> Description(Solvers, "Disable selector/quantifier simplifications in solvers"),
- solvers.unrolling.optModelFinding -> Description(Solvers, "Enhance model-finding capabilities of solvers"),
+ solvers.unrolling.optModelFinding -> Description(Solvers, "Enhance model-finding capabilities of solvers by given aggresivity"),
solvers.smtlib.optCVC4Options -> Description(Solvers, "Pass extra options to CVC4"),
evaluators.optMaxCalls -> Description(Evaluators, "Maximum function invocations allowed during evaluation (-1 for unbounded)"),
evaluators.optIgnoreContracts -> Description(Evaluators, "Don't fail on invalid contracts during evaluation")
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index c07a618f1..f81808755 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -46,10 +46,11 @@ trait Templates extends TemplateGenerator
private[unrolling] lazy val falseT = mkEncoder(Map.empty)(BooleanLiteral(false))
protected lazy val simplify = !ctx.options.findOptionOrDefault(optNoSimplifications)
+ protected lazy val deferFactor = 3 * ctx.options.findOptionOrDefault(optModelFinding)
private var currentGen: Int = 0
protected def currentGeneration: Int = currentGen
- protected def nextGeneration(gen: Int): Int = gen + 3
+ protected def nextGeneration(gen: Int): Int = gen + 3 + deferFactor
trait Manager extends IncrementalStateWrapper {
def unrollGeneration: Option[Int]
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 052cfaf17..caae2a21a 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -12,10 +12,15 @@ import combinators._
import scala.collection.mutable.{Map => MutableMap}
-object optUnrollFactor extends LongOptionDef("unrollfactor", default = 1, "<PosInt>")
+object optUnrollFactor extends IntOptionDef("unrollfactor", default = 1, "<PosInt>")
object optFeelingLucky extends FlagOptionDef("feelinglucky", false)
object optUnrollAssumptions extends FlagOptionDef("unrollassumptions", false)
-object optModelFinding extends FlagOptionDef("modelfinding", false)
+object optModelFinding extends IntOptionDef("modelfinding", 0, "<PosInt> | 0 (off)") {
+ override val parser: OptionParsers.OptionParser[Int] = (s => s match {
+ case "" => Some(1)
+ case _ => OptionParsers.intParser(s)
+ })
+}
trait AbstractUnrollingSolver extends Solver { self =>
@@ -70,7 +75,7 @@ trait AbstractUnrollingSolver extends Solver { self =>
lazy val unrollFactor = options.findOptionOrDefault(optUnrollFactor)
lazy val feelingLucky = options.findOptionOrDefault(optFeelingLucky)
lazy val unrollAssumptions = options.findOptionOrDefault(optUnrollAssumptions)
- lazy val modelFinding = options.findOptionOrDefault(optModelFinding)
+ lazy val modelFinding = options.findOptionOrDefault(optModelFinding) > 0
def check(config: CheckConfiguration): config.Response[Model, Assumptions] =
checkAssumptions(config)(Set.empty)
@@ -628,7 +633,7 @@ trait AbstractUnrollingSolver extends Solver { self =>
val timer = ctx.timers.solvers.unroll.start()
// unfolling `unrollFactor` times
- for (i <- 1 to unrollFactor.toInt if templates.canUnroll) {
+ for (i <- 1 to unrollFactor.toInt if templates.canUnroll && !abort && !pause) {
val newClauses = templates.unroll
for (ncl <- newClauses) {
underlying.assertCnstr(ncl)
--
GitLab