From 6a146f673cfbc81c954d2ef56990af599e55102b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 6 Jul 2015 13:43:49 +0200
Subject: [PATCH] If the test has outputs, use it to filter as well
---
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 13 ++++++++++---
1 file changed, 10 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 8178cc6c8..bdd5e54d9 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -408,9 +408,16 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// TODO: Test output value as well
val envMap = bs.map(b => b -> BooleanLiteral(bValues(b))).toMap
- val fi = FunctionInvocation(phiFd.typed, ex.ins)
-
- evaluator.eval(fi, envMap)
+ ex match {
+ case InExample(ins) =>
+ val fi = FunctionInvocation(phiFd.typed, ins)
+ evaluator.eval(fi, envMap)
+
+ case InOutExample(ins, outs) =>
+ val fi = FunctionInvocation(cTreeFd.typed, ins)
+ val eq = equality(fi, tupleWrap(outs))
+ evaluator.eval(eq, envMap)
+ }
}
}
--
GitLab