diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 7da928faf68b71bdb48068e77f3f3c42018d678a..02510c7c8b10f26b3924c49d9a1f5d1715c9009f 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -724,14 +724,14 @@ object ExprOps extends GenTreeOps[Expr] {
case None => patCond
}
val newRhs = replaceFromIDs(map, cse.rhs)
- (realCond.toClause, newRhs)
+ (realCond.toClause, newRhs, cse)
}
val bigIte = condsAndRhs.foldRight[Expr](Error(m.getType, "Match is non-exhaustive").copiedFrom(m))((p1, ex) => {
if(p1._1 == BooleanLiteral(true)) {
p1._2
} else {
- IfExpr(p1._1, p1._2, ex)
+ IfExpr(p1._1, p1._2, ex).copiedFrom(p1._3)
}
})
diff --git a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
index cdf471836beed54ce17d82504e576d96286cb8a8..b46d2e3a517a341e59129e511fefdbaa457781ae 100644
--- a/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/InputCoverage.scala
@@ -98,13 +98,30 @@ class InputCoverage(fd: FunDef, fds: Set[FunDef])(implicit c: LeonContext, p: Pr
val arg_b = FreshIdentifier("bc", BooleanType)
(letTuple(Seq(arg_id, arg_b), c1, IfExpr(Variable(arg_id), t1, e1).copiedFrom(e)).copiedFrom(e), merge(merge(cv1, tv1), ev1))
}
- case MatchExpr(scrut, cases) =>
- val (c1, cv1) = markBranches(scrut)
- val (new_cases, variables) = (cases map { case m@MatchCase(pattern, opt, rhs) =>
- val (rhs_new, ids) = wrapBranch(markBranches(rhs))
- (MatchCase(pattern, opt, rhs_new).copiedFrom(m), ids)
- }).unzip // TODO: Check for unapply with function pattern ?
- (MatchExpr(c1, new_cases).copiedFrom(e), variables.fold(None)(merge))
+ case m@MatchExpr(scrut, cases) =>
+ val (c, ids) = markBranches(ExprOps.matchToIfThenElse(m)) // And replace the last error else statement with a dummy flag.
+ def replaceFinalElse(e: Expr): (Expr, Identifier)= e match {
+ case IfExpr(c1, t1, e1) =>
+ val (newElse, id) = replaceFinalElse(e1)
+ (IfExpr(c1, t1, newElse).copiedFrom(e), id)
+ case Tuple(Seq(Error(tpe, msg), Variable(i))) =>
+ (Tuple(Seq(Error(tpe, msg), BooleanLiteral(false))), i)
+ }
+ val (new_c, id_to_remove) = replaceFinalElse(c)
+ (new_c, ids.map(_.filter(_ != id_to_remove)))
+ case Or(args) if args.length >= 1 =>
+ val c = args.foldRight[Expr](BooleanLiteral(false).copiedFrom(e)){
+ case (arg, prev) =>
+ IfExpr(arg, BooleanLiteral(true), prev).copiedFrom(e)
+ }
+ markBranches(c.copiedFrom(e))
+ case And(args) if args.length >= 1 =>
+ val c = args.foldRight[Expr](BooleanLiteral(true).copiedFrom(e)){
+ case (arg, prev) =>
+ IfExpr(Not(arg), BooleanLiteral(false), prev).copiedFrom(e)
+ }
+ markBranches(c.copiedFrom(e))
+
case Operator(lhsrhs, builder) =>
// The exprBuilder adds variable definitions needed to compute the arguments.
val (exprBuilder, children, tmpIds, ids) = (((e: Expr) => e, ListBuffer[Expr](), ListBuffer[Identifier](), None: Option[Seq[Identifier]]) /: lhsrhs) {
diff --git a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
index 3c0376039ce33972deac9e3210d81757c6c6126e..57c7e20a804562c3a6771cc6c835f18aff28102a 100644
--- a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
+++ b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
@@ -106,6 +106,21 @@ class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with Sca
| def withCoveredFun3(input: Int) = {
| withCoveredFun2(withCoveredFun2(input + 5))
| }
+ |
+ | def coveredCond(a: Boolean, b: Boolean, c: Boolean, d: Boolean) = {
+ | if(a || b) {
+ | if(c && d) {
+ | 1
+ | } else if(c) {
+ | 2
+ | } else {
+ | 3
+ | }
+ | } else if(!a && c) {
+ | 4
+ | } else 5
+ | }
+ |
|}""".stripMargin)
test("wrapBranch should wrap expressions if they are not already containing wrapped calls"){ ctxprogram =>
@@ -174,25 +189,6 @@ class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with Sca
case (res, Some(ids)) =>
withClue(res.toString) {
ids should have size 4
- res match {
- case MatchExpr(scrut,
- Seq(
- MatchCase(CaseClassPattern(_, _, Seq()), None, rhs1),
- MatchCase(CaseClassPattern(_, _, _), None, rhs2),
- MatchCase(CaseClassPattern(_, _, _), None, rhs3),
- MatchCase(CaseClassPattern(_, _, _), None, rhs4))
- ) =>
- rhs1 match {
- case Tuple(Seq(_, Variable(b))) => b shouldEqual ids(0)
- case _ => fail(s"$rhs1 should be a Tuple")
- }
- rhs2 match {
- case LetTuple(_, _, Tuple(Seq(_, Or(Seq(_, Variable(b)))))) => b shouldEqual ids(1)
- case _ => fail(s"$rhs2 should be a val + tuple like val ... = ... ; (..., ... || ${ids(1)})")
- }
-
- case _ => fail(s"$res does not have the format a match { case B() => .... x 4 }")
- }
}
}
}
@@ -210,22 +206,6 @@ class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with Sca
fail(s"Should have not added any ids, but got $ids")
}
case (res, _) =>
- 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.uniqueName shouldEqual a2.uniqueName
- ida2.uniqueName shouldEqual a1.uniqueName
- 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) } }")
- }
}
}
@@ -239,17 +219,6 @@ class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with Sca
coverage.markBranches(expr) match {
case (res, None) => fail("No ids added")
case (res, Some(ids)) =>
- 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) } }")
- }
}
}
@@ -273,6 +242,15 @@ class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with Sca
res2 should have size 3
}
+ test("input coverage for boolean, disjunctions and conjunctions should find all of them") { ctxprogram =>
+ implicit val (c, p) = ctxprogram
+ val coveredCond = funDef("InputCoverageSuite.coveredCond")
+ val coverage = new InputCoverage(coveredCond, Set(coveredCond))
+ coverage.minimizeExamples = true
+ val res2 = coverage.result().toSet
+ res2 should have size 5
+ }
+
test("input coverage for combined functions should find all of them") { ctxprogram =>
implicit val (c, p) = ctxprogram
val withCoveredFun1 = funDef("InputCoverageSuite.withCoveredFun1")