diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 36a2a18d11fcb2c5f69d5a708a8185264a4ccc85..89dca4fcbae9866abb336e27bcadd97d2ad4ee60 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -786,10 +786,7 @@ trait CodeGeneration {
ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
ch << ATHROW
- case Choose(_, Some(e)) =>
- mkExpr(e, ch)
-
- case choose @ Choose(_, None) =>
+ case choose: Choose =>
val prob = synthesis.Problem.fromChoose(choose)
val id = runtime.ChooseEntryPoint.register(prob, this)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index fa5ebb6c3c6458e14897341a7a582a5994ea2813..aac2586ed1cc0286593ad6458ff713dd5a352516 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -506,10 +506,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case p : Passes =>
e(p.asConstraint)
- case choose @ Choose(_, Some(impl)) =>
- e(impl)
-
- case choose @ Choose(_, None) =>
+ case choose: Choose =>
implicit val debugSection = utils.DebugSectionSynthesis
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c8e6886ba3079d40955f5fa62dd9fa8327e5c753..2b2b2b36976703d1c8f268af0e9558e64461e555 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1292,7 +1292,7 @@ object ExprOps {
def isDeterministic(e: Expr): Boolean = {
preTraversal{
- case Choose(_, None) => return false
+ case Choose(_) => return false
case Hole(_, _) => return false
//@EK FIXME: do we need it?
//case Error(_, _) => return false
@@ -1518,7 +1518,7 @@ object ExprOps {
case (Variable(i1), Variable(i2)) =>
idHomo(i1, i2)
- case (Choose(e1, _), Choose(e2, _)) =>
+ case (Choose(e1), Choose(e2)) =>
isHomo(e1, e2)
case (Let(id1, v1, e1), Let(id2, v2, e2)) =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 03385aec2645a0945ebd549e7f22a50bca8beb4b..580388348445316d04f32381661edd818b2ea7ed 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -51,25 +51,13 @@ object Expressions {
val getType = body.getType
}
- case class Choose(pred: Expr, private var impl_ : Option[Expr] = None) extends Expr {
+ case class Choose(pred: Expr) extends Expr {
val getType = pred.getType match {
case FunctionType(from, to) if from.nonEmpty => // @mk why nonEmpty?
tupleTypeWrap(from)
case _ =>
Untyped
}
-
- require(impl_ forall { imp => isSubtypeOf(imp.getType, this.getType)})
-
- def impl_= (newImpl: Option[Expr]) = {
- require(
- newImpl forall {imp => isSubtypeOf(imp.getType,this.getType)},
- newImpl.get +":" + newImpl.get.getType + " vs " + this + ":" + this.getType
- )
- impl_ = newImpl
- }
-
- def impl = impl_
}
/* Like vals */
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 8b5b3cf240957a1d7cf0aab08a0fa1aad27157b9..d6e5ba0d9a7bc66551d302cfbf4cc98c0706b283 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -15,6 +15,7 @@ object Extractors {
object UnaryOperator {
def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
case Not(t) => Some((t,not))
+ case Choose(expr) => Some((expr,Choose))
case UMinus(t) => Some((t,UMinus))
case BVUMinus(t) => Some((t,BVUMinus))
case BVNot(t) => Some((t,BVNot))
@@ -99,10 +100,6 @@ object Extractors {
object NAryOperator {
def unapply(expr: Expr) : Option[(Seq[Expr],(Seq[Expr])=>Expr)] = expr match {
- case Choose(pred, impl) => Some((Seq(pred) ++ impl.toSeq, {
- case Seq(pred) => Choose(pred, None)
- case Seq(pred, impl) => Choose(pred, Some(impl))
- }))
case fi @ FunctionInvocation(fd, args) => Some((args, FunctionInvocation(fd, _)))
case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, as => MethodInvocation(as.head, cd, tfd, as.tail)))
case fa @ Application(caller, args) => Some(caller +: args, as => application(as.head, as.tail))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index e273e9e62f9e6b953602b0c0e9b29854d83bbdc6..57269f7cedaa5cb84697e78dd6bc54ed110b6d63 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -184,13 +184,7 @@ class PrettyPrinter(opts: PrinterOptions,
case Tuple(exprs) => p"($exprs)"
case TupleSelect(t, i) => p"$t._$i"
case NoTree(tpe) => p"???($tpe)"
- case Choose(pred, oimpl) =>
- oimpl match {
- case Some(e) =>
- p"$e /* choose: $pred */"
- case None =>
- p"choose($pred)"
- }
+ case Choose(pred) => p"choose($pred)"
case e @ Error(tpe, err) => p"""error[$tpe]("$err")"""
case CaseClassInstanceOf(cct, e) =>
if (cct.classDef.isCaseObject) {
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 4eb039e6e3e1d8670992b5cc7c2fb53af7cfb5a7..0bf34096ce0fc61a98063a9f2e449dd0787a65ff 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -27,7 +27,7 @@ class ScalaPrinter(opts: PrinterOptions,
}))
case Not(Equals(l, r)) => p"$l != $r"
case Implies(l,r) => pp(or(not(l), r))
- case Choose(pred, None) => p"choose($pred)"
+ case Choose(pred) => p"choose($pred)"
case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})"
case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 635f8a03128d3d896b942c7c1bdab7ff2d506065..1ab068c7bfc91aa82dcf26d772287ee537010d9e 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -279,8 +279,8 @@ object TypeOps {
val newId = freshId(id, tpeSub(id.getType))
Let(newId, srec(value), rec(idsMap + (id -> newId))(body)).copiedFrom(l)
- case c @ Choose(pred, oimpl) =>
- Choose(rec(idsMap)(pred), oimpl.map(srec)).copiedFrom(c)
+ case c @ Choose(pred) =>
+ Choose(rec(idsMap)(pred)).copiedFrom(c)
case l @ Lambda(args, body) =>
val newArgs = args.map { arg =>
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 0449334d3702fd4164274b7b494642c647db994f..b8214d456ea8e6259e5df7fc4c24e3fc2d7fbed2 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -96,32 +96,21 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
}
def getSynthesizer(tb: TestBank): Synthesizer = {
- val (np, fdMap) = replaceFunDefs(program)({ fd =>
- if (fd == this.fd) {
- Some(fd.duplicate)
- } else {
- None
- }
- })
-
- val nfd = fdMap(fd)
- val origBody = nfd.body.get
+ val origBody = fd.body.get
- val spec = nfd.postcondition.getOrElse(
- Lambda(Seq(ValDef(FreshIdentifier("res", nfd.returnType))), BooleanLiteral(true))
+ val spec = fd.postcondition.getOrElse(
+ Lambda(Seq(ValDef(FreshIdentifier("res", fd.returnType))), BooleanLiteral(true))
)
val choose = Choose(spec)
- choose.impl = Some(origBody)
- nfd.body = Some(choose)
- val term = Terminating(nfd.typed, nfd.params.map(_.id.toVariable))
+ val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
val guide = Guide(origBody)
- val pre = nfd.precondition.getOrElse(BooleanLiteral(true))
+ val pre = fd.precondition.getOrElse(BooleanLiteral(true))
val ci = ChooseInfo(
- nfd,
+ fd,
andJoin(Seq(pre, guide, term)),
origBody,
choose,
@@ -143,7 +132,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
)) diff Seq(ADTInduction, TEGIS, IntegerInequalities, IntegerEquation)
)
- new Synthesizer(ctx, np, ci, soptions)
+ new Synthesizer(ctx, program, ci, soptions)
}
def getVerificationCExs(fd: FunDef): Seq[Example] = {
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index fd3af5c50278afd441804b0962a36613f4c89d41..fc0826dbbc8bc78552e94a672d463c7ae7de6deb 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -244,10 +244,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
}
}
- case c @ Choose(cond, Some(impl)) =>
- rec(pathVar, impl)
-
- case c @ Choose(cond, None) =>
+ case c @ Choose(cond) =>
val cid = FreshIdentifier("choose", c.getType, true)
storeExpr(cid)
storeGuarded(pathVar, application(cond, Seq(Variable(cid))))
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index ca53ba5ae5f045bb1a451ae94508f16ecd6e42a3..884c18254fe97cf3cd61d450d70e5ca3d6165252 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -355,7 +355,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val nfd = fd.duplicate
nfd.fullBody = postMap {
- case ch if ch eq hctx.ci.ch =>
+ case src if src eq hctx.ci.source =>
Some(outerSolution.term)
case _ => None
@@ -363,6 +363,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
Some(nfd)
+ // We freshen/duplicate every functions, except these two as they are
+ // fresh anyway and we refer to them directly.
case `cTreeFd` | `phiFd` =>
None
@@ -373,10 +375,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
/**
- * Since CEGIS works with a copy of the outer program,
- * it needs to map outer function calls to inner function calls
- * and vice-versa. 'inner' refers to the CEGIS-specific program,
- * 'outer' refers to the actual program on which we do synthesis.
+ * Since CEGIS works with a copy of the program, it needs to map outer
+ * function calls to inner function calls and vice-versa. 'inner' refers
+ * to the CEGIS-specific program, 'outer' refers to the actual program on
+ * which we do synthesis.
*/
private def outerExprToInnerExpr(e: Expr): Expr = {
replaceFunCalls(e, {fd => origFdMap.getOrElse(fd, fd) })
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index ec24b4c93f642e02390c5add25fde7a13910684f..e6ef2c65d717f4956844dba3f681e5a1cea92b1b 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -233,7 +233,7 @@ object ImperativeCodeElimination extends TransformationPhase {
val (bodyRes, bodyScope, bodyFun) = toFunction(b)
(bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)).copiedFrom(expr), bodyFun)
}
- case c @ Choose(b, _) => {
+ case c @ Choose(b) => {
//Recall that Choose cannot mutate variables from the scope
(c, (b2: Expr) => b2, Map())
}