diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 1be21b20feda7d2fe9fd3af52378c23c32fd3c0b..edcc53db26b9b104071300d216f2a5983d065f3e 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -41,6 +41,17 @@ object Constructors {
*/
def tupleSelect(t: Expr, index: Int, originalSize: Int): Expr = tupleSelect(t, index, originalSize > 1)
+ /** $encodingof ``def foo(..) {} ...; e``.
+ * @see [[purescala.Expressions.LetDef]]
+ */
+ def letDef(defs: Seq[FunDef], e: Expr) = {
+ if (defs.isEmpty) {
+ e
+ } else {
+ LetDef(defs, e)
+ }
+ }
+
/** $encodingof ``val id = e; bd``, and returns `bd` if the identifier is not bound in `bd`.
* @see [[purescala.Expressions.Let]]
*/
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 27525657e8605ea828607951b2c29a56b1f0fc84..49d945ec6217a42578da7fef97bf572252cb6c26 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1148,6 +1148,15 @@ object ExprOps {
case _ => throw LeonFatalError("I can't choose simplest value for type " + tpe)
}
+ /* Checks if a given expression is 'real' and does not contain generic
+ * values. */
+ def isRealExpr(v: Expr): Boolean = {
+ !exists {
+ case gv: GenericValue => true
+ case _ => false
+ }(v)
+ }
+
def valuesOf(tp: TypeTree): Stream[Expr] = {
import utils.StreamUtils._
tp match {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 50efdf4065a005b234b696f0b2589c85855cc13f..bb70a6676923db89648df770318f8c04129bad3e 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -165,6 +165,7 @@ object Expressions {
* @param body The body of the expression after the function
*/
case class LetDef(fds: Seq[FunDef], body: Expr) extends Expr {
+ assert(fds.nonEmpty)
val getType = body.getType
}
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 84825d29a8ea2a293f04732fab06b2a88a36a4b8..db655365c24a7304831e818849238bba0a849de9 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -167,6 +167,11 @@ object TypeOps {
}
}
+ def isParametricType(tpe: TypeTree): Boolean = tpe match {
+ case (tp: TypeParameter) => true
+ case NAryType(tps, builder) => tps.exists(isParametricType)
+ }
+
// Helpers for instantiateType
private def typeParamSubst(map: Map[TypeParameter, TypeTree])(tpe: TypeTree): TypeTree = tpe match {
case (tp: TypeParameter) => map.getOrElse(tp, tp)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index ea52b9bab1c3e0d2b9be05df1cd2ec1c1f65c23f..dfe90d2f775e8ed3736020cb1e827c75fe602ad9 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -31,7 +31,7 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
}
def toExpr = {
- LetDef(defs.toList, guardedTerm)
+ letDef(defs.toList, guardedTerm)
}
// Projects a solution (ignore several output variables)
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 9bba63c87d50b3ca7f1adf7e445a8a0b54172b2f..d2cdb5b69f1f88b847ad91499e3946257ef6c167 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -5,7 +5,9 @@ package synthesis
package rules
import purescala.ExprOps._
+import purescala.TypeOps._
import purescala.Extractors._
+import purescala.Expressions._
import purescala.Constructors._
/** Moves the preconditions without output variables to the precondition. */
@@ -19,7 +21,13 @@ case object Assert extends NormalizingRule("Assert") {
if (exprsA.nonEmpty) {
// If there is no more postcondition, then output the solution.
if (others.isEmpty) {
- Some(solve(Solution(pre=andJoin(exprsA), defs=Set(), term=tupleWrap(p.xs.map(id => simplestValue(id.getType))))))
+ val simplestOut = simplestValue(tupleTypeWrap(p.xs.map(_.getType)))
+
+ if (!isRealExpr(simplestOut)) {
+ None
+ } else {
+ Some(solve(Solution(pre = andJoin(exprsA), defs = Set(), term = simplestOut)))
+ }
} else {
val sub = p.copy(pc = andJoin(p.pc +: exprsA), phi = andJoin(others), eb = p.qeb.filterIns(andJoin(exprsA)))
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 49663409fab1fb22dc102e35cfcfd3fb0ab5cdb4..d36cb15c0ff6f487d5d7b5e296fda0c406406886 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -19,8 +19,14 @@ case object Ground extends Rule("Ground") {
val result = solver.solveSAT(p.phi) match {
case (Some(true), model) =>
- val sol = Solution(BooleanLiteral(true), Set(), tupleWrap(p.xs.map(valuateWithModel(model))))
- RuleClosed(sol)
+ val solExpr = tupleWrap(p.xs.map(valuateWithModel(model)))
+
+ if (!isRealExpr(solExpr)) {
+ RuleFailed()
+ } else {
+ val sol = Solution(BooleanLiteral(true), Set(), solExpr)
+ RuleClosed(sol)
+ }
case (Some(false), model) =>
RuleClosed(Solution.UNSAT(p))
case _ =>
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 6085ef9eb2067fa092ffacfdefbf27532b02b5d9..679e49e38fb25ce3c4f79a26e1078651eccb69a5 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -36,7 +36,6 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
//println("SOLVING " + phi + " ...")
solver.solveSAT(phi) match {
case (Some(true), satModel) =>
-
val newNotPhi = valuateWithModelIn(notPhi, xss, satModel)
//println("REFUTING " + Not(newNotPhi) + "...")
@@ -46,8 +45,15 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
case (Some(false), _) =>
- result = Some(RuleClosed(Solution(BooleanLiteral(true), Set(), tupleWrap(p.xs.map(valuateWithModel(satModel))))))
-
+ // Model apprears valid, but it might be a fake expression (generic values)
+ val outExpr = tupleWrap(p.xs.map(valuateWithModel(satModel)))
+
+ if (!isRealExpr(outExpr)) {
+ // It does contain a generic value, we skip
+ predicates = valuateWithModelIn(phi, xss, satModel) +: predicates
+ } else {
+ result = Some(RuleClosed(Solution(BooleanLiteral(true), Set(), outExpr)))
+ }
case _ =>
continue = false
result = None
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index f753d3884e71e4ba76c84b72985f6401c0666256..eb3d83ed8d13b8235a98b48d4c209a2db5a7f08c 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -7,10 +7,13 @@ package rules
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Constructors._
+import purescala.TypeOps._
case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val unconstr = p.xs.toSet -- variablesOf(p.phi)
+ val unconstr = (p.xs.toSet -- variablesOf(p.phi)).filter { x =>
+ isRealExpr(simplestValue(x.getType))
+ }
if (unconstr.nonEmpty) {
val sub = p.copy(xs = p.xs.filterNot(unconstr), eb = p.qeb.removeOuts(unconstr))
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 677c9b852aafeadcfc96bd63f2b98aaaaf289940..4570501d7646b3f8d77d4fb484451ff957ac723f 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -5,10 +5,13 @@ package synthesis
package rules
import purescala.ExprOps._
+import purescala.TypeOps._
case object UnusedInput extends NormalizingRule("UnusedInput") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc) -- variablesOf(p.ws)
+ val unused = (p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc) -- variablesOf(p.ws)).filter { a =>
+ !isParametricType(a.getType)
+ }
if (unused.nonEmpty) {
val sub = p.copy(as = p.as.filterNot(unused), eb = p.qeb.removeIns(unused))