diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala index 3b77842b9a0725df6b448d46656bf90f68dbb79d..fecd9f6baf5fef58e0424fce41dd93971123fa16 100644 --- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala +++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala @@ -26,7 +26,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int protected var clpCache = Map[(Choose, Seq[Expr]), Expr]() - protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match { + protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match { case Variable(id) => rctx.mappings.get(id) match { case Some(v) if v != expr => diff --git a/src/main/scala/leon/evaluators/StringTracingEvaluator.scala b/src/main/scala/leon/evaluators/StringTracingEvaluator.scala new file mode 100644 index 0000000000000000000000000000000000000000..7ee82434adf68586bea06446f980f3756ecfb8e7 --- /dev/null +++ b/src/main/scala/leon/evaluators/StringTracingEvaluator.scala @@ -0,0 +1,34 @@ +/* Copyright 2009-2015 EPFL, Lausanne */ + +package leon +package evaluators + +import purescala.Extractors.Operator +import purescala.Expressions._ +import purescala.Definitions.Program +import purescala.Expressions.Expr + +class StringTracingEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvaluator(ctx, prog, 50000) with DefaultContexts { + + val underlying = new DefaultEvaluator(ctx, prog) + override type Value = (Expr, Expr) + + override val description: String = ??? // FIXME + override val name: String = ??? // FIXME + + protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = expr match { + case StringConcat(s1, s2) => + val (es1, t1) = e(s1) + val (es2, t2) = e(s2) + (underlying.e(StringConcat(es1, es2)), StringConcat(t1, t2)) + + case StringLength(_) => ??? // FIXME + case StringLiteral(_) => ??? // FIXME + + case Operator(es, builder) => + val (ees, ts) = es.map(e).unzip + (underlying.e(builder(ees)), builder(ts)) + } + + +}