From 2712fddb8cb60802a40d4b62697795e25af792c1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Fri, 20 May 2011 13:27:51 +0000
Subject: [PATCH] perform lucky tests by default at it substantially helps
finding models
---
src/cp/CPPlugin.scala | 2 ++
src/cp/RuntimeSettings.scala | 1 +
src/funcheck/FunCheckPlugin.scala | 4 ++--
src/purescala/Settings.scala | 2 +-
4 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/cp/CPPlugin.scala b/src/cp/CPPlugin.scala
index 3c8a14418..fd0d3b64e 100644
--- a/src/cp/CPPlugin.scala
+++ b/src/cp/CPPlugin.scala
@@ -28,6 +28,7 @@ class CPPlugin(val global: Global) extends Plugin {
" -P:constraint-programming:CAV CAV 2011 settings. In progress." + "\n" +
" -P:constraint-programming:prune (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
" -P:constraint-programming:cores (with CAV) Use UNSAT cores in the unrolling/refinement step." + "\n" +
+ " -P:constraint-programming:noLuckyTests (with CAV) Do not perform additional tests to potentially find models early." + "\n" +
" -P:constraint-programming:scalaEval (with CAV) Use functions stored in constraints to evaluate models."
)
@@ -47,6 +48,7 @@ class CPPlugin(val global: Global) extends Plugin {
case "CAV" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case "prune" => purescala.Settings.pruneBranches = true
case "cores" => purescala.Settings.useCores = true
+ case "noLuckyTests" => purescala.Settings.luckyTest = false
case "scalaEval" => cp.Settings.useScalaEvaluator = 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/cp/RuntimeSettings.scala b/src/cp/RuntimeSettings.scala
index 813ebb884..051ea9b94 100644
--- a/src/cp/RuntimeSettings.scala
+++ b/src/cp/RuntimeSettings.scala
@@ -12,6 +12,7 @@ package cp
var useCores : Boolean = purescala.Settings.useCores
var pruneBranches : Boolean = purescala.Settings.pruneBranches
var solverTimeout : Option[Int] = purescala.Settings.solverTimeout
+ var luckyTest : Boolean = purescala.Settings.luckyTest
var useScalaEvaluator : Boolean = Settings.useScalaEvaluator
}
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 08945e8d8..8180ef78c 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -37,7 +37,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
" -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" +
" -P:funcheck:prune (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
" -P:funcheck:cores (with CAV) Use UNSAT cores in the unrolling/refinement step." + "\n" +
- " -P:funcheck:lucky (with CAV) Perform additional tests to potentially find models early."
+ " -P:funcheck:noLuckyTests (with CAV) Do not perform additional tests to potentially find models early."
)
/** Processes the command-line options. */
@@ -59,7 +59,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
case "CAV" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case "prune" => purescala.Settings.pruneBranches = true
case "cores" => purescala.Settings.useCores = true
- case "lucky" => purescala.Settings.luckyTest = true
+ case "noLuckyTests" => purescala.Settings.luckyTest = false
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 a872ad20e..555e07958 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -21,5 +21,5 @@ object Settings {
var pruneBranches : Boolean = false
def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
var solverTimeout : Option[Int] = None
- var luckyTest : Boolean = false
+ var luckyTest : Boolean = true
}
--
GitLab