From d04f60ba1fd97a8ac71fe3aaab9c1645a1be7f22 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 5 Aug 2016 13:05:40 +0200
Subject: [PATCH] Native z3 solvers finished
---
src/main/scala/inox/ast/Expressions.scala | 4 +
src/main/scala/inox/ast/TypeOps.scala | 23 ++
src/main/scala/inox/solvers/ADTManager.scala | 149 --------
src/main/scala/inox/solvers/ADTManagers.scala | 96 +++++
.../inox/solvers/CantResetException.scala | 2 +-
src/main/scala/inox/solvers/Model.scala | 102 ------
src/main/scala/inox/solvers/Solver.scala | 45 +--
.../scala/inox/solvers/SolverResponses.scala | 38 +-
.../inox/solvers/theories/TheoryEncoder.scala | 15 +-
.../solvers/unrolling/DatatypeTemplates.scala | 2 +-
.../solvers/unrolling/LambdaTemplates.scala | 21 +-
.../inox/solvers/unrolling/Templates.scala | 12 +-
.../solvers/unrolling/UnrollingSolver.scala | 19 +-
.../inox/solvers/z3/AbstractZ3Solver.scala | 333 +++++++++---------
.../scala/inox/solvers/z3/FairZ3Solver.scala | 199 -----------
.../inox/solvers/z3/NativeZ3Solver.scala | 114 ++++++
.../solvers/z3/UninterpretedZ3Solver.scala | 77 ++--
.../solvers/z3/Z3ModelReconstruction.scala | 70 ----
src/main/scala/inox/solvers/z3/Z3Solver.scala | 7 -
.../inox/utils/IncrementalStateWrapper.scala | 2 +-
src/main/scala/inox/utils/SCC.scala | 6 +-
21 files changed, 536 insertions(+), 800 deletions(-)
delete mode 100644 src/main/scala/inox/solvers/ADTManager.scala
create mode 100644 src/main/scala/inox/solvers/ADTManagers.scala
delete mode 100644 src/main/scala/inox/solvers/Model.scala
delete mode 100644 src/main/scala/inox/solvers/z3/FairZ3Solver.scala
create mode 100644 src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
delete mode 100644 src/main/scala/inox/solvers/z3/Z3ModelReconstruction.scala
delete mode 100644 src/main/scala/inox/solvers/z3/Z3Solver.scala
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 119ac9df4..4aa8a174f 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -247,6 +247,10 @@ trait Expressions { self: Trees =>
*/
case class CaseClassSelector(caseClass: Expr, selector: Identifier) extends Expr with CachingTyped {
+ def selectorIndex(implicit s: Symbols) = classIndex.map(_._2).getOrElse {
+ throw FatalError("Not well formed selector: " + this)
+ }
+
def classIndex(implicit s: Symbols) = caseClass.getType match {
case ct: ClassType => ct.lookupClass match {
case Some(tcd: TypedCaseClassDef) =>
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index 8724b6e0e..84ae5e354 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -262,4 +262,27 @@ trait TypeOps {
}
}
+ def typeDependencies(tpe: Type): Map[Type, Set[Type]] = {
+ var dependencies: Map[Type, Set[Type]] = Map.empty
+
+ def rec(tpe: Type): Unit = if (!dependencies.isDefinedAt(tpe)) {
+ val next = tpe match {
+ case ct: ClassType => ct.tcd match {
+ case accd: TypedAbstractClassDef =>
+ accd.descendants.map(_.toType)
+ case tccd: TypedCaseClassDef =>
+ tccd.fieldsTypes
+ }
+ case NAryType(tps, _) =>
+ tps
+ }
+
+ dependencies += tpe -> next.toSet
+ next.foreach(rec)
+ }
+
+ rec(tpe)
+ dependencies
+ }
+
}
diff --git a/src/main/scala/inox/solvers/ADTManager.scala b/src/main/scala/inox/solvers/ADTManager.scala
deleted file mode 100644
index 25f4021d0..000000000
--- a/src/main/scala/inox/solvers/ADTManager.scala
+++ /dev/null
@@ -1,149 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package inox
-package solvers
-
-trait ADTManagers {
- val program: Program
- import program._
- import trees._
-
- case class DataType(sym: Identifier, cases: Seq[Constructor]) extends Printable {
- def asString(implicit opts: PrinterOptions) = {
- "Datatype: " + sym.asString(opts) + "\n" + cases.map(c => " - " + c.asString(opts)).mkString("\n")
- }
- }
-
- case class Constructor(sym: Identifier, tpe: Type, fields: Seq[(Identifier, Type)]) extends Printable {
- def asString(implicit opts: PrinterOptions) = {
- sym.asString(opts) + " [" + tpe.asString(opts) + "] " + fields.map(f => f._1.asString(opts) + ": " + f._2.asString(opts)).mkString("(", ", ", ")")
- }
- }
-
- class ADTManager(ctx: InoxContext) {
- val reporter = ctx.reporter
-
- protected def freshId(id: Identifier): Identifier = freshId(id.name)
-
- protected def freshId(name: String): Identifier = FreshIdentifier(name)
-
- protected def getHierarchy(ct: TypedClassDef): (TypedClassDef, Seq[TypedCaseClassDef]) = ct match {
- case acd: TypedAbstractClassDef =>
- (acd, acd.descendants)
- case ccd: TypedCaseClassDef =>
- (ccd, List(ccd))
-
- }
-
- protected var defined = Set[Type]()
- protected var locked = Set[Type]()
-
- protected var discovered = Map[Type, DataType]()
-
- def defineADT(t: Type): Either[Map[Type, DataType], Set[Type]] = {
- discovered = Map()
- locked = Set()
-
- findDependencies(t)
-
- val conflicts = discovered.keySet & locked
-
- if (conflicts(t)) {
- // There is no way to solve this, the type we requested is in conflict
- val str = "Encountered ADT that can't be defined.\n" +
- "It appears it has recursive references through non-structural types (such as arrays, maps, or sets)."
- val err = new Unsupported(t, str)(ctx)
- reporter.warning(err.getMessage)
- throw err
- } else {
- // We might be able to define some despite conflicts
- if (conflicts.isEmpty) {
- for ((t, dt) <- discovered) {
- defined += t
- }
- Left(discovered)
- } else {
- Right(conflicts)
- }
- }
- }
-
- def forEachType(t: Type, alreadyDone: Set[Type] = Set())(f: Type => Unit): Unit = if (!alreadyDone(t)) {
- t match {
- case NAryType(tps, builder) =>
- f(t)
- val alreadyDone2 = alreadyDone + t
- // note: each of the tps could be abstract classes in which case we need to
- // lock their dependencies, transitively.
- tps.foreach {
- case ct: ClassType =>
- val (root, sub) = getHierarchy(ct.lookupClass.get)
- sub.flatMap(_.fields.map(_.getType)).foreach(subt => forEachType(subt, alreadyDone2)(f))
- case othert =>
- forEachType(othert, alreadyDone2)(f)
- }
- }
- }
-
- protected def findDependencies(t: Type): Unit = t match {
- case _: SetType | _: MapType =>
- forEachType(t) { tpe =>
- if (!defined(tpe)) {
- locked += tpe
- }
- }
-
- case ct: ClassType =>
- val (root, sub) = getHierarchy(ct.lookupClass.get)
-
- if (!(discovered contains root.toType) && !(defined contains root.toType)) {
- val sym = freshId(root.id)
-
- val conss = sub.map { case cct =>
- Constructor(freshId(cct.id), cct.toType, cct.fields.map(vd => (freshId(vd.id), vd.getType)))
- }
-
- discovered += (root.toType -> DataType(sym, conss))
-
- // look for dependencies
- for (ct <- sub; f <- ct.fields) {
- findDependencies(f.getType)
- }
- }
-
- case tt@TupleType(bases) =>
- if (!(discovered contains t) && !(defined contains t)) {
- val sym = freshId("tuple" + bases.size)
-
- val c = Constructor(freshId(sym.name), tt, bases.zipWithIndex.map {
- case (tpe, i) => (freshId("_" + (i + 1)), tpe)
- })
-
- discovered += (tt -> DataType(sym, Seq(c)))
-
- for (b <- bases) {
- findDependencies(b)
- }
- }
-
- case UnitType =>
- if (!(discovered contains t) && !(defined contains t)) {
- discovered += (t -> DataType(freshId("Unit"), Seq(Constructor(freshId("Unit"), t, Nil))))
- }
-
- case tp@TypeParameter(id) =>
- if (!(discovered contains t) && !(defined contains t)) {
- val sym = freshId(id.name)
-
- val c = Constructor(freshId(sym.name), tp, List(
- (freshId("val"), IntegerType)
- ))
-
- discovered += (tp -> DataType(sym, Seq(c)))
- }
-
- case _ =>
- }
- }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/inox/solvers/ADTManagers.scala b/src/main/scala/inox/solvers/ADTManagers.scala
new file mode 100644
index 000000000..51e1bdadf
--- /dev/null
+++ b/src/main/scala/inox/solvers/ADTManagers.scala
@@ -0,0 +1,96 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+
+import utils._
+
+trait ADTManagers {
+ val program: Program
+ import program._
+ import program.trees._
+ import program.symbols._
+
+ case class DataType(sym: Identifier, cases: Seq[Constructor]) extends Printable {
+ def asString(implicit opts: PrinterOptions) = {
+ "Datatype: " + sym.asString(opts) + "\n" + cases.map(c => " - " + c.asString(opts)).mkString("\n")
+ }
+ }
+
+ case class Constructor(sym: Identifier, tpe: Type, fields: Seq[(Identifier, Type)]) extends Printable {
+ def asString(implicit opts: PrinterOptions) = {
+ sym.asString(opts) + " [" + tpe.asString(opts) + "] " + fields.map(f => f._1.asString(opts) + ": " + f._2.asString(opts)).mkString("(", ", ", ")")
+ }
+ }
+
+ class ADTManager extends IncrementalStateWrapper {
+
+ protected def freshId(id: Identifier): Identifier = freshId(id.name)
+
+ protected def freshId(name: String): Identifier = FreshIdentifier(name)
+
+ private val declared = new IncrementalSet[Type]
+ protected val incrementals = Seq(declared)
+
+ def declareADTs(tpe: Type, declare: Seq[(Type, DataType)] => Unit): Unit = {
+ val deps = typeDependencies(tpe)
+ val transitiveDeps: Map[Type, Set[Type]] = utils.fixpoint { (map: Map[Type, Set[Type]]) =>
+ map.map { case (tpe, types) => tpe -> (types ++ types.flatMap(map.getOrElse(_, Set.empty))) }
+ } (deps)
+
+ val sccs = SCC.scc(deps)
+
+ // check whether all types can be defined
+ for (scc <- sccs if scc.exists(tpe => (transitiveDeps(tpe) & scc).nonEmpty); tpe <- scc) tpe match {
+ case t @ ((_: MapType) | (_: SetType) | (_: BagType)) =>
+ val str = "Encountered ADT that can't be defined.\n" +
+ "It appears it has recursive references through non-structural types (such as arrays, maps, or sets)."
+ val err = new Unsupported(t, str)
+ ctx.reporter.warning(err.getMessage)
+ throw err
+ case _ =>
+ }
+
+ for (scc <- sccs) {
+
+ val declarations = (for (tpe <- scc if !declared(tpe)) yield (tpe match {
+ case ct: ClassType =>
+ val (root, deps) = ct.tcd.root match {
+ case tacd: TypedAbstractClassDef =>
+ (tacd, tacd.descendants)
+ case tccd: TypedCaseClassDef =>
+ (tccd, Seq(tccd))
+ }
+
+ Some(ct -> DataType(freshId(root.id), deps.map { tccd =>
+ Constructor(freshId(tccd.id), tccd.toType, tccd.fields.map(vd => freshId(vd.id) -> vd.tpe))
+ }))
+
+ case TupleType(tps) =>
+ val sym = freshId("tuple" + tps.size)
+
+ Some(tpe -> DataType(sym, Seq(Constructor(freshId(sym.name), tpe, tps.zipWithIndex.map {
+ case (tpe, i) => (freshId("_" + (i + 1)), tpe)
+ }))))
+
+ case UnitType =>
+ Some(tpe -> DataType(freshId("Unit"), Seq(Constructor(freshId("Unit"), tpe, Nil))))
+
+ case TypeParameter(id) =>
+ val sym = freshId(id.name)
+
+ Some(tpe -> DataType(sym, Seq(Constructor(freshId(sym.name), tpe, List(
+ (freshId("val"), IntegerType)
+ )))))
+
+ case _ => None
+ })).flatten
+
+ if (declarations.nonEmpty) {
+ declare(declarations.toSeq)
+ declared ++= declarations.map(_._1)
+ }
+ }
+ }
+ }
+}
diff --git a/src/main/scala/inox/solvers/CantResetException.scala b/src/main/scala/inox/solvers/CantResetException.scala
index 59999fca4..a9d048466 100644
--- a/src/main/scala/inox/solvers/CantResetException.scala
+++ b/src/main/scala/inox/solvers/CantResetException.scala
@@ -2,4 +2,4 @@
package inox.solvers
-class CantResetException(s: Solver) extends Exception(s"Unable to reset solver $s")
+class CantResetException(s: AbstractSolver) extends Exception(s"Unable to reset solver $s")
diff --git a/src/main/scala/inox/solvers/Model.scala b/src/main/scala/inox/solvers/Model.scala
deleted file mode 100644
index 78b5b0501..000000000
--- a/src/main/scala/inox/solvers/Model.scala
+++ /dev/null
@@ -1,102 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Expressions._
-import purescala.Common.Identifier
-import purescala.Quantification.Domains
-import purescala.ExprOps._
-
-trait AbstractModel[+This <: Model with AbstractModel[This]]
- extends scala.collection.IterableLike[(Identifier, Expr), This]
- with Printable {
-
- protected val mapping: Map[Identifier, Expr]
-
- def set(allVars: Iterable[Identifier]): This = {
- val builder = newBuilder
- builder ++= allVars.map(id => id -> mapping.getOrElse(id, simplestValue(id.getType)))
- builder.result
- }
-
- def ++(mapping: Map[Identifier, Expr]): This = {
- val builder = newBuilder
- builder ++= this.mapping ++ mapping
- builder.result
- }
-
- def filter(allVars: Iterable[Identifier]): This = {
- val builder = newBuilder
- for (p <- mapping.filterKeys(allVars.toSet)) {
- builder += p
- }
- builder.result
- }
-
- def iterator = mapping.iterator
- def seq = mapping.seq
-
- def asString(implicit ctx: LeonContext) = {
- if (mapping.isEmpty) {
- "Model()"
- } else {
- (for ((k,v) <- mapping.toSeq.sortBy(_._1)) yield {
- val valuePadded = v.asString.replaceAll("\n", "\n"+(" "*26))
- f" ${k.asString}%-20s -> ${valuePadded}"
- }).mkString("Model(\n", ",\n", "\n)")
- }
- }
-}
-
-trait AbstractModelBuilder[+This <: Model with AbstractModel[This]]
- extends scala.collection.mutable.Builder[(Identifier, Expr), This] {
-
- import scala.collection.mutable.MapBuilder
- protected val mapBuilder = new MapBuilder[Identifier, Expr, Map[Identifier, Expr]](Map.empty)
-
- def +=(elem: (Identifier, Expr)): this.type = {
- mapBuilder += elem
- this
- }
-
- def clear(): Unit = mapBuilder.clear
-}
-
-class Model(protected val mapping: Map[Identifier, Expr])
- extends AbstractModel[Model]
- with (Identifier => Expr) {
-
- def newBuilder = new ModelBuilder
- def isDefinedAt(id: Identifier): Boolean = mapping.isDefinedAt(id)
- def get(id: Identifier): Option[Expr] = mapping.get(id)
- def getOrElse[E >: Expr](id: Identifier, e: E): E = get(id).getOrElse(e)
- def ids = mapping.keys
- def apply(id: Identifier): Expr = get(id).getOrElse { throw new IllegalArgumentException }
-}
-
-object Model {
- def empty = new Model(Map.empty)
-}
-
-class ModelBuilder extends AbstractModelBuilder[Model] {
- def result = new Model(mapBuilder.result)
-}
-
-class PartialModel(mapping: Map[Identifier, Expr], val domains: Domains)
- extends Model(mapping)
- with AbstractModel[PartialModel] {
-
- override def newBuilder = new PartialModelBuilder(domains)
-}
-
-object PartialModel {
- def empty = new PartialModel(Map.empty, Domains.empty)
-}
-
-class PartialModelBuilder(domains: Domains)
- extends ModelBuilder
- with AbstractModelBuilder[PartialModel] {
-
- override def result = new PartialModel(mapBuilder.result, domains)
-}
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 6c2ef90a9..e72533148 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -26,6 +26,9 @@ trait AbstractSolver extends Interruptible {
val program: Program
val options: SolverOptions
+ import program._
+ import program.trees._
+
type Trees
type Model
type Cores
@@ -37,6 +40,27 @@ trait AbstractSolver extends Interruptible {
// This is ugly, but helpful for smtlib solvers
def dbg(msg: => Any) {}
+ object SolverUnsupportedError {
+ def msg(t: Tree, reason: Option[String]) = {
+ s"(of ${t.getClass}) is unsupported by solver ${name}" + reason.map(":\n " + _ ).getOrElse("")
+ }
+ }
+
+ case class SolverUnsupportedError(t: Tree, reason: Option[String] = None)
+ extends Unsupported(t, SolverUnsupportedError.msg(t,reason))
+
+ protected def unsupported(t: Tree): Nothing = {
+ val err = SolverUnsupportedError(t, None)
+ reporter.warning(err.getMessage)
+ throw err
+ }
+
+ protected def unsupported(t: Tree, str: String): Nothing = {
+ val err = SolverUnsupportedError(t, Some(str))
+ reporter.warning(err.getMessage)
+ throw err
+ }
+
def assertCnstr(expression: Trees): Unit
def check(config: Configuration): config.Response[Model, Cores]
@@ -64,26 +88,5 @@ trait Solver extends AbstractSolver {
type Model = Map[ValDef, Expr]
type Cores = Set[Expr]
- object SolverUnsupportedError {
- def msg(t: Tree, reason: Option[String]) = {
- s"(of ${t.getClass}) is unsupported by solver ${name}" + reason.map(":\n " + _ ).getOrElse("")
- }
- }
-
- case class SolverUnsupportedError(t: Tree, reason: Option[String] = None)
- extends Unsupported(t, SolverUnsupportedError.msg(t,reason))
-
def getResultSolver: Option[Solver] = Some(this)
-
- protected def unsupported(t: Tree): Nothing = {
- val err = SolverUnsupportedError(t, None)
- reporter.warning(err.getMessage)
- throw err
- }
-
- protected def unsupported(t: Tree, str: String): Nothing = {
- val err = SolverUnsupportedError(t, Some(str))
- reporter.warning(err.getMessage)
- throw err
- }
}
diff --git a/src/main/scala/inox/solvers/SolverResponses.scala b/src/main/scala/inox/solvers/SolverResponses.scala
index ac4f84418..d2ffdbdb2 100644
--- a/src/main/scala/inox/solvers/SolverResponses.scala
+++ b/src/main/scala/inox/solvers/SolverResponses.scala
@@ -48,6 +48,8 @@ object SolverResponses {
sealed trait Configuration {
type Response[+M,+C] <: SolverResponse[M,C]
+ def withModel: Boolean
+ def withCores: Boolean
def max(that: Configuration): Configuration = (this, that) match {
case (All , _ ) => All
@@ -79,6 +81,15 @@ object SolverResponses {
case (Cores | All , u @ UnsatWithCores(_)) => u
case _ => throw FatalError("Unexpected response " + resp + " for configuration " + this)
}).asInstanceOf[Response[M,C]]
+
+ def convert[M1,C1,M2,C2](resp: Response[M1,C1], cm: M1 => M2, cc: C1 => C2): Response[M2,C2] =
+ cast(resp.asInstanceOf[SolverResponse[M1,C1]] match {
+ case Unknown => Unknown
+ case Sat => Sat
+ case Unsat => Unsat
+ case SatWithModel(model) => SatWithModel(cm(model))
+ case UnsatWithCores(cores) => UnsatWithCores(cc(cores))
+ })
}
object Configuration {
@@ -89,10 +100,29 @@ object SolverResponses {
else Simple
}
- case object Simple extends Configuration { type Response[+M,+C] = SimpleResponse }
- case object Model extends Configuration { type Response[+M,+C] = ResponseWithModel[M] }
- case object Cores extends Configuration { type Response[+M,+C] = ResponseWithCores[C] }
- case object All extends Configuration { type Response[+M,+C] = ResponseWithModelAndCores[M, C] }
+ case object Simple extends Configuration {
+ type Response[+M,+C] = SimpleResponse
+ def withModel = false
+ def withCores = false
+ }
+
+ case object Model extends Configuration {
+ type Response[+M,+C] = ResponseWithModel[M]
+ def withModel = true
+ def withCores = false
+ }
+
+ case object Cores extends Configuration {
+ type Response[+M,+C] = ResponseWithCores[C]
+ def withModel = false
+ def withCores = true
+ }
+
+ case object All extends Configuration {
+ type Response[+M,+C] = ResponseWithModelAndCores[M, C]
+ def withModel = true
+ def withCores = true
+ }
implicit def wideningConfiguration[M,C](config: Configuration)
(resp: config.Response[M,C]): SolverResponse[M, C] = {
diff --git a/src/main/scala/inox/solvers/theories/TheoryEncoder.scala b/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
index 5c78ad27b..d358d0c7b 100644
--- a/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
@@ -7,17 +7,13 @@ package theories
import utils._
trait TheoryEncoder {
- val trees: ast.Trees
- import trees._
-
- val sourceProgram: Program { val trees: TheoryEncoder.this.trees.type }
+ val sourceProgram: Program
+ lazy val trees: sourceProgram.trees.type = sourceProgram.trees
lazy val targetProgram: Program { val trees: TheoryEncoder.this.trees.type } = {
sourceProgram.transform(encoder)
}
- private type SameTrees = TheoryEncoder {
- val trees: TheoryEncoder.this.trees.type
- }
+ import trees._
protected val encoder: TreeTransformer
protected val decoder: TreeTransformer
@@ -31,8 +27,9 @@ trait TheoryEncoder {
def encode(tpe: Type): Type = encoder.transform(tpe)
def decode(tpe: Type): Type = decoder.transform(tpe)
- def >>(that: SameTrees): SameTrees = new TheoryEncoder {
- val trees: TheoryEncoder.this.trees.type = TheoryEncoder.this.trees
+ def >>(that: TheoryEncoder { val sourceProgram: TheoryEncoder.this.targetProgram.type }): TheoryEncoder {
+ val sourceProgram: TheoryEncoder.this.sourceProgram.type
+ } = new TheoryEncoder {
val sourceProgram: TheoryEncoder.this.sourceProgram.type = TheoryEncoder.this.sourceProgram
val encoder = new TreeTransformer {
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index de89d2274..9d7f34597 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -19,7 +19,7 @@ trait DatatypeTemplates { self: Templates =>
/** Represents a type unfolding of a free variable (or input) in the unfolding procedure */
case class TemplateTypeInfo(tcd: TypedAbstractClassDef, arg: Encoded) {
- override def toString = tcd.toType.asString + "(" + arg.asString + ")"
+ override def toString = tcd.toType.asString + "(" + asString(arg) + ")"
}
private val cache: MutableMap[Type, DatatypeTemplate] = MutableMap.empty
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 2fd60dba7..98f9c9be6 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -23,13 +23,13 @@ trait LambdaTemplates { self: Templates =>
case class TemplateAppInfo(template: Either[LambdaTemplate, Encoded], equals: Encoded, args: Seq[Arg]) {
override def toString = {
val caller = template match {
- case Left(tmpl) => tmpl.ids._2.asString
- case Right(c) => c.asString
+ case Left(tmpl) => asString(tmpl.ids._2)
+ case Right(c) => asString(c)
}
- caller + "|" + equals.asString + args.map {
+ caller + "|" + asString(equals) + args.map {
case Right(m) => m.toString
- case Left(v) => v.asString
+ case Left(v) => asString(v)
}.mkString("(", ",", ")")
}
}
@@ -227,19 +227,6 @@ trait LambdaTemplates { self: Templates =>
private lazy val str : String = stringRepr()
override def toString : String = str
-
- /** When instantiating closure templates, we want to preserve the condition
- * under which the associated closure can be evaluated in the program
- * (namely `pathVar._2`), as well as the condition under which the current
- * application can take place. We therefore have
- * {{{
- * aVar && pathVar._2 ==> instantiation
- * }}}
- */
- override def instantiate(aVar: Encoded, args: Seq[Arg]): Clauses = {
- val (freshBlocker, eqClauses) = encodeBlockers(Set(aVar, pathVar._2))
- eqClauses ++ super.instantiate(freshBlocker, args)
- }
}
def registerFunction(b: Encoded, tpe: FunctionType, f: Encoded): Clauses = {
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index fbb3da51e..eda22625b 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -20,7 +20,9 @@ trait Templates extends TemplateGenerator
import program.trees._
import program.symbols._
- type Encoded <: Printable
+ type Encoded
+
+ def asString(e: Encoded): String
def encodeSymbol(v: Variable): Encoded
def mkEncoder(bindings: Map[Variable, Encoded])(e: Expr): Encoded
@@ -177,7 +179,7 @@ trait Templates extends TemplateGenerator
override def toString = {
tfd.signature + args.map {
case Right(m) => m.toString
- case Left(v) => v.asString
+ case Left(v) => asString(v)
}.mkString("(", ", ", ")")
}
@@ -189,7 +191,7 @@ trait Templates extends TemplateGenerator
/** Represents an application of a first-class function in the unfolding procedure */
case class App(caller: Encoded, tpe: FunctionType, args: Seq[Arg], encoded: Encoded) {
override def toString: String =
- "(" + caller.asString + " : " + tpe.asString + ")" + args.map(_.encoded.asString).mkString("(", ",", ")")
+ "(" + asString(caller) + " : " + tpe.asString + ")" + args.map(a => asString(a.encoded)).mkString("(", ",", ")")
def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): App = copy(
caller = substituter(caller),
@@ -201,11 +203,11 @@ trait Templates extends TemplateGenerator
/** Represents an E-matching matcher that will be used to instantiate relevant quantified propositions */
case class Matcher(key: Either[(Encoded, Type), TypedFunDef], args: Seq[Arg], encoded: Encoded) {
override def toString: String = (key match {
- case Left((c, tpe)) => c.asString + ":" + tpe.asString
+ case Left((c, tpe)) => asString(c) + ":" + tpe.asString
case Right(tfd) => tfd.signature
}) + args.map {
case Right(m) => m.toString
- case Left(v) => v.asString
+ case Left(v) => asString(v)
}.mkString("(", ",", ")")
def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): Matcher = copy(
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 455729157..667e1b8e3 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -24,9 +24,8 @@ trait AbstractUnrollingSolver
import SolverResponses._
protected type Encoded
- protected implicit val printable: Encoded => Printable
- protected val theories: TheoryEncoder { val trees: program.trees.type }
+ protected val theories: TheoryEncoder { val sourceProgram: program.type }
protected val templates: Templates {
val program: theories.targetProgram.type
@@ -284,14 +283,7 @@ trait AbstractUnrollingSolver
object CheckResult {
def cast(resp: SolverResponse[underlying.Model, underlying.Cores]): CheckResult =
- new CheckResult(config cast (resp match {
- case Unknown => Unknown
- case Sat => Sat
- case Unsat => Unsat
- case SatWithModel(model) => SatWithModel(extractSimpleModel(model))
- case UnsatWithCores(cores) => UnsatWithCores(encodedCoreToCore(cores))
- case _ => throw FatalError("Unexpected response " + resp + " for configuration " + config)
- }))
+ new CheckResult(config.convert(config.cast(resp), extractSimpleModel, encodedCoreToCore))
def apply[M <: Model, C <: Cores](resp: config.Response[M, C]) = new CheckResult(resp)
def unapply(res: CheckResult): Option[config.Response[Model, Cores]] = Some(res.response)
@@ -490,6 +482,8 @@ trait UnrollingSolver extends AbstractUnrollingSolver {
val program: theories.targetProgram.type = theories.targetProgram
type Encoded = Expr
+ def asString(expr: Expr): String = expr.asString
+
def encodeSymbol(v: Variable): Expr = v.freshen
def mkEncoder(bindings: Map[Variable, Expr])(e: Expr): Expr =
exprOps.replaceFromSymbols(bindings, e)
@@ -508,9 +502,10 @@ trait UnrollingSolver extends AbstractUnrollingSolver {
}
}
- def declareVariable(v: Variable): Variable = v
+ protected def declareVariable(v: Variable): Variable = v
+ protected def wrapModel(model: Map[ValDef, Expr]): super.ModelWrapper = ModelWrapper(model)
- case class ModelWrapper(model: Map[ValDef, Expr]) extends super.ModelWrapper {
+ private case class ModelWrapper(model: Map[ValDef, Expr]) extends super.ModelWrapper {
def modelEval(elem: Expr, tpe: Type): Option[Expr] = evaluator.eval(elem, model).result
override def toString = model.mkString("\n")
}
diff --git a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
index c5c19a249..e9008fbc5 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -13,13 +13,20 @@ case class UnsoundExtractionException(ast: Z3AST, msg: String)
// This is just to factor out the things that are common in "classes that deal
// with a Z3 instance"
-trait AbstractZ3Solver extends AbstractSolver {
- context.interruptManager.registerForInterrupts(this)
+trait AbstractZ3Solver
+ extends AbstractSolver
+ with ADTManagers {
import program._
import program.trees._
import program.symbols._
- import program.symbols.typeOps.bestRealType
+ import program.symbols.bestRealType
+
+ import SolverResponses._
+
+ val name = "AbstractZ3"
+
+ ctx.interruptManager.registerForInterrupts(this)
type Trees = Z3AST
type Model = Z3Model
@@ -39,7 +46,7 @@ trait AbstractZ3Solver extends AbstractSolver {
}
}
- protected var z3 : Z3Context = new Z3Context(
+ protected[z3] var z3 : Z3Context = new Z3Context(
"MODEL" -> true,
"TYPE_CHECK" -> true,
"WELL_SORTED_CHECK" -> true
@@ -76,22 +83,58 @@ trait AbstractZ3Solver extends AbstractSolver {
}
}
+ def declareVariable(v: Variable): Z3AST = variables.cachedB(v) {
+ symbolToFreshZ3Symbol(v)
+ }
+
// ADT Manager
- protected val adtManager = new ADTManager(context)
+ private val adtManager = new ADTManager
// Bijections between Leon Types/Functions/Ids to Z3 Sorts/Decls/ASTs
- protected val functions = new IncrementalBijection[TypedFunDef, Z3FuncDecl]()
- protected val lambdas = new IncrementalBijection[FunctionType, Z3FuncDecl]()
- protected val variables = new IncrementalBijection[Expr, Z3AST]()
+ private val functions = new IncrementalBijection[TypedFunDef, Z3FuncDecl]()
+ private val lambdas = new IncrementalBijection[FunctionType, Z3FuncDecl]()
+ private val variables = new IncrementalBijection[Variable, Z3AST]()
+
+ private val constructors = new IncrementalBijection[Type, Z3FuncDecl]()
+ private val selectors = new IncrementalBijection[(Type, Int), Z3FuncDecl]()
+ private val testers = new IncrementalBijection[Type, Z3FuncDecl]()
+
+ private val sorts = new IncrementalMap[Type, Z3Sort]()
+
+ def push(): Unit = {
+ adtManager.push()
+ functions.push()
+ lambdas.push()
+ variables.push()
+
+ constructors.push()
+ selectors.push()
+ testers.push()
+
+ sorts.push()
+ if (isInitialized) solver.push()
+ }
+
+ def pop(): Unit = {
+ adtManager.pop()
+ functions.pop()
+ lambdas.pop()
+ variables.pop()
- protected val constructors = new IncrementalBijection[Type, Z3FuncDecl]()
- protected val selectors = new IncrementalBijection[(Type, Int), Z3FuncDecl]()
- protected val testers = new IncrementalBijection[Type, Z3FuncDecl]()
+ constructors.pop()
+ selectors.pop()
+ testers.pop()
- protected val sorts = new IncrementalMap[Type, Z3Sort]()
+ sorts.pop()
+ if (isInitialized) solver.pop()
+ }
+
+ def reset(): Unit = {
+ throw new CantResetException(this)
+ }
- var isInitialized = false
- protected[leon] def initZ3(): Unit = {
+ private var isInitialized = false
+ protected def initZ3(): Unit = {
if (!isInitialized) {
solver = z3.mkSolver()
@@ -111,24 +154,9 @@ trait AbstractZ3Solver extends AbstractSolver {
initZ3()
- def rootType(ct: Type): Type = ct match {
- case ct: ClassType => ct.root
- case t => t
- }
-
def declareStructuralSort(t: Type): Z3Sort = {
- //println("///"*40)
- //println("Declaring for: "+t)
-
- adtManager.defineADT(t) match {
- case Left(adts) =>
- declareDatatypes(adts.toSeq)
- sorts(bestRealType(t))
-
- case Right(conflicts) =>
- conflicts.foreach { declareStructuralSort }
- declareStructuralSort(t)
- }
+ adtManager.declareADTs(t, declareDatatypes)
+ sorts(bestRealType(t))
}
def declareDatatypes(adts: Seq[(Type, DataType)]): Unit = {
@@ -137,7 +165,10 @@ trait AbstractZ3Solver extends AbstractSolver {
val indexMap: Map[Type, Int] = adts.map(_._1).zipWithIndex.toMap
def typeToSortRef(tt: Type): ADTSortReference = {
- val tpe = rootType(tt)
+ val tpe = tt match {
+ case ct: ClassType => ct.tcd.root.toType
+ case _ => tt
+ }
if (indexMap contains tpe) {
RecursiveType(indexMap(tpe))
@@ -177,14 +208,6 @@ trait AbstractZ3Solver extends AbstractSolver {
// Prepares some of the Z3 sorts, but *not* the tuple sorts; these are created on-demand.
private def prepareSorts(): Unit = {
- z3.mkADTSorts(
- Seq((
- "Unit",
- Seq("Unit"),
- Seq(Seq())
- ))
- )
-
//TODO: mkBitVectorType
sorts += Int32Type -> z3.mkBVSort(32)
sorts += CharType -> z3.mkBVSort(32)
@@ -198,17 +221,18 @@ trait AbstractZ3Solver extends AbstractSolver {
}
// assumes prepareSorts has been called....
- protected[leon] def typeToSort(oldtt: Type): Z3Sort = bestRealType(oldtt) match {
+ protected def typeToSort(oldtt: Type): Z3Sort = bestRealType(oldtt) match {
case Int32Type | BooleanType | IntegerType | RealType | CharType =>
sorts(oldtt)
- case tpe @ (_: ClassType | _: ArrayType | _: TupleType | _: TypeParameter | UnitType) =>
+ case tpe @ (_: ClassType | _: TupleType | _: TypeParameter | UnitType) =>
sorts.cached(tpe) {
declareStructuralSort(tpe)
}
case tt @ SetType(base) =>
sorts.cached(tt) {
+ declareStructuralSort(tt)
z3.mkSetSort(typeToSort(base))
}
@@ -217,6 +241,7 @@ trait AbstractZ3Solver extends AbstractSolver {
case tt @ MapType(from, to) =>
sorts.cached(tt) {
+ declareStructuralSort(tt)
val fromSort = typeToSort(from)
val toSort = typeToSort(to)
@@ -233,7 +258,7 @@ trait AbstractZ3Solver extends AbstractSolver {
unsupported(other)
}
- protected[leon] def toZ3Formula(expr: Expr, bindings: Map[Variable, Z3AST] = Map.empty): Z3AST = {
+ protected[z3] def toZ3Formula(expr: Expr, bindings: Map[Variable, Z3AST] = Map.empty): Z3AST = {
def rec(ex: Expr)(implicit bindings: Map[Variable, Z3AST]): Z3AST = ex match {
@@ -256,8 +281,8 @@ trait AbstractZ3Solver extends AbstractSolver {
case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r))
case Not(e) => z3.mkNot(rec(e))
case IntLiteral(v) => z3.mkInt(v, typeToSort(Int32Type))
- case InfiniteIntegerLiteral(v) => z3.mkNumeral(v.toString, typeToSort(IntegerType))
- case FractionalLiteral(n, d) => z3.mkNumeral(s"$n / $d", typeToSort(RealType))
+ case IntegerLiteral(v) => z3.mkNumeral(v.toString, typeToSort(IntegerType))
+ case FractionLiteral(n, d) => z3.mkNumeral(s"$n / $d", typeToSort(RealType))
case CharLiteral(c) => z3.mkInt(c, typeToSort(CharType))
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) )
@@ -355,7 +380,7 @@ trait AbstractZ3Solver extends AbstractSolver {
case c @ CaseClassSelector(cc, sel) =>
val cct = cc.getType
typeToSort(cct) // Making sure the sort is defined
- val selector = selectors.toB(cct, sel)
+ val selector = selectors.toB(cct -> c.selectorIndex)
selector(rec(cc))
case AsInstanceOf(expr, ct) =>
@@ -368,11 +393,11 @@ trait AbstractZ3Solver extends AbstractSolver {
rec(IsInstanceOf(e, tccd.toType))
case more =>
val v = Variable(FreshIdentifier("e", true), ct)
- rec(Let(v.toVal, e, orJoin(more map (IsInstanceOf(v, _)))))
+ rec(Let(v.toVal, e, orJoin(more map (tccd => IsInstanceOf(v, tccd.toType)))))
}
case tccd: TypedCaseClassDef =>
typeToSort(ct)
- val tester = tester.toB(ct)
+ val tester = testers.toB(ct)
tester(rec(e))
}
@@ -390,16 +415,28 @@ trait AbstractZ3Solver extends AbstractSolver {
}
z3.mkApp(funDecl, (caller +: args).map(rec): _*)
+ /**
+ * ===== Set operations =====
+ */
+ case f @ FiniteSet(elems, base) =>
+ elems.foldLeft(z3.mkEmptySet(typeToSort(base)))((ast, el) => z3.mkSetAdd(ast, rec(el)))
+
case ElementOfSet(e, s) => z3.mkSetMember(rec(e), rec(s))
+
case SubsetOf(s1, s2) => z3.mkSetSubset(rec(s1), rec(s2))
+
case SetIntersection(s1, s2) => z3.mkSetIntersect(rec(s1), rec(s2))
+
case SetUnion(s1, s2) => z3.mkSetUnion(rec(s1), rec(s2))
+
case SetDifference(s1, s2) => z3.mkSetDifference(rec(s1), rec(s2))
- case f @ FiniteSet(elems, base) => elems.foldLeft(z3.mkEmptySet(typeToSort(base)))((ast, el) => z3.mkSetAdd(ast, rec(el)))
+ /**
+ * ===== Bag operations =====
+ */
case fb @ FiniteBag(elems, base) =>
typeToSort(fb.getType)
- rec(FiniteMap(base, elems, IntegerLiteral(0)))
+ rec(FiniteMap(elems, IntegerLiteral(0), base))
case BagAdd(b, e) =>
val (bag, elem) = (rec(b), rec(e))
@@ -425,69 +462,35 @@ trait AbstractZ3Solver extends AbstractSolver {
val withNeg = z3.mkArrayMap(minus, rec(b1), rec(b2))
z3.mkArrayMap(div, z3.mkArrayMap(plus, withNeg, z3.mkArrayMap(abs, withNeg)), all2)
+ /**
+ * ===== Map operations =====
+ */
case al @ MapApply(a, i) =>
z3.mkSelect(rec(a), rec(i))
- case al @ RawArrayUpdated(a, i, e) =>
+ case al @ MapUpdated(a, i, e) =>
z3.mkStore(rec(a), rec(i), rec(e))
- case RawArrayValue(keyTpe, elems, default) =>
+
+ case FiniteMap(elems, default, keyTpe) =>
val ar = z3.mkConstArray(typeToSort(keyTpe), rec(default))
elems.foldLeft(ar) {
case (array, (k, v)) => z3.mkStore(array, rec(k), rec(v))
}
- /**
- * ===== Map operations =====
- */
- case m @ FiniteMap(elems, from, to) =>
- val MapType(_, t) = bestRealType(m.getType)
-
- rec(RawArrayValue(from, elems.map{
- case (k, v) => (k, CaseClass(library.someType(t), Seq(v)))
- }, CaseClass(library.noneType(t), Seq())))
-
- case MapApply(m, k) =>
- val mt @ MapType(_, t) = bestRealType(m.getType)
- typeToSort(mt)
-
- val el = z3.mkSelect(rec(m), rec(k))
-
- // Really ?!? We don't check that it is actually != None?
- selectors.toB(library.someType(t), 0)(el)
-
- case MapIsDefinedAt(m, k) =>
- val mt @ MapType(_, t) = bestRealType(m.getType)
- typeToSort(mt)
-
- val el = z3.mkSelect(rec(m), rec(k))
-
- testers.toB(library.someType(t))(el)
-
- case MapUnion(m1, FiniteMap(elems, _, _)) =>
- val mt @ MapType(_, t) = bestRealType(m1.getType)
- typeToSort(mt)
-
- elems.foldLeft(rec(m1)) { case (m, (k,v)) =>
- z3.mkStore(m, rec(k), rec(CaseClass(library.someType(t), Seq(v))))
- }
-
case gv @ GenericValue(tp, id) =>
typeToSort(tp)
val constructor = constructors.toB(tp)
- constructor(rec(InfiniteIntegerLiteral(id)))
-
- case synthesis.utils.MutableExpr(ex) =>
- rec(ex)
+ constructor(rec(IntegerLiteral(id)))
case other =>
unsupported(other)
}
- rec(expr)
+ rec(expr)(bindings)
}
- protected[leon] def fromZ3Formula(model: Z3Model, tree: Z3AST, tpe: Type): Expr = {
+ protected[z3] def fromZ3Formula(model: Z3Model, tree: Z3AST, tpe: Type): Expr = {
def rec(t: Z3AST, tpe: Type): Expr = {
val kind = z3.getASTKind(t)
@@ -500,7 +503,7 @@ trait AbstractZ3Solver extends AbstractSolver {
tpe match {
case Int32Type => IntLiteral(hexa.toInt)
case CharType => CharLiteral(hexa.toInt.toChar)
- case IntegerType => InfiniteIntegerLiteral(BigInt(hexa.toInt))
+ case IntegerType => IntegerLiteral(BigInt(hexa.toInt))
case other =>
unsupported(other, "Unexpected target type for BV value")
}
@@ -510,7 +513,7 @@ trait AbstractZ3Solver extends AbstractSolver {
tpe match {
case Int32Type => IntLiteral(v)
case CharType => CharLiteral(v.toChar)
- case IntegerType => InfiniteIntegerLiteral(BigInt(v))
+ case IntegerType => IntegerLiteral(BigInt(v))
case other =>
unsupported(other, "Unexpected type for BV value: " + other)
}
@@ -518,7 +521,6 @@ trait AbstractZ3Solver extends AbstractSolver {
case Z3NumeralIntAST(None) =>
val ts = t.toString
- reporter.ifDebug(printer => printer(ts))(DebugSectionSynthesis)
if(ts.length > 4 && ts.substring(0, 2) == "bv" && ts.substring(ts.length - 4) == "[32]") {
val integer = ts.substring(2, ts.length - 4)
tpe match {
@@ -526,7 +528,7 @@ trait AbstractZ3Solver extends AbstractSolver {
IntLiteral(integer.toLong.toInt)
case CharType => CharLiteral(integer.toInt.toChar)
case IntegerType =>
- InfiniteIntegerLiteral(BigInt(integer))
+ IntegerLiteral(BigInt(integer))
case _ =>
reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
}
@@ -542,7 +544,7 @@ trait AbstractZ3Solver extends AbstractSolver {
}
}
- case Z3NumeralRealAST(n: BigInt, d: BigInt) => FractionalLiteral(n, d)
+ case Z3NumeralRealAST(n: BigInt, d: BigInt) => FractionLiteral(n, d)
case Z3AppAST(decl, args) =>
val argsSize = args.size
@@ -551,11 +553,11 @@ trait AbstractZ3Solver extends AbstractSolver {
} else if(functions containsB decl) {
val tfd = functions.toA(decl)
assert(tfd.params.size == argsSize)
- FunctionInvocation(tfd, args.zip(tfd.params).map{ case (a, p) => rec(a, p.getType) })
+ FunctionInvocation(tfd.id, tfd.tps, args.zip(tfd.params).map{ case (a, p) => rec(a, p.getType) })
} else if (constructors containsB decl) {
constructors.toA(decl) match {
- case cct: CaseClassType =>
- CaseClass(cct, args.zip(cct.fieldsTypes).map { case (a, t) => rec(a, t) })
+ case ct: ClassType =>
+ CaseClass(ct, args.zip(ct.tcd.toCase.fieldsTypes).map { case (a, t) => rec(a, t) })
case UnitType =>
UnitLiteral()
@@ -563,29 +565,8 @@ trait AbstractZ3Solver extends AbstractSolver {
case TupleType(ts) =>
tupleWrap(args.zip(ts).map { case (a, t) => rec(a, t) })
- case ArrayType(to) =>
- val size = rec(args(0), Int32Type)
- val map = rec(args(1), RawArrayType(Int32Type, to))
-
- (size, map) match {
-
- case (s : IntLiteral, RawArrayValue(_, elems, default)) =>
-
- if (s.value < 0)
- unsupported(s, s"Z3 returned array of negative size")
-
- val entries = elems.map {
- case (IntLiteral(i), v) => i -> v
- case (e,_) => unsupported(e, s"Z3 returned unexpected array index ${e.asString}")
- }
-
- finiteArray(entries, Some(default, s), to)
- case (s : IntLiteral, arr) => unsound(args(1), "invalid array type")
- case (size, _) => unsound(args(0), "invalid array size")
- }
-
case tp @ TypeParameter(id) =>
- val InfiniteIntegerLiteral(n) = rec(args(0), IntegerType)
+ val IntegerLiteral(n) = rec(args(0), IntegerType)
GenericValue(tp, n.toInt)
case t =>
@@ -593,59 +574,47 @@ trait AbstractZ3Solver extends AbstractSolver {
}
} else {
tpe match {
- case RawArrayType(from, to) =>
- model.getArrayValue(t) match {
- case Some((z3map, z3default)) =>
- val default = rec(z3default, to)
- val entries = z3map.map {
- case (k,v) => (rec(k, from), rec(v, to))
- }
-
- RawArrayValue(from, entries, default)
- case None => unsound(t, "invalid array AST")
- }
-
case ft @ FunctionType(fts, tt) => lambdas.getB(ft) match {
case None => simplestValue(ft)
case Some(decl) => model.getFuncInterpretations.find(_._1 == decl) match {
case None => simplestValue(ft)
case Some((_, mapping, elseValue)) =>
- val leonElseValue = rec(elseValue, tt)
- FiniteLambda(mapping.flatMap { case (z3Args, z3Result) =>
+ val args = fts.map(tpe => ValDef(FreshIdentifier("x", true), tpe))
+ val body = mapping.foldLeft(rec(elseValue, tt)) { case (elze, (z3Args, z3Result)) =>
if (t == z3Args.head) {
- List((z3Args.tail zip fts).map(p => rec(p._1, p._2)) -> rec(z3Result, tt))
+ val cond = andJoin((args zip z3Args.tail).map { case (vd, z3Arg) =>
+ Equals(vd.toVariable, rec(z3Arg, vd.tpe))
+ })
+
+ IfExpr(cond, rec(z3Result, tt), elze)
} else {
- Nil
+ elze
}
- }, leonElseValue, ft)
+ }
+
+ Lambda(args, body)
}
}
case MapType(from, to) =>
- rec(t, RawArrayType(from, library.optionType(to))) match {
- case r: RawArrayValue =>
- // We expect a RawArrayValue with keys in from and values in Option[to],
- // with default value == None
- if (r.default.getType != library.noneType(to)) {
- unsupported(r, "Solver returned a co-finite map which is not supported.")
- }
- require(r.keyTpe == from, s"Type error in solver model, expected ${from.asString}, found ${r.keyTpe.asString}")
-
- val elems = r.elems.flatMap {
- case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
- case (k, _) => None
+ model.getArrayValue(t) match {
+ case Some((z3map, z3default)) =>
+ val default = rec(z3default, to)
+ val entries = z3map.map {
+ case (k,v) => (rec(k, from), rec(v, to))
}
- FiniteMap(elems, from, to)
+ FiniteMap(entries.toSeq, default, from)
+ case None => unsound(t, "invalid array AST")
}
case BagType(base) =>
- val r @ RawArrayValue(_, elems, default) = rec(t, RawArrayType(base, IntegerType))
- if (default != InfiniteIntegerLiteral(0)) {
- unsupported(r, "Solver returned a co-finite bag which is not supported.")
+ val fm @ FiniteMap(entries, default, from) = rec(t, MapType(base, IntegerType))
+ if (default != IntegerLiteral(0)) {
+ unsound(t, "co-finite bag AST")
}
- FiniteBag(elems, base)
+ FiniteBag(entries, base)
case tpe @ SetType(dt) =>
model.getSetValue(t) match {
@@ -653,7 +622,7 @@ trait AbstractZ3Solver extends AbstractSolver {
case Some((_, false)) => unsound(t, "co-finite set AST")
case Some((set, true)) =>
val elems = set.map(e => rec(e, dt))
- FiniteSet(elems, dt)
+ FiniteSet(elems.toSeq, dt)
}
case _ =>
@@ -696,7 +665,7 @@ trait AbstractZ3Solver extends AbstractSolver {
rec(tree, bestRealType(tpe))
}
- protected[leon] def softFromZ3Formula(model: Z3Model, tree: Z3AST, tpe: Type) : Option[Expr] = {
+ protected[z3] def softFromZ3Formula(model: Z3Model, tree: Z3AST, tpe: Type) : Option[Expr] = {
try {
Some(fromZ3Formula(model, tree, tpe))
} catch {
@@ -710,8 +679,50 @@ trait AbstractZ3Solver extends AbstractSolver {
z3.mkFreshConst(v.id.uniqueName, typeToSort(v.getType))
}
- def reset(): Unit = {
- throw new CantResetException(this)
+ def assertCnstr(ast: Z3AST): Unit = solver.assertCnstr(ast)
+
+ private def extractResult(config: Configuration)(res: Option[Boolean]) = config.cast(res match {
+ case Some(true) =>
+ if (config.withModel) SatWithModel(solver.getModel)
+ else Sat
+
+ case Some(false) =>
+ if (config.withCores) UnsatWithCores(solver.getUnsatCore.toSet)
+ else Unsat
+
+ case None => Unknown
+ })
+
+ def check(config: Configuration) = extractResult(config)(solver.check)
+ def checkAssumptions(config: Configuration)(assumptions: Set[Z3AST]) =
+ extractResult(config)(solver.checkAssumptions(assumptions.toSeq : _*))
+
+ def extractModel(model: Z3Model): Map[ValDef, Expr] = variables.aToB.flatMap {
+ case (v,z3ID) => (v.getType match {
+ case BooleanType =>
+ model.evalAs[Boolean](z3ID).map(BooleanLiteral)
+
+ case Int32Type =>
+ model.evalAs[Int](z3ID).map(IntLiteral(_)).orElse {
+ model.eval(z3ID).flatMap(t => softFromZ3Formula(model, t, Int32Type))
+ }
+
+ case IntegerType =>
+ model.evalAs[Int](z3ID).map(i => IntegerLiteral(BigInt(i)))
+
+ case other => model.eval(z3ID).flatMap(t => softFromZ3Formula(model, t, other))
+ }).map(v.toVal -> _)
}
+ def extractCores(cores: Set[Z3AST]): Set[Expr] = {
+ cores.flatMap { c =>
+ variables.getA(c).orElse(z3.getASTKind(c) match {
+ case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
+ case OpNot => variables.getA(args.head)
+ case _ => None
+ }
+ case ast => None
+ })
+ }
+ }
}
diff --git a/src/main/scala/inox/solvers/z3/FairZ3Solver.scala b/src/main/scala/inox/solvers/z3/FairZ3Solver.scala
deleted file mode 100644
index 5223f915a..000000000
--- a/src/main/scala/inox/solvers/z3/FairZ3Solver.scala
+++ /dev/null
@@ -1,199 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package inox
-package solvers
-package z3
-
-import _root_.z3.scala._
-
-import unrolling._
-import theories._
-import utils._
-
-trait FairZ3Solver
- extends AbstractZ3Solver
- with AbstractUnrollingSolver {
-
- import program._
- import program.trees._
- import program.symbols._
-
- override val name = "Z3-f"
- override val description = "Fair Z3 Solver"
-
- type Encoded = Z3AST
- val printable = (z3: Z3AST) => new Printable {
- def asString(implicit ctx: LeonContext) = z3.toString
- }
-
- object theories extends {
- val trees: program.trees.type = program.trees
- } with StringEncoder
-
- object templates extends {
- val program: FairZ3Solver.this.program.type = FairZ3Solver.this.program
- type Encoded = FairZ3Solver.this.Encoded
- } with Templates {
-
- def encodeSymbol(v: Variable): Z3AST = symbolToFreshZ3Symbol(v)
-
- def encodeExpr(bindings: Map[Variable, Z3AST])(e: Expr): Z3AST = {
- toZ3Formula(e, bindings)
- }
-
- def substitute(substMap: Map[Z3AST, Z3AST]): Z3AST => Z3AST = {
- val (from, to) = substMap.unzip
- val (fromArray, toArray) = (from.toArray, to.toArray)
-
- (c: Z3AST) => z3.substitute(c, fromArray, toArray)
- }
-
- def mkNot(e: Z3AST) = z3.mkNot(e)
- def mkOr(es: Z3AST*) = z3.mkOr(es : _*)
- def mkAnd(es: Z3AST*) = z3.mkAnd(es : _*)
- def mkEquals(l: Z3AST, r: Z3AST) = z3.mkEq(l, r)
- def mkImplies(l: Z3AST, r: Z3AST) = z3.mkImplies(l, r)
-
- def extractNot(l: Z3AST): Option[Z3AST] = z3.getASTKind(l) match {
- case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
- case OpNot => Some(args.head)
- case _ => None
- }
- case ast => None
- }
- }
-
- override def reset(): Unit = super[AbstractZ3Solver].reset()
-
- def declareVariable(v: Variable): Z3AST = variables.cachedB(v) {
- templates.encodeSymbol(v)
- }
-
- def solverAssert(cnstr: Z3AST): Unit = {
- val timer = context.timers.solvers.z3.assert.start()
- solver.assertCnstr(cnstr)
- timer.stop()
- }
-
- def solverCheck[R](config: Configuration)
- (clauses: Seq[Z3AST])
- (block: Response => R): R = {
- solver.push()
- for (cls <- clauses) solver.assertCnstr(cls)
- val res = solver.check
- val r = block(res)
- solver.pop()
- r
- }
-
- override def solverCheckAssumptions[R](assumptions: Seq[Z3AST])(block: Option[Boolean] => R): R = {
- solver.push() // FIXME: remove when z3 bug is fixed
- val res = solver.checkAssumptions(assumptions : _*)
- solver.pop() // FIXME: remove when z3 bug is fixed
- block(res)
- }
-
- def solverGetModel: ModelWrapper = new ModelWrapper {
- val model: Z3Model = solver.getModel
-
- /*
- val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
- val functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
- if (functions containsB p._1) {
- val tfd = functions.toA(p._1)
- if (!tfd.hasImplementation) {
- val (cses, default) = p._2
- val ite = cses.foldLeft(fromZ3Formula(model, default, tfd.returnType))((expr, q) => IfExpr(
- andJoin(q._1.zip(tfd.params).map(a12 => Equals(fromZ3Formula(model, a12._1, a12._2.getType), Variable(a12._2.id)))),
- fromZ3Formula(model, q._2, tfd.returnType),
- expr))
- Seq((tfd.id, ite))
- } else Seq()
- } else Seq()
- })
-
- val constantFunctionsAsMap: Map[Identifier, Expr] = model.getModelConstantInterpretations.flatMap(p => {
- if(functions containsB p._1) {
- val tfd = functions.toA(p._1)
- if(!tfd.hasImplementation) {
- Seq((tfd.id, fromZ3Formula(model, p._2, tfd.returnType)))
- } else Seq()
- } else Seq()
- }).toMap
-
- val leonModel = extractModel(model, freeVars.toSet)
- val fullModel = leonModel ++ (functionsAsMap ++ constantFunctionsAsMap)
- */
-
- def modelEval(elem: Z3AST, tpe: TypeTree): Option[Expr] = {
- val timer = context.timers.solvers.z3.eval.start()
- val res = tpe match {
- case BooleanType => model.evalAs[Boolean](elem).map(BooleanLiteral)
- case Int32Type => model.evalAs[Int](elem).map(IntLiteral).orElse {
- model.eval(elem).flatMap(t => softFromZ3Formula(model, t, Int32Type))
- }
- case IntegerType => model.evalAs[Int](elem).map(InfiniteIntegerLiteral(_))
- case other => model.eval(elem) match {
- case None => None
- case Some(t) => softFromZ3Formula(model, t, other)
- }
- }
- timer.stop()
- res
- }
-
- override def toString = model.toString
- }
-
- private val incrementals: List[IncrementalState] = List(
- errors, functions, lambdas, sorts, variables,
- constructors, selectors, testers
- )
-
- override def push(): Unit = {
- super.push()
- solver.push()
- incrementals.foreach(_.push())
- }
-
- override def pop(): Unit = {
- super.pop()
- solver.pop(1)
- incrementals.foreach(_.pop())
- }
-
- override def check: Option[Boolean] = {
- if (hasError) {
- None
- } else {
- super.check
- }
- }
-
- override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
- if (hasError) {
- None
- } else {
- super.checkAssumptions(assumptions)
- }
- }
-
- def solverUnsatCore = Some(solver.getUnsatCore)
-
- override def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
- super.foundAnswer(res, model, core)
-
- if (!interrupted && res.isEmpty && model.isEmpty) {
- reporter.ifDebug { debug =>
- if (solver.getReasonUnknown != "canceled") {
- debug("Z3 returned unknown: " + solver.getReasonUnknown)
- }
- }
- }
- }
-
- override def interrupt(): Unit = {
- super[AbstractZ3Solver].interrupt()
- super[AbstractUnrollingSolver].interrupt()
- }
-}
diff --git a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
new file mode 100644
index 000000000..ae3e08eed
--- /dev/null
+++ b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
@@ -0,0 +1,114 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers.z3
+
+import utils._
+import solvers.{z3 => _, _}
+import unrolling._
+import theories._
+
+import z3.scala._
+
+trait NativeZ3Solver
+ extends AbstractUnrollingSolver {
+
+ import program._
+ import program.trees._
+ import program.symbols._
+
+ override val name = "NativeZ3"
+
+ type Encoded = Z3AST
+
+ object theories extends {
+ val sourceProgram: program.type = program
+ } with StringEncoder
+
+ protected object underlying extends {
+ val program: theories.targetProgram.type = theories.targetProgram
+ val options = NativeZ3Solver.this.options
+ } with AbstractZ3Solver
+
+ private lazy val z3 = underlying.z3
+
+ object templates extends {
+ val program: theories.targetProgram.type = theories.targetProgram
+ } with Templates {
+ type Encoded = NativeZ3Solver.this.Encoded
+
+ def asString(ast: Z3AST): String = ast.toString
+
+ def encodeSymbol(v: Variable): Z3AST = underlying.symbolToFreshZ3Symbol(v)
+
+ def mkEncoder(bindings: Map[Variable, Z3AST])(e: Expr): Z3AST = {
+ underlying.toZ3Formula(e, bindings)
+ }
+
+ def mkSubstituter(substMap: Map[Z3AST, Z3AST]): Z3AST => Z3AST = {
+ val (from, to) = substMap.unzip
+ val (fromArray, toArray) = (from.toArray, to.toArray)
+
+ (c: Z3AST) => z3.substitute(c, fromArray, toArray)
+ }
+
+ def mkNot(e: Z3AST) = z3.mkNot(e)
+ def mkOr(es: Z3AST*) = z3.mkOr(es : _*)
+ def mkAnd(es: Z3AST*) = z3.mkAnd(es : _*)
+ def mkEquals(l: Z3AST, r: Z3AST) = z3.mkEq(l, r)
+ def mkImplies(l: Z3AST, r: Z3AST) = z3.mkImplies(l, r)
+
+ def extractNot(l: Z3AST): Option[Z3AST] = z3.getASTKind(l) match {
+ case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
+ case OpNot => Some(args.head)
+ case _ => None
+ }
+ case ast => None
+ }
+ }
+
+ override def reset(): Unit = {
+ super.reset()
+ underlying.reset()
+ }
+
+ protected def declareVariable(v: Variable): Z3AST = underlying.declareVariable(v)
+
+ protected def wrapModel(model: Z3Model): super.ModelWrapper = ModelWrapper(model)
+
+ private case class ModelWrapper(model: Z3Model) extends super.ModelWrapper {
+ def modelEval(elem: Z3AST, tpe: Type): Option[Expr] = {
+ val timer = ctx.timers.solvers.z3.eval.start()
+ val res = tpe match {
+ case BooleanType => model.evalAs[Boolean](elem).map(BooleanLiteral)
+ case Int32Type => model.evalAs[Int](elem).map(IntLiteral(_)).orElse {
+ model.eval(elem).flatMap(t => underlying.softFromZ3Formula(model, t, Int32Type))
+ }
+ case IntegerType => model.evalAs[Int](elem).map(IntegerLiteral(_))
+ case other => model.eval(elem) match {
+ case None => None
+ case Some(t) => underlying.softFromZ3Formula(model, t, other)
+ }
+ }
+ timer.stop()
+ res
+ }
+
+ override def toString = model.toString
+ }
+
+ override def push(): Unit = {
+ super.push()
+ underlying.push()
+ }
+
+ override def pop(): Unit = {
+ super.pop()
+ underlying.pop()
+ }
+
+ override def interrupt(): Unit = {
+ underlying.interrupt()
+ super.interrupt()
+ }
+}
diff --git a/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
index 88031219a..249f08ad7 100644
--- a/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
@@ -1,20 +1,13 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
package solvers.z3
import z3.scala._
-import leon.solvers._
+import solvers._
import utils.IncrementalSet
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.Extractors._
-import purescala.ExprOps._
-import purescala.Types._
-
/** This is a rather direct mapping to Z3, where all functions are left uninterpreted.
* It reports the results as follows (based on the negation of the formula):
* - if Z3 reports UNSAT, it reports VALID
@@ -22,46 +15,56 @@ import purescala.Types._
* - otherwise it returns UNKNOWN
* Results should come back very quickly.
*/
-class UninterpretedZ3Solver(val sctx: SolverContext, val program: Program)
- extends AbstractZ3Solver
- with Z3ModelReconstruction {
+trait UninterpretedZ3Solver
+ extends Solver { self =>
+
+ import program._
+ import program.trees._
+ import program.symbols._
+
+ import SolverResponses._
val name = "Z3-u"
val description = "Uninterpreted Z3 Solver"
- def push() {
- solver.push()
- freeVariables.push()
+ private object underlying extends {
+ val program: self.program.type = self.program
+ val options = self.options
+ } with AbstractZ3Solver
+
+ private val freeVars = new IncrementalSet[Variable]
+
+ def push(): Unit = {
+ underlying.push()
+ freeVars.push()
}
- def pop() {
- solver.pop(1)
- freeVariables.pop()
+ def pop(): Unit = {
+ underlying.pop()
+ freeVars.pop()
}
- private val freeVariables = new IncrementalSet[Identifier]()
+ def reset(): Unit = {
+ underlying.reset()
+ freeVars.reset()
+ }
def assertCnstr(expression: Expr) {
- freeVariables ++= variablesOf(expression)
- solver.assertCnstr(toZ3Formula(expression))
+ freeVars ++= exprOps.variablesOf(expression)
+ underlying.assertCnstr(underlying.toZ3Formula(expression))
}
- override def check: Option[Boolean] = solver.check()
+ private def completeModel(model: Map[ValDef, Expr]): Map[ValDef, Expr] =
+ freeVars.map(v => v.toVal -> model.getOrElse(v.toVal, simplestValue(v.getType))).toMap
- override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
- freeVariables ++= assumptions.flatMap(variablesOf)
- solver.checkAssumptions(assumptions.toSeq.map(toZ3Formula(_)) : _*)
- }
+ def check(config: Configuration): config.Response[Model, Cores] =
+ config.convert(underlying.check(config),
+ (model: Z3Model) => completeModel(underlying.extractModel(model)),
+ underlying.extractCores)
- def getModel = {
- new Model(modelToMap(solver.getModel(), freeVariables.toSet))
- }
-
- def getUnsatCore = {
- solver.getUnsatCore().map(ast => fromZ3Formula(null, ast, BooleanType) match {
- case n @ Not(Variable(_)) => n
- case v @ Variable(_) => v
- case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
- }).toSet
- }
+ override def checkAssumptions(config: Configuration)
+ (assumptions: Set[Expr]): config.Response[Model, Cores] =
+ config.convert(underlying.checkAssumptions(config)(assumptions.map(underlying.toZ3Formula(_))),
+ (model: Z3Model) => completeModel(underlying.extractModel(model)),
+ underlying.extractCores)
}
diff --git a/src/main/scala/inox/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/inox/solvers/z3/Z3ModelReconstruction.scala
deleted file mode 100644
index a626199f1..000000000
--- a/src/main/scala/inox/solvers/z3/Z3ModelReconstruction.scala
+++ /dev/null
@@ -1,70 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers.z3
-
-import z3.scala._
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Constructors._
-import purescala.ExprOps._
-import purescala.Types._
-
-trait Z3ModelReconstruction {
- self: AbstractZ3Solver =>
-
- // exprToZ3Id, softFromZ3Formula, reporter
-
- private final val AUTOCOMPLETEMODELS : Boolean = true
-
- def modelValue(model: Z3Model, id: Identifier, tpe: TypeTree = null) : Option[Expr] = {
- val expectedType = if(tpe == null) id.getType else tpe
-
- variables.getB(id.toVariable).flatMap { z3ID =>
- expectedType match {
- case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral)
- case Int32Type =>
- model.evalAs[Int](z3ID).map(IntLiteral).orElse{
- model.eval(z3ID).flatMap(t => softFromZ3Formula(model, t, Int32Type))
- }
- case IntegerType => model.evalAs[Int](z3ID).map(InfiniteIntegerLiteral(_))
- case other => model.eval(z3ID) match {
- case None => None
- case Some(t) => softFromZ3Formula(model, t, other)
- }
- }
- }
- }
-
- def modelToMap(model: Z3Model, ids: Iterable[Identifier]) : Map[Identifier,Expr] = {
- var asMap = Map.empty[Identifier,Expr]
-
- def completeID(id : Identifier) : Unit = {
- asMap = asMap + (id -> simplestValue(id.getType))
- reporter.debug("Completing variable '" + id + "' to simplest value")
- }
-
- for (id <- ids) {
- modelValue(model, id) match {
- case None if AUTOCOMPLETEMODELS => completeID(id)
- case None => ;
- case Some(v @ Variable(exprId)) if AUTOCOMPLETEMODELS && exprId == id => completeID(id)
- case Some(ex) => asMap = asMap + (id -> ex)
- }
- }
-
- asMap
- }
-
- def printExtractedModel(model: Z3Model, ids : Iterable[Identifier]) : Unit = {
- reporter.info("Tentative extracted model")
- reporter.info("*************************")
- for(id <- ids) {
- val strRep = modelValue(model, id) match {
- case Some(e) => e.toString
- case None => "??"
- }
- reporter.info(id + " -> " + strRep)
- }
- }
-}
diff --git a/src/main/scala/inox/solvers/z3/Z3Solver.scala b/src/main/scala/inox/solvers/z3/Z3Solver.scala
deleted file mode 100644
index a3648904a..000000000
--- a/src/main/scala/inox/solvers/z3/Z3Solver.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package inox
-package solvers
-package z3
-
-trait Z3Solver extends Solver
diff --git a/src/main/scala/inox/utils/IncrementalStateWrapper.scala b/src/main/scala/inox/utils/IncrementalStateWrapper.scala
index ea7628ae3..54bc56a22 100644
--- a/src/main/scala/inox/utils/IncrementalStateWrapper.scala
+++ b/src/main/scala/inox/utils/IncrementalStateWrapper.scala
@@ -3,7 +3,7 @@
package inox.utils
trait IncrementalStateWrapper extends IncrementalState {
- val incrementals: Seq[IncrementalState]
+ protected val incrementals: Seq[IncrementalState]
def push(): Unit = incrementals.foreach(_.push())
def pop(): Unit = incrementals.foreach(_.pop())
diff --git a/src/main/scala/inox/utils/SCC.scala b/src/main/scala/inox/utils/SCC.scala
index 06f090a9e..3c1e62a39 100644
--- a/src/main/scala/inox/utils/SCC.scala
+++ b/src/main/scala/inox/utils/SCC.scala
@@ -5,9 +5,7 @@ package utils
/** Returns the list of strongly connected sets of vertices.
* A set is said strongly connected is from any vertex we can reach another vertex transitively.
- *
- * This could be defined anywhere, it's just that the
- * termination checker is the only place where it is used. */
+ */
object SCC {
def scc[T](graph: Map[T,Set[T]]) : List[Set[T]] = {
// The first part is a shameless adaptation from Wikipedia
@@ -54,6 +52,6 @@ object SCC {
}
}
- components
+ components.reverse
}
}
--
GitLab