Skip to content
Snippets Groups Projects
Commit ba443cd1 authored by Philippe Suter's avatar Philippe Suter
Browse files

new unrealistic VCs that work well

parent d4d7decf
Branches
Tags
No related merge requests found
......@@ -22,7 +22,6 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
)
Z3Global.toggleWarningMessages(true)
// we restart Z3 for each new program
private var z3: Z3Context = null
private var bapa: BAPATheory = null
private var program: Program = null
......@@ -49,6 +48,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
bapa = new BAPATheory(z3)
counter = 0
prepareSorts
prepareFunctions
}
private var counter = 0
......
......@@ -24,7 +24,7 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
// This makes the Theory Proxy print out all calls that are
// forwarded to the theory.
showCallbacks(true)
// showCallbacks(true)
/* Theory constructs */
val mkSetSort = mkTheorySort(z3.mkStringSymbol("SetSort"))
......@@ -62,7 +62,7 @@ class BAPATheory(val z3: Z3Context) extends Z3Theory(z3, "BAPATheory") with Venn
/* Callbacks */
def assertAxiom2(ast: Z3AST) {
println("Asserting: " + ast)
// println("Asserting: " + ast)
assertAxiom(ast)
}
......
......@@ -59,8 +59,8 @@ trait VennRegions {
if (setVariables contains name) {
this
} else {
println("Adding set: " + symbol)
println("AKA : " + name)
// println("Adding set: " + symbol)
// println("AKA : " + name)
new ExtendedUniverse(name, this)
}
}
......
......@@ -45,4 +45,21 @@ object JustFormulas {
)
x != y
} ensuring(!_)
def vc7_I(a: Set[Int], b: Set[Int]) : Boolean = {
require(
a == Set(1, 2, 3)
&& (b subsetOf a)
)
a.contains(b.size)
} ensuring(_ == true)
def vc8_V(a: Set[Int], b: Set[Int]) : Boolean = {
require(
a == Set(1, 2, 3)
&& (b subsetOf a)
&& b != Set.empty[Int]
)
a.contains(b.size)
} ensuring(_ == true)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment