From 3932b6e517c16ab083d4291e86177c4fdf1ce7e3 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sun, 6 Nov 2016 16:05:21 +0100
Subject: [PATCH] Guaranteed finite bags and sets
---
build.sbt | 7 +-
src/main/scala/inox/ast/DSL.scala | 1 +
.../scala/inox/solvers/SolverFactory.scala | 56 +++++++-
.../inox/solvers/theories/BagEncoder.scala | 45 ++++--
.../scala/inox/solvers/theories/package.scala | 17 +++
.../solvers/unrolling/DatatypeTemplates.scala | 131 +++++++++++++-----
src/test/scala/inox/TestContext.scala | 13 ++
.../scala/inox/TestSilentReporter.scala | 0
.../inox/solvers/GlobalVariablesSuite.scala | 39 ++++++
.../scala/inox/solvers/SolverPoolSuite.scala | 2 +-
.../scala/inox/solvers/SolversSuite.scala | 79 +++++++++++
.../inox/solvers/TimeoutSolverSuite.scala | 60 ++++++++
12 files changed, 399 insertions(+), 51 deletions(-)
create mode 100644 src/test/scala/inox/TestContext.scala
rename src/{it => test}/scala/inox/TestSilentReporter.scala (100%)
create mode 100644 src/test/scala/inox/solvers/GlobalVariablesSuite.scala
create mode 100644 src/test/scala/inox/solvers/SolversSuite.scala
create mode 100644 src/test/scala/inox/solvers/TimeoutSolverSuite.scala
diff --git a/build.sbt b/build.sbt
index f95639cec..4486befa0 100644
--- a/build.sbt
+++ b/build.sbt
@@ -47,7 +47,10 @@ Keys.fork in run := true
testOptions in Test := Seq(Tests.Argument("-oDF"))
-testOptions in IntegrationTest := Seq(Tests.Argument("-oDF"))
+// Note that we can't use IntegrationTest because it is already defined in sbt._
+lazy val ItTest = config("it") extend(Test)
+
+testOptions in ItTest := Seq(Tests.Argument("-oDF"))
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
@@ -57,7 +60,7 @@ lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "567e
lazy val root = (project in file("."))
.configs(IntegrationTest)
.settings(Defaults.itSettings : _*)
- .settings(inConfig(IntegrationTest)(Defaults.testTasks ++ Seq(
+ .settings(inConfig(ItTest)(Defaults.testTasks ++ Seq(
logBuffered := false,
parallelExecution := false
)) : _*)
diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala
index f8de46db2..1981602bc 100644
--- a/src/main/scala/inox/ast/DSL.scala
+++ b/src/main/scala/inox/ast/DSL.scala
@@ -57,6 +57,7 @@ trait DSL {
def ++ = SetUnion(e, _: Expr)
def -- = SetDifference(e, _: Expr)
def & = SetIntersection(e, _: Expr)
+ def contains = ElementOfSet(_: Expr, e)
// Misc.
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 8f6610dca..a98f7776d 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -24,6 +24,33 @@ trait SolverFactory {
}
object SolverFactory {
+
+ lazy val hasNativeZ3 = try {
+ _root_.z3.Z3Wrapper.withinJar()
+ true
+ } catch {
+ case _: java.lang.UnsatisfiedLinkError =>
+ false
+ }
+
+ import _root_.smtlib.interpreters._
+
+ lazy val hasZ3 = try {
+ new Z3Interpreter("z3", Array("-in", "-smt2"))
+ true
+ } catch {
+ case _: java.io.IOException =>
+ false
+ }
+
+ lazy val hasCVC4 = try {
+ new CVC4Interpreter("cvc4", Array("-q", "--lang", "smt2.5"))
+ true
+ } catch {
+ case _: java.io.IOException =>
+ false
+ }
+
def create[S1 <: Solver](p: Program)(nme: String, builder: () => S1 { val program: p.type }):
SolverFactory { val program: p.type; type S = S1 { val program: p.type } } = {
new SolverFactory {
@@ -115,10 +142,37 @@ object SolverFactory {
val solvers: Set[String] = solverNames.map(_._1).toSet
+ private var reported: Boolean = false
+
def apply(name: String, p: InoxProgram, opts: Options): SolverFactory {
val program: p.type
type S <: TimeoutSolver { val program: p.type }
- } = getFromName(name)(p, opts)(RecursiveEvaluator(p, opts), ast.ProgramEncoder.empty(p))
+ } = {
+ val fallbacks = Map(
+ "nativez3" -> (() => hasNativeZ3, Seq("smt-z3", "smt-cvc4"), "Z3 native interface"),
+ "unrollz3" -> (() => hasNativeZ3, Seq("smt-z3", "smt-cvc4"), "Z3 native interface"),
+ "smt-z3" -> (() => hasZ3, Seq("nativez3", "smt-cvc4"), "'z3' binary"),
+ "smt-cvc4" -> (() => hasCVC4, Seq("nativez3", "smt-z3"), "'cvc4' binary")
+ )
+
+ fallbacks.get(name) match {
+ case Some((guard, names, requirement)) if !guard() =>
+ names.collectFirst { case name if fallbacks(name)._1() => name } match {
+ case Some(name) =>
+ if (!reported) {
+ p.ctx.reporter.warning(s"The $requirement is not available. Falling back onto $name.")
+ reported = true
+ }
+ apply(name, p, opts)
+
+ case None =>
+ p.ctx.reporter.fatalError("No SMT solver available: " +
+ "native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
+ }
+ case _ =>
+ getFromName(name)(p, opts)(RecursiveEvaluator(p, opts), ast.ProgramEncoder.empty(p))
+ }
+ }
def apply(p: InoxProgram, opts: Options): SolverFactory {
val program: p.type
diff --git a/src/main/scala/inox/solvers/theories/BagEncoder.scala b/src/main/scala/inox/solvers/theories/BagEncoder.scala
index c7badaee2..f984320e9 100644
--- a/src/main/scala/inox/solvers/theories/BagEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/BagEncoder.scala
@@ -8,11 +8,16 @@ trait BagEncoder extends TheoryEncoder {
import trees._
import trees.dsl._
+ val evaluator: evaluators.DeterministicEvaluator {
+ val program: sourceProgram.type
+ }
+
val BagID = FreshIdentifier("Bag")
+ val keys = FreshIdentifier("keys")
val f = FreshIdentifier("f")
val bagADT = mkConstructor(BagID)("T")(None) {
- case Seq(aT) => Seq(ValDef(f, aT =>: IntegerType))
+ case Seq(aT) => Seq(ValDef(keys, SetType(aT)), ValDef(f, aT =>: IntegerType))
}
val Bag = T(BagID)
@@ -20,13 +25,20 @@ trait BagEncoder extends TheoryEncoder {
val GetID = FreshIdentifier("get")
val Get = mkFunDef(GetID)("T") { case Seq(aT) => (
Seq("bag" :: Bag(aT), "x" :: aT),
- IntegerType, { case Seq(bag, x) => bag.getField(f)(x) })
+ IntegerType, { case Seq(bag, x) =>
+ if_ (bag.getField(keys) contains x) {
+ bag.getField(f)(x)
+ } else_ {
+ E(BigInt(0))
+ }
+ })
}
val AddID = FreshIdentifier("add")
val Add = mkFunDef(AddID)("T") { case Seq(aT) => (
Seq("bag" :: Bag(aT), "x" :: aT),
Bag(aT), { case Seq(bag, x) => Bag(aT)(
+ bag.getField(keys) insert x,
\("y" :: aT)(y => bag.getField(f)(y) + {
if_ (y === x) { E(BigInt(1)) } else_ { E(BigInt(0)) }
}))
@@ -37,6 +49,7 @@ trait BagEncoder extends TheoryEncoder {
val Union = mkFunDef(UnionID)("T") { case Seq(aT) => (
Seq("b1" :: Bag(aT), "b2" :: Bag(aT)),
Bag(aT), { case Seq(b1, b2) => Bag(aT)(
+ b1.getField(keys) ++ b2.getField(keys),
\("y" :: aT)(y => b1.getField(f)(y) + b2.getField(f)(y)))
})
}
@@ -45,6 +58,7 @@ trait BagEncoder extends TheoryEncoder {
val Difference = mkFunDef(DifferenceID)("T") { case Seq(aT) => (
Seq("b1" :: Bag(aT), "b2" :: Bag(aT)),
Bag(aT), { case Seq(b1, b2) => Bag(aT)(
+ b1.getField(keys),
\("y" :: aT)(y => let("res" :: IntegerType, b1.getField(f)(y) - b2.getField(f)(y)) {
res => if_ (res < E(BigInt(0))) { E(BigInt(0)) } else_ { res }
}))
@@ -55,6 +69,7 @@ trait BagEncoder extends TheoryEncoder {
val Intersect = mkFunDef(IntersectID)("T") { case Seq(aT) => (
Seq("b1" :: Bag(aT), "b2" :: Bag(aT)),
Bag(aT), { case Seq(b1, b2) => Bag(aT)(
+ b1.getField(keys) & b2.getField(keys),
\("y" :: aT)(y => let("r1" :: IntegerType, b1.getField(f)(y)) { r1 =>
let("r2" :: IntegerType, b2.getField(f)(y)) { r2 =>
if_ (r1 > r2) { r2 } else_ { r1 }
@@ -80,9 +95,12 @@ trait BagEncoder extends TheoryEncoder {
override def transform(e: Expr): Expr = e match {
case FiniteBag(elems, tpe) =>
val newTpe = transform(tpe)
- Bag(newTpe)(\("x" :: newTpe)(x => elems.foldRight[Expr](IntegerLiteral(0).copiedFrom(e)) {
- case ((k, v), ite) => IfExpr(x === transform(k), transform(v), ite).copiedFrom(e)
- })).copiedFrom(e)
+ Bag(newTpe)(
+ FiniteSet(elems.map(_._1), newTpe),
+ \("x" :: newTpe)(x => elems.foldRight[Expr](IntegerLiteral(0).copiedFrom(e)) {
+ case ((k, v), ite) => IfExpr(x === transform(k), transform(v), ite).copiedFrom(e)
+ })
+ ).copiedFrom(e)
case BagAdd(bag, elem) =>
val BagType(base) = bag.getType
@@ -121,15 +139,14 @@ trait BagEncoder extends TheoryEncoder {
import targetProgram._
override def transform(e: Expr): Expr = e match {
- case cc @ ADT(ADTType(BagID, Seq(tpe)), Seq(Lambda(Seq(vd), body))) =>
- val Variable = vd.toVariable
- def rec(expr: Expr): Seq[(Expr, Expr)] = expr match {
- case IfExpr(Equals(Variable, k), v, elze) => rec(elze) :+ (transform(k) -> transform(v))
- case IntegerLiteral(v) if v == 0 => Seq.empty
- case _ => throw new Unsupported(expr, "Bags can't have default value " + expr.asString)
- }
-
- FiniteBag(rec(body), transform(tpe)).copiedFrom(e)
+ case cc @ ADT(ADTType(BagID, Seq(tpe)), Seq(FiniteSet(elems, _), l @ Lambda(Seq(_), _))) =>
+ val tl = transform(l)
+ FiniteBag(elems.map { e =>
+ val te = transform(e)
+ te -> evaluator.eval(Application(tl, Seq(te))).result.getOrElse {
+ throw new Unsupported(e, "Unexpectedly failed to evaluate bag lambda")
+ }.copiedFrom(e)
+ }, transform(tpe)).copiedFrom(e)
case cc @ ADT(ADTType(BagID, Seq(tpe)), args) =>
throw new Unsupported(e, "Unexpected argument to bag constructor")
diff --git a/src/main/scala/inox/solvers/theories/package.scala b/src/main/scala/inox/solvers/theories/package.scala
index 617dde8e0..8eddcfd85 100644
--- a/src/main/scala/inox/solvers/theories/package.scala
+++ b/src/main/scala/inox/solvers/theories/package.scala
@@ -14,6 +14,23 @@ package object theories {
trait CVC4Theories { self: unrolling.AbstractUnrollingSolver =>
object theories extends {
val sourceProgram: self.encoder.targetProgram.type = self.encoder.targetProgram
+ val evaluator: evaluators.DeterministicEvaluator { val program: self.encoder.targetProgram.type } = new {
+ val program: self.encoder.targetProgram.type = self.encoder.targetProgram
+ val options = self.options
+ } with evaluators.DeterministicEvaluator {
+ import program.trees._
+ import evaluators.EvaluationResults._
+
+ def eval(e: Expr, model: Map[ValDef, Expr]): EvaluationResult = {
+ self.evaluator.eval(self.encoder.decode(e), model.map {
+ case (vd, value) => self.encoder.decode(vd) -> self.encoder.decode(value)
+ }) match {
+ case Successful(value) => Successful(self.encoder.encode(value))
+ case RuntimeError(message) => RuntimeError(message)
+ case EvaluatorError(message) => EvaluatorError(message)
+ }
+ }
+ }
} with BagEncoder
}
}
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index 49114239e..c2ba6409a 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -29,10 +29,22 @@ trait DatatypeTemplates { self: Templates =>
type Functions = Set[(Encoded, FunctionType, Encoded)]
+ sealed abstract class TypeInfo {
+ def getType: Type = this match {
+ case SortInfo(tsort) => tsort.toType
+ case SetInfo(base) => SetType(base)
+ case BagInfo(base) => BagType(base)
+ }
+ }
+
+ case class SortInfo(tsort: TypedADTSort) extends TypeInfo
+ case class SetInfo(base: Type) extends TypeInfo
+ case class BagInfo(base: Type) extends TypeInfo
+
/** Represents a type unfolding of a free variable (or input) in the unfolding procedure */
- case class TemplateTypeInfo(tsort: TypedADTSort, arg: Encoded, outer: Option[(Encoded, FunctionType)]) {
+ case class TemplateTypeInfo(info: TypeInfo, arg: Encoded, outer: Option[(Encoded, FunctionType)]) {
override def toString: String =
- tsort.toType.asString + "(" + asString(arg) + ")" + (outer match {
+ info + "(" + asString(arg) + ")" + (outer match {
case Some((f, tpe)) => " in " + asString(f)
case None => ""
})
@@ -101,7 +113,7 @@ trait DatatypeTemplates { self: Templates =>
case BooleanType | UnitType | CharType | IntegerType |
RealType | StringType | (_: BVType) | (_: TypeParameter) => false
- case ft: FunctionType => true
+ case (_: FunctionType) | (_: BagType) | (_: SetType) => true
case NAryType(tpes, _) => tpes.exists(unroll)
})
@@ -125,6 +137,11 @@ trait DatatypeTemplates { self: Templates =>
val pathVar = Variable(FreshIdentifier("b", true), BooleanType)
val (idT, pathVarT) = (encodeSymbol(v), encodeSymbol(pathVar))
+ private var exprVars = Map[Variable, Encoded]()
+ @inline protected def storeExpr(v: Variable): Unit = {
+ exprVars += v -> encodeSymbol(v)
+ }
+
private var condVars = Map[Variable, Encoded]()
private var condTree = Map[Variable, Set[Variable]](pathVar -> Set.empty).withDefaultValue(Set.empty)
@inline protected def storeCond(pathVar: Variable, v: Variable): Unit = {
@@ -141,9 +158,9 @@ trait DatatypeTemplates { self: Templates =>
private var equations = Seq[Expr]()
@inline protected def iff(e1: Expr, e2: Expr): Unit = equations :+= Equals(e1, e2)
- private var tpes = Map[Variable, Set[(TypedADTSort, Expr)]]()
- @inline protected def storeType(pathVar: Variable, tsort: TypedADTSort, arg: Expr): Unit = {
- tpes += pathVar -> (tpes.getOrElse(pathVar, Set.empty) + (tsort -> arg))
+ private var tpes = Map[Variable, Set[(TypeInfo, Expr)]]()
+ @inline protected def storeType(pathVar: Variable, info: TypeInfo, arg: Expr): Unit = {
+ tpes += pathVar -> (tpes.getOrElse(pathVar, Set.empty) + (info -> arg))
}
private var functions = Map[Variable, Set[Expr]]()
@@ -151,17 +168,23 @@ trait DatatypeTemplates { self: Templates =>
functions += pathVar -> (functions.getOrElse(pathVar, Set.empty) + expr)
}
+ protected case class RecursionState(
+ recurseSort: Boolean, // visit sort children
+ recurseSet: Boolean, // unroll set definition
+ recurseBag: Boolean // unroll bag definition
+ )
+
/** Generates the clauses and other bookkeeping relevant to a type unfolding template.
* Subtypes of [[Builder]] can override this method to change clause generation. */
- protected def rec(pathVar: Variable, expr: Expr, recurse: Boolean): Unit = expr.getType match {
+ protected def rec(pathVar: Variable, expr: Expr, state: RecursionState): Unit = expr.getType match {
case tpe if !unroll(tpe) =>
// nothing to do here!
case adt: ADTType =>
val tadt = adt.getADT
- if (tadt.definition.isSort && tadt.toSort.definition.isInductive && !recurse) {
- storeType(pathVar, tadt.toSort, expr)
+ if (tadt.definition.isSort && tadt.toSort.definition.isInductive && !state.recurseSort) {
+ storeType(pathVar, SortInfo(tadt.toSort), expr)
} else {
val matchers = tadt.root match {
case (tsort: TypedADTSort) => tsort.constructors
@@ -176,7 +199,7 @@ trait DatatypeTemplates { self: Templates =>
storeCond(pathVar, newBool)
for (vd <- tcons.fields) {
- rec(newBool, ADTSelector(AsInstanceOf(expr, tpe), vd.id), false)
+ rec(newBool, ADTSelector(AsInstanceOf(expr, tpe), vd.id), state.copy(recurseSort = false))
}
val vars = tpes.keys.toSet ++ functions.keys ++
@@ -192,21 +215,61 @@ trait DatatypeTemplates { self: Templates =>
case TupleType(tpes) =>
for ((_, idx) <- tpes.zipWithIndex) {
- rec(pathVar, TupleSelect(expr, idx + 1), recurse)
+ rec(pathVar, TupleSelect(expr, idx + 1), state)
}
case FunctionType(_, _) =>
storeFunction(pathVar, expr)
- case _ => scala.sys.error("TODO")
+ case SetType(base) =>
+ val newBool: Variable = Variable(FreshIdentifier("b", true), BooleanType)
+ storeCond(pathVar, newBool)
+
+ iff(and(pathVar, Not(Equals(expr, FiniteSet(Seq.empty, base)))), newBool)
+
+ if (!state.recurseSet) {
+ storeType(newBool, SetInfo(base), expr)
+ } else {
+ val elemExpr: Variable = Variable(FreshIdentifier("elem", true), base)
+ val restExpr: Variable = Variable(FreshIdentifier("rest", true), SetType(base))
+ storeExpr(elemExpr)
+ storeExpr(restExpr)
+
+ storeGuarded(newBool, Equals(expr, SetUnion(FiniteSet(Seq(elemExpr), base), restExpr)))
+ rec(newBool, restExpr, state.copy(recurseSet = false))
+ rec(newBool, elemExpr, state)
+ }
+
+ case BagType(base) =>
+ val newBool: Variable = Variable(FreshIdentifier("b", true), BooleanType)
+ storeCond(pathVar, newBool)
+
+ iff(and(pathVar, Not(Equals(expr, FiniteBag(Seq.empty, base)))), newBool)
+
+ if (!state.recurseBag) {
+ storeType(pathVar, BagInfo(base), expr)
+ } else {
+ val elemExpr: Variable = Variable(FreshIdentifier("elem", true), base)
+ val multExpr: Variable = Variable(FreshIdentifier("mult", true), IntegerType)
+ val restExpr: Variable = Variable(FreshIdentifier("rest", true), BagType(base))
+ storeExpr(elemExpr)
+ storeExpr(multExpr)
+ storeExpr(restExpr)
+
+ storeGuarded(newBool, Equals(expr, BagUnion(FiniteBag(Seq(elemExpr -> multExpr), base), restExpr)))
+ rec(newBool, restExpr, state.copy(recurseBag = false))
+ rec(newBool, elemExpr, state)
+ }
+
+ case _ => throw FatalError("Unexpected unrollable")
}
/* Calls [[rec]] and finalizes the bookkeeping collection before returning everything
* necessary to a template creation. */
- lazy val (encoder, conds, tree, clauses, calls, types, funs) = {
- rec(pathVar, v, true)
+ lazy val (encoder, exprs, conds, tree, clauses, calls, types, funs) = {
+ rec(pathVar, v, RecursionState(true, true, true))
- val encoder: Expr => Encoded = mkEncoder(condVars + (v -> idT) + (pathVar -> pathVarT))
+ val encoder: Expr => Encoded = mkEncoder(exprVars ++ condVars + (v -> idT) + (pathVar -> pathVarT))
var clauses: Clauses = Seq.empty
var calls: CallBlockers = Map.empty
@@ -227,8 +290,8 @@ trait DatatypeTemplates { self: Templates =>
clauses ++= equations.map(encoder)
- val encodedTypes: Map[Encoded, Set[(TypedADTSort, Encoded)]] = tpes.map { case (b, tps) =>
- encoder(b) -> tps.map { case (tadt, expr) => (tadt, encoder(expr)) }
+ val encodedTypes: Map[Encoded, Set[(TypeInfo, Encoded)]] = tpes.map { case (b, tps) =>
+ encoder(b) -> tps.map { case (info, expr) => (info, encoder(expr)) }
}
val encodedFunctions: Functions = functions.flatMap { case (b, fs) =>
@@ -236,7 +299,7 @@ trait DatatypeTemplates { self: Templates =>
fs.map(expr => (bp, bestRealType(expr.getType).asInstanceOf[FunctionType], encoder(expr)))
}.toSet
- (encoder, condVars, condTree, clauses, calls, encodedTypes, encodedFunctions)
+ (encoder, exprVars, condVars, condTree, clauses, calls, encodedTypes, encodedFunctions)
}
}
}
@@ -245,7 +308,6 @@ trait DatatypeTemplates { self: Templates =>
trait TypesTemplate extends Template {
val types: Map[Encoded, Set[TemplateTypeInfo]]
- val exprVars = Map.empty[Variable, Encoded]
val applications = Map.empty[Encoded, Set[App]]
val lambdas = Seq.empty[LambdaTemplate]
val matchers = Map.empty[Encoded, Set[Matcher]]
@@ -276,6 +338,7 @@ trait DatatypeTemplates { self: Templates =>
class DatatypeTemplate private[DatatypeTemplates] (
val pathVar: (Variable, Encoded),
val argument: Encoded,
+ val exprVars: Map[Variable, Encoded],
val condVars: Map[Variable, Encoded],
val condTree: Map[Variable, Set[Variable]],
val clauses: Clauses,
@@ -323,7 +386,7 @@ trait DatatypeTemplates { self: Templates =>
/** Clause generation is specialized to handle ADT constructor types that require
* type guards as well as ADT invariants. */
protected class Builder(tpe: Type) extends super.Builder(tpe) {
- override protected def rec(pathVar: Variable, expr: Expr, recurse: Boolean): Unit = expr.getType match {
+ override protected def rec(pathVar: Variable, expr: Expr, state: RecursionState): Unit = expr.getType match {
case adt: ADTType =>
val tadt = adt.getADT
@@ -336,24 +399,24 @@ trait DatatypeTemplates { self: Templates =>
val tpe = tadt.toType
for (vd <- tadt.toConstructor.fields) {
- rec(pathVar, ADTSelector(AsInstanceOf(expr, tpe), vd.id), false)
+ rec(pathVar, ADTSelector(AsInstanceOf(expr, tpe), vd.id), state.copy(recurseSort = false))
}
} else {
- super.rec(pathVar, expr, recurse)
+ super.rec(pathVar, expr, state)
}
- case _ => super.rec(pathVar, expr, recurse)
+ case _ => super.rec(pathVar, expr, state)
}
}
def apply(tpe: Type): DatatypeTemplate = cache.getOrElseUpdate(tpe, {
val b = new Builder(tpe)
val typeBlockers: TypeBlockers = b.types.map { case (blocker, tps) =>
- blocker -> tps.map { case (tadt, arg) => TemplateTypeInfo(tadt, arg, None) }
+ blocker -> tps.map { case (info, arg) => TemplateTypeInfo(info, arg, None) }
}
new DatatypeTemplate(b.pathVar -> b.pathVarT, b.idT,
- b.conds, b.tree, b.clauses, b.calls, typeBlockers, b.funs)
+ b.exprs, b.conds, b.tree, b.clauses, b.calls, typeBlockers, b.funs)
})
}
@@ -362,6 +425,7 @@ trait DatatypeTemplates { self: Templates =>
val pathVar: (Variable, Encoded),
val container: Encoded,
val argument: Encoded,
+ val exprVars: Map[Variable, Encoded],
val condVars: Map[Variable, Encoded],
val condTree: Map[Variable, Set[Variable]],
val clauses: Clauses,
@@ -393,9 +457,10 @@ trait DatatypeTemplates { self: Templates =>
(Variable, Encoded),
Encoded,
Map[Variable, Encoded],
+ Map[Variable, Encoded],
Map[Variable, Set[Variable]],
Clauses,
- Map[Encoded, Set[(TypedADTSort, Encoded)]],
+ Map[Encoded, Set[(TypeInfo, Encoded)]],
Functions
)] = MutableMap.empty
@@ -420,10 +485,10 @@ trait DatatypeTemplates { self: Templates =>
})
def apply(tpe: Type, containerType: FunctionType): CaptureTemplate = cache.getOrElseUpdate(tpe -> containerType, {
- val (ps, idT, condVars, condTree, clauses, types, funs) = tmplCache.getOrElseUpdate(tpe, {
+ val (ps, idT, exprVars, condVars, condTree, clauses, types, funs) = tmplCache.getOrElseUpdate(tpe, {
val b = new Builder(tpe)
assert(b.calls.isEmpty, "Captured function templates shouldn't have any calls: " + b.calls)
- (b.pathVar -> b.pathVarT, b.idT, b.conds, b.tree, b.clauses, b.types, b.funs)
+ (b.pathVar -> b.pathVarT, b.idT, b.exprs, b.conds, b.tree, b.clauses, b.types, b.funs)
})
val ctpe = bestRealType(containerType).asInstanceOf[FunctionType]
@@ -431,7 +496,7 @@ trait DatatypeTemplates { self: Templates =>
val containerT = encodeSymbol(container)
val typeBlockers: TypeBlockers = types.map { case (blocker, tps) =>
- blocker -> tps.map { case (tadt, arg) => TemplateTypeInfo(tadt, arg, Some(containerT -> ctpe)) }
+ blocker -> tps.map { case (info, arg) => TemplateTypeInfo(info, arg, Some(containerT -> ctpe)) }
}
val orderClauses = funs.map { case (blocker, tpe, f) =>
@@ -439,7 +504,7 @@ trait DatatypeTemplates { self: Templates =>
}
new CaptureTemplate(ps, containerT, idT,
- condVars, condTree, clauses ++ orderClauses, typeBlockers, funs.map(_._3))
+ exprVars, condVars, condTree, clauses ++ orderClauses, typeBlockers, funs.map(_._3))
})
}
@@ -482,12 +547,12 @@ trait DatatypeTemplates { self: Templates =>
val newTypeInfos = typeBlockers.flatMap(id => typeInfos.get(id).map(id -> _))
typeInfos --= typeBlockers
- for ((blocker, (gen, _, _, tps)) <- newTypeInfos; info @ TemplateTypeInfo(tadt, arg, oc) <- tps) oc match {
+ for ((blocker, (gen, _, _, tps)) <- newTypeInfos; TemplateTypeInfo(info, arg, oc) <- tps) oc match {
case None =>
- val template = DatatypeTemplate(tadt.toType)
+ val template = DatatypeTemplate(info.getType)
newClauses ++= template.instantiate(blocker, arg)
case Some((container, containerType)) =>
- val template = CaptureTemplate(tadt.toType, containerType)
+ val template = CaptureTemplate(info.getType, containerType)
newClauses ++= template.instantiate(blocker, container, arg)
}
diff --git a/src/test/scala/inox/TestContext.scala b/src/test/scala/inox/TestContext.scala
new file mode 100644
index 000000000..ebc8f457f
--- /dev/null
+++ b/src/test/scala/inox/TestContext.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+
+object TestContext {
+
+ def apply(options: Options) = {
+ val reporter = new TestSilentReporter
+ Context(reporter, new utils.InterruptManager(reporter), options)
+ }
+
+ def empty = apply(Options.empty)
+}
diff --git a/src/it/scala/inox/TestSilentReporter.scala b/src/test/scala/inox/TestSilentReporter.scala
similarity index 100%
rename from src/it/scala/inox/TestSilentReporter.scala
rename to src/test/scala/inox/TestSilentReporter.scala
diff --git a/src/test/scala/inox/solvers/GlobalVariablesSuite.scala b/src/test/scala/inox/solvers/GlobalVariablesSuite.scala
new file mode 100644
index 000000000..541135689
--- /dev/null
+++ b/src/test/scala/inox/solvers/GlobalVariablesSuite.scala
@@ -0,0 +1,39 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+
+import org.scalatest._
+
+class GlobalVariablesSuite extends FunSuite {
+ import inox.trees._
+ import dsl._
+
+ val ctx = TestContext.empty
+
+ val freeVariable = Variable(FreshIdentifier("b"), BooleanType)
+
+ val testFd = mkFunDef(FreshIdentifier("test"))()(_ => (
+ Seq("i" :: IntegerType), IntegerType, { case Seq(i) =>
+ if_ (freeVariable) {
+ i
+ } else_ {
+ E(BigInt(-1))
+ }
+ }))
+
+ val program = InoxProgram(ctx, NoSymbols.withFunctions(Seq(testFd)))
+
+ val solverNames: Seq[String] = {
+ (if (SolverFactory.hasNativeZ3) Seq("nativez3") else Nil) ++
+ (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
+ (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
+ }
+
+ for (sname <- solverNames) {
+ test(s"Global Variables in $sname") {
+ val cnstr = freeVariable && testFd(E(BigInt(42))) < E(BigInt(0))
+ assert(SimpleSolverAPI(SolverFactory(sname, program, program.ctx.options)).solveSAT(cnstr).isUNSAT)
+ }
+ }
+}
diff --git a/src/test/scala/inox/solvers/SolverPoolSuite.scala b/src/test/scala/inox/solvers/SolverPoolSuite.scala
index 452fffcc9..d7c75862d 100644
--- a/src/test/scala/inox/solvers/SolverPoolSuite.scala
+++ b/src/test/scala/inox/solvers/SolverPoolSuite.scala
@@ -11,7 +11,7 @@ class SolverPoolSuite extends FunSuite {
import inox.trees._
import SolverResponses._
- implicit val ctx = Context.empty
+ implicit val ctx = TestContext.empty
private trait DummySolver extends Solver {
val name = "Dummy"
diff --git a/src/test/scala/inox/solvers/SolversSuite.scala b/src/test/scala/inox/solvers/SolversSuite.scala
new file mode 100644
index 000000000..115e7153d
--- /dev/null
+++ b/src/test/scala/inox/solvers/SolversSuite.scala
@@ -0,0 +1,79 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+
+import org.scalatest._
+
+class SolversSuite extends FunSuite {
+ import inox.trees._
+ import SolverResponses._
+
+ val ctx = TestContext.empty
+ val p = InoxProgram(ctx, NoSymbols)
+
+ import p._
+ import p.symbols._
+
+ val solverNames: Seq[String] = {
+ (if (SolverFactory.hasNativeZ3) Seq("nativez3") else Nil) ++
+ (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
+ (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
+ }
+
+ val types = Seq(
+ BooleanType,
+ UnitType,
+ CharType,
+ RealType,
+ IntegerType,
+ Int32Type,
+ StringType,
+ TypeParameter.fresh("T"),
+ SetType(IntegerType),
+ BagType(IntegerType),
+ MapType(IntegerType, IntegerType),
+ FunctionType(Seq(IntegerType), IntegerType),
+ TupleType(Seq(IntegerType, BooleanType, Int32Type))
+ )
+
+ val vs = types.map(tpe => Variable(FreshIdentifier("v", true), tpe))
+
+ // We need to make sure models are not co-finite
+ val cnstrs = vs.map(v => v.getType match {
+ case UnitType =>
+ Equals(v, simplestValue(v.getType))
+ case SetType(base) =>
+ Not(ElementOfSet(simplestValue(base), v))
+ case BagType(base) =>
+ Not(Equals(MultiplicityInBag(simplestValue(base), v), simplestValue(IntegerType)))
+ case MapType(from, to) =>
+ Not(Equals(MapApply(v, simplestValue(from)), simplestValue(to)))
+ case FunctionType(froms, to) =>
+ Not(Equals(Application(v, froms.map(simplestValue)), simplestValue(to)))
+ case _ =>
+ not(Equals(v, simplestValue(v.getType)))
+ })
+
+ def checkSolver(sf: SolverFactory { val program: p.type }, vs: Set[Variable], cnstr: Expr): Unit = {
+ SimpleSolverAPI(sf).solveSAT(cnstr) match {
+ case SatWithModel(model) =>
+ for (v <- vs) model.get(v.toVal) match {
+ case Some(e) =>
+ assert(e.getType === v.tpe, s"Solver ${sf.name} - Extracting value of type ${v.tpe}")
+ case _ =>
+ fail(s"Solver ${sf.name} - Model does not contain ${v.id.uniqueName} of type ${v.tpe}")
+ }
+ case res =>
+ fail(s"Solver ${sf.name} - Constraint ${cnstr.asString} is unsat!?")
+ }
+ }
+
+ // Check that we correctly extract several types from solver models
+ for (sname <- solverNames) {
+ test(s"Model Extraction in $sname") {
+ val sf = SolverFactory(sname, p, ctx.options)
+ checkSolver(sf, vs.toSet, andJoin(cnstrs))
+ }
+ }
+}
diff --git a/src/test/scala/inox/solvers/TimeoutSolverSuite.scala b/src/test/scala/inox/solvers/TimeoutSolverSuite.scala
new file mode 100644
index 000000000..849fda8eb
--- /dev/null
+++ b/src/test/scala/inox/solvers/TimeoutSolverSuite.scala
@@ -0,0 +1,60 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+
+import org.scalatest._
+
+class TimeoutSolverSuite extends FunSuite {
+ import inox.trees._
+ import dsl._
+
+ val ctx = TestContext.empty
+ val p = InoxProgram(ctx, NoSymbols)
+
+ private class IdioticSolver extends Solver {
+ val name = "Idiotic"
+ val program: p.type = p
+ val options = ctx.options
+
+ var interrupted = false
+
+ import SolverResponses._
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions] = {
+ while(!interrupted) Thread.sleep(50L)
+ config.cast(Unknown)
+ }
+
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = {
+ while(!interrupted) Thread.sleep(50L)
+ config.cast(Unknown)
+ }
+
+ def recoverInterrupt(): Unit = { interrupted = false }
+ def interrupt(): Unit = { interrupted = true }
+
+ def assertCnstr(e: Expr) = ()
+
+ def push(): Unit = ()
+ def pop(): Unit = ()
+ def free(): Unit = ()
+ def reset(): Unit = ()
+ }
+
+ private val sfactory = SolverFactory.create(p)("idiotic",
+ () => (new IdioticSolver with combinators.TimeoutSolver).setTimeout(200L))
+
+ test("TimeoutSolver 1") {
+ assert(SimpleSolverAPI(sfactory).solveVALID(BooleanLiteral(true)) === None)
+ assert(SimpleSolverAPI(sfactory).solveVALID(BooleanLiteral(false)) === None)
+
+ val x = Variable(FreshIdentifier("x"), IntegerType)
+ assert(SimpleSolverAPI(sfactory).solveVALID(x === x) === None)
+ }
+
+ test("TimeoutSolver 2") {
+ val x = Variable(FreshIdentifier("x"), IntegerType)
+ assert(SimpleSolverAPI(sfactory).solveVALID(x + E(BigInt(1)) === E(BigInt(1)) + x) === None)
+ assert(SimpleSolverAPI(sfactory).solveVALID(x + E(BigInt(1)) === x) === None)
+ }
+}
--
GitLab