From 79eb9ef7bb81701ac1b2e4acbdc17747b28d07ee Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 20 Nov 2015 15:54:12 +0100
Subject: [PATCH] String Tracing evaluator (invomplete!)
---
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../evaluators/StringTracingEvaluator.scala | 34 +++++++++++++++++++
2 files changed, 35 insertions(+), 1 deletion(-)
create mode 100644 src/main/scala/leon/evaluators/StringTracingEvaluator.scala
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 3b77842b9..fecd9f6ba 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 000000000..7ee82434a
--- /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))
+ }
+
+
+}
--
GitLab