diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala
index 052abc20eba77b6dbe94bca787b40c72c113745c..edb08f59bd6378e0d1408347e5235970ac88017a 100644
--- a/src/main/scala/inox/ast/DSL.scala
+++ b/src/main/scala/inox/ast/DSL.scala
@@ -180,6 +180,9 @@ trait DSL {
body(vd1.toVariable, vd2.toVariable, vd3.toVariable, vd4.toVariable))
}
+ // Choose
+ def choose(res: ValDef)(pred: Variable => Expr) = Choose(res, pred(res.toVariable))
+
// Block-like
class BlockSuspension(susp: Expr => Expr) {
def in(e: Expr) = susp(e)
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 1f85f14f75f8a8da9d787f1c2852e8d51801c005..a17968b4196e692473cf41d269f80f3d18f31ab5 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -53,6 +53,7 @@ trait ExprOps extends GenTreeOps {
case Let(vd, _, _) => subvs - vd.toVariable
case Lambda(args, _) => subvs -- args.map(_.toVariable)
case Forall(args, _) => subvs -- args.map(_.toVariable)
+ case Choose(res, _) => subvs - res.toVariable
case _ => subvs
}
}(expr)
@@ -85,7 +86,7 @@ trait ExprOps extends GenTreeOps {
* unrolling solver. See implementation for what this means exactly.
*/
def isSimple(e: Expr): Boolean = !exists {
- case (_: Assume) | (_: Forall) | (_: Lambda) |
+ case (_: Assume) | (_: Forall) | (_: Lambda) | (_: Choose) |
(_: FunctionInvocation) | (_: Application) => true
case _ => false
} (e)
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 4aa8a174f2c7b9c6b0885b534fd07e71dffb2c99..2828e2cfe8ba50f1237f90af12ad325926c31e7f 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -115,12 +115,16 @@ trait Expressions { self: Trees =>
}
}
- /* Universal Quantification */
-
+ /** $encodingof `forall(...)` (universal quantification) */
case class Forall(args: Seq[ValDef], body: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type = body.getType
}
+ /** $encodingof `choose(...)` (returns a value satisfying the provided predicate) */
+ case class Choose(res: ValDef, pred: Expr) extends Expr {
+ def getType(implicit s: Symbols): Type = res.tpe
+ }
+
/* Control flow */
/** $encodingof `function(...)` (function invocation) */
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index e59547df2838296802ae3935f48ff4b6834f62e0..173e2d5d1c28ecd233b5120bbfe59b90bf345305 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -46,6 +46,8 @@ trait Extractors { self: Trees =>
Some((Seq(body), (es: Seq[Expr]) => Lambda(args, es.head)))
case Forall(args, body) =>
Some((Seq(body), (es: Seq[Expr]) => Forall(args, es.head)))
+ case Choose(res, pred) =>
+ Some((Seq(pred), (es: Seq[Expr]) => Choose(res, es.head)))
/* Binary operators */
case Equals(t1, t2) =>
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index de9b4326411821336c4609e89eb23da531e17f48..9e751eec0c3be889e73b3e0ab0d509e56c63e133 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -96,6 +96,9 @@ trait Printers { self: Trees =>
case Forall(args, e) =>
p"\u2200${nary(args)}. $e"
+ case Choose(res, pred) =>
+ p"choose(($res) => $pred)"
+
case e @ CaseClass(cct, args) =>
p"$cct($args)"
@@ -324,7 +327,7 @@ trait Printers { self: Trees =>
case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
case (_, None) => false
case (_, Some(
- _: Definition | _: Let | _: IfExpr | _ : CaseClass | _ : Lambda | _ : Tuple
+ _: Definition | _: Let | _: IfExpr | _: CaseClass | _: Lambda | _: Choose | _: Tuple
)) => false
case (ex: StringConcat, Some(_: StringConcat)) => false
case (_, Some(_: FunctionInvocation)) => false
diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index d2da99b30e5a610fccc736f18f1e23026c611cfc..2e5a44c4df6fbd49f532dea73cf6d62692741a85 100644
--- a/src/main/scala/inox/ast/TreeOps.scala
+++ b/src/main/scala/inox/ast/TreeOps.scala
@@ -82,6 +82,15 @@ trait TreeOps { self: Trees =>
e
}
+ case Choose(res, pred) =>
+ val newRes = transform(res)
+ val newPred = transform(pred)
+ if ((res ne newRes) || (pred ne newPred)) {
+ Choose(newRes, newPred).copiedFrom(e)
+ } else {
+ e
+ }
+
case Let(vd, expr, body) =>
val newVd = transform(vd)
val newExpr = transform(expr)
@@ -210,6 +219,10 @@ trait TreeOps { self: Trees =>
args foreach (vd => traverse(vd.tpe))
traverse(body)
+ case Choose(res, pred) =>
+ traverse(res.tpe)
+ traverse(pred)
+
case Let(a, expr, body) =>
traverse(expr)
traverse(body)
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 66d4d3e1ed0fa428997b7542fea67529a67f31c5..983bc3a49c9583c96595a225f234767fa3e7129c 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -500,6 +500,8 @@ trait RecursiveEvaluator
case f: Forall => onForallInvocation(f)
+ case c: Choose => onChooseInvocation(c)
+
case f @ FiniteMap(ss, dflt, vT) =>
// we use toMap.toSeq to reduce dupplicate keys
FiniteMap(ss.map{ case (k, v) => (e(k), e(v)) }.toMap.toSeq, e(dflt), vT)
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 6b84839cf1a19c9c109ac46aea88e77c1e1468e2..fd18f706003ee6df9ebab8149e99b7455736d2de 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -22,11 +22,10 @@ trait SolvingEvaluator extends Evaluator {
def getSolver(opts: InoxOption[Any]*): SolverFactory { val program: SolvingEvaluator.this.program.type }
- private val specCache: MutableMap[Expr, Expr] = MutableMap.empty
+ private val chooseCache: MutableMap[Choose, Expr] = MutableMap.empty
private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
- def onSpecInvocation(specs: Lambda): Expr = specCache.getOrElseUpdate(specs, {
- val Lambda(Seq(vd), body) = specs
+ def onChooseInvocation(choose: Choose): Expr = chooseCache.getOrElseUpdate(choose, {
val timer = ctx.timers.evaluators.specs.start()
val sf = getSolver(options.options.collect {
@@ -36,15 +35,15 @@ trait SolvingEvaluator extends Evaluator {
import SolverResponses._
val api = SimpleSolverAPI(sf)
- val res = api.solveSAT(body)
+ val res = api.solveSAT(choose.pred)
timer.stop()
res match {
case SatWithModel(model) =>
- valuateWithModel(model)(vd)
+ valuateWithModel(model)(choose.res)
case _ =>
- throw new RuntimeException("Failed to evaluate specs " + specs.asString)
+ throw new RuntimeException("Failed to evaluate choose " + choose.asString)
}
})
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 68041401851d74cb684ffd4603361bdf670c2690..68e2f8994ee2155e7c8e6d4c563be3dcc140bbc7 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -143,6 +143,14 @@ trait TemplateGenerator { self: Templates =>
storeGuarded(pathVar, e)
rec(pathVar, body, pol)
+ case c @ Choose(res, pred) =>
+ val newExpr = res.toVariable.freshen
+ storeExpr(newExpr)
+
+ val p = rec(pathVar, exprOps.replace(Map(res.toVariable -> newExpr), pred), Some(true))
+ storeGuarded(pathVar, p)
+ newExpr
+
case l @ Let(i, e: Lambda, b) =>
val re = rec(pathVar, e, None) // guaranteed variable!
val rb = rec(pathVar, exprOps.replace(Map(i.toVariable -> re), b), pol)