From b629f6bd33042904cb4e977b6c7791af20ae1e44 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 29 Apr 2016 16:39:13 +0200
Subject: [PATCH] Work on ExamplesBank
All map* -> flatMap*
Add evalIns which evaluates all inputs
All QualifiedExamplesBank methods now return QEBs
Problem.qebFiltered evaluates first
---
.../scala/leon/evaluators/Evaluator.scala | 34 +++++++++++--------
.../scala/leon/synthesis/ExamplesBank.scala | 19 +++++++----
src/main/scala/leon/synthesis/Problem.scala | 2 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 4 +--
.../leon/synthesis/rules/DetupleInput.scala | 2 +-
.../synthesis/rules/EquivalentInputs.scala | 2 +-
6 files changed, 36 insertions(+), 27 deletions(-)
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 9f7f0fbe2..e5e6fd1a7 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -53,25 +53,29 @@ trait DeterministicEvaluator extends Evaluator {
override def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = {
if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
super.eval(expr, mapping.toMap)
- } else (_evalEnv(mapping) match {
- case Left(m) => super.eval(expr, m)
- case Right(errorMessage) =>
- val m = mapping.filter{ case (k, v) => purescala.ExprOps.isValue(v) }.toMap
- super.eval(expr, m) match {
- case res @ evaluators.EvaluationResults.Successful(result) => res
- case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
- }
- })
+ } else {
+ _evalEnv(mapping) match {
+ case Left(m) => super.eval(expr, m)
+ case Right(errorMessage) =>
+ val m = mapping.filter { case (k, v) => purescala.ExprOps.isValue(v) }
+ super.eval(expr, m) match {
+ case res@evaluators.EvaluationResults.Successful(result) => res
+ case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
+ }
+ }
+ }
}
/** Returns an evaluated environment. If it fails, removes all non-values from the environment. */
def evalEnv(mapping: Iterable[(Identifier, Expr)]): Map[Identifier, Value] = {
if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
mapping.toMap
- } else (_evalEnv(mapping) match {
- case Left(m) => m
- case Right(msg) => mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
- })
+ } else {
+ _evalEnv(mapping) match {
+ case Left(m) => m
+ case Right(msg) => mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
+ }
+ }
}
/** From a not yet well evaluated context with dependencies between variables, returns a head where all exprs are values (as a Left())
@@ -158,10 +162,10 @@ object Evaluator {
/* Status of the invariant checking for `cc` */
def invariantCheck(cc: CaseClass): CheckStatus = synchronized {
if (!cc.ct.classDef.hasInvariant) Complete(true)
- else checkCache.get(cc).getOrElse {
+ else checkCache.getOrElse(cc, {
checkCache(cc) = Pending
NoCheck
- }
+ })
}
/* Update the cache with the invariant check result for `cc` */
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index ed22fa0ec..9d48defd5 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -70,13 +70,13 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
}
}
- def map(f: Example => List[Example]) = {
+ def flatMap(f: Example => List[Example]) = {
ExamplesBank(valids.flatMap(f), invalids.flatMap(f))
}
/** Expands each input example through the function f */
def flatMapIns(f: Seq[Expr] => List[Seq[Expr]]) = {
- map {
+ flatMap {
case InExample(in) =>
f(in).map(InExample)
@@ -87,7 +87,7 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
/** Expands each output example through the function f */
def flatMapOuts(f: Seq[Expr] => List[Seq[Expr]]) = {
- map {
+ flatMap {
case InOutExample(in, out) =>
f(out).map(InOutExample(in, _))
@@ -97,7 +97,7 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
}
def stripOuts = {
- map {
+ flatMap {
case InOutExample(in, out) =>
List(InExample(in))
case e =>
@@ -190,6 +190,11 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
filterIns(m => evaluator.eval(expr, m).result.contains(BooleanLiteral(true)))
}
+ def evalIns: QualifiedExamplesBank = flatMapIns { mapping =>
+ val evalAs = evaluator.evalEnv(mapping)
+ List(as map evalAs)
+ }
+
/** Filters inputs through the predicate pred, with an assignment of input variables to expressions. */
def filterIns(pred: Map[Identifier, Expr] => Boolean): QualifiedExamplesBank = {
QualifiedExamplesBank(as, xs,
@@ -207,14 +212,14 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
/** Maps inputs through the function f
*
* @return A new ExampleBank */
- def mapIns(f: Seq[(Identifier, Expr)] => List[Seq[Expr]]) = {
- eb map {
+ def flatMapIns(f: Seq[(Identifier, Expr)] => List[Seq[Expr]]): QualifiedExamplesBank = {
+ copy(eb = eb flatMap {
case InExample(in) =>
f(as zip in).map(InExample)
case InOutExample(in, out) =>
f(as zip in).map(InOutExample(_, out))
- }
+ })
}
}
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 46d01ece1..8d7677d32 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -52,7 +52,7 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Path, phi: Expr, xs: List
copy(ws = andJoin(wsList ++ es))
}
- def qebFiltered(implicit sctx: SearchContext) = qeb.filterIns(pc.fullClause)
+ def qebFiltered(implicit sctx: SearchContext) = qeb.evalIns.filterIns(pc.fullClause)
// Qualified example bank, allows us to perform operations (e.g. filter) with expressions
def qeb(implicit sctx: SearchContext) = QualifiedExamplesBank(this.as, this.xs, eb)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 5b5070124..379eaf59f 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -91,7 +91,7 @@ case object ADTSplit extends Rule("ADT Split.") {
if (isInputVar) {
// Filter out examples where id has the wrong type, and fix input variables
// Note: It is fine to filter here as no evaluation is required
- p.qeb.mapIns { inInfo =>
+ p.qeb.flatMapIns { inInfo =>
inInfo.toMap.apply(id) match {
case CaseClass(`cct`, vs) =>
List(vs ++ inInfo.filter(_._1 != id).map(_._2))
@@ -100,7 +100,7 @@ case object ADTSplit extends Rule("ADT Split.") {
}
}
} else {
- p.eb
+ p.qeb
}
}
val newAs = if (isInputVar) args ::: oas else p.as
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index a08f10479..73bd53363 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -103,7 +103,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
}
}.toMap
- val eb = p.qeb.mapIns { info =>
+ val eb = p.qeb.flatMapIns { info =>
List(info.flatMap { case (id, v) =>
ebMapInfo.get(id) match {
case Some(m) =>
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 65e5dd1ac..74abe6721 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -79,7 +79,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
// XXX: must take place in this order!! obsolete & free is typically non-empty
val newAs = (p.as ++ free).distinct.filterNot(obsolete)
- val newBank = p.eb.map { ex =>
+ val newBank = p.eb.flatMap { ex =>
val mapping = (p.as zip ex.ins).toMap
val newIns = newAs.map(a => mapping.getOrElse(a, replaceFromIDs(mapping, reverseSubst(a))))
List(ex match {
--
GitLab