diff --git a/.gitignore b/.gitignore
index eac146feb701eca372077ae98c07f034477b0573..ab9f1b31435e9253435adc80f56e81500a3eba21 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,3 +11,6 @@ target
# synthesis
derivation*.dot
+
+# leon
+last.log
diff --git a/project/Build.scala b/project/Build.scala
index 6cead39eb4e6e866554d617a6247a61a54678b94..b0551d5413ff85b1dd5384edc921f1af0a5a0652 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -96,7 +96,7 @@ object Leon extends Build {
// the Java command that uses sbt's local Scala to run the whole contraption.
fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"$SCALA_HOME\" -Dscala.usejavacp=true ")
fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
- fw.write(mainClass+" $@" + nl)
+ fw.write(mainClass+" $@ 2>&1 | tee last.log" + nl)
fw.close
file.setExecutable(true)
} catch {
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index f0eee53a67cbe379212745dc71c159f421bcb9e8..761f882d2b7bc55e54ad9f25cd4eb142a2b20d33 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -15,5 +15,6 @@ case class LeonContext(
interruptManager: InterruptManager,
settings: Settings = Settings(),
options: Seq[LeonOption] = Seq(),
- files: Seq[File] = Seq()
+ files: Seq[File] = Seq(),
+ timers: StopwatchCollections = new StopwatchCollections
)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index b3b2736f1888b0d311fd959d15bf47700b094755..10e5c8953f8b96c96807d94c6eda2fd0574dcf89 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -110,8 +110,7 @@ object Main {
optionsValues += allOptionsMap(name) -> v
}
} else {
- initReporter.error("'"+name+"' is not a valid option. See 'leon --help'")
- None
+ initReporter.fatalError("'"+name+"' is not a valid option. See 'leon --help'")
}
}
@@ -143,12 +142,16 @@ object Main {
settings = settings.copy(xlang = value)
case LeonValueOption("debug", ListValue(sections)) =>
val debugSections = sections.flatMap { s =>
- ReportingSections.all.find(_.name == s) match {
- case Some(rs) =>
- Some(rs)
- case None =>
- initReporter.error("Section "+s+" not found, available: "+ReportingSections.all.map(_.name).mkString(", "))
- None
+ if (s == "all") {
+ ReportingSections.all
+ } else {
+ ReportingSections.all.find(_.name == s) match {
+ case Some(rs) =>
+ Some(rs)
+ case None =>
+ initReporter.error("Section "+s+" not found, available: "+ReportingSections.all.map(_.name).mkString(", "))
+ None
+ }
}
}
settings = settings.copy(debugSections = debugSections.toSet)
@@ -160,8 +163,7 @@ object Main {
// Create a new reporter taking settings into account
val reporter = new DefaultReporter(settings)
- reporter.ifDebug(ReportingOptions) {
- val debug = reporter.debug(ReportingOptions)_
+ reporter.ifDebug(ReportingOptions) { debug =>
debug("Options considered by Leon:")
for (lo <- leonOptions) lo match {
@@ -207,13 +209,19 @@ object Main {
}
def main(args : Array[String]) {
- // Process options
- val ctx = processOptions(args.toList)
+ try {
+ // Process options
+ val timer = new Stopwatch().start
- // Compute leon pipeline
- val pipeline = computePipeline(ctx.settings)
+ val ctx = processOptions(args.toList)
+
+ ctx.timers.get("Leon Opts") += timer
+
+ // Compute leon pipeline
+ val pipeline = computePipeline(ctx.settings)
+
+ timer.restart
- try {
// Run pipeline
pipeline.run(ctx)(args.toList) match {
case report: verification.VerificationReport =>
@@ -224,6 +232,18 @@ object Main {
case _ =>
}
+
+ ctx.timers.get("Leon Run") += timer
+
+ ctx.reporter.ifDebug(ReportingTimers) { debug =>
+ debug("-"*80)
+ debug("Times:")
+ debug("-"*80)
+ for ((name, swc) <- ctx.timers.getAll.toSeq.sortBy(_._1)) {
+ debug(swc.toString)
+ }
+ debug("-"*80)
+ }
} catch {
case LeonFatalError() => sys.exit(1)
}
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 63478b4b7113836c08196b61c393241b5d5f478c..6b89537c2d8afdcf85fefb51327c371c9d66953b 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -36,15 +36,15 @@ abstract class Reporter(settings: Settings) {
private val debugMask = settings.debugSections.foldLeft(0){ _ | _.mask }
- def ifDebug(section: ReportingSection)(body: => Any) {
+ def ifDebug(section: ReportingSection)(body: (Any => Unit) => Any) {
if ((debugMask & section.mask) == section.mask) {
- body
+ body(debugFunction)
}
}
def debug(section: ReportingSection)(msg: => Any) {
- ifDebug(section) {
- debugFunction(msg)
+ ifDebug(section) { debug =>
+ debug(msg)
}
}
}
@@ -84,16 +84,18 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
sealed abstract class ReportingSection(val name: String, val mask: Int)
-case object ReportingSolver extends ReportingSection("solver", 1 << 0)
-case object ReportingSynthesis extends ReportingSection("synthesis", 1 << 1)
-case object ReportingTimers extends ReportingSection("timers", 1 << 2)
-case object ReportingOptions extends ReportingSection("options", 1 << 3)
+case object ReportingSolver extends ReportingSection("solver", 1 << 0)
+case object ReportingSynthesis extends ReportingSection("synthesis", 1 << 1)
+case object ReportingTimers extends ReportingSection("timers", 1 << 2)
+case object ReportingOptions extends ReportingSection("options", 1 << 3)
+case object ReportingVerification extends ReportingSection("verification", 1 << 4)
object ReportingSections {
val all = Set[ReportingSection](
ReportingSolver,
ReportingSynthesis,
ReportingTimers,
- ReportingOptions
+ ReportingOptions,
+ ReportingVerification
)
}
diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
index 40c1ac5a61c51ad559ae5a93de6cf3a7364fe475..4812f117115ad2a2a369eba0c2aa9b6f069199a2 100644
--- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
@@ -11,6 +11,10 @@ case class SimpleSolverAPI(sf: SolverFactory[Solver]) {
s.check.map(r => !r)
}
+ def free() {
+ sf.free()
+ }
+
def solveSAT(expression: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
val s = sf.getNewSolver()
s.assertCnstr(expression)
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 6e848e99dc83ae1c751042aa74ada4277a132fa4..c637f1764c32237920ff0d1118b7b7d8131187eb 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -13,20 +13,7 @@ trait SolverFactory[S <: Solver] extends Interruptible with LeonComponent {
val context: LeonContext
val program: Program
- var freed = false
- val traceE = new Exception()
-
- override def finalize() {
- if (!freed) {
- //println("!! Solver not freed properly prior to GC:")
- //traceE.printStackTrace()
- free()
- }
- }
-
- def free() {
- freed = true
- }
+ def free() {}
var interrupted = false
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index ba406948d82694b85ea372a27b90609782080259..fe8c590c0999e00cece981fbc8886043697808a3 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -41,6 +41,10 @@ class TimeoutSolverFactory[S <: Solver](val sf: SolverFactory[S], val timeoutMs:
}
}
+ override def free() {
+ sf.free()
+ }
+
def withTimeout[T](solver: S)(body: => T): T = {
val timer = new Timer(timeout(solver))
timer.start
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 2f83d92720d76e9cc0d0c7b2dfb5c1ba1f1ef25b..75c828e71dce937b7e857c72544b5675a0e20e77 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -27,12 +27,26 @@ trait AbstractZ3Solver extends SolverFactory[Solver] {
context.interruptManager.registerForInterrupts(this)
+ val debug = context.reporter.debug(ReportingSolver)_
+
+ private[this] var freed = false
+ val traceE = new Exception()
+
+ override def finalize() {
+ if (!freed) {
+ println("!! Solver "+this.getClass.getName+"["+this.hashCode+"] not freed properly prior to GC:")
+ traceE.printStackTrace()
+ free()
+ }
+ }
+
class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t)
protected[leon] val z3cfg : Z3Config
protected[leon] var z3 : Z3Context = null
override def free() {
+ freed = true
super.free()
if (z3 ne null) {
z3.delete()
@@ -112,6 +126,7 @@ trait AbstractZ3Solver extends SolverFactory[Solver] {
var isInitialized = false
protected[leon] def initZ3() {
if (!isInitialized) {
+ val initTime = new Stopwatch().start
counter = 0
z3 = new Z3Context(z3cfg)
@@ -120,6 +135,9 @@ trait AbstractZ3Solver extends SolverFactory[Solver] {
prepareFunctions
isInitialized = true
+
+ initTime.stop
+ context.timers.get("Z3Solver init") += initTime
}
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala b/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
index ca49ca5332c75db5bd7635707fcf1d5e0b9fbd76..3ece4d56ca086e79b93812b221800c53f3bc164e 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
@@ -30,9 +30,6 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
enclosing =>
- val debug = context.reporter.debug(ReportingSolver)_
-
- // What wouldn't we do to avoid defining vars?
val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores) = locally {
var lucky = false
var check = false
@@ -406,13 +403,6 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
}
def fairCheck(assumptions: Set[Expr]): Option[Boolean] = {
- val totalTime = new Stopwatch().start
- val luckyTime = new Stopwatch()
- val z3Time = new Stopwatch()
- val scalaTime = new Stopwatch()
- val unrollingTime = new Stopwatch()
- val unlockingTime = new Stopwatch()
-
foundDefinitiveAnswer = false
def entireFormula = And(assumptions.toSeq ++ frameExpressions.flatten)
@@ -447,11 +437,9 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
// debug("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
// debug("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
- z3Time.start
solver.push() // FIXME: remove when z3 bug is fixed
val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.z3CurrentZ3Blockers) :_*)
solver.pop() // FIXME: remove when z3 bug is fixed
- z3Time.stop
debug(" - Finished search with blocked literals")
@@ -476,9 +464,7 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
foundAnswer(None, model)
}
} else {
- scalaTime.start
val model = modelToMap(z3model, varsInVC)
- scalaTime.stop
//lazy val modelAsString = model.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
//debug("- Found a model:")
@@ -537,11 +523,9 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
debug(" - Running search without blocked literals (w/o lucky test)")
}
- z3Time.start
solver.push() // FIXME: remove when z3 bug is fixed
val res2 = solver.checkAssumptions(assumptionsAsZ3 : _*)
solver.pop() // FIXME: remove when z3 bug is fixed
- z3Time.stop
res2 match {
case Some(false) =>
@@ -551,9 +535,7 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
//debug("SAT WITHOUT Blockers")
if (this.feelingLucky && !interrupted) {
// we might have been lucky :D
- luckyTime.start
val (wereWeLucky, cleanModel) = validateModel(solver.getModel, entireFormula, varsInVC, silenceErrors = true)
- luckyTime.stop
if(wereWeLucky) {
foundAnswer(Some(true), cleanModel)
@@ -577,15 +559,11 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
debug(" - more unrollings")
for(id <- toRelease) {
- unlockingTime.start
val newClauses = unrollingBank.unlock(id)
- unlockingTime.stop
- unrollingTime.start
for(ncl <- newClauses) {
solver.assertCnstr(ncl)
}
- unrollingTime.stop
}
debug(" - finished unrolling")
@@ -593,14 +571,6 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
}
}
- totalTime.stop
- StopwatchCollections.get("FairZ3 Total") += totalTime
- StopwatchCollections.get("FairZ3 Lucky Tests") += luckyTime
- StopwatchCollections.get("FairZ3 Z3") += z3Time
- StopwatchCollections.get("FairZ3 Unrolling") += unrollingTime
- StopwatchCollections.get("FairZ3 Unlocking") += unlockingTime
- StopwatchCollections.get("FairZ3 ScalaTime") += scalaTime
-
//debug(" !! DONE !! ")
if(interrupted) {
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index e4bf309d480654545351be867549b6be5de22943..0511dde98afaa7178c99e478cd804c69c94ea4e6 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -23,13 +23,7 @@ class ParallelSearch(synth: Synthesizer,
private[this] var contexts = List[SynthesisContext]()
def initWorkerContext(wr: ActorRef) = {
- val solverf = new FairZ3SolverFactory(synth.context, synth.program)
- solverf.initZ3
-
- val fastSolverf = new UninterpretedZ3SolverFactory(synth.context, synth.program)
- fastSolverf.initZ3
-
- val ctx = SynthesisContext.fromSynthesizer(synth).copy(solverf = solverf, fastSolverf = fastSolverf)
+ val ctx = SynthesisContext.fromSynthesizer(synth)
synchronized {
contexts = ctx :: contexts
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 21d1e72e49834055ac13fefee7597c89d6557980..dc3c2aaff391ef3c299b153989e600020c46caae 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -80,7 +80,7 @@ object RuleInstantiation {
}
abstract class Rule(val name: String) {
- def instantiateOn(scrx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation]
+ def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation]
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 543731c2351d75cc5f5ae288581eed7a8dfc59b1..39d7f0c774183ab7592b1056f1f03db94579b395 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -159,17 +159,26 @@ class SimpleSearch(synth: Synthesizer,
}
-
def searchStep() {
- nextLeaf() match {
+ val t = new Stopwatch().start
+ val nl = nextLeaf()
+ synth.context.timers.get("Synthesis NextLeaf") += t
+
+ nl match {
case Some(l) =>
l match {
case al: g.AndLeaf =>
val sub = expandAndTask(al.task)
+
+ t.restart
onExpansion(al, sub)
+ synth.context.timers.get("Synthesis Expand") += t
case ol: g.OrLeaf =>
val sub = expandOrTask(ol.task)
+
+ t.restart
onExpansion(ol, sub)
+ synth.context.timers.get("Synthesis Expand") += t
}
case None =>
stop()
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 1609064ce55e2ab248027ca7722286d74bb9329b..4269f4175cbda5a8d54f721d952cb76308a4faf5 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -4,6 +4,8 @@ package leon
package synthesis
import solvers._
+import solvers.z3._
+
import purescala.Trees._
import purescala.Definitions.{Program, FunDef}
import purescala.Common.Identifier
@@ -15,10 +17,18 @@ case class SynthesisContext(
options: SynthesisOptions,
functionContext: Option[FunDef],
program: Program,
- solverf: SolverFactory[Solver],
- fastSolverf: SolverFactory[Solver],
reporter: Reporter
-)
+) {
+
+ def solverFactory: SolverFactory[Solver] = {
+ new FairZ3SolverFactory(context, program)
+ }
+
+ def fastSolverFactory: SolverFactory[Solver] = {
+ new UninterpretedZ3SolverFactory(context, program)
+ }
+
+}
object SynthesisContext {
def fromSynthesizer(synth: Synthesizer) = {
@@ -27,8 +37,6 @@ object SynthesisContext {
synth.options,
synth.functionContext,
synth.program,
- synth.solverf,
- synth.fastSolverf,
synth.reporter)
}
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 3418c14fe7f4c32f18525c4328556539693552a7..40c3e49511c1f12801f45aca9c5decef86b460f6 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -24,9 +24,6 @@ class Synthesizer(val context : LeonContext,
val rules: Seq[Rule] = options.rules
- val solverf = new FairZ3SolverFactory(context, program)
- val fastSolverf = new UninterpretedZ3SolverFactory(context, program)
-
val reporter = context.reporter
def synthesize(): (Solution, Boolean) = {
@@ -49,6 +46,13 @@ class Synthesizer(val context : LeonContext,
val res = search.search()
+ search match {
+ case pr: ParallelSearch =>
+ context.timers.add(pr.expandTimers)
+ context.timers.add(pr.sendWorkTimers)
+ case _ =>
+ }
+
val diff = System.currentTimeMillis()-ts
reporter.info("Finished in "+diff+"ms")
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 594eecb76562e75dd7b44ed8a98c007a74abb10d..35cad0762f3da847e253ed41e71bdd6b27937759 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -14,11 +14,14 @@ import purescala.Definitions._
case object ADTInduction extends Rule("ADT Induction") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val tsolver = new TimeoutSolverFactory(sctx.solverf, 500L)
+ val tsolver = sctx.solverFactory.withTimeout(500L)
+
val candidates = p.as.collect {
case IsTyped(origId, AbstractClassType(cd)) if isInductiveOn(tsolver)(p.pc, origId) => (origId, cd)
}
+ tsolver.free()
+
val instances = for (candidate <- candidates) yield {
val (origId, cd) = candidate
val oas = p.as.filterNot(_ == origId)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
index 6bf7cc92e382f645bab7b11ba7a75b7bf03e78e9..e11f09448fa31606b2cd4030d7eef35e12a073d4 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
@@ -14,11 +14,13 @@ import purescala.Definitions._
case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val tsolver = sctx.solverf.withTimeout(500L)
+ val tsolver = sctx.solverFactory.withTimeout(500L)
val candidates = p.as.collect {
case IsTyped(origId, AbstractClassType(cd)) if isInductiveOn(tsolver)(p.pc, origId) => (origId, cd)
}
+ tsolver.free()
+
val instances = for (candidate <- candidates) yield {
val (origId, cd) = candidate
val oas = p.as.filterNot(_ == origId)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 18a48edbb6c03695c4cba87f5b74461c77e0f3ac..261b371433db98fca18afe3892b44be94c528774 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -14,7 +14,7 @@ import solvers._
case object ADTSplit extends Rule("ADT Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
- val solver = SimpleSolverAPI(sctx.solverf.withTimeout(200L))
+ val solver = SimpleSolverAPI(sctx.solverFactory.withTimeout(200L))
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
@@ -46,6 +46,8 @@ case object ADTSplit extends Rule("ADT Split.") {
}
}
+ solver.free()
+
candidates.collect{ _ match {
case Some((id, cases)) =>
val oas = p.as.filter(_ != id)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 9af12ce3d75876a2304c129e2732e27de47751b0..0ee2b35523c585cb809d66e1f965a5637eee8690 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -451,328 +451,333 @@ case object CEGIS extends Rule("CEGIS") {
var unrolings = 0
val maxUnrolings = 3
- val exSolver = sctx.solverf.withTimeout(3000L) // 3sec
- val cexSolver = sctx.solverf.withTimeout(3000L) // 3sec
+ val exSolver = sctx.solverFactory.withTimeout(3000L) // 3sec
+ val cexSolver = sctx.solverFactory.withTimeout(3000L) // 3sec
- var baseExampleInputs: Seq[Seq[Expr]] = Seq()
+ try {
+ var baseExampleInputs: Seq[Seq[Expr]] = Seq()
- // We populate the list of examples with a predefined one
- if (p.pc == BooleanLiteral(true)) {
- baseExampleInputs = p.as.map(a => simplestValue(a.getType)) +: baseExampleInputs
- } else {
- val solver = exSolver.getNewSolver
+ // We populate the list of examples with a predefined one
+ if (p.pc == BooleanLiteral(true)) {
+ baseExampleInputs = p.as.map(a => simplestValue(a.getType)) +: baseExampleInputs
+ } else {
+ val solver = exSolver.getNewSolver
- solver.assertCnstr(p.pc)
+ solver.assertCnstr(p.pc)
- solver.check match {
- case Some(true) =>
- val model = solver.getModel
- baseExampleInputs = p.as.map(a => model.getOrElse(a, simplestValue(a.getType))) +: baseExampleInputs
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
+ baseExampleInputs = p.as.map(a => model.getOrElse(a, simplestValue(a.getType))) +: baseExampleInputs
- case Some(false) =>
- return RuleApplicationImpossible
+ case Some(false) =>
+ return RuleApplicationImpossible
+
+ case None =>
+ sctx.reporter.warning("Solver could not solve path-condition")
+ return RuleApplicationImpossible // This is not necessary though, but probably wanted
+ }
- case None =>
- sctx.reporter.warning("Solver could not solve path-condition")
- return RuleApplicationImpossible // This is not necessary though, but probably wanted
}
- }
+ val inputIterator: Iterator[Seq[Expr]] = if (useVanuatoo) {
+ new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, 20, 3000)
+ } else {
+ new NaiveDataGen(sctx.context, sctx.program, evaluator).generateFor(p.as, p.pc, 20, 1000)
+ }
- val inputIterator: Iterator[Seq[Expr]] = if (useVanuatoo) {
- new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, 20, 3000)
- } else {
- new NaiveDataGen(sctx.context, sctx.program, evaluator).generateFor(p.as, p.pc, 20, 1000)
- }
+ val cachedInputIterator = new Iterator[Seq[Expr]] {
+ def next() = {
+ val i = inputIterator.next()
+ baseExampleInputs = i +: baseExampleInputs
+ i
+ }
- val cachedInputIterator = new Iterator[Seq[Expr]] {
- def next() = {
- val i = inputIterator.next()
- baseExampleInputs = i +: baseExampleInputs
- i
+ def hasNext() = inputIterator.hasNext
}
- def hasNext() = inputIterator.hasNext
- }
+ def hasInputExamples() = baseExampleInputs.size > 0 || cachedInputIterator.hasNext
- def hasInputExamples() = baseExampleInputs.size > 0 || cachedInputIterator.hasNext
+ def allInputExamples() = baseExampleInputs.iterator ++ cachedInputIterator
- def allInputExamples() = baseExampleInputs.iterator ++ cachedInputIterator
+ def checkForPrograms(programs: Set[Set[Identifier]]): RuleApplicationResult = {
+ for (prog <- programs) {
+ val expr = ndProgram.determinize(prog)
+ val res = Equals(Tuple(p.xs.map(Variable(_))), expr)
+ val solver3 = cexSolver.getNewSolver
+ solver3.assertCnstr(And(p.pc :: res :: Not(p.phi) :: Nil))
- def checkForPrograms(programs: Set[Set[Identifier]]): RuleApplicationResult = {
- for (prog <- programs) {
- val expr = ndProgram.determinize(prog)
- val res = Equals(Tuple(p.xs.map(Variable(_))), expr)
- val solver3 = cexSolver.getNewSolver
- solver3.assertCnstr(And(p.pc :: res :: Not(p.phi) :: Nil))
-
- solver3.check match {
- case Some(false) =>
- return RuleSuccess(Solution(BooleanLiteral(true), Set(), expr), isTrusted = true)
- case None =>
- return RuleSuccess(Solution(BooleanLiteral(true), Set(), expr), isTrusted = false)
- case Some(true) =>
- // invalid program, we skip
+ solver3.check match {
+ case Some(false) =>
+ return RuleSuccess(Solution(BooleanLiteral(true), Set(), expr), isTrusted = true)
+ case None =>
+ return RuleSuccess(Solution(BooleanLiteral(true), Set(), expr), isTrusted = false)
+ case Some(true) =>
+ // invalid program, we skip
+ }
}
+
+ RuleApplicationImpossible
}
- RuleApplicationImpossible
- }
+ // Keep track of collected cores to filter programs to test
+ var collectedCores = Set[Set[Identifier]]()
- // Keep track of collected cores to filter programs to test
- var collectedCores = Set[Set[Identifier]]()
+ val initExClause = And(p.pc :: p.phi :: Variable(initGuard) :: Nil)
+ val initCExClause = And(p.pc :: Not(p.phi) :: Variable(initGuard) :: Nil)
- val initExClause = And(p.pc :: p.phi :: Variable(initGuard) :: Nil)
- val initCExClause = And(p.pc :: Not(p.phi) :: Variable(initGuard) :: Nil)
+ // solver1 is used for the initial SAT queries
+ var solver1 = exSolver.getNewSolver
+ solver1.assertCnstr(initExClause)
- // solver1 is used for the initial SAT queries
- var solver1 = exSolver.getNewSolver
- solver1.assertCnstr(initExClause)
+ // solver2 is used for validating a candidate program, or finding new inputs
+ var solver2 = cexSolver.getNewSolver
+ solver2.assertCnstr(initCExClause)
- // solver2 is used for validating a candidate program, or finding new inputs
- var solver2 = cexSolver.getNewSolver
- solver2.assertCnstr(initCExClause)
+ var didFilterAlready = false
- var didFilterAlready = false
+ val tpe = TupleType(p.xs.map(_.getType))
- val tpe = TupleType(p.xs.map(_.getType))
+ try {
+ do {
+ var needMoreUnrolling = false
- try {
- do {
- var needMoreUnrolling = false
+ var bssAssumptions = Set[Identifier]()
- var bssAssumptions = Set[Identifier]()
+ if (!didFilterAlready) {
+ val (clauses, closedBs) = ndProgram.unroll
- if (!didFilterAlready) {
- val (clauses, closedBs) = ndProgram.unroll
+ bssAssumptions = closedBs
- bssAssumptions = closedBs
+ //println("UNROLLING: ")
+ //for (c <- clauses) {
+ // println(" - " + c)
+ //}
+ //println("CLOSED Bs "+closedBs)
- //println("UNROLLING: ")
- //for (c <- clauses) {
- // println(" - " + c)
- //}
- //println("CLOSED Bs "+closedBs)
+ val clause = And(clauses)
- val clause = And(clauses)
+ solver1.assertCnstr(clause)
+ solver2.assertCnstr(clause)
+ }
- solver1.assertCnstr(clause)
- solver2.assertCnstr(clause)
- }
+ // Compute all programs that have not been excluded yet
+ var prunedPrograms: Set[Set[Identifier]] = if (useCEPruning) {
+ ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p)))
+ } else {
+ Set()
+ }
- // Compute all programs that have not been excluded yet
- var prunedPrograms: Set[Set[Identifier]] = if (useCEPruning) {
- ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p)))
- } else {
- Set()
- }
+ val allPrograms = prunedPrograms.size
- val allPrograms = prunedPrograms.size
+ //println("Programs: "+prunedPrograms.size)
+ //println("#Tests: "+exampleInputs.size)
- //println("Programs: "+prunedPrograms.size)
- //println("#Tests: "+exampleInputs.size)
+ // We further filter the set of working programs to remove those that fail on known examples
+ if (useCEPruning && hasInputExamples() && ndProgram.canTest()) {
- // We further filter the set of working programs to remove those that fail on known examples
- if (useCEPruning && hasInputExamples() && ndProgram.canTest()) {
+ for (p <- prunedPrograms) {
+ if (!allInputExamples().forall(ndProgram.testForProgram(p))) {
+ // This program failed on at least one example
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ prunedPrograms -= p
+ }
+ }
- for (p <- prunedPrograms) {
- if (!allInputExamples().forall(ndProgram.testForProgram(p))) {
- // This program failed on at least one example
- solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
- prunedPrograms -= p
+ if (prunedPrograms.isEmpty) {
+ needMoreUnrolling = true
}
- }
- if (prunedPrograms.isEmpty) {
- needMoreUnrolling = true
+ //println("Passing tests: "+prunedPrograms.size)
}
- //println("Passing tests: "+prunedPrograms.size)
- }
+ val nPassing = prunedPrograms.size
+
+ if (nPassing == 0) {
+ needMoreUnrolling = true;
+ } else if (nPassing <= testUpTo) {
+ // Immediate Test
+ result = Some(checkForPrograms(prunedPrograms))
+ } else if (((nPassing < allPrograms*filterThreshold) || didFilterAlready) && useBssFiltering) {
+ // We filter the Bss so that the formula we give to z3 is much smalled
+ val bssToKeep = prunedPrograms.foldLeft(Set[Identifier]())(_ ++ _)
+ //println("To Keep: "+bssToKeep.size+"/"+ndProgram.bss.size)
+
+ // Cannot unroll normally after having filtered, so we need to
+ // repeat the filtering procedure at next unrolling.
+ didFilterAlready = true
+
+ // Freshening solvers
+ solver1 = exSolver.getNewSolver
+ solver1.assertCnstr(initExClause)
+ solver2 = cexSolver.getNewSolver
+ solver2.assertCnstr(initCExClause)
+
+ val clauses = ndProgram.filterFor(bssToKeep)
+ val clause = And(clauses)
+
+ solver1.assertCnstr(clause)
+ solver2.assertCnstr(clause)
+
+ //println("Filtered clauses:")
+ //for (c <- clauses) {
+ // println(" - " + c)
+ //}
- val nPassing = prunedPrograms.size
-
- if (nPassing == 0) {
- needMoreUnrolling = true;
- } else if (nPassing <= testUpTo) {
- // Immediate Test
- result = Some(checkForPrograms(prunedPrograms))
- } else if (((nPassing < allPrograms*filterThreshold) || didFilterAlready) && useBssFiltering) {
- // We filter the Bss so that the formula we give to z3 is much smalled
- val bssToKeep = prunedPrograms.foldLeft(Set[Identifier]())(_ ++ _)
- //println("To Keep: "+bssToKeep.size+"/"+ndProgram.bss.size)
-
- // Cannot unroll normally after having filtered, so we need to
- // repeat the filtering procedure at next unrolling.
- didFilterAlready = true
-
- // Freshening solvers
- solver1 = exSolver.getNewSolver
- solver1.assertCnstr(initExClause)
- solver2 = cexSolver.getNewSolver
- solver2.assertCnstr(initCExClause)
-
- val clauses = ndProgram.filterFor(bssToKeep)
- val clause = And(clauses)
-
- solver1.assertCnstr(clause)
- solver2.assertCnstr(clause)
-
- //println("Filtered clauses:")
- //for (c <- clauses) {
- // println(" - " + c)
- //}
+ }
- }
+ val bss = ndProgram.bss
- val bss = ndProgram.bss
+ while (result.isEmpty && !needMoreUnrolling && !interruptManager.isInterrupted()) {
- while (result.isEmpty && !needMoreUnrolling && !interruptManager.isInterrupted()) {
+ solver1.checkAssumptions(bssAssumptions.map(id => Not(Variable(id)))) match {
+ case Some(true) =>
+ val satModel = solver1.getModel
- solver1.checkAssumptions(bssAssumptions.map(id => Not(Variable(id)))) match {
- case Some(true) =>
- val satModel = solver1.getModel
+ val bssAssumptions: Set[Expr] = bss.map(b => satModel(b) match {
+ case BooleanLiteral(true) => Variable(b)
+ case BooleanLiteral(false) => Not(Variable(b))
+ })
- val bssAssumptions: Set[Expr] = bss.map(b => satModel(b) match {
- case BooleanLiteral(true) => Variable(b)
- case BooleanLiteral(false) => Not(Variable(b))
- })
+ //println("CEGIS OUT!")
+ //println("Found solution: "+bssAssumptions)
- //println("CEGIS OUT!")
- //println("Found solution: "+bssAssumptions)
+ //bssAssumptions.collect { case Variable(b) => ndProgram.mappings(b) }.foreach {
+ // case (c, ex) =>
+ // println(". "+c+" = "+ex)
+ //}
- //bssAssumptions.collect { case Variable(b) => ndProgram.mappings(b) }.foreach {
- // case (c, ex) =>
- // println(". "+c+" = "+ex)
- //}
+ val validateWithZ3 = if (useCETests && hasInputExamples() && ndProgram.canTest()) {
- val validateWithZ3 = if (useCETests && hasInputExamples() && ndProgram.canTest()) {
+ val p = bssAssumptions.collect { case Variable(b) => b }
- val p = bssAssumptions.collect { case Variable(b) => b }
-
- if (allInputExamples().forall(ndProgram.testForProgram(p))) {
- // All valid inputs also work with this, we need to
- // make sure by validating this candidate with z3
- true
+ if (allInputExamples().forall(ndProgram.testForProgram(p))) {
+ // All valid inputs also work with this, we need to
+ // make sure by validating this candidate with z3
+ true
+ } else {
+ // One valid input failed with this candidate, we can skip
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ false
+ }
} else {
- // One valid input failed with this candidate, we can skip
- solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
- false
+ // No inputs or capability to test, we need to ask Z3
+ true
}
- } else {
- // No inputs or capability to test, we need to ask Z3
- true
- }
- if (validateWithZ3) {
- //println("Looking for CE...")
- solver2.checkAssumptions(bssAssumptions) match {
- case Some(true) =>
- //println("#"*80)
- val invalidModel = solver2.getModel
+ if (validateWithZ3) {
+ //println("Looking for CE...")
+ solver2.checkAssumptions(bssAssumptions) match {
+ case Some(true) =>
+ //println("#"*80)
+ val invalidModel = solver2.getModel
- val fixedAss = And(ass.collect {
- case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
- }.toSeq)
+ val fixedAss = And(ass.collect {
+ case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
+ }.toSeq)
- val newCE = p.as.map(valuateWithModel(invalidModel))
+ val newCE = p.as.map(valuateWithModel(invalidModel))
- baseExampleInputs = newCE +: baseExampleInputs
+ baseExampleInputs = newCE +: baseExampleInputs
- //println("Found counter example: "+fixedAss)
+ //println("Found counter example: "+fixedAss)
- // Retest whether the newly found C-E invalidates all programs
- if (useCEPruning && ndProgram.canTest) {
- if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
- // println("I found a killer example!")
- needMoreUnrolling = true
+ // Retest whether the newly found C-E invalidates all programs
+ if (useCEPruning && ndProgram.canTest) {
+ if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
+ // println("I found a killer example!")
+ needMoreUnrolling = true
+ }
}
- }
- val unsatCore = if (useUnsatCores) {
- solver1.push()
- solver1.assertCnstr(fixedAss)
+ val unsatCore = if (useUnsatCores) {
+ solver1.push()
+ solver1.assertCnstr(fixedAss)
- val core = solver1.checkAssumptions(bssAssumptions) match {
- case Some(false) =>
- // Core might be empty if unrolling level is
- // insufficient, it becomes unsat no matter what
- // the assumptions are.
- solver1.getUnsatCore
+ val core = solver1.checkAssumptions(bssAssumptions) match {
+ case Some(false) =>
+ // Core might be empty if unrolling level is
+ // insufficient, it becomes unsat no matter what
+ // the assumptions are.
+ solver1.getUnsatCore
- case Some(true) =>
- // Can't be!
- bssAssumptions
+ case Some(true) =>
+ // Can't be!
+ bssAssumptions
- case None =>
- return RuleApplicationImpossible
- }
+ case None =>
+ return RuleApplicationImpossible
+ }
- solver1.pop()
+ solver1.pop()
- collectedCores += core.collect{ case Variable(id) => id }
+ collectedCores += core.collect{ case Variable(id) => id }
- core
- } else {
- bssAssumptions
- }
+ core
+ } else {
+ bssAssumptions
+ }
- if (unsatCore.isEmpty) {
- needMoreUnrolling = true
- } else {
- solver1.assertCnstr(Not(And(unsatCore.toSeq)))
- }
+ if (unsatCore.isEmpty) {
+ needMoreUnrolling = true
+ } else {
+ solver1.assertCnstr(Not(And(unsatCore.toSeq)))
+ }
- case Some(false) =>
+ case Some(false) =>
- val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
+ val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
- case _ =>
- if (useOptTimeout) {
- // Interpret timeout in CE search as "the candidate is valid"
- sctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
- val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr), isTrusted = false))
- } else {
- return RuleApplicationImpossible
- }
+ case _ =>
+ if (useOptTimeout) {
+ // Interpret timeout in CE search as "the candidate is valid"
+ sctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
+ val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr), isTrusted = false))
+ } else {
+ return RuleApplicationImpossible
+ }
+ }
}
- }
- case Some(false) =>
- //println("%%%% UNSAT")
+ case Some(false) =>
+ //println("%%%% UNSAT")
- if (useUninterpretedProbe) {
- solver1.check match {
- case Some(false) =>
- // Unsat even without blockers (under which fcalls are then uninterpreted)
- return RuleApplicationImpossible
+ if (useUninterpretedProbe) {
+ solver1.check match {
+ case Some(false) =>
+ // Unsat even without blockers (under which fcalls are then uninterpreted)
+ return RuleApplicationImpossible
- case _ =>
+ case _ =>
+ }
}
- }
- needMoreUnrolling = true
+ needMoreUnrolling = true
- case _ =>
- // Last chance, we test first few programs
- return checkForPrograms(prunedPrograms.take(testUpTo))
+ case _ =>
+ // Last chance, we test first few programs
+ return checkForPrograms(prunedPrograms.take(testUpTo))
+ }
}
- }
- unrolings += 1
- } while(unrolings < maxUnrolings && result.isEmpty && !interruptManager.isInterrupted())
+ unrolings += 1
+ } while(unrolings < maxUnrolings && result.isEmpty && !interruptManager.isInterrupted())
- result.getOrElse(RuleApplicationImpossible)
+ result.getOrElse(RuleApplicationImpossible)
- } catch {
- case e: Throwable =>
- sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
- e.printStackTrace
- RuleApplicationImpossible
+ } catch {
+ case e: Throwable =>
+ sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
+ e.printStackTrace
+ RuleApplicationImpossible
+ }
+ } finally {
+ exSolver.free()
+ cexSolver.free()
}
}
})
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index df5d2dd8c274251bd5bb37d16a71bf792f5dd24a..26867fd76f9162569cbb7f96f3f98efbd2b45e47 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -14,7 +14,7 @@ import solvers._
case object EqualitySplit extends Rule("Eq. Split") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val solver = SimpleSolverAPI(sctx.fastSolverf)
+ val solver = SimpleSolverAPI(sctx.fastSolverFactory)
val candidates = p.as.groupBy(_.getType).mapValues(_.combinations(2).filter {
case List(a1, a2) =>
@@ -40,6 +40,7 @@ case object EqualitySplit extends Rule("Eq. Split") {
case _ => false
}).values.flatten
+ solver.free()
candidates.flatMap(_ match {
case List(a1, a2) =>
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 440f6e78da59f132e22902db1060a2db4ba5d6ae..31bfcefad9dad1ec9cd59b4acaff2fffaa80f05e 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -14,11 +14,11 @@ case object Ground extends Rule("Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
- val solver = SimpleSolverAPI(sctx.solverf.withTimeout(5000L)) // We give that 5s
+ val solver = SimpleSolverAPI(sctx.solverFactory.withTimeout(5000L)) // We give that 5s
val tpe = TupleType(p.xs.map(_.getType))
- solver.solveSAT(p.phi) match {
+ val result = solver.solveSAT(p.phi) match {
case (Some(true), model) =>
val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
Some(RuleInstantiation.immediateSuccess(p, this, sol))
@@ -28,6 +28,10 @@ case object Ground extends Rule("Ground") {
case _ =>
None
}
+
+ solver.free()
+
+ result
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 8fddc9099acca2e1494909630d6e88e8305f3878..a2a2952165755d2bcd0013331a105e0667d5b9f7 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -15,7 +15,7 @@ import solvers._
case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val solver = SimpleSolverAPI(sctx.fastSolverf)
+ val solver = SimpleSolverAPI(sctx.fastSolverFactory)
val candidates = p.as.filter(_.getType == Int32Type).combinations(2).toList.filter {
case List(a1, a2) =>
@@ -52,6 +52,8 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
case _ => false
}
+ solver.free()
+
candidates.flatMap(_ match {
case List(a1, a2) =>
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index a3c9cbf61b477fbb55f43783a9eadf1db971db0a..6085007e313b78afd8774245556d9ac1d2c52792 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -17,7 +17,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
val res = new RuleInstantiation(p, this, SolutionBuilder.none, this.name) {
def apply(sctx: SynthesisContext) = {
- val solver = SimpleSolverAPI(sctx.fastSolverf) // Optimistic ground is given a simple solver (uninterpreted)
+ val solver = SimpleSolverAPI(sctx.fastSolverFactory) // Optimistic ground is given a simple solver (uninterpreted)
val xss = p.xs.toSet
val ass = p.as.toSet
@@ -69,6 +69,8 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
i += 1
}
+ solver.free()
+
result.getOrElse(RuleApplicationImpossible)
}
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index b2725b809bb3600388eacab352cb26c966a155c5..8aba2ad6f15b874587d9bce689ef5f825ba65ed2 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -2,6 +2,7 @@
package leon.synthesis.search
+import leon.utils._
import akka.actor._
import scala.concurrent.duration._
import scala.concurrent.Await
@@ -21,6 +22,9 @@ abstract class AndOrGraphParallelSearch[WC,
var system: ActorSystem = _
+ val sendWorkTimers = new StopwatchCollection("Synthesis-par SendWork")
+ val expandTimers = new StopwatchCollection("Synthesis-par Expand")
+
def search(): Option[(S, Boolean)] = {
system = ActorSystem("ParallelSearch")
@@ -92,6 +96,8 @@ abstract class AndOrGraphParallelSearch[WC,
assert(idleWorkers.size > 0)
+ val t = new Stopwatch().start
+
getNextLeaves(idleWorkers, workingWorkers) match {
case Nil =>
if (workingWorkers.isEmpty) {
@@ -112,6 +118,8 @@ abstract class AndOrGraphParallelSearch[WC,
}
}
}
+
+ sendWorkTimers += t
}
context.setReceiveTimeout(10.seconds)
@@ -128,7 +136,9 @@ abstract class AndOrGraphParallelSearch[WC,
case WorkerAndTaskDone(w, res) =>
workers.get(w) match {
case Some(Some(l: g.AndLeaf)) =>
+ val t = new Stopwatch().start
onExpansion(l, res)
+ expandTimers += t
workers += w -> None
case _ =>
}
@@ -137,7 +147,9 @@ abstract class AndOrGraphParallelSearch[WC,
case WorkerOrTaskDone(w, res) =>
workers.get(w) match {
case Some(Some(l: g.OrLeaf)) =>
+ val t = new Stopwatch().start
onExpansion(l, res)
+ expandTimers += t
workers += w -> None
case _ =>
}
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 0e6ae51b168c922b7f9523fbbf5113502e169511..228e8720cda12474517a0ac5bab8314d77361479 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -7,8 +7,6 @@ import leon.utils._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
-import leon.solvers.z3._
-import leon.solvers._
import leon.synthesis._
import java.util.Date
@@ -90,9 +88,6 @@ object Benchmarks extends App {
val (program, results) = pipeline.run(innerCtx)(file.getPath :: Nil)
- val solverf = new FairZ3SolverFactory(ctx, program)
-
- val fastSolverf = new UninterpretedZ3SolverFactory(ctx, program)
for ((f, ps) <- results.toSeq.sortBy(_._1.id.toString); p <- ps) {
val sctx = SynthesisContext(
@@ -100,8 +95,6 @@ object Benchmarks extends App {
options = opts,
functionContext = Some(f),
program = program,
- solverf = solverf,
- fastSolverf = fastSolverf,
reporter = ctx.reporter
)
@@ -144,13 +137,13 @@ object Benchmarks extends App {
println
- val infoHeader2 : String = " ┌────────────â”\n" +
- "â•”â•â•¡ Timers â•ž" + ("â•" * 71) + "â•—\n" +
- "║ └────────────┘" + (" " * 71) + "║"
+ //val infoHeader2 : String = " ┌────────────â”\n" +
+ // "â•”â•â•¡ Timers â•ž" + ("â•" * 71) + "â•—\n" +
+ // "║ └────────────┘" + (" " * 71) + "║"
- println(infoHeader2)
- for ((name, sw) <- StopwatchCollections.getAll.toSeq.sortBy(_._1)) {
- println("â•‘ %-70s %10s ms â•‘".format(name, sw.getMillis))
- }
- println(infoFooter)
+ //println(infoHeader2)
+ //for ((name, sw) <- StopwatchCollections.getAll.toSeq.sortBy(_._1)) {
+ // println("â•‘ %-70s %10s ms â•‘".format(name, sw.getMillis))
+ //}
+ //println(infoFooter)
}
diff --git a/src/main/scala/leon/utils/Stopwatch.scala b/src/main/scala/leon/utils/Stopwatch.scala
index 38b38bbf35cfe7510a4b94d179ebcbc6dea63c53..9622a4bd8d005a86978ef3bca89ca3e462701507 100644
--- a/src/main/scala/leon/utils/Stopwatch.scala
+++ b/src/main/scala/leon/utils/Stopwatch.scala
@@ -3,14 +3,35 @@
package leon
package utils
-class StopwatchCollection(name: String) {
- var acc: Long = 0L
+class StopwatchCollection(val name: String) {
+ var min: Long = 0L
+ var tot: Long = 0L
+ var max: Long = 0L
+ var n: Int = 0
- def +=(sw: Stopwatch) = synchronized { acc += sw.getMillis }
+ def +=(sw: Stopwatch) = synchronized {
+ val ms = sw.getMillis
+ if(n == 0 || ms < min) {
+ min = ms
+ }
+ if(n == 0 || ms > max) {
+ max = ms
+ }
+ n += 1
+ tot += ms
+ }
- def getMillis = acc
+ override def toString = {
+ if (n == 0) {
+ "%-30s N/A".format(name+":")
+ } else if (n > 1) {
+ "%-30s %6d ms (min: %d, avg: %d, max: %d, n: %d)".format(name+":", tot, min, tot/n, max, n)
+ } else {
+ "%-30s %6d ms".format(name+":", tot)
+ }
+ }
- override def toString = "%20s: %5dms".format(name, acc)
+ def getMillis = tot
}
/** Implements a stopwatch for profiling purposes */
@@ -25,6 +46,14 @@ class Stopwatch(name: String = "Stopwatch") {
this
}
+ def restart: this.type = {
+ beginning = 0L
+ end = 0L
+ acc = 0L
+
+ start
+ }
+
def stop {
end = System.currentTimeMillis
acc += (end - beginning)
@@ -44,7 +73,7 @@ class Stopwatch(name: String = "Stopwatch") {
override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "")
}
-object StopwatchCollections {
+class StopwatchCollections {
private var all = Map[String, StopwatchCollection]()
def get(name: String): StopwatchCollection = all.getOrElse(name, {
@@ -53,5 +82,9 @@ object StopwatchCollections {
sw
})
+ def add(swc: StopwatchCollection) {
+ all += swc.name -> swc
+ }
+
def getAll = all
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 653d9f021626991450b8b7b218c44b446b4ff394..9d670277356fda571ccccfd6afa4f017e8443179 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -61,6 +61,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val reporter = vctx.reporter
val solvers = vctx.solvers
+ val debug = reporter.debug(ReportingVerification)_
+
val interruptManager = vctx.context.interruptManager
for((funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1 < b._1); vcInfo <- vcs if !interruptManager.isInterrupted()) {
@@ -68,12 +70,12 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val vc = vcInfo.condition
reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
- reporter.info("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
- reporter.info(simplifyLets(vc))
+ debug("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
+ debug(simplifyLets(vc))
// try all solvers until one returns a meaningful answer
solvers.find(se => {
- reporter.info("Trying with solver: " + se.name)
+ debug("Trying with solver: " + se.name)
val t1 = System.nanoTime
val (satResult, counterexample) = SimpleSolverAPI(se).solveSAT(Not(vc))
val solverResult = satResult.map(!_)
@@ -114,7 +116,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}) match {
case None => {
vcInfo.hasValue = true
- reporter.warning("No solver could prove or disprove the verification condition.")
+ reporter.warning("==== UNKNOWN ====")
}
case _ =>
}
@@ -154,8 +156,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val vctx = VerificationContext(ctx, solvers, reporter)
+ val debug = reporter.debug(ReportingVerification)_
+
val report = if(solvers.size >= 1) {
- reporter.info("Running verification condition generation...")
+ debug("Running verification condition generation...")
val vcs = generateVerificationConditions(reporter, program, functionsToAnalyse)
checkVerificationConditions(vctx, vcs)
} else {
@@ -163,6 +167,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
VerificationReport.emptyReport
}
+ solvers.foreach(_.free())
+
report
}
}
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index 202a76fb7545a2d207738d93172259507bb7e978..056d97327e7e6557fdf8d770a6c80e2b0a8c3da6 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -18,7 +18,7 @@ trait LeonTestSuite extends FunSuite with Timeouts {
case class Statistics(values: List[Long]) {
val n = values.size
val avg = values.sum.toDouble/n
- val stddev = Math.sqrt(Math.abs(values.map(_.toDouble - avg).sum/n))
+ val stddev = Math.sqrt(values.map(v => Math.pow(v.toDouble - avg, 2)).sum/n)
def accountsFor(ms: Long) = {
if (n < 5) {
@@ -47,7 +47,9 @@ trait LeonTestSuite extends FunSuite with Timeouts {
}
def testIdentifier(name: String): String = {
- (this.getClass.getName+"-"+name).replaceAll("[^0-9a-zA-Z-]", "")
+ def sanitize(s: String) = s.replaceAll("[^0-9a-zA-Z-]", "")
+
+ sanitize(this.getClass.getName)+"/"+sanitize(name)
}
def bookKeepingFile(id: String) = {
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 9878b66dbb094a4c5e32c487ce5c1bb9fa15c860..a1d804171d499f8ca59a2d24a23686802f68d7ec 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -17,9 +17,12 @@ class TreeOpsTests extends LeonTestSuite {
test("Path-aware simplifications") {
val solver = new UninterpretedZ3SolverFactory(testContext, Program.empty)
+
// TODO actually testing something here would be better, sorry
// PS
+ solver.free()
+
assert(true)
}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 3dd9579f8f41ae434826a9ae14e68bc1e7b270e1..cdc28175ee16514a64f8b6c1c78dd86f2aa3ad7f 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -102,4 +102,6 @@ class FairZ3SolverTests extends LeonTestSuite {
assert(core === Set(b2))
}
}
+
+ solver.free()
}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 4d9036d8611d77eb7a4c5b6e0f0e0ecdbaf27d1f..e44e3697f05b8079ffd0bea263c077bc0c5bd84d 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -113,4 +113,6 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
assert(sub.getUnsatCore === Set(b2))
}
}
+
+ solver.free()
}
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index ed3d5419899fdf3aae2d028ccab3ea06418dae0c..050c5a8efc63ec582baf7d1216615cdfd4e84889 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -89,4 +89,6 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
solver.solveVALID(Equals(g(x), g(x)))
}
}
+
+ solver.free()
}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 49651699cd3c6c33446f113961edc13eb1bba0fa..16f3ce73b2ae5b60a97752c4e7762628313f405a 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -37,18 +37,12 @@ class SynthesisSuite extends LeonTestSuite {
val (program, results) = pipeline.run(ctx)((content, Nil))
- val solver = new FairZ3SolverFactory(ctx, program)
-
- val simpleSolver = new UninterpretedZ3SolverFactory(ctx, program)
-
for ((f, ps) <- results; p <- ps) {
test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, title)) {
val sctx = SynthesisContext(ctx,
opts,
Some(f),
program,
- solver,
- simpleSolver,
ctx.reporter)
block(sctx, f, p)