diff --git a/src/main/scala/leon/evaluators/AngelicEvaluator.scala b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
index c1374b54f39117c4ddf09c8315df012cc5d6a989..090eeff0f6d38a5802718989ff81fe623e670d4e 100644
--- a/src/main/scala/leon/evaluators/AngelicEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
@@ -4,12 +4,11 @@ package leon
package evaluators
import leon.solvers.Model
-import purescala.Definitions.Program
import purescala.Expressions.Expr
import EvaluationResults._
-class AngelicEvaluator(ctx: LeonContext, prog: Program, underlying: NDEvaluator)
- extends Evaluator(ctx, prog)
+class AngelicEvaluator(underlying: NDEvaluator)
+ extends Evaluator(underlying.context, underlying.program)
with DeterministicEvaluator
{
val description: String = "angelic evaluator"
@@ -24,3 +23,20 @@ class AngelicEvaluator(ctx: LeonContext, prog: Program, underlying: NDEvaluator)
other.asInstanceOf[Result[Nothing]]
}
}
+
+class DemonicEvaluator(underlying: NDEvaluator)
+ extends Evaluator(underlying.context, underlying.program)
+ with DeterministicEvaluator
+{
+ val description: String = "demonic evaluator"
+ val name: String = "Interpreter that demands an underlying non-deterministic program has unique solution"
+
+ def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
+ case Successful(Stream(h)) =>
+ Successful(h)
+ case Successful(_) =>
+ RuntimeError("Underlying ND-evaluator did not return unique solution!")
+ case other@(RuntimeError(_) | EvaluatorError(_)) =>
+ other.asInstanceOf[Result[Nothing]]
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index 5c951eedc1a68943c42d9ee4f07f8d58e5f74bf9..ed71ff7e33d14503e1871ce9b0347032d56b62f3 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
package leon
package evaluators
@@ -5,4 +7,5 @@ import purescala.Definitions.Program
class DefaultEvaluator(ctx: LeonContext, prog: Program)
extends RecursiveEvaluator(ctx, prog, 5000)
- with DefaultContexts
\ No newline at end of file
+ with HasDefaultGlobalContext
+ with HasDefaultRecContext
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index 05f60fd270f7d7ebc28b8627b703d23f30b6e214..98fd4b03c5133535eb6ff67ad9a2b86dfadc1a82 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -10,17 +10,16 @@ import purescala.Types._
import codegen._
-class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations) {
+class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams)
+ extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations)
+ with HasDefaultGlobalContext
+{
type RC = DualRecContext
- type GC = GlobalContext
-
- def initGC(model: solvers.Model) = new GlobalContext(model, this.maxSteps)
+ def initRC(mappings: Map[Identifier, Expr]): RC = DualRecContext(mappings)
implicit val debugSection = utils.DebugSectionEvaluation
- def initRC(mappings: Map[Identifier, Expr]): RC = DualRecContext(mappings)
-
var monitor = new runtime.LeonCodeGenRuntimeMonitor(params.maxFunctionInvocations)
val unit = new CompilationUnit(ctx, prog, params)
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 9843da81d4187e468cf418c6100f2ce68f2dfefd..7f86322b07b760c042d932d61002207609bb6524 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -3,6 +3,7 @@
package leon
package evaluators
+import leon.purescala.Types.TypeTree
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
@@ -50,4 +51,4 @@ trait DeterministicEvaluator extends Evaluator {
trait NDEvaluator extends Evaluator {
type Value = Stream[Expr]
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/evaluators/EvaluatorContexts.scala b/src/main/scala/leon/evaluators/EvaluatorContexts.scala
index 776e389dd855736132d8c066fc837cc2b4bc34ad..f5c71f8d9951a6ca4b90428e98c80984ae5f4328 100644
--- a/src/main/scala/leon/evaluators/EvaluatorContexts.scala
+++ b/src/main/scala/leon/evaluators/EvaluatorContexts.scala
@@ -29,11 +29,12 @@ class GlobalContext(val model: Model, val maxSteps: Int) {
var stepsLeft = maxSteps
}
-protected[evaluators] trait DefaultContexts extends ContextualEvaluator {
-
- final type RC = DefaultRecContext
- final type GC = GlobalContext
-
+trait HasDefaultRecContext extends ContextualEvaluator {
+ type RC = DefaultRecContext
def initRC(mappings: Map[Identifier, Expr]) = DefaultRecContext(mappings)
+}
+
+trait HasDefaultGlobalContext extends ContextualEvaluator {
def initGC(model: solvers.Model) = new GlobalContext(model, this.maxSteps)
+ type GC = GlobalContext
}
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index d1392d498b367475191ad8e42f82aa64778f5ccc..972a2a459af2285ef4fc1de8e6b73d69e1723c2f 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -3,17 +3,16 @@
package leon
package evaluators
-import leon.purescala.Constructors._
-import leon.purescala.ExprOps._
-import leon.purescala.Expressions.Pattern
-import leon.purescala.Extractors._
-import leon.purescala.Quantification._
-import leon.purescala.TypeOps._
-import leon.purescala.Types._
-import leon.solvers.{SolverFactory, HenkinModel}
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Expressions.Pattern
+import purescala.Extractors._
+import purescala.TypeOps._
+import purescala.Types._
import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._
+import solvers.SolverFactory
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int)
extends ContextualEvaluator(ctx, prog, maxSteps)
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index 5b387368ba259ac4cbeb2cf8f716feace7d370d9..1a5c9e0630e720e4769236688d9e22eec6bbf45c 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -13,21 +13,18 @@ import purescala.Definitions.{TypedFunDef, Program}
import purescala.Expressions._
import leon.solvers.SolverFactory
-import leon.utils.StreamUtils.cartesianProduct
+import leon.utils.StreamUtils._
class StreamEvaluator(ctx: LeonContext, prog: Program)
extends ContextualEvaluator(ctx, prog, 50000)
with NDEvaluator
- with DefaultContexts
+ with HasDefaultGlobalContext
+ with HasDefaultRecContext
{
val name = "ND-evaluator"
val description = "Non-deterministic interpreter for Leon programs that returns a Stream of solutions"
- case class NDValue(tp: TypeTree) extends Expr with Terminal {
- val getType = tp
- }
-
protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Stream[Expr] = expr match {
case Variable(id) =>
rctx.mappings.get(id).toStream
@@ -74,10 +71,6 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
case Error(tpe, desc) =>
Stream()
- case NDValue(tp) =>
- import grammars.ValueGrammar
- ValueGrammar.getProductions(tp).toStream.map{ g => g.builder(Seq())}
-
case IfExpr(cond, thenn, elze) =>
e(cond).distinct.flatMap {
case BooleanLiteral(true) => e(thenn)
@@ -226,7 +219,8 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
solverf.shutdown()
}
sol
- }).takeWhile(_.isDefined).map(_.get)
+ }).takeWhile(_.isDefined).take(10).map(_.get)
+ // This take(10) is there because we are not working well with infinite streams yet...
} catch {
case e: Throwable =>
solverf.reclaim(solver)
@@ -586,6 +580,4 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
}
-
}
-
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c0fd0d23603d0d55ad7f2ca0c12c80ee03a721ba..9150e91bfef8e062958198958565910973cb6498 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1140,12 +1140,47 @@ object ExprOps {
GenericValue(tp, 0)
case FunctionType(from, to) =>
- val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true)))
+ val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, alwaysShowUniqueID = true)))
Lambda(args, simplestValue(to))
case _ => throw LeonFatalError("I can't choose simplest value for type " + tpe)
}
+ def valuesOf(tp: TypeTree): Stream[Expr] = {
+ import utils.StreamUtils._
+ tp match {
+ case BooleanType =>
+ Stream(BooleanLiteral(false), BooleanLiteral(true))
+ case Int32Type =>
+ Stream.iterate(0) { prev =>
+ if (prev > 0) -prev else -prev + 1
+ } map IntLiteral
+ case IntegerType =>
+ Stream.iterate(BigInt(0)) { prev =>
+ if (prev > 0) -prev else -prev + 1
+ } map InfiniteIntegerLiteral
+ case UnitType =>
+ Stream(UnitLiteral())
+ case tp: TypeParameter =>
+ Stream.from(0) map (GenericValue(tp, _))
+ case TupleType(stps) =>
+ cartesianProduct(stps map (tp => valuesOf(tp))) map Tuple
+ case SetType(base) =>
+ def elems = valuesOf(base)
+ elems.scanLeft(Stream(FiniteSet(Set(), base): Expr)){ (prev, curr) =>
+ prev flatMap {
+ case fs@FiniteSet(elems, tp) =>
+ Stream(fs, FiniteSet(elems + curr, tp))
+ }
+ }.flatten // FIXME Need cp οr is this fine?
+ case cct: CaseClassType =>
+ cartesianProduct(cct.fieldsTypes map valuesOf) map (CaseClass(cct, _))
+ case act: AbstractClassType =>
+ interleave(act.knownCCDescendants.map(cct => valuesOf(cct)))
+ }
+ }
+
+
/** Hoists all IfExpr at top level.
*
* Guarantees that all IfExpr will be at the top level and as soon as you
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index e9d63b1b96db406da3aa34e80c735b7bbbe9cdf6..56e8467478f5f0135945b9a72da0e525e4ac2c70 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -1,81 +1,25 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-package leon.repair
-
-import leon.purescala._
-import Definitions._
-import Expressions._
-import Types._
-import ExprOps.postMap
-import Constructors.not
-import leon.LeonContext
-import leon.evaluators.DefaultEvaluator
-import scala.util.Try
-
-// This evaluator treats the condition cond non-deterministically in the following sense:
-// If a function invocation fails or violates a postcondition for cond,
-// it backtracks and gets executed again for !cond
-class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr) extends DefaultEvaluator(ctx, prog) {
-
- override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
-
- case FunctionInvocation(tfd, args) if tfd.fd == fd =>
- if (gctx.stepsLeft < 0) {
- throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
- }
- gctx.stepsLeft -= 1
-
- val evArgs = args.map(a => e(a))
-
- // build a mapping for the function...
- val frame = rctx.newVars(tfd.paramSubst(evArgs))
-
- if(tfd.hasPrecondition) {
- e(tfd.precondition.get)(frame, gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) =>
- throw RuntimeError("Precondition violation for " + tfd.id.name + " reached in evaluation.: " + tfd.precondition.get)
- case other =>
- throw RuntimeError(typeErrorMsg(other, BooleanType))
- }
- }
-
- if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Evaluation of function with unknown implementation.")
- }
-
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
-
- def treat(subst : Expr => Expr) = {
- val callResult = e(subst(body))(frame, gctx)
-
- tfd.postcondition match {
- case Some(post) =>
- e(subst(Application(post, Seq(callResult))))(frame, gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) => throw RuntimeError("Postcondition violation for " + tfd.id.name + " reached in evaluation.")
- case other => throw EvalError(typeErrorMsg(other, BooleanType))
- }
- case None =>
- }
-
- callResult
- }
-
- Try {
- treat(e => e)
- }.getOrElse {
- treat( postMap {
- // Use reference equality, just in case cond appears again in the program
- case c if c eq cond => Some(not(cond))
- case _ => None
- })
- }
-
- case _ => super.e(expr)
+package leon
+package repair
+
+import purescala.Definitions.Program
+import purescala.Expressions._
+import purescala.ExprOps.valuesOf
+import evaluators.StreamEvaluator
+
+/** This evaluator treats the expression [[nd]] (reference equality) as a non-deterministic value */
+class RepairNDEvaluator(ctx: LeonContext, prog: Program, nd: Expr) extends StreamEvaluator(ctx, prog) {
+
+ override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Stream[Expr] = expr match {
+ case Not(c) if c eq nd =>
+ // This is a hack: We know the only way nd is wrapped within a Not is if it is NOT within
+ // a recursive call. So we need to treat it deterministically at this point...
+ super.e(c) collect { case BooleanLiteral(b) => BooleanLiteral(!b) }
+ case c if c eq nd =>
+ valuesOf(c.getType)
+ case other =>
+ super.e(other)
}
-
-
-
}
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 2846bc4848bd12147a68f7c03a3b7319f8aae88c..fd12f7216f482fa50ce84816caa79fa8a450d689 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -16,13 +16,11 @@ import leon.evaluators._
* as well as if each invocation was successful or erroneous (led to an error)
* (.fiStatus)
*/
-class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) {
+class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext {
type RC = CollectingRecContext
- type GC = GlobalContext
def initRC(mappings: Map[Identifier, Expr]) = CollectingRecContext(mappings, None)
- def initGC(model: leon.solvers.Model) = new GlobalContext(model, maxSteps)
-
+
type FI = (FunDef, Seq[Expr])
// This is a call graph to track dependencies of function invocations.
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index d6b4d874ffc1063dc2288f39af3f862a35542371..93520c5ea9cd467cf73a94392a565022782eb3d9 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -4,8 +4,9 @@ package leon
package repair
package rules
+import sun.nio.cs.StreamEncoder
import synthesis._
-import evaluators._
+import leon.evaluators._
import purescala.Expressions._
import purescala.Common._
@@ -93,11 +94,10 @@ case object Focus extends PreprocessingRule("Focus") {
def testCondition(cond: Expr) = {
val ndSpec = postMap {
- case c if c eq cond => Some(not(cond)) // Use reference equality
+ case c if c eq cond => Some(not(cond))
case _ => None
}(fdSpec)
-
- forAllTests(ndSpec, Map(), new RepairNDEvaluator(ctx, program, fd, cond))
+ forAllTests(ndSpec, Map(), new AngelicEvaluator(new RepairNDEvaluator(ctx, program, cond)))
}
guides.flatMap {
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index c972f2e27dd1a28325f8477fa2042ea0620bc78f..2ea08a593725b6f28f4e96be85a00088eb1f9f76 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -3,17 +3,23 @@
package leon.utils
object StreamUtils {
- def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
- var ss = streams
- while(ss.nonEmpty && ss.head.isEmpty) {
- ss = ss.tail
+
+ def interleave[T](streams: Stream[Stream[T]]): Stream[T] = {
+ def rec(streams: Stream[Stream[T]], diag: Int): Stream[T] = {
+ if(streams.isEmpty) Stream() else {
+ val (take, leave) = streams.splitAt(diag)
+ val (nonEmpty, empty) = take partition (_.nonEmpty)
+ nonEmpty.map(_.head) ++ rec(nonEmpty.map(_.tail) ++ leave, diag + 1 - empty.size)
+ }
}
- if(ss.isEmpty) return Stream.empty
- if(ss.size == 1) return ss.head
+ rec(streams, 1)
+ }
- // TODO: This circular-shifts the list. I'd be interested in a constant time
- // operation. Perhaps simply by choosing the right data-structure?
- Stream.cons(ss.head.head, interleave(ss.tail :+ ss.head.tail))
+ def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
+ if (streams.isEmpty) Stream() else {
+ val nonEmpty = streams filter (_.nonEmpty)
+ nonEmpty.toStream.map(_.head) ++ interleave(nonEmpty.map(_.tail))
+ }
}
def cartesianProduct[T](streams : Seq[Stream[T]]) : Stream[List[T]] = {
diff --git a/src/test/resources/regression/repair/Heap3.scala b/src/test/resources/regression/repair/Heap3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3305b5d15a0731bd3aeaa1269c2404807f49a266
--- /dev/null
+++ b/src/test/resources/regression/repair/Heap3.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2015 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.lang._
+import leon.collection._
+
+object Heaps {
+
+ sealed abstract class Heap {
+ val rank : BigInt = this match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ 1 + max(l.rank, r.rank)
+ }
+ def content : Set[BigInt] = this match {
+ case Leaf() => Set[BigInt]()
+ case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+ case class Leaf() extends Heap
+ case class Node(value:BigInt, left: Heap, right: Heap) extends Heap
+
+ def max(i1 : BigInt, i2 : BigInt) = if (i1 >= i2) i1 else i2
+
+ def hasHeapProperty(h : Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(v, l, r) =>
+ ( l match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ }) &&
+ ( r match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ })
+ }
+
+ def hasLeftistProperty(h: Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(_,l,r) =>
+ hasLeftistProperty(l) &&
+ hasLeftistProperty(r) &&
+ l.rank >= r.rank
+ }
+
+ def heapSize(t: Heap): BigInt = { t match {
+ case Leaf() => BigInt(0)
+ case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+ }} ensuring(_ >= 0)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 >= v2) // FIXME swapped the branches
+ makeN(v2, l2, merge(h1, r2))
+ else
+ makeN(v1, l1, merge(r1, h2))
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+ }
+
+ private def makeN(value: BigInt, left: Heap, right: Heap) : Heap = {
+ require(
+ hasLeftistProperty(left) && hasLeftistProperty(right)
+ )
+ if(left.rank >= right.rank)
+ Node(value, left, right)
+ else
+ Node(value, right, left)
+ } ensuring { res =>
+ hasLeftistProperty(res) }
+
+ def insert(element: BigInt, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1 &&
+ res.content == heap.content ++ Set(element)
+ }
+
+ def findMax(h: Heap) : Option[BigInt] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h) && hasHeapProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res)
+ }
+
+}
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index 82c419b043468ebe20cc5422630f96a1d5128457..ff882c96157cb6b85b02e101a3c0b84e0cfe058f 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -206,7 +206,7 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
List(
new DefaultEvaluator(ctx, pgm),
- new AngelicEvaluator(ctx, pgm, new StreamEvaluator(ctx, pgm))
+ new AngelicEvaluator(new StreamEvaluator(ctx, pgm))
)
}
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 50b845f923e2356d1ce4c0c9a27692a78cd30ce5..5b6667d5f4233521a4dc79a5d309618e49e8f07d 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -16,6 +16,7 @@ class RepairSuite extends LeonRegressionSuite {
val fileToFun = Map(
"Compiler1.scala" -> "desugar",
+ "Heap3.scala" -> "merge",
"Heap4.scala" -> "merge",
"ListEasy.scala" -> "pad",
"List1.scala" -> "pad",
@@ -23,7 +24,10 @@ class RepairSuite extends LeonRegressionSuite {
"MergeSort2.scala" -> "merge"
)
- for (file <- filesInResourceDir("regression/repair/", _.endsWith(".scala")) if fileToFun contains file.getName) {
+ for (file <- filesInResourceDir("regression/repair/", _.endsWith(".scala"))) {
+ if (!(fileToFun contains file.getName)) {
+ fail(s"Don't know which function to repair for ${file.getName}")
+ }
val path = file.getAbsoluteFile.toString
val name = file.getName
diff --git a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
index 4002a0af0fb4ef8c71bf7542af74a6f8d6d366c9..b510c01bb891532c60cace6017b2a61d09bfdbb3 100644
--- a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
@@ -20,7 +20,7 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
List(
new DefaultEvaluator(ctx, pgm),
- new AngelicEvaluator(ctx, pgm, new StreamEvaluator(ctx, pgm))
+ new AngelicEvaluator(new StreamEvaluator(ctx, pgm))
)
}