diff --git a/WISHLIST b/WISHLIST
index 20fdc0402f668061ee7100a9af7983d9ac851742..f5e81b5f4f9a6f8e64a1de51e42bd6045c030302 100644
--- a/WISHLIST
+++ b/WISHLIST
@@ -1,13 +1,10 @@
Add here what you would love FunCheck to be able to do
------------------------------------------------------
-PS: generate VCs for preconditions
-PS: generate VCs for pattern-matching
PS: support multiple top-level objects
-PS: use 'private' accessor to indicate what's part of the interface
PS: support tuples (including natively in Z3)
-PS: implement @induct tactic
-PS: use a theory plugin to instantiate/unroll function bodies
+PS: implement @induct tactic, completely, not just for one arg
+PS: instantiate/unroll function bodies in a fair way, to guarantee termination
Wishes granted so far
---------------------
@@ -15,3 +12,7 @@ Wishes granted so far
PS: create a wishlist
PS: rewrite pattern-matching translator to use if-then-else
VK: add IsValid class to allow for writing just "holds" in place of ensuring(_ == true)
+PS: generate VCs for preconditions
+PS: generate VCs for pattern-matching
+PS: use 'private' accessor to indicate what's part of the interface
+PS: use a theory plugin to instantiate/unroll function bodies
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 03031e9b345343df480bd410c064a5f6a90297e3..1d27e3f215eb26f9b9c03dcc8658776354ead15c 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -29,7 +29,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:nobapa Disable BAPA Z3 extension" + "\n" +
" -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
- " -P:funcheck:PLDI PLDI 2011 settings. Subject to change. Same warning as for XP."
+ " -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
+ " -P:funcheck:CAV CAV 2011 settings. In progress."
)
/** Processes the command-line options. */
@@ -47,7 +48,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "nobapa" => purescala.Settings.useBAPA = false
case "newPM" => { println("''newPM'' is no longer a command-line option, because the new translation is now on by default."); System.exit(0) }
case "XP" => purescala.Settings.experimental = true
- case "PLDI" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
+ case "PLDI" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = true; purescala.Settings.useFairInstantiator = false; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
+ case "CAV" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index a4e3307993de125401a5faf94375ca1a37731c0a..c3ffa74eccb825897ad9aecf8fea89555a50818b 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -15,4 +15,6 @@ object Settings {
var zeroInlining : Boolean = false
var useBAPA: Boolean = true
var useInstantiator: Boolean = false
+ var useFairInstantiator: Boolean = false
+ def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
}
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 70e94b608f43054586ab3f1db7474a29d5a96977..eba8fffd03a65a16862d93f6e53b1ac699f91bfa 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -8,13 +8,13 @@ import Trees._
import TypeTrees._
import z3plugins.bapa.{BAPATheory, BAPATheoryEqc, BAPATheoryBubbles}
-import z3plugins.instantiator.Instantiator
+import z3plugins.instantiator.{AbstractInstantiator,Instantiator,FairInstantiator}
import scala.collection.mutable.{HashMap => MutableHashMap}
class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReconstruction {
import Settings.useBAPA
- import Settings.useInstantiator
+ import Settings.{useInstantiator,useFairInstantiator,useAnyInstantiator}
val description = "Z3 Solver"
override val shortDescription = "Z3"
@@ -37,7 +37,7 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
protected[purescala] var z3: Z3Context = null
protected[purescala] var program: Program = null
private var bapa: BAPATheoryType = null
- private var instantiator: Instantiator = null
+ private var instantiator: AbstractInstantiator = null
private var neverInitialized = true
private val IntSetType = SetType(Int32Type)
@@ -55,7 +55,8 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
z3 = new Z3Context(z3cfg)
// z3.traceToStdout
if (useBAPA) bapa = new BAPATheoryType(z3)
- if (useInstantiator) instantiator = new Instantiator(this)
+ if (useInstantiator) instantiator = new Instantiator(this) else
+ if (useFairInstantiator) instantiator = new FairInstantiator(this)
exprToZ3Id = Map.empty
z3IdToExpr = Map.empty
diff --git a/src/purescala/z3plugins/instantiator/Instantiator.scala b/src/purescala/z3plugins/instantiator/Instantiator.scala
index ef86f9a9eef2c0682f8a88bd13aa16d5a2738c3e..74f571ecd5099d19e9428eda284541c4b95c74cc 100644
--- a/src/purescala/z3plugins/instantiator/Instantiator.scala
+++ b/src/purescala/z3plugins/instantiator/Instantiator.scala
@@ -14,7 +14,7 @@ import purescala.PartialEvaluator
import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
import scala.collection.mutable.PriorityQueue
-class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instantiator") {
+class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instantiator") with AbstractInstantiator {
import z3Solver.{z3,program,typeToSort,fromZ3Formula,toZ3Formula}
val partialEvaluator = new PartialEvaluator(program)
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index df2522cb88aee9dd8ba7137c355fc65064f02f59..49e08b9da9fdabf643d6115820142cbb5b71c861 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -18,7 +18,7 @@ object ListWithSize {
def size(l: List) : Int = (l match {
case Nil() => 0
case Cons(_, t) => 1 + size(t)
- }) ensuring(_ >= 0)
+ }) ensuring(res => res >= 0)
def iplSize(l: IntPairList) : Int = (l match {
case IPNil() => 0