diff --git a/build.sbt b/build.sbt
index a6757eeca215c7453ebd8bc42d9103d2d21656a8..c4afd1266752e5c23ba014df2859304ee75e4ce3 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,13 +4,13 @@ version := "2.3"
organization := "ch.epfl.lara"
-scalaVersion := "2.10.2"
+scalaVersion := "2.11.1"
-scalacOptions += "-deprecation"
-
-scalacOptions += "-unchecked"
-
-scalacOptions += "-feature"
+scalacOptions ++= Seq(
+ "-deprecation",
+ "-unchecked",
+ "-feature"
+)
javacOptions += "-Xlint:unchecked"
@@ -23,25 +23,21 @@ if(System.getProperty("sun.arch.data.model") == "64") {
resolvers += "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/"
libraryDependencies ++= Seq(
- "org.scala-lang" % "scala-compiler" % "2.10.2",
- "org.scalatest" % "scalatest_2.10" % "2.0.M5b" % "test" excludeAll(ExclusionRule(organization="org.scala-lang")),
- "junit" % "junit" % "4.8" % "test",
- "com.typesafe.akka" %% "akka-actor" % "2.2.0" excludeAll(ExclusionRule(organization="org.scala-lang"))
+ "org.scala-lang" % "scala-compiler" % "2.11.1",
+ "org.scalatest" %% "scalatest" % "2.2.0" % "test",
+ "com.typesafe.akka" %% "akka-actor" % "2.3.4"
)
Keys.fork in run := true
Keys.fork in test := true
-logBuffered in Test := false
+logBuffered in test := false
-testOptions in Test += Tests.Argument("-oD")
+testOptions in test += Tests.Argument("-oD")
javaOptions in test += "-Xss32M"
-parallelExecution in Test := false
+parallelExecution in test := false
sourcesInBase in Compile := false
-
-// do not skip parent Eclipse project definition
-EclipseKeys.skipParents in ThisBuild := false
diff --git a/project/Build.scala b/project/Build.scala
index 87440e748e9e9347f00a76fac67d7b6a6e2874d6..1d9e5787079bdc800c0fb84c0a383ce9242630ea 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -4,114 +4,69 @@ import Keys._
object Leon extends Build {
private val scriptName = "leon"
- private val setupScriptName = "setupenv"
- private val benchScriptName = "leon-bench"
def scriptFile = file(".") / scriptName
- def benchScriptFile = file(".") / benchScriptName
- def setupScriptFile = file(".") / setupScriptName
def is64 = System.getProperty("sun.arch.data.model") == "64"
def ldLibraryDir32 = file(".") / "lib-bin" / "32"
def ldLibraryDir64 = file(".") / "lib-bin" / "64"
val cleanTask = TaskKey[Unit]("clean", "Cleans up the generated binaries and scripts.") <<= (streams, clean) map { (s,c) =>
- c
if(scriptFile.exists && scriptFile.isFile) {
scriptFile.delete
}
- if(setupScriptFile.exists && setupScriptFile.isFile) {
- setupScriptFile.delete
- }
- if(benchScriptFile.exists && benchScriptFile.isFile) {
- benchScriptFile.delete
- }
}
val nl = System.getProperty("line.separator")
- val setupScriptTask = TaskKey[Seq[String]]("setup", "Generate the " + setupScriptName + " Bash script")
-
- val setupSetting = setupScriptTask <<= (streams, dependencyClasspath in Compile, classDirectory in Compile) map { (s, deps, out) =>
-
- val depsPaths = deps.map(_.data.absolutePath)
-
- val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
- case None => throw new Exception("Couldn't guess SCALA_HOME.")
- case Some(p) => p.substring(0, p.length - 21)
- }
+ val scriptTask = TaskKey[Unit]("script", "Generate the leon Bash script") <<= (streams, dependencyClasspath in Compile, classDirectory in Compile, resourceDirectory in Compile) map { (s, cps, out, res) =>
+ try {
+ val f = file("leon")
+ // Paths discovery
+ if(f.exists) {
+ s.log.info("Regenerating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+ f.delete
+ } else {
+ s.log.info("Generating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+ }
- val ldLibPath = if (is64) ldLibraryDir64.absolutePath else ldLibraryDir32.absolutePath
+ val paths = (res.getAbsolutePath +: out.getAbsolutePath +: cps.map(_.data.absolutePath)).mkString(":")
- // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
- s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
+ IO.write(f, s"""|#!/bin/bash --posix
+ |
+ |SCALACLASSPATH="$paths"
+ |
+ |java -Xmx2G -Xms512M -classpath $${SCALACLASSPATH} -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath $${SCALACLASSPATH} leon.Main $$@ 2>&1 | tee last.log
+ |""".stripMargin)
- if (setupScriptFile.exists) {
- s.log.info("Regenerating '"+setupScriptFile.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
- setupScriptFile.delete
- } else {
- s.log.info("Generating '"+setupScriptFile.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+ f.setExecutable(true)
+ } catch {
+ case e: Throwable =>
+ s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
}
- val sfw = new java.io.FileWriter(setupScriptFile)
- sfw.write("#!/bin/bash --posix" + nl)
- if (!is64) {
- sfw.write("if [ `uname -m` == \"x86_64\" ]; then "+nl)
- sfw.write(" echo \"It appears you have compiled Leon with a 32bit virtual machine, but are now trying to run it on a 64bit architecture. This is unfortunately not supported.\"" + nl)
- sfw.write(" exit -1" + nl)
- sfw.write("fi"+ nl)
- }
- sfw.write("export LD_LIBRARY_PATH=\""+ldLibPath+"\"" + nl)
-
- val libFiles = file("library") ** "*.scala"
-
- sfw.write("export LEON_LIBFILES=\""+libFiles.getPaths.mkString(" ")+"\"" + nl)
- sfw.write("export SCALA_HOME=\""+scalaHomeDir+"\"" + nl)
- sfw.close
- setupScriptFile.setExecutable(true)
-
- (out.absolutePath +: depsPaths)
}
- def genRunnerTask(taskName: String, file: File, name: String, mainClass: String) = {
- TaskKey[Unit](taskName, "Generate the " + name + " Bash script") <<= (streams, setupScriptTask, resourceDirectory in Compile) map { (s, cps, res) =>
- try {
- // Paths discovery
- if(file.exists) {
- s.log.info("Regenerating '"+file.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
- file.delete
- } else {
- s.log.info("Generating '"+file.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
- }
+ val sourceGen = {
+ sourceGenerators in Compile += Def.task {
+ val libFiles = (file("library") ** "*.scala").getPaths.mkString("List(\"", "\", \"", "\")")
- val fw = new java.io.FileWriter(file)
- fw.write("#!/bin/bash --posix" + nl)
+ val build = (sourceManaged in Compile).value / "leon" / "Build.scala";
- fw.write("SCALACLASSPATH=\"")
- fw.write((res.getAbsolutePath +: cps).mkString(":"))
- fw.write("\"" + nl + nl)
+ IO.write(build, s"""|package leon;
+ |
+ |object Build {
+ |val libFiles = $libFiles;
+ |}""".stripMargin)
- fw.write("source "+setupScriptFile.getAbsolutePath()+nl)
- // the Java command that uses sbt's local Scala to run the whole contraption.
- fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"$SCALA_HOME\" -Dscala.usejavacp=false ")
- fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
- fw.write(mainClass+" $@ 2>&1 | tee last.log" + nl)
- fw.close
- file.setExecutable(true)
- } catch {
- case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
- }
- }
+ Seq(build)
+ }.taskValue
}
- val scriptTask = genRunnerTask("script", scriptFile, scriptName, "leon.Main")
- val benchTask = genRunnerTask("bench", benchScriptFile, benchScriptName, "leon.synthesis.utils.Benchmarks")
-
object LeonProject {
val settings = Seq(
- setupSetting,
scriptTask,
- benchTask,
- cleanTask
+ cleanTask,
+ sourceGen
)
}
diff --git a/project/build.properties b/project/build.properties
index 4474a03e1aa9671540ef1677b5579ef91481f503..be6c454fbaca75cd249c483b6a64515d6d52fd8c 100644
--- a/project/build.properties
+++ b/project/build.properties
@@ -1 +1 @@
-sbt.version=0.12.1
+sbt.version=0.13.5
diff --git a/project/plugins.sbt b/project/plugins.sbt
deleted file mode 100644
index c2371be43444b9e9b99a0ae3b34b9c69969956d9..0000000000000000000000000000000000000000
--- a/project/plugins.sbt
+++ /dev/null
@@ -1 +0,0 @@
-addSbtPlugin("com.typesafe.sbteclipse" % "sbteclipse-plugin" % "2.1.0")
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 66034599f2524a3a4d3005d7849641fb21b17a6b..702ef9c2e07d4b60d2670031262bd8d1f76ce568 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -11,33 +11,5 @@ case class Settings(
val synthesis: Boolean = false,
val xlang: Boolean = false,
val verify: Boolean = true,
- val injectLibrary: Boolean = false,
- val classPath: List[String] = Settings.defaultClassPath()
+ val injectLibrary: Boolean = false
)
-
-object Settings {
- // This is a list of directories that is passed as class-path of the inner-compiler.
- // It needs to contain at least a directory containing scala-library.jar, and
- // one for the leon runtime library.
-
- private def defaultClassPath() = {
- val scalaHome = System.getenv("SCALA_HOME")
- assert(scalaHome ne null, "SCALA_HOME was not found in the environment, did you run `source setupenv.sh` ?")
-
- if (scalaHome != "") {
- val f = new java.io.File(scalaHome+"/lib")
-
- f.listFiles().collect {
- case f if f.getPath().endsWith(".jar") => f.getAbsolutePath()
- }.toList
-
- } else {
- Nil
- }
- }
-
- private[leon] def defaultLibFiles() = {
- Option(System.getenv("LEON_LIBFILES")).map(_.split(" ").toList).getOrElse(Nil)
- }
-
-}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 5c988ebd73615d970d59de8478e2dbb6828a073a..f387182d8257e30a433db9aa3c314054b9498202 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -120,11 +120,10 @@ trait ASTExtractors {
object ExEnsuredExpression {
/** Extracts the 'ensuring' contract from an expression. */
- def unapply(tree: Apply): Option[(Tree,Symbol,Tree)] = tree match {
- case Apply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "any2Ensuring"), TypeTree() :: Nil),
- body :: Nil), ExNamed("ensuring")),
+ def unapply(tree: Apply): Option[(Tree,ValDef,Tree)] = tree match {
+ case Apply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "Ensuring"), _ :: Nil), body :: Nil), ExNamed("ensuring")),
(Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, contractBody)) :: Nil)
- => Some((body, vd.symbol, contractBody))
+ => Some((body, vd, contractBody))
case _ => None
}
}
@@ -166,7 +165,7 @@ trait ASTExtractors {
* visibility. Does not match on the automatically generated companion
* objects of case classes (or any synthetic class). */
def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
- case ClassDef(_, name, tparams, impl) if ((cd.symbol.isModuleClass || cd.symbol.isPackage) && tparams.isEmpty && !cd.symbol.isSynthetic) => {
+ case ClassDef(_, name, tparams, impl) if ((cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic) => {
Some((name.toString, impl))
}
case _ => None
@@ -186,14 +185,14 @@ trait ASTExtractors {
}
object ExCaseClass {
- def unapply(cd: ClassDef): Option[(String,Symbol,Seq[(String,Tree)], Template)] = cd match {
+ def unapply(cd: ClassDef): Option[(String,Symbol,Seq[(String, ValDef)], Template)] = cd match {
case ClassDef(_, name, tparams, impl) if (cd.symbol.isCase && !cd.symbol.isAbstractClass && impl.body.size >= 8) => {
val constructor: DefDef = impl.children.find(child => child match {
case ExConstructorDef() => true
case _ => false
}).get.asInstanceOf[DefDef]
- val args = constructor.vparamss.flatten.map(vd => (vd.name.toString, vd.tpt))
+ val args = constructor.vparamss.flatten.map(vd => (vd.name.toString, vd))
Some((name.toString, cd.symbol, args, impl))
}
@@ -409,7 +408,7 @@ trait ASTExtractors {
case _ => None
}
// Match e1 -> e2
- case Apply(TypeApply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "any2ArrowAssoc"), List(tpeFrom)), List(from)), ExNamed("$minus$greater")), List(tpeTo)), List(to)) =>
+ case Apply(TypeApply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "ArrowAssoc"), List(tpeFrom)), List(from)), ExNamed("$minus$greater")), List(tpeTo)), List(to)) =>
Some((Seq(tpeFrom.tpe, tpeTo.tpe), Seq(from, to)))
case _ => None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index e77b25d5058980483c802112104163e2a8d59c78..3a98f859a8b6805e0638fc95a00f9946e7f3107a 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -237,7 +237,7 @@ trait CodeExtraction extends ASTExtractors {
}
- private var seenClasses = Map[Symbol, (Seq[(String, Tree)], Template)]()
+ private var seenClasses = Map[Symbol, (Seq[(String, ValDef)], Template)]()
private var classesToClasses = Map[Symbol, LeonClassDef]()
@@ -318,10 +318,9 @@ trait CodeExtraction extends ASTExtractors {
private var isMethod = Set[Symbol]()
private var methodToClass = Map[FunDef, LeonClassDef]()
- def extractClassDef(sym: Symbol, args: Seq[(String, Tree)], tmpl: Template): LeonClassDef = {
+ def extractClassDef(sym: Symbol, args: Seq[(String, ValDef)], tmpl: Template): LeonClassDef = {
val id = FreshIdentifier(sym.name.toString).setPos(sym.pos)
-
val tparamsMap = sym.tpe match {
case TypeRef(_, _, tps) =>
extractTypeParams(tps)
@@ -363,7 +362,8 @@ trait CodeExtraction extends ASTExtractors {
classesToClasses += sym -> ccd
val fields = args.map { case (name, t) =>
- val tpe = toPureScalaType(t.tpe)(defCtx, sym.pos)
+ val tpt = t.tpt
+ val tpe = toPureScalaType(tpt.tpe)(defCtx, sym.pos)
LeonValDef(FreshIdentifier(name).setType(tpe).setPos(t.pos), tpe).setPos(t.pos)
}
@@ -714,9 +714,9 @@ trait CodeExtraction extends ASTExtractors {
var rest = tmpRest
val res = current match {
- case ExEnsuredExpression(body, resSym, contract) =>
- val resId = FreshIdentifier(resSym.name.toString).setType(extractType(current)).setPos(resSym.pos)
- val post = extractTree(contract)(dctx.withNewVar(resSym -> (() => Variable(resId))))
+ case ExEnsuredExpression(body, resVd, contract) =>
+ val resId = FreshIdentifier(resVd.symbol.name.toString).setType(extractType(current)).setPos(resVd.pos)
+ val post = extractTree(contract)(dctx.withNewVar(resVd.symbol -> (() => Variable(resId))))
val b = try {
extractTree(body)
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index f538a0d92df9272f925448e0687d115734a1f787..06658e31d33f298d042a7d37ccddcc2a71311697 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -21,11 +21,19 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
val settings = new NSCSettings
- settings.classpath.value = ctx.settings.classPath.mkString(":")
+ val neededClasses = List[Class[_]](
+ scala.Predef.getClass
+ )
+
+ val urls = neededClasses.map(_.getProtectionDomain().getCodeSource().getLocation())
+ val classpath = urls.map(_.getPath).mkString(":")
+
+ settings.classpath.value = classpath
settings.usejavacp.value = false
+ settings.Yrangepos.value = true
settings.skip.value = List("patmat")
- val libFiles = Settings.defaultLibFiles()
+ val libFiles = Build.libFiles
val injected = if (ctx.settings.injectLibrary) {
libFiles
diff --git a/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala b/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
index dfb76662489ef9c79d269b1bb80b7beb86fbbb44..55afa914fb1fd662051fef96d178063a29b3480f 100644
--- a/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
+++ b/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
@@ -4,9 +4,9 @@ package leon
package frontends.scalac
import scala.tools.nsc.{Global,Settings=>NSCSettings}
-import scala.tools.nsc.interactive.RangePositions
+import scala.reflect.internal.Positions
-class ScalaCompiler(settings : NSCSettings, ctx: LeonContext) extends Global(settings, new SimpleReporter(settings, ctx.reporter)) with RangePositions {
+class ScalaCompiler(settings : NSCSettings, ctx: LeonContext) extends Global(settings, new SimpleReporter(settings, ctx.reporter)) with Positions {
object leonExtraction extends {
val global: ScalaCompiler.this.type = ScalaCompiler.this
diff --git a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
index 62cf0773aeecfbed8cf9520ed5a7084b23149067..be51f8b6393efe2ac354694b8977f2e723431fe4 100644
--- a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
+++ b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
@@ -42,7 +42,7 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab
/** Prints the message with the given position indication. */
def printMessage(posIn: Position, msg: String, severity: Severity) {
val pos = if (posIn eq null) NoPosition
- else if (posIn.isDefined) posIn.inUltimateSource(posIn.source)
+ else if (posIn.isDefined) posIn.finalPosition
else posIn
pos match {
case FakePos(fmsg) =>
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 22c0bf885b32a3d53447b58291dddfd8850f527a..2ec8bacff230378cccd6d7f1b7d31d96435355be 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -110,7 +110,8 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
reporter.debug("- Model validated.")
(true, asMap)
- case EvaluationResults.Successful(BooleanLiteral(false)) =>
+ case EvaluationResults.Successful(res) =>
+ assert(res == BooleanLiteral(false), "Checking model returned non-boolean")
reporter.debug("- Invalid model.")
(false, asMap)
diff --git a/src/main/scala/leon/synthesis/ManualSearch.scala b/src/main/scala/leon/synthesis/ManualSearch.scala
index 137d79c6828e0599cdc71ec830d72c764e2bb555..b7e728d236d8855579ada9c6262b9b6608efcc2c 100644
--- a/src/main/scala/leon/synthesis/ManualSearch.scala
+++ b/src/main/scala/leon/synthesis/ManualSearch.scala
@@ -28,9 +28,9 @@ class ManualSearch(synth: Synthesizer,
}
}
- def title(str: String) = "\033[1m"+str+"\033[0m"
- def failed(str: String) = "\033[31m"+str+"\033[0m"
- def solved(str: String) = "\033[32m"+str+"\033[0m"
+ def title(str: String) = "\u001b[1m" + str + "\u001b[0m"
+ def failed(str: String) = "\u001b[31m" + str + "\u001b[0m"
+ def solved(str: String) = "\u001b[32m" + str + "\u001b[0m"
def displayApp(app: RuleInstantiation): String = {
f"(${costModel.ruleAppCost(app).value}%3d) $app"
@@ -116,7 +116,7 @@ class ManualSearch(synth: Synthesizer,
print("Next action? (q to quit) "+cd.mkString(" ")+" $ ")
val line = if (cmdQueue.isEmpty) {
- readLine()
+ scala.io.StdIn.readLine()
} else {
val n = cmdQueue.head
println(n)
diff --git a/src/main/scala/leon/utils/ASCIITable.scala b/src/main/scala/leon/utils/ASCIITable.scala
index 0daba6f96182fa2aa671c2279df7e7829ac9c333..4d32206ad70af1df6916e9fdd11e0f5f3095d9ce 100644
--- a/src/main/scala/leon/utils/ASCIITable.scala
+++ b/src/main/scala/leon/utils/ASCIITable.scala
@@ -41,7 +41,7 @@ object ASCIITables {
for (k @ (from, to) <- toRemove) {
val min = constraints(k)
- val parts = (from to to).map(i => constraints((i, i)))
+ val parts = (from to to).map(i => constraints.getOrElse((i, i), 1))
var sum = parts.sum
@@ -59,7 +59,7 @@ object ASCIITables {
constraints -= k
}
- (0 until cellsPerRow).map(i => constraints((i, i)))
+ (0 until cellsPerRow).map(i => constraints.getOrElse((i, i), 1))
}
def render: String = {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index b884d229eab7523405ee81765961b231732f6d87..a504b478f0a7243f45e8359b790d9f3f6c2c0059 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -7,7 +7,7 @@ import purescala.Definitions.FunDef
class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
import scala.math.Ordering.Implicits._
- val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortBy(vc => (vc.funDef.id.name, vc.kind))
+ val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortBy(vc => (vc.funDef.id.name, vc.kind.toString))
lazy val totalConditions : Int = conditions.size
diff --git a/src/main/scala/leon/z3plugins/bapa/AST.scala b/src/main/scala/leon/z3plugins/bapa/AST.scala
deleted file mode 100644
index a214d91cfd2f930d5756cd8bd0e0cf726e2da78b..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/AST.scala
+++ /dev/null
@@ -1,103 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package purescala.z3plugins.bapa
-
-import scala.language.implicitConversions
-
-import z3.scala._
-
-object AST {
-
- /* AST */
- case class IllegalTerm(tree: Tree) extends Exception(tree + " should not be present in the formula.")
-
- sealed abstract class Tree {
- override def toString = PrettyPrinter(this)
- def ||(tree: Tree) = Op(OR, Seq(this, tree))
- def &&(tree: Tree) = Op(AND, Seq(this, tree))
- def unary_! = Op(NOT, Seq(this))
- def iff(tree: Tree) = Op(IFF, Seq(this, tree))
- def ===(tree: Tree) = Op(EQ, Seq(this, tree))
- def =!=(tree: Tree) = !(this === tree)
- def <(tree: Tree) = Op(LT, Seq(this, tree))
- def <=(tree: Tree) = !(tree < this)
- def >(tree: Tree) = tree < this
- def >=(tree: Tree) = !(this < tree)
- def seteq(tree: Tree) = Op(SETEQ, Seq(this, tree))
- def subseteq(tree: Tree) = Op(SUBSETEQ, Seq(this, tree))
- def +(tree: Tree) = Op(ADD, Seq(this, tree))
-// def ifThenElse(thenn: Tree, elze: Tree) = Op(ITE, Seq(this, thenn, elze))
- def card = Op(CARD, Seq(this))
- def ++(tree: Tree) = Op(UNION, Seq(this, tree))
- def **(tree: Tree) = Op(INTER, Seq(this, tree))
- def --(tree: Tree) = this ** ~tree
- def unary_~ = Op(COMPL, Seq(this))
- }
- case class Op(op: Operand, args: Seq[Tree]) extends Tree
- case class Lit(lit: Literal) extends Tree
- case class Var(sym: Symbol) extends Tree
-
- /* Literals */
- sealed abstract class Literal
- case object TrueLit extends Literal
- case object FalseLit extends Literal
- case class IntLit(value: Int) extends Literal
- case object EmptySetLit extends Literal
- case object FullSetLit extends Literal
-
- val True = Lit(TrueLit)
- val False = Lit(FalseLit)
-// val Zero = Lit(IntLit(0))
-// val One = Lit(IntLit(1))
- val EmptySet = Lit(EmptySetLit)
- val FullSet = Lit(FullSetLit)
-
- implicit def int2tree(i: Int) = Lit(IntLit(i))
-
- /* Operands */
-
- sealed abstract class Operand(val name: String) {
- override def toString = name
- }
- // return booleans
- case object OR extends Operand("||")
- case object AND extends Operand("&&")
- case object NOT extends Operand("!")
- case object IFF extends Operand("<=>")
- case object EQ extends Operand("==")
- case object LT extends Operand("<")
- case object SETEQ extends Operand("seteq")
- case object SUBSETEQ extends Operand("subseteq")
- // return integers
- case object ADD extends Operand("+")
- case object CARD extends Operand("CARD")
- // return sets
- case object UNION extends Operand("++")
- case object INTER extends Operand("**")
- case object COMPL extends Operand("~")
-
- /* Types */
-
- sealed abstract class Type
- case object BoolType extends Type
- case object IntType extends Type
- case object SetType extends Type
-
- /* Symbols */
-
- class Symbol private[AST](val typ: Type, val ast: Z3AST) {
- def name = ast.toString
- override def toString = name
- override def hashCode = ast.ptr.hashCode
- override def equals(that: Any) =
- ( that != null &&
- that.isInstanceOf[Symbol] &&
- that.asInstanceOf[Symbol].ast.ptr == this.ast.ptr )
- }
-
- implicit def sym2tree(sym: Symbol): Tree = Var(sym)
-
- def BoolSymbol(ast: Z3AST) = new Symbol(BoolType, ast)
- def IntSymbol(ast: Z3AST) = new Symbol(IntType, ast)
- def SetSymbol(ast: Z3AST) = new Symbol(SetType, ast)
-}
diff --git a/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
deleted file mode 100644
index 7fc52a1821ac3876063d4c9c20f1d81ddfdc680f..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
+++ /dev/null
@@ -1,378 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-/********************************************************************
-
- WARNING : THIS VERSION IS NOT USED (AND CERTAINLY NOT MAINTAINED).
- SEE BAPATheoryBubbles INSTEAD !
-
- ******************************************************************/
-
-package purescala.z3plugins.bapa
-
-import scala.collection.mutable.Stack
-import scala.collection.mutable.{Set => MutableSet}
-import scala.collection.immutable.{Map => ImmutableMap}
-import z3.scala._
-import AST._
-import NormalForms.{simplify, rewriteSetRel, setVariables, purify}
-
-import scala.sys.error
-
-class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with VennRegions { //with InclusionGraphs {
-
- /* Register callbacks */
-
- setCallbacks(
- reduceApp = true,
- finalCheck = true,
- push = true,
- pop = true,
- newApp = true,
- newAssignment = true,
- newEq = true,
- newDiseq = true,
- reset = true,
- restart = true
- )
-
- // This makes the Theory Proxy print out all calls that are
- // forwarded to the theory.
- showCallbacks(true)
-
- /* Theory constructs */
-
- val mkSetSort = mkTheorySort(z3.mkStringSymbol("SetSort"))
- val mkEmptySet = mkTheoryValue(z3.mkStringSymbol("EmptySet"), mkSetSort)
- val mkSingleton = mkTheoryFuncDecl(z3.mkStringSymbol("Singleton"), Seq(z3.mkIntSort), mkSetSort)
- val mkCard = mkUnarySetfun("Cardinality", z3.mkIntSort)
- val mkSubsetEq = mkBinarySetfun("SubsetEq", z3.mkBoolSort)
- val mkElementOf = mkTheoryFuncDecl(z3.mkStringSymbol("IsElementOf"), Seq(z3.mkIntSort, mkSetSort), z3.mkBoolSort)
- val mkUnion = mkBinarySetfun("Union", mkSetSort)
- val mkIntersect = mkBinarySetfun("Intersect", mkSetSort)
- val mkComplement = mkUnarySetfun("Complement", mkSetSort)
-
- private[bapa] val mkDomainSize = z3.mkFreshConst("DomainSize", z3.mkIntSort)
- // This function returns the single element for singletons, and is uninterpreted otherwise.
- private[bapa] val mkAsElement = mkUnarySetfun("AsElement", z3.mkIntSort)
-
- def mkDisjoint(set1: Z3AST, set2: Z3AST) =
- z3.mkEq(mkIntersect(set1, set2), mkEmptySet)
-
- private var freshCounter = 0
-
- def mkSetConst(name: String) = mkTheoryConstant(z3.mkStringSymbol(name), mkSetSort)
-
- def mkFreshConst(name: String) = {
- freshCounter += 1
- mkSetConst(name + "." + freshCounter)
- }
-
- private def mkUnarySetfun(name: String, rType: Z3Sort) =
- mkTheoryFuncDecl(z3.mkStringSymbol(name), Seq(mkSetSort), rType)
-
- private def mkBinarySetfun(name: String, rType: Z3Sort) =
- mkTheoryFuncDecl(z3.mkStringSymbol(name), Seq(mkSetSort, mkSetSort), rType)
-
- /* Theory stack */
-
- private val universeStack = new Stack[Universe]
- // private val inclusionStack = new Stack[InclusionGraph]
-
- def assertAxiomFromVennRegions(ast: Z3AST) {
- // println("Asserting: " + ast)
- assertAxiom(ast)
- }
-
- def assertAxiom2(ast: Z3AST) {
- // println("Asserting: " + ast)
- assertAxiom(ast)
- }
-
- def assertAxiomSafe(ast: Z3AST) {
- // println("Asserting: " + ast)
- assertAxiomEventually(ast)
- }
-
- // We use this trick to circumvent the fact that you (apparently) can't
- // assertAxioms with some callbacks, such as newApp...
- private val axiomsToAssert: MutableSet[(Int, Z3AST)] = MutableSet.empty
-
- protected def assertAxiomEventually(axiom: Z3AST) = {
- axiomsToAssert += ((pushLevel, axiom))
- }
-
- private def assertAllRemaining: Unit = {
- if (axiomsToAssert.nonEmpty) {
- val toPreserve: MutableSet[(Int, Z3AST)] = MutableSet.empty
-
- for ((lvl, ax) <- axiomsToAssert) {
- // println("Asserting eventual axiom: " + ax)
- assertAxiom2(ax)
- if (lvl < pushLevel) toPreserve += ((lvl, ax))
- }
- axiomsToAssert.clear
- axiomsToAssert ++= toPreserve
- }
- }
-
- /* Callbacks */
-
- override def reset {
- axiomsToAssert.clear
- universeStack.clear
- // inclusionStack.clear
- universeStack push new EmptyUniverse(mkDomainSize)
- // inclusionStack push EmptyInclusionGraph()
- }
- reset
-
- override def restart {
- reset
- }
-
- private var pushLevel = 0
-
- override def push {
- pushLevel = pushLevel + 1
- //assertAllRemaining
- universeStack push universeStack.head
- // inclusionStack push inclusionStack.head
- }
-
- override def pop {
- pushLevel = pushLevel - 1
- //assertAllRemaining
- universeStack.pop
- // inclusionStack.pop
- }
-
- override def newAssignment(ast: Z3AST, polarity: Boolean) {
- assertAllRemaining
-
- // if (polarity) {
- // z3.getASTKind(ast) match {
- // case Z3AppAST(decl, args) if decl == mkSubsetEq => inclusionStack.push(inclusionStack.pop.newSubsetEq(args(0), args(1)))
- // case _ =>;
- // }
- // }
-
- val assumption = if (polarity) ast else z3.mkNot(ast)
- val bapaTree = if (polarity) z3ToTree(ast) else !z3ToTree(ast)
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- val axiom = z3.mkIff(assumption, treeToZ3(paTree))
- assertAxiom2(axiom)
- // println(axiom)
- // println("New Axiom : " + bapaTree + " implies\n" + paTree)
- }
-
- override def newEq(ast1: Z3AST, ast2: Z3AST) {
- assertAllRemaining
-
- if (z3.getSort(ast1) == mkSetSort) {
- // inclusionStack.push(inclusionStack.pop.newEq(ast1, ast2))
- // TODO: if either ast1 or ast2 is a variable => don't add it/remove it from the stack and remember congruence class
- // println("*** new Eq : " + ast1 + " == " + ast2)
-
- //println("Equals : " + (ast1 == ast2))
- //println("Root Equals : " + (getEqClassRoot(ast1) == getEqClassRoot(ast2)))
- //println("Ast 1 : " + ast1)
- //println("Ast 2 : " + ast2)
- //println("Ast 1 root : " + getEqClassRoot(ast1))
- //println("Ast 2 root : " + getEqClassRoot(ast2))
- //println("Ast 1 class : " + getEqClassMembers(ast1).toList.mkString(", "))
- //println("Ast 2 class : " + getEqClassMembers(ast2).toList.mkString(", "))
- //println("Ast 1 parents : " + getParents(ast1).toList.mkString(", "))
- //println("Ast 2 parents : " + getParents(ast2).toList.mkString(", "))
-
- if (ast1 == mkEmptySet || ast2 == mkEmptySet) {
- val nonEmpty = if (ast1 == mkEmptySet) ast2 else ast1
- for (congruent <- getEqClassMembers(nonEmpty)) {
- for (parent <- getParents(congruent)) {
- z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) if decl == mkCard && args(0) == congruent =>
- assertAxiom2(z3.mkIff(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkCard(congruent), z3.mkInt(0, z3.mkIntSort))))
- case Z3AppAST(decl, args) if decl == mkUnion && args(0) == congruent =>
- assertAxiom2(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(congruent, args(1)), args(1))))
- case Z3AppAST(decl, args) if decl == mkUnion && args(1) == congruent =>
- assertAxiom2(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(args(0), congruent), args(0))))
- case Z3AppAST(decl, args) if decl == mkIntersect && args(0) == congruent =>
- assertAxiom2(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(congruent, args(1)), mkEmptySet)))
- case Z3AppAST(decl, args) if decl == mkIntersect && args(1) == congruent =>
- assertAxiom2(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(args(0), congruent), mkEmptySet)))
- case _ =>;
- }
- }
- }
- }
-
- val assumption = z3.mkEq(ast1, ast2)
- val bapaTree = z3ToTree(ast1) seteq z3ToTree(ast2)
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- val axiom = z3.mkImplies(assumption, treeToZ3(paTree))
- assertAxiom2(axiom)
- }
- }
-
- override def newDiseq(ast1: Z3AST, ast2: Z3AST) {
- assertAllRemaining
- // println("*** new Diseq : " + ast1 + " == " + ast2)
-
- if (z3.getSort(ast1) == mkSetSort) {
- //println("Ast 1 : " + ast1)
- //println("Ast 2 : " + ast2)
- //println("Ast 1 root : " + getEqClassRoot(ast1))
- //println("Ast 2 root : " + getEqClassRoot(ast2))
- //println("Ast 1 class : " + getEqClassMembers(ast1).toList.mkString(", "))
- //println("Ast 2 class : " + getEqClassMembers(ast2).toList.mkString(", "))
- //println("Ast 1 parents : " + getParents(ast1).toList.mkString(", "))
- //println("Ast 2 parents : " + getParents(ast2).toList.mkString(", "))
-
- if (ast1 == mkEmptySet || ast2 == mkEmptySet) {
- val nonEmpty = if (ast1 == mkEmptySet) ast2 else ast1
- for (congruent <- getEqClassMembers(nonEmpty)) {
- for (parent <- getParents(congruent)) {
- z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) if decl == mkCard && args(0) == congruent =>
- assertAxiom2(z3.mkImplies(
- z3.mkDistinct(congruent, mkEmptySet),
- z3.mkGT(mkCard(congruent), z3.mkInt(0, z3.mkIntSort))))
- case _ =>;
- }
- }
- }
- }
-
- val assumption = z3.mkDistinct(ast1, ast2)
- val bapaTree = !(z3ToTree(ast1) seteq z3ToTree(ast2))
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- val axiom = z3.mkImplies(assumption, treeToZ3(paTree))
- assertAxiom2(axiom)
- }
- }
-
- override def newApp(ast: Z3AST) {
- // println("*** new App : " + ast)
- z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkCard =>
- val bapaTree = z3ToTree(ast)
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- assertAxiomEventually(z3.mkEq(treeToZ3(paTree), ast))
- assertAxiomEventually(z3.mkIff(z3.mkEq(ast, z3.mkInt(0, z3.mkIntSort)), z3.mkEq(args(0), mkEmptySet)))
- case Z3AppAST(decl, args) if decl == mkSingleton =>
- assertAxiomEventually(z3.mkEq(mkAsElement(ast), args(0)))
- assertAxiomEventually(z3.mkEq(mkCard(ast), z3.mkInt(1, z3.mkIntSort)))
- case _ =>
- // ignore other functions
- }
- }
-
- // TODO: add reductions for union & inter (empty set) and compl (nnf ?)
- override def reduceApp(fd: Z3FuncDecl, args: Z3AST*): Option[Z3AST] = {
- if (fd == mkCard) {
- if (args(0) == mkEmptySet) {
- Some(z3.mkInt(0, z3.mkIntSort))
- } else {
- None
- }
- } else if (fd == mkSubsetEq) {
- if (args(0) == mkEmptySet) {
- Some(z3.mkTrue)
- } else if (args(1) == mkEmptySet) {
- Some(z3.mkEq(mkEmptySet, args(0)))
- } else {
- None
- }
- // } else if (fd == mkIsSingleton) {
- // if (args(0) == mkEmptySet) {
- // Some(z3.mkFalse)
- // } else {
- // None
- // }
- } else if (fd == mkElementOf) {
- val elem = args(0)
- val set = args(1)
- if (set == mkEmptySet) {
- Some(z3.mkFalse)
- } else {
- Some(mkSubsetEq(mkSingleton(elem), set))
- }
- } else {
- None
- }
- }
-
- override def finalCheck: Boolean = {
- assertAllRemaining
- true
- }
-
- /* Transformations */
-
- def treeToZ3(tree: Tree): Z3AST = treeToZ3_rec(purify(z3, tree))
-
- private def treeToZ3_rec(tree: Tree): Z3AST = tree match {
- case Var(sym) => sym.ast
- case Lit(TrueLit) => z3.mkTrue
- case Lit(FalseLit) => z3.mkFalse
- case Lit(IntLit(i)) => z3.mkInt(i, z3.mkIntSort)
- case Op(AND, ts) => z3.mkAnd((ts map treeToZ3_rec): _*)
- case Op(OR, ts) => z3.mkOr((ts map treeToZ3_rec): _*)
- case Op(NOT, Seq(t)) => z3.mkNot(treeToZ3_rec(t))
- case Op(IFF, Seq(t1, t2)) => z3.mkIff(treeToZ3_rec(t1), treeToZ3_rec(t2))
- // case Op(EQ, Seq(Op(CARD, Seq(t)), Lit(IntLit(1)))) => mkIsSingleton(treeToZ3_rec(t))
- // case Op(EQ, Seq(Lit(IntLit(1)), Op(CARD, Seq(t)))) => mkIsSingleton(treeToZ3_rec(t))
- case Op(EQ, Seq(t1, t2)) => z3.mkEq(treeToZ3_rec(t1), treeToZ3_rec(t2))
- case Op(LT, Seq(t1, t2)) => z3.mkLT(treeToZ3_rec(t1), treeToZ3_rec(t2))
- case Op(ADD, ts) => z3.mkAdd((ts map treeToZ3_rec): _*)
- case Op(CARD, Seq(t)) => mkCard(treeToZ3_rec(t))
- case Op(SETEQ, Seq(t1, t2)) => z3.mkEq(treeToZ3_rec(t1), treeToZ3_rec(t2))
- case Op(SUBSETEQ, Seq(t1, t2)) => mkSubsetEq(treeToZ3_rec(t1), treeToZ3_rec(t2))
- case Op(UNION, ts) => mkUnion((ts map treeToZ3_rec): _*)
- case Op(INTER, ts) => mkIntersect((ts map treeToZ3_rec): _*)
- case Op(COMPL, Seq(t)) => mkComplement(treeToZ3_rec(t))
- case Lit(EmptySetLit) => mkEmptySet
- case _ => error("Unsupported conversion from BAPA-tree to Z3AST :\n" + tree)
- }
-
- def knownRepresentative(ast: Z3AST): Z3AST = ast
-
- def z3ToTree(ast: Z3AST): Tree = z3.getASTKind(ast) match {
- case _ if ast == mkEmptySet => EmptySet
- case Z3AppAST(decl, Nil) => SetSymbol(knownRepresentative(ast))
- case Z3AppAST(decl, args) if decl == mkSubsetEq => Op(SUBSETEQ, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkUnion => Op(UNION, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkIntersect => Op(INTER, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkComplement => Op(COMPL, args map z3ToTree)
- // case Z3AppAST(decl, args) if decl == mkIsSingleton => z3ToTree(args(0)).card === 1
- // case Z3AppAST(decl, args) if decl == mkCardPred => Op(EQ, Seq(Op(CARD, Seq(z3ToTree(args(0)))), IntSymbol(args(1))))
- case Z3AppAST(decl, args) if decl == mkCard => Op(CARD, Seq(z3ToTree(args(0))))
- case _ =>
- //println("** Cannot convert Z3AST to BAPA-tree :\n** " + ast)
- //println("** Treating it as an uninterpreted function")
- SetSymbol(knownRepresentative(ast))
- // println("** Cannot convert Z3AST to BAPA tree :\n** " + ast)
- // error("Cannot convert Z3AST to BAPA tree")
- }
-
- def NaiveBapaToPaTranslator(tree0: Tree) = {
- def rec(tree: Tree): Tree = tree match {
- case Op(CARD, Seq(set)) => universeStack.head translate set
- case Op(op, ts) => Op(op, ts map rec)
- case Var(_) | Lit(_) => tree
- }
- val tree1 = simplify(tree0)
- universeStack.push(universeStack.pop addSets setVariables(tree1))
- simplify(rec(simplify(rewriteSetRel(tree1))))
- }
-
-}
diff --git a/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
deleted file mode 100644
index d294e8b117495fb4f1f56caa95702f3f6a2003b6..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
+++ /dev/null
@@ -1,500 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package purescala.z3plugins.bapa
-
-import scala.collection.mutable.{Stack, ArrayBuffer, Set => MutableSet, HashMap => MutableMap}
-import scala.collection.immutable.{Map => ImmutableMap}
-import z3.scala._
-import AST._
-import NormalForms.{simplify, setVariables, rewriteSetRel}
-
-import scala.sys.error
-
-class BAPATheoryBubbles(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory (bubbles)") with Bubbles {
-
- /* Flags */
-
-// private val WITH_Z3_SET_AXIOMS = true
- private val WITH_Z3_SET_AXIOMS = false
-
- private val SINGLETON_DISEQUALITIES = true // theory is incomplete otherwise
-// private val SINGLETON_DISEQUALITIES = false
-
- /* Register callbacks */
-
- setCallbacks(
- reset = true,
- restart = true,
- push = true,
- pop = true,
- reduceApp = true,
- newApp = true,
- newElem = true,
- newAssignment = true,
- newEq = true,
- newDiseq = true,
- finalCheck = true
- )
- // This makes the Theory Proxy print out all calls that are
- // forwarded to the theory.
- // showCallbacks(true)
-
- /* Theory constructs */
-
- val mkElemSort = z3.mkIntSort
- val mkSetSort = mkTheorySort(z3.mkStringSymbol("SetSort"))
- val mkEmptySet = mkTheoryValue(z3.mkStringSymbol("EmptySet"), mkSetSort)
- val mkSingleton = mkTheoryFuncDecl(z3.mkStringSymbol("Singleton"), Seq(mkElemSort), mkSetSort)
- val mkCard = mkUnarySetfun("Cardinality", z3.mkIntSort)
- val mkSubsetEq = mkBinarySetfun("SubsetEq", z3.mkBoolSort)
- val mkElementOf = mkTheoryFuncDecl(z3.mkStringSymbol("IsElementOf"), Seq(mkElemSort, mkSetSort), z3.mkBoolSort)
- val mkUnion = mkBinarySetfun("Union", mkSetSort)
- val mkIntersect = mkBinarySetfun("Intersect", mkSetSort)
- val mkComplement = mkUnarySetfun("Complement", mkSetSort)
-
- private[bapa] val mkDomainSize = z3.mkFreshConst("DomainSize", z3.mkIntSort)
- // This function returns the single element for singletons, and is uninterpreted otherwise.
- private[bapa] val mkAsElement = mkUnarySetfun("AsElement", z3.mkIntSort)
- private[bapa] val mkZ3SetSort = z3.mkSetSort(mkElemSort)
- private[bapa] val mkAsBAPA = mkTheoryFuncDecl(z3.mkStringSymbol("asBAPA"), Seq(mkZ3SetSort), mkSetSort)
-
- def mkDisjoint(set1: Z3AST, set2: Z3AST) =
- z3.mkEq(mkIntersect(set1, set2), mkEmptySet)
-
- def mkDifference(set1: Z3AST, set2: Z3AST) =
- mkIntersect(set1, mkComplement(set2))
-
- def mkConst(name: String) = mkTheoryConstant(z3.mkStringSymbol(name), mkSetSort)
-
- private var freshCounter = 0
-
- def mkFreshConst(name: String) = {
- freshCounter += 1
- mkConst(name + "." + freshCounter)
- }
-
- private def mkUnarySetfun(name: String, rType: Z3Sort) =
- mkTheoryFuncDecl(z3.mkStringSymbol(name), Seq(mkSetSort), rType)
-
- private def mkBinarySetfun(name: String, rType: Z3Sort) =
- mkTheoryFuncDecl(z3.mkStringSymbol(name), Seq(mkSetSort, mkSetSort), rType)
-
- /* Theory stack */
-
- private val bubbleStack = new Stack[(Int,Bubble)]()
-
- private sealed abstract class Clause
- private case class CardClause(tree: Tree) extends Clause
- private case class SingletonClause(tree: Tree) extends Clause
- private case class AssignClause(tree: Tree, polarity: Boolean) extends Clause
- private case class EqClause(tree1: Tree, tree2: Tree) extends Clause
- private case class DiseqClause(tree1: Tree, tree2: Tree) extends Clause
-
- private def addClause(clause: Clause) {
- assertClause(clause)
- }
-
- /* Axiom assertion helper functions */
-
- private def assertAxiomNow(axiom: Z3AST) {
- // println(axiom)
- assertAxiom(axiom)
- }
-
- protected def assertAxiomSafe(axiom: Z3AST) {
- if (canAssertAxiom) {
- assertAxiomNow(axiom)
- } else {
- // Assert axiom eventually
- axiomsToAssert += ((pushLevel, axiom))
- }
- // println("> Asserting: " + axiom)
- }
-
- // We use this trick to circumvent the fact that you (apparently) can't
- // assertAxioms with some callbacks, such as newApp...
- private val axiomsToAssert: MutableSet[(Int, Z3AST)] = MutableSet.empty
- private var pushLevel = 0
- private var canAssertAxiom = false
-
- private def safeBlockToAssertAxioms[A](block: => A): A = {
- canAssertAxiom = true;
- {
- // Assert all remaining axioms
- if (axiomsToAssert.nonEmpty) {
- val toPreserve: MutableSet[(Int, Z3AST)] = MutableSet.empty
-
- for ((lvl, ax) <- axiomsToAssert) {
- // println("Asserting eventual axiom: " + ax)
- assertAxiomNow(ax)
- if (lvl < pushLevel)
- toPreserve += ((lvl, ax))
- }
- axiomsToAssert.clear
- axiomsToAssert ++= toPreserve
- }
- }
- val result = block
- canAssertAxiom = false
- result
- }
-
- /* Callbacks */
-
- def init {
- pushLevel = 0
- // push
- }
- init
-
- override def reset {
- init
- }
-
- override def restart {
- init
- }
-
- override def push {
- pushLevel += 1
- }
-
- override def pop {
- pushLevel -= 1
- while (bubbleStack.nonEmpty && bubbleStack.head._1 > pushLevel) {
- Universe removeBubble bubbleStack.pop._2
- }
- }
-
- override def reduceApp(fd: Z3FuncDecl, args: Z3AST*): Option[Z3AST] = {
- if (fd == mkCard) {
- if (args(0) == mkEmptySet) {
- Some(z3.mkInt(0, z3.mkIntSort))
- } else {
- None
- }
- } else if (fd == mkSubsetEq) {
- if (args(0) == mkEmptySet) {
- Some(z3.mkTrue)
- } else if (args(1) == mkEmptySet) {
- Some(z3.mkEq(mkEmptySet, args(0)))
- } else {
- None
- }
- } else if (fd == mkElementOf) {
- val elem = args(0)
- val set = args(1)
- if (set == mkEmptySet) {
- Some(z3.mkFalse)
- } else {
- Some(mkSubsetEq(mkSingleton(elem), set))
- }
- } else {
- None
- }
- }
-
- override def newElem(ast1: Z3AST) {
- def asSingleton(ast: Z3AST) = z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkSingleton => Some(args(0))
- case _ => None
- }
- if (SINGLETON_DISEQUALITIES) asSingleton(ast1) match {
- case None =>
- case Some(elem1) =>
- for (ast2 <- getElems; if ast2 != ast1) asSingleton(ast2) match {
- case None =>
- case Some(elem2) =>
- val bapaTree = !(z3ToTree(ast1) seteq z3ToTree(ast2))
- val paTree = BubbleBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkImplies(
- z3.mkDistinct(elem1, elem2),
- treeToZ3(paTree)
- ))
- }
- }
- // Connection to Z3 sets
- if (WITH_Z3_SET_AXIOMS) addSetExpression(ast1)
- }
-
- override def newApp(ast: Z3AST) {
- z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkCard =>
- addClause(CardClause(z3ToTree(ast)))
- assertAxiomSafe(z3.mkIff(
- z3.mkEq(ast, z3.mkInt(0, z3.mkIntSort)),
- z3.mkEq(args(0), mkEmptySet)
- ))
- case Z3AppAST(decl, args) if decl == mkSingleton =>
- addClause(SingletonClause(z3ToTree(ast)))
- assertAxiomSafe(z3.mkEq(mkAsElement(ast), args(0)))
- assertAxiomSafe(z3.mkEq(mkCard(ast), z3.mkInt(1, z3.mkIntSort)))
- case _ =>
- }
- // Connection to Z3 sets
- if (WITH_Z3_SET_AXIOMS) addSetExpression(ast)
- }
-
- override def newAssignment(ast: Z3AST, polarity: Boolean): Unit = safeBlockToAssertAxioms {
- /*
- if(polarity) {
- z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkSubsetEq =>
- inclusionStack push (inclusionStack.pop newSubsetEq (args(0), args(1)))
- case _ =>
- }
- }
- */
- addClause(AssignClause(z3ToTree(ast), polarity))
- }
-
- override def newEq(ast1: Z3AST, ast2: Z3AST): Unit = safeBlockToAssertAxioms {
- if (z3.getSort(ast1) == mkSetSort && !(WITH_Z3_SET_AXIOMS && (isAsBapa(ast1) || isAsBapa(ast2)))) {
- /*
- inclusionStack.push(inclusionStack.pop.newEq(ast1, ast2))
- */
- // S = {} implies the following for sets T in the equivalence class of S
- // - |T| = 0
- // - T ++ U = U
- // - U ++ T = U
- // - T ** U = {}
- // - U ** T = {}
- if (ast1 == mkEmptySet || ast2 == mkEmptySet) {
- val nonEmpty = if (ast1 == mkEmptySet) ast2 else ast1
- for (congruent <- getEqClassMembers(nonEmpty)) {
- for (parent <- getParents(congruent)) {
- z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) if decl == mkCard && args(0) == congruent =>
- assertAxiomSafe(z3.mkIff(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(parent, z3.mkInt(0, z3.mkIntSort))))
-// z3.mkEq(mkCard(congruent), z3.mkInt(0, z3.mkIntSort))))
- case Z3AppAST(decl, args) if decl == mkUnion && args(0) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(parent, args(1))))
-// z3.mkEq(mkUnion(congruent, args(1)), args(1))))
- case Z3AppAST(decl, args) if decl == mkUnion && args(1) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(parent, args(0))))
-// z3.mkEq(mkUnion(args(0), congruent), args(0))))
- case Z3AppAST(decl, args) if decl == mkIntersect && args(0) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(parent, mkEmptySet)))
-// z3.mkEq(mkUnion(congruent, args(1)), mkEmptySet)))
- case Z3AppAST(decl, args) if decl == mkIntersect && args(1) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(parent, mkEmptySet)))
-// z3.mkEq(mkUnion(args(0), congruent), mkEmptySet)))
- case _ =>
- }
- }
- }
- }
- addClause(EqClause(z3ToTree(ast1), z3ToTree(ast2)))
- }
- }
-
- override def newDiseq(ast1: Z3AST, ast2: Z3AST): Unit = safeBlockToAssertAxioms {
- if (z3.getSort(ast1) == mkSetSort) {
- if (WITH_Z3_SET_AXIOMS && (isAsBapa(ast1) || isAsBapa(ast2))) return ()
- // S != {} implies |T| > 0 for all sets T in the equivalence class of S
- if (ast1 == mkEmptySet || ast2 == mkEmptySet) {
- val nonEmpty = if (ast1 == mkEmptySet) ast2 else ast1
- for (congruent <- getEqClassMembers(nonEmpty)) {
- for (parent <- getParents(congruent)) {
- z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) if decl == mkCard && args(0) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkDistinct(congruent, mkEmptySet),
- z3.mkGT(parent, z3.mkInt(0, z3.mkIntSort))))
-// z3.mkGT(mkCard(congruent), z3.mkInt(0, z3.mkIntSort))))
- case _ =>
- }
- }
- }
- }
- addClause(DiseqClause(z3ToTree(ast1), z3ToTree(ast2)))
- } else {
- /*
- val set1 = mkSingleton(ast1)
- val set2 = mkSingleton(ast2)
- if (SINGLETON_DISEQUALITIES && (getElems contains set1) && (getElems contains set2)) {
- val bapaTree = (z3ToTree(set1) seteq z3ToTree(set2))
- val paTree = BubbleBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkIff(
- treeToZ3(paTree),
- z3.mkEq(ast1, ast2)
- ))
- }
- */
- }
- }
-
- override def finalCheck: Boolean = safeBlockToAssertAxioms {
- // println("==== Bubbles at final check ====")
- // Universe.showState
- // println("================================")
- true
- }
-
- /* Transformations */
-
- def treeToZ3(tree: Tree): Z3AST = tree match {
- case Var(sym) => sym.ast
- case Lit(TrueLit) => z3.mkTrue
- case Lit(FalseLit) => z3.mkFalse
- case Lit(IntLit(i)) => z3.mkInt(i, z3.mkIntSort)
- case Op(AND, ts) => z3.mkAnd((ts map treeToZ3): _*)
- case Op(OR, ts) => z3.mkOr((ts map treeToZ3): _*)
- case Op(NOT, Seq(t)) => z3.mkNot(treeToZ3(t))
- case Op(IFF, Seq(t1, t2)) => z3.mkIff(treeToZ3(t1), treeToZ3(t2))
- case Op(EQ, Seq(t1, t2)) => z3.mkEq(treeToZ3(t1), treeToZ3(t2))
- case Op(LT, Seq(t1, t2)) => z3.mkLT(treeToZ3(t1), treeToZ3(t2))
- case Op(ADD, ts) => z3.mkAdd((ts map treeToZ3): _*)
- case Op(CARD, Seq(t)) => mkCard(treeToZ3(t))
- case Op(SETEQ, Seq(t1, t2)) => z3.mkEq(treeToZ3(t1), treeToZ3(t2))
- case Op(SUBSETEQ, Seq(t1, t2)) => mkSubsetEq(treeToZ3(t1), treeToZ3(t2))
- case Op(UNION, ts) => mkUnion((ts map treeToZ3): _*)
- case Op(INTER, ts) => mkIntersect((ts map treeToZ3): _*)
- case Op(COMPL, Seq(t)) => mkComplement(treeToZ3(t))
- case Lit(EmptySetLit) => mkEmptySet
- case _ => error("Unsupported conversion from BAPA-tree to Z3AST :\n" + tree)
- }
-
- def z3ToTree(ast: Z3AST): Tree = {
- if (ast == mkEmptySet) EmptySet
- else z3.getASTKind(ast) match {
- case Z3AppAST(decl, Nil) => SetSymbol(ast)
- case Z3AppAST(decl, args) if decl == mkSubsetEq => Op(SUBSETEQ, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkUnion => Op(UNION, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkIntersect => Op(INTER, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkComplement => Op(COMPL, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkCard => Op(CARD, Seq(z3ToTree(args(0))))
- case Z3AppAST(decl, args) if decl == mkAsBAPA =>
- if (!(asBapaToBapa contains ast)) {
- for ((asB, b) <- asBapaToBapa) println(asB + " -> " + b)
- error("Could not find : \n" + ast)
- }
- z3ToTree(asBapaToBapa(ast))
- case _ => SetSymbol(ast)
- }
- }
-
- /* Interaction with Z3 sets */
-
- private val asBapaToBapa = new MutableMap[Z3AST,Z3AST]()
- private val cachedBapaToAsBapa = new MutableMap[Z3AST,Z3AST]()
- private val cachedBapaVarToZ3set = new MutableMap[Z3AST,Z3AST]()
-
- def addSetExpression(ast: Z3AST) {
- if (z3.getSort(ast) == mkSetSort) z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkAsBAPA =>
- // Not needed
-// println("Not needed : " + ast)
- case _ if cachedBapaToAsBapa contains ast =>
- // Already added
-// println("Already added : " + ast)
- case _ =>
- val axiom = z3.mkEq(ast, bapaSetToAsBapa(ast))
-// println("Axiom : " + axiom)
- assertAxiomSafe(axiom)
- }
- }
-
- private def bapaSetToAsBapa(ast: Z3AST) = {
-// var level = 0
- def toZ3set(ast: Z3AST): Z3AST = {
-// level += 1
-// println((" " * level) + "translating " + ast)
- val res = if (ast == mkEmptySet) z3.mkEmptySet(mkElemSort)
- else z3.getASTKind(ast) match {
- case Z3AppAST(decl, Nil) =>
- mkZ3SetVar(ast)
- case Z3AppAST(decl, args) if decl == mkSubsetEq =>
- z3.mkSetSubset(toZ3set(args(0)), toZ3set(args(1)))
- case Z3AppAST(decl, args) if decl == mkUnion =>
- z3.mkSetUnion(toZ3set(args(0)), toZ3set(args(1)))
- case Z3AppAST(decl, args) if decl == mkIntersect =>
- z3.mkSetIntersect(toZ3set(args(0)), toZ3set(args(1)))
- case Z3AppAST(decl, args) if decl == mkComplement =>
- z3.mkSetComplement(toZ3set(args(0)))
- case Z3AppAST(decl, args) if decl == mkSingleton =>
- z3.mkSetAdd(z3.mkEmptySet(mkElemSort), args(0))
- case Z3AppAST(decl, args) if decl == mkAsBAPA =>
- args(0)
- case _ =>
- mkZ3SetVar(ast)
- }
-// println((" " * level) + "result " + res)
-// level -= 1
- res
- }
- cachedBapaToAsBapa getOrElse(ast, {
- val asBapa = mkAsBAPA(toZ3set(ast))
- cachedBapaToAsBapa(ast) = asBapa
- asBapaToBapa(asBapa) = ast
- asBapa
- })
- }
-
- private def mkZ3SetVar(ast: Z3AST) = cachedBapaVarToZ3set getOrElse(ast, {
- val fresh = z3.mkFreshConst("z3twin", mkZ3SetSort)
- cachedBapaVarToZ3set(ast) = fresh
- fresh
- })
-
- private def isAsBapa(ast: Z3AST) = z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkAsBAPA => true
- case _ => false
- }
-
- /* PA translation */
-
- def BubbleBapaToPaTranslator(tree0: Tree) = {
- val tree1 = simplify(tree0)
- val (myBubble, isNew) = Universe addBubble setVariables(tree1)
- if (isNew) bubbleStack push ((pushLevel, myBubble))
- def rec(tree: Tree): Tree = tree match {
- case Op(CARD, Seq(set)) => myBubble translate set
- case Op(op, ts) => Op(op, ts map rec)
- case Var(_) | Lit(_) => tree
- }
- simplify(rec(simplify(rewriteSetRel(tree1))))
- }
-
- private def assertClause(clause: Clause) = clause match {
- case CardClause(bapaTree) =>
- val paTree = BubbleBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkEq(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- case SingletonClause(tree) =>
- // nothing to do (except optimizations :P)
- case AssignClause(tree, polarity) =>
- val bapaTree = if (polarity) tree else !tree
- val paTree = BubbleBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkImplies(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- case EqClause(tree1, tree2) =>
- val bapaTree = tree1 seteq tree2
- val paTree = BubbleBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkImplies(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- case DiseqClause(tree1, tree2) =>
- val bapaTree = !(tree1 seteq tree2)
- val paTree = BubbleBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkImplies(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- }
-}
diff --git a/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
deleted file mode 100644
index 031a957bb379553958462ac8c1a5f803f5a6f9d2..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
+++ /dev/null
@@ -1,563 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-/********************************************************************
-
- WARNING : THIS VERSION IS NOT USED (AND CERTAINLY NOT MAINTAINED).
- SEE BAPATheoryBubbles INSTEAD !
-
- ******************************************************************/
-
-package purescala.z3plugins.bapa
-
-import scala.collection.mutable.{Stack, ArrayBuffer, Set => MutableSet, Map => MutableMap}
-import scala.collection.immutable.{Map => ImmutableMap}
-import z3.scala._
-import AST._
-import NormalForms.{simplify, setVariables, rewriteSetRel}
-
-import scala.sys.error
-
-class BAPATheoryEqc(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory (eqc)") with VennRegions {
-
- /* Register callbacks */
-
- setCallbacks(
- reset = true,
- restart = true,
- push = true,
- pop = true,
- reduceApp = true,
- newApp = true,
- newAssignment = true,
- newEq = true,
- newDiseq = true,
- finalCheck = true
- )
- // This makes the Theory Proxy print out all calls that are
- // forwarded to the theory.
- // showCallbacks(true)
-
- /* Theory constructs */
-
- val mkSetSort = mkTheorySort(z3.mkStringSymbol("SetSort"))
- val mkEmptySet = mkTheoryValue(z3.mkStringSymbol("EmptySet"), mkSetSort)
- val mkSingleton = mkTheoryFuncDecl(z3.mkStringSymbol("Singleton"), Seq(z3.mkIntSort), mkSetSort)
- val mkCard = mkUnarySetfun("Cardinality", z3.mkIntSort)
- val mkSubsetEq = mkBinarySetfun("SubsetEq", z3.mkBoolSort)
- val mkElementOf = mkTheoryFuncDecl(z3.mkStringSymbol("IsElementOf"), Seq(z3.mkIntSort, mkSetSort), z3.mkBoolSort)
- val mkUnion = mkBinarySetfun("Union", mkSetSort)
- val mkIntersect = mkBinarySetfun("Intersect", mkSetSort)
- val mkComplement = mkUnarySetfun("Complement", mkSetSort)
-
- private[bapa] val mkDomainSize = z3.mkFreshConst("DomainSize", z3.mkIntSort)
- // This function returns the single element for singletons, and is uninterpreted otherwise.
- private[bapa] val mkAsElement = mkUnarySetfun("AsElement", z3.mkIntSort)
-
- def mkDisjoint(set1: Z3AST, set2: Z3AST) =
- z3.mkEq(mkIntersect(set1, set2), mkEmptySet)
-
- def mkDifference(set1: Z3AST, set2: Z3AST) =
- mkIntersect(set1, mkComplement(set2))
-
- private var freshCounter = 0
-
- def mkConst(name: String) = mkTheoryConstant(z3.mkStringSymbol(name), mkSetSort)
-
- def mkFreshConst(name: String) = {
- freshCounter += 1
- mkConst(name + "." + freshCounter)
- }
-
- private def mkUnarySetfun(name: String, rType: Z3Sort) =
- mkTheoryFuncDecl(z3.mkStringSymbol(name), Seq(mkSetSort), rType)
-
- private def mkBinarySetfun(name: String, rType: Z3Sort) =
- mkTheoryFuncDecl(z3.mkStringSymbol(name), Seq(mkSetSort, mkSetSort), rType)
-
- /* Theory stack */
-
- private var universe: Universe = null
- private val clauseStack = new Stack[Stack[Seq[Clause]]]
- // private val boundaryElemsStack = new Stack[Set[Z3AST]]
- // boundaryElemsStack push Set.empty[Z3AST]
-
- private sealed abstract class Clause
- private case class CardClause(tree: Tree) extends Clause
- private case class SingletonClause(tree: Tree) extends Clause
- private case class AssignClause(tree: Tree, polarity: Boolean) extends Clause
- private case class EqClause(tree1: Tree, tree2: Tree) extends Clause
- private case class DiseqClause(tree1: Tree, tree2: Tree) extends Clause
-
- private def addClause(clause: Clause) {
- // println(" Clause: " + clause)
- // clauseStack.head.head += clause
-
- // Try to assert clause axiom immediately, push it otherwise
- transformClause(clause) match {
- case (newClause, newSymbols) if newSymbols.isEmpty =>
- print(". ")
- assertClause(newClause)
- case (_, newSymbols) =>
- print(newSymbols.size + " ")
- clauseStack.head push (clause +: clauseStack.head.pop)
- }
- }
-
- def showStack = {
- (clauseStack map {cls => (cls map {cl => cl.size}).mkString("{", ",", "}")}).mkString("{", ",", "}")
- }
-
- /* Axiom assertion helper functions */
-
- def assertAxiomSafe(axiom: Z3AST) {
- if (canAssertAxiom) {
- assertAxiom(axiom)
- } else {
- // Assert axiom eventually
- axiomsToAssert += ((pushLevel, axiom))
- }
- // println("> Asserting: " + axiom)
- }
-
- // We use this trick to circumvent the fact that you (apparently) can't
- // assertAxioms with some callbacks, such as newApp...
- private val axiomsToAssert: MutableSet[(Int, Z3AST)] = MutableSet.empty
- private var pushLevel = 0
- private var canAssertAxiom = false
-
- private def safeBlockToAssertAxioms[A](block: => A): A = {
- canAssertAxiom = true;
- {
- // Assert all remaining axioms
- if (axiomsToAssert.nonEmpty) {
- val toPreserve: MutableSet[(Int, Z3AST)] = MutableSet.empty
-
- for ((lvl, ax) <- axiomsToAssert) {
- // println("Asserting eventual axiom: " + ax)
- assertAxiom(ax)
- if (lvl < pushLevel)
- toPreserve += ((lvl, ax))
- }
- axiomsToAssert.clear
- axiomsToAssert ++= toPreserve
- }
- }
- val result = block
- canAssertAxiom = false
- result
- }
-
- /* Callbacks */
-
- def init {
- universe = new EmptyUniverse(mkDomainSize)
- clauseStack.clear
- clauseStack push new Stack[Seq[Clause]]
- axiomsToAssert.clear
- pushLevel = 0
- push
- }
- init
-
- override def reset {
- init
- // new AssertionError("Reset was called").printStackTrace
- }
-
- override def restart {
- init
- // new AssertionError("Restart was called").printStackTrace
- }
-
- override def push {
- pushLevel += 1
- clauseStack.head push Seq[Clause]()
- // println("Push level " + pushLevel + " " + showStack)
- }
-
- override def pop {
- // println("Pop level " + pushLevel + " " + showStack)
- pushLevel -= 1
- clauseStack.head.pop
- while (clauseStack.head.isEmpty) {
- clauseStack.pop
- clauseStack.head.pop
- }
-
- // println("---------- " + pushLevel + " " + showStack)
- }
-
- override def reduceApp(fd: Z3FuncDecl, args: Z3AST*): Option[Z3AST] = {
- if (fd == mkCard) {
- if (args(0) == mkEmptySet) {
- Some(z3.mkInt(0, z3.mkIntSort))
- } else {
- None
- }
- } else if (fd == mkSubsetEq) {
- if (args(0) == mkEmptySet) {
- Some(z3.mkTrue)
- } else if (args(1) == mkEmptySet) {
- Some(z3.mkEq(mkEmptySet, args(0)))
- } else {
- None
- }
- } else if (fd == mkElementOf) {
- val elem = args(0)
- val set = args(1)
- if (set == mkEmptySet) {
- Some(z3.mkFalse)
- } else {
- Some(mkSubsetEq(mkSingleton(elem), set))
- }
- } else {
- None
- }
- }
-
- override def newApp(ast: Z3AST) {
- z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkCard =>
- addClause(CardClause(z3ToTree(ast)))
- assertAxiomSafe(z3.mkIff(z3.mkEq(ast, z3.mkInt(0, z3.mkIntSort)), z3.mkEq(args(0), mkEmptySet)))
- case Z3AppAST(decl, args) if decl == mkSingleton =>
- addClause(SingletonClause(z3ToTree(ast)))
- assertAxiomSafe(z3.mkEq(mkAsElement(ast), args(0)))
- assertAxiomSafe(z3.mkEq(mkCard(ast), z3.mkInt(1, z3.mkIntSort)))
- case _ =>
- }
- }
-
- override def newAssignment(ast: Z3AST, polarity: Boolean) = safeBlockToAssertAxioms {
- /*
- if(polarity) {
- z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkSubsetEq =>
- inclusionStack push (inclusionStack.pop newSubsetEq (args(0), args(1)))
- case _ =>
- }
- }
- */
- addClause(AssignClause(z3ToTree(ast), polarity))
- ()
- }
-
- override def newEq(ast1: Z3AST, ast2: Z3AST) = safeBlockToAssertAxioms {
-
- if (z3.getSort(ast1) == mkSetSort) {
- /*
- inclusionStack.push(inclusionStack.pop.newEq(ast1, ast2))
- */
- // println("Equals : " + (ast1 == ast2))
- // println("Root Equals : " + (getEqClassRoot(ast1) == getEqClassRoot(ast2)))
- // println("Ast 1 : " + ast1)
- // println("Ast 2 : " + ast2)
- // println("Ast 1 root : " + getEqClassRoot(ast1))
- // println("Ast 2 root : " + getEqClassRoot(ast2))
- // println("Ast 1 class : " + getEqClassMembers(ast1).toList.mkString(", "))
- // println("Ast 2 class : " + getEqClassMembers(ast2).toList.mkString(", "))
- // println("Ast 1 parents : " + getParents(ast1).toList.mkString(", "))
- // println("Ast 2 parents : " + getParents(ast2).toList.mkString(", "))
-
- if (ast1 == mkEmptySet || ast2 == mkEmptySet) {
- val nonEmpty = if (ast1 == mkEmptySet) ast2 else ast1
- for (congruent <- getEqClassMembers(nonEmpty)) {
- for (parent <- getParents(congruent)) {
- z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) if decl == mkCard && args(0) == congruent =>
- assertAxiomSafe(z3.mkIff(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkCard(congruent), z3.mkInt(0, z3.mkIntSort))))
- case Z3AppAST(decl, args) if decl == mkUnion && args(0) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(congruent, args(1)), args(1))))
- case Z3AppAST(decl, args) if decl == mkUnion && args(1) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(args(0), congruent), args(0))))
- case Z3AppAST(decl, args) if decl == mkIntersect && args(0) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(congruent, args(1)), mkEmptySet)))
- case Z3AppAST(decl, args) if decl == mkIntersect && args(1) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkEq(congruent, mkEmptySet),
- z3.mkEq(mkUnion(args(0), congruent), mkEmptySet)))
- case _ =>;
- }
- }
- }
- }
- addClause(EqClause(z3ToTree(ast1), z3ToTree(ast2)))
- }
- ()
- }
-
- override def newDiseq(ast1: Z3AST, ast2: Z3AST) = safeBlockToAssertAxioms {
-
- if (z3.getSort(ast1) == mkSetSort) {
- // println("*** new Diseq : " + ast1 + " == " + ast2)
- // println("Ast 1 : " + ast1)
- // println("Ast 2 : " + ast2)
- // println("Ast 1 root : " + getEqClassRoot(ast1))
- // println("Ast 2 root : " + getEqClassRoot(ast2))
- // println("Ast 1 class : " + getEqClassMembers(ast1).toList.mkString(", "))
- // println("Ast 2 class : " + getEqClassMembers(ast2).toList.mkString(", "))
- // println("Ast 1 parents : " + getParents(ast1).toList.mkString(", "))
- // println("Ast 2 parents : " + getParents(ast2).toList.mkString(", "))
-
- if (ast1 == mkEmptySet || ast2 == mkEmptySet) {
- val nonEmpty = if (ast1 == mkEmptySet) ast2 else ast1
- for (congruent <- getEqClassMembers(nonEmpty)) {
- for (parent <- getParents(congruent)) {
- z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) if decl == mkCard && args(0) == congruent =>
- assertAxiomSafe(z3.mkImplies(
- z3.mkDistinct(congruent, mkEmptySet),
- z3.mkGT(mkCard(congruent), z3.mkInt(0, z3.mkIntSort))))
- case _ =>
- }
- }
- }
- }
- addClause(DiseqClause(z3ToTree(ast1), z3ToTree(ast2)))
- }
- ()
- }
-
- private def assertClause(clause: Clause) = clause match {
- case CardClause(bapaTree) =>
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkEq(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- case SingletonClause(tree) =>
- // nothing to do (except optimizations :P)
- case AssignClause(tree, polarity) =>
- val bapaTree = if (polarity) tree else !tree
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkIff(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- case EqClause(tree1, tree2) =>
- val bapaTree = tree1 seteq tree2
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkIff(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- case DiseqClause(tree1, tree2) =>
- val bapaTree = !(tree1 seteq tree2)
- val paTree = NaiveBapaToPaTranslator(bapaTree)
- assertAxiomSafe(z3.mkIff(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- }
-
- override def finalCheck: Boolean = safeBlockToAssertAxioms {
- println("\n==== Final check ====")
-
- val clauses = clauseStack.head flatMap {cl => cl}
- val boundary = getBoundaryElems
-
- clauseStack push new Stack[Seq[Clause]]
- clauseStack.head push Seq[Clause]()
-
- // Prints all clauses at final check
- /*
- println("Clauses\n")
- for (cl <- clauses) cl match {
- case CardClause(ast) =>
- println(z3ToTreeEqc(ast))
- case SingletonClause(ast) =>
- // nothing to do (except optimizations :P)
- case AssignClause(ast, polarity) =>
- val bapaTree = if (polarity) z3ToTreeEqc(ast) else !z3ToTreeEqc(ast)
- println(bapaTree)
- case EqClause(ast1, ast2) =>
- val bapaTree = z3ToTreeEqc(ast1) seteq z3ToTreeEqc(ast2)
- println(bapaTree)
- case DiseqClause(ast1, ast2) =>
- val bapaTree = !(z3ToTreeEqc(ast1) seteq z3ToTreeEqc(ast2))
- println(bapaTree)
- }
-// error("STOP")
- */
-
- val ((newClauses, newBoundary), newSymbols) = transformClausesAndBoundary(clauses, boundary)
-
- // Extend universe
- universe = universe addSets newSymbols
-
- println
- println("===> Number of set variables at final check : " + universe.setVariables.size
- + " (just added " + newSymbols.size + ")")
- println
-
- // Assert axioms for clauses
- newClauses foreach assertClause
-
- // Axioms for venn regions
- universe.assertAllAxioms
-
- // Axioms for implied set equalities
- val B = newBoundary.toArray
- for (i <- 0 until B.size; j <- 0 until i) {
- val bapaTree = B(i) seteq B(j)
- val paTree = NaiveBapaToPaTranslator(B(i) seteq B(j))
- assertAxiomSafe(z3.mkIff(
- treeToZ3(bapaTree),
- treeToZ3(paTree)
- ))
- }
-
- true
- }
-
- /* Transformations */
-
- def treeToZ3(tree: Tree): Z3AST = tree match {
- case Var(sym) => sym.ast
- case Lit(TrueLit) => z3.mkTrue
- case Lit(FalseLit) => z3.mkFalse
- case Lit(IntLit(i)) => z3.mkInt(i, z3.mkIntSort)
- case Op(AND, ts) => z3.mkAnd((ts map treeToZ3): _*)
- case Op(OR, ts) => z3.mkOr((ts map treeToZ3): _*)
- case Op(NOT, Seq(t)) => z3.mkNot(treeToZ3(t))
- case Op(IFF, Seq(t1, t2)) => z3.mkIff(treeToZ3(t1), treeToZ3(t2))
- case Op(EQ, Seq(t1, t2)) => z3.mkEq(treeToZ3(t1), treeToZ3(t2))
- case Op(LT, Seq(t1, t2)) => z3.mkLT(treeToZ3(t1), treeToZ3(t2))
- case Op(ADD, ts) => z3.mkAdd((ts map treeToZ3): _*)
- case Op(CARD, Seq(t)) => mkCard(treeToZ3(t))
- case Op(SETEQ, Seq(t1, t2)) => z3.mkEq(treeToZ3(t1), treeToZ3(t2))
- case Op(SUBSETEQ, Seq(t1, t2)) => mkSubsetEq(treeToZ3(t1), treeToZ3(t2))
- case Op(UNION, ts) => ts map treeToZ3 reduceLeft {(t1, t2) => mkUnion(t1, t2)}
- case Op(INTER, ts) => ts map treeToZ3 reduceLeft {(t1, t2) => mkIntersect(t1, t2)}
- case Op(COMPL, Seq(t)) => mkComplement(treeToZ3(t))
- case Lit(EmptySetLit) => mkEmptySet
- case _ => error("Unsupported conversion from BAPA-tree to Z3AST :\n" + tree)
- }
-
- def z3ToTree(ast: Z3AST): Tree = {
- if (ast == mkEmptySet) EmptySet
- else z3.getASTKind(ast) match {
- case Z3AppAST(decl, Nil) => SetSymbol(ast)
- case Z3AppAST(decl, args) if decl == mkSubsetEq => Op(SUBSETEQ, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkUnion => Op(UNION, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkIntersect => Op(INTER, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkComplement => Op(COMPL, args map z3ToTree)
- case Z3AppAST(decl, args) if decl == mkCard => Op(CARD, args map z3ToTree)
- case _ => SetSymbol(ast)
- }
- }
-
- private def mapClause(f: Tree => Tree)(clause: Clause): Clause = clause match {
- case CardClause(tree) => CardClause(f(tree))
- case SingletonClause(tree) => SingletonClause(f(tree))
- case AssignClause(tree, polarity) => AssignClause(f(tree), polarity)
- case EqClause(tree1, tree2) => EqClause(f(tree1), f(tree2))
- case DiseqClause(tree1, tree2) => DiseqClause(f(tree1), f(tree2))
- }
-
- private def transformClausesAndBoundary(clauses: Seq[Clause], boundary: Seq[Tree]): ((Seq[Clause], Seq[Tree]), Seq[Symbol]) = {
- def accept(f: Tree => Tree): (Seq[Clause], Seq[Tree]) = {
- val newClauses = clauses map mapClause(f)
- val newBoundary = boundary map f
- (newClauses, newBoundary)
- }
- eqcTransform(accept)
- }
-
- private def transformClause(clause: Clause): (Clause, Seq[Symbol]) = {
- eqcTransform(f => mapClause(f)(clause))
- }
-
- // Returns transformed clauses (after eqc lookup) and new symbols to add
- def eqcTransform[A](callback: (Tree => Tree) => A): (A, Seq[Symbol]) = {
- var symbolsBeingAdded = new ArrayBuffer[Symbol]
- def canonicalize2(tree: Tree): Tree = canonicalize(simplify(tree))
- def canonicalize(tree: Tree): Tree = tree match {
- case Var(symbol) => knownRepresentative(symbol)
- case Op(op, args) => Op(op, args map canonicalize)
- case Lit(_) => tree
- }
- // def canonicalize2(tree: Tree) = canonicalize(simplify(tree))
- // def canonicalize(clause: Clause): Clause = clause match {
- // case CardClause(tree) => CardClause(canonicalize2(tree))
- // case SingletonClause(tree) => SingletonClause(canonicalize2(tree))
- // case AssignClause(tree1, tree2) => AssignClause(canonicalize2(tree1), canonicalize2(tree2))
- // case EqClause(tree1, tree2) => AssignClause(canonicalize2(tree1), canonicalize2(tree2))
- // case DiseqClause(tree1, tree2) => AssignClause(canonicalize2(tree1), canonicalize2(tree2))
- // }
- def knownRepresentative(symbol: Symbol): Tree = {
- if (getEqClassMembers(symbol.ast) contains mkEmptySet) {
- // println("KNOWN REPRESENTATIVE : " + symbol + " -> " + EmptySet)
- return EmptySet
- }
- val knownSymbols = universe.variables ++ symbolsBeingAdded
- if (!(knownSymbols contains symbol)) {
- for (congruent <- getEqClassMembers(symbol.ast)) {
- val tree = z3ToTree(congruent)
- if (setVariables(tree) forall knownSymbols.contains) {
- // println("KNOWN REPRESENTATIVE : " + symbol + " -> " + tree)
- return tree
- }
- }
- // extend universe
- symbolsBeingAdded += symbol
- // universe += symbol
- }
- symbol
- }
- val result = callback(canonicalize2)
- // val newClauses = clauses map canonicalize
- (result, symbolsBeingAdded.toSeq)
- }
-
- // private val interpretedFunctions = Seq(mkCard, mkSubsetEq, mkUnion, mkIntersect, mkComplement)
-
- def getBoundaryElems = {
- // 'Smart' search that checks parents [BROKEN]
- /*
- for (elem <- getElems; if z3.getSort(elem) == mkSetSort; parent <- getParents(elem)) z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) =>
- if ((args contains elem) && (interpretedFunctions contains decl)) {
- boundary += z3ToTreeEqc(elem)
- }
- case _ =>
- }
- for (app <- getApps; if z3.getSort(app) == mkSetSort; parent <- getParents(app)) z3.getASTKind(parent) match {
- case Z3AppAST(decl, args) =>
- if ((args contains app) && (interpretedFunctions contains decl)) {
- boundary += z3ToTreeEqc(app)
- }
- case _ =>
- }
- */
-
- val boundary = MutableSet[Tree]()
- for (elem <- getElems; if z3.getSort(elem) == mkSetSort)
- boundary += z3ToTree(elem)
- for (app <- getApps; if z3.getSort(app) == mkSetSort)
- boundary += z3ToTree(app)
- boundary.toSeq
- }
-
- def NaiveBapaToPaTranslator(tree0: Tree) = {
- def rec(tree: Tree): Tree = tree match {
- case Op(CARD, Seq(set)) => universe translate set
- case Op(op, ts) => Op(op, ts map rec)
- case Var(_) | Lit(_) => tree
- }
- val tree1 = simplify(tree0)
- if (setVariables(tree1) exists {x => !(universe.variables contains x)}) {
- error("No new venn regions should be created at this point")
- }
- // universe = universe addSets setVariables(tree1)
- simplify(rec(simplify(rewriteSetRel(tree1))))
- }
-}
diff --git a/src/main/scala/leon/z3plugins/bapa/Bubbles.scala b/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
deleted file mode 100644
index 4763acae2542eb5b76613ae462bcf456b5e73b7b..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
+++ /dev/null
@@ -1,775 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package purescala.z3plugins.bapa
-
-import scala.collection.mutable.{HashSet => MutableSet, HashMap => MutableMap, ArrayBuffer}
-import scala.collection.{BitSet}
-import z3.scala._
-import AST._
-import NormalForms.simplify
-
-import scala.sys.error
-
-trait Bubbles {
-
- /* Flags */
-
-// val SHOW_INTERMEDIATE_STATISTICS = true
- val SHOW_INTERMEDIATE_STATISTICS = false
-
-// val SHOW_STATISTICS = true
- val SHOW_STATISTICS = false
-
-
- /* Connection to theory plugin */
-
- val z3: Z3Context
-
- private[bapa] val mkDomainSize: Z3AST
-
- protected def assertAxiomSafe(ast: Z3AST): Unit
-
- protected def treeToZ3(tree: Tree): Z3AST
-
- protected def z3ToTree(ast: Z3AST): Tree
-
- protected def BubbleBapaToPaTranslator(tree: Tree): Tree
-
- private def assertAxiomSafe(tree: Tree) {
- assertAxiomSafe(treeToZ3(simplify(tree)))
- }
-
- /* Definitions */
-
- type IDSet = BitSet
- type VRSet = BitSet
- type IDList = Seq[Int]
-
- case class SetName(name: String, sym: Symbol) {
- def complName = name.toLowerCase
- override def toString = name
- }
-
- case class VennRegion(name: String, ast: Z3AST) {
- def toTree = Var(IntSymbol(ast))
- override def toString = name
- }
-
- /* Cache of venn regions */
-
- private val cachedSymbolIDs = MutableMap[Symbol, Int]()
- private val cachedSymbols = new ArrayBuffer[Symbol]()
- private val cachedRegions = MutableMap[String, VennRegion]()
- private val mkZero = z3.mkInt(0, z3.mkIntSort)
-
- private def mkID(symbol: Symbol) = {
- cachedSymbolIDs getOrElse (symbol, {
- val id = cachedSymbols.size
- cachedSymbols += symbol
- cachedSymbolIDs(symbol) = id
- // println ("mkName " + symbol + " -> " + mkName(id))
- id
- })
- }
-
- private def mkName(id: Int) = ('A' + id).toChar.toString
-
- private def mkSym(id: Int) = cachedSymbols(id)
-
- private def mkRegion(idList: IDList, bitset: Long) = {
- def region(i: Int) = ((1L << i) & bitset) != 0
- val names = for (i <- 0 until idList.size) yield
- if (region(i)) mkName(idList(i))
- else mkName(idList(i)).toLowerCase
- val name = names.mkString
- cachedRegions getOrElse (name, {
- val region = VennRegion(name, z3.mkFreshConst(name, z3.mkIntSort))
- cachedRegions(name) = region
- region
- })
- }
-
- def idToName(ids: IDSet) = ids map mkName
-
-
- /* Bubbles */
-
- sealed abstract class AbstractBubble(val label: IDSet) {
- val ids: IDList = label.toSeq sortWith {_ < _}
- lazy val vennRegions: Array[VennRegion] = (Array tabulate (1 << ids.size)) {i => mkRegion(ids, i)}
-
- def numSetVars = ids.size
-
- def numFreeIntVars: Int
-
- def numVennRegions = vennRegions.size
-
- def mkVennAxiom = {
- z3.mkAnd(
- // Non-negative
- z3.mkAnd((vennRegions map {
- region =>
- z3.mkGE(region.ast, mkZero)
- }): _*
- ),
- // Sum is domain size
- z3.mkEq(
- mkDomainSize,
- z3.mkAdd((vennRegions map {_.ast}): _*)
- )
- )
- }
-
- def translate(tree: Tree): Tree = {
- val regions = translate0(tree).toSeq.sortWith {_ < _} map {i => vennRegions(i).toTree}
- if (regions.size > 0) Op(ADD, regions) else 0
- }
-
- private def translate0(tree: Tree): VRSet = tree match {
- case Lit(EmptySetLit) =>
- BitSet.empty
- case Op(COMPL, Seq(Lit(EmptySetLit))) =>
- BitSet((0 until vennRegions.size): _*)
- case Var(sym) =>
- if (sym.typ != SetType) error("Not a set variable : " + sym)
- val setNum = ids indexOf mkID(sym)
- if (setNum == -1) error("Unknown set '" + sym + "' aka " + mkName(mkID(sym)) + " in this bubble/edge : " + this)
- val regions = for (i <- 0 until vennRegions.size; if (i & (1 << setNum)) != 0) yield i
- BitSet(regions: _*)
- case Op(COMPL, Seq(Var(sym))) =>
- if (sym.typ != SetType) error("Not a set variable : " + sym)
- val setNum = ids indexOf mkID(sym)
- if (setNum == -1) error("Unknown set '" + sym + "' aka " + mkName(mkID(sym)) + " in this bubble/edge : " + this)
- val regions = for (i <- 0 until vennRegions.size; if (i & (1 << setNum)) == 0) yield i
- BitSet(regions: _*)
- case Op(UNION, ts) =>
- (ts map translate0 foldLeft BitSet.empty){_ ++ _}
- case Op(INTER, ts) =>
- val fullSet = BitSet((0 until vennRegions.size): _*)
- (ts map translate0 foldLeft fullSet){_ & _}
- case _ =>
- error("Not a simplified set expression : " + tree)
- }
- }
-
- // Node in Hyper-tree
- class Bubble(label: IDSet) extends AbstractBubble(label) {
- val edges = MutableSet[HyperEdge]()
- var component: Bubble = null
-
- def setVars = label map mkSym
-
- def numFreeIntVars = ids.size
-
- def toLongString = toString + " comp = " + component + " edges = " + edges
-
- override def toString = "b" + (label map mkName).mkString("(", "", ")")
-
- override def hashCode = label.hashCode
-
- override def equals(that: Any) =
- (that != null &&
- that.isInstanceOf[Bubble] &&
- that.asInstanceOf[Bubble].label == this.label)
-
- def mkImpliedEqAxioms = {
- val buffer = new ArrayBuffer[Z3AST]()
- val B = (Array tabulate ids.size)(i => mkSym(ids(i)))
- for (i <- 0 until B.size; j <- 0 until i) {
- val bapaTree = B(i) seteq B(j)
- val paTree = BubbleBapaToPaTranslator(bapaTree)
- buffer += z3.mkImplies(
- treeToZ3(paTree),
- treeToZ3(bapaTree)
- )
- }
- buffer
- }
- }
-
- // Edge in Hyper-tree
- class HyperEdge(label: IDSet) extends AbstractBubble(label) {
- val nodes = MutableSet[Bubble]()
-
- def addNode(bubble: Bubble) {
- bubble.edges += this
- nodes += bubble
- }
-
- def numFreeIntVars = {
- if (nodes exists {label subsetOf _.label}) {
- 0
- } else {
- vennRegions.size
- }
- }
-
- def toLongString = toString + " nodes = " + nodes
-
- override def toString = "e" + (label map mkName).mkString("(", "", ")")
-
- override def hashCode = label.hashCode
-
- override def equals(that: Any) =
- (that != null &&
- that.isInstanceOf[HyperEdge] &&
- that.asInstanceOf[HyperEdge].label == this.label)
-
- def mkAgreeAxioms = {
- val buffer = new ArrayBuffer[Tree]()
- for (node <- nodes) {
- val axiom = mkAxiom(node)
- if (axiom != null)
- buffer += axiom
- }
- buffer
- }
-
- private def mkAxiom(bubble: Bubble) = {
- val common = bubble.label & this.label
- val buffer = new ArrayBuffer[Tree]()
- def rec(ids: List[Int], sets: List[Tree]): Unit = ids match {
- case Nil =>
- val tree = Op(INTER, sets)
- buffer += (bubble translate tree) === (this translate tree)
- case s :: ss =>
- rec(ss, ~mkSym(s) :: sets)
- rec(ss, mkSym(s) :: sets)
- }
- if (bubble.label != this.label) {
- rec((bubble.label & this.label).toList, Nil)
- Op(AND, buffer)
- } else {
- null
- }
- }
- }
-
- private def unionFind(a: Bubble, b: Bubble, union: Boolean) = {
- var _a = a
- var _b = b
- var x = a
- var y = b
- while (x.component ne null) x = x.component
- while (y.component ne null) y = y.component
- while (_a.component ne null) {
- val t = _a
- _a = _a.component
- t.component = x
- }
- while (_b.component ne null) {
- val t = _b
- _b = _b.component
- t.component = y
- }
- if (union && (x ne y)) {
- y.component = x
- }
- (x eq y)
- }
-
- /* Universe */
-
- object Universe {
- val allBubbles = MutableMap[IDSet, Bubble]()
- val allEdges = MutableMap[IDSet, HyperEdge]()
-
- def addBubble(symbols: Set[Symbol]): (Bubble, Boolean) = {
- val symIDs = BitSet((symbols.toSeq map mkID): _*)
-
- allBubbles find {symIDs subsetOf _._1} match {
- case Some((_, bubble)) =>
- (bubble, false)
- case None =>
- // Create new bubble
- val bubble = new Bubble(symIDs)
-
- // Find common sets
- val intersections = for (bIDs <- allBubbles.keySet) yield bIDs & symIDs
- var core = Set[IDSet]()
- for (set <- intersections; if !set.isEmpty) {
- core = core filterNot {_ subsetOf set}
- if (!(core exists {set subsetOf _})) {
- core = core + set
- }
- }
- allBubbles(symIDs) = bubble
-
- // Create connections
- for (set <- core) {
- val bubbles = for (b <- allBubbles.values; if (b.label & set).nonEmpty) yield b
- val edge = collapseCycles(bubbles.toSeq, set)
- allEdges(edge.label) = edge
- }
-
- // Assert Axioms
- assertAxiomSafe(bubble.mkVennAxiom)
- bubble.mkImpliedEqAxioms foreach assertAxiomSafe
- for (edge <- bubble.edges) {
- assertAxiomSafe(edge.mkVennAxiom)
- edge.mkAgreeAxioms foreach assertAxiomSafe
- }
-
- if (SHOW_INTERMEDIATE_STATISTICS) showInfo2
-
- (bubble, true)
- }
- }
-
- private def collapseCycles(initialNodes: Seq[Bubble], initialLabel: IDSet) = {
- val nodesInNewEdge = MutableSet[Bubble](initialNodes: _*)
- var labelOfNewEdge = initialLabel
- // Merge and remove an edge
- def mergeEdge(edge: HyperEdge) {
- nodesInNewEdge ++= edge.nodes
- labelOfNewEdge ++= edge.label
- edge.nodes foreach {_.edges -= edge}
- edge.nodes.clear
- allEdges -= edge.label
- }
- // Find the paths from one bubble to some others
- def dfs(from: Bubble, to: Set[Bubble]) {
- val seen = MutableSet[Bubble](from)
- val prev = MutableMap[Bubble, (Bubble, HyperEdge)]()
- var stack = List(from)
- var numFound = 0
- while (stack.nonEmpty && numFound < to.size) {
- val node = stack.head
- stack = stack.tail
- for (edge <- node.edges; next <- edge.nodes; if !seen(next)) {
- seen(next) = true
- stack = next :: stack
- prev(next) = (node, edge)
- }
- if (to(node)) {
- numFound += 1
- var n = node
- while (n ne from) {
- val (b, e) = prev(n)
- if (e != null) {
- mergeEdge(e)
- prev(n) = (b, null)
- }
- n = b
- }
- }
- }
- if (numFound != to.size) error("Could not find all destinations !!!")
- }
- // Partition into components and collapse inner paths
- val partitions = MutableMap[Bubble, MutableSet[Bubble]]()
-// val oneNode = initialNodes.iterator.next
-// partitions(oneNode) = initialNodes.toSet - oneNode
- for (node <- initialNodes) partitions find {n => unionFind(node, n._1, false)} match {
- case Some((_, set)) => set += node
- case None => partitions(node) = new MutableSet[Bubble]()
- }
- for ((from, to) <- partitions; if to.nonEmpty) dfs(from, to.toSet)
- val first = partitions.keys.iterator.next
- for (node <- partitions.keys) unionFind(first, node, true)
- // Build edge
- val edge = new HyperEdge(labelOfNewEdge)
- nodesInNewEdge foreach edge.addNode
- edge
- }
-
- def removeBubble(node: Bubble) {
- def rebuildUnionFind {
- for (bubble <- allBubbles.values) bubble.component = null
- for (edge <- allEdges.values) {
- val node1 = edge.nodes.iterator.next
- for (node <- edge.nodes; if node != node1)
- unionFind(node1, node, true)
- }
- }
- for (edge <- node.edges) {
- edge.nodes -= node
- if (edge.nodes.size <= 1) {
- edge.nodes foreach {_.edges -= edge}
- edge.nodes.clear
- allEdges -= edge.label
- } else {
- var labelOfNewEdge = BitSet.empty
- for (node1 <- edge.nodes; node2 <- edge.nodes; if node1 != node2) {
- labelOfNewEdge ++= node1.label & node2.label
- }
- if (!(labelOfNewEdge subsetOf edge.label)) {
- println("edge : " + edge.label)
- println("new : " + labelOfNewEdge)
- }
- require(labelOfNewEdge subsetOf edge.label)
- if (labelOfNewEdge.size < edge.label.size) {
- val nodesInNewEdge = new ArrayBuffer() ++ edge.nodes
- edge.nodes foreach {_.edges -= edge}
- edge.nodes.clear
- allEdges -= edge.label
- // Build edge
- val newEdge = new HyperEdge(labelOfNewEdge)
- nodesInNewEdge foreach newEdge.addNode
- allEdges(newEdge.label) = newEdge
- assertAxiomSafe(newEdge.mkVennAxiom)
- newEdge.mkAgreeAxioms foreach assertAxiomSafe
- }
- }
- }
- node.edges.clear
- allBubbles -= node.label
- rebuildUnionFind
- }
-
-// /*
- def showState {
- println("------------")
- println("Bubbles :")
- allBubbles.values foreach {x => println(x.toLongString)}
- println
-
- println("Edges :")
- allEdges.values foreach {x => println(x.toLongString)}
- println
- }
-// */
- }
-
- /* Misc */
-
- def showInfo = if (SHOW_STATISTICS) showInfo2
-
- def showInfo2 {
-
- val setVars = MutableSet[Symbol]()
- val bubbleSizes = new ArrayBuffer[Int]()
- val edgeSizes = new ArrayBuffer[Int]()
- var bubbleSum = 0
- var edgeSum = 0
-
- for (bubble <- Universe.allBubbles.values) {
- bubbleSizes += bubble.numSetVars
- bubbleSum += bubble.numFreeIntVars
- setVars ++= bubble.setVars
- }
- for (edge <- Universe.allEdges.values) {
- edgeSizes += edge.numSetVars
- edgeSum += edge.numFreeIntVars
- }
-
- println("________________________________________")
- println
- println("# set variables : " + setVars.size)
- println("# bubbles : " + bubbleSizes.size)
- println("# venn regions for bubbles : " + bubbleSum)
- println("# hyper edges : " + edgeSizes.size)
- println("# venn regions for edges : " + edgeSum)
- println("# venn regions (total) : " + (bubbleSum + edgeSum))
- println("________________________________________")
- println
- println("Bubble sizes : " + bubbleSizes.mkString("{", ", ", "}"))
- println("Edge sizes : " + edgeSizes.mkString("{", ", ", "}"))
- println("Set variables : " + setVars.mkString("{", ", ", "}"))
- println
- }
-
-
- /* Model construction */
-
- import scala.collection.mutable.{BitSet => MutableBitSet, StringBuilder}
-
- val mkSingleton: Z3FuncDecl
- val mkCard: Z3FuncDecl
-
-
- def toBapaModel(z3model: Z3Model): BAPAModel = {
-
- case class Node(label: BitSet, regions: MutableMap[BitSet,Int]) {
- var parent : Node = null
- val neighbors = new MutableSet[Node]()
- val content = new MutableMap[BitSet,MutableSet[Int]]()
-
- override def hashCode = label.hashCode
-
- override def equals(that: Any) =
- (that != null &&
- that.isInstanceOf[Node] &&
- that.asInstanceOf[Node].label == this.label)
-
- def addNeighbor(node: Node) {
- if (node != this) {
- this.neighbors += node
- node.neighbors += this
- }
- }
-
- def name = (label map mkName).mkString
-
- override def toString = {
- "Node " + name +
- " parent = " + (if (parent == null) "null" else parent.name) +
- " neighbors = " + (neighbors map {_.name})
- }
- }
-
- val cache = new MutableMap[BitSet,Option[Node]]()
- val nodeOrder = new ArrayBuffer[Node]()
- var errorVennRegion: String = null
-
- // Read model for venn regions and add them to the cache
- def bubbleToNode(bubble: AbstractBubble) = cache getOrElse(bubble.label, {
- var regions = new MutableMap[BitSet,Int]()
- def indexToIDset(index: Int): BitSet = {
- val idset = MutableBitSet()
- for (i <- 0 until bubble.numSetVars; if (index & (1 << i)) != 0) {
- idset += bubble.ids(i)
- }
- idset
- }
- var failure = false
- for (i <- 0 until bubble.numVennRegions) {
- z3model.evalAs[Int](bubble.vennRegions(i).ast) match {
- case Some(size) =>
- if (size > 0) {
- val ids = indexToIDset(i)
- regions(ids) = size
- }
- case None =>
- failure = true
- if (errorVennRegion == null) {
- errorVennRegion = "evalAs[Int] on venn region failed ! " + bubble.vennRegions(i).ast
- }
- }
- }
- val result = if (failure) None else Some(Node(bubble.label, regions))
- cache(bubble.label) = result
-// if (bubble.isInstanceOf[Bubble]) print("Bubble ") else print("Edge ")
-// println((bubble.label map mkName).mkString + " => " + result.toString)
- result
- })
- // Initialize data structures
- def init {
- // (Try to) read sizes of venn regions and build the new tree
- for (bubble <- Universe.allBubbles.values; bnode <- bubbleToNode(bubble); edge <- bubble.edges; enode <- bubbleToNode(edge)) {
- bnode addNeighbor enode
- }
- // Build ordering over the new tree
- val seen = new MutableSet[Node]()
- def dfs(from: Node) {
- seen += from
- var stack = List(from)
- while (stack.nonEmpty) {
- val node = stack.head
- stack = stack.tail
- nodeOrder += node
- for (next <- node.neighbors; if !seen(next)) {
- seen(next) = true
- next.parent = node
- stack = next :: stack
- }
- }
- }
- for (opt <- cache.values; node <- opt) if (!seen(node)) dfs(node)
- }
- // Create a set of representative integers for each venn region
- def populate {
- var lastInt = 0
- def nextInt = {
- lastInt += 1
- lastInt
- }
- def nextSeq(size: Int) = {
- val temp = lastInt + 1
- lastInt += size
- new MutableSet() ++ (temp to lastInt)
- }
- def fillInitial(node: Node) {
- for ((reg, size) <- node.regions) {
- node.content(reg) = nextSeq(size)
- }
- }
- def fillNext(from: Node, to: Node) {
- val copiedRegions = new MutableMap[BitSet,Int]() ++ to.regions
- for ((reg2, _) <- copiedRegions) to.content(reg2) = new MutableSet[Int]()
- for ((reg, set) <- from.content; elem <- set) {
- val relevant = reg & to.label
- def matches(entry: (BitSet,Int)) = (entry._1 & from.label) == relevant
- copiedRegions find matches match {
- case None => error("Uuh, this is bad...")
- case Some((reg2, size)) =>
- to.content(reg2) += elem
- if (size > 1) {
- copiedRegions(reg2) = size - 1
- } else {
- copiedRegions -= reg2
- require(size == 1)
- }
- }
- }
- }
- for (node <- nodeOrder) {
- if (node.parent == null) fillInitial(node)
- else fillNext(node.parent, node)
- }
- }
- // Reconstruct sets from venn regions
- def reconstruct = {
- val recons = new MutableMap[Int,MutableSet[Int]]()
- for (node <- nodeOrder; setID <- node.label) {
- val set = new MutableSet[Int]()
- for ((reg, elems) <- node.content; if reg(setID)) set ++= elems
-// println(mkName(setID) + " = " + set + " because " + node)
- if (recons contains setID) {
- if (recons(setID) != set) {
- // DEBUG: assertion failed
-// printDebug
- error("Inconsistent set " + mkSym(setID) + " aka " + mkName(setID) + " " +
- set + " != " + recons(setID))
- }
- } else {
- recons(setID) = set
- }
- }
-// for ((setID, set) <- recons) {
-// println("Set " + mkSym(setID) + " aka " + mkName(setID) + " : " + set)
-// }
-// println(recons)
- recons
- }
- // Evalute cardinality as integer
- def evalAsBapaInt(ast: Z3AST) = z3.getASTKind(ast) match {
- case Z3AppAST(decl, args) if decl == mkCard =>
- val ast2 = treeToZ3(BubbleBapaToPaTranslator(z3ToTree(ast)))
- z3model.evalAs[Int](ast2)
- case _ => None
- }
- // DEBUG: print stuff
- def printDebug {
- println("=== Nodes ===")
- for (node <- nodeOrder) {
- println(node)
- for ((bits, set) <- node.content) {
- println(" " + (idToName(bits).mkString) + " -> " + set)
- }
- }
- println("=== Hyper tree ===")
- Universe.showState
- }
- // rename elements such that singletons sets have a correct representation
- def singletons(recons: MutableMap[Int,MutableSet[Int]]) = {
- val map = new MutableMap[Int,Int]()
- val rev = new MutableMap[Int,Int]()
- def rename(i: Int) = map getOrElse(i, i)
- def reverse(i: Int) = rev getOrElse(i, i)
-
- for ((setID, content) <- recons) {
- z3.getASTKind(mkSym(setID).ast) match {
- case Z3AppAST(decl, args) if decl == mkSingleton =>
- val evaluated = z3model.evalAs[Int](args(0))
- (if (evaluated.isEmpty) evalAsBapaInt(args(0)) else evaluated) match {
- case Some(rElem) =>
- require(recons(setID).size == 1)
- val lCurrent = recons(setID).iterator.next
-// println(mkSym(setID).ast + " " + lCurrent + " -> " + rElem)
- val rCurrent = rename( lCurrent )
- val lElem = reverse( rElem )
- if (rCurrent != rElem) {
- map(lCurrent) = rElem
- map(lElem) = rCurrent
- rev(rCurrent) = lElem
- rev(rElem) = lCurrent
-// for ((i,j) <- map) println(i+ " -> " + j)
- }
- case None =>
- println("WARNING : evalAs[Int] on singleton element failed ! " + mkSym(setID).ast )
-// for (ast <- getEqClassMembers(args(0))) println("> " + ast)
- }
- case _ =>
- }
- }
-// for ((i,j) <- map) println(i+ " -> " + j)
- recons map { case (id,ctnt) => {
-// println(mkSym(id).toString + " " + ctnt + " -> " + (ctnt map rename))
- (id, ctnt map rename)
- }}
- }
- // Create model object
- def toModel(recons: MutableMap[Int,MutableSet[Int]]) = {
- val blacklist = new MutableSet[Z3AST]()
- for ((_, venn) <- cachedRegions) blacklist += venn.ast
- val result = MutableMap[Z3AST,Set[Int]]()
- for ((id, set) <- recons) result(mkSym(id).ast) = set.toSet
- BAPAModel(z3model, result.toMap, blacklist.toSet, null)
- }
- try {
- init
- populate
- // printDebug
- // Universe.showState
- // nodeOrder foreach println
- toModel(singletons(reconstruct))
- } catch {
- case ex: Throwable =>
- var err = ex.toString
- if (errorVennRegion != null) err += "\nPossible cause :\n " + errorVennRegion
- BAPAModel(z3model, Map.empty[Z3AST,Set[Int]], Set.empty[Z3AST], err)
- }
- }
-// def getEqClassMembers(ast: Z3AST) : Iterator[Z3AST]
-}
-
-/* Bapa model class */
-
-case class BAPAModel(z3model: Z3Model, setModel: Map[Z3AST,Set[Int]], blacklist: Set[Z3AST], error: String = null) {
-
- def evalAsIntSet(ast: Z3AST) = setModel get ast
-
- override def toString = {
- val buf = new StringBuilder()
- // Z3 model
- /*
- val temp = new ArrayBuffer[(String,String)]()
- for (decl <- z3model.getConstants) {
- val app = decl()
- if (!blacklist(app)) z3model eval app match {
- case None =>
- case Some(ast) =>
- temp += app.toString -> ast.toString
- }
- }
- temp sortWith {_._1 < _._1}
- val max1 = (temp foldLeft 0){(a,b) => scala.math.max(a, b._1.size)}
- for ((name, value) <- temp) {
- val n = max1 - name.size
- buf ++= " " + name + (" " * n) +" -> " + value + "\n"
- }
- */
- // TODO: HACK ! (scalaZ3 interface has no model navigation yet)
- val badstart = blacklist map {_.toString}
- val lines = (z3model.toString split '\n').toList filterNot {line =>
- badstart exists {line startsWith _}
- }
- buf ++= "Z3 model :\n"
- for (line <- lines) {
- buf ++= " "
- buf ++= line
- buf += '\n'
- }
- // BAPA model
- if (error == null) {
- def format(pair: (Z3AST, Set[Int])): (String, String) = (pair._1.toString, pair._2.toList.sortWith{_ < _}.mkString("{ "," "," }"))
- val pairs = (setModel.toList map format) sortWith {_._1 < _._1}
- val max2 = (pairs foldLeft 0){(a,b) => scala.math.max(a, b._1.size)}
- buf ++= "BAPA model :\n"
- for ((name, set) <- pairs) {
- val n = max2 - name.size
- buf ++= " "
- buf ++= name
- buf ++= " " * n
- buf ++= " -> "
- buf ++= set
- buf += '\n'
- }
- } else {
- buf ++= "An error occurred while creating the BAPA model :\n "
- buf ++= error
- }
- buf.toString
- }
-}
diff --git a/src/main/scala/leon/z3plugins/bapa/NormalForms.scala b/src/main/scala/leon/z3plugins/bapa/NormalForms.scala
deleted file mode 100644
index 5d90172626093ede0b2e3bae98d26a6e7185bf69..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/NormalForms.scala
+++ /dev/null
@@ -1,127 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package purescala.z3plugins.bapa
-
-import z3.scala.Z3Context
-import AST._
-
-object NormalForms {
- def boolVariables(tree: Tree) = variables(tree, _ == BoolType)
-
- def intVariables(tree: Tree) = variables(tree, _ == IntType)
-
- def setVariables(tree: Tree) = variables(tree, _ == SetType)
-
- private def variables(tree0: Tree, pred: Type => Boolean): Set[Symbol] = {
- val set = new scala.collection.mutable.HashSet[Symbol]
- def rec(tree: Tree): Unit = tree match {
- case Var(sym) if pred(sym.typ) => set += sym
- case Op(_, ts) => ts foreach rec
- case _ =>
- }
- rec(tree0)
- set.toSet
- }
-
- // replace Seteq and Subseteq with Card(...) = 0
- def rewriteSetRel(tree: Tree): Tree = tree match {
- case Op(SETEQ, Seq(s1, s2)) =>
- rewriteSetRel(s1 subseteq s2) && rewriteSetRel(s2 subseteq s1)
- case Op(SUBSETEQ, Seq(s1, s2)) =>
- (s1 ** ~s2).card === 0
- case Op(NOT, Seq(Op(SETEQ, Seq(s1, s2)))) =>
- rewriteSetRel(!(s1 subseteq s2)) || rewriteSetRel(!(s2 subseteq s1))
- case Op(NOT, Seq(Op(SUBSETEQ, Seq(s1, s2)))) =>
- (s1 ** ~s2).card > 0
- case Op(op@(AND | OR | NOT), ts) =>
- Op(op, ts map rewriteSetRel)
- case Op(EQ, Seq(t1, t2@Op(CARD, _))) =>
- t2 === t1
- case _ => tree
- }
-
- def simplify(tree: Tree): Tree = tree match {
- case Lit(_) | Var(_) => tree
- case Op(AND, ts) => flatten(ts, AND, True, False)
- case Op(OR, ts) => flatten(ts, OR, False, True)
- case Op(NOT, Seq(Op(NOT, Seq(t)))) => simplify(t)
- case Op(NOT, Seq(Op(AND, ts))) => simplify(Op(OR, ts map {~_}))
- case Op(NOT, Seq(Op(OR, ts))) => simplify(Op(AND, ts map {~_}))
- case Op(NOT, Seq(t)) => simplify(t) match {
- case Lit(TrueLit) => False
- case Lit(FalseLit) => True
- case tt => !tt
- }
- case Op(INTER, ts) => flatten(ts, INTER, FullSet, EmptySet)
- case Op(UNION, ts) => flatten(ts, UNION, EmptySet, FullSet)
- case Op(COMPL, Seq(Lit(EmptySetLit))) => FullSet
- case Op(COMPL, Seq(Lit(FullSetLit))) => EmptySet
- case Op(COMPL, Seq(Op(COMPL, Seq(t)))) => simplify(t)
- case Op(COMPL, Seq(Op(INTER, ts))) => simplify(Op(UNION, ts map {~_}))
- case Op(COMPL, Seq(Op(UNION, ts))) => simplify(Op(INTER, ts map {~_}))
- case Op(CARD, Seq(Lit(EmptySetLit))) => 0
- // case Op(ITE, Seq(c, t, e)) => simplify(c) match {
- // case Lit(TrueLit) => simplify(t)
- // case Lit(FalseLit) => simplify(e)
- // case cond => cond ifThenElse (simplify(t), simplify(e))
- // }
- case Op(ADD, ts) =>
- var intPart = 0
- val acc = new scala.collection.mutable.ListBuffer[Tree]
- for (t <- ts) simplify(t) match {
- case Lit(IntLit(i)) => intPart += i
- case tt => acc += tt
- }
- if (intPart != 0) acc += intPart
- acc.size match {
- case 0 => 0
- case 1 => acc(0)
- case _ => Op(ADD, acc.toSeq)
- }
- case Op(IFF, Seq(t1, t2)) => (simplify(t1), simplify(t2)) match {
- case (tt1, Lit(TrueLit)) => tt1
- case (tt1, Lit(FalseLit)) => simplify(!tt1)
- case (Lit(TrueLit), tt2) => tt2
- case (Lit(FalseLit), tt2) => simplify(!tt2)
- case (tt1, tt2) => tt1 iff tt2
- }
- case Op(EQ, Seq(t1, t2)) => (simplify(t1), simplify(t2)) match {
- case (Lit(l1), Lit(l2)) => if (l1 == l2) True else False
- case (tt1, tt2) => tt1 === tt2
- }
- case Op(op, ts) => Op(op, ts map simplify)
- }
-
- private def flatten(ts: Seq[Tree], operand: Operand, neutral: Tree, absorbing: Tree) = {
- def flat(t: Tree) = t match {
- case Op(op, ts) if op == operand => ts
- case _ => Seq(t)
- }
- val trees = ts map simplify filterNot {_ == neutral}
- if (trees contains absorbing) absorbing
- else trees flatMap flat match {
- case Nil => neutral
- case Seq(t) => t
- case ts => Op(operand, ts)
- }
- }
-
-
- def purify(z3: Z3Context, tree0: Tree) = tree0
- // Used to be that this replaced the cardinality function with the cardinality operator...
- // def purify(z3: Z3Context, tree0: Tree) = {
- // var defs: Seq[Tree] = Nil
- // def rec(tree: Tree): Tree = tree match {
- // case Op(EQ, Seq(Op(CARD, Seq(s)), t)) => Op(CARD_PRED, Seq(rec(s), rec(t)))
- // case Op(EQ, Seq(t, Op(CARD, Seq(s)))) => Op(CARD_PRED, Seq(rec(s), rec(t)))
- // case Op(CARD, Seq(s)) =>
- // val t = Var(IntSymbol(z3.mkFreshConst("pure", z3.mkIntSort)))
- // defs = defs :+ Op(CARD_PRED, Seq(rec(s), t))
- // t
- // case Op(op, ts) => Op(op, ts map rec)
- // case Var(_) | Lit(_) => tree
- // }
- // val tree1 = rec(tree0)
- // if (defs.size > 0) Op(AND, defs :+ tree1) else tree1
- // }
-}
diff --git a/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala b/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
deleted file mode 100644
index 882727d53f24ac5ced3eeb70b8b7ea7fb243dd86..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
+++ /dev/null
@@ -1,122 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package purescala.z3plugins.bapa
-
-import scala.text.{Document, DocBreak}
-import scala.language.implicitConversions
-
-import Document._
-import AST._
-
-import scala.sys.error
-
-object PrettyPrinter {
-
- /* Interface */
-
- def apply(tree: Tree) = writeString(p(tree))
-
-
- /* Implementation */
-
- private val indent = 2
- private val docWidth = 80
-
- private def writeString(doc: Document) = {
- val writer = new java.io.StringWriter()
- doc.format(docWidth, writer)
- writer.flush()
- writer.toString
- }
-
-
- // Helper methods
- private implicit def stringToDoc(s: String): Document = text(s)
- private val nl: Document = DocBreak
- private def g(d: Document) = group(d)
- private def n(d: Document) = nest(indent, d)
- private def gn(d: Document) = g(n(d))
- private def op(sep: Document, d: Document): Document = op(sep, Seq(d))
- private def op(sep: Document, d1: Document, d2: Document): Document = op(sep, Seq(d1, d2))
- private def op(sep: Document, docs: Seq[Document]): Document = docs.toList match {
- case Nil => empty
- case List(d) => sep :: d
- case d :: ds =>
- gn((d :: (ds map {dd => g(sep :: " " :: dd)})) reduceLeft {_ :/: _})
- // n(ds reduceLeft {(doc, di) => g(g(doc :: " " :: sep) :/: di)})
- }
- private def list(docs: Seq[Document]) = docs.toSeq match {
- case Nil => empty
- case Seq(d) => d
- case ds => n(ds reduceLeft {(doc, di) => g(doc :: "," :/: di)})
- }
- private def plist(ds: Seq[Document]) = paren(list(ds))
- private def blist(ds: Seq[Document]) = brace(list(ds))
- private def paren(d: Document): Document = "(" :: d :: ")"
- private def brace(d: Document): Document = "{" :: d :: "}"
- private def block(d: Document): Document = gn("{" :/: d :/: "}")
-
- // Symbols
- val (_AND, _OR, _NOT, _IFF, _IMPL, _DEF) = ("n", "v", "!", "<=>", "==>", ":=")
- val (_EQ, _NE, _LE, _LT, _GE, _GT) = ("==", "!=", "<=", "<", ">=", ">")
- val (_NEG) = ("-")
- val (_SEQ, _SNE, _SSEQ, _SSNE, _EMPTYSET, _FULLSET, _UNION, _INTER, _COMPL) = ("s==", "!s==", "s<=", "!s<=", "{}", "{full}", "++", "**", "~")
-
- // Beautify names
- /*
- private var counter = 0
- private val map = new scala.collection.mutable.HashMap[Symbol,String]
- private def lookup(sym: Symbol) = map getOrElse(sym, {
- counter += 1
- val name = sym.typ match {
- case BoolType => "p_" + counter
- case IntType => "t" + counter
- case SetType => "S" + counter
- }
- map(sym) = name
- name
- })
- */
-
- // print with parens (if necessary)
- private def pp(tree: Tree): Document = tree match {
- case Var(_) | Lit(_) | Op(_, Seq(_)) => p(tree)
- case _ => paren(p(tree))
- }
-
- // print with braces (if necessary)
- private def bp(tree: Tree): Document = tree match {
- case Var(_) | Lit(_) | Op(_, Seq(_)) => p(tree)
- case _ => block(p(tree))
- }
-
- // print without parens
- private def p(tree: Tree): Document = tree match {
- case Var(sym) => sym.name // lookup(sym)
- case Lit(TrueLit) => "true"
- case Lit(FalseLit) => "false"
- case Lit(EmptySetLit) => _EMPTYSET
- case Lit(FullSetLit) => _FULLSET
- case Lit(IntLit(i)) => i.toString
- case Op(OR, ts) => op(_OR, ts map pp)
- case Op(AND, ts) => op(_AND, ts map pp)
- case Op(NOT, Seq(Op(SETEQ, ts))) => op(_SNE, ts map pp)
- case Op(NOT, Seq(Op(SUBSETEQ, ts))) => op(_SSNE, ts map pp)
- case Op(NOT, Seq(Op(EQ, ts))) => op(_NE, ts map pp)
- case Op(NOT, Seq(Op(LT, ts))) => op(_GE, ts map pp)
- case Op(NOT, Seq(t)) => op(_NOT, pp(t))
- case Op(IFF, ts) => op(_IFF, ts map pp)
- case Op(EQ, ts) => op(_EQ, ts map pp)
- case Op(LT, ts) => op(_LT, ts map pp)
- case Op(SETEQ, ts) => op(_SEQ, ts map pp)
- case Op(SUBSETEQ, ts) => op(_SSEQ, ts map pp)
- case Op(ADD, ts) => op("+", ts map pp)
- case Op(CARD, Seq(t)) => "|" :: pp(t) :: "|"
- case Op(UNION, ts) => op(_UNION, ts map pp)
- case Op(INTER, ts) => op(_INTER, ts map pp)
- case Op(COMPL, Seq(t)) => op(_COMPL, pp(t))
- case Op(op, args) => error("Unhandled Op-tree : Op(" + op + ", #" + args.size + ")")
- case Lit(lit) => error("Unhandled Lit-tree : Lit(" + lit + ")")
- case _ => error("Unhandled tree : " + tree.getClass)
- }
-}
diff --git a/src/main/scala/leon/z3plugins/bapa/VennRegions.scala b/src/main/scala/leon/z3plugins/bapa/VennRegions.scala
deleted file mode 100644
index 4640690700dd5a781a3bcac6b68b7815aa877858..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/z3plugins/bapa/VennRegions.scala
+++ /dev/null
@@ -1,181 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package purescala.z3plugins.bapa
-
-import scala.collection.mutable.{ArrayBuffer,HashMap}
-import z3.scala.{Z3Context, Z3AST, Z3Theory}
-import AST._
-
-import scala.sys.error
-
-trait VennRegions {
- val z3: Z3Context
- protected def assertAxiomSafe(ast: Z3AST): Unit
-
- case class SetName(name: String, sym: Symbol) {
- def complName = name.toLowerCase
- override def toString = name
- }
-
- case class VennRegion(name: String, ast: Z3AST) {
- def toTree = Var(IntSymbol(ast))
- override def toString = name
- }
-
- /* Cache */
-
- private val cachedNames = new HashMap[Symbol, SetName]
- private val cachedRegions = new HashMap[String, VennRegion]
- private var namesCounter = 0
- private val mkZero = z3.mkInt(0, z3.mkIntSort)
-
- private def mkName(sym: Symbol) = {
- cachedNames getOrElse (sym, {
- val name = SetName(('A' + namesCounter).toChar.toString, sym)
- namesCounter += 1
- cachedNames(sym) = name
-// println("*** New Set : " + sym + " -> '" + name + "' ***")
- name
- })
- }
-
- private def mkRegion(sets: Seq[SetName], region: Long) = {
- val names = for (i <- 0 until sets.size) yield
- if ((region & (1 << i)) != 0) sets(i).name
- else sets(i).complName
- val name = (names sortWith {_.toLowerCase < _.toLowerCase}).mkString
- cachedRegions getOrElse(name, {
- val region = VennRegion(name, z3.mkFreshConst(name, z3.mkIntSort))
- cachedRegions(name) = region
- region
- })
- }
-
- /* Venn region bookkeeping */
-
- sealed abstract class Universe {
- val setVariables: Seq[SetName]
- val vennRegions: Array[VennRegion]
-
- def variables = setVariables map {_.sym}
-
- def addSet(symbol: Symbol) = {
- val name = mkName(symbol)
- if (setVariables contains name) {
- this
- } else {
-// println("Adding set: " + symbol)
-// println("AKA : " + name)
- new ExtendedUniverse(name, this)
- }
- }
-
- def addSets(symbols: Iterable[Symbol]) = {
- var universe = this
- for (sym <- symbols) universe = universe addSet sym
- universe
- }
-
- def translate(tree: Tree): Tree = {
- val regions = translate0(tree).toSeq.sortWith{_ < _} map {i => vennRegions(i).toTree}
- if (regions.size > 0) Op(ADD, regions) else 0
- }
-
- private def translate0(tree: Tree): Set[Int] = tree match {
- case Lit(EmptySetLit) =>
- Set.empty
- case Op(COMPL, Seq(Lit(EmptySetLit))) =>
- val regions = new scala.collection.mutable.HashSet[Int]
- for (i <- 0 until vennRegions.size)
- regions += i
- regions.toSet
- case Var(sym) =>
- if (sym.typ != SetType) error("Not a set variable : " + sym)
- val setNum = setVariables indexOf mkName(sym)
- if (setNum == -1) error("Unknown set in this universe : " + sym)
- val regions = new scala.collection.mutable.HashSet[Int]
- for (i <- 0 until vennRegions.size; if (i & (1 << setNum)) != 0)
- regions += i
- regions.toSet
- case Op(COMPL, Seq(Var(sym))) =>
- if (sym.typ != SetType) error("Not a set variable : " + sym)
- val setNum = setVariables indexOf mkName(sym)
- val regions = new scala.collection.mutable.HashSet[Int]
- for (i <- 0 until vennRegions.size; if (i & (1 << setNum)) == 0)
- regions += i
- regions.toSet
- case Op(UNION, ts) =>
- ts map translate0 reduceLeft {_ ++ _}
- case Op(INTER, ts) =>
- ts map translate0 reduceLeft {_ & _}
- case _ =>
- error("Not a simplified set expression : " + tree)
- }
-
- def assertAllAxioms: Unit
- }
-
- class EmptyUniverse(val domainSize: Z3AST) extends Universe {
- val setVariables = Nil
- val vennRegions = Array(VennRegion("UnivRegion", domainSize))
- def assertAllAxioms { }
- }
-
- class ExtendedUniverse(setVar: SetName, val parent: Universe) extends Universe {
- val setVariables = parent.setVariables :+ setVar
- val (vennRegions, axioms) = {
- if (setVariables.size > 16) {
- println("WARNING: Creating venn regions for more than 16 set variables (" + setVariables.size + " variables).")
-// error("More than 16 set variables")
- }
- val n = parent.vennRegions.size
- val _vennRegions = new Array[VennRegion](2 * n)
- val _axioms = new ArrayBuffer[Z3AST](3 * n)
-
- for (i <- 0 until n) {
- val old = parent.vennRegions(i)
- val vr1 = mkRegion(setVariables, i)
- val vr2 = mkRegion(setVariables, i + n)
- _vennRegions(i) = vr1
- _vennRegions(i + n) = vr2
- _axioms += z3.mkEq(old.ast, z3.mkAdd(vr1.ast, vr2.ast))
- _axioms += z3.mkGE(vr1.ast, mkZero)
- _axioms += z3.mkGE(vr2.ast, mkZero)
-// val axiom = z3.mkAnd(axiom1, axiom2, axiom3)
-// assertAxiom(axiom)
-// println(axiom)
-// assertAxiomEventually(axiom1)
-// assertAxiomEventually(axiom2)
-// assertAxiomEventually(axiom3)
-// println(axiom1)
-// println(axiom2)
-// println(axiom3)
-// println("*** " + old.ast + " := " + vr1.ast + " + " + vr2.ast)
- }
- (_vennRegions, _axioms.toArray)
- }
- assertAllAxioms
-
- def assertAllAxioms {
- parent.assertAllAxioms
- axioms foreach assertAxiomSafe
- }
- /*
- // (Ab = 0 & aB = 0) <=> A = B
- {
- val a = Var(setVar.sym)
- for (oldSetVar <- parent.setVariables) {
- val b = Var(oldSetVar.sym)
-// println("******** LOOOL : " + (a seteq b))
- val tree = (
- (translate(a ** ~b) === 0) &&
- (translate(~a ** b) === 0)
- ) iff (a seteq b)
- assertAxiomEventually(tree)
- }
- }
- */
- }
-}
-
-
diff --git a/unmanaged/32/cafebabe_2.10-1.2.jar b/unmanaged/32/cafebabe_2.10-1.2.jar
deleted file mode 120000
index 37f428a8b2941987bdc522bac7e2fa90c0f37467..0000000000000000000000000000000000000000
--- a/unmanaged/32/cafebabe_2.10-1.2.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/cafebabe_2.10-1.2.jar
\ No newline at end of file
diff --git a/unmanaged/32/insynth_2.10-2.1.jar b/unmanaged/32/insynth_2.10-2.1.jar
deleted file mode 120000
index 49be391b699bbe7d8f1f4b004e3be9633cefe4f4..0000000000000000000000000000000000000000
--- a/unmanaged/32/insynth_2.10-2.1.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/insynth_2.10-2.1.jar
\ No newline at end of file
diff --git a/unmanaged/32/vanuatoo_2.10-0.1.jar b/unmanaged/32/vanuatoo_2.10-0.1.jar
deleted file mode 120000
index 5148a49942a1aed689b0dc4d5b6ec5729aef14e1..0000000000000000000000000000000000000000
--- a/unmanaged/32/vanuatoo_2.10-0.1.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/vanuatoo_2.10-0.1.jar
\ No newline at end of file
diff --git a/unmanaged/64/cafebabe_2.10-1.2.jar b/unmanaged/64/cafebabe_2.10-1.2.jar
deleted file mode 120000
index 37f428a8b2941987bdc522bac7e2fa90c0f37467..0000000000000000000000000000000000000000
--- a/unmanaged/64/cafebabe_2.10-1.2.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/cafebabe_2.10-1.2.jar
\ No newline at end of file
diff --git a/unmanaged/64/cafebabe_2.11-1.2.jar b/unmanaged/64/cafebabe_2.11-1.2.jar
new file mode 120000
index 0000000000000000000000000000000000000000..0fe546385fa30c7ea45764e3c7ff32bd89238380
--- /dev/null
+++ b/unmanaged/64/cafebabe_2.11-1.2.jar
@@ -0,0 +1 @@
+../common/cafebabe_2.11-1.2.jar
\ No newline at end of file
diff --git a/unmanaged/64/insynth_2.10-2.1.jar b/unmanaged/64/insynth_2.10-2.1.jar
deleted file mode 120000
index 49be391b699bbe7d8f1f4b004e3be9633cefe4f4..0000000000000000000000000000000000000000
--- a/unmanaged/64/insynth_2.10-2.1.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/insynth_2.10-2.1.jar
\ No newline at end of file
diff --git a/unmanaged/64/scalaz3-unix-64b-2.1.jar b/unmanaged/64/scalaz3-unix-64b-2.1.jar
index e9d6572886481b8c0294453ea4ec0d22e8bb2c24..db94f26380b6b5a7eaab64ed730b03d48cf23f46 100644
Binary files a/unmanaged/64/scalaz3-unix-64b-2.1.jar and b/unmanaged/64/scalaz3-unix-64b-2.1.jar differ
diff --git a/unmanaged/64/vanuatoo_2.10-0.1.jar b/unmanaged/64/vanuatoo_2.10-0.1.jar
deleted file mode 120000
index 5148a49942a1aed689b0dc4d5b6ec5729aef14e1..0000000000000000000000000000000000000000
--- a/unmanaged/64/vanuatoo_2.10-0.1.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/vanuatoo_2.10-0.1.jar
\ No newline at end of file
diff --git a/unmanaged/64/vanuatoo_2.11-0.1.jar b/unmanaged/64/vanuatoo_2.11-0.1.jar
new file mode 120000
index 0000000000000000000000000000000000000000..304c722aa43cd9667428ce8b83c12797a53255cd
--- /dev/null
+++ b/unmanaged/64/vanuatoo_2.11-0.1.jar
@@ -0,0 +1 @@
+../common/vanuatoo_2.11-0.1.jar
\ No newline at end of file
diff --git a/unmanaged/common/cafebabe_2.10-1.2.jar b/unmanaged/common/cafebabe_2.10-1.2.jar
deleted file mode 100644
index 4dc1806689a5932ddc8097afe769df62f2d5ffbb..0000000000000000000000000000000000000000
Binary files a/unmanaged/common/cafebabe_2.10-1.2.jar and /dev/null differ
diff --git a/unmanaged/common/cafebabe_2.11-1.2.jar b/unmanaged/common/cafebabe_2.11-1.2.jar
new file mode 100644
index 0000000000000000000000000000000000000000..a1b985a60e625b09235ed91ca6a279321fc8bb85
Binary files /dev/null and b/unmanaged/common/cafebabe_2.11-1.2.jar differ
diff --git a/unmanaged/common/vanuatoo_2.10-0.1.jar b/unmanaged/common/vanuatoo_2.10-0.1.jar
deleted file mode 100644
index 47eb1687a76e47f9d117b13b647da86d1eb8b340..0000000000000000000000000000000000000000
Binary files a/unmanaged/common/vanuatoo_2.10-0.1.jar and /dev/null differ
diff --git a/unmanaged/common/vanuatoo_2.11-0.1.jar b/unmanaged/common/vanuatoo_2.11-0.1.jar
new file mode 100644
index 0000000000000000000000000000000000000000..9550eb732bb464d91853cb6edc5fcedee9f8f481
Binary files /dev/null and b/unmanaged/common/vanuatoo_2.11-0.1.jar differ