From a1f164dd14ba8b07d16797e3ae48ed7a7c8dde81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Tue, 12 Apr 2016 18:07:17 +0200
Subject: [PATCH] Added the function invocation coverage.
---
.../disambiguation/InputCoverage.scala | 27 +++++++++++++------
1 file changed, 19 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
index e50a51440..409e55440 100644
--- a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
@@ -17,8 +17,8 @@ import bonsai.enumerators.MemoizedEnumerator
import solvers.Model
import solvers.ModelBuilder
import scala.collection.mutable.ListBuffer
-
import leon.LeonContext
+import leon.purescala.Definitions.TypedFunDef
/**
* @author Mikael
@@ -63,6 +63,7 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
}).unzip // TODO: Check for unapply with function pattern ?
(MatchExpr(c1, new_cases).copiedFrom(e), variables.flatten)
case Operator(lhsrhs, builder) =>
+ // The exprBuilder adds variable definitions needed to compute the arguments.
val (exprBuilder, children, ids) = (((e: Expr) => e, List[Expr](), ListBuffer[Identifier]()) /: lhsrhs) {
case ((exprBuilder, children, ids), arg) =>
val (arg1, argv1) = markBranches(arg)
@@ -75,13 +76,23 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
(exprBuilder, arg::children, ids)
}
}
- if(e.isInstanceOf[FunctionInvocation]) {
- // Should be different.
- } else if(ids.isEmpty) {
- (e, Seq.empty)
- } else {
- val body = tupleWrap(Seq(builder(children).copiedFrom(e), or(ids.map(Variable): _*)))
- (exprBuilder(body), ids)
+ e match {
+ case FunctionInvocation(TypedFunDef(fd, targs), args) =>
+ // Should be different since functions will return a boolean as well.
+ val res_id = FreshIdentifier("res", fd.returnType)
+ val res_b = FreshIdentifier("b", BooleanType)
+ val finalIds = (ids :+ res_b)
+ val finalExpr =
+ tupleWrap(Seq(Variable(res_id), or(finalIds.map(Variable(_)): _*)))
+ val funCall = letTuple(Seq(res_id, res_b), builder(children).copiedFrom(e), finalExpr)
+ (exprBuilder(funCall), finalIds)
+ case _ =>
+ if(ids.isEmpty) {
+ (e, Seq.empty)
+ } else {
+ val finalExpr = tupleWrap(Seq(builder(children).copiedFrom(e), or(ids.map(Variable): _*)))
+ (exprBuilder(finalExpr), ids)
+ }
}
}
--
GitLab