From e8e87ca81b551dc59816dba40ae676c6c4ea40da Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 19 Oct 2015 12:27:11 +0200
Subject: [PATCH] convertHoles -> convert
---
.../scala/leon/evaluators/RecursiveEvaluator.scala | 11 ++++++-----
src/main/scala/leon/synthesis/ConversionPhase.scala | 4 ++--
2 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 502563f0f..80f71fd87 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -14,8 +14,6 @@ import purescala.Extractors._
import purescala.Quantification._
import solvers.{Model, HenkinModel}
import solvers.SolverFactory
-import synthesis.ConversionPhase.convertHoles
-import leon.purescala.ExprOps
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int) extends Evaluator(ctx, prog) {
val name = "evaluator"
@@ -123,11 +121,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case en@Ensuring(body, post) =>
if ( exists{
case Hole(_,_) => true
+ case WithOracle(_,_) => true
case _ => false
- }(en))
- e(convertHoles(en, ctx))
- else
+ }(en)) {
+ import synthesis.ConversionPhase.convert
+ e(convert(en, ctx))
+ } else {
e(en.toAssert)
+ }
case Error(tpe, desc) =>
throw RuntimeError("Error reached in evaluation: " + desc)
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index bab77552b..d76cff69b 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -78,7 +78,7 @@ object ConversionPhase extends UnitPhase[Program] {
*
*/
- def convertHoles(e : Expr, ctx : LeonContext) : Expr = {
+ def convert(e : Expr, ctx : LeonContext) : Expr = {
val (pre, body, post) = breakDownSpecs(e)
// Ensure that holes are not found in pre and/or post conditions
@@ -178,7 +178,7 @@ object ConversionPhase extends UnitPhase[Program] {
def apply(ctx: LeonContext, pgm: Program): Unit = {
// TODO: remove side-effects
for (fd <- pgm.definedFunctions) {
- fd.fullBody = convertHoles(fd.fullBody,ctx)
+ fd.fullBody = convert(fd.fullBody,ctx)
}
}
--
GitLab