From d9055bee37329686a5b8c3d90d1dc69803a4567d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Mon, 18 Apr 2011 12:17:03 +0000
Subject: [PATCH] Script a la 'vs' for constraint programming
---
cp | 23 +++++++++++++++++++
cp-demo/FindAllCalls.scala | 21 ++++--------------
project/build/funcheck.scala | 2 +-
src/cp/CPPlugin.scala | 39 +++++++++++----------------------
src/cp/CallTransformation.scala | 4 ++--
5 files changed, 43 insertions(+), 46 deletions(-)
create mode 100755 cp
diff --git a/cp b/cp
new file mode 100755
index 000000000..2af6bf671
--- /dev/null
+++ b/cp
@@ -0,0 +1,23 @@
+#!/bin/bash
+
+runner="./scalac-cp"
+newargs=""
+
+for arg in $@
+do
+ if [ -e ${arg} ]
+ then
+ newargs="${newargs} ${arg}"
+ else
+ newargs="${newargs} -P:constraint-programming:${arg}"
+ fi
+done
+
+if [ -e ${runner} ]
+then
+ ${runner} ${newargs}
+ exit 0
+else
+ echo "${runner} not found. Have you run 'sbt all' ?"
+ exit 1
+fi
diff --git a/cp-demo/FindAllCalls.scala b/cp-demo/FindAllCalls.scala
index 820acab8b..7a9275ed3 100644
--- a/cp-demo/FindAllCalls.scala
+++ b/cp-demo/FindAllCalls.scala
@@ -126,23 +126,10 @@ object FindAllCalls {
Timer.stop
println("Solution set size: " + set1.size)
- if (set1 != set2) {
- println(set1)
- println(set2)
- assert(false)
- }
- if (set2 != set3) {
- println(set2)
- println(set3)
- assert(false)
- }
- if (set3 != set4) {
- println(set3)
- println(set4)
- assert(false)
- }
-
- println("Fixed size solution set size : " + set5.size)
+ assert(set1 == set2)
+ assert(set1 == set3)
+ assert(set1 == set4)
+ println("Fixed-size solution set size : " + set5.size)
}
/** Printing trees */
diff --git a/project/build/funcheck.scala b/project/build/funcheck.scala
index ae1171d3c..855456fc7 100644
--- a/project/build/funcheck.scala
+++ b/project/build/funcheck.scala
@@ -18,7 +18,7 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
lazy val extensionJars : List[Path] = multisetsLib.jarPath :: multisets.jarPath :: orderedsets.jarPath :: setconstraints.jarPath :: Nil
val scriptPath: Path = "." / "funcheck"
- val cpScriptPath: Path = "." / "cp"
+ val cpScriptPath: Path = "." / "scalac-cp"
lazy val all = task { None } dependsOn(generateScript, generateCpScript) describedAs("Compile everything and produce a script file.")
diff --git a/src/cp/CPPlugin.scala b/src/cp/CPPlugin.scala
index 3bcee3456..6c0db086f 100644
--- a/src/cp/CPPlugin.scala
+++ b/src/cp/CPPlugin.scala
@@ -11,31 +11,23 @@ class CPPlugin(val global: Global) extends Plugin {
val name = "constraint-programming"
val description = "Constraint programming in Scala by LARA."
- var stopAfterAnalysis: Boolean = true
- var stopAfterExtraction: Boolean = false
-
var silentlyTolerateNonPureBodies = false
/** The help message displaying the options for that plugin. */
override val optionsHelp: Option[String] = Some(
- " -P:funcheck:uniqid When pretty-printing funcheck trees, show identifiers IDs" + "\n" +
- " -P:funcheck:with-code Allows the compiler to keep running after the static analysis" + "\n" +
- " -P:funcheck:parse Checks only whether the program is valid PureScala" + "\n" +
- " -P:funcheck:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
- " -P:funcheck:nodefaults Runs only the analyses provided by the extensions" + "\n" +
- " -P:funcheck:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
- " -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
- " -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:impure Generate testcases only for impure functions" + "\n" +
- " -P:funcheck:testcases=[1,2] Number of testcases to generate per function" + "\n" +
- " -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
- " -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
- " -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
- " -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."
+ " -P:constraint-programming:uniqid When pretty-printing funcheck trees, show identifiers IDs" + "\n" +
+ " -P:constraint-programming:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
+ " -P:constraint-programming:nodefaults Runs only the analyses provided by the extensions" + "\n" +
+ " -P:constraint-programming:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
+ " -P:constraint-programming:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
+ " -P:constraint-programming:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
+ " -P:constraint-programming:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
+ " -P:constraint-programming:nobapa Disable BAPA Z3 extension" + "\n" +
+ " -P:constraint-programming:XP Enable weird transformations and other bug-producing features" + "\n" +
+ " -P:constraint-programming:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
+ " -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."
)
/** Processes the command-line options. */
@@ -43,14 +35,11 @@ class CPPlugin(val global: Global) extends Plugin {
override def processOptions(options: List[String], error: String => Unit) {
for(option <- options) {
option match {
- case "with-code" => stopAfterAnalysis = false
case "uniqid" => purescala.Settings.showIDs = true
- case "parse" => stopAfterExtraction = true
case "tolerant" => silentlyTolerateNonPureBodies = true
case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case "axioms" => purescala.Settings.noForallAxioms = false
case "nobapa" => purescala.Settings.useBAPA = false
- case "impure" => purescala.Settings.impureTestcases = true
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.useFairInstantiator = false; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
@@ -60,8 +49,6 @@ class CPPlugin(val global: Global) extends Plugin {
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))
- case s if s.startsWith("testbounds=") => purescala.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
- case s if s.startsWith("testcases=") => purescala.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
case _ => error("Invalid option: " + option)
}
}
diff --git a/src/cp/CallTransformation.scala b/src/cp/CallTransformation.scala
index ab8a96f58..5acd16293 100644
--- a/src/cp/CallTransformation.scala
+++ b/src/cp/CallTransformation.scala
@@ -301,8 +301,8 @@ object CallTransformation {
import Definitions.UnsatisfiableConstraintException
import Definitions.UnknownConstraintException
- private def newSolver() = new FairZ3Solver(new QuietReporter())
- // private def newSolver() = new FairZ3Solver(new purescala.DefaultReporter())
+ private def newReporter() = new QuietReporter()
+ private def newSolver() = new FairZ3Solver(newReporter())
def chooseExec(progString : String, progId : Int, exprString : String, exprId : Int, outputVarsString : String, outputVarsId : Int, inputConstraints : Expr) : Seq[Expr] = {
val program = deserialize[Program](progString, progId)
--
GitLab