From a80dd23df7375e4f148b0c8a0f33d1648fcf41c3 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 26 Oct 2012 18:04:10 +0200
Subject: [PATCH] Refactoring of solvers.
---
src/main/scala/leon/AbstractZ3Solver.scala | 97 ---
src/main/scala/leon/Analysis.scala | 4 +
src/main/scala/leon/Extensions.scala | 8 +-
.../leon/{ => solvers}/ParallelSolver.scala | 1 +
.../leon/{ => solvers}/RandomSolver.scala | 1 +
.../leon/{ => solvers}/TimeoutSolver.scala | 1 +
.../leon/{ => solvers}/TrivialSolver.scala | 3 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 765 ++++++++++++++++++
.../leon/{ => solvers/z3}/FairZ3Solver.scala | 536 +-----------
.../z3}/Z3ModelReconstruction.scala | 1 +
.../scala/leon/synthesis/SynthesisPhase.scala | 3 +
src/main/scala/leon/testgen/CallGraph.scala | 2 +-
.../scala/leon/testgen/TestGeneration.scala | 2 +-
13 files changed, 791 insertions(+), 633 deletions(-)
delete mode 100644 src/main/scala/leon/AbstractZ3Solver.scala
rename src/main/scala/leon/{ => solvers}/ParallelSolver.scala (99%)
rename src/main/scala/leon/{ => solvers}/RandomSolver.scala (99%)
rename src/main/scala/leon/{ => solvers}/TimeoutSolver.scala (97%)
rename src/main/scala/leon/{ => solvers}/TrivialSolver.scala (91%)
create mode 100644 src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
rename src/main/scala/leon/{ => solvers/z3}/FairZ3Solver.scala (63%)
rename src/main/scala/leon/{ => solvers/z3}/Z3ModelReconstruction.scala (99%)
diff --git a/src/main/scala/leon/AbstractZ3Solver.scala b/src/main/scala/leon/AbstractZ3Solver.scala
deleted file mode 100644
index 5c1fc48fa..000000000
--- a/src/main/scala/leon/AbstractZ3Solver.scala
+++ /dev/null
@@ -1,97 +0,0 @@
-package leon
-
-import z3.scala._
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.TypeTrees._
-import Extensions._
-
-import scala.collection.mutable.{Map => MutableMap}
-import scala.collection.mutable.{Set => MutableSet}
-
-// This is just to factor out the things that are common in "classes that deal
-// with a Z3 instance"
-trait AbstractZ3Solver {
- self: Solver =>
-
- val reporter: Reporter
-
- class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t)
-
- protected[leon] var z3 : Z3Context
- protected[leon] var program : Program
-
- def typeToSort(tt: TypeTree): Z3Sort
- protected[leon] var adtTesters: Map[CaseClassDef, Z3FuncDecl]
- protected[leon] var adtConstructors: Map[CaseClassDef, Z3FuncDecl]
- protected[leon] var adtFieldSelectors: Map[Identifier, Z3FuncDecl]
-
- protected[leon] val mapRangeSorts: MutableMap[TypeTree, Z3Sort]
- protected[leon] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl]
- protected[leon] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl]
- protected[leon] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl]
- protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl]
- protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl]
-
- protected[leon] var funSorts: Map[TypeTree, Z3Sort]
- protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl]
- protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]]
-
- protected[leon] var exprToZ3Id : Map[Expr,Z3AST]
- protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree]) : Expr
-
- protected[leon] def softFromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: TypeTree) : Option[Expr] = {
- try {
- Some(fromZ3Formula(model, tree, Some(expectedType)))
- } catch {
- case e: CantTranslateException => None
- }
- }
-
- protected[leon] def solveWithBounds(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr])
-
- protected[leon] def boundValues : Unit = {
- val lowerBound: Z3AST = z3.mkInt(Settings.testBounds._1, z3.mkIntSort)
- val upperBound: Z3AST = z3.mkInt(Settings.testBounds._2, z3.mkIntSort)
-
- def isUnbounded(field: VarDecl) : Boolean = field.getType match {
- case Int32Type => true
- case _ => false
- }
-
- def boundConstraint(boundVar: Z3AST) : Z3AST = {
- z3.mkAnd(z3.mkLE(lowerBound, boundVar), z3.mkLE(boundVar, upperBound))
- }
-
- // for all recursive type roots
- // for all child ccd of a root
- // if ccd contains unbounded types
- // create bound vars (mkBound) for each field
- // create pattern that says (valueBounds(ccd(f1, ..)))
- // create axiom tree that says "values of unbounded types are within bounds"
- // assert axiom for the tree above
-
- val roots = program.classHierarchyRoots
- for (root <- roots) {
- val children: List[CaseClassDef] = (root match {
- case c: CaseClassDef => List(c)
- case a: AbstractClassDef => a.knownChildren.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef]).toList
- })
- for (child <- children) child match {
- case CaseClassDef(id, parent, fields) =>
- val unboundedFields = fields.filter(isUnbounded(_))
- if (!unboundedFields.isEmpty) {
- val boundVars = fields.zipWithIndex.map{case (f, i) => z3.mkBound(i, typeToSort(f.getType))}
- val term = adtConstructors(child)(boundVars : _*)
- val pattern = z3.mkPattern(term)
- //val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(p._2)).foldLeft(z3.mkTrue)((a, b) => a && b)
- val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(adtFieldSelectors(p._1.id)(term))).foldLeft(z3.mkTrue)((a, b) => z3.mkAnd(a, b))
- val axiom = z3.mkForAll(0, List(pattern), fields.zipWithIndex.map{case (f, i) => (z3.mkIntSymbol(i), typeToSort(f.getType))}, constraint)
- //println("Asserting: " + axiom)
- z3.assertCnstr(axiom)
- }
- }
- }
- }
-}
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 62ea2a39b..e1fc9fb1f 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -5,7 +5,11 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
+
import Extensions._
+
+import solvers.TrivialSolver
+
import scala.collection.mutable.{Set => MutableSet}
class Analysis(val program : Program, val reporter: Reporter = Settings.reporter) {
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 1d6bb8198..4b54a3855 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -95,7 +95,7 @@ object Extensions {
}
// these extensions are always loaded, unless specified otherwise
val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) {
- val z3 : Solver = new FairZ3Solver(extensionsReporter)
+ val z3 : Solver = new solvers.z3.FairZ3Solver(extensionsReporter)
z3 :: Nil
} else {
Nil
@@ -106,14 +106,14 @@ object Extensions {
//analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
- val solverExtensions1 = if(Settings.useQuickCheck) new RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
- val solverExtensions2 = if(Settings.useParallel) Seq(new ParallelSolver(solverExtensions1: _*)) else solverExtensions1
+ val solverExtensions1 = if(Settings.useQuickCheck) new solvers.RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
+ val solverExtensions2 = if(Settings.useParallel) Seq(new solvers.ParallelSolver(solverExtensions1: _*)) else solverExtensions1
val solverExtensions3 =
if(Settings.solverTimeout == None) {
solverExtensions2
} else {
val t = Settings.solverTimeout.get
- solverExtensions2.map(s => new TimeoutSolver(s, t))
+ solverExtensions2.map(s => new solvers.TimeoutSolver(s, t))
}
solverExtensions = solverExtensions3
loaded
diff --git a/src/main/scala/leon/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
similarity index 99%
rename from src/main/scala/leon/ParallelSolver.scala
rename to src/main/scala/leon/solvers/ParallelSolver.scala
index 1a3e1d7c4..9a9e39829 100644
--- a/src/main/scala/leon/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -1,4 +1,5 @@
package leon
+package solvers
import purescala.Common._
import purescala.Definitions._
diff --git a/src/main/scala/leon/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
similarity index 99%
rename from src/main/scala/leon/RandomSolver.scala
rename to src/main/scala/leon/solvers/RandomSolver.scala
index 778a44e59..89c0c6752 100644
--- a/src/main/scala/leon/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -1,4 +1,5 @@
package leon
+package solvers
import purescala.Common._
import purescala.Definitions._
diff --git a/src/main/scala/leon/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
similarity index 97%
rename from src/main/scala/leon/TimeoutSolver.scala
rename to src/main/scala/leon/solvers/TimeoutSolver.scala
index 1785aec5e..6b08a36f7 100644
--- a/src/main/scala/leon/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -1,4 +1,5 @@
package leon
+package solvers
import purescala.Common._
import purescala.Definitions._
diff --git a/src/main/scala/leon/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
similarity index 91%
rename from src/main/scala/leon/TrivialSolver.scala
rename to src/main/scala/leon/solvers/TrivialSolver.scala
index 0b05bbb59..054ae3f93 100644
--- a/src/main/scala/leon/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -1,6 +1,6 @@
package leon
+package solvers
-import z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
@@ -16,6 +16,7 @@ class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
case Not(BooleanLiteral(v)) => Some(!v)
case Or(exs) if exs.contains(BooleanLiteral(true)) => Some(true)
case And(exs) if exs.contains(BooleanLiteral(false)) => Some(false)
+ case Equals(l,r) if l == r => Some(true)
case _ => None
}
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
new file mode 100644
index 000000000..a2a78f952
--- /dev/null
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -0,0 +1,765 @@
+package leon
+package solvers.z3
+
+import z3.scala._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import Extensions._
+
+import scala.collection.mutable.{Map => MutableMap}
+import scala.collection.mutable.{Set => MutableSet}
+
+// This is just to factor out the things that are common in "classes that deal
+// with a Z3 instance"
+trait AbstractZ3Solver {
+ self: Solver =>
+
+ val reporter: Reporter
+
+ protected[leon] val USEBV : Boolean = Settings.bitvectorBitwidth.isDefined
+ protected[leon] val BVWIDTH : Int = Settings.bitvectorBitwidth.getOrElse(-1)
+
+ class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t)
+
+ protected[leon] var z3 : Z3Context = null
+ protected[leon] var program : Program = null
+ protected[leon] val z3cfg : Z3Config
+
+ override def setProgram(prog: Program): Unit = {
+ program = prog
+ }
+
+ protected[leon] def prepareFunctions : Unit
+ protected[leon] def functionDefToDecl(funDef: FunDef) : Z3FuncDecl
+ protected[leon] def functionDeclToDef(decl: Z3FuncDecl) : FunDef
+ protected[leon] def isKnownDecl(decl: Z3FuncDecl) : Boolean
+
+ // Lifting of common parts starts here
+ protected[leon] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty
+ protected[leon] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty
+
+ protected[leon] var intSort: Z3Sort = null
+ protected[leon] var boolSort: Z3Sort = null
+ protected[leon] var setSorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var unitSort: Z3Sort = null
+ protected[leon] var unitValue: Z3AST = null
+
+ protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
+
+ protected[leon] var tupleSorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var tupleConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var tupleSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
+
+ protected[leon] var arraySorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var arrayTupleCons: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var arrayTupleSelectorArray: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var arrayTupleSelectorLength: Map[TypeTree, Z3FuncDecl] = Map.empty
+
+ protected[leon] var reverseTupleConstructors: Map[Z3FuncDecl, TupleType] = Map.empty
+ protected[leon] var reverseTupleSelectors: Map[Z3FuncDecl, (TupleType, Int)] = Map.empty
+
+ protected[leon] var intSetMinFun: Z3FuncDecl = null
+ protected[leon] var intSetMaxFun: Z3FuncDecl = null
+ protected[leon] var setCardFuns: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var adtSorts: Map[ClassTypeDef, Z3Sort] = Map.empty
+ protected[leon] var fallbackSorts: Map[TypeTree, Z3Sort] = Map.empty
+
+ protected[leon] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
+ protected[leon] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
+ protected[leon] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
+
+ protected[leon] var reverseADTTesters: Map[Z3FuncDecl, CaseClassDef] = Map.empty
+ protected[leon] var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
+ protected[leon] var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty
+
+ protected[leon] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
+ protected[leon] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+
+ private var neverInitialized = true
+ private var counter = 0
+ private object nextIntForSymbol {
+ def apply(): Int = {
+ val res = counter
+ counter = counter + 1
+ res
+ }
+ }
+
+ protected[leon] def restartZ3 : Unit = {
+ counter = 0
+ if (neverInitialized) {
+ neverInitialized = false
+ } else {
+ z3.delete
+ }
+ z3 = new Z3Context(z3cfg)
+
+ exprToZ3Id = Map.empty
+ z3IdToExpr = Map.empty
+
+ fallbackSorts = Map.empty
+
+ mapSorts = Map.empty
+ arraySorts = Map.empty
+ funSorts = Map.empty
+ funDomainConstructors = Map.empty
+ funDomainSelectors = Map.empty
+
+ tupleSorts = Map.empty
+ tupleConstructors = Map.empty
+ tupleSelectors = Map.empty
+
+ mapRangeSorts.clear
+ mapRangeSomeConstructors.clear
+ mapRangeNoneConstructors.clear
+ mapRangeSomeTesters.clear
+ mapRangeNoneTesters.clear
+ mapRangeValueSelectors.clear
+
+ prepareSorts
+
+ prepareFunctions
+ }
+ protected[leon] def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
+ case Some(z3sort) => z3sort
+ case None => {
+ import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
+ intSort = if(USEBV) {
+ z3.mkBVSort(BVWIDTH)
+ } else {
+ z3.mkIntSort
+ }
+ boolSort = z3.mkBoolSort
+
+ def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
+ case BooleanType => RegularSort(boolSort)
+ case Int32Type => RegularSort(intSort)
+ case AbstractClassType(d) => RegularSort(adtSorts(d))
+ case CaseClassType(d) => RegularSort(adtSorts(d))
+ case SetType(d) => RegularSort(setSorts(d))
+ case mt @ MapType(d,r) => RegularSort(mapSorts(mt))
+ case _ => throw UntranslatableTypeException("Can't handle type " + tt)
+ }
+
+ val z3info = z3.mkADTSorts(
+ Seq(
+ (
+ toType.toString + "Option",
+ Seq(toType.toString + "Some", toType.toString + "None"),
+ Seq(
+ Seq(("value", typeToSortRef(toType))),
+ Seq()
+ )
+ )
+ )
+ )
+
+ z3info match {
+ case Seq((optionSort, Seq(someCons, noneCons), Seq(someTester, noneTester), Seq(Seq(valueSelector), Seq()))) =>
+ mapRangeSorts += ((toType, optionSort))
+ mapRangeSomeConstructors += ((toType, someCons))
+ mapRangeNoneConstructors += ((toType, noneCons))
+ mapRangeSomeTesters += ((toType, someTester))
+ mapRangeNoneTesters += ((toType, noneTester))
+ mapRangeValueSelectors += ((toType, valueSelector))
+ optionSort
+ }
+ }
+ }
+
+ case class UntranslatableTypeException(msg: String) extends Exception(msg)
+ // Prepares some of the Z3 sorts, but *not* the tuple sorts; these are created on-demand.
+ private def prepareSorts: Unit = {
+ import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
+ // NOTE THAT abstract classes that extend abstract classes are not
+ // currently supported in the translation
+ intSort = if(USEBV) {
+ z3.mkBVSort(BVWIDTH)
+ } else {
+ z3.mkIntSort
+ }
+ boolSort = z3.mkBoolSort
+ setSorts = Map.empty
+ setCardFuns = Map.empty
+
+ //unitSort = z3.mkUninterpretedSort("unit")
+ //unitValue = z3.mkFreshConst("Unit", unitSort)
+ //val bound = z3.mkBound(0, unitSort)
+ //val eq = z3.mkEq(bound, unitValue)
+ //val decls = Seq((z3.mkFreshStringSymbol("u"), unitSort))
+ //val unitAxiom = z3.mkForAll(0, Seq(), decls, eq)
+ //println(unitAxiom)
+ //println(unitValue)
+ //z3.assertCnstr(unitAxiom)
+ val Seq((us, Seq(unitCons), Seq(unitTester), _)) = z3.mkADTSorts(
+ Seq(
+ (
+ "Unit",
+ Seq("Unit"),
+ Seq(Seq())
+ )
+ )
+ )
+ unitSort = us
+ unitValue = unitCons()
+
+ val intSetSort = typeToSort(SetType(Int32Type))
+ intSetMinFun = z3.mkFreshFuncDecl("setMin", Seq(intSetSort), intSort)
+ intSetMaxFun = z3.mkFreshFuncDecl("setMax", Seq(intSetSort), intSort)
+
+ val roots = program.classHierarchyRoots
+ val indexMap: Map[ClassTypeDef, Int] = Map(roots.zipWithIndex: _*)
+ //println("indexMap: " + indexMap)
+
+ def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
+ // case BooleanType => RegularSort(boolSort)
+ // case Int32Type => RegularSort(intSort)
+ case AbstractClassType(d) => RecursiveType(indexMap(d))
+ case CaseClassType(d) => indexMap.get(d) match {
+ case Some(i) => RecursiveType(i)
+ case None => RecursiveType(indexMap(d.parent.get))
+ }
+ // case _ => throw UntranslatableTypeException("Can't handle type " + tt)
+ case _ => RegularSort(typeToSort(tt))
+ }
+
+ val childrenLists: Seq[List[CaseClassDef]] = roots.map(_ match {
+ case c: CaseClassDef => List(c)
+ case a: AbstractClassDef => a.knownChildren.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef]).toList
+ })
+ //println("children lists: " + childrenLists.toList.mkString("\n"))
+
+ val rootsAndChildren = (roots zip childrenLists)
+
+ val defs = rootsAndChildren.map(p => {
+ val (root, childrenList) = p
+
+ root match {
+ case c: CaseClassDef => {
+ // we create a recursive type with exactly one constructor
+ (c.id.uniqueName, List(c.id.uniqueName), List(c.fields.map(f => (f.id.uniqueName, typeToSortRef(f.tpe)))))
+ }
+ case a: AbstractClassDef => {
+ (a.id.uniqueName, childrenList.map(ccd => ccd.id.uniqueName), childrenList.map(ccd => ccd.fields.map(f => (f.id.uniqueName, typeToSortRef(f.tpe)))))
+ }
+ }
+ })
+
+ //println(defs)
+ // everything should be alright now...
+ val resultingZ3Info = z3.mkADTSorts(defs)
+
+ adtSorts = Map.empty
+ adtTesters = Map.empty
+ adtConstructors = Map.empty
+ adtFieldSelectors = Map.empty
+ reverseADTTesters = Map.empty
+ reverseADTConstructors = Map.empty
+ reverseADTFieldSelectors = Map.empty
+
+ for ((z3Inf, (root, childrenList)) <- (resultingZ3Info zip rootsAndChildren)) {
+ adtSorts += (root -> z3Inf._1)
+ assert(childrenList.size == z3Inf._2.size)
+ for ((child, (consFun, testFun)) <- childrenList zip (z3Inf._2 zip z3Inf._3)) {
+ adtTesters += (child -> testFun)
+ adtConstructors += (child -> consFun)
+ }
+ for ((child, fieldFuns) <- childrenList zip z3Inf._4) {
+ assert(child.fields.size == fieldFuns.size)
+ for ((fid, selFun) <- (child.fields.map(_.id) zip fieldFuns)) {
+ adtFieldSelectors += (fid -> selFun)
+ reverseADTFieldSelectors += (selFun -> (child, fid))
+ }
+ }
+ }
+
+ reverseADTTesters = adtTesters.map(_.swap)
+ reverseADTConstructors = adtConstructors.map(_.swap)
+ // ...and now everything should be in there...
+ }
+
+ // assumes prepareSorts has been called....
+ protected[leon] def typeToSort(tt: TypeTree): Z3Sort = tt match {
+ case Int32Type => intSort
+ case BooleanType => boolSort
+ case UnitType => unitSort
+ case AbstractClassType(cd) => adtSorts(cd)
+ case CaseClassType(cd) => {
+ if (cd.hasParent) {
+ adtSorts(cd.parent.get)
+ } else {
+ adtSorts(cd)
+ }
+ }
+ case SetType(base) => setSorts.get(base) match {
+ case Some(s) => s
+ case None => {
+ val newSetSort = z3.mkSetSort(typeToSort(base))
+ setSorts = setSorts + (base -> newSetSort)
+ val newCardFun = z3.mkFreshFuncDecl("card", Seq(newSetSort), intSort)
+ setCardFuns = setCardFuns + (base -> newCardFun)
+ newSetSort
+ }
+ }
+ case mt @ MapType(fromType, toType) => mapSorts.get(mt) match {
+ case Some(s) => s
+ case None => {
+ val fromSort = typeToSort(fromType)
+ val toSort = mapRangeSort(toType)
+ val ms = z3.mkArraySort(fromSort, toSort)
+ mapSorts += ((mt, ms))
+ ms
+ }
+ }
+ case at @ ArrayType(base) => arraySorts.get(at) match {
+ case Some(s) => s
+ case None => {
+ val intSort = typeToSort(Int32Type)
+ val toSort = typeToSort(base)
+ val as = z3.mkArraySort(intSort, toSort)
+ val tupleSortSymbol = z3.mkFreshStringSymbol("Array")
+ val (arrayTupleSort, arrayTupleCons_, Seq(arrayTupleSelectorArray_, arrayTupleSelectorLength_)) = z3.mkTupleSort(tupleSortSymbol, as, intSort)
+ arraySorts += (at -> arrayTupleSort)
+ arrayTupleCons += (at -> arrayTupleCons_)
+ arrayTupleSelectorArray += (at -> arrayTupleSelectorArray_)
+ arrayTupleSelectorLength += (at -> arrayTupleSelectorLength_)
+ arrayTupleSort
+ }
+ }
+ case ft @ FunctionType(fts, tt) => funSorts.get(ft) match {
+ case Some(s) => s
+ case None => {
+ val fss = fts map typeToSort
+ val ts = typeToSort(tt)
+ val (tupleSort, consFuncDecl, projFuncDecls) = z3.mkTupleSort(fts.map(_.toString).mkString("(",", ", ")"), fss: _*)
+ val funSort = z3.mkArraySort(tupleSort, ts)
+ funSorts += (ft -> funSort)
+ funDomainConstructors += (ft -> consFuncDecl)
+ funDomainSelectors += (ft -> projFuncDecls)
+ funSort
+ }
+ }
+ case tt @ TupleType(tpes) => tupleSorts.get(tt) match {
+ case Some(s) => s
+ case None => {
+ val tpesSorts = tpes.map(typeToSort)
+ val sortSymbol = z3.mkFreshStringSymbol("Tuple")
+ val (tupleSort, consTuple, projsTuple) = z3.mkTupleSort(sortSymbol, tpesSorts: _*)
+ tupleSorts += (tt -> tupleSort)
+ tupleConstructors += (tt -> consTuple)
+ reverseTupleConstructors += (consTuple -> tt)
+ tupleSelectors += (tt -> projsTuple)
+ projsTuple.zipWithIndex.foreach{ case (proj, i) => reverseTupleSelectors += (proj -> (tt, i)) }
+ tupleSort
+ }
+ }
+ case other => fallbackSorts.get(other) match {
+ case Some(s) => s
+ case None => {
+ reporter.warning("Resorting to uninterpreted type for : " + other)
+ val symbol = z3.mkIntSymbol(nextIntForSymbol())
+ val newFBSort = z3.mkUninterpretedSort(symbol)
+ fallbackSorts = fallbackSorts + (other -> newFBSort)
+ newFBSort
+ }
+ }
+ }
+
+ protected[leon] def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
+ class CantTranslateException extends Exception
+
+ val varsInformula: Set[Identifier] = variablesOf(expr)
+
+ var z3Vars: Map[Identifier,Z3AST] = if(!initialMap.isEmpty) {
+ initialMap
+ } else {
+ // FIXME TODO pleeeeeeeease make this cleaner. Ie. decide what set of
+ // variable has to remain in a map etc.
+ exprToZ3Id.filter(p => p._1.isInstanceOf[Variable]).map(p => (p._1.asInstanceOf[Variable].id -> p._2))
+ }
+
+ def rec(ex: Expr): Z3AST = {
+ //println("Stacking up call for:")
+ //println(ex)
+ val recResult = (ex match {
+ case tu @ Tuple(args) => {
+ // This call is required, because the Z3 sort may not have been generated yet.
+ // If it has, it's just a map lookup and instant return.
+ typeToSort(tu.getType)
+ val constructor = tupleConstructors(tu.getType)
+ constructor(args.map(rec(_)): _*)
+ }
+ case ts @ TupleSelect(tu, i) => {
+ // See comment above for similar code.
+ typeToSort(tu.getType)
+ val selector = tupleSelectors(tu.getType)(i-1)
+ selector(rec(tu))
+ }
+ case Let(i, e, b) => {
+ val re = rec(e)
+ z3Vars = z3Vars + (i -> re)
+ val rb = rec(b)
+ z3Vars = z3Vars - i
+ rb
+ }
+ case Waypoint(_, e) => rec(e)
+ case e @ Error(_) => {
+ val tpe = e.getType
+ val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
+ exprToZ3Id += (e -> newAST)
+ z3IdToExpr += (newAST -> e)
+ newAST
+ }
+ case v @ Variable(id) => z3Vars.get(id) match {
+ case Some(ast) => ast
+ case None => {
+ // if (id.isLetBinder) {
+ // scala.sys.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition")
+ // }
+ val newAST = z3.mkFreshConst(id.uniqueName/*name*/, typeToSort(v.getType))
+ z3Vars = z3Vars + (id -> newAST)
+ exprToZ3Id += (v -> newAST)
+ z3IdToExpr += (newAST -> v)
+ newAST
+ }
+ }
+
+ case ite @ IfExpr(c, t, e) => z3.mkITE(rec(c), rec(t), rec(e))
+ case And(exs) => z3.mkAnd(exs.map(rec(_)): _*)
+ case Or(exs) => z3.mkOr(exs.map(rec(_)): _*)
+ case Implies(l, r) => z3.mkImplies(rec(l), rec(r))
+ case Iff(l, r) => {
+ val rl = rec(l)
+ val rr = rec(r)
+ // z3.mkIff used to trigger a bug
+ z3.mkAnd(z3.mkImplies(rl, rr), z3.mkImplies(rr, rl))
+ }
+ case Not(Iff(l, r)) => z3.mkXor(rec(l), rec(r))
+ case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r))
+ case Not(e) => z3.mkNot(rec(e))
+ case IntLiteral(v) => z3.mkInt(v, intSort)
+ case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
+ case UnitLiteral => unitValue
+ case Equals(l, r) => z3.mkEq(rec(l), rec(r))
+ case Plus(l, r) => if(USEBV) z3.mkBVAdd(rec(l), rec(r)) else z3.mkAdd(rec(l), rec(r))
+ case Minus(l, r) => if(USEBV) z3.mkBVSub(rec(l), rec(r)) else z3.mkSub(rec(l), rec(r))
+ case Times(l, r) => if(USEBV) z3.mkBVMul(rec(l), rec(r)) else z3.mkMul(rec(l), rec(r))
+ case Division(l, r) => if(USEBV) z3.mkBVSdiv(rec(l), rec(r)) else z3.mkDiv(rec(l), rec(r))
+ case Modulo(l, r) => if(USEBV) sys.error("I don't know what to do here!") else z3.mkMod(rec(l), rec(r))
+ case UMinus(e) => if(USEBV) z3.mkBVNeg(rec(e)) else z3.mkUnaryMinus(rec(e))
+ case LessThan(l, r) => if(USEBV) z3.mkBVSlt(rec(l), rec(r)) else z3.mkLT(rec(l), rec(r))
+ case LessEquals(l, r) => if(USEBV) z3.mkBVSle(rec(l), rec(r)) else z3.mkLE(rec(l), rec(r))
+ case GreaterThan(l, r) => if(USEBV) z3.mkBVSgt(rec(l), rec(r)) else z3.mkGT(rec(l), rec(r))
+ case GreaterEquals(l, r) => if(USEBV) z3.mkBVSge(rec(l), rec(r)) else z3.mkGE(rec(l), rec(r))
+ case c @ CaseClass(cd, args) => {
+ val constructor = adtConstructors(cd)
+ constructor(args.map(rec(_)): _*)
+ }
+ case c @ CaseClassSelector(_, cc, sel) => {
+ val selector = adtFieldSelectors(sel)
+ selector(rec(cc))
+ }
+ case c @ CaseClassInstanceOf(ccd, e) => {
+ val tester = adtTesters(ccd)
+ tester(rec(e))
+ }
+ case f @ FunctionInvocation(fd, args) => {
+ z3.mkApp(functionDefToDecl(fd), args.map(rec(_)): _*)
+ }
+ case e @ EmptySet(_) => z3.mkEmptySet(typeToSort(e.getType.asInstanceOf[SetType].base))
+
+ case SetEquals(s1, s2) => z3.mkEq(rec(s1), rec(s2))
+ case ElementOfSet(e, s) => z3.mkSetSubset(z3.mkSetAdd(z3.mkEmptySet(typeToSort(e.getType)), 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) => elems.foldLeft(z3.mkEmptySet(typeToSort(f.getType.asInstanceOf[SetType].base)))((ast, el) => z3.mkSetAdd(ast, rec(el)))
+ case SetCardinality(s) => {
+ val rs = rec(s)
+ setCardFuns(s.getType.asInstanceOf[SetType].base)(rs)
+ }
+ case SetMin(s) => intSetMinFun(rec(s))
+ case SetMax(s) => intSetMaxFun(rec(s))
+ case s @ SingletonMap(from,to) => s.getType match {
+ case MapType(fromType, toType) =>
+ val fromSort = typeToSort(fromType)
+ val toSort = typeToSort(toType)
+ val constArray = z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
+ z3.mkStore(constArray, rec(from), mapRangeSomeConstructors(toType)(rec(to)))
+ case errorType => scala.sys.error("Unexpected type for singleton map: " + (ex, errorType))
+ }
+ case e @ EmptyMap(fromType, toType) => {
+ typeToSort(e.getType) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
+ val fromSort = typeToSort(fromType)
+ val toSort = typeToSort(toType)
+ z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
+ }
+ case f @ FiniteMap(elems) => f.getType match {
+ case MapType(fromType, toType) =>
+ val fromSort = typeToSort(fromType)
+ val toSort = typeToSort(toType)
+ elems.foldLeft(z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())){ case (ast, SingletonMap(k,v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(toType)(rec(v))) }
+ case errorType => scala.sys.error("Unexpected type for finite map: " + (ex, errorType))
+ }
+ case mg @ MapGet(m,k) => m.getType match {
+ case MapType(fromType, toType) =>
+ val selected = z3.mkSelect(rec(m), rec(k))
+ mapRangeValueSelectors(toType)(selected)
+ case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
+ }
+ case MapUnion(m1,m2) => m1.getType match {
+ case MapType(ft, tt) => m2 match {
+ case FiniteMap(ss) =>
+ ss.foldLeft(rec(m1)){
+ case (ast, SingletonMap(k, v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(tt)(rec(v)))
+ }
+ case SingletonMap(k, v) => z3.mkStore(rec(m1), rec(k), mapRangeSomeConstructors(tt)(rec(v)))
+ case _ => scala.sys.error("map updates can only be applied with concrete map instances")
+ }
+ case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
+ }
+ case MapIsDefinedAt(m,k) => m.getType match {
+ case MapType(ft, tt) => z3.mkDistinct(z3.mkSelect(rec(m), rec(k)), mapRangeNoneConstructors(tt)())
+ case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
+ }
+ case fill @ ArrayFill(length, default) => {
+ val at@ArrayType(base) = fill.getType
+ typeToSort(at)
+ val cons = arrayTupleCons(at)
+ val ar = z3.mkConstArray(typeToSort(base), rec(default))
+ val res = cons(ar, rec(length))
+ res
+ }
+ case ArraySelect(a, index) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getArray = arrayTupleSelectorArray(a.getType)
+ val res = z3.mkSelect(getArray(ar), rec(index))
+ res
+ }
+ case ArrayUpdated(a, index, newVal) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getArray = arrayTupleSelectorArray(a.getType)
+ val getLength = arrayTupleSelectorLength(a.getType)
+ val cons = arrayTupleCons(a.getType)
+ val store = z3.mkStore(getArray(ar), rec(index), rec(newVal))
+ val res = cons(store, getLength(ar))
+ res
+ }
+ case ArrayLength(a) => {
+ typeToSort(a.getType)
+ val ar = rec(a)
+ val getLength = arrayTupleSelectorLength(a.getType)
+ val res = getLength(ar)
+ res
+ }
+ case AnonymousFunctionInvocation(id, args) => id.getType match {
+ case ft @ FunctionType(fts, tt) => {
+ val consFD = funDomainConstructors(ft)
+ val rid = rec(Variable(id))
+ val rargs = args map rec
+ z3.mkSelect(rid, consFD(rargs: _*))
+ }
+ case errorType => scala.sys.error("Unexpected type for function: " + (ex, errorType))
+ }
+
+ case Distinct(exs) => z3.mkDistinct(exs.map(rec(_)): _*)
+
+ case _ => {
+ reporter.warning("Can't handle this in translation to Z3: " + ex)
+ throw new CantTranslateException
+ }
+ })
+ recResult
+ }
+
+ try {
+ val res = Some(rec(expr))
+ res
+ } catch {
+ case e: CantTranslateException => None
+ }
+ }
+
+ protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = {
+ def rec(t: Z3AST, expType: Option[TypeTree] = None) : Expr = expType match {
+ case Some(MapType(kt,vt)) =>
+ model.getArrayValue(t) match {
+ case None => throw new CantTranslateException(t)
+ case Some((map, elseValue)) =>
+ val singletons = map.map(e => (e, z3.getASTKind(e._2))).collect {
+ case ((index, value), Z3AppAST(someCons, arg :: Nil)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(rec(index, Some(kt)), rec(arg, Some(vt)))
+ }
+ (if (singletons.isEmpty) EmptyMap(kt, vt) else FiniteMap(singletons.toSeq)).setType(expType.get)
+ }
+ case funType @ Some(FunctionType(fts, tt)) =>
+ model.getArrayValue(t) match {
+ case None => throw new CantTranslateException(t)
+ case Some((es, ev)) =>
+ val entries: Seq[(Seq[Expr], Expr)] = es.toSeq.map(e => (e, z3.getASTKind(e._1))).collect {
+ case ((key, value), Z3AppAST(cons, args)) if cons == funDomainConstructors(funType.get) => ((args zip fts) map (p => rec(p._1, Some(p._2))), rec(value, Some(tt)))
+ }
+ val elseValue = rec(ev, Some(tt))
+ AnonymousFunction(entries, elseValue).setType(expType.get)
+ }
+ case Some(SetType(dt)) =>
+ model.getSetValue(t) match {
+ case None => throw new CantTranslateException(t)
+ case Some(set) => {
+ val elems = set.map(e => rec(e, Some(dt)))
+ (if (elems.isEmpty) EmptySet(dt) else FiniteSet(elems.toSeq)).setType(expType.get)
+ }
+ }
+ case Some(ArrayType(dt)) => {
+ val Z3AppAST(decl, args) = z3.getASTKind(t)
+ assert(args.size == 2)
+ val IntLiteral(length) = rec(args(1), Some(Int32Type))
+ val array = model.getArrayValue(args(0)) match {
+ case None => throw new CantTranslateException(t)
+ case Some((map, elseValue)) => {
+ val exprs = map.foldLeft((1 to length).map(_ => rec(elseValue, Some(dt))).toSeq)((acc, p) => {
+ val IntLiteral(index) = rec(p._1, Some(Int32Type))
+ if(index >= 0 && index < length)
+ acc.updated(index, rec(p._2, Some(dt)))
+ else acc
+ })
+ FiniteArray(exprs)
+ }
+ }
+ array
+ }
+ case other =>
+ if(t == unitValue)
+ UnitLiteral
+ else z3.getASTKind(t) match {
+ case Z3AppAST(decl, args) => {
+ val argsSize = args.size
+ if(argsSize == 0 && z3IdToExpr.isDefinedAt(t)) {
+ val toRet = z3IdToExpr(t)
+ // println("Map says I should replace " + t + " by " + toRet)
+ toRet
+ } else if(isKnownDecl(decl)) {
+ val fd = functionDeclToDef(decl)
+ assert(fd.args.size == argsSize)
+ FunctionInvocation(fd, (args zip fd.args).map(p => rec(p._1,Some(p._2.tpe))))
+ } else if(argsSize == 1 && reverseADTTesters.isDefinedAt(decl)) {
+ CaseClassInstanceOf(reverseADTTesters(decl), rec(args(0)))
+ } else if(argsSize == 1 && reverseADTFieldSelectors.isDefinedAt(decl)) {
+ val (ccd, fid) = reverseADTFieldSelectors(decl)
+ CaseClassSelector(ccd, rec(args(0)), fid)
+ } else if(reverseADTConstructors.isDefinedAt(decl)) {
+ val ccd = reverseADTConstructors(decl)
+ assert(argsSize == ccd.fields.size)
+ CaseClass(ccd, (args zip ccd.fields).map(p => rec(p._1, Some(p._2.tpe))))
+ } else if(reverseTupleConstructors.isDefinedAt(decl)) {
+ val TupleType(subTypes) = reverseTupleConstructors(decl)
+ val rargs = args.zip(subTypes).map(p => rec(p._1, Some(p._2)))
+ Tuple(rargs)
+ } else {
+ import Z3DeclKind._
+ val rargs = args.map(rec(_))
+ z3.getDeclKind(decl) match {
+ case OpTrue => BooleanLiteral(true)
+ case OpFalse => BooleanLiteral(false)
+ case OpEq => Equals(rargs(0), rargs(1))
+ case OpITE => {
+ assert(argsSize == 3)
+ val r0 = rargs(0)
+ val r1 = rargs(1)
+ val r2 = rargs(2)
+ try {
+ IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType).get)
+ } catch {
+ case e => {
+ println("I was asking for lub because of this.")
+ println(t)
+ println("which was translated as")
+ println(IfExpr(r0,r1,r2))
+ throw e
+ }
+ }
+ }
+ case OpAnd => And(rargs)
+ case OpOr => Or(rargs)
+ case OpIff => Iff(rargs(0), rargs(1))
+ case OpXor => Not(Iff(rargs(0), rargs(1)))
+ case OpNot => Not(rargs(0))
+ case OpImplies => Implies(rargs(0), rargs(1))
+ case OpLE => LessEquals(rargs(0), rargs(1))
+ case OpGE => GreaterEquals(rargs(0), rargs(1))
+ case OpLT => LessThan(rargs(0), rargs(1))
+ case OpGT => GreaterThan(rargs(0), rargs(1))
+ case OpAdd => {
+ assert(argsSize == 2)
+ Plus(rargs(0), rargs(1))
+ }
+ case OpSub => {
+ assert(argsSize == 2)
+ Minus(rargs(0), rargs(1))
+ }
+ case OpUMinus => UMinus(rargs(0))
+ case OpMul => {
+ assert(argsSize == 2)
+ Times(rargs(0), rargs(1))
+ }
+ case OpDiv => {
+ assert(argsSize == 2)
+ Division(rargs(0), rargs(1))
+ }
+ case OpIDiv => {
+ assert(argsSize == 2)
+ Division(rargs(0), rargs(1))
+ }
+ case OpMod => {
+ assert(argsSize == 2)
+ Modulo(rargs(0), rargs(1))
+ }
+ case OpAsArray => {
+ assert(argsSize == 0)
+ throw new Exception("encountered OpAsArray")
+ }
+ case other => {
+ System.err.println("Don't know what to do with this declKind : " + other)
+ System.err.println("The arguments are : " + args)
+ throw new CantTranslateException(t)
+ }
+ }
+ }
+ }
+
+ case Z3NumeralAST(Some(v)) => IntLiteral(v)
+ case Z3NumeralAST(None) => {
+ reporter.info("Cannot read exact model from Z3: Integer does not fit in machine word")
+ reporter.info("Exiting procedure now")
+ sys.exit(0)
+ }
+ case other @ _ => {
+ System.err.println("Don't know what this is " + other)
+ throw new CantTranslateException(t)
+ }
+ }
+ }
+ rec(tree, expectedType)
+ }
+
+ protected[leon] def softFromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: TypeTree) : Option[Expr] = {
+ try {
+ Some(fromZ3Formula(model, tree, Some(expectedType)))
+ } catch {
+ case e: CantTranslateException => None
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
similarity index 63%
rename from src/main/scala/leon/FairZ3Solver.scala
rename to src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 23f93d497..b0d7ba9d2 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -1,4 +1,5 @@
package leon
+package solvers.z3
import z3.scala._
import purescala.Common._
@@ -16,15 +17,13 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
// have to comment this to use the solver for constraint solving...
// assert(Settings.useFairInstantiator)
- private final val UNKNOWNASSAT : Boolean = !Settings.noForallAxioms
- private final val USEBV : Boolean = Settings.bitvectorBitwidth.isDefined
- private final val BVWIDTH : Int = Settings.bitvectorBitwidth.getOrElse(-1)
+ private val UNKNOWNASSAT : Boolean = !Settings.noForallAxioms
val description = "Fair Z3 Solver"
override val shortDescription = "Z3-f"
// this is fixed
- private val z3cfg = new Z3Config(
+ protected[leon] val z3cfg = new Z3Config(
"MODEL" -> true,
"MBQI" -> false,
// "SOFT_TIMEOUT" -> 100,
@@ -33,53 +32,13 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
)
toggleWarningMessages(true)
- protected[leon] var z3: Z3Context = null
- protected[leon] var program: Program = null
- private var neverInitialized = true
-
private var unrollingBank: UnrollingBank = null
private var blockingSet: Set[Expr] = Set.empty
private var toCheckAgainstModels: Expr = BooleanLiteral(true)
private var varsInVC: Set[Identifier] = Set.empty
- override def setProgram(prog: Program): Unit = {
- program = prog
- }
-
- def restartZ3: Unit = {
- if (neverInitialized) {
- neverInitialized = false
- } else {
- z3.delete
- }
- z3 = new Z3Context(z3cfg)
- // z3.traceToStdout
-
- exprToZ3Id = Map.empty
- z3IdToExpr = Map.empty
-
- fallbackSorts = Map.empty
-
- mapSorts = Map.empty
- arraySorts = Map.empty
- funSorts = Map.empty
- funDomainConstructors = Map.empty
- funDomainSelectors = Map.empty
-
- tupleSorts = Map.empty
- tupleConstructors = Map.empty
- tupleSelectors = Map.empty
-
- mapRangeSorts.clear
- mapRangeSomeConstructors.clear
- mapRangeNoneConstructors.clear
- mapRangeSomeTesters.clear
- mapRangeNoneTesters.clear
- mapRangeValueSelectors.clear
-
- counter = 0
- prepareSorts
- prepareFunctions
+ override def restartZ3 : Unit = {
+ super.restartZ3
unrollingBank = new UnrollingBank
blockingSet = Set.empty
@@ -87,218 +46,6 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
varsInVC = Set.empty
}
- private var counter = 0
- private object nextIntForSymbol {
- def apply(): Int = {
- val res = counter
- counter = counter + 1
- res
- }
- }
-
- private var intSort: Z3Sort = null
- private var boolSort: Z3Sort = null
- private var setSorts: Map[TypeTree, Z3Sort] = Map.empty
- private var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
-
- private var unitSort: Z3Sort = null
- private var unitValue: Z3AST = null
-
- protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
- protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
-
- protected[leon] var tupleSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[leon] var tupleConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
- protected[leon] var tupleSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
-
- private var arraySorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[leon] var arrayTupleCons: Map[TypeTree, Z3FuncDecl] = Map.empty
- protected[leon] var arrayTupleSelectorArray: Map[TypeTree, Z3FuncDecl] = Map.empty
- protected[leon] var arrayTupleSelectorLength: Map[TypeTree, Z3FuncDecl] = Map.empty
-
- private var reverseTupleConstructors: Map[Z3FuncDecl, TupleType] = Map.empty
- private var reverseTupleSelectors: Map[Z3FuncDecl, (TupleType, Int)] = Map.empty
-
- private var intSetMinFun: Z3FuncDecl = null
- private var intSetMaxFun: Z3FuncDecl = null
- private var setCardFuns: Map[TypeTree, Z3FuncDecl] = Map.empty
- private var adtSorts: Map[ClassTypeDef, Z3Sort] = Map.empty
- private var fallbackSorts: Map[TypeTree, Z3Sort] = Map.empty
-
- protected[leon] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
- protected[leon] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
- protected[leon] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
-
- private var reverseADTTesters: Map[Z3FuncDecl, CaseClassDef] = Map.empty
- private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
- private var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty
-
- protected[leon] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
- protected[leon] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[leon] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[leon] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
-
- private def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
- case Some(z3sort) => z3sort
- case None => {
- import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
- intSort = if(USEBV) {
- z3.mkBVSort(BVWIDTH)
- } else {
- z3.mkIntSort
- }
- boolSort = z3.mkBoolSort
-
- def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
- case BooleanType => RegularSort(boolSort)
- case Int32Type => RegularSort(intSort)
- case AbstractClassType(d) => RegularSort(adtSorts(d))
- case CaseClassType(d) => RegularSort(adtSorts(d))
- case SetType(d) => RegularSort(setSorts(d))
- case mt @ MapType(d,r) => RegularSort(mapSorts(mt))
- case _ => throw UntranslatableTypeException("Can't handle type " + tt)
- }
-
- val z3info = z3.mkADTSorts(
- Seq(
- (
- toType.toString + "Option",
- Seq(toType.toString + "Some", toType.toString + "None"),
- Seq(
- Seq(("value", typeToSortRef(toType))),
- Seq()
- )
- )
- )
- )
-
- z3info match {
- case Seq((optionSort, Seq(someCons, noneCons), Seq(someTester, noneTester), Seq(Seq(valueSelector), Seq()))) =>
- mapRangeSorts += ((toType, optionSort))
- mapRangeSomeConstructors += ((toType, someCons))
- mapRangeNoneConstructors += ((toType, noneCons))
- mapRangeSomeTesters += ((toType, someTester))
- mapRangeNoneTesters += ((toType, noneTester))
- mapRangeValueSelectors += ((toType, valueSelector))
- optionSort
- }
- }
- }
-
- case class UntranslatableTypeException(msg: String) extends Exception(msg)
- // Prepares some of the Z3 sorts, but *not* the tuple sorts; these are created on-demand.
- private def prepareSorts: Unit = {
- import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
- // NOTE THAT abstract classes that extend abstract classes are not
- // currently supported in the translation
- intSort = if(USEBV) {
- z3.mkBVSort(BVWIDTH)
- } else {
- z3.mkIntSort
- }
- boolSort = z3.mkBoolSort
- setSorts = Map.empty
- setCardFuns = Map.empty
-
- //unitSort = z3.mkUninterpretedSort("unit")
- //unitValue = z3.mkFreshConst("Unit", unitSort)
- //val bound = z3.mkBound(0, unitSort)
- //val eq = z3.mkEq(bound, unitValue)
- //val decls = Seq((z3.mkFreshStringSymbol("u"), unitSort))
- //val unitAxiom = z3.mkForAll(0, Seq(), decls, eq)
- //println(unitAxiom)
- //println(unitValue)
- //z3.assertCnstr(unitAxiom)
- val Seq((us, Seq(unitCons), Seq(unitTester), _)) = z3.mkADTSorts(
- Seq(
- (
- "Unit",
- Seq("Unit"),
- Seq(Seq())
- )
- )
- )
- unitSort = us
- unitValue = unitCons()
-
- val intSetSort = typeToSort(SetType(Int32Type))
- intSetMinFun = z3.mkFreshFuncDecl("setMin", Seq(intSetSort), intSort)
- intSetMaxFun = z3.mkFreshFuncDecl("setMax", Seq(intSetSort), intSort)
-
- val roots = program.classHierarchyRoots
- val indexMap: Map[ClassTypeDef, Int] = Map(roots.zipWithIndex: _*)
- //println("indexMap: " + indexMap)
-
- def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
- // case BooleanType => RegularSort(boolSort)
- // case Int32Type => RegularSort(intSort)
- case AbstractClassType(d) => RecursiveType(indexMap(d))
- case CaseClassType(d) => indexMap.get(d) match {
- case Some(i) => RecursiveType(i)
- case None => RecursiveType(indexMap(d.parent.get))
- }
- // case _ => throw UntranslatableTypeException("Can't handle type " + tt)
- case _ => RegularSort(typeToSort(tt))
- }
-
- val childrenLists: Seq[List[CaseClassDef]] = roots.map(_ match {
- case c: CaseClassDef => List(c)
- case a: AbstractClassDef => a.knownChildren.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef]).toList
- })
- //println("children lists: " + childrenLists.toList.mkString("\n"))
-
- val rootsAndChildren = (roots zip childrenLists)
-
- val defs = rootsAndChildren.map(p => {
- val (root, childrenList) = p
-
- root match {
- case c: CaseClassDef => {
- // we create a recursive type with exactly one constructor
- (c.id.uniqueName, List(c.id.uniqueName), List(c.fields.map(f => (f.id.uniqueName, typeToSortRef(f.tpe)))))
- }
- case a: AbstractClassDef => {
- (a.id.uniqueName, childrenList.map(ccd => ccd.id.uniqueName), childrenList.map(ccd => ccd.fields.map(f => (f.id.uniqueName, typeToSortRef(f.tpe)))))
- }
- }
- })
-
- //println(defs)
- // everything should be alright now...
- val resultingZ3Info = z3.mkADTSorts(defs)
-
- adtSorts = Map.empty
- adtTesters = Map.empty
- adtConstructors = Map.empty
- adtFieldSelectors = Map.empty
- reverseADTTesters = Map.empty
- reverseADTConstructors = Map.empty
- reverseADTFieldSelectors = Map.empty
-
- for ((z3Inf, (root, childrenList)) <- (resultingZ3Info zip rootsAndChildren)) {
- adtSorts += (root -> z3Inf._1)
- assert(childrenList.size == z3Inf._2.size)
- for ((child, (consFun, testFun)) <- childrenList zip (z3Inf._2 zip z3Inf._3)) {
- adtTesters += (child -> testFun)
- adtConstructors += (child -> consFun)
- }
- for ((child, fieldFuns) <- childrenList zip z3Inf._4) {
- assert(child.fields.size == fieldFuns.size)
- for ((fid, selFun) <- (child.fields.map(_.id) zip fieldFuns)) {
- adtFieldSelectors += (fid -> selFun)
- reverseADTFieldSelectors += (selFun -> (child, fid))
- }
- }
- }
-
- reverseADTTesters = adtTesters.map(_.swap)
- reverseADTConstructors = adtConstructors.map(_.swap)
- // ...and now everything should be in there...
- }
-
def isKnownDef(funDef: FunDef) : Boolean = functionMap.isDefinedAt(funDef)
def functionDefToDecl(funDef: FunDef) : Z3FuncDecl =
@@ -389,92 +136,6 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
})
}
- // assumes prepareSorts has been called....
- def typeToSort(tt: TypeTree): Z3Sort = tt match {
- case Int32Type => intSort
- case BooleanType => boolSort
- case UnitType => unitSort
- case AbstractClassType(cd) => adtSorts(cd)
- case CaseClassType(cd) => {
- if (cd.hasParent) {
- adtSorts(cd.parent.get)
- } else {
- adtSorts(cd)
- }
- }
- case SetType(base) => setSorts.get(base) match {
- case Some(s) => s
- case None => {
- val newSetSort = z3.mkSetSort(typeToSort(base))
- setSorts = setSorts + (base -> newSetSort)
- val newCardFun = z3.mkFreshFuncDecl("card", Seq(newSetSort), intSort)
- setCardFuns = setCardFuns + (base -> newCardFun)
- newSetSort
- }
- }
- case mt @ MapType(fromType, toType) => mapSorts.get(mt) match {
- case Some(s) => s
- case None => {
- val fromSort = typeToSort(fromType)
- val toSort = mapRangeSort(toType)
- val ms = z3.mkArraySort(fromSort, toSort)
- mapSorts += ((mt, ms))
- ms
- }
- }
- case at @ ArrayType(base) => arraySorts.get(at) match {
- case Some(s) => s
- case None => {
- val intSort = typeToSort(Int32Type)
- val toSort = typeToSort(base)
- val as = z3.mkArraySort(intSort, toSort)
- val tupleSortSymbol = z3.mkFreshStringSymbol("Array")
- val (arrayTupleSort, arrayTupleCons_, Seq(arrayTupleSelectorArray_, arrayTupleSelectorLength_)) = z3.mkTupleSort(tupleSortSymbol, as, intSort)
- arraySorts += (at -> arrayTupleSort)
- arrayTupleCons += (at -> arrayTupleCons_)
- arrayTupleSelectorArray += (at -> arrayTupleSelectorArray_)
- arrayTupleSelectorLength += (at -> arrayTupleSelectorLength_)
- arrayTupleSort
- }
- }
- case ft @ FunctionType(fts, tt) => funSorts.get(ft) match {
- case Some(s) => s
- case None => {
- val fss = fts map typeToSort
- val ts = typeToSort(tt)
- val (tupleSort, consFuncDecl, projFuncDecls) = z3.mkTupleSort(fts.map(_.toString).mkString("(",", ", ")"), fss: _*)
- val funSort = z3.mkArraySort(tupleSort, ts)
- funSorts += (ft -> funSort)
- funDomainConstructors += (ft -> consFuncDecl)
- funDomainSelectors += (ft -> projFuncDecls)
- funSort
- }
- }
- case tt @ TupleType(tpes) => tupleSorts.get(tt) match {
- case Some(s) => s
- case None => {
- val tpesSorts = tpes.map(typeToSort)
- val sortSymbol = z3.mkFreshStringSymbol("Tuple")
- val (tupleSort, consTuple, projsTuple) = z3.mkTupleSort(sortSymbol, tpesSorts: _*)
- tupleSorts += (tt -> tupleSort)
- tupleConstructors += (tt -> consTuple)
- reverseTupleConstructors += (consTuple -> tt)
- tupleSelectors += (tt -> projsTuple)
- projsTuple.zipWithIndex.foreach{ case (proj, i) => reverseTupleSelectors += (proj -> (tt, i)) }
- tupleSort
- }
- }
- case other => fallbackSorts.get(other) match {
- case Some(s) => s
- case None => {
- reporter.warning("Resorting to uninterpreted type for : " + other)
- val symbol = z3.mkIntSymbol(nextIntForSymbol())
- val newFBSort = z3.mkUninterpretedSort(symbol)
- fallbackSorts = fallbackSorts + (other -> newFBSort)
- newFBSort
- }
- }
- }
override def isUnsat(vc: Expr) = decide(vc, false)
@@ -485,12 +146,6 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
decideWithModel(vc, true)
}
- def solveWithBounds(vc: Expr, fv: Boolean) : (Option[Boolean], Map[Identifier,Expr]) = {
- restartZ3
- boundValues
- decideWithModel(vc, fv)
- }
-
def decide(vc: Expr, forValidity: Boolean):Option[Boolean] = {
restartZ3
decideWithModel(vc, forValidity)._1
@@ -533,17 +188,6 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
initializationStopwatch.start
foundDefinitiveAnswer = false
- /*
- def stopCallback() : Unit = {
- if(!foundDefinitiveAnswer) {
- reporter.error(" - Timeout reached.")
- forceStop = true
- z3.softCheckCancel
- }
- }*/
-
- //val timer : Option[Timer] = Settings.solverTimeout.map(t => new Timer(stopCallback, t))
- //timer.foreach(_.start())
var definitiveAnswer : Option[Boolean] = None
var definitiveModel : Map[Identifier,Expr] = Map.empty
@@ -554,7 +198,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
//timer.foreach(t => t.halt)
}
- if (neverInitialized) {
+ if (program == null) {
reporter.error("Z3 Solver was not initialized with a PureScala Program.")
None
}
@@ -925,9 +569,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(cleanedUp, newClauses.reverse, ite2Bools)
}
- protected[leon] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty
- protected[leon] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty
- protected[leon] def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
+ protected[leon] override def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
class CantTranslateException extends Exception
val varsInformula: Set[Identifier] = variablesOf(expr)
@@ -1164,170 +806,6 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
- protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = {
- def rec(t: Z3AST, expType: Option[TypeTree] = None) : Expr = expType match {
- case Some(MapType(kt,vt)) =>
- model.getArrayValue(t) match {
- case None => throw new CantTranslateException(t)
- case Some((map, elseValue)) =>
- val singletons = map.map(e => (e, z3.getASTKind(e._2))).collect {
- case ((index, value), Z3AppAST(someCons, arg :: Nil)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(rec(index, Some(kt)), rec(arg, Some(vt)))
- }
- (if (singletons.isEmpty) EmptyMap(kt, vt) else FiniteMap(singletons.toSeq)).setType(expType.get)
- }
- case funType @ Some(FunctionType(fts, tt)) =>
- model.getArrayValue(t) match {
- case None => throw new CantTranslateException(t)
- case Some((es, ev)) =>
- val entries: Seq[(Seq[Expr], Expr)] = es.toSeq.map(e => (e, z3.getASTKind(e._1))).collect {
- case ((key, value), Z3AppAST(cons, args)) if cons == funDomainConstructors(funType.get) => ((args zip fts) map (p => rec(p._1, Some(p._2))), rec(value, Some(tt)))
- }
- val elseValue = rec(ev, Some(tt))
- AnonymousFunction(entries, elseValue).setType(expType.get)
- }
- case Some(SetType(dt)) =>
- model.getSetValue(t) match {
- case None => throw new CantTranslateException(t)
- case Some(set) => {
- val elems = set.map(e => rec(e, Some(dt)))
- (if (elems.isEmpty) EmptySet(dt) else FiniteSet(elems.toSeq)).setType(expType.get)
- }
- }
- case Some(ArrayType(dt)) => {
- val Z3AppAST(decl, args) = z3.getASTKind(t)
- assert(args.size == 2)
- val IntLiteral(length) = rec(args(1), Some(Int32Type))
- val array = model.getArrayValue(args(0)) match {
- case None => throw new CantTranslateException(t)
- case Some((map, elseValue)) => {
- val exprs = map.foldLeft((1 to length).map(_ => rec(elseValue, Some(dt))).toSeq)((acc, p) => {
- val IntLiteral(index) = rec(p._1, Some(Int32Type))
- if(index >= 0 && index < length)
- acc.updated(index, rec(p._2, Some(dt)))
- else acc
- })
- FiniteArray(exprs)
- }
- }
- array
- }
- case other =>
- if(t == unitValue)
- UnitLiteral
- else z3.getASTKind(t) match {
- case Z3AppAST(decl, args) => {
- val argsSize = args.size
- if(argsSize == 0 && z3IdToExpr.isDefinedAt(t)) {
- val toRet = z3IdToExpr(t)
- // println("Map says I should replace " + t + " by " + toRet)
- toRet
- } else if(isKnownDecl(decl)) {
- val fd = functionDeclToDef(decl)
- assert(fd.args.size == argsSize)
- FunctionInvocation(fd, (args zip fd.args).map(p => rec(p._1,Some(p._2.tpe))))
- } else if(argsSize == 1 && reverseADTTesters.isDefinedAt(decl)) {
- CaseClassInstanceOf(reverseADTTesters(decl), rec(args(0)))
- } else if(argsSize == 1 && reverseADTFieldSelectors.isDefinedAt(decl)) {
- val (ccd, fid) = reverseADTFieldSelectors(decl)
- CaseClassSelector(ccd, rec(args(0)), fid)
- } else if(reverseADTConstructors.isDefinedAt(decl)) {
- val ccd = reverseADTConstructors(decl)
- assert(argsSize == ccd.fields.size)
- CaseClass(ccd, (args zip ccd.fields).map(p => rec(p._1, Some(p._2.tpe))))
- } else if(reverseTupleConstructors.isDefinedAt(decl)) {
- val TupleType(subTypes) = reverseTupleConstructors(decl)
- val rargs = args.zip(subTypes).map(p => rec(p._1, Some(p._2)))
- Tuple(rargs)
- } else {
- import Z3DeclKind._
- val rargs = args.map(rec(_))
- z3.getDeclKind(decl) match {
- case OpTrue => BooleanLiteral(true)
- case OpFalse => BooleanLiteral(false)
- case OpEq => Equals(rargs(0), rargs(1))
- case OpITE => {
- assert(argsSize == 3)
- val r0 = rargs(0)
- val r1 = rargs(1)
- val r2 = rargs(2)
- try {
- IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType).get)
- } catch {
- case e => {
- println("I was asking for lub because of this.")
- println(t)
- println("which was translated as")
- println(IfExpr(r0,r1,r2))
- throw e
- }
- }
- }
- case OpAnd => And(rargs)
- case OpOr => Or(rargs)
- case OpIff => Iff(rargs(0), rargs(1))
- case OpXor => Not(Iff(rargs(0), rargs(1)))
- case OpNot => Not(rargs(0))
- case OpImplies => Implies(rargs(0), rargs(1))
- case OpLE => LessEquals(rargs(0), rargs(1))
- case OpGE => GreaterEquals(rargs(0), rargs(1))
- case OpLT => LessThan(rargs(0), rargs(1))
- case OpGT => GreaterThan(rargs(0), rargs(1))
- case OpAdd => {
- assert(argsSize == 2)
- Plus(rargs(0), rargs(1))
- }
- case OpSub => {
- assert(argsSize == 2)
- Minus(rargs(0), rargs(1))
- }
- case OpUMinus => UMinus(rargs(0))
- case OpMul => {
- assert(argsSize == 2)
- Times(rargs(0), rargs(1))
- }
- case OpDiv => {
- assert(argsSize == 2)
- Division(rargs(0), rargs(1))
- }
- case OpIDiv => {
- assert(argsSize == 2)
- Division(rargs(0), rargs(1))
- }
- case OpMod => {
- assert(argsSize == 2)
- Modulo(rargs(0), rargs(1))
- }
- case OpAsArray => {
- assert(argsSize == 0)
- throw new Exception("encountered OpAsArray")
- }
- case other => {
- System.err.println("Don't know what to do with this declKind : " + other)
- System.err.println("The arguments are : " + args)
- throw new CantTranslateException(t)
- }
- }
- }
- }
-
- case Z3NumeralAST(Some(v)) => IntLiteral(v)
- case Z3NumeralAST(None) => {
- reporter.info("Cannot read exact model from Z3: Integer does not fit in machine word")
- reporter.info("Exiting procedure now")
- sys.exit(0)
- }
- case other @ _ => {
- System.err.println("Don't know what this is " + other)
- System.err.println("REVERSE FUNCTION MAP:")
- System.err.println(reverseFunctionMap.toSeq.mkString("\n"))
- System.err.println("REVERSE CONS MAP:")
- System.err.println(reverseADTConstructors.toSeq.mkString("\n"))
- throw new CantTranslateException(t)
- }
- }
- }
- rec(tree, expectedType)
- }
class UnrollingBank {
private val blockMap : MutableMap[(Identifier,Boolean),Set[FunctionInvocation]] = MutableMap.empty
diff --git a/src/main/scala/leon/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
similarity index 99%
rename from src/main/scala/leon/Z3ModelReconstruction.scala
rename to src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 87c75ddd5..5fc00acd0 100644
--- a/src/main/scala/leon/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -1,4 +1,5 @@
package leon
+package solvers.z3
import z3.scala._
import purescala.Common._
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 898891307..91134fcbd 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,6 +1,9 @@
package leon
package synthesis
+import solvers.TrivialSolver
+import solvers.z3.FairZ3Solver
+
import purescala.Definitions.Program
object SynthesisPhase extends LeonPhase[Program, Program] {
diff --git a/src/main/scala/leon/testgen/CallGraph.scala b/src/main/scala/leon/testgen/CallGraph.scala
index afebd8bde..d7169bb17 100644
--- a/src/main/scala/leon/testgen/CallGraph.scala
+++ b/src/main/scala/leon/testgen/CallGraph.scala
@@ -6,7 +6,7 @@ import leon.purescala.TreeOps._
import leon.purescala.Extractors._
import leon.purescala.TypeTrees._
import leon.purescala.Common._
-import leon.FairZ3Solver
+import leon.solvers.z3.FairZ3Solver
class CallGraph(val program: Program) {
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 8404294ee..5056ec0e8 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -7,7 +7,7 @@ import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
import leon.purescala.ScalaPrinter
import leon.Extensions._
-import leon.FairZ3Solver
+import leon.solvers.z3.FairZ3Solver
import leon.Reporter
import scala.collection.mutable.{Set => MutableSet}
--
GitLab