Commit fdbb138e authored by Christian Müller's avatar Christian Müller

generate better ineqs

parent 3b0070b2
......@@ -160,7 +160,7 @@ object FormulaFunctions extends LazyLogging {
val eqs = for (x <- vars; y <- otherthan) yield {
Neg(Eq(x,y))
}
Forall(vars, Implies(And.make(eqs), fp))
Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
}
})
}
......
......@@ -18,9 +18,9 @@ class FOLTLTest extends FlatSpec {
)
val f2 = ForallOtherThan(List("x","y"), "z", Globally("x"))
val res2 = f.removeOTQuantifiers()
val res2 = f2.removeOTQuantifiers()
res2 should be(
Forall(List("x","y"), Implies(And(Neg(Eq("x", "y")), Neg(Eq("y", "z"))), Globally("x")))
Forall(List("x","y"), Implies(And(Neg(Eq("x", "z")), Neg(Eq("y", "z"))), Globally("x")))
)
}
}
\ No newline at end of file
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