From 25803b6f9bf8231b069b1d7aa685cd692cc39227 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Sat, 21 Aug 2010 21:33:45 +0000
Subject: [PATCH] some cleaning up, and a now correct handling of singletons
etc.
---
src/purescala/Reporter.scala | 2 +-
src/purescala/Z3Solver.scala | 2 +-
src/purescala/z3plugins/bapa/AST.scala | 63 +----
src/purescala/z3plugins/bapa/BAPATheory.scala | 95 ++------
.../z3plugins/bapa/BapaToPaTranslator.scala | 222 ------------------
.../z3plugins/bapa/NormalForms.scala | 10 +-
.../z3plugins/bapa/PrettyPrinter.scala | 4 -
.../z3plugins/bapa/VennRegions.scala | 9 +-
vmcai2011-testcases/CADE07.scala | 48 ----
vmcai2011-testcases/JustFormulas.scala | 5 +-
vmcai2011-testcases/Nasty.scala | 2 +-
11 files changed, 45 insertions(+), 417 deletions(-)
delete mode 100644 src/purescala/z3plugins/bapa/BapaToPaTranslator.scala
diff --git a/src/purescala/Reporter.scala b/src/purescala/Reporter.scala
index 7261d1121..a9bb02141 100644
--- a/src/purescala/Reporter.scala
+++ b/src/purescala/Reporter.scala
@@ -27,7 +27,7 @@ class DefaultReporter extends Reporter {
protected val fatalPfx = "[ Fatal ] "
def output(msg: String) : Unit = {
- Console.err.println(msg)
+ /*Console.err.*/println(msg)
}
protected def reline(pfx: String, msg: String) : String = {
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index f502ffd3d..d9697d291 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -394,7 +394,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
z3.mkSetDifference(rec(s1), rec(s2))
}
case f @ FiniteSet(elems) => if(f.getType == IntSetType) {
- throw new CantTranslateException
+ elems.map(e => bapa.mkSingleton(rec(e))).reduceLeft(bapa.mkUnion(_,_))
} else {
elems.foldLeft(z3.mkEmptySet(typeToSort(f.getType.asInstanceOf[SetType].base)))((ast,el) => z3.mkSetAdd(ast,rec(el)))
}
diff --git a/src/purescala/z3plugins/bapa/AST.scala b/src/purescala/z3plugins/bapa/AST.scala
index 44bad9a9e..2f2a328f3 100644
--- a/src/purescala/z3plugins/bapa/AST.scala
+++ b/src/purescala/z3plugins/bapa/AST.scala
@@ -5,10 +5,8 @@ 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))
@@ -24,7 +22,7 @@ object AST {
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(then: Tree, elze: Tree) = Op(ITE, Seq(this, then, elze))
+// def ifThenElse(then: Tree, elze: Tree) = Op(ITE, Seq(this, then, elze))
def card = Op(CARD, Seq(this))
def ++(tree: Tree) = Op(UNION, Seq(this, tree))
def **(tree: Tree) = Op(INTER, Seq(this, tree))
@@ -35,34 +33,7 @@ object AST {
case class Lit(lit: Literal) extends Tree
case class Var(sym: Symbol) extends Tree
- /* AST extractors */
-
- // Seems to be broken (scala bug ?)
- /*
- object UnOp {
- def unapply(tree: Tree): Option[(Operand, Tree)] = tree match {
- case Op(op, Seq(t)) => Some(op, t)
- case _ => None
- }
- }
-
- object BinOp {
- def unapply(tree: Tree): Option[(Operand, Tree, Tree)] = tree match {
- case Op(op, Seq(t1, t2)) => Some(op, t1, t2)
- case _ => None
- }
- }
-
- object TernOp {
- def unapply(tree: Tree): Option[(Operand, Tree, Tree, Tree)] = tree match {
- case Op(op, Seq(t1, t2, t3)) => Some(op, t1, t2, t3)
- case _ => None
- }
- }
- */
-
/* Literals */
-
sealed abstract class Literal
case object TrueLit extends Literal
case object FalseLit extends Literal
@@ -91,16 +62,11 @@ object AST {
case object IFF extends Operand("<=>")
case object EQ extends Operand("==")
case object LT extends Operand("<")
- case object LESS extends Operand("<<") // less-than for min / max
case object SETEQ extends Operand("seteq")
case object SUBSETEQ extends Operand("subseteq")
// return integers
case object ADD extends Operand("+")
- case object ITE extends Operand("IF-THEN-ELSE")
case object CARD extends Operand("CARD")
-// case object CARD_PRED extends Operand("CARD-predicate")
- case object MIN extends Operand("MIN")
- case object MAX extends Operand("MAX")
// return sets
case object UNION extends Operand("++")
case object INTER extends Operand("**")
@@ -125,36 +91,9 @@ object AST {
that.asInstanceOf[Symbol].ast.ptr == this.ast.ptr )
}
-
-// object Symbol {
- /*
- def apply(typ: Type, z3: Z3Context, ast: Z3AST): Symbol = z3.getASTKind(ast) match {
- case Z3AppAST(decl, Nil) =>
-// val name = z3sym2string(z3, z3.getDeclName(decl))
- new Symbol(typ, z3.getDeclName(decl).toString, ast)
- case Z3AppAST(decl, Seq(set)) =>
- //val name = "Z3_TH_" + z3.getDeclName(decl) + "(" + set + ")"
- new Symbol(typ, decl(set).toString, ast)
- case bad => error("Z3AST is not a variable : " + bad)
- }
- */
-// def apply(typ: Type, z3: Z3Context, ast: Z3AST): Symbol =
-// new Symbol(typ, ast)
- /*
- def unapply(sym: Symbol): Option[(Type,Z3AST)] =
- Some(sym.typ, sym.ast)
- */
-// }
-
-// private def z3sym2string(z3: Z3Context, sym: Z3Symbol): String = z3.getSymbolKind(sym) match {
-// case Z3IntSymbol(i) => i.toString
-// case Z3StringSymbol(s) => s
-// }
-
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/purescala/z3plugins/bapa/BAPATheory.scala b/src/purescala/z3plugins/bapa/BAPATheory.scala
index 089e5f646..7baf60c7d 100644
--- a/src/purescala/z3plugins/bapa/BAPATheory.scala
+++ b/src/purescala/z3plugins/bapa/BAPATheory.scala
@@ -9,10 +9,7 @@ import AST._
import NormalForms.{simplify, rewriteSetRel, setVariables, purify}
class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with VennRegions {
- // def this() = this(new Z3Context(new Z3Config("MODEL" -> true)))
- //def this() = this(new Z3Context(new Z3Config("MODEL" -> true, "RELEVANCY" -> 0)))
setCallbacks(
-// initSearch = true,
reduceApp = true,
finalCheck = true,
push = true,
@@ -25,33 +22,32 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
restart = true
)
-// This makes the Theory Proxy print out all calls that are forwarded to the theory.
- //showCallbacks(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 mkIsSingleton = mkUnarySetfun("IsSingleton", z3.mkBoolSort)
+ val mkSingleton = mkTheoryFuncDecl(z3.mkStringSymbol("Singleton"), Seq(z3.mkIntSort), mkSetSort)
val mkCard = mkUnarySetfun("Cardinality", z3.mkIntSort)
- // val mkCardPred = mkTheoryFuncDecl(z3.mkStringSymbol("HasCardinality"), Seq(mkSetSort, z3.mkIntSort), z3.mkBoolSort)
- val mkElementOf = mkTheoryFuncDecl(z3.mkStringSymbol("IsElementOf"), Seq(z3.mkIntSort, mkSetSort), z3.mkBoolSort)
- val mkAsSingleton = mkTheoryFuncDecl(z3.mkStringSymbol("AsSingleton"), Seq(z3.mkIntSort), mkSetSort)
- val mkAsElement = mkUnarySetfun("AsElement", 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)
- val mkDomainSize = z3.mkFreshConst("DomainSize", z3.mkIntSort)
+
+ private[bapa] val mkDomainSize = z3.mkFreshConst("DomainSize", z3.mkIntSort)
+ 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 mkConst(name: String) = mkTheoryConstant(z3.mkStringSymbol(name), mkSetSort)
+ def mkSetConst(name: String) = mkTheoryConstant(z3.mkStringSymbol(name), mkSetSort)
def mkFreshConst(name: String) = {
freshCounter += 1
- mkConst(name + "." + freshCounter)
+ mkSetConst(name + "." + freshCounter)
}
private def mkUnarySetfun(name: String, rType: Z3Sort) =
@@ -60,14 +56,13 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
mkTheoryFuncDecl(z3.mkStringSymbol(name), Seq(mkSetSort, mkSetSort), rType)
/* Theory stack */
-
private val stack = new Stack[Universe]
stack push new EmptyUniverse(mkDomainSize)
/* Callbacks */
def assertAxiom2(ast: Z3AST) {
- //println("Asserting: " + ast)
+ println("Asserting: " + ast)
assertAxiom(ast)
}
@@ -93,13 +88,11 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
}
override def reset {
- knownSetExprs = Nil
axiomsToAssert.clear
stack.clear
}
override def restart {
- knownSetExprs = Nil
axiomsToAssert.clear
stack.clear
}
@@ -232,24 +225,15 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
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 =>
+ //XXXX
+ assertAxiomEventually(z3.mkEq(mkAsElement(ast), args(0)))
+ assertAxiomEventually(z3.mkEq(mkCard(ast), z3.mkInt(1, z3.mkIntSort)))
case _ =>
// ignore other functions
}
}
- override def initSearch : Unit = {
- // Indicates that mkUnion is commutative
- // val b1 = z3.mkBound(0, mkSetSort)
- // val b2 = z3.mkBound(1, mkSetSort)
- // val pattern = z3.mkPattern(mkUnion(b1, b2))
- // val axiomTree = z3.mkEq(mkUnion(b1,b2),mkUnion(b2,b1))
- // // TODO: make sure these symbols are unique.
- // val bn1 = z3.mkIntSymbol(0)
- // val bn2 = z3.mkIntSymbol(1)
- // val axiom = z3.mkForAll(0, List(pattern), List((bn1, mkSetSort), (bn2, mkSetSort)), axiomTree)
- // z3.assertCnstr(axiom)
- }
-
// TODO: add reductions for union & inter (empty set) and compl (nnf ?)
override def reduceApp(fd: Z3FuncDecl, args: Z3AST*) : Option[Z3AST] = {
if (fd == mkCard) {
@@ -266,25 +250,19 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
} else {
None
}
- } else if (fd == mkIsSingleton) {
- if (args(0) == mkEmptySet) {
- Some(z3.mkFalse)
- } 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 {
- val singleton = z3.mkFreshConst("singleton", mkSetSort)
- Some(z3.mkAnd(
- mkIsSingleton(singleton),
- z3.mkEq(mkAsSingleton(elem), singleton),
- z3.mkEq(mkAsElement(singleton), elem),
- mkSubsetEq(singleton, set)
- ))
+ Some(mkSubsetEq(mkSingleton(elem), set))
}
} else {
None
@@ -309,14 +287,12 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
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(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(ITE, Seq(t1, t2, t3)) => z3.mkITE(treeToZ3_rec(t1), treeToZ3_rec(t2), treeToZ3_rec(t3))
case Op(CARD, Seq(t)) => mkCard(treeToZ3_rec(t))
-// case Op(CARD_PRED, Seq(s, t)) => mkCardPred(treeToZ3_rec(s), 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):_*)
@@ -326,26 +302,7 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
case _ => error("Unsupported conversion from BAPA-tree to Z3AST :\n" + tree)
}
- private var knownSetExprs: List[Z3AST] = Nil
- private def knownRepresentative(set: Z3AST) : Z3AST = {
- // This can get slow in theory. I'd use a Set for inClass, but the hashing
- // of Z3AST does not seem to work like it should. We need to check whether
- // we can trust the C pointer to be a valid hash.
- var inClass: List[Z3AST] = getEqClassMembers(set).toList
- // println(" -- Equivalence class contains " + getEqClassMembers(set).toList)
- // println(" -- List is " + knownSetExprs)
-
- val result = knownSetExprs.find(inClass.contains(_)) match {
- case Some(repr) => repr
- case None => {
- knownSetExprs = knownSetExprs ::: List(set)
- set
- }
- }
-
- // println(" -- Known representative for : " + set + " is : " + result)
- result
- }
+ def knownRepresentative(ast: Z3AST) : Z3AST = ast
def z3ToTree(ast: Z3AST): Tree = z3.getASTKind(ast) match {
case _ if ast == mkEmptySet => EmptySet
@@ -354,7 +311,7 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
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 == 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 _ =>
diff --git a/src/purescala/z3plugins/bapa/BapaToPaTranslator.scala b/src/purescala/z3plugins/bapa/BapaToPaTranslator.scala
deleted file mode 100644
index ea8afcfaa..000000000
--- a/src/purescala/z3plugins/bapa/BapaToPaTranslator.scala
+++ /dev/null
@@ -1,222 +0,0 @@
-package purescala.z3plugins.bapa
-
-import scala.math.{log, min}
-import AST._
-import NormalForms.{setVariables, rewriteSetRel, simplify}
-import z3.scala.Z3Context
-
-class BapaToPaTranslator(z3: Z3Context) {
- //private implicit def rangeToSeq[T](r: IndexedSeq[T]): Seq[T] = r.toSeq
-
- // returns a PA formula and the number of Venn regions
- def apply(formula: Tree): (Tree, Int) = {
- val setvars = setVariables(formula)
- val formula1 = simplify(rewriteSetRel(formula))
- val (atoms, zeroes, ones) = countCardinalityExpressions(formula1)
- val n0 = findSparsenessBound(atoms - zeroes - ones)
- val n = if (setvars.size <= 30) min(n0 + ones, 1 << setvars.size)
- else (n0 + ones)
- val body = reduce(n)(formula1)
- /*
- println("In QFBAPAtoPATranslator:")
- f1.print
- println("** Set variables : " + setvars)
- println("** #atoms : " + atoms)
- println("** #cards = 0 : " + zeroes)
- println("** #cards <= 1 : " + ones)
- println("** d : " + (atoms - zeroes - ones))
- println("** sparseness bound : " + n0)
- println("** body : ")
- body.print
-*/
- /*
- println("** Set variables : " + setvars)
- println("** sparseness bound : " + n0 +" (+ " + ones + ")")
- println("** n : " + n)
- */
- /* if (setvars.isEmpty)
-(True, 0)
-else */
- val buf = new scala.collection.mutable.ArrayBuffer[Tree]
- buf += body
- buf ++= nonNegativeCards(n)
- buf ++= breakSymmetry(n, setvars.toSeq)
- (simplify(Op(AND, buf.toSeq)), n)
- }
-
- // Create / cache fresh variables
- private val cache = new scala.collection.mutable.HashMap[String,Var]
-
- private def lookup(varName: String, typ: Type) = cache getOrElse(varName, {
- val freshVar = typ match {
- case BoolType => Var(BoolSymbol(z3.mkFreshConst(varName, z3.mkBoolSort)))
- case IntType => Var(IntSymbol(z3.mkFreshConst(varName, z3.mkIntSort)))
- case SetType => error("no new set variables allowed")
- }
- cache(varName) = freshVar
- freshVar
- })
-
- private def propVar(k: Int, sym: Symbol): Tree = lookup(sym.name + "_" + k, BoolType) //Symbol.beta(k, id)
-
- private def intVar(k: Int): Tree = lookup("venn_" + k, IntType)//Symbol.vennSize(k, i)
-
-
- // translate BA to PA expression
- // Generate formula of the form
- // (if st0 then l_k else 0)
- // where st0 is the result of replacing, in setTerm, the set variables with k-family
- // of propositional variables, as given by set2prop.
- def ba2pa(setTree: Tree, k: Int): Tree = {
- def set2prop(stree: Tree): Tree = stree match {
- case Var(sym) => propVar(k, sym)
- case Lit(EmptySetLit) => False
- case Lit(FullSetLit) => True
- case Op(COMPL, Seq(set)) => !set2prop(set)
- case Op(UNION, sets) => Op(OR, sets map set2prop)
- case Op(INTER, sets) => Op(AND, sets map set2prop)
- case _ => throw IllegalTerm(setTree)
- }
- set2prop(setTree) ifThenElse (intVar(k), 0)
- //Op(ITE(set2prop(setTerm)), List(intVar(k), 0))
- }
-
- // reduce QFBAPA formula f to QFPA formula,
- // introducing only n generic partition cardinality variables
- // pre: formula is in nnf
- def reduce(n: Int) = {
- /*
- def reduceFormula(form: Formula): Formula = form match {
- case True | False | PropVar(_) => form
- case Not(f) => !reduceFormula(f)
- case And(fs) => And(fs map reduceFormula)
- case Or(fs) => Or(fs map reduceFormula)
- case Predicate(c: IntLogical, ts) => Predicate(c, ts map reduceTerm)
- case _ => throw IllegalTerm(form)
- }
- def reduceTerm(term: Term): Term = term match {
- case Op(CARD, List(set)) =>
- if (n == 0) 0 else Op(ADD, for (k <- 1 to n) yield ba2pa(set, k, eqClassNum))
- case Op(c, ts) =>
- Op(c, ts map reduceTerm)
- case Lit(_) | TermVar(_) => term
- }
- */
- def reduceTree(tree: Tree): Tree = tree match {
- case Op(CARD, Seq(set)) =>
- if (n == 0) 0
- else Op(ADD, for (k <- 1 to n) yield ba2pa(set, k))
- case Op(op, args) =>
- Op(op, args map reduceTree)
- case _ => tree
- }
- reduceTree _
- }
-
- // Extractor for countCardinalityExpressions
- private object ExCardLessEqual {
- def unapply(tree: Tree): Option[(Tree, Int)] = tree match {
- case Op(EQ, Seq(Lit(IntLit(card)), Op(CARD, Seq(set)))) => Some((set, card))
- case Op(EQ, Seq(Op(CARD, Seq(set)), Lit(IntLit(card)))) => Some((set, card))
-/*GE*/case Op(NOT, Seq(Op(LT, Seq(Lit(IntLit(card)), Op(CARD, Seq(set)))))) => Some((set, card))
-// case Op(LE, Seq(Op(CARD, Seq(set)), Lit(IntLit(card)))) => Some((set, card))
-// case Op(GT, Seq(Lit(IntLit(card)), Op(CARD, Seq(set)))) => Some((set, card - 1))
-/*LT*/case Op(LT, Seq(Op(CARD, Seq(set)), Lit(IntLit(card)))) => Some((set, card - 1))
- case _ => None
- }
- }
-
- def countCardinalityExpressions(tree0: Tree): (Int, Int, Int) = {
- var atoms = 0
- var cardIs0 = 0
- var cardIs1 = 0
- /*
- def countFormula(form: Formula): Unit = form match {
- case And(fs) => fs foreach countFormula
- case Or(fs) => fs foreach countFormula
- case ExCardLessEqual(_, 0) => cardIs0 += 1; atoms += 1
- case ExCardLessEqual(_, 1) => cardIs1 += 1; atoms += 1
- case Predicate(c: IntLogical, ts) => ts foreach countTerm
- case True | False | PropVar(_) => ()
- case _ => IllegalTerm(form)
- }
- def countTerm(term: Term): Unit = term match {
- case Op(CARD, List(Lit(_))) => ()
- case Op(CARD, _) => atoms += 1
- case Op(_, ts) => ts foreach countTerm
- case _ => ()
- }
- */
- def countTree(tree: Tree): Unit = tree match {
- case ExCardLessEqual(_, 0) => cardIs0 += 1; atoms += 1
- case ExCardLessEqual(_, 1) => cardIs1 += 1; atoms += 1
- case Op(CARD, Seq(Lit(_))) => ()
- case Op(CARD, _) => atoms += 1
- case Op(_, ts) => ts foreach countTree
- case _ => ()
- }
- countTree(tree0)
- (atoms, cardIs0, cardIs1)
- }
-
- // symmetry_breaking predicate says that
- // propositional variables denote a strictly
- // increasing sequence of regions (lexical ordering)
- private val BREAK_SYMMETRY = true
-
- def breakSymmetry(n: Int, svars: Seq[Symbol]): Seq[Tree] =
- if (BREAK_SYMMETRY)
- Seq.tabulate(n - 1)(i => mkIndexLess(i + 1)(svars))
- else Nil
-
- private def mkIndexLess(i: Int) = {
- def rec(sets: Seq[Symbol]): Tree = sets match {
- case Nil => True
- case Seq(s) =>
- // prop less
- val varI = propVar(i, s)
- val varI_1 = propVar(i + 1, s)
- !varI && varI_1
- case s :: ss =>
- // prop equal
- val varI = propVar(i, s)
- val varI_1 = propVar(i + 1, s)
- // TODO: looks like if-and-only-if constraint
-// val equal = (!varI && !varI_1) || (varI && varI_1)
-// rec(Seq(s)) || (equal && rec(ss))
- rec(Seq(s)) || ((varI iff varI_1) && rec(ss))
- }
- rec _
- }
-
- // Imposes non-negativity for cardinalities of venn regions
- private def nonNegativeCards(n: Int): Seq[Tree] =
- for (i <- 1 to n) yield 0 <= intVar(i)
-
- // compute the largest n such that 2^n <= (n+1)^d
- def findSparsenessBound(d: Int) = {
- // Check if 2^n <= (n+1)^d by taking log of both sides
- def small_n(n: Int) = n * log(2) <= d * log(n + 1)
- def binSearch(low: Int, high: Int): Int = {
- if (high <= low + 1) {
- if (small_n(high))
- high
- else
- low
- } else {
- val mid = (high + low) / 2
- if (small_n(mid))
- binSearch(mid, high)
- else
- binSearch(low, mid)
- }
- }
- if (d <= 3)
- d
- else {
- val a0 = d * log(d)
- val b0 = 2 * d * (1 + log(d))
- binSearch(a0.toInt, b0.toInt)
- }
- }
-}
diff --git a/src/purescala/z3plugins/bapa/NormalForms.scala b/src/purescala/z3plugins/bapa/NormalForms.scala
index 26d732e14..1dbb597cf 100644
--- a/src/purescala/z3plugins/bapa/NormalForms.scala
+++ b/src/purescala/z3plugins/bapa/NormalForms.scala
@@ -57,11 +57,11 @@ object NormalForms {
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(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]
diff --git a/src/purescala/z3plugins/bapa/PrettyPrinter.scala b/src/purescala/z3plugins/bapa/PrettyPrinter.scala
index 9c05a918a..62a2c7ab8 100644
--- a/src/purescala/z3plugins/bapa/PrettyPrinter.scala
+++ b/src/purescala/z3plugins/bapa/PrettyPrinter.scala
@@ -105,10 +105,6 @@ object PrettyPrinter {
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(ITE, Seq(c, t, e)) =>
- g(gn("if" :/: pp(c)) :/:
- gn("then" :/: bp(t)) :/:
- gn("else" :/: bp(e)))
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)
diff --git a/src/purescala/z3plugins/bapa/VennRegions.scala b/src/purescala/z3plugins/bapa/VennRegions.scala
index 601b70fca..dc2e1fa87 100644
--- a/src/purescala/z3plugins/bapa/VennRegions.scala
+++ b/src/purescala/z3plugins/bapa/VennRegions.scala
@@ -55,8 +55,13 @@ trait VennRegions {
def addSet(symbol: Symbol) = {
val name = mkName(symbol)
- if (setVariables contains name) this
- else new ExtendedUniverse(name, this)
+ if (setVariables contains name) {
+ this
+ } else {
+ println("Adding set: " + symbol)
+ println("AKA : " + name)
+ new ExtendedUniverse(name, this)
+ }
}
def addSets(symbols: Iterable[Symbol]) = {
diff --git a/vmcai2011-testcases/CADE07.scala b/vmcai2011-testcases/CADE07.scala
index f6f47f72f..aa18c20d7 100644
--- a/vmcai2011-testcases/CADE07.scala
+++ b/vmcai2011-testcases/CADE07.scala
@@ -10,11 +10,6 @@ object CADE07 {
listContent ++ Set(x)
} ensuring(_.size == listContent.size + 1)
- def vc2r(x: Set[Int], listContent: Set[Int]) : Set[Int] = {
- require(x.size == 1 && !x.subsetOf(listContent))
- listContent ++ x
- } ensuring(_.size == listContent.size + 1)
-
def vc2a(listRoot: Int, list: Set[Int], x: Int, listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
require(
list.contains(listRoot)
@@ -26,19 +21,6 @@ object CADE07 {
listContent ++ Set(x)
} ensuring(_.size == listContent.size + 1)
- def vc2ar(listRoot: Set[Int], list: Set[Int], x: Set[Int], listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
- require(
- listRoot.size == 1
- && listRoot.subsetOf(list)
- && x.size == 1
- && !x.subsetOf(listContent)
- && listContent.subsetOf(objectAlloc)
- && x.subsetOf(objct)
- && x.subsetOf(objectAlloc))
-
- listContent ++ x
- } ensuring(_.size == listContent.size + 1)
-
def vc2b(listRoot: Int, list: Set[Int], x: Int, listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
require(
list.contains(listRoot)
@@ -49,28 +31,10 @@ object CADE07 {
listContent ++ Set(x)
} ensuring(_.size == listContent.size + 1)
- def vc2br(listRoot: Set[Int], list: Set[Int], x: Set[Int], listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
- require(
- listRoot.size == 1
- && listRoot.subsetOf(list)
- && x.size == 1
- && listContent.subsetOf(objectAlloc)
- && x.subsetOf(objct)
- && x.subsetOf(objectAlloc)
- )
-
- listContent ++ x
- } ensuring(_.size == listContent.size + 1)
-
def vc3(x: Int, listContent: Set[Int]) : Set[Int] = {
listContent ++ Set(x)
} ensuring(_.size <= listContent.size + 1)
- def vc3r(x: Set[Int], listContent: Set[Int]) : Set[Int] = {
- require(x.size == 1)
- listContent ++ x
- } ensuring(_.size <= listContent.size + 1)
-
def vc6(x: Int, c: Set[Int], c1: Set[Int], alloc0: Set[Int], alloc1: Set[Int], alloc2: Set[Int]) : Set[Int] = {
require(
c.contains(x)
@@ -81,16 +45,4 @@ object CADE07 {
alloc2 -- alloc0
} ensuring(_.size <= c.size)
-
- def vc6r(x: Set[Int], c: Set[Int], c1: Set[Int], alloc0: Set[Int], alloc1: Set[Int], alloc2: Set[Int]) : Set[Int] = {
- require(
- x.size == 1
- && x.subsetOf(c)
- && c1 == c -- x
- && (alloc1 -- alloc0).size <= 1
- && (alloc2 -- alloc1).size <= c1.size
- )
-
- alloc2 -- alloc0
- } ensuring(_.size <= c.size)
}
diff --git a/vmcai2011-testcases/JustFormulas.scala b/vmcai2011-testcases/JustFormulas.scala
index 731cc8270..7a046abc3 100644
--- a/vmcai2011-testcases/JustFormulas.scala
+++ b/vmcai2011-testcases/JustFormulas.scala
@@ -27,7 +27,7 @@ object JustFormulas {
def vc5_V(x: Int, y: Int, a: Set[Int], b: Set[Int]) : Boolean = {
require(
a.contains(f1(x))
- && b.contains(f1(x))
+ && b.contains(f1(y))
&& x < y + 1
&& 2*y - 1 < 2*x
)
@@ -36,7 +36,8 @@ object JustFormulas {
def vc6_V(x: Int, y: Int, a: Set[Int], b: Set[Int]) : Boolean = {
require(
- f2(a).contains(x)
+ (!((a -- b).size == 0 && (b -- a).size == 0) || a == b)
+ && f2(a).contains(x)
&& f2(b).contains(y)
&& (a -- b) == Set.empty[Int]
&& (b -- a) == Set.empty[Int]
diff --git a/vmcai2011-testcases/Nasty.scala b/vmcai2011-testcases/Nasty.scala
index e317f7ae7..b9c3d9024 100644
--- a/vmcai2011-testcases/Nasty.scala
+++ b/vmcai2011-testcases/Nasty.scala
@@ -103,5 +103,5 @@ object Nasty {
&& (objAlloc16 -- objAlloc30).size <= s241.size
)
objAlloc16 -- objAlloc
- } ensuring(_.size < s142.size)
+ } ensuring(_.size <= s142.size)
}
--
GitLab