diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/evaluators/TrackingEvaluator.scala similarity index 88% rename from src/main/scala/leon/repair/RepairTrackingEvaluator.scala rename to src/main/scala/leon/evaluators/TrackingEvaluator.scala index 67707d6cfd7136c2145ff29c33cebde200cf18e7..e4815992c415b588de30c5bdd27de53146c519a0 100644 --- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala +++ b/src/main/scala/leon/evaluators/TrackingEvaluator.scala @@ -1,22 +1,20 @@ /* Copyright 2009-2016 EPFL, Lausanne */ -package leon.repair +package leon +package evaluators + +import purescala.Common._ +import purescala.Definitions._ +import purescala.Expressions._ +import purescala.Types._ -import scala.collection.immutable.Map import scala.collection.mutable.{Map => MMap} -import leon.purescala.Common._ -import leon.purescala.Expressions._ -import leon.purescala.Types._ -import leon.purescala.Definitions._ -import leon.LeonContext -import leon.evaluators._ -/** - * This evaluator tracks all dependencies between function calls (.fullCallGraph) - * as well as if each invocation was successful or erroneous (led to an error) - * (.fiStatus) +/** An [[Evaluator]] that tracks information about the runtime call tree. + * Transitive dependencies between function calls are stored in [[fullCallGraph]]. + * Additionally, [[fiStatus]] tracks if each function invocation was successful or erroneous (led to an error). */ -class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext { +class TrackingEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext { type RC = CollectingRecContext def initRC(mappings: Map[Identifier, Expr]) = CollectingRecContext(mappings, None) diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala index 7859f7957d59eaefd9f1dfcfd03cbded09f724b9..63a114ff9dcc0c4b934b2c92ce3a399937abb629 100644 --- a/src/main/scala/leon/repair/RepairNDEvaluator.scala +++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala @@ -8,7 +8,9 @@ import purescala.Expressions._ import purescala.ExprOps.valuesOf import evaluators.StreamEvaluator -/** This evaluator treats the expression [[nd]] (reference equality) as a non-deterministic value */ +/** A [[leon.evaluators.StreamEvaluator StreamEvaluator]] that treats a specified expression [[nd]] as a non-deterministic value + * @note Expressions are compared against [[nd]] with reference equality. + */ 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 { diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala index ad75eaace4937ec1403e5523f176489717b7a20b..690ba4b87868cb14e109a56732b8aaddd53f26d3 100644 --- a/src/main/scala/leon/synthesis/ExamplesBank.scala +++ b/src/main/scala/leon/synthesis/ExamplesBank.scala @@ -3,12 +3,11 @@ package leon package synthesis -import evaluators.DefaultEvaluator import purescala.Definitions._ import purescala.Expressions._ import purescala.Constructors._ import purescala.Common._ -import repair._ +import evaluators.{TrackingEvaluator, DefaultEvaluator} import leon.utils.ASCIIHelpers._ /** Sets of valid and invalid examples */ @@ -18,7 +17,7 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) { // 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): ExamplesBank = { - val evaluator = new RepairTrackingEvaluator(ctx, program) + val evaluator = new TrackingEvaluator(ctx, program) invalids foreach { ts => evaluator.eval(functionInvocation(fd, ts.ins))