From be10ccd399d9e60e2da52138842cfe3fcc431413 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 12 Jan 2011 13:03:40 +0000
Subject: [PATCH] laid the groundwork for new instantiator
---
WISHLIST | 11 ++++++-----
src/funcheck/FunCheckPlugin.scala | 6 ++++--
src/purescala/Settings.scala | 2 ++
src/purescala/Z3Solver.scala | 9 +++++----
.../z3plugins/instantiator/Instantiator.scala | 2 +-
testcases/ListWithSize.scala | 2 +-
6 files changed, 19 insertions(+), 13 deletions(-)
diff --git a/WISHLIST b/WISHLIST
index 20fdc0402..f5e81b5f4 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 03031e9b3..1d27e3f21 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 a4e330799..c3ffa74ec 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 70e94b608..eba8fffd0 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 ef86f9a9e..74f571ecd 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 df2522cb8..49e08b9da 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
--
GitLab