diff --git a/demo/Maps.scala b/demo/Maps.scala
index 25ca9627eff5c2508f3d2274576012457966e5a4..79554aa5d72dcf5d0cefc09e053c92bbbf7e9fe9 100644
--- a/demo/Maps.scala
+++ b/demo/Maps.scala
@@ -44,4 +44,8 @@ object Maps {
else
true
} holds
+
+ def findModel(m : Map[Int,Int]) : Boolean = {
+ m != Map.empty[Int,Int].updated(0, 42)
+ } holds
}
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index ad8de4eca2716133a15df539fdb1f06fb44e504a..2b89efb9abbf96111e68338256399569a075027f 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -531,11 +531,9 @@ trait CodeExtraction extends Extractors {
val rf = rec(f)
val rt = rec(t)
val newSingleton = SingletonMap(rf, rt).setType(rm.getType)
- println("singleton: " + newSingleton)
rm.getType match {
case MapType(ft, tt) =>
- println("extracted maptype: " + MapType(ft, tt))
- MapUnion(rm, newSingleton).setType(rm.getType)
+ MapUnion(rm, FiniteMap(Seq(newSingleton)).setType(rm.getType)).setType(rm.getType)
case _ => {
if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
throw ImpureCodeEncounteredException(tree)
diff --git a/src/purescala/AbstractZ3Solver.scala b/src/purescala/AbstractZ3Solver.scala
index b0ae4af3b747aea8e9ba0cfe7fd2b47ee8948516..6d95da313ca2f5fe4529889d4628dec1956b0fc4 100644
--- a/src/purescala/AbstractZ3Solver.scala
+++ b/src/purescala/AbstractZ3Solver.scala
@@ -7,6 +7,9 @@ import Extensions._
import Trees._
import TypeTrees._
+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 {
@@ -24,6 +27,13 @@ trait AbstractZ3Solver {
protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl]
protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl]
+ protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort]
+ protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl]
+ protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl]
+ protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl]
+
protected[purescala] var exprToZ3Id : Map[Expr,Z3AST]
protected[purescala] def fromZ3Formula(tree : Z3AST) : Expr
diff --git a/src/purescala/Evaluator.scala b/src/purescala/Evaluator.scala
index 3a9ab97acf8d4cb6948ae69c1a83a599bc2e6f48..55c9cf7467cf4452d7ef21ad8f26ce6fe3e638d4 100644
--- a/src/purescala/Evaluator.scala
+++ b/src/purescala/Evaluator.scala
@@ -128,6 +128,7 @@ object Evaluator {
(lv,rv) match {
case (FiniteSet(el1),FiniteSet(el2)) => BooleanLiteral(el1.toSet == el2.toSet)
+ case (FiniteMap(el1),FiniteMap(el2)) => BooleanLiteral(el1.toSet == el2.toSet)
case _ => BooleanLiteral(lv == rv)
}
}
@@ -228,6 +229,34 @@ object Evaluator {
case i @ IntLiteral(_) => i
case b @ BooleanLiteral(_) => b
+ case f @ FiniteMap(ss) => FiniteMap(ss.map(rec(ctx,_)).distinct.asInstanceOf[Seq[SingletonMap]]).setType(f.getType)
+ case e @ EmptyMap(_,_) => e
+ case s @ SingletonMap(f,t) => SingletonMap(rec(ctx,f), rec(ctx,t)).setType(s.getType)
+ case g @ MapGet(m,k) => (rec(ctx,m), rec(ctx,k)) match {
+ case (FiniteMap(ss), e) => ss.find(_.from == e) match {
+ case Some(v) => v
+ case None => throw RuntimeErrorEx("key not found: " + e)
+ }
+ case (EmptyMap(ft,tt), e) => throw RuntimeErrorEx("key not found: " + e)
+ // case (SingletonMap(f,t), e) => if (f == e) t else throw RuntimeErrorEx("key not found: " + e)
+ case (l,r) => throw TypeErrorEx(TypeError(l, MapType(r.getType, g.getType)))
+ }
+ case u @ MapUnion(m1,m2) => (rec(ctx,m1), rec(ctx,m2)) match {
+ case (EmptyMap(_,_), r) => r
+ case (l, EmptyMap(_,_)) => l
+ case (f1@FiniteMap(ss1), FiniteMap(ss2)) => {
+ val filtered1 = ss1.filterNot(s => ss2.contains(s))
+ val newSs = filtered1 ++ ss2
+ FiniteMap(newSs).setType(f1.getType)
+ }
+ case (l, r) => throw TypeErrorEx(TypeError(l, m1.getType))
+ }
+ case i @ MapIsDefinedAt(m,k) => (rec(ctx,m), rec(ctx,k)) match {
+ case (EmptyMap(_,_),_) => BooleanLiteral(false)
+ case (FiniteMap(ss), e) => BooleanLiteral(ss.exists(_.from == e))
+ case (l, r) => throw TypeErrorEx(TypeError(l, m.getType))
+ }
+
case Distinct(args) => {
val newArgs = args.map(rec(ctx, _))
BooleanLiteral(newArgs.distinct.size == newArgs.size)
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 4822702df8c803a4a5b3b236bb663c41c66b4dd8..e6320c2c729b5ba201b55cf79aa3009bf88be044 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -100,12 +100,12 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty
- private val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
- private val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- private val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- private val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- private val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- private val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
+ protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
private def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
case Some(z3sort) => z3sort
@@ -391,7 +391,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
val validatingStopwatch = new Stopwatch("validating", false)
val decideTopLevelSw = new Stopwatch("top-level", false).start
- println("Deciding : " + vc)
+ // println("Deciding : " + vc)
initializationStopwatch.start
@@ -504,8 +504,6 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
}
case (Some(true), m) => { // SAT
- println("the model is ")
- println(m)
validatingStopwatch.start
val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
validatingStopwatch.stop
@@ -1003,8 +1001,13 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
assert(argsSize == 2)
Division(rargs(0), rargs(1))
}
+ // case OpAsArray => {
+ // assert(argsSize == 0)
+ //
+ // }
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)
}
}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index e5259abd796b466e584f2a6a561785e4839475bf..a24b4c5c7ca79e934f7c3ef238d1956b3e2462ff 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -395,6 +395,7 @@ object Trees {
case And(args) => Some((args, And.apply))
case Or(args) => Some((args, Or.apply))
case FiniteSet(args) => Some((args, FiniteSet))
+ case FiniteMap(args) => Some((args, (as : Seq[Expr]) => FiniteMap(as.asInstanceOf[Seq[SingletonMap]])))
case FiniteMultiset(args) => Some((args, FiniteMultiset))
case Distinct(args) => Some((args, Distinct))
case _ => None
@@ -1169,7 +1170,8 @@ object Trees {
case CaseClassType(ccd) =>
val fields = ccd.fields
CaseClass(ccd, fields.map(f => simplestValue(f.getType)))
- case SetType(baseType) => FiniteSet(Nil)
+ case SetType(baseType) => FiniteSet(Nil).setType(tpe)
+ case MapType(fromType, toType) => EmptyMap(fromType, toType).setType(tpe)
case _ => throw new Exception("I can't choose simplest value for type " + tpe)
}
}
diff --git a/src/purescala/Z3ModelReconstruction.scala b/src/purescala/Z3ModelReconstruction.scala
index 74f85812d6ff3309fc48b25c5c39d5f26f342d23..0d42c6aaa27f426c04f81b7e46da17920e12fb21 100644
--- a/src/purescala/Z3ModelReconstruction.scala
+++ b/src/purescala/Z3ModelReconstruction.scala
@@ -24,6 +24,21 @@ trait Z3ModelReconstruction {
expectedType match {
case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral(_))
case Int32Type => model.evalAs[Int](z3ID).map(IntLiteral(_))
+ case MapType(kt,vt) => model.eval(z3ID) match {
+ case None => None
+ case Some(t) => model.getArrayValue(t) match {
+ case None => None
+ case Some((map, elseValue)) =>
+ assert(elseValue == mapRangeNoneConstructors(vt)())
+ val singletons = for ((index, value) <- map if z3.getASTKind(value) != mapRangeNoneConstructors(vt)()) yield {
+ z3.getASTKind(value) match {
+ case Z3AppAST(someCons, List(arg)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(fromZ3Formula(index), fromZ3Formula(arg))
+ case _ => scala.Predef.error("unexpected value in map: " + value)
+ }
+ }
+ if (singletons.isEmpty) Some(EmptyMap(kt, vt)) else Some(FiniteMap(singletons.toSeq))
+ }
+ }
case other => model.eval(z3ID) match {
case None => None
case Some(t) => softFromZ3Formula(t)
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index f6f9a424fd2fa6c17d873e9d69e5b7eb5b7c959e..9c9e89894c11853ffafc8515ef48e0a9d3fc2df7 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -11,6 +11,8 @@ import z3plugins.bapa.{BAPATheory, BAPATheoryEqc, BAPATheoryBubbles}
import z3plugins.instantiator.{AbstractInstantiator,Instantiator}
import scala.collection.mutable.{HashMap => MutableHashMap}
+import scala.collection.mutable.{Map => MutableMap}
+import scala.collection.mutable.{Set => MutableSet}
class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction {
import Settings.useBAPA
@@ -94,6 +96,13 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty
+ protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
+ protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+
case class UntranslatableTypeException(msg: String) extends Exception(msg)
private def prepareSorts: Unit = {
import Z3Context.{ADTSortReference, RecursiveType, RegularSort}