From b9d98db8a49e89aca9097873b322f7998512d4cf Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 14 Dec 2012 15:58:39 +0100
Subject: [PATCH] Improve performance of FairZ3 by lowering unrolling to the z3
level. Improve synthesis profiling script.
Improve performance of FairZ3:
Make function templates and unlocking/unrolling work directly at the z3 level for performance reasons.
Implement push-pop at the unrolling-bank level. Works around a z3 bug.
Z3 apparently side-effects during check-assumptions, causing a following
check without assumptions to produce unreliable results. We work around this
by backtracking to the state before the check-assumptions using
push/pop.
Improve synthesis profiling/benchmarking:
Move benchrmarking suite away from tests. Synthesis Rule application
benchmark can now use a --rule option specifying what rule to apply.
Add Testcase to evaluate CEGIS unrolling of different depth.
Benchmarking script is now generated via the 'bench' sbt task.
---
.gitignore | 2 +
project/Build.scala | 138 +++++-----
src/main/scala/leon/FunctionTemplate.scala | 238 ------------------
src/main/scala/leon/LeonContext.scala | 4 +-
src/main/scala/leon/Main.scala | 2 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 7 +
.../scala/leon/solvers/z3/FairZ3Solver.scala | 160 ++++++++----
.../leon/solvers/z3/FunctionTemplate.scala | 213 ++++++++++++++++
.../leon/synthesis/utils/Benchmarks.scala} | 75 ++++--
.../SynthesisProblemExtractionPhase.scala | 45 ++++
.../leon/verification/AnalysisPhase.scala | 6 -
...cationSuite.scala => SynthesisSuite.scala} | 38 +--
testcases/synthesis/CegisExamples.scala | 24 ++
13 files changed, 531 insertions(+), 421 deletions(-)
delete mode 100644 src/main/scala/leon/FunctionTemplate.scala
create mode 100644 src/main/scala/leon/solvers/z3/FunctionTemplate.scala
rename src/{test/scala/leon/benchmark/SynthesisBenchmarks.scala => main/scala/leon/synthesis/utils/Benchmarks.scala} (59%)
create mode 100644 src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
rename src/test/scala/leon/test/synthesis/{RuleApplicationSuite.scala => SynthesisSuite.scala} (70%)
create mode 100644 testcases/synthesis/CegisExamples.scala
diff --git a/.gitignore b/.gitignore
index 0d1fa1988..12c115fd5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,6 +5,8 @@
target
/project/build
/leon
+/setupenv
+/leon-bench
# synthesis
derivation*.dot
diff --git a/project/Build.scala b/project/Build.scala
index 43a54c499..eff96902f 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -3,10 +3,12 @@ import Process._
import Keys._
object Leon extends Build {
- private val scriptName = "leon"
+ private val scriptName = "leon"
private val setupScriptName = "setupenv"
+ private val benchScriptName = "leon-bench"
def scriptFile = file(".") / scriptName
+ def benchScriptFile = file(".") / benchScriptName
def setupScriptFile = file(".") / setupScriptName
def is64 = System.getProperty("sun.arch.data.model") == "64"
@@ -18,85 +20,99 @@ object Leon extends Build {
if(scriptFile.exists && scriptFile.isFile) {
scriptFile.delete
}
+ if(setupScriptFile.exists && setupScriptFile.isFile) {
+ setupScriptFile.delete
+ }
+ if(benchScriptFile.exists && benchScriptFile.isFile) {
+ benchScriptFile.delete
+ }
}
- val scriptTask = TaskKey[Unit]("script", "Generate the " + scriptName + " and " + setupScriptName + " Bash scriptes") <<= (streams, dependencyClasspath in Compile, classDirectory in Compile) map { (s, deps, out) =>
- if(scriptFile.exists) {
- s.log.info("Re-generating script ("+(if(is64) "64b" else "32b")+")...")
- scriptFile.delete
- } else {
- s.log.info("Generating script ("+(if(is64) "64b" else "32b")+")...")
+ val nl = System.getProperty("line.separator")
+
+ val setupScriptTask = TaskKey[Seq[String]]("setup", "Generate the " + setupScriptName + " Bash script")
+
+ val setupSetting = setupScriptTask <<= (streams, dependencyClasspath in Compile, classDirectory in Compile) map { (s, deps, out) =>
+
+ val depsPaths = deps.map(_.data.absolutePath)
+
+ val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
+ case None => throw new Exception("Couldn't guess SCALA_HOME.")
+ case Some(p) => p.substring(0, p.length - 21)
}
- try {
- val depsPaths = deps.map(_.data.absolutePath)
- // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
- val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
- case None => throw new Exception("Couldn't guess SCALA_HOME.")
- case Some(p) => p.substring(0, p.length - 21)
- }
- s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
+ val ldLibPath = if (is64) ldLibraryDir64.absolutePath else ldLibraryDir32.absolutePath
- val nl = System.getProperty("line.separator")
- val fw = new java.io.FileWriter(scriptFile)
- fw.write("#!/bin/bash --posix" + nl)
- val ldLibPath = if (is64) {
- fw.write("SCALACLASSPATH=\"")
- fw.write((out.absolutePath +: depsPaths).mkString(":"))
- fw.write("\"" + nl + nl)
+ val leonLibPath = depsPaths.find(_.endsWith("/library/target/scala-2.9.2/classes")) match {
+ case None => throw new Exception("Couldn't find leon-library in the classpath.")
+ case Some(p) => p
+ }
- // Setting the dynamic lib path
- ldLibraryDir64.absolutePath
- } else {
- fw.write("if [ `uname -m` == \"x86_64\" ]; then "+nl)
+ // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
+ s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
- fw.write(" echo \"It appears you have compiled Leon with a 32bit virtual machine, but are now trying to run it on a 64bit architecture. This is unfortunately not supported.\"" + nl)
- fw.write(" exit -1" + nl)
+ if (setupScriptFile.exists) {
+ s.log.info("Regenerating '"+setupScriptFile.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+ setupScriptFile.delete
+ } else {
+ s.log.info("Generating '"+setupScriptFile.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+ }
+ val sfw = new java.io.FileWriter(setupScriptFile)
+ sfw.write("#!/bin/bash --posix" + nl)
+ if (!is64) {
+ sfw.write("if [ `uname -m` == \"x86_64\" ]; then "+nl)
+ sfw.write(" echo \"It appears you have compiled Leon with a 32bit virtual machine, but are now trying to run it on a 64bit architecture. This is unfortunately not supported.\"" + nl)
+ sfw.write(" exit -1" + nl)
+ sfw.write("fi"+ nl)
+ }
+ sfw.write("export LD_LIBRARY_PATH=\""+ldLibPath+"\"" + nl)
+ sfw.write("export LEON_LIBRARY_PATH=\""+leonLibPath+"\"" + nl)
+ sfw.write("export SCALA_HOME=\""+scalaHomeDir+"\"" + nl)
+ sfw.close
+ setupScriptFile.setExecutable(true)
- fw.write("else" + nl)
+ (out.absolutePath +: depsPaths)
+ }
- fw.write(" SCALACLASSPATH=\"")
- fw.write((out.absolutePath +: depsPaths).mkString(":"))
- fw.write("\"" + nl)
+ def genRunnerTask(taskName: String, file: File, name: String, mainClass: String) = {
+ TaskKey[Unit](taskName, "Generate the " + name + " Bash script") <<= (streams, setupScriptTask) map { (s, cps) =>
+ try {
+ // Paths discovery
+ if(file.exists) {
+ s.log.info("Regenerating '"+file.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+ file.delete
+ } else {
+ s.log.info("Generating '"+file.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+ }
- // Setting the dynamic lib path
- fw.write("fi" + nl + nl)
+ val fw = new java.io.FileWriter(file)
+ fw.write("#!/bin/bash --posix" + nl)
- ldLibraryDir32.absolutePath
- }
+ fw.write("SCALACLASSPATH=\"")
+ fw.write(cps.mkString(":"))
+ fw.write("\"" + nl + nl)
- val leonLibPath = depsPaths.find(_.endsWith("/library/target/scala-2.9.2/classes")) match {
- case None => throw new Exception("Couldn't find leon-library in the classpath.")
- case Some(p) => p
+ fw.write("source "+setupScriptFile.getAbsolutePath()+nl)
+ // 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.close
+ file.setExecutable(true)
+ } catch {
+ case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
}
-
- fw.write("source "+setupScriptFile.getAbsolutePath()+nl)
- // the Java command that uses sbt's local Scala to run the whole contraption.
- fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"")
- fw.write(scalaHomeDir)
- fw.write("\" -Dscala.usejavacp=true ")
- fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
- fw.write("leon.Main $@" + nl)
- fw.close
- scriptFile.setExecutable(true)
-
- s.log.info("Generating setup script ("+(if(is64) "64b" else "32b")+")...")
- val sfw = new java.io.FileWriter(setupScriptFile)
- sfw.write("#!/bin/bash --posix" + nl)
- sfw.write("export LD_LIBRARY_PATH=\""+ldLibPath+"\"" + nl)
- sfw.write("export LEON_LIBRARY_PATH=\""+leonLibPath+"\"" + nl)
- sfw.write("export SCALA_HOME=\""+scalaHomeDir+"\"" + nl)
- sfw.close
- setupScriptFile.setExecutable(true)
-
- } catch {
- case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
}
}
+ val scriptTask = genRunnerTask("script", scriptFile, scriptName, "leon.Main")
+ val benchTask = genRunnerTask("bench", benchScriptFile, benchScriptName, "leon.synthesis.utils.Benchmarks")
+
object LeonProject {
val settings = Seq(
+ setupSetting,
scriptTask,
+ benchTask,
cleanTask
)
}
diff --git a/src/main/scala/leon/FunctionTemplate.scala b/src/main/scala/leon/FunctionTemplate.scala
deleted file mode 100644
index 3f3494524..000000000
--- a/src/main/scala/leon/FunctionTemplate.scala
+++ /dev/null
@@ -1,238 +0,0 @@
-package leon
-
-import purescala.Common._
-import purescala.Trees._
-import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
-
-import scala.collection.mutable.{Set=>MutableSet,Map=>MutableMap}
-
-// TODO: maybe a candidate for moving into purescala package?
-class FunctionTemplate private(
- funDef : Option[FunDef],
- activatingBool : Identifier,
- condVars : Set[Identifier],
- exprVars : Set[Identifier],
- guardedExprs : Map[(Identifier,Boolean),Seq[Expr]]) {
-
- val asClauses : Seq[Expr] = {
- (for(((b,p),es) <- guardedExprs; e <- es) yield {
- Implies(if(!p) Not(Variable(b)) else Variable(b), e)
- }).toSeq
- }
-
- val blockers : Map[(Identifier,Boolean),Set[FunctionInvocation]] = {
- val idCall = funDef.map(fd => FunctionInvocation(fd, fd.args.map(_.toVariable)))
-
- Map((for((p, es) <- guardedExprs) yield {
- val calls = es.foldLeft(Set.empty[FunctionInvocation])((s,e) => s ++ functionCallsOf(e)) -- idCall
- if(calls.isEmpty) {
- None
- } else {
- Some((p, calls))
- }
- }).flatten.toSeq : _*)
- }
-
- // Returns two things:
- // - a set of clauses representing the computation of the function/post
- // - a map indicating which boolean variables guard which (recursive) fun. invoc.
- def instantiate(aVar : Identifier, aPol : Boolean, args : Seq[Expr]) : (Seq[Expr],Map[(Identifier,Boolean),Set[FunctionInvocation]]) = {
- assert(this.funDef.isDefined)
-
- val funDef = this.funDef.get
- assert(args.size == funDef.args.size)
-
- val idSubstMap : Map[Identifier,Identifier] =
- Map((for(c <- condVars) yield {
- val f = FreshIdentifier("bf", true).setType(BooleanType)
- c -> f
- }).toSeq : _*) ++
- Map((for(e <- exprVars) yield {
- val f = FreshIdentifier("ef", true).setType(e.getType)
- e -> f
- }).toSeq : _*)
-
- val substMap : Map[Expr,Expr] =
- idSubstMap.map(p => Variable(p._1) -> Variable(p._2)) ++
- Map(Variable(activatingBool) -> (if(aPol) Variable(aVar) else Not(Variable(aVar)))) ++
- Map((funDef.args.map(_.toVariable) zip args) : _*)
-
- (
- asClauses.map(c => replace(substMap, c)),
- blockers.map(pair => {
- val (b,p) = pair._1
- val newBP = if(b == activatingBool) {
- (aVar, p == aPol)
- } else {
- (idSubstMap(b), p)
- }
- (newBP, pair._2.map(e => replace(substMap, e).asInstanceOf[FunctionInvocation]))
- })
- )
- }
-
- override def toString : String = {
- if (funDef.isDefined) {
- "Template for def " + funDef.get.id + "(" + funDef.get.args.map(a => a.id + " : " + a.tpe).mkString(", ") + ") : " + funDef.get.returnType + " is :\n"
- } else {
- "Template for expr is :\n"
- } +
- " * Activating boolean : " + activatingBool + "\n" +
- " * Control booleans : " + condVars.toSeq.map(_.toString).mkString(", ") + "\n" +
- " * Expression vars : " + exprVars.toSeq.map(_.toString).mkString(", ") + "\n" +
- " * \"Clauses\" : " + "\n " + asClauses.mkString("\n ") + "\n" +
- " * Block-map : " + blockers.toString
- }
-}
-
-object FunctionTemplate {
- private val SIMPLERIFS : Boolean = true // don't clausify ite exprs. with no function calls inside
- private val PREPENDPRECONDS : Boolean = true // always instantiate axioms guarded by the precond.
- private val KEEPLETS : Boolean = true // don't expand the lets, instantiate them with the rest
-
- private val cache : MutableMap[(Option[FunDef], Option[Expr]),FunctionTemplate] = MutableMap.empty
-
- def mkTemplate(funDef: FunDef): FunctionTemplate =
- mkTemplate(Some(funDef), funDef.body)
-
- def mkTemplate(body: Expr): FunctionTemplate =
- mkTemplate(None, Some(body))
-
- private def mkTemplate(funDef: Option[FunDef], body : Option[Expr]) : FunctionTemplate = if(cache.isDefinedAt((funDef, body))) {
- cache((funDef, body))
- } else {
- val result = {
- val condVars : MutableSet[Identifier] = MutableSet.empty
- val exprVars : MutableSet[Identifier] = MutableSet.empty
-
- // represents clauses of the form:
- // (~)id => expr && ... && expr
- val guardedExprs : MutableMap[(Identifier,Boolean),Seq[Expr]] = MutableMap.empty
-
- def storeGuarded(guardVar : Identifier, guardPol : Boolean, expr : Expr) : Unit = {
- assert(expr.getType == BooleanType)
- val p : (Identifier,Boolean) = (guardVar,guardPol)
- if(guardedExprs.isDefinedAt(p)) {
- val prev : Seq[Expr] = guardedExprs(p)
- guardedExprs(p) = expr +: prev
- } else {
- guardedExprs(p) = Seq(expr)
- }
- }
-
- def rec(pathVar : Identifier, pathPol : Boolean, expr : Expr) : Expr = {
- expr match {
- case l : Let if(!KEEPLETS) => sys.error("Let's should have been eliminated.")
- case l @ Let(i, e, b) if(KEEPLETS) => {
- val newExpr : Identifier = FreshIdentifier("lt", true).setType(i.getType)
- exprVars += newExpr
- val re = rec(pathVar, pathPol, e)
- storeGuarded(pathVar, pathPol, Equals(Variable(newExpr), re))
- val rb = rec(pathVar, pathPol, replace(Map(Variable(i) -> Variable(newExpr)), b))
- rb
- }
-
- case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
-
- case i @ IfExpr(cond, then, elze) => {
- if(SIMPLERIFS && !containsFunctionCalls(cond) && !containsFunctionCalls(then) && !containsFunctionCalls(elze)) {
- i
- } else {
- val newBool : Identifier = FreshIdentifier("b", true).setType(BooleanType)
- val newExpr : Identifier = FreshIdentifier("e", true).setType(i.getType)
- condVars += newBool
- exprVars += newExpr
-
- val crec = rec(pathVar, pathPol, cond)
- val trec = rec(newBool, true, then)
- val erec = rec(newBool, false, elze)
-
- storeGuarded(pathVar, pathPol, Iff(Variable(newBool), crec))
- storeGuarded(newBool, true, Equals(Variable(newExpr), trec))
- storeGuarded(newBool, false, Equals(Variable(newExpr), erec))
- Variable(newExpr)
- }
- }
-
- case n @ NAryOperator(as, r) => r(as.map(a => rec(pathVar, pathPol, a))).setType(n.getType)
- case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, pathPol, a1), rec(pathVar, pathPol, a2)).setType(b.getType)
- case u @ UnaryOperator(a, r) => r(rec(pathVar, pathPol, a)).setType(u.getType)
- case t : Terminal => t
- }
- }
-
- // The precondition if it exists.
- val prec : Option[Expr] = if(KEEPLETS) {
- funDef.flatMap(_.precondition.map(p => matchToIfThenElse(p)))
- } else {
- funDef.flatMap(_.precondition.map(p => matchToIfThenElse(expandLets(p))))
- }
-
- val newBody : Option[Expr] = if(KEEPLETS) {
- body.map(b => matchToIfThenElse(b))
- } else {
- body.map(b => matchToIfThenElse(expandLets(b)))
- }
-
- val invocation : Option[Expr] = funDef.map(fd => FunctionInvocation(fd, fd.args.map(_.toVariable)))
-
- val invocationEqualsBody : Option[Expr] = (invocation, newBody) match {
- case (Some(inv), Some(body)) =>
- val b : Expr = Equals(inv, body)
-
- Some(if(PREPENDPRECONDS && prec.isDefined) {
- Implies(prec.get, b)
- } else {
- b
- })
-
- case _ =>
- None
- }
-
- val activatingBool : Identifier = FreshIdentifier("start", true).setType(BooleanType)
-
- funDef match {
- case Some(fd) =>
- val finalPred : Option[Expr] = invocationEqualsBody.map(expr => rec(activatingBool, true, expr))
- finalPred.foreach(p => storeGuarded(activatingBool, true, p))
-
- case None =>
- storeGuarded(activatingBool, false, BooleanLiteral(false))
- val newFormula = rec(activatingBool, true, newBody.get)
- storeGuarded(activatingBool, true, newFormula)
- }
-
- // Now the postcondition.
- funDef match {
- case Some(fd) if fd.hasPostcondition =>
- val postHolds : Expr = {
- val post0 : Expr = if(KEEPLETS) {
- matchToIfThenElse(fd.getPostcondition)
- } else {
- matchToIfThenElse(expandLets(fd.getPostcondition))
- }
- val post : Expr = replace(Map(ResultVariable() -> invocation.get), post0)
- if(PREPENDPRECONDS && fd.hasPrecondition) {
- Implies(prec.get, post)
- } else {
- post
- }
- }
- val finalPred2 : Expr = rec(activatingBool, true, postHolds)
- storeGuarded(activatingBool, true, postHolds)
- case _ =>
-
-
- }
-
- new FunctionTemplate(funDef, activatingBool, Set(condVars.toSeq : _*), Set(exprVars.toSeq : _*), Map(guardedExprs.toSeq : _*))
- }
-
- cache((funDef, body)) = result
- result
- }
-}
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index d41a4136f..cdd1ecf4e 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -8,7 +8,7 @@ import java.io.File
* exception of the reporter). */
case class LeonContext(
val settings: Settings = Settings(),
- val options: List[LeonOption] = Nil,
- val files: List[File] = Nil,
+ val options: Seq[LeonOption] = Seq.empty,
+ val files: Seq[File] = Seq.empty,
val reporter: Reporter = new DefaultReporter
)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 1e4592f5e..26477afd3 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -56,7 +56,7 @@ object Main {
sys.exit(1)
}
- def processOptions(reporter: Reporter, args: List[String]) = {
+ def processOptions(reporter: Reporter, args: Seq[String]): LeonContext = {
val phases = allPhases
val allOptions = this.allOptions
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index c5f6c0f7e..d836e5f9e 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -392,6 +392,9 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
// if (id.isLetBinder) {
// scala.sys.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition")
// }
+
+ assert(!this.isInstanceOf[FairZ3Solver], "This should not happen using FairZ3Solver")
+
val newAST = z3.mkFreshConst(id.uniqueName/*name*/, typeToSort(v.getType))
z3Vars = z3Vars + (id -> newAST)
exprToZ3Id += (v -> newAST)
@@ -693,4 +696,8 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
}
}
+ def idToFreshZ3Id(id: Identifier): Z3AST = {
+ z3.mkFreshConst(id.uniqueName, typeToSort(id.getType))
+ }
+
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 49a7c5399..517080077 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -181,25 +181,58 @@ class FairZ3Solver(context : LeonContext)
}
}
+ private val funDefTemplateCache : MutableMap[FunDef, FunctionTemplate] = MutableMap.empty
+ private val exprTemplateCache : MutableMap[Expr , FunctionTemplate] = MutableMap.empty
+
+ private def getTemplate(funDef: FunDef): FunctionTemplate = {
+ funDefTemplateCache.getOrElse(funDef, {
+ val res = FunctionTemplate.mkTemplate(this, funDef, true)
+ funDefTemplateCache += funDef -> res
+ res
+ })
+ }
+
+ private def getTemplate(body: Expr): FunctionTemplate = {
+ exprTemplateCache.getOrElse(body, {
+ val fakeFunDef = new FunDef(FreshIdentifier("fake", true), body.getType, variablesOf(body).toSeq.map(id => VarDecl(id, id.getType)))
+ fakeFunDef.body = Some(body)
+
+ val res = FunctionTemplate.mkTemplate(this, fakeFunDef, false)
+ exprTemplateCache += body -> res
+ res
+ })
+ }
+
class UnrollingBank {
// Keep which function invocation is guarded by which guard with polarity,
// also specify the generation of the blocker
- private val blockersInfo : MutableMap[(Identifier,Boolean), (Int, Z3AST, Set[FunctionInvocation])] = MutableMap.empty
- def currentZ3Blockers = blockersInfo.map(_._2._2)
+ private var blockersInfoStack : List[MutableMap[(Z3AST,Boolean), (Int, Z3AST, Set[Z3FunctionInvocation])]] = List(MutableMap())
+
+ def blockersInfo = blockersInfoStack.head
+
+ def push() {
+ blockersInfoStack = (MutableMap() ++ blockersInfo) :: blockersInfoStack
+ }
+
+ def pop(lvl: Int) {
+ blockersInfoStack = blockersInfoStack.drop(lvl)
+ }
+
+ def z3CurrentZ3Blockers = blockersInfo.map(_._2._2)
def canUnroll = !blockersInfo.isEmpty
- def getBlockersToUnlock: Seq[(Identifier, Boolean)] = {
+ def getZ3BlockersToUnlock: Seq[(Z3AST, Boolean)] = {
val minGeneration = blockersInfo.values.map(_._1).min
blockersInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1)
}
- private def registerBlocker(gen: Int, id: Identifier, pol: Boolean, fis: Set[FunctionInvocation]) {
+ private def registerBlocker(gen: Int, id: Z3AST, pol: Boolean, fis: Set[Z3FunctionInvocation]) {
val pair = (id, pol)
- val z3ast = toZ3Formula(if (pol) Not(Variable(id)) else Variable(id)).get
+ val z3ast = if (pol) z3.mkNot(id) else id
blockersInfo.get(pair) match {
case Some((exGen, _, exFis)) =>
@@ -211,28 +244,42 @@ class FairZ3Solver(context : LeonContext)
}
}
- def scanForNewTemplates(expr: Expr): Seq[Expr] = {
- val tmp = FunctionTemplate.mkTemplate(expr)
+ def scanForNewTemplates(expr: Expr): Seq[Z3AST] = {
+ val template = getTemplate(expr)
- for (((i, p), fis) <- tmp.blockers) {
- registerBlocker(0, i, p, fis)
+ val z3args = for (vd <- template.funDef.args) yield {
+ exprToZ3Id.get(Variable(vd.id)) match {
+ case Some(ast) =>
+ ast
+ case None =>
+ val ast = idToFreshZ3Id(vd.id)
+ exprToZ3Id += Variable(vd.id) -> ast
+ z3IdToExpr += ast -> Variable(vd.id)
+ ast
+ }
}
- tmp.asClauses
+ val (newClauses, newBlocks) = template.instantiate(template.z3ActivatingBool, true, z3args)
+
+ for(((i, p), fis) <- newBlocks) {
+ registerBlocker(1, i, p, fis)
+ }
+
+ newClauses
}
- def unlock(id: Identifier, pol: Boolean) : Seq[Expr] = {
+ def unlock(id: Z3AST, pol: Boolean) : Seq[Z3AST] = {
val pair = (id, pol)
assert(blockersInfo contains pair)
val (gen, _, fis) = blockersInfo(pair)
blockersInfo -= pair
- var newClauses : Seq[Expr] = Seq.empty
+ var newClauses : Seq[Z3AST] = Seq.empty
for(fi <- fis) {
- val temp = FunctionTemplate.mkTemplate(fi.funDef)
- val (newExprs, newBlocks) = temp.instantiate(id, pol, fi.args)
+ val template = getTemplate(fi.funDef)
+ val (newExprs, newBlocks) = template.instantiate(id, pol, fi.args)
for(((i, p), fis) <- newBlocks) {
registerBlocker(gen+1, i, p, fis)
@@ -261,16 +308,16 @@ class FairZ3Solver(context : LeonContext)
}
}
- private var varsInVC = Set[Identifier]()
+ private var varsInVC = Set[Identifier]()
- private var frameGuards = List[Z3AST](z3.mkFreshConst("frame", z3.mkBoolSort))
private var frameExpressions = List[List[Expr]](Nil)
- def entireFormula = And(frameExpressions.flatten)
+ val unrollingBank = new UnrollingBank()
def push() {
- frameGuards = z3.mkFreshConst("frame", z3.mkBoolSort) :: frameGuards
- frameExpressions = Nil :: frameExpressions
+ solver.push()
+ unrollingBank.push()
+ frameExpressions = Nil :: frameExpressions
}
def halt() {
@@ -278,15 +325,9 @@ class FairZ3Solver(context : LeonContext)
}
def pop(lvl: Int = 1) {
- // TODO FIXME : this is wrong if lvl != 1.
- // We could fix it, or change the interface to remove the optional arg.
-
- // We make sure we discard the expressions guarded by this frame
- solver.assertCnstr(z3.mkNot(frameGuards.head))
-
- // Pop the frames
- frameGuards = frameGuards.tail
- frameExpressions = frameExpressions.tail
+ solver.pop(lvl)
+ unrollingBank.pop(lvl)
+ frameExpressions = frameExpressions.drop(lvl)
}
def check: Option[Boolean] = {
@@ -297,16 +338,12 @@ class FairZ3Solver(context : LeonContext)
fairCheck(assumptions)
}
- val unrollingBank = new UnrollingBank()
-
var foundDefinitiveAnswer = false
var definitiveAnswer : Option[Boolean] = None
var definitiveModel : Map[Identifier,Expr] = Map.empty
var definitiveCore : Set[Expr] = Set.empty
def assertCnstr(expression: Expr) {
- val guard = frameGuards.head
-
varsInVC ++= variablesOf(expression)
frameExpressions = (expression :: frameExpressions.head) :: frameExpressions.tail
@@ -314,7 +351,7 @@ class FairZ3Solver(context : LeonContext)
val newClauses = unrollingBank.scanForNewTemplates(expression)
for (cl <- newClauses) {
- solver.assertCnstr(z3.mkImplies(guard, toZ3Formula(cl).get))
+ solver.assertCnstr(cl)
}
}
@@ -330,10 +367,14 @@ class FairZ3Solver(context : LeonContext)
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)
+
def foundAnswer(answer : Option[Boolean], model : Map[Identifier,Expr] = Map.empty, core: Set[Expr] = Set.empty) : Unit = {
foundDefinitiveAnswer = true
definitiveAnswer = answer
@@ -341,19 +382,18 @@ class FairZ3Solver(context : LeonContext)
definitiveCore = core
}
- def z3CoreToCore(core: Seq[Z3AST]): Set[Expr] = {
- val internalAssumptions = frameGuards.toSet
- val userlandAssumptions = core.filterNot(internalAssumptions)
+ // these are the optional sequence of assumption literals
+ val assumptionsAsZ3: Seq[Z3AST] = assumptions.flatMap(toZ3Formula(_)).toSeq
+ val assumptionsAsZ3Set: Set[Z3AST] = assumptionsAsZ3.toSet
- userlandAssumptions.map(ast => fromZ3Formula(null, ast, None) match {
+ def z3CoreToCore(core: Seq[Z3AST]): Set[Expr] = {
+ core.filter(assumptionsAsZ3Set).map(ast => fromZ3Formula(null, ast, None) match {
case n @ Not(Variable(_)) => n
case v @ Variable(_) => v
case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
}).toSet
}
- // these are the optional sequence of assumption literals
- val assumptionsAsZ3: Seq[Z3AST] = frameGuards ++ assumptions.map(toZ3Formula(_).get)
while(!foundDefinitiveAnswer && !forceStop) {
@@ -363,11 +403,13 @@ class FairZ3Solver(context : LeonContext)
reporter.info(" - Running Z3 search...")
//reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
- //reporter.info("UAssumptions:\n"+unrollingBank.currentZ3Blockers.mkString(" && "))
- //reporter.info("Assumptions:\n"+(unrollingBank.currentZ3Blockers ++ assumptionsAsZ3).mkString(" AND "))
+ //reporter.info("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
+ //reporter.info("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
z3Time.start
- val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.currentZ3Blockers) :_*)
+ 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
reporter.info(" - Finished search with blocked literals")
@@ -393,16 +435,19 @@ class FairZ3Solver(context : LeonContext)
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")
- reporter.info("- Found a model:")
- reporter.info(modelAsString)
+ //lazy val modelAsString = model.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
+ //reporter.info("- Found a model:")
+ //reporter.info(modelAsString)
foundAnswer(Some(true), model)
}
case Some(false) if !unrollingBank.canUnroll =>
+
val core = z3CoreToCore(solver.getUnsatCore)
foundAnswer(Some(false), core = core)
@@ -411,9 +456,10 @@ class FairZ3Solver(context : LeonContext)
// distinction is made inside.
case Some(false) =>
- val core = z3CoreToCore(solver.getUnsatCore)
+ //val core = z3CoreToCore(solver.getUnsatCore)
- reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
+ //reporter.info("UNSAT BECAUSE: "+solver.getUnsatCore.mkString(" AND "))
+ //reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
if (!forceStop) {
if (this.feelingLucky) {
@@ -424,7 +470,9 @@ class FairZ3Solver(context : LeonContext)
}
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 {
@@ -443,6 +491,7 @@ class FairZ3Solver(context : LeonContext)
foundAnswer(Some(true), cleanModel)
}
}
+
case None =>
}
}
@@ -454,18 +503,25 @@ class FairZ3Solver(context : LeonContext)
if(!foundDefinitiveAnswer) {
reporter.info("- We need to keep going.")
- val toReleaseAsPairs = unrollingBank.getBlockersToUnlock
+ //val toReleaseAsPairs = unrollingBank.getBlockersToUnlock
+ val toReleaseAsPairs = unrollingBank.getZ3BlockersToUnlock
reporter.info(" - more unrollings")
for((id, polarity) <- toReleaseAsPairs) {
- unrollingTime.start
+ unlockingTime.start
val newClauses = unrollingBank.unlock(id, polarity)
- unrollingTime.stop
+ unlockingTime.stop
+ //reporter.info(" - - Unrolling behind "+(if(!polarity) "¬" else "")+id)
+ //for (cl <- newClauses) {
+ // reporter.info(" - - - "+cl)
+ //}
+ unrollingTime.start
for(ncl <- newClauses) {
- solver.assertCnstr(toZ3Formula(ncl).get)
+ solver.assertCnstr(ncl)
}
+ unrollingTime.stop
}
reporter.info(" - finished unrolling")
@@ -478,6 +534,8 @@ class FairZ3Solver(context : LeonContext)
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
if(forceStop) {
None
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
new file mode 100644
index 000000000..5e4d08d0e
--- /dev/null
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -0,0 +1,213 @@
+package leon
+package solvers.z3
+
+import z3.scala._
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Definitions._
+
+import scala.collection.mutable.{Set=>MutableSet,Map=>MutableMap}
+
+case class Z3FunctionInvocation(funDef: FunDef, args: Seq[Z3AST])
+
+// TODO: maybe a candidate for moving into purescala package?
+class FunctionTemplate private(
+ solver: AbstractZ3Solver,
+ val funDef : FunDef,
+ activatingBool : Identifier,
+ condVars : Set[Identifier],
+ exprVars : Set[Identifier],
+ guardedExprs : Map[(Identifier,Boolean),Seq[Expr]]) {
+
+ private val z3 = solver.z3
+
+ private val asClauses : Seq[Expr] = {
+ (for(((b,p),es) <- guardedExprs; e <- es) yield {
+ Implies(if(!p) Not(Variable(b)) else Variable(b), e)
+ }).toSeq
+ }
+
+ val z3ActivatingBool = solver.idToFreshZ3Id(activatingBool)
+
+ private val z3FunDefArgs = funDef.args.map( ad => solver.idToFreshZ3Id(ad.id))
+
+ private val zippedCondVars = condVars.map(id => (id, solver.idToFreshZ3Id(id)))
+ private val zippedExprVars = exprVars.map(id => (id, solver.idToFreshZ3Id(id)))
+ private val zippedFunDefArgs = funDef.args.map(_.id) zip z3FunDefArgs
+
+ val idToZ3Ids: Map[Identifier, Z3AST] = {
+ Map(activatingBool -> z3ActivatingBool) ++
+ zippedCondVars ++
+ zippedExprVars ++
+ zippedFunDefArgs
+ }
+
+ val asZ3Clauses: Seq[Z3AST] = asClauses.map(solver.toZ3Formula(_, idToZ3Ids).get)
+
+ private val blockers : Map[(Identifier,Boolean),Set[FunctionInvocation]] = {
+ val idCall = FunctionInvocation(funDef, funDef.args.map(_.toVariable))
+
+ Map((for((p, es) <- guardedExprs) yield {
+ val calls = es.foldLeft(Set.empty[FunctionInvocation])((s,e) => s ++ functionCallsOf(e)) - idCall
+ if(calls.isEmpty) {
+ None
+ } else {
+ Some((p, calls))
+ }
+ }).flatten.toSeq : _*)
+ }
+
+ val z3Blockers: Map[(Z3AST, Boolean), Set[Z3FunctionInvocation]] = blockers.map {
+ case ((b, p), funs) => ((idToZ3Ids(b), p) -> funs.map(fi => Z3FunctionInvocation(fi.funDef, fi.args.map(solver.toZ3Formula(_, idToZ3Ids).get))))
+ }
+
+ def instantiate(aVar : Z3AST, aPol : Boolean, args : Seq[Z3AST]) : (Seq[Z3AST], Map[(Z3AST, Boolean), Set[Z3FunctionInvocation]]) = {
+ assert(args.size == funDef.args.size)
+
+ val idSubstMap : Map[Z3AST, Z3AST] =
+ Map(z3ActivatingBool -> (if (aPol) aVar else z3.mkNot(aVar))) ++
+ (zippedExprVars ++ zippedCondVars).map{ case (id, c) => c -> solver.idToFreshZ3Id(id) } ++
+ (z3FunDefArgs zip args)
+
+ val (from, to) = idSubstMap.unzip
+ val (fromArray, toArray) = (from.toArray, to.toArray)
+
+ val newClauses = asZ3Clauses.map(z3.substitute(_, fromArray, toArray))
+ val newBlockers = z3Blockers.map { case ((b, p), funs) =>
+ val bp = if (b == z3ActivatingBool) {
+ (aVar, p == aPol)
+ } else {
+ (idSubstMap(b), p)
+ }
+
+ val newFuns = funs.map(fi => fi.copy(args = fi.args.map(z3.substitute(_, fromArray, toArray))))
+
+ bp -> newFuns
+ }
+
+ (newClauses, newBlockers)
+ }
+
+ override def toString : String = {
+ "Template for def " + funDef.id + "(" + funDef.args.map(a => a.id + " : " + a.tpe).mkString(", ") + ") : " + funDef.returnType + " is :\n" +
+ " * Activating boolean : " + activatingBool + "\n" +
+ " * Control booleans : " + condVars.toSeq.map(_.toString).mkString(", ") + "\n" +
+ " * Expression vars : " + exprVars.toSeq.map(_.toString).mkString(", ") + "\n" +
+ " * \"Clauses\" : " + "\n " + asClauses.mkString("\n ") + "\n" +
+ " * Block-map : " + blockers.toString
+ }
+}
+
+object FunctionTemplate {
+ def mkTemplate(solver: AbstractZ3Solver, funDef: FunDef, isRealFunDef : Boolean = true) : FunctionTemplate = {
+ val condVars : MutableSet[Identifier] = MutableSet.empty
+ val exprVars : MutableSet[Identifier] = MutableSet.empty
+
+ // represents clauses of the form:
+ // (~)id => expr && ... && expr
+ val guardedExprs : MutableMap[(Identifier,Boolean),Seq[Expr]] = MutableMap.empty
+
+ def storeGuarded(guardVar : Identifier, guardPol : Boolean, expr : Expr) : Unit = {
+ assert(expr.getType == BooleanType)
+ val p : (Identifier,Boolean) = (guardVar,guardPol)
+ if(guardedExprs.isDefinedAt(p)) {
+ val prev : Seq[Expr] = guardedExprs(p)
+ guardedExprs(p) = expr +: prev
+ } else {
+ guardedExprs(p) = Seq(expr)
+ }
+ }
+
+ def rec(pathVar : Identifier, pathPol : Boolean, expr : Expr) : Expr = {
+ expr match {
+ case l @ Let(i, e, b) =>
+ val newExpr : Identifier = FreshIdentifier("lt", true).setType(i.getType)
+ exprVars += newExpr
+ val re = rec(pathVar, pathPol, e)
+ storeGuarded(pathVar, pathPol, Equals(Variable(newExpr), re))
+ val rb = rec(pathVar, pathPol, replace(Map(Variable(i) -> Variable(newExpr)), b))
+ rb
+
+ case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
+
+ case i @ IfExpr(cond, then, elze) => {
+ if(!containsFunctionCalls(cond) && !containsFunctionCalls(then) && !containsFunctionCalls(elze)) {
+ i
+ } else {
+ val newBool : Identifier = FreshIdentifier("b", true).setType(BooleanType)
+ val newExpr : Identifier = FreshIdentifier("e", true).setType(i.getType)
+ condVars += newBool
+ exprVars += newExpr
+
+ val crec = rec(pathVar, pathPol, cond)
+ val trec = rec(newBool, true, then)
+ val erec = rec(newBool, false, elze)
+
+ storeGuarded(pathVar, pathPol, Iff(Variable(newBool), crec))
+ storeGuarded(newBool, true, Equals(Variable(newExpr), trec))
+ storeGuarded(newBool, false, Equals(Variable(newExpr), erec))
+ Variable(newExpr)
+ }
+ }
+
+ case n @ NAryOperator(as, r) => r(as.map(a => rec(pathVar, pathPol, a))).setType(n.getType)
+ case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, pathPol, a1), rec(pathVar, pathPol, a2)).setType(b.getType)
+ case u @ UnaryOperator(a, r) => r(rec(pathVar, pathPol, a)).setType(u.getType)
+ case t : Terminal => t
+ }
+ }
+
+ // The precondition if it exists.
+ val prec : Option[Expr] = funDef.precondition.map(p => matchToIfThenElse(p))
+
+ val newBody : Option[Expr] = funDef.body.map(b => matchToIfThenElse(b))
+
+ val invocation : Expr = FunctionInvocation(funDef, funDef.args.map(_.toVariable))
+
+ val invocationEqualsBody : Option[Expr] = newBody match {
+ case Some(body) if isRealFunDef =>
+ val b : Expr = Equals(invocation, body)
+
+ Some(if(prec.isDefined) {
+ Implies(prec.get, b)
+ } else {
+ b
+ })
+
+ case _ =>
+ None
+ }
+
+ val activatingBool : Identifier = FreshIdentifier("start", true).setType(BooleanType)
+
+ if (isRealFunDef) {
+ val finalPred : Option[Expr] = invocationEqualsBody.map(expr => rec(activatingBool, true, expr))
+ finalPred.foreach(p => storeGuarded(activatingBool, true, p))
+ } else {
+ storeGuarded(activatingBool, false, BooleanLiteral(false))
+ val newFormula = rec(activatingBool, true, newBody.get)
+ storeGuarded(activatingBool, true, newFormula)
+ }
+
+ // Now the postcondition.
+ if (funDef.hasPostcondition) {
+ val post0 : Expr = matchToIfThenElse(funDef.getPostcondition)
+ val post : Expr = replace(Map(ResultVariable() -> invocation), post0)
+
+ val postHolds : Expr =
+ if(funDef.hasPrecondition) {
+ Implies(prec.get, post)
+ } else {
+ post
+ }
+
+ val finalPred2 : Expr = rec(activatingBool, true, postHolds)
+ storeGuarded(activatingBool, true, postHolds)
+ }
+
+ new FunctionTemplate(solver, funDef, activatingBool, Set(condVars.toSeq : _*), Set(exprVars.toSeq : _*), Map(guardedExprs.toSeq : _*))
+ }
+}
diff --git a/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
similarity index 59%
rename from src/test/scala/leon/benchmark/SynthesisBenchmarks.scala
rename to src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 5ede05a1a..f5cd758c4 100644
--- a/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -1,4 +1,4 @@
-package leon.benchmark
+package leon.synthesis.utils
import leon._
import leon.purescala.Definitions._
@@ -7,23 +7,53 @@ import leon.purescala.TreeOps._
import leon.solvers.z3._
import leon.solvers.Solver
import leon.synthesis._
-import leon.test.synthesis._
+
+import java.util.Date
+import java.text.SimpleDateFormat
+
+import sys.process._
import java.io.File
-object SynthesisBenchmarks extends App {
+object Benchmarks extends App {
- private def forEachFileIn(dirName : String)(block : File=>Unit) {
- import scala.collection.JavaConversions._
+ val allRules = Rules.all ++ Heuristics.all
- for(f <- (new File(dirName)).listFiles() if f.getPath().endsWith(".scala")) {
- block(f)
- }
+ var rule: Rule = rules.CEGIS
+
+ // Parse arguments
+ val (options, others) = args.partition(_.startsWith("--"))
+
+ val newOptions = options flatMap {
+ case setting if setting.startsWith("--rule=") =>
+ val name = setting.drop(7)
+
+ allRules.find(_.name.toLowerCase == name.toLowerCase) match {
+ case Some(r) =>
+ rule = r
+ case None =>
+ println("Could not find rule: "+name)
+ println("Available rules: ")
+ for (r <- allRules) {
+ println(" - "+r.name)
+ }
+ sys.exit(1);
+ }
+
+ None
+
+ case setting =>
+ Some(setting)
}
+ println("# Date: "+new SimpleDateFormat("dd.MM.yyyy HH:mm:ss").format(new Date()))
+ println("# Git tree: "+("git log -1 --format=\"%H\"".!!).trim)
+ println("# Using rule: "+rule.name)
+
+
val infoSep : String = "╟" + ("┄" * 86) + "╢"
val infoFooter : String = "â•š" + ("â•" * 86) + "â•"
- val infoHeader : String = ". ┌────────────â”\n" +
+ val infoHeader : String = " ┌────────────â”\n" +
"â•”â•â•¡ Benchmarks â•ž" + ("â•" * 71) + "â•—\n" +
"║ └────────────┘" + (" " * 71) + "║"
@@ -41,33 +71,26 @@ object SynthesisBenchmarks extends App {
var nSuccessTotal, nInnapTotal, nDecompTotal, nAltTotal = 0
var tTotal: Long = 0
- for (path <- args) {
- val file = new File(path)
+ val ctx = leon.Main.processOptions(new DefaultReporter, others ++ newOptions)
- val ctx = LeonContext(
- settings = Settings(
- synthesis = true,
- xlang = false,
- verify = false
- ),
- files = List(file),
- reporter = new DefaultReporter
- )
+ for (file <- ctx.files) {
+ val innerCtx = ctx.copy(files = List(file))
val opts = SynthesizerOptions()
- val pipeline = leon.plugin.ExtractionPhase andThen ExtractProblemsPhase
+ val pipeline = leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
+
+ val (results, solver) = pipeline.run(innerCtx)(file.getPath :: Nil)
- val (results, solver) = pipeline.run(ctx)(file.getPath :: Nil)
val sctx = SynthesisContext(solver, new DefaultReporter, new java.util.concurrent.atomic.AtomicBoolean)
- for ((f, ps) <- results; p <- ps) {
+ for ((f, ps) <- results.toSeq.sortBy(_._1.id.toString); p <- ps) {
val ts = System.currentTimeMillis
- val rr = rules.CEGIS.instantiateOn(sctx, p)
-
+ val rr = rule.instantiateOn(sctx, p)
+
val nAlt = rr.size
var nSuccess, nInnap, nDecomp = 0
@@ -103,7 +126,7 @@ object SynthesisBenchmarks extends App {
println
- val infoHeader2 : String = ". ┌────────────â”\n" +
+ val infoHeader2 : String = " ┌────────────â”\n" +
"â•”â•â•¡ Timers â•ž" + ("â•" * 71) + "â•—\n" +
"║ └────────────┘" + (" " * 71) + "║"
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
new file mode 100644
index 000000000..d875118df
--- /dev/null
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -0,0 +1,45 @@
+package leon
+package synthesis
+package utils
+
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.Definitions._
+import solvers.z3._
+import solvers.Solver
+
+object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Map[FunDef, Seq[Problem]], Solver)] {
+ val name = "Synthesis Problem Extraction"
+ val description = "Synthesis Problem Extraction"
+
+ def run(ctx: LeonContext)(p: Program): (Map[FunDef, Seq[Problem]], Solver) = {
+
+ val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
+ val mainSolver = new FairZ3Solver(silentContext)
+ mainSolver.setProgram(p)
+
+ var results = Map[FunDef, Seq[Problem]]()
+ def noop(u:Expr, u2: Expr) = u
+
+
+ def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
+ case ch @ Choose(vars, pred) =>
+ val problem = Problem.fromChoose(ch)
+
+ results += f -> (results.getOrElse(f, Seq()) :+ problem)
+
+ a
+ case _ =>
+ a
+ }
+
+ // Look for choose()
+ for (f <- p.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
+ treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
+ }
+
+ (results, mainSolver)
+ }
+
+}
+
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 65e8dcce5..07fe90ae7 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -149,12 +149,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
report
}
- // We generate all function templates in advance.
- for(funDef <- program.definedFunctions if funDef.hasImplementation) {
- // this gets cached :D
- FunctionTemplate.mkTemplate(funDef)
- }
-
val report = if(solvers.size > 1) {
reporter.info("Running verification condition generation...")
checkVerificationConditions(generateVerificationConditions)
diff --git a/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
similarity index 70%
rename from src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
rename to src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index c40844ce6..80e4bd133 100644
--- a/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -7,47 +7,13 @@ import leon.purescala.TreeOps._
import leon.solvers.z3._
import leon.solvers.Solver
import leon.synthesis._
+import leon.synthesis.utils._
import org.scalatest.FunSuite
import org.scalatest.matchers.ShouldMatchers._
import java.io.{BufferedWriter, FileWriter, File}
-object ExtractProblemsPhase extends LeonPhase[Program, (Map[FunDef, Seq[Problem]], Solver)] {
- val name = "Synthesis Problem Extraction"
- val description = "Synthesis Problem Extraction"
-
- def run(ctx: LeonContext)(p: Program): (Map[FunDef, Seq[Problem]], Solver) = {
-
- val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
- val mainSolver = new FairZ3Solver(silentContext)
- mainSolver.setProgram(p)
-
- var results = Map[FunDef, Seq[Problem]]()
- def noop(u:Expr, u2: Expr) = u
-
-
- def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
- case ch @ Choose(vars, pred) =>
- val problem = Problem.fromChoose(ch)
-
- results += f -> (results.getOrElse(f, Seq()) :+ problem)
-
- a
- case _ =>
- a
- }
-
- // Look for choose()
- for (f <- p.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
- treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
- }
-
- (results, mainSolver)
- }
-
-}
-
class SynthesisSuite extends FunSuite {
private var counter : Int = 0
private def nextInt() : Int = {
@@ -69,7 +35,7 @@ class SynthesisSuite extends FunSuite {
val opts = SynthesizerOptions()
- val pipeline = leon.plugin.TemporaryInputPhase andThen leon.plugin.ExtractionPhase andThen ExtractProblemsPhase
+ val pipeline = leon.plugin.TemporaryInputPhase andThen leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
val (results, solver) = pipeline.run(ctx)((content, Nil))
diff --git a/testcases/synthesis/CegisExamples.scala b/testcases/synthesis/CegisExamples.scala
new file mode 100644
index 000000000..a7f23e817
--- /dev/null
+++ b/testcases/synthesis/CegisExamples.scala
@@ -0,0 +1,24 @@
+import leon.Utils._
+
+object CegisTests {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ // proved with unrolling=0
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil() => Set()
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def cegis1(a: Int) = choose { x: List => size(x) == 1 && content(x) == Set(a) }
+ def cegis2(a: Int) = choose { x: List => size(x) == 2 && content(x) == Set(a) }
+ def cegis3(a: Int) = choose { x: List => size(x) == 3 && content(x) == Set(a) }
+ def cegis4(a: Int) = choose { x: List => size(x) == 4 && content(x) == Set(a) }
+ def cegis5(a: Int) = choose { x: List => size(x) == 5 && content(x) == Set(a) }
+}
--
GitLab