diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index 7ee370361e30105c345d3cd7410c758a5dec8b65..1fd32caff60d4f5dacb9f4f264f90c268b951112 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -285,7 +285,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
protected def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = {
e match {
- case v@Variable(id, tp) =>
+ case v @ Variable(id, tp) =>
declareSort(tp)
bindings.getOrElse(id, variables.toB(v))
@@ -316,7 +316,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
case AsInstanceOf(expr, cct) =>
toSMT(expr)
- case io@IsInstanceOf(e, cct) =>
+ case io @ IsInstanceOf(e, cct) =>
declareSort(cct)
val cases = cct.lookupClass match {
case Some(act: TypedAbstractClassDef) =>
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index d31f11fc97ed0e879afb85a025d31943af454a05..db0a91287975a3992d8d30c12548b73b0d77ae65 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -65,83 +65,13 @@ trait DatatypeTemplates { self: Templates =>
res
}
- private case class FreshFunction(expr: Expr) extends Expr { //with Extractable {
- def getType(implicit s: Symbols) = BooleanType
- val extract = Some(Seq(expr), (exprs: Seq[Expr]) => FreshFunction(exprs.head))
- }
-
- private case class InductiveType(tcd: TypedAbstractClassDef, expr: Expr) extends Expr { //with Extractable {
- def getType(implicit s: Symbols) = BooleanType
- val extract = Some(Seq(expr), (exprs: Seq[Expr]) => InductiveType(tcd, exprs.head))
- }
-
- private def typeUnroller(expr: Expr): Expr = expr.getType match {
- case tpe if !requireTypeUnrolling(tpe) =>
- BooleanLiteral(true)
-
- case ct: ClassType =>
- val tcd = ct.tcd
-
- val inv: Seq[Expr] = if (tcd.hasInvariant) {
- Seq(tcd.invariant.get.applied(Seq(expr)))
- } else {
- Seq.empty
- }
-
- def unrollFields(tcd: TypedCaseClassDef): Seq[Expr] = tcd.fields.map { vd =>
- val tpe = tcd.toType
- typeUnroller(CaseClassSelector(AsInstanceOf(expr, tpe), vd.id))
- }
-
- val fields: Seq[Expr] = if (tcd != tcd.root) {
- IsInstanceOf(expr, tcd.toType) +: unrollFields(tcd.toCase)
- } else {
- val isInductive = tcd.cd match {
- case acd: AbstractClassDef => acd.isInductive
- case _ => false
- }
-
- if (!isInductive) {
- val matchers = tcd.root match {
- case (act: TypedAbstractClassDef) => act.descendants
- case (cct: TypedCaseClassDef) => Seq(cct)
- }
-
- val thens = matchers.map(tcd => tcd -> andJoin(unrollFields(tcd)))
-
- if (thens.forall(_._2 == BooleanLiteral(true))) {
- Seq.empty
- } else {
- val (ifs :+ last) = thens
- Seq(ifs.foldRight(last._2) { case ((tcd, thenn), res) =>
- IfExpr(IsInstanceOf(expr, tcd.toType), thenn, res)
- })
- }
- } else {
- Seq(InductiveType(tcd.toAbstract, expr))
- }
- }
-
- andJoin(inv ++ fields)
-
- case TupleType(tpes) =>
- andJoin(tpes.zipWithIndex.map(p => typeUnroller(TupleSelect(expr, p._2 + 1))))
-
- case FunctionType(_, _) =>
- FreshFunction(expr)
-
- case _ => scala.sys.error("TODO")
- }
-
def apply(tpe: Type): DatatypeTemplate = {
val v = Variable(FreshIdentifier("x", true), tpe)
- val expr = typeUnroller(v)
-
val pathVar = Variable(FreshIdentifier("b", true), BooleanType)
var condVars = Map[Variable, Encoded]()
var condTree = Map[Variable, Set[Variable]](pathVar -> Set.empty).withDefaultValue(Set.empty)
- def storeCond(pathVar: Variable, v: Variable): Unit = {
+ @inline def storeCond(pathVar: Variable, v: Variable): Unit = {
condVars += v -> encodeSymbol(v)
condTree += pathVar -> (condTree(pathVar) + v)
}
@@ -152,85 +82,103 @@ trait DatatypeTemplates { self: Templates =>
guardedExprs += pathVar -> (expr +: prev)
}
- def iff(e1: Expr, e2: Expr): Unit = storeGuarded(pathVar, Equals(e1, e2))
+ @inline def iff(e1: Expr, e2: Expr): Unit = storeGuarded(pathVar, Equals(e1, e2))
+
+ var types = Map[Variable, Set[(TypedAbstractClassDef, Expr)]]()
+ @inline def storeType(pathVar: Variable, tacd: TypedAbstractClassDef, arg: Expr): Unit = {
+ types += pathVar -> (types.getOrElse(pathVar, Set.empty) + (tacd -> arg))
+ }
+
+ var functions = Map[Variable, Set[Expr]]()
+ @inline def storeFunction(pathVar: Variable, expr: Expr): Unit = {
+ functions += pathVar -> (functions.getOrElse(pathVar, Set.empty) + expr)
+ }
+
+ def rec(pathVar: Variable, expr: Expr): Unit = expr.getType match {
+ case tpe if !requireTypeUnrolling(tpe) =>
+ // nothing to do here!
- def requireDecomposition(e: Expr): Boolean = exprOps.exists {
- case _: FunctionInvocation => true
- case _: InductiveType => true
- case _ => false
- } (e)
+ case ct: ClassType =>
+ val tcd = ct.tcd
- def rec(pathVar: Variable, expr: Expr): Unit = expr match {
- case i @ IfExpr(cond, thenn, elze) if requireDecomposition(i) =>
- val newBool1: Variable = Variable(FreshIdentifier("b", true), BooleanType)
- val newBool2: Variable = Variable(FreshIdentifier("b", true), BooleanType)
+ if (tcd.hasInvariant) {
+ storeGuarded(pathVar, tcd.invariant.get.applied(Seq(expr)))
+ }
- storeCond(pathVar, newBool1)
- storeCond(pathVar, newBool2)
+ if (tcd.cd.isAbstract && tcd.toAbstract.cd.isInductive) {
+ storeType(pathVar, tcd.toAbstract, expr)
+ } else if (tcd != tcd.root) {
+ storeGuarded(pathVar, IsInstanceOf(expr, tcd.toType))
- iff(and(pathVar, cond), newBool1)
- iff(and(pathVar, not(cond)), newBool2)
+ val tpe = tcd.toType
+ for (vd <- tcd.toCase.fields) {
+ rec(pathVar, CaseClassSelector(AsInstanceOf(expr, tpe), vd.id))
+ }
+ } else {
+ val matchers = tcd.root match {
+ case (act: TypedAbstractClassDef) => act.descendants
+ case (cct: TypedCaseClassDef) => Seq(cct)
+ }
- rec(newBool1, thenn)
- rec(newBool2, elze)
+ for (tccd <- matchers) {
+ val tpe = tccd.toType
- case a @ And(es) if requireDecomposition(a) =>
- val partitions = SeqUtils.groupWhile(es)(!requireDecomposition(_))
- for (e <- partitions.map(andJoin)) rec(pathVar, e)
+ if (requireTypeUnrolling(tpe)) {
+ val newBool: Variable = Variable(FreshIdentifier("b", true), BooleanType)
+ storeCond(pathVar, newBool)
- case _ =>
- storeGuarded(pathVar, expr)
+ iff(and(pathVar, IsInstanceOf(expr, tpe)), newBool)
+ for (vd <- tccd.fields) {
+ rec(newBool, CaseClassSelector(AsInstanceOf(expr, tpe), vd.id))
+ }
+ }
+ }
+ }
+
+ case TupleType(tpes) =>
+ for ((_, idx) <- tpes.zipWithIndex) {
+ rec(pathVar, TupleSelect(expr, idx + 1))
+ }
+
+ case FunctionType(_, _) =>
+ storeFunction(pathVar, expr)
+
+ case _ => scala.sys.error("TODO")
}
- rec(pathVar, expr)
+ rec(pathVar, v)
val (idT, pathVarT) = (encodeSymbol(v), encodeSymbol(pathVar))
val encoder: Expr => Encoded = mkEncoder(condVars + (v -> idT) + (pathVar -> pathVarT))
var clauses: Clauses = Seq.empty
var calls: CallBlockers = Map.empty
- var types: Map[Encoded, Set[TemplateTypeInfo]] = Map.empty
- var functions: Functions = Set.empty
for ((b, es) <- guardedExprs) {
- var callInfos : Set[Call] = Set.empty
- var typeInfos : Set[TemplateTypeInfo] = Set.empty
+ var callInfos : Set[Call] = Set.empty
for (e <- es) {
- val collected = collectWithPaths {
- case expr @ (_: InductiveType | _: FreshFunction) => expr
- } (e)
-
- def clean(e: Expr) = exprOps.postMap {
- case _: InductiveType => Some(BooleanLiteral(true))
- case _: FreshFunction => Some(BooleanLiteral(true))
- case _ => None
- } (e)
-
- functions ++= collected.collect { case (FreshFunction(f), path) =>
- val tpe = bestRealType(f.getType).asInstanceOf[FunctionType]
- val cleanPath = path.map(clean)
- (encoder(and(b, cleanPath.toPath)), tpe, encoder(f))
- }
-
- typeInfos ++= collected.collect { case (InductiveType(tcd, e), path) =>
- assert(path.isEmpty, "Inductive datatype unfolder should be implied directly by the blocker")
- TemplateTypeInfo(tcd, encoder(e))
- }
-
- val cleanExpr = clean(e)
- callInfos ++= firstOrderCallsOf(cleanExpr).map { case (id, tps, args) =>
+ callInfos ++= firstOrderCallsOf(e).map { case (id, tps, args) =>
Call(getFunction(id, tps), args.map(arg => Left(encoder(arg))))
}
- clauses :+= encoder(Implies(b, cleanExpr))
+ clauses :+= encoder(Implies(b, e))
}
- if (typeInfos.nonEmpty) types += encoder(b) -> typeInfos
if (callInfos.nonEmpty) calls += encoder(b) -> callInfos
}
- new DatatypeTemplate(pathVar -> pathVarT, idT, condVars, condTree, clauses, calls, types, functions)
+ val encodedTypes: Map[Encoded, Set[TemplateTypeInfo]] = types.map { case (b, tps) =>
+ encoder(b) -> tps.map { case (tacd, expr) => TemplateTypeInfo(tacd, encoder(expr)) }
+ }
+
+ val encodedFunctions: Functions = functions.flatMap { case (b, fs) =>
+ val bp = encoder(b)
+ fs.map(expr => (bp, bestRealType(expr.getType).asInstanceOf[FunctionType], encoder(expr)))
+ }.toSet
+
+ new DatatypeTemplate(pathVar -> pathVarT, idT, condVars, condTree,
+ clauses, calls, encodedTypes, encodedFunctions)
}
}
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 68e2f8994ee2155e7c8e6d4c563be3dcc140bbc7..4c8b36e895428218f9d95db6db62c958a7f1d370 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -121,7 +121,7 @@ trait TemplateGenerator { self: Templates =>
guardedExprs += guardVar -> (expr +: prev)
}
- def iff(e1: Expr, e2: Expr): Unit = storeGuarded(pathVar, Equals(e1, e2))
+ @inline def iff(e1: Expr, e2: Expr): Unit = storeGuarded(pathVar, Equals(e1, e2))
var lambdaVars = Map[Variable, Encoded]()
@inline def storeLambda(id: Variable): Encoded = {