diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 77b451094ae1451ce7e46c9e3312488c7c398058..1dfddd0ca025caf3c7faafce3904c304be362f43 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -4,7 +4,6 @@ package synthesis
import purescala.Definitions._
import purescala.Expressions._
import purescala.Constructors._
-import evaluators._
import purescala.Common._
import repair._
import leon.utils.ASCIIHelpers._
@@ -175,9 +174,7 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
}
def filterIns(expr: Expr): ExamplesBank = {
- val ev = new DefaultEvaluator(hctx.sctx.context, hctx.sctx.program)
-
- filterIns(m => ev.eval(expr, m).result == Some(BooleanLiteral(true)))
+ filterIns(m => hctx.sctx.defaultEvaluator.eval(expr, m).result == Some(BooleanLiteral(true)))
}
def filterIns(pred: Map[Identifier, Expr] => Boolean): ExamplesBank = {
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index bb90d2a268411c44e9dfdbde013886b7db5b56d9..b01077ce751f6b53e397b15eb3d5126e560d1b56 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -6,6 +6,7 @@ package synthesis
import solvers._
import solvers.combinators._
import purescala.Definitions.{Program, FunDef}
+import evaluators._
/**
* This is global information per entire search, contains necessary information
@@ -22,6 +23,10 @@ case class SynthesisContext(
val rules = settings.rules
val solverFactory = SolverFactory.getFromSettings(context, program)
+
+ lazy val defaultEvaluator = {
+ new DefaultEvaluator(context, program)
+ }
}
object SynthesisContext {
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index f3fa5947d0c8cb8092f9d8fc032ca71c12cc2846..4b70832e97ec60123f58f2576f76f2e22725778e 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -43,14 +43,15 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val sctx = hctx.sctx
val ctx = sctx.context
+ val timings = ctx.timers.synthesis.rules.get(name)
// CEGIS Flags to activate or deactivate features
val useOptTimeout = sctx.settings.cegisUseOptTimeout.getOrElse(true)
val useVanuatoo = sctx.settings.cegisUseVanuatoo.getOrElse(false)
- val useShrink = sctx.settings.cegisUseShrink.getOrElse(true)
+ val useShrink = sctx.settings.cegisUseShrink.getOrElse(false)
// Limits the number of programs CEGIS will specifically validate individually
- val validateUpTo = 5
+ val validateUpTo = 0
// Shrink the program when the ratio of passing cases is less than the threshold
val shrinkThreshold = 1.0/2
@@ -513,19 +514,26 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
* First phase of CEGIS: solve for potential programs (that work on at least one input)
*/
def solveForTentativeProgram(): Option[Option[Set[Identifier]]] = {
+ timings.get("Solving for tentative").start();
val solverf = SolverFactory.default(ctx, programCTree).withTimeout(exSolverTo)
val solver = solverf.getNewSolver()
val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
//debugCExpr(cTree)
+ println("Program: ")
+ println("-"*80)
+ println(programCTree.asString)
+
//println(" --- PhiFD ---")
//println(phiFd.fullBody.asString(ctx))
val toFind = and(innerPc, cnstr)
- //println(" --- Constraints ---")
- //println(" - "+toFind)
+ println(" --- Constraints ---")
+ println(" - "+toFind.asString)
try {
- solver.assertCnstr(andJoin(bsOrdered.map(b => if (bs(b)) b.toVariable else Not(b.toVariable))))
+ //TODO: WHAT THE F IS THIS?
+ //val bsOrNotBs = andJoin(bsOrdered.map(b => if (bs(b)) b.toVariable else Not(b.toVariable)))
+ //solver.assertCnstr(bsOrNotBs)
solver.assertCnstr(toFind)
for ((c, alts) <- cTree) {
@@ -565,11 +573,12 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val bModel = bs.filter(b => model.get(b).contains(BooleanLiteral(true)))
- //println("Tentative expr: "+getExpr(bModel))
+ println("Tentative model: "+bModel)
+ println("Tentative expr: "+getExpr(bModel))
Some(Some(bModel))
case Some(false) =>
- //println("UNSAT!")
+ println("UNSAT!")
Some(None)
case None =>
@@ -582,6 +591,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
Some(None)
}
} finally {
+ timings.get("Solving for tentative").stop();
solverf.reclaim(solver)
solverf.shutdown()
}
@@ -591,6 +601,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
* Second phase of CEGIS: verify a given program by looking for CEX inputs
*/
def solveForCounterExample(bs: Set[Identifier]): Option[Option[Seq[Expr]]] = {
+ timings.get("Solving for cex").start();
+
val solverf = SolverFactory.default(ctx, programCTree).withTimeout(cexSolverTo)
val solver = solverf.getNewSolver()
val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
@@ -615,6 +627,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
None
}
} finally {
+ timings.get("Solving for cex").stop();
solverf.reclaim(solver)
solverf.shutdown()
}
@@ -623,6 +636,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
+ timings.get("Prefix").start()
var result: Option[RuleApplication] = None
val sctx = hctx.sctx
implicit val ctx = sctx.context
@@ -718,6 +732,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
gi.iterator
}
+ timings.get("Prefix").stop()
+ timings.get("Main Block").start();
try {
do {
var skipCESearch = false
@@ -749,6 +765,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
for (bs <- prunedPrograms if !interruptManager.isInterrupted) {
var valid = true
val examples = allInputExamples()
+ timings.get("Testing").start()
while(valid && examples.hasNext) {
val e = examples.next()
if (!ndProgram.testForProgram(bs)(e)) {
@@ -760,6 +777,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
valid = false
}
}
+ timings.get("Testing").stop()
if (wrongPrograms.size+1 % 1000 == 0) {
sctx.reporter.debug("..."+wrongPrograms.size)
@@ -795,6 +813,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
var doFilter = true
if (validateUpTo > 0) {
+ timings.get("Validating first N").start()
// Validate the first N programs individualy
ndProgram.validatePrograms(prunedPrograms.take(validateUpTo)) match {
case Left(sols) if sols.nonEmpty =>
@@ -810,18 +829,20 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
skipCESearch = true
}
}
+ timings.get("Validating first N").stop()
}
if (doFilter && !(nPassing < nInitial * shrinkThreshold && useShrink)) {
+ sctx.reporter.debug("Excluding "+wrongPrograms.size+" programs")
wrongPrograms.foreach {
ndProgram.excludeProgram
}
}
}
+ timings.get("Loop").start()
// CEGIS Loop at a given unfolding level
while (result.isEmpty && !skipCESearch && !interruptManager.isInterrupted) {
-
ndProgram.solveForTentativeProgram() match {
case Some(Some(bs)) =>
// Should we validate this program with Z3?
@@ -833,6 +854,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// make sure by validating this candidate with z3
true
} else {
+ println("testing failed ?!")
// One valid input failed with this candidate, we can skip
ndProgram.excludeProgram(bs)
false
@@ -841,10 +863,12 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// No inputs or capability to test, we need to ask Z3
true
}
+ sctx.reporter.debug("Found tentative model (Validate="+validateWithZ3+")!")
if (validateWithZ3) {
ndProgram.solveForCounterExample(bs) match {
case Some(Some(inputsCE)) =>
+ sctx.reporter.debug("Found counter-example:"+inputsCE)
val ce = InExample(inputsCE)
// Found counter example!
baseExampleInputs += ce
@@ -863,6 +887,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
case None =>
// We are not sure
+ sctx.reporter.debug("Unknown")
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")
@@ -881,6 +906,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
result = Some(RuleFailed())
}
}
+ timings.get("Loop").stop()
unfolding += 1
} while(unfolding <= maxUnfoldings && result.isEmpty && !interruptManager.isInterrupted)
@@ -892,6 +918,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
e.printStackTrace()
RuleFailed()
+ } finally {
+ timings.get("Main Block").stop();
}
}
})
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 8925276af63069f78cab842142ab80b74b2f648c..ed8a285ff3f0a52a61760598ac742013d0e77f5d 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -43,7 +43,6 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
candidates.flatMap {
case List(a1, a2) =>
-
val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc),
eb = p.qeb.filterIns(LessThan(Variable(a1), Variable(a2))))
val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc),
diff --git a/testcases/synthesis/etienne-thesis/List/Delete.scala b/testcases/synthesis/etienne-thesis/List/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..46f0710878d25a30e679f034ff07f985078950d1
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Delete.scala
@@ -0,0 +1,41 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Delete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ //def delete(in1: List, v: BigInt): List = {
+ // in1 match {
+ // case Cons(h,t) =>
+ // if (h == v) {
+ // delete(t, v)
+ // } else {
+ // Cons(h, delete(t, v))
+ // }
+ // case Nil =>
+ // Nil
+ // }
+ //} ensuring { content(_) == content(in1) -- Set(v) }
+
+ def delete(in1: List, v: BigInt) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- Set(v)
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Diff.scala b/testcases/synthesis/etienne-thesis/List/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9b452ed7f7b8816d4e87b3d9044e40e1347d3492
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Diff.scala
@@ -0,0 +1,59 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Diff {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def delete(in1: List, v: BigInt): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ def union(in1: List, in2: List): List = {
+ in1 match {
+ case Cons(h, t) =>
+ Cons(h, union(t, in2))
+ case Nil =>
+ in2
+ }
+ } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ // def diff(in1: List, in2: List): List = {
+ // in2 match {
+ // case Nil =>
+ // in1
+ // case Cons(h, t) =>
+ // diff(delete(in1, h), t)
+ // }
+ // } ensuring { content(_) == content(in1) -- content(in2) }
+
+ def diff(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- content(in2)
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Insert.scala b/testcases/synthesis/etienne-thesis/List/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6da044ca346e0cb95e194bdf42897f5f066ec23c
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Insert.scala
@@ -0,0 +1,28 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Insert {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ //def insert(in1: List, v: BigInt): List = {
+ // Cons(v, in1)
+ //} ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def insert(in1: List, v: BigInt) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ Set(v)
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Split.scala b/testcases/synthesis/etienne-thesis/List/Split.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1f709a8669c047ecc300c0d78e558cb4bb720b90
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Split.scala
@@ -0,0 +1,101 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ //def insert(in1: List, v: BigInt) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) ++ Set(v)
+ //}
+
+ def delete(in1: List, v: BigInt): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ //def delete(in1: List, v: BigInt) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) -- Set(v)
+ //}
+
+ def union(in1: List, in2: List): List = {
+ in1 match {
+ case Cons(h, t) =>
+ Cons(h, union(t, in2))
+ case Nil =>
+ in2
+ }
+ } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ //def union(in1: List, in2: List) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) ++ content(in2)
+ //}
+
+ def diff(in1: List, in2: List): List = {
+ in2 match {
+ case Nil =>
+ in1
+ case Cons(h, t) =>
+ diff(delete(in1, h), t)
+ }
+ } ensuring { content(_) == content(in1) -- content(in2) }
+
+ //def diff(in1: List, in2: List) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) -- content(in2)
+ //}
+
+ def splitSpec(list : List, res : (List,List)) : Boolean = {
+
+ val s1 = size(res._1)
+ val s2 = size(res._2)
+ abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+ content(res._1) ++ content(res._2) == content(list)
+ }
+
+ def abs(i : BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ // def split(list : List) : (List,List) = (list match {
+ // case Nil => (Nil, Nil)
+ // case Cons(x, Nil) => (Cons(x, Nil), Nil)
+ // case Cons(x1, Cons(x2, xs)) =>
+ // val (s1,s2) = split(xs)
+ // (Cons(x1, s1), Cons(x2, s2))
+ // }) ensuring(res => splitSpec(list, res))
+
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Union.scala b/testcases/synthesis/etienne-thesis/List/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b170648665dad909abac2e3978b8675355195cde
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Union.scala
@@ -0,0 +1,50 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Union {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def delete(in1: List, v: BigInt): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ // def union(in1: List, in2: List): List = {
+ // in1 match {
+ // case Cons(h, t) =>
+ // Cons(h, union(t, in2))
+ // case Nil =>
+ // in2
+ // }
+ // } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ content(in2)
+ }
+}