From b1717ead01394101b70789cb9f13af845aeb1c62 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 7 Oct 2010 15:49:53 +0000
Subject: [PATCH]
---
WISHLIST | 1 +
src/funcheck/FunCheckPlugin.scala | 2 ++
src/purescala/Settings.scala | 1 +
src/purescala/Z3Solver.scala | 4 ++--
4 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/WISHLIST b/WISHLIST
index ad101dd4e..f3f3f786d 100644
--- a/WISHLIST
+++ b/WISHLIST
@@ -5,6 +5,7 @@ PS: rewrite pattern-matching translator to use if-then-else
PS: generate VCs for preconditions
PS: generate VCs for pattern-matching
PS: support multiple top-level objects, and use 'private' accessor to indicate what's part of the interface
+PS: support tuples (including natively in Z3)
Wishes granted so far
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 826e99d2d..4a580fa23 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -27,6 +27,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
" -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
" -P:funcheck:nobapa Disable BAPA Z3 extension" + "\n" +
+ " -P:funcheck:newPM Use the new pattern-matching translator" + "\n" +
" -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features"
)
@@ -44,6 +45,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case "axioms" => purescala.Settings.noForallAxioms = false
case "nobapa" => purescala.Settings.useBAPA = false
+ case "newPM" => purescala.Settings.useNewPatternMatchingTranslator = true
case "XP" => purescala.Settings.experimental = 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)): _*)
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 8be325547..51225d73f 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -13,4 +13,5 @@ object Settings {
var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0
var useBAPA: Boolean = true
+ var useNewPatternMatchingTranslator: Boolean = false
}
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 25073c324..f85158b62 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -9,7 +9,7 @@ import TypeTrees._
import z3plugins.bapa.{BAPATheory, BAPATheoryEqc, BAPATheoryBubbles}
-class Z3Solver(reporter: Reporter) extends Solver(reporter) {
+class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstruction {
import Settings.useBAPA
val description = "Z3 Solver"
override val shortDescription = "Z3"
@@ -23,7 +23,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
// this is fixed
private val z3cfg = new Z3Config(
"MODEL" -> true,
- "SOFT_TIMEOUT" -> 180000, // this one doesn't work apparently
+ "SOFT_TIMEOUT" -> 100,
"TYPE_CHECK" -> true,
"WELL_SORTED_CHECK" -> true
)
--
GitLab