No commit message

No commit message

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

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)): _*)

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
 }

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
     )