diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 67dcf315770120734684a459bad0b0d3be96120e..8597a0af22859ba0f730a0b534dd0b244a79a2c0 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -61,7 +61,7 @@ object Constructors {
else bd
}
- /** $encodingof ``val (id1, id2, ...) = e; bd``, and returns `bd` if the identifiers are not bound in `bd`.
+ /** $encodingof ``val (...binders...) = value; body`` which is translated to ``value match { case (...binders...) => body }``, and returns `body` if the identifiers are not bound in `body`.
* @see [[purescala.Expressions.Let]]
*/
def letTuple(binders: Seq[Identifier], value: Expr, body: Expr) = binders match {
@@ -72,7 +72,7 @@ object Constructors {
case xs =>
require(
value.getType.isInstanceOf[TupleType],
- s"The definition value in LetTuple must be of some tuple type; yet we got [${value.getType}]. In expr: \n$this"
+ s"The definition value in LetTuple must be of some tuple type; yet we got [${value.getType}]. In expr: \n$value"
)
Extractors.LetPattern(TuplePattern(None,binders map { b => WildcardPattern(Some(b)) }), value, body)
diff --git a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
index 409e55440e7fbee137be1e2836786ca00eed9115..f2b0946c6036c422f07623d619eb2d7ebc13a548 100644
--- a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
@@ -33,10 +33,10 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
/** If the sub-branches contain identifiers, it returns them unchanged.
Else it creates a new boolean indicating this branch. */
def wrapBranch(e: (Expr, Seq[Identifier])): (Expr, Seq[Identifier]) = {
- if(e._2.isEmpty) { // No need to introduce a new boolean since if one of the child booleans is true, then this IfExpr has been called.
- val b = FreshIdentifier("l" + e._1.getPos.line + "c" + e._1.getPos.col)
+ if(e._2.isEmpty) {
+ val b = FreshIdentifier("l" + e._1.getPos.line + "c" + e._1.getPos.col, BooleanType)
(tupleWrap(Seq(e._1, Variable(b))), Seq(b))
- } else e
+ } else e // No need to introduce a new boolean since if one of the child booleans is true, then this IfExpr has been called.
}
def hasConditionals(e: Expr) = {
@@ -53,8 +53,13 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
val (c1, cv1) = markBranches(cond)
val (t1, tv1) = wrapBranch(markBranches(thenn))
val (e1, ev1) = wrapBranch(markBranches(elze))
- // TODO: Deal with the case when t1 and e1 is empty.
- (IfExpr(c1, t1, e1).copiedFrom(e), cv1 ++ tv1 ++ ev1)
+ if(cv1.isEmpty) {
+ (IfExpr(c1, t1, e1).copiedFrom(e), tv1 ++ ev1)
+ } else {
+ val arg_id = FreshIdentifier("arg", BooleanType)
+ val arg_b = FreshIdentifier("b", BooleanType)
+ (letTuple(Seq(arg_id, arg_b), c1, IfExpr(Variable(arg_id), t1, e1).copiedFrom(e)), cv1 ++ tv1 ++ ev1)
+ }
case MatchExpr(scrut, cases) =>
val (c1, cv1) = markBranches(scrut)
val (new_cases, variables) = (cases map { case MatchCase(pattern, opt, rhs) =>
@@ -77,15 +82,21 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
}
}
e match {
- case FunctionInvocation(TypedFunDef(fd, targs), args) =>
- // Should be different since functions will return a boolean as well.
+ case FunctionInvocation(TypedFunDef(fd, targs), args) if fds(fd) =>
+ val new_fd = wrapFunDef(fd)
+ // Is 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)
+ if(ids.isEmpty) {
+ val funCall = FunctionInvocation(TypedFunDef(new_fd, targs), children).copiedFrom(e)
+ (exprBuilder(funCall), Seq(res_b))
+ } else {
+ val finalIds = (ids :+ res_b)
+ val finalExpr =
+ tupleWrap(Seq(Variable(res_id), or(finalIds.map(Variable(_)): _*)))
+ val funCall = letTuple(Seq(res_id, res_b), FunctionInvocation(TypedFunDef(new_fd, targs), children).copiedFrom(e), finalExpr)
+ (exprBuilder(funCall), finalIds)
+ }
case _ =>
if(ids.isEmpty) {
(e, Seq.empty)
@@ -96,6 +107,17 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
}
}
+ var cache = Map[FunDef, FunDef]()
+
+ def wrapFunDef(fd: FunDef): FunDef = {
+ if(!(cache contains fd)) {
+ val new_fd = fd.duplicate(returnType = TupleType(Seq(fd.returnType, BooleanType)))
+ new_fd.body = None
+ cache += fd -> new_fd
+ }
+ cache(fd)
+ }
+
/** The number of expressions is the same as the number of arguments. */
def result(): Stream[Seq[Expr]] = {
/* Algorithm:
diff --git a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7bc13e757ead777a797a79fae98fb284c8089b98
--- /dev/null
+++ b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
@@ -0,0 +1,184 @@
+package leon.integration.solvers
+
+import org.scalatest.FunSuite
+import org.scalatest.Matchers
+import leon.test.helpers.ExpressionsDSL
+import leon.solvers.string.StringSolver
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Common.Identifier
+import leon.purescala.Expressions._
+import leon.purescala.Definitions._
+import leon.purescala.DefOps
+import leon.purescala.ExprOps
+import leon.purescala.Types._
+import leon.purescala.TypeOps
+import leon.purescala.Constructors._
+import leon.synthesis.rules.{StringRender, TypedTemplateGenerator}
+import scala.collection.mutable.{HashMap => MMap}
+import scala.concurrent.Future
+import scala.concurrent.ExecutionContext.Implicits.global
+import org.scalatest.concurrent.Timeouts
+import org.scalatest.concurrent.ScalaFutures
+import org.scalatest.time.SpanSugar._
+import org.scalatest.FunSuite
+import org.scalatest.concurrent.Timeouts
+import org.scalatest.concurrent.ScalaFutures
+import org.scalatest.time.SpanSugar._
+import leon.purescala.Types.Int32Type
+import leon.test.LeonTestSuiteWithProgram
+import leon.synthesis.SourceInfo
+import leon.synthesis.CostModels
+import leon.synthesis.graph.AndNode
+import leon.synthesis.SearchContext
+import leon.synthesis.Synthesizer
+import leon.synthesis.SynthesisSettings
+import leon.synthesis.RuleApplication
+import leon.synthesis.RuleClosed
+import leon.evaluators._
+import leon.LeonContext
+import leon.synthesis.rules.DetupleInput
+import leon.synthesis.Rules
+import leon.solvers.ModelBuilder
+import scala.language.implicitConversions
+import leon.LeonContext
+import leon.test.LeonTestSuiteWithProgram
+import leon.test.helpers.ExpressionsDSL
+import leon.synthesis.disambiguation.InputCoverage
+import leon.test.helpers.ExpressionsDSLProgram
+import leon.test.helpers.ExpressionsDSLVariables
+
+class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures with ExpressionsDSLProgram with ExpressionsDSLVariables {
+ val sources = List("""
+ |import leon.lang._
+ |import leon.collection._
+ |import leon.lang.synthesis._
+ |import leon.annotation._
+ |
+ |object InputCoverageSuite {
+ | def dummy = 2
+ | def withIf(cond: Boolean) = {
+ | if(cond) {
+ | 1
+ | } else {
+ | 2
+ | }
+ | }
+ | def withIfInIf(cond: Boolean) = {
+ | if(if(cond) false else true) {
+ | 1
+ | } else {
+ | 2
+ | }
+ | }
+ |
+ | def withCoveredFun1(input: Int) = {
+ | withCoveredFun2(input - 5) + withCoveredFun2(input + 5)
+ | }
+ |
+ | def withCoveredFun2(input: Int) = {
+ | if(input > 0) {
+ | 2
+ | } else {
+ | 0
+ | }
+ | }
+ |
+ | def withCoveredFun3(input: Int) = {
+ | withCoveredFun2(withCoveredFun2(input + 5))
+ | }
+ |}""".stripMargin)
+
+ test("wrapBranch should wrap expressions if they are not already containing wrapped calls"){ ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val dummy = funDef("InputCoverageSuite.dummy")
+ val coverage = new InputCoverage(dummy, Set(dummy))
+ val simpleExpr = Plus(IntLiteral(1), b)
+ coverage.wrapBranch((simpleExpr, Seq(p.id, q.id))) should equal ((simpleExpr, Seq(p.id, q.id)))
+ val (covered, ids) = coverage.wrapBranch((simpleExpr, Seq()))
+ ids should have size 1
+ covered should equal (Tuple(Seq(simpleExpr, Variable(ids.head))))
+ }
+
+ test("If-coverage should work"){ ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withIf = funDef("InputCoverageSuite.withIf")
+ val coverage = new InputCoverage(withIf, Set(withIf))
+ val expr = withIf.body.get
+
+ val (res, ids) = coverage.markBranches(expr)
+ ids should have size 2
+ expr match {
+ case IfExpr(cond, thenn, elze) =>
+ res should equal (IfExpr(cond, Tuple(Seq(thenn, Variable(ids(0)))), Tuple(Seq(elze, Variable(ids(1))))))
+ case _ => fail(s"$expr is not an IfExpr")
+ }
+ }
+
+ test("If-cond-coverage should work"){ ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withIfInIf = funDef("InputCoverageSuite.withIfInIf")
+ val coverage = new InputCoverage(withIfInIf, Set(withIfInIf))
+ val expr = withIfInIf.body.get
+
+ val (res, ids) = coverage.markBranches(expr)
+ ids should have size 4
+ expr match {
+ case IfExpr(IfExpr(cond, t1, e1), t2, e2) =>
+ res match {
+ case MatchExpr(IfExpr(c, t1, e1), Seq(MatchCase(TuplePattern(None, s), None, IfExpr(c2, t2, e2)))) if s.size == 2 =>
+ case _ => fail("should have a shape like (if() else ) match { case (a, b) => if(...) else }")
+ }
+ case _ => fail(s"$expr is not an IfExpr")
+ }
+ }
+
+ test("fundef combination-coverage should work"){ ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withCoveredFun1 = funDef("InputCoverageSuite.withCoveredFun1")
+ val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
+ val coverage = new InputCoverage(withCoveredFun1, Set(withCoveredFun1, withCoveredFun2))
+ val expr = withCoveredFun1.body.get
+
+ val (res, ids) = coverage.markBranches(expr)
+ ids should have size 2
+
+ res match {
+ case MatchExpr(funCall, Seq(
+ MatchCase(TuplePattern(None, Seq(WildcardPattern(Some(a1)), WildcardPattern(Some(b1)))), None,
+ MatchExpr(funCall2, Seq(
+ MatchCase(TuplePattern(None, Seq(WildcardPattern(Some(a2)), WildcardPattern(Some(b2)))), None,
+ Tuple(Seq(BVPlus(Variable(ida1), Variable(ida2)), Or(Seq(Variable(idb1), Variable(idb2)))))
+ )
+ ))))) =>
+ withClue(res.toString) {
+ ida1 shouldEqual a1
+ ida2 shouldEqual a2
+ Set(idb1.uniqueName, idb2.uniqueName) shouldEqual Set(b1.uniqueName, b2.uniqueName)
+ }
+ case _ =>
+ fail(s"$res is not of type funCall() match { case (a1, b1) => funCall() match { case (a2, b2) => (a1 + a2, b1 || b2) } }")
+ }
+ }
+
+ test("fundef composition-coverage should work"){ ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
+ val withCoveredFun3 = funDef("InputCoverageSuite.withCoveredFun3")
+ val coverage = new InputCoverage(withCoveredFun3, Set(withCoveredFun3, withCoveredFun2))
+ val expr = withCoveredFun3.body.get
+
+ val (res, ids) = coverage.markBranches(expr)
+ ids should have size 2
+ res match {
+ case MatchExpr(funCall, Seq(
+ MatchCase(TuplePattern(None, Seq(WildcardPattern(Some(a)), WildcardPattern(Some(b1)))), None,
+ MatchExpr(FunctionInvocation(_, Seq(Variable(ida))), Seq(
+ MatchCase(TuplePattern(None, Seq(WildcardPattern(_), WildcardPattern(Some(b2)))), None,
+ Tuple(Seq(p, Or(Seq(Variable(id1), Variable(id2)))))
+ )
+ ))))) if ida == a && id1 == b1 && id2 == b2 =>
+ case _ =>
+ fail(s"$res is not of type funCall() match { case (a, b1) => funCall(a) match { case (c, b2) => (c, b1 || b2) } }")
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
index 63469ead59c6c4441ce12a92fc92c4349ae99d5b..91b77284cc16518a4b86e0bdcb5ad7e98230061f 100644
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
@@ -9,6 +9,10 @@ import leon.purescala.Common._
import leon.purescala.Types._
import leon.purescala.Expressions._
+trait ExpressionsDSLVariables_a {
+ val a = FreshIdentifier("a", Int32Type).toVariable
+}
+
trait ExpressionsDSLVariables {
val F = BooleanLiteral(false)
val T = BooleanLiteral(true)
@@ -18,7 +22,6 @@ trait ExpressionsDSLVariables {
def i(x: Int) = IntLiteral(x)
def r(n: BigInt, d: BigInt) = FractionalLiteral(n, d)
- val a = FreshIdentifier("a", Int32Type).toVariable
val b = FreshIdentifier("b", Int32Type).toVariable
val c = FreshIdentifier("c", Int32Type).toVariable
@@ -97,7 +100,7 @@ self: Assertions =>
}
}
-trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram {
+trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram with ExpressionsDSLVariables_a {
self: Assertions =>
}