From 76c761d22fb6626133ddec5c3e86a71ba0eda9af Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Wed, 17 Dec 2014 17:13:24 +0100
Subject: [PATCH] Introduce Witness, and Guide and Terminating as implementing
classes
---
library/annotation/package.scala | 2 --
library/lang/synthesis/package.scala | 7 ------
.../scala/leon/purescala/PrettyPrinter.scala | 8 ++++++
src/main/scala/leon/purescala/TreeOps.scala | 25 +++++++++++++++++--
.../scala/leon/repair/RepairCostModel.scala | 1 +
src/main/scala/leon/repair/Repairman.scala | 10 +++-----
.../leon/repair/rules/GuidedCloser.scala | 6 ++---
.../leon/repair/rules/GuidedDecomp.scala | 6 ++---
.../scala/leon/synthesis/ChooseInfo.scala | 5 ++--
src/main/scala/leon/synthesis/Problem.scala | 4 ++-
src/main/scala/leon/synthesis/Witnesses.scala | 24 ++++++++++++++++++
.../scala/leon/synthesis/rules/Cegless.scala | 5 ++--
.../scala/leon/synthesis/rules/Tegless.scala | 5 ++--
.../scala/leon/synthesis/utils/Helpers.scala | 8 +++---
src/main/scala/leon/utils/Library.scala | 8 ------
15 files changed, 78 insertions(+), 46 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/Witnesses.scala
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index 2db992498..f6e084cda 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -11,8 +11,6 @@ package object annotation {
class verified extends StaticAnnotation
@ignore
class repair extends StaticAnnotation
- @ignore
- class witness extends StaticAnnotation
@ignore
class induct extends StaticAnnotation
diff --git a/library/lang/synthesis/package.scala b/library/lang/synthesis/package.scala
index 1f5f749b6..e4f50b403 100644
--- a/library/lang/synthesis/package.scala
+++ b/library/lang/synthesis/package.scala
@@ -38,11 +38,4 @@ package object synthesis {
@ignore
def withOracle[A, R](body: Oracle[A] => R): R = noImpl
- @library
- @witness
- def terminating[T](t: T): Boolean = true
-
- @library
- @witness
- def guide[T](e: T): Boolean = true
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 899605eb1..cda5084b9 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -16,6 +16,8 @@ import PrinterHelpers._
import TreeOps.{isStringLiteral, isListLiteral}
import TypeTreeOps.leastUpperBound
+import synthesis.Witnesses._
+
case class PrinterContext(
current: Tree,
parent: Option[Tree],
@@ -389,6 +391,12 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
|} else $ie"""
}
+ case Terminating(tfd, args) =>
+ p"↓ ${tfd.id}($args)"
+
+ case Guide(e) =>
+ p"⊙ {$e}"
+
case IfExpr(c, t, e) =>
optP {
p"""|if ($c) {
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index db98554b6..e493ecbb3 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1331,6 +1331,8 @@ object TreeOps {
newFD
}
+ import synthesis.Witnesses.Terminating
+
def pre(e : Expr) : Expr = e match {
case Tuple(Seq()) => UnitLiteral()
case Variable(id) if idMap contains id => Variable(idMap(id))
@@ -1351,6 +1353,9 @@ object TreeOps {
case FunctionInvocation(tfd, args) =>
FunctionInvocation(fd2fd(tfd.fd).typed(tfd.tps), args)
+
+ case Terminating(tfd, args) =>
+ Terminating(fd2fd(tfd.fd).typed(tfd.tps), args)
case _ => e
}
@@ -1626,6 +1631,8 @@ object TreeOps {
}
+ import synthesis.Witnesses.Terminating
+
val res = (t1, t2) match {
case (Variable(i1), Variable(i2)) =>
idHomo(i1, i2)
@@ -1659,7 +1666,12 @@ object TreeOps {
// TODO: Check type params
fdHomo(tfd1.fd, tfd2.fd) &&
(args1 zip args2).forall{ case (a1, a2) => isHomo(a1, a2) }
-
+
+ case (Terminating(tfd1, args1), Terminating(tfd2, args2)) =>
+ // TODO: Check type params
+ fdHomo(tfd1.fd, tfd2.fd) &&
+ (args1 zip args2).forall{ case (a1, a2) => isHomo(a1, a2) }
+
case Same(UnaryOperator(e1, _), UnaryOperator(e2, _)) =>
isHomo(e1, e2)
@@ -2041,6 +2053,8 @@ object TreeOps {
*/
def liftClosures(e: Expr): (Set[FunDef], Expr) = {
var fds: Map[FunDef, FunDef] = Map()
+
+ import synthesis.Witnesses.Terminating
val res1 = preMap({
case LetDef(fd, b) =>
val nfd = new FunDef(fd.id.freshen, fd.tparams, fd.returnType, fd.params, fd.defType)
@@ -2051,12 +2065,19 @@ object TreeOps {
Some(LetDef(nfd, b))
- case fi @ FunctionInvocation(tfd, args) =>
+ case FunctionInvocation(tfd, args) =>
if (fds contains tfd.fd) {
Some(FunctionInvocation(fds(tfd.fd).typed(tfd.tps), args))
} else {
None
}
+
+ case Terminating(tfd, args) =>
+ if (fds contains tfd.fd) {
+ Some(Terminating(fds(tfd.fd).typed(tfd.tps), args))
+ } else {
+ None
+ }
case _ =>
None
diff --git a/src/main/scala/leon/repair/RepairCostModel.scala b/src/main/scala/leon/repair/RepairCostModel.scala
index 8de1a98f5..8525db32f 100644
--- a/src/main/scala/leon/repair/RepairCostModel.scala
+++ b/src/main/scala/leon/repair/RepairCostModel.scala
@@ -3,6 +3,7 @@
package leon
package repair
import synthesis._
+import Witnesses._
import synthesis.rules._
import repair.rules._
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 65aa3f9b8..1c34786ad 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -20,6 +20,7 @@ import verification._
import synthesis._
import synthesis.rules._
import synthesis.heuristics._
+import synthesis.Witnesses._
import graph.DotGenerator
import leon.utils.ASCIIHelpers.title
@@ -100,7 +101,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val (newBody, replacedExpr) = focusRepair(program, fd, passingTests, failingTests)
fd.body = Some(newBody)
- val guide = guideOf(replacedExpr)
+ val guide = Guide(replacedExpr)
// Return synthesizer for this choose
val soptions0 = SynthesisPhase.processOptions(ctx);
@@ -119,18 +120,13 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
// extract chooses from nfd
val Seq(ci) = ChooseInfo.extractFromFunction(ctx, program, fd, soptions)
- val nci = ci.copy(pc = and(ci.pc, guideOf(replacedExpr)))
+ val nci = ci.copy(pc = and(ci.pc, guide))
val p = nci.problem
new Synthesizer(ctx, fd, program, p, soptions)
}
- private def guideOf(expr: Expr): Expr = {
- val gfd = program.library.guide.get.typed(Seq(expr.getType))
- FunctionInvocation(gfd, Seq(expr))
- }
-
private def focusRepair(program: Program, fd: FunDef, passingTests: List[Example], failingTests: List[Example]): (Expr, Expr) = {
reporter.ifDebug { printer =>
diff --git a/src/main/scala/leon/repair/rules/GuidedCloser.scala b/src/main/scala/leon/repair/rules/GuidedCloser.scala
index 30062477c..0b74f529a 100644
--- a/src/main/scala/leon/repair/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/repair/rules/GuidedCloser.scala
@@ -15,16 +15,16 @@ import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
+import Witnesses._
+
import solvers._
case object GuidedCloser extends NormalizingRule("Guided Closer") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(clauses) = p.ws
- val guide = sctx.program.library.guide.get
-
val guides = clauses.collect {
- case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+ case Guide(expr) => expr
}
val alts = guides.filter(isDeterministic).flatMap { e =>
diff --git a/src/main/scala/leon/repair/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
index f200f6909..b07af84b9 100644
--- a/src/main/scala/leon/repair/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
@@ -16,16 +16,16 @@ import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
+import Witnesses._
+
import solvers._
case object GuidedDecomp extends Rule("Guided Decomp") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(clauses) = p.ws
- val guide = sctx.program.library.guide.get
-
val guides = clauses.collect {
- case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+ case Guide(expr) => expr
}
val simplify = Simplifiers.bestEffort(sctx.context, sctx.program)_
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 1cf50638d..142498c59 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -9,6 +9,7 @@ import purescala.Constructors._
import purescala.Trees._
import purescala.TreeOps._
import purescala.DefOps._
+import Witnesses._
case class ChooseInfo(ctx: LeonContext,
prog: Program,
@@ -35,11 +36,9 @@ object ChooseInfo {
}
def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef, options: SynthesisSettings): Seq[ChooseInfo] = {
- val fterm = prog.library.terminating.getOrElse(ctx.reporter.fatalError("No library ?!?"))
val actualBody = and(fd.precondition.getOrElse(BooleanLiteral(true)), fd.body.get)
- val withinCall = FunctionInvocation(fd.typedWithDef, fd.params.map(_.id.toVariable))
- val term = FunctionInvocation(fterm.typed(Seq(fd.returnType)), Seq(withinCall))
+ val term = Terminating(fd.typedWithDef, fd.params.map(_.id.toVariable))
for ((ch, path) <- new ChooseCollectorWithPaths().traverse(actualBody)) yield {
ChooseInfo(ctx, prog, fd, and(path, term), ch, ch, options)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 468754c7c..24d95f577 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -10,6 +10,7 @@ import leon.purescala.TypeTrees.TypeTree
import leon.purescala.Common._
import leon.purescala.Constructors._
import leon.purescala.Extractors._
+import Witnesses._
// Defines a synthesis triple of the form:
// ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧
@@ -28,10 +29,11 @@ object Problem {
val phi = simplifyLets(ch.pred)
val as = (variablesOf(And(pc, phi))--xs).toList
+ // FIXME do we need this at all?
val TopLevelAnds(clauses) = pc
val (pcs, wss) = clauses.partition {
- case FunctionInvocation(TypedFunDef(fd, _), _) if fd.annotations("witness") => false
+ case w : Witness => false
case _ => true
}
diff --git a/src/main/scala/leon/synthesis/Witnesses.scala b/src/main/scala/leon/synthesis/Witnesses.scala
new file mode 100644
index 000000000..cfb8e00d2
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Witnesses.scala
@@ -0,0 +1,24 @@
+package leon.synthesis
+
+import leon.purescala._
+import TypeTrees._
+import Definitions.TypedFunDef
+import Extractors._
+import Trees.Expr
+
+
+object Witnesses {
+
+ class Witness extends Expr {
+ def getType = BooleanType
+ }
+
+ case class Guide(e : Expr) extends Witness with UnaryExtractable {
+ def extract: Option[(Expr, Expr => Expr)] = Some((e, Guide))
+ }
+
+ case class Terminating(tfd: TypedFunDef, args: Seq[Expr]) extends Witness with NAryExtractable {
+ def extract: Option[(Seq[Expr], Seq[Expr] => Expr)] = Some((args, Terminating(tfd, _)))
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/Cegless.scala
index 9c36964a2..914003fec 100644
--- a/src/main/scala/leon/synthesis/rules/Cegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegless.scala
@@ -12,16 +12,15 @@ import purescala.Definitions._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
+import Witnesses._
case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
val TopLevelAnds(clauses) = p.ws
- val guide = sctx.program.library.guide.get
-
val guides = clauses.collect {
- case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+ case Guide(e) => e
}
val inputs = p.as.map(_.toVariable)
diff --git a/src/main/scala/leon/synthesis/rules/Tegless.scala b/src/main/scala/leon/synthesis/rules/Tegless.scala
index cdef20a9b..e1880752a 100644
--- a/src/main/scala/leon/synthesis/rules/Tegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegless.scala
@@ -12,16 +12,15 @@ import purescala.Definitions._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
+import Witnesses._
case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
val TopLevelAnds(clauses) = p.ws
- val guide = sctx.program.library.guide.get
-
val guides = clauses.collect {
- case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+ case Guide(expr) => expr
}
val inputs = p.as.map(_.toVariable)
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index e30571d6d..790711ba7 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -12,6 +12,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.DefOps._
import purescala.Common._
+import Witnesses._
object Helpers {
/**
@@ -35,13 +36,12 @@ object Helpers {
}
def terminatingCalls(prog: Program, tpe: TypeTree, ws: Expr, pc: Expr): List[(Expr, Set[Identifier])] = {
- val terminating = prog.library.terminating.get
val TopLevelAnds(wss) = ws
val TopLevelAnds(clauses) = pc
- val gs: List[FunctionInvocation] = wss.toList.collect {
- case FunctionInvocation(TypedFunDef(`terminating`, _), Seq(fi: FunctionInvocation)) => fi
+ val gs: List[Terminating] = wss.toList.collect {
+ case t : Terminating => t
}
def subExprsOf(expr: Expr, v: Variable): Option[(Variable, Expr)] = expr match {
@@ -68,7 +68,7 @@ object Helpers {
}
val res = gs.flatMap {
- case FunctionInvocation(tfd, args) if isSubtypeOf(tfd.returnType, tpe) =>
+ case Terminating(tfd, args) if isSubtypeOf(tfd.returnType, tpe) =>
val ids = tfd.params.map(vd => FreshIdentifier("<hole>", true).setType(vd.tpe)).toList
for (((a, i), tpe) <- args.zipWithIndex zip tfd.params.map(_.tpe);
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 2a254a861..d80fd76a0 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -13,14 +13,6 @@ case class Library(pgm: Program) {
lazy val String = lookup("leon.lang.string.String")
- lazy val terminating: Option[FunDef] = lookup("leon.lang.synthesis.terminating").collect {
- case fd: FunDef => fd
- }
-
- lazy val guide = lookup("leon.lang.synthesis.guide") collect {
- case (fd: FunDef) => fd
- }
-
def lookup(name: String): Option[Definition] = {
searchByFullName(name, pgm)
}
--
GitLab