From 3914a9a09592aa30f30c0d26978d872721def35c Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 9 Feb 2016 11:49:30 +0100
Subject: [PATCH] CEGIS: Skip CE search if all programs have been excluded.
Also some fixes
---
.../leon/synthesis/rules/CEGISLike.scala | 92 +++++--------------
1 file changed, 21 insertions(+), 71 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 4a0a315d7..a5fceaad8 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -102,11 +102,11 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
* b3 => c6 == H(c4, c5)
*
* c1 -> Seq(
- * (b1, F(c2, c3), Set(c2, c3))
- * (b2, G(c4, c5), Set(c4, c5))
+ * (b1, F(_, _), Seq(c2, c3))
+ * (b2, G(_, _), Seq(c4, c5))
* )
* c6 -> Seq(
- * (b3, H(c7, c8), Set(c7, c8))
+ * (b3, H(_, _), Seq(c7, c8))
* )
*/
private var cTree: Map[Identifier, Seq[(Identifier, Seq[Expr] => Expr, Seq[Identifier])]] = Map()
@@ -198,6 +198,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
}
bsOrdered = bs.toSeq.sorted
+ excludedPrograms = ArrayBuffer()
setCExpr(computeCExpr())
ctx.timers.synthesis.cegis.updateCTree.stop()
@@ -250,44 +251,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
SeqUtils.cartesianProduct(seqs).map(_.flatten.toSet)
}
- def redundant(e: Expr): Boolean = {
- val (op1, op2) = e match {
- case Minus(o1, o2) => (o1, o2)
- case Modulo(o1, o2) => (o1, o2)
- case Division(o1, o2) => (o1, o2)
- case BVMinus(o1, o2) => (o1, o2)
- case BVRemainder(o1, o2) => (o1, o2)
- case BVDivision(o1, o2) => (o1, o2)
-
- case And(Seq(Not(o1), Not(o2))) => (o1, o2)
- case And(Seq(Not(o1), o2)) => (o1, o2)
- case And(Seq(o1, Not(o2))) => (o1, o2)
- case And(Seq(o1, o2)) => (o1, o2)
-
- case Or(Seq(Not(o1), Not(o2))) => (o1, o2)
- case Or(Seq(Not(o1), o2)) => (o1, o2)
- case Or(Seq(o1, Not(o2))) => (o1, o2)
- case Or(Seq(o1, o2)) => (o1, o2)
-
- case SetUnion(o1, o2) => (o1, o2)
- case SetIntersection(o1, o2) => (o1, o2)
- case SetDifference(o1, o2) => (o1, o2)
-
- case Equals(Not(o1), Not(o2)) => (o1, o2)
- case Equals(Not(o1), o2) => (o1, o2)
- case Equals(o1, Not(o2)) => (o1, o2)
- case Equals(o1, o2) => (o1, o2)
- case _ => return false
- }
-
- op1 == op2
- }
-
- allProgramsFor(Seq(rootC))/* filterNot { bs =>
- val res = params.optimizations && exists(redundant)(getExpr(bs))
- if (!res) excludeProgram(bs, false)
- res
- }*/
+ allProgramsFor(Seq(rootC))
}
private def debugCTree(cTree: Map[Identifier, Seq[(Identifier, Seq[Expr] => Expr, Seq[Identifier])]],
@@ -377,8 +341,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
Lambda(p.xs.map(ValDef), p.phi)
)
-
- phiFd.body = Some(
+ phiFd.body = Some(
letTuple(p.xs,
FunctionInvocation(cTreeFd.typed, p.as.map(_.toVariable)),
p.phi)
@@ -566,6 +529,8 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
var excludedPrograms = ArrayBuffer[Set[Identifier]]()
+ def allProgramsClosed = allProgramsCount() <= excludedPrograms.size
+
// Explicitly remove program computed by bValues from the search space
//
// If the bValues comes from models, we make sure the bValues we exclude
@@ -825,18 +790,12 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
if (hasInputExamples) {
timers.filter.start()
for (bs <- prunedPrograms if !interruptManager.isInterrupted) {
- var valid = true
val examples = allInputExamples()
- while(valid && examples.hasNext) {
- val e = examples.next()
- if (!ndProgram.testForProgram(bs)(e)) {
- failedTestsStats(e) += 1
- sctx.reporter.debug(f" Program: ${ndProgram.getExpr(bs).asString}%-80s failed on: ${e.asString}")
- wrongPrograms += bs
- prunedPrograms -= bs
-
- valid = false
- }
+ examples.find(e => !ndProgram.testForProgram(bs)(e)).foreach { e =>
+ failedTestsStats(e) += 1
+ sctx.reporter.debug(f" Program: ${ndProgram.getExpr(bs).asString}%-80s failed on: ${e.asString}")
+ wrongPrograms += bs
+ prunedPrograms -= bs
}
if (wrongPrograms.size+1 % 1000 == 0) {
@@ -850,14 +809,6 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val nTotal = ndProgram.allProgramsCount()
//println(s"Iotal: $nTotal, passing: $nPassing")
- /*locally {
- val progs = ndProgram.allPrograms() map ndProgram.getExpr
- val ground = progs count isGround
- println("Programs")
- progs take 100 foreach println
- println(s"$ground ground out of $nTotal")
- }*/
-
sctx.reporter.debug(s"#Programs passing tests: $nPassing out of $nTotal")
sctx.reporter.ifDebug{ printer =>
for (p <- prunedPrograms.take(100)) {
@@ -898,14 +849,11 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val newCexs = cexs.map(InExample)
baseExampleInputs ++= newCexs
// Retest whether the newly found C-E invalidates some programs
- for (p <- otherPrograms) {
- // Exclude any programs that fail the new cex's
- var valid = true
- newCexs.takeWhile(_ => valid).foreach { cex =>
- if (!ndProgram.testForProgram(p)(cex)) {
- ndProgram.excludeProgram(p, true)
- valid = false
- }
+ for (p <- otherPrograms if !interruptManager.isInterrupted) {
+ // Exclude any programs that fail at least one new cex
+ newCexs.find { cex => !ndProgram.testForProgram(p)(cex) }.foreach { cex =>
+ failedTestsStats(cex) += 1
+ ndProgram.excludeProgram(p, true)
}
}
// If we excluded all programs, we can skip CE search
@@ -921,7 +869,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
}
// CEGIS Loop at a given unfolding level
- while (result.isEmpty && !skipCESearch && !interruptManager.isInterrupted) {
+ while (result.isEmpty && !skipCESearch && !interruptManager.isInterrupted && !ndProgram.allProgramsClosed) {
timers.loop.start()
ndProgram.solveForTentativeProgram() match {
case Some(Some(bs)) =>
@@ -968,12 +916,14 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
case None =>
result = Some(RuleFailed())
}
+
timers.loop.stop()
}
unfolding += 1
} while(unfolding <= maxSize && result.isEmpty && !interruptManager.isInterrupted)
+ if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
result.getOrElse(RuleFailed())
} catch {
--
GitLab