From 41a143ae4c05a07d5ec05edf645149fabf23e801 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 6 Jul 2015 13:00:58 +0200
Subject: [PATCH] Test -> Example
---
src/main/scala/leon/repair/Repairman.scala | 30 ++++++------
src/main/scala/leon/repair/rules/Focus.scala | 24 +++++-----
src/main/scala/leon/repair/rules/Split.scala | 16 +++----
.../scala/leon/synthesis/ChooseInfo.scala | 18 +++++--
.../{TestBank.scala => ExampleBank.scala} | 48 ++++++++++---------
.../scala/leon/synthesis/ExamplesFinder.scala | 10 ++--
.../scala/leon/synthesis/InOutExample.scala | 20 ++++++--
src/main/scala/leon/synthesis/Problem.scala | 21 ++++----
.../scala/leon/synthesis/SynthesisPhase.scala | 2 +-
.../scala/leon/synthesis/rules/ADTDual.scala | 2 +-
.../scala/leon/synthesis/rules/Assert.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 40 ++++++++--------
.../leon/synthesis/rules/CaseSplit.scala | 2 +-
.../leon/synthesis/rules/Disunification.scala | 2 +-
.../leon/synthesis/rules/EqualitySplit.scala | 4 +-
.../scala/leon/synthesis/rules/IfSplit.scala | 4 +-
.../synthesis/rules/InequalitySplit.scala | 6 +--
.../scala/leon/synthesis/rules/OnePoint.scala | 2 +-
.../synthesis/rules/UnconstrainedOutput.scala | 4 +-
.../leon/synthesis/rules/UnusedInput.scala | 2 +-
.../SynthesisProblemExtractionPhase.scala | 2 +-
.../test/performance/CegisPerformance.scala | 2 +-
.../test/synthesis/StablePrintingSuite.scala | 2 +-
.../synthesis/SynthesisRegressionSuite.scala | 2 +-
24 files changed, 146 insertions(+), 121 deletions(-)
rename src/main/scala/leon/synthesis/{TestBank.scala => ExampleBank.scala} (73%)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 4f33a52bc..df6f42905 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -45,30 +45,30 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val timer = new Timer().start
- val tb = discoverTests()
+ val eb = discoverTests()
- if (tb.invalids.nonEmpty) {
- reporter.info(f" - Passing: ${tb.valids.size}%3d")
- reporter.info(f" - Failing: ${tb.invalids.size}%3d")
+ if (eb.invalids.nonEmpty) {
+ reporter.info(f" - Passing: ${eb.valids.size}%3d")
+ reporter.info(f" - Failing: ${eb.invalids.size}%3d")
reporter.ifDebug { printer =>
- printer(tb.asString("Discovered Tests"))
+ printer(eb.asString("Discovered Tests"))
}
reporter.info(ASCIIHelpers.title("2. Minimizing tests"))
- val tb2 = tb.minimizeInvalids(fd, ctx, program)
+ val eb2 = eb.minimizeInvalids(fd, ctx, program)
// We exclude redundant failing tests, and only select the minimal tests
- reporter.info(f" - Minimal Failing Set Size: ${tb2.invalids.size}%3d")
+ reporter.info(f" - Minimal Failing Set Size: ${eb2.invalids.size}%3d")
reporter.ifDebug { printer =>
- printer(tb2.asString("Minimal Failing Tests"))
+ printer(eb2.asString("Minimal Failing Tests"))
}
val timeTests = timer.stop
timer.start
- val synth = getSynthesizer(tb2)
+ val synth = getSynthesizer(eb2)
try {
reporter.info(ASCIIHelpers.title("3. Synthesizing repair"))
@@ -123,7 +123,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
}
}
- def getSynthesizer(tb: TestBank): Synthesizer = {
+ def getSynthesizer(eb: ExampleBank): Synthesizer = {
val origBody = fd.body.get
@@ -142,7 +142,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
andJoin(Seq(pre, guide, term)),
origBody,
choose,
- tb
+ eb
)
// Return synthesizer for this choose
@@ -187,7 +187,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
}
}
- def discoverTests(): TestBank = {
+ def discoverTests(): ExampleBank = {
import bonsai.enumerators._
import utils.ExpressionGrammars.ValueGrammar
@@ -234,15 +234,15 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
case _ => false
}
- val genTb = TestBank(genPassing, genFailing).stripOuts
+ val genTb = ExampleBank(genPassing, genFailing).stripOuts
// Extract passing/failing from the passes in POST
- val userTb = new ExamplesFinder(ctx, program).extractTests(fd)
+ val userTb = new ExamplesFinder(ctx, program).extractExampleBank(fd)
val allTb = genTb union userTb
if (allTb.invalids.isEmpty) {
- TestBank(allTb.valids, getVerificationCExs(fd))
+ ExampleBank(allTb.valids, getVerificationCExs(fd))
} else {
allTb
}
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 50516c6db..e4a5e3404 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -51,7 +51,7 @@ case object Focus extends PreprocessingRule("Focus") {
def forAllTests(e: Expr, env: Map[Identifier, Expr], evaluator: Evaluator): Option[Boolean] = {
var soFar: Option[Boolean] = None
- p.tb.invalids.foreach { ex =>
+ p.eb.invalids.foreach { ex =>
evaluator.eval(e, (p.as zip ex.ins).toMap ++ env) match {
case EvaluationResults.Successful(BooleanLiteral(b)) =>
soFar match {
@@ -107,7 +107,7 @@ case object Focus extends PreprocessingRule("Focus") {
case Some(true) =>
val cx = FreshIdentifier("cond", BooleanType)
// Focus on condition
- val np = Problem(p.as, ws(c), p.pc, letTuple(p.xs, IfExpr(cx.toVariable, thn, els), p.phi), List(cx), p.tb.stripOuts)
+ val np = Problem(p.as, ws(c), p.pc, letTuple(p.xs, IfExpr(cx.toVariable, thn, els), p.phi), List(cx), p.eb.stripOuts)
Some(decomp(List(np), termWrap(IfExpr(_, thn, els)), s"Focus on if-cond '$c'")(p))
@@ -115,11 +115,11 @@ case object Focus extends PreprocessingRule("Focus") {
// Try to focus on branches
forAllTests(c, Map(), evaluator) match {
case Some(true) =>
- val np = Problem(p.as, ws(thn), and(p.pc, c), p.phi, p.xs, p.tbOps.filterIns(c))
+ val np = Problem(p.as, ws(thn), and(p.pc, c), p.phi, p.xs, p.qeb.filterIns(c))
Some(decomp(List(np), termWrap(IfExpr(c, _, els), c), s"Focus on if-then")(p))
case Some(false) =>
- val np = Problem(p.as, ws(els), and(p.pc, not(c)), p.phi, p.xs, p.tbOps.filterIns(not(c)))
+ val np = Problem(p.as, ws(els), and(p.pc, not(c)), p.phi, p.xs, p.qeb.filterIns(not(c)))
Some(decomp(List(np), termWrap(IfExpr(c, thn, _), not(c)), s"Focus on if-else")(p))
case None =>
@@ -147,10 +147,10 @@ case object Focus extends PreprocessingRule("Focus") {
val vars = map.toSeq.map(_._1)
// Filter tests by the path-condition
- val tb2 = p.tbOps.filterIns(cond)
+ val eb2 = p.qeb.filterIns(cond)
// Augment test with the additional variables and their valuations
- val tbF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
+ val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
val emap = (p.as zip e).toMap
evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
@@ -158,15 +158,15 @@ case object Focus extends PreprocessingRule("Focus") {
}.toList
}
- val tb3 = if (vars.nonEmpty) {
- tb2.mapIns(tbF)
+ val eb3 = if (vars.nonEmpty) {
+ eb2.mapIns(ebF)
} else {
- tb2
+ eb2
}
val newPc = andJoin(cond +: vars.map { id => equality(id.toVariable, map(id)) })
- val np = Problem(p.as ++ vars, ws(c.rhs), and(p.pc, newPc), p.phi, p.xs, tb3)
+ val np = Problem(p.as ++ vars, ws(c.rhs), and(p.pc, newPc), p.phi, p.xs, eb3)
res = Some(
Some(
@@ -188,7 +188,7 @@ case object Focus extends PreprocessingRule("Focus") {
case Let(id, value, body) =>
- val tbF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
+ val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
val map = (p.as zip e).toMap
evaluator.eval(value, map).result.map { r =>
@@ -196,7 +196,7 @@ case object Focus extends PreprocessingRule("Focus") {
}.toList
}
- val np = Problem(p.as :+ id, ws(body), and(p.pc, equality(id.toVariable, value)), p.phi, p.xs, p.tb.mapIns(tbF))
+ val np = Problem(p.as :+ id, ws(body), and(p.pc, equality(id.toVariable, value)), p.phi, p.xs, p.eb.mapIns(ebF))
Some(decomp(List(np), termWrap(Let(id, value, _)), s"Focus on let-body")(p))
diff --git a/src/main/scala/leon/repair/rules/Split.scala b/src/main/scala/leon/repair/rules/Split.scala
index b05f3570e..94b7ff24b 100644
--- a/src/main/scala/leon/repair/rules/Split.scala
+++ b/src/main/scala/leon/repair/rules/Split.scala
@@ -50,8 +50,8 @@ case object Split extends Rule("Split") {
val alts = guides.collect {
case g @ IfExpr(c, thn, els) =>
- val sub1 = p.copy(ws = replace(Map(g -> thn), p.ws), pc = and(c, replace(Map(g -> thn), p.pc)), tb = p.tbOps.filterIns(c))
- val sub2 = p.copy(ws = replace(Map(g -> els), p.ws), pc = and(Not(c), replace(Map(g -> els), p.pc)), tb = p.tbOps.filterIns(Not(c)))
+ val sub1 = p.copy(ws = replace(Map(g -> thn), p.ws), pc = and(c, replace(Map(g -> thn), p.pc)), eb = p.qeb.filterIns(c))
+ val sub2 = p.copy(ws = replace(Map(g -> els), p.ws), pc = and(Not(c), replace(Map(g -> els), p.pc)), eb = p.qeb.filterIns(Not(c)))
val onSuccess: List[Solution] => Option[Solution] = {
case List(s1, s2) =>
@@ -76,10 +76,10 @@ case object Split extends Rule("Split") {
val vars = map.toSeq.map(_._1)
// Filter tests by the path-condition
- val tb2 = p.tbOps.filterIns(cond)
+ val eb2 = p.qeb.filterIns(cond)
// Augment test with the additional variables and their valuations
- val tbF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
+ val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
val emap = (p.as zip e).toMap
evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
@@ -87,15 +87,15 @@ case object Split extends Rule("Split") {
}.toList
}
- val tb3 = if (vars.nonEmpty) {
- tb2.mapIns(tbF)
+ val eb3 = if (vars.nonEmpty) {
+ eb2.mapIns(ebF)
} else {
- tb2
+ eb2
}
val newPc = andJoin(cond +: vars.map { id => equality(id.toVariable, map(id)) })
- (cond, Problem(p.as ++ vars, ws(c.rhs), and(p.pc, newPc), p.phi, p.xs, tb3))
+ (cond, Problem(p.as ++ vars, ws(c.rhs), and(p.pc, newPc), p.phi, p.xs, eb3))
}
val onSuccess = { (sols: List[Solution]) =>
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 68f8745af..6975bb682 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -13,30 +13,38 @@ case class ChooseInfo(fd: FunDef,
pc: Expr,
source: Expr,
ch: Choose,
- tests: TestBank) {
+ eb: ExampleBank) {
val problem = Problem.fromChooseInfo(this)
}
object ChooseInfo {
- def extractFromProgram(prog: Program): List[ChooseInfo] = {
+ def extractFromProgram(ctx: LeonContext, prog: Program): List[ChooseInfo] = {
// Look for choose()
val results = for (f <- prog.definedFunctions if f.body.isDefined;
- ci <- extractFromFunction(prog, f)) yield {
+ ci <- extractFromFunction(ctx, prog, f)) yield {
ci
}
results.sortBy(_.source.getPos)
}
- def extractFromFunction(prog: Program, fd: FunDef): Seq[ChooseInfo] = {
+ def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef): Seq[ChooseInfo] = {
val actualBody = and(fd.precondition.getOrElse(BooleanLiteral(true)), fd.body.get)
val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
+ val userEb = new ExamplesFinder(ctx, prog).extractExampleBank(fd)
+
for ((ch, path) <- new ChooseCollectorWithPaths().traverse(actualBody)) yield {
- ChooseInfo(fd, and(path, term), ch, ch, TestBank.empty)
+ val eb = if (path == BooleanLiteral(true)) {
+ userEb
+ } else {
+ ExampleBank.empty
+ }
+
+ ChooseInfo(fd, and(path, term), ch, ch, eb)
}
}
}
diff --git a/src/main/scala/leon/synthesis/TestBank.scala b/src/main/scala/leon/synthesis/ExampleBank.scala
similarity index 73%
rename from src/main/scala/leon/synthesis/TestBank.scala
rename to src/main/scala/leon/synthesis/ExampleBank.scala
index b5ee5790c..29c82015b 100644
--- a/src/main/scala/leon/synthesis/TestBank.scala
+++ b/src/main/scala/leon/synthesis/ExampleBank.scala
@@ -9,12 +9,13 @@ import purescala.Common._
import repair._
import leon.utils.ASCIIHelpers._
-case class TestBank(valids: Seq[Example], invalids: Seq[Example]) {
- def examples: Seq[Example] = valids ++ invalids
+
+case class ExampleBank(valids: Seq[Example], invalids: Seq[Example]) {
+ def examples = valids ++ invalids
// Minimize tests of a function so that tests that are invalid because of a
// recursive call are eliminated
- def minimizeInvalids(fd: FunDef, ctx: LeonContext, program: Program): TestBank = {
+ def minimizeInvalids(fd: FunDef, ctx: LeonContext, program: Program): ExampleBank = {
val evaluator = new RepairTrackingEvaluator(ctx, program)
invalids foreach { ts =>
@@ -34,7 +35,7 @@ case class TestBank(valids: Seq[Example], invalids: Seq[Example]) {
}
val newInvalids = failing.keySet map {
- case (_, args) =>
+ case (_, args) =>
outInfo.get(args) match {
case Some(outs) =>
InOutExample(args, outs)
@@ -44,18 +45,18 @@ case class TestBank(valids: Seq[Example], invalids: Seq[Example]) {
}
}
- TestBank(valids, newInvalids.toSeq)
+ ExampleBank(valids, newInvalids.toSeq)
}
- def union(that: TestBank) = {
- TestBank(
- (this.valids ++ that.valids).distinct,
- (this.invalids ++ that.invalids).distinct
+ def union(that: ExampleBank) = {
+ ExampleBank(
+ (this.valids union that.valids).distinct,
+ (this.invalids union that.invalids).distinct
)
}
def map(f: Example => List[Example]) = {
- TestBank(valids.flatMap(f), invalids.flatMap(f))
+ ExampleBank(valids.flatMap(f), invalids.flatMap(f))
}
def mapIns(f: Seq[Expr] => List[Seq[Expr]]) = {
@@ -124,9 +125,11 @@ case class TestBank(valids: Seq[Example], invalids: Seq[Example]) {
)
}
}
+
if (valids.nonEmpty) {
testsRows("Valid tests", valids)
}
+
if (invalids.nonEmpty) {
testsRows("Invalid tests", invalids)
}
@@ -138,32 +141,34 @@ case class TestBank(valids: Seq[Example], invalids: Seq[Example]) {
}
}
-object TestBank {
- def empty = TestBank(Nil, Nil)
+object ExampleBank {
+ def empty = ExampleBank(Nil, Nil)
}
-case class ProblemTestBank(p: Problem, tb: TestBank)(implicit hctx: SearchContext) {
+// Same as an ExampleBank, but with identifiers corresponding to values. This
+// allows us to evaluate expressions
+case class QualifiedExampleBank(as: List[Identifier], xs: List[Identifier], eb: ExampleBank)(implicit hctx: SearchContext) {
def removeOuts(toRemove: Set[Identifier]) = {
- val toKeep = p.xs.zipWithIndex.filterNot(x => toRemove(x._1)).map(_._2)
+ val toKeep = xs.zipWithIndex.filterNot(x => toRemove(x._1)).map(_._2)
- tb mapOuts { out => List(toKeep.map(out)) }
+ eb mapOuts { out => List(toKeep.map(out)) }
}
def removeIns(toRemove: Set[Identifier]) = {
- val toKeep = p.as.zipWithIndex.filterNot(a => toRemove(a._1)).map(_._2)
- tb mapIns { in => List(toKeep.map(in)) }
+ val toKeep = as.zipWithIndex.filterNot(a => toRemove(a._1)).map(_._2)
+ eb mapIns { in => List(toKeep.map(in)) }
}
- def filterIns(expr: Expr): TestBank = {
+ def filterIns(expr: Expr): ExampleBank = {
val ev = new DefaultEvaluator(hctx.sctx.context, hctx.sctx.program)
filterIns(m => ev.eval(expr, m).result == Some(BooleanLiteral(true)))
}
- def filterIns(pred: Map[Identifier, Expr] => Boolean): TestBank = {
- tb mapIns { in =>
- val m = (p.as zip in).toMap
+ def filterIns(pred: Map[Identifier, Expr] => Boolean): ExampleBank = {
+ eb mapIns { in =>
+ val m = (as zip in).toMap
if(pred(m)) {
List(in)
} else {
@@ -171,5 +176,4 @@ case class ProblemTestBank(p: Problem, tb: TestBank)(implicit hctx: SearchContex
}
}
}
-
}
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 4dc281f17..2fbf1d87d 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -20,7 +20,7 @@ class ExamplesFinder(ctx: LeonContext, program: Program) {
val reporter = ctx.reporter
- def extractTests(fd: FunDef): TestBank = fd.postcondition match {
+ def extractExampleBank(fd: FunDef): ExampleBank = fd.postcondition match {
case Some(Lambda(Seq(ValDef(id, _)), post)) =>
// @mk FIXME: make this more general
val tests = extractTestsOf(post)
@@ -53,13 +53,9 @@ class ExamplesFinder(ctx: LeonContext, program: Program) {
}
val (v, iv) = examples.partition(isValidTest)
- TestBank(v, iv)
+ ExampleBank(v, iv)
case None =>
- TestBank(Nil, Nil)
- }
-
- def generateTests(p: Problem): Seq[Example] = {
- Nil
+ ExampleBank(Nil, Nil)
}
// Extract examples from the passes found in expression
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index 67adb0787..ae6e24bbc 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -6,6 +6,20 @@ package synthesis
import purescala.Expressions._
import leon.utils.ASCIIHelpers._
-class Example(val ins: Seq[Expr])
-case class InOutExample(is: Seq[Expr], outs: Seq[Expr]) extends Example(is)
-case class InExample(is: Seq[Expr]) extends Example(is)
+sealed abstract class Example {
+ def ins: Seq[Expr]
+
+ def asString(implicit ctx: LeonContext) = {
+ def esToStr(es: Seq[Expr]): String = {
+ es.map(_.asString).mkString("(", ", ", ")")
+ }
+
+ this match {
+ case InExample(ins) => esToStr(ins)
+ case InOutExample(ins, outs) => esToStr(ins)+" ~> "+esToStr(outs)
+ }
+ }
+}
+
+case class InOutExample(ins: Seq[Expr], outs: Seq[Expr]) extends Example
+case class InExample(ins: Seq[Expr]) extends Example
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 164b1a102..99b1d699d 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -13,7 +13,7 @@ import Witnesses._
// Defines a synthesis triple of the form:
// ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧
-case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier], tb: TestBank = TestBank.empty) {
+case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier], eb: ExampleBank = ExampleBank.empty) {
def inType = tupleTypeWrap(as.map(_.getType))
def outType = tupleTypeWrap(xs.map(_.getType))
@@ -21,24 +21,25 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List
def asString(implicit ctx: LeonContext): String = {
val pcws = and(ws, pc)
- val tbInfo = "/"+tb.valids.size+","+tb.invalids.size+"/"
+ val ebInfo = "/"+eb.valids.size+","+eb.invalids.size+"/"
- "⟦ "+as.map(_.asString).mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws.asString+" ≺ " else "")+" ⟨ "+phi.asString+" ⟩ "+xs.map(_.asString).mkString(";")+" ⟧ "+tbInfo
+ "⟦ "+as.map(_.asString).mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws.asString+" ≺ " else "")+" ⟨ "+phi.asString+" ⟩ "+xs.map(_.asString).mkString(";")+" ⟧ "+ebInfo
}
override def toString = {
val pcws = and(ws, pc)
- val tbInfo = "/"+tb.valids.size+","+tb.invalids.size+"/"
+ val ebInfo = "/"+eb.valids.size+","+eb.invalids.size+"/"
- "⟦ "+as.mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "+tbInfo
+ "⟦ "+as.mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "+ebInfo
}
- def tbOps(implicit sctx: SearchContext) = ProblemTestBank(this, tb)
+ // Qualified example bank, allows us to perform operations (e.g. filter) with expressions
+ def qeb(implicit sctx: SearchContext) = QualifiedExampleBank(this.as, this.xs, eb)
}
object Problem {
- def fromChoose(ch: Choose, pc: Expr = BooleanLiteral(true), tb: TestBank = TestBank.empty): Problem = {
+ def fromChoose(ch: Choose, pc: Expr = BooleanLiteral(true), eb: ExampleBank = ExampleBank.empty): Problem = {
val xs = {
val tps = ch.pred.getType.asInstanceOf[FunctionType].from
tps map (FreshIdentifier("x", _, true))
@@ -54,15 +55,15 @@ object Problem {
case _ => true
}
- Problem(as, andJoin(wss), andJoin(pcs), phi, xs, tb)
+ Problem(as, andJoin(wss), andJoin(pcs), phi, xs, eb)
}
def fromChooseInfo(ci: ChooseInfo): Problem = {
// Same as fromChoose, but we order the input variables by the arguments of
// the functions, so that tests are compatible
- val p = fromChoose(ci.ch, ci.pc, ci.tests)
+ val p = fromChoose(ci.ch, ci.pc, ci.eb)
val argsIndex = ci.fd.params.map(_.id).zipWithIndex.toMap.withDefaultValue(100)
-
+
p.copy( as = p.as.sortBy(a => argsIndex(a)))
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 31327bf8a..1439ca25a 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -74,7 +74,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
filterInclusive(options.functions.map(fdMatcher), Some(excludeByDefault _)) compose ciTofd
}
- val chooses = ChooseInfo.extractFromProgram(p).filter(fdFilter)
+ val chooses = ChooseInfo.extractFromProgram(ctx, p).filter(fdFilter)
var functions = Set[FunDef]()
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 6b33597ca..4e4c8b07e 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -26,7 +26,7 @@ case object ADTDual extends NormalizingRule("ADTDual") {
}.unzip
if (toRemove.nonEmpty) {
- val sub = p.copy(phi = andJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq), tb = TestBank.empty)
+ val sub = p.copy(phi = andJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq), eb = ExampleBank.empty)
Some(decomp(List(sub), forward, "ADTDual"))
} else {
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index bd070e6d0..270392aa1 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -19,7 +19,7 @@ case object Assert extends NormalizingRule("Assert") {
if (others.isEmpty) {
Some(solve(Solution(andJoin(exprsA), Set(), tupleWrap(p.xs.map(id => simplestValue(id.getType))))))
} else {
- val sub = p.copy(pc = andJoin(p.pc +: exprsA), phi = andJoin(others), tb = p.tbOps.filterIns(andJoin(exprsA)))
+ val sub = p.copy(pc = andJoin(p.pc +: exprsA), phi = andJoin(others), eb = p.qeb.filterIns(andJoin(exprsA)))
Some(decomp(List(sub), {
case (s @ Solution(pre, defs, term)) :: Nil => Some(Solution(andJoin(exprsA :+ pre), defs, term, s.isTrusted))
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index c2eac3128..8178cc6c8 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -388,7 +388,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private val innerPhi = outerExprToInnerExpr(p.phi)
private var programCTree: Program = _
- private var tester: (Seq[Expr], Set[Identifier]) => EvaluationResults.Result = _
+ private var tester: (Example, Set[Identifier]) => EvaluationResults.Result = _
private def setCExpr(cTreeInfo: (Expr, Seq[FunDef])): Unit = {
val (cTree, newFds) = cTreeInfo
@@ -404,18 +404,19 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val evaluator = new DefaultEvaluator(sctx.context, programCTree)
tester =
- { (ins: Seq[Expr], bValues: Set[Identifier]) =>
+ { (ex: Example, bValues: Set[Identifier]) =>
+ // TODO: Test output value as well
val envMap = bs.map(b => b -> BooleanLiteral(bValues(b))).toMap
- val fi = FunctionInvocation(phiFd.typed, ins)
+ val fi = FunctionInvocation(phiFd.typed, ex.ins)
evaluator.eval(fi, envMap)
}
}
- def testForProgram(bValues: Set[Identifier])(ins: Seq[Expr]): Boolean = {
- tester(ins, bValues) match {
+ def testForProgram(bValues: Set[Identifier])(ex: Example): Boolean = {
+ tester(ex, bValues) match {
case EvaluationResults.Successful(res) =>
res == BooleanLiteral(true)
@@ -649,7 +650,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
sctx.reporter.debug(s"maxUnfoldings=$maxUnfoldings")
- var baseExampleInputs: ArrayBuffer[Seq[Expr]] = new ArrayBuffer[Seq[Expr]]()
+ var baseExampleInputs: ArrayBuffer[Example] = new ArrayBuffer[Example]()
sctx.reporter.ifDebug { printer =>
ndProgram.grammar.printProductions(printer)
@@ -658,10 +659,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// We populate the list of examples with a predefined one
sctx.reporter.debug("Acquiring initial list of examples")
- baseExampleInputs ++= p.tb.examples.map(_.ins).toSet
+ baseExampleInputs ++= p.eb.examples
if (p.pc == BooleanLiteral(true)) {
- baseExampleInputs += p.as.map(a => simplestValue(a.getType))
+ baseExampleInputs += InExample(p.as.map(a => simplestValue(a.getType)))
} else {
val solver = sctx.newSolver.setTimeout(exSolverTo)
@@ -671,7 +672,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
solver.check match {
case Some(true) =>
val model = solver.getModel
- baseExampleInputs += p.as.map(a => model.getOrElse(a, simplestValue(a.getType)))
+ baseExampleInputs += InExample(p.as.map(a => model.getOrElse(a, simplestValue(a.getType))))
case Some(false) =>
sctx.reporter.debug("Path-condition seems UNSAT")
@@ -688,7 +689,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
sctx.reporter.ifDebug { debug =>
baseExampleInputs.foreach { in =>
- debug(" - "+in.map(_.asString).mkString(", "))
+ debug(" - "+in.asString)
}
}
@@ -703,9 +704,9 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
new GrammarDataGen(evaluator, ExpressionGrammars.ValueGrammar).generateFor(p.as, p.pc, 20, 1000)
}
- val cachedInputIterator = new Iterator[Seq[Expr]] {
+ val cachedInputIterator = new Iterator[Example] {
def next() = {
- val i = inputIterator.next()
+ val i = InExample(inputIterator.next())
baseExampleInputs += i
i
}
@@ -715,7 +716,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
}
- val failedTestsStats = new MutableMap[Seq[Expr], Int]().withDefaultValue(0)
+ val failedTestsStats = new MutableMap[Example, Int]().withDefaultValue(0)
def hasInputExamples = baseExampleInputs.size > 0 || cachedInputIterator.hasNext
@@ -767,7 +768,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
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.map(_.asString).mkString(", ")}")
+ sctx.reporter.debug(f" Program: ${ndProgram.getExpr(bs).asString}%-80s failed on: ${e.asString}")
wrongPrograms += bs
prunedPrograms -= bs
@@ -793,8 +794,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
sctx.reporter.debug("#Tests: "+baseExampleInputs.size)
sctx.reporter.ifDebug{ printer =>
- for (i <- baseExampleInputs.take(10)) {
- printer(" - "+i.mkString(", "))
+ for (e <- baseExampleInputs.take(10)) {
+ printer(" - "+e.asString)
}
if(baseExampleInputs.size > 10) {
printer(" - ...")
@@ -815,7 +816,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
doFilter = false
result = Some(RuleClosed(sols))
case Right(cexs) =>
- baseExampleInputs ++= cexs
+ baseExampleInputs ++= cexs.map(InExample(_))
if (nPassing <= validateUpTo) {
// All programs failed verification, we filter everything out and unfold
@@ -865,11 +866,12 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
if (validateWithZ3) {
ndProgram.solveForCounterExample(bs) match {
case Some(Some(inputsCE)) =>
+ val ce = InExample(inputsCE)
// Found counter example!
- baseExampleInputs += inputsCE
+ baseExampleInputs += ce
// Retest whether the newly found C-E invalidates all programs
- if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(inputsCE))) {
+ if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(ce))) {
skipCESearch = true
} else {
ndProgram.excludeProgram(bs)
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 9140eaf23..29f27a931 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -18,7 +18,7 @@ case object CaseSplit extends Rule("Case-Split") {
}
def split(alts: Seq[Expr], description: String)(implicit p: Problem): RuleInstantiation = {
- val subs = alts.map(a => Problem(p.as, p.ws, p.pc, a, p.xs, p.tb)).toList
+ val subs = alts.map(a => Problem(p.as, p.ws, p.pc, a, p.xs, p.eb)).toList
val onSuccess: List[Solution] => Option[Solution] = {
case sols if sols.size == subs.size =>
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 402f59bf7..4c8a2c4f7 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -25,7 +25,7 @@ object Disunification {
}.unzip
if (toRemove.nonEmpty) {
- val sub = p.copy(phi = orJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq), tb = TestBank.empty)
+ val sub = p.copy(phi = orJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq), eb = ExampleBank.empty)
Some(decomp(List(sub), forward, this.name))
} else {
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 44043b0e0..b1653596a 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -43,11 +43,11 @@ case object EqualitySplit extends Rule("Eq. Split") {
val sub1 = p.copy(
pc = and(Equals(Variable(a1), Variable(a2)), p.pc),
- tb = p.tbOps.filterIns( (m: Map[Identifier, Expr]) => m(a1) == m(a2))
+ eb = p.qeb.filterIns( (m: Map[Identifier, Expr]) => m(a1) == m(a2))
)
val sub2 = p.copy(
pc = and(not(Equals(Variable(a1), Variable(a2))), p.pc),
- tb = p.tbOps.filterIns( (m: Map[Identifier, Expr]) => m(a1) != m(a2))
+ eb = p.qeb.filterIns( (m: Map[Identifier, Expr]) => m(a1) != m(a2))
)
val onSuccess: List[Solution] => Option[Solution] = {
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index 2016570b5..0ff4cf4fd 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -13,8 +13,8 @@ case object IfSplit extends Rule("If-Split") {
def split(i: IfExpr, description: String): RuleInstantiation = {
val subs = List(
- Problem(p.as, p.ws, and(p.pc, i.cond), replace(Map(i -> i.thenn), p.phi), p.xs, p.tbOps.filterIns(i.cond)),
- Problem(p.as, p.ws, and(p.pc, not(i.cond)), replace(Map(i -> i.elze), p.phi), p.xs, p.tbOps.filterIns(not(i.cond)))
+ Problem(p.as, p.ws, and(p.pc, i.cond), replace(Map(i -> i.thenn), p.phi), p.xs, p.qeb.filterIns(i.cond)),
+ Problem(p.as, p.ws, and(p.pc, not(i.cond)), replace(Map(i -> i.elze), p.phi), p.xs, p.qeb.filterIns(not(i.cond)))
)
val onSuccess: List[Solution] => Option[Solution] = {
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 741b4d02e..8cc0f2f31 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -57,11 +57,11 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
case List(a1, a2) =>
val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc),
- tb = p.tbOps.filterIns(LessThan(Variable(a1), Variable(a2))))
+ eb = p.qeb.filterIns(LessThan(Variable(a1), Variable(a2))))
val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc),
- tb = p.tbOps.filterIns(Equals(Variable(a1), Variable(a2))))
+ eb = p.qeb.filterIns(Equals(Variable(a1), Variable(a2))))
val subGT = p.copy(pc = and(GreaterThan(Variable(a1), Variable(a2)), p.pc),
- tb = p.tbOps.filterIns(GreaterThan(Variable(a1), Variable(a2))))
+ eb = p.qeb.filterIns(GreaterThan(Variable(a1), Variable(a2))))
val onSuccess: List[Solution] => Option[Solution] = {
case sols@List(sLT, sEQ, sGT) =>
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 230102b74..451dc8c3c 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -31,7 +31,7 @@ case object OnePoint extends NormalizingRule("One-point") {
val others = exprs.filter(_ != eq)
val oxs = p.xs.filter(_ != x)
- val newProblem = Problem(p.as, p.ws, p.pc, subst(x -> e, andJoin(others)), oxs, p.tbOps.removeOuts(Set(x)))
+ val newProblem = Problem(p.as, p.ws, p.pc, subst(x -> e, andJoin(others)), oxs, p.qeb.removeOuts(Set(x)))
val onSuccess: List[Solution] => Option[Solution] = {
case List(s @ Solution(pre, defs, term)) =>
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index f261f3637..f753d3884 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -13,9 +13,9 @@ case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
val unconstr = p.xs.toSet -- variablesOf(p.phi)
if (unconstr.nonEmpty) {
- val sub = p.copy(xs = p.xs.filterNot(unconstr), tb = p.tbOps.removeOuts(unconstr))
+ val sub = p.copy(xs = p.xs.filterNot(unconstr), eb = p.qeb.removeOuts(unconstr))
- val onSuccess: List[Solution] => Option[Solution] = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(s) =>
val term = letTuple(sub.xs, s.term, tupleWrap(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 534dbea78..677c9b852 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -11,7 +11,7 @@ case object UnusedInput extends NormalizingRule("UnusedInput") {
val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc) -- variablesOf(p.ws)
if (unused.nonEmpty) {
- val sub = p.copy(as = p.as.filterNot(unused), tb = p.tbOps.removeIns(unused))
+ val sub = p.copy(as = p.as.filterNot(unused), eb = p.qeb.removeIns(unused))
List(decomp(List(sub), forward, s"Unused inputs ${p.as.filter(unused).mkString(", ")}"))
} else {
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index 7b0324d14..ae4632031 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -14,7 +14,7 @@ object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[
def run(ctx: LeonContext)(p: Program): (Program, Map[FunDef, Seq[ChooseInfo]]) = {
// Look for choose()
val results = for (f <- funDefsFromMain(p).toSeq.sortBy(_.id.toString) if f.body.isDefined) yield {
- f -> ChooseInfo.extractFromFunction(p, f)
+ f -> ChooseInfo.extractFromFunction(ctx, p, f)
}
(p, results.toMap)
diff --git a/src/test/scala/leon/test/performance/CegisPerformance.scala b/src/test/scala/leon/test/performance/CegisPerformance.scala
index 1ca107ff6..fb758a5dd 100644
--- a/src/test/scala/leon/test/performance/CegisPerformance.scala
+++ b/src/test/scala/leon/test/performance/CegisPerformance.scala
@@ -45,7 +45,7 @@ class CegisPerfTest extends PerformanceTest.OfflineRegressionReport {
for ((name, ctx, pgm) <- ctxPrograms) {
measure.method(name) in {
using(Gen.unit("test")) in { _ =>
- val cis = ChooseInfo.extractFromProgram(pgm).filterNot(_.fd.annotations("library"))
+ val cis = ChooseInfo.extractFromProgram(ctx, pgm).filterNot(_.fd.annotations("library"))
for (ci <- cis) {
val synth = new Synthesizer(ctx, pgm, ci, settings)
val s = synth.getSearch
diff --git a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
index f497bb79c..360b4a5d0 100644
--- a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -37,7 +37,7 @@ class StablePrintingSuite extends LeonTestSuite {
val program = pipeline.run(ctx)((content, Nil))
- (program, opts, ChooseInfo.extractFromProgram(program))
+ (program, opts, ChooseInfo.extractFromProgram(ctx, program))
}
case class Job(content: String, choosesToProcess: Set[Int], rules: List[String]) {
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 1095e9c8e..35513481a 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -34,7 +34,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
program = pipeline.run(ctx)(f.getAbsolutePath :: Nil)
- chooses = ChooseInfo.extractFromProgram(program)
+ chooses = ChooseInfo.extractFromProgram(ctx, program)
}
for (ci <- chooses) {
--
GitLab