Commit 9d997d99 authored by Christian Müller's avatar Christian Müller

fix bindings

parent 57f880ed
...@@ -94,12 +94,15 @@ object Preconditions extends LazyLogging { ...@@ -94,12 +94,15 @@ object Preconditions extends LazyLogging {
} }
def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleBlock): Formula = { def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleBlock): Formula = {
// TODO: should this contain f.freeVars?
val boundvars = f.boundVars
updates.foldRight(f)((update, f) => { updates.foldRight(f)((update, f) => {
val (repname, (vars, form)) = update val (repname, (vars, form)) = update
val fixupdate = FormulaFunctions.fixBinding(form, boundvars -- vars)
f everywhere { f everywhere {
case Fun(name, ind, params) if name == repname => { case Fun(name, ind, params) if name == repname => {
val renamed = form.parallelRename(vars, params) val renamed = fixupdate.parallelRename(vars, params)
// Annotate the precondition with the index // Annotate the precondition with the index
if (ind.isDefined) { if (ind.isDefined) {
...@@ -162,7 +165,7 @@ object Preconditions extends LazyLogging { ...@@ -162,7 +165,7 @@ object Preconditions extends LazyLogging {
val neg1 = replaced.toNegNf val neg1 = replaced.toNegNf
val neg2 = removed.toNegNf val neg2 = removed.toNegNf
if (FormulaFunctions.collectQuantifiers(neg1) != FormulaFunctions.collectQuantifiers(neg2)) { if (FormulaFunctions.collectQuantifiers(neg1) != FormulaFunctions.collectQuantifiers(neg2)) {
logger.warn(s"Would have removed a quantifier:\nBefore: ${neg1}\nAfter: $neg2") logger.error(s"Would have removed a quantifier:\nBefore: ${neg1}\nAfter: $neg2")
} }
} }
......
...@@ -60,7 +60,7 @@ object FOTransformers extends LazyLogging { ...@@ -60,7 +60,7 @@ object FOTransformers extends LazyLogging {
val cnf = f.toCNF val cnf = f.toCNF
// TODO: add equalities? // TODO: saturate before doing this?
val repld = cnf everywhere { val repld = cnf everywhere {
case Neg(Fun(AUX, _, _)) => False case Neg(Fun(AUX, _, _)) => False
case Fun(AUX, _, _) => False case Fun(AUX, _, _) => False
......
...@@ -484,8 +484,15 @@ object FormulaFunctions extends LazyLogging { ...@@ -484,8 +484,15 @@ object FormulaFunctions extends LazyLogging {
fixGeneralBindings(f)._1 fixGeneralBindings(f)._1
} }
} }
def fixBinding(f: Formula, bound:Set[Var]) = {
if (f.isUniversal) {
fixUniversalBindings(f, bound)._1
} else {
fixGeneralBindings(f, bound)._1
}
}
def fixGeneralBindings(f:Formula):(Formula, Set[Var]) = { private def fixGeneralBindings(f:Formula, bound:Set[Var] = Set()):(Formula, Set[Var]) = {
def fix(f: Formula, bound: Set[Var]): (Formula, Set[Var]) = f match { def fix(f: Formula, bound: Set[Var]): (Formula, Set[Var]) = f match {
case UnOp(make, f1) => { case UnOp(make, f1) => {
val (newf, newbounds) = fix(f1, bound) val (newf, newbounds) = fix(f1, bound)
...@@ -510,11 +517,11 @@ object FormulaFunctions extends LazyLogging { ...@@ -510,11 +517,11 @@ object FormulaFunctions extends LazyLogging {
case f => (f, bound) case f => (f, bound)
} }
logger.warn("Using fallback fixbindings method for general formulas.") logger.warn("Using fallback fixbindings method for general formulas.")
fix(f, f.freeVars) fix(f, bound ++ f.freeVars)
} }
def fixUniversalBindings(f: Formula): (Formula, Set[Var]) = { private def fixUniversalBindings(f: Formula, bound:Set[Var] = Set()): (Formula, Set[Var]) = {
def fix(f:Formula, bound: Set[Var]):(Formula, Set[Var]) = { def fix(f:Formula, bound: Set[Var]):(Formula, Set[Var]) = {
f match { f match {
case UnOp(make, f1) => { case UnOp(make, f1) => {
...@@ -549,7 +556,7 @@ object FormulaFunctions extends LazyLogging { ...@@ -549,7 +556,7 @@ object FormulaFunctions extends LazyLogging {
if (!f.isUniversal) { if (!f.isUniversal) {
logger.error("Trying to fix universal bindings of non-universal formula") logger.error("Trying to fix universal bindings of non-universal formula")
} }
fix(f, f.freeVars) fix(f, bound ++ f.freeVars)
} }
// TODO: make sure no quantifiers in scope of others with same name // TODO: make sure no quantifiers in scope of others with same name
......
...@@ -65,7 +65,7 @@ object Z3FOEncoding extends LazyLogging { ...@@ -65,7 +65,7 @@ object Z3FOEncoding extends LazyLogging {
} }
case Equiv(f1, f2) => { case Equiv(f1, f2) => {
logger.warn("Sending equiv <-> to Z3") // logger.warn("Sending equiv <-> to Z3")
val e1 = toBoolZ3(ctx, f1, var_ctx) val e1 = toBoolZ3(ctx, f1, var_ctx)
val e2 = toBoolZ3(ctx, f2, var_ctx) val e2 = toBoolZ3(ctx, f2, var_ctx)
ctx.mkEq(e1, e2) ctx.mkEq(e1, e2)
......
...@@ -60,7 +60,7 @@ class InferenceTests extends FlatSpec { ...@@ -60,7 +60,7 @@ class InferenceTests extends FlatSpec {
assert(checkSafeStubborn(name, "", inv)) assert(checkSafeStubborn(name, "", inv))
} }
ignore should "prove safe loopy causal stuff safe" in { it should "prove safe loopy causal stuff safe" in {
val name = "tests/conference_stubborn_withB" val name = "tests/conference_stubborn_withB"
val xat = Var("xat","A") val xat = Var("xat","A")
val xbt = Var("xbt","A") val xbt = Var("xbt","A")
......
...@@ -93,7 +93,7 @@ class LeaderElectionTest extends FlatSpec { ...@@ -93,7 +93,7 @@ class LeaderElectionTest extends FlatSpec {
assert(check(name, inv, knowledge, properties)) assert(check(name, inv, knowledge, properties))
} }
"Deterministic Leader election" should "be inferred safe" in { "Deterministic Leader election" should "be inferred safe" ignore {
val name = "tests/leaderelection" val name = "tests/leaderelection"
println(le_total_order_axioms) println(le_total_order_axioms)
...@@ -112,7 +112,7 @@ class LeaderElectionTest extends FlatSpec { ...@@ -112,7 +112,7 @@ class LeaderElectionTest extends FlatSpec {
} }
it should "be inferred safe with Bs" in { it should "be inferred safe with Bs" ignore {
val name = "tests/leaderelection_withB" val name = "tests/leaderelection_withB"
val knowledge = And.make( val knowledge = And.make(
...@@ -126,7 +126,7 @@ class LeaderElectionTest extends FlatSpec { ...@@ -126,7 +126,7 @@ class LeaderElectionTest extends FlatSpec {
assert(check(name, inv, knowledge, properties)) assert(check(name, inv, knowledge, properties))
} }
"Unsafe Deterministic Leader election" should "be proven unsafe" in { "Unsafe Deterministic Leader election" should "be proven unsafe" ignore {
val name = "tests/leaderelection_unsafe" val name = "tests/leaderelection_unsafe"
val total_order = And.make(le_total_order_axioms) val total_order = And.make(le_total_order_axioms)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment