Commit 5dac4c08 authored by Christian Müller's avatar Christian Müller

constants

parent 60a69f09
......@@ -35,8 +35,9 @@ object FOTransformers extends LazyLogging {
}
def collectMultiClause(f:Formula):List[List[Formula]] = f collect {
case t:Or => List(collectClause(t))
case And(t1, t2) => collectMultiClause(t1) ++ collectMultiClause(t2)
case Quantifier(vars, make, t) => collectMultiClause(t)
case t => List(collectClause(t))
}
collectMultiClause(f)
......@@ -173,7 +174,9 @@ object FOTransformers extends LazyLogging {
val nf = f.toNegNf()
val (agents, inner) = FOTransformers.eliminateExistentials(nf)
val existbound = Exists(agents, inner)
FOTransformers.eliminateUniversals(existbound, agents)
val constants = existbound.freeVars()
FOTransformers.eliminateUniversals(existbound, constants.toList)
}
/**
......@@ -191,7 +194,8 @@ object FOTransformers extends LazyLogging {
val (agents, inner) = FOTransformers.eliminateExistentials(neg)
val existbound = Exists(agents, inner)
val res = FOTransformers.eliminateUniversals(existbound, List())
val constants = neg.freeVars()
val res = FOTransformers.eliminateUniversals(existbound, constants.toList)
Neg(res).simplify()
}
}
\ No newline at end of file
......@@ -81,6 +81,14 @@ class FOTransformSpec extends FlatSpec {
)
}
it should "work with constants" in {
val f = Forall(List("x"), Or(Var("c"), Exists("z", Fun("f", List("x","z")))))
FOTransformers.abstractExistentials(f) should be (
Forall(List("x"), Or(Var("c"), Or(Fun("f", List("x","c")), Fun("f", List("x","x")))))
)
}
"hasSubFormula" should "find subformulas" in {
val f = Forall(List("x","y"), Exists("z", Fun("f", List("x","z"))))
val f2 = And("b", Or("c", f))
......
......@@ -30,11 +30,11 @@ class InvariantCausalFilesTest extends FlatSpec {
// assert(!checkSafeCausal(name, inv))
// }
//
// it should "fail to prove conference_linear alleq" in {
// val name = "nonomitting/conference_linear"
// val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
// assert(!checkSafeCausal(name, "alleq", inv))
// }
it should "fail to prove conference_linear alleq" in {
val name = "nonomitting/conference_linear"
val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
assert(!checkSafeCausal(name, "alleq", inv))
}
//
// // HEAP SPACE
// it should "fail to prove conference_linear with elim" ignore {
......@@ -92,13 +92,13 @@ class InvariantCausalFilesTest extends FlatSpec {
// assert(!checkSafeCausal(name, "alleq", inv))
// }
// it should "prove omitting/conference_fixed" in {
// val name = "omitting/conference_fixed"
// val xt = Var("xt","A")
// val pt = Var("rt","R")
// val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt)))
// assert(checkSafeCausal(name, inv))
// }
it should "prove omitting/conference_fixed" in {
val name = "omitting/conference_fixed"
val xt = Var("xt","A")
val pt = Var("rt","R")
val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt)))
assert(checkSafeCausal(name, inv))
}
//
// it should "prove omitting/conference_fixed alleq" ignore {
// val name = "omitting/conference_fixed"
......
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