Commit 86de4de4 authored by Christian Müller's avatar Christian Müller
Browse files

generate Inequalities

parent 4466e442
...@@ -15,6 +15,8 @@ object FOLTL { ...@@ -15,6 +15,8 @@ object FOLTL {
def in(name: String, ignore: Set[String]) = FormulaFunctions.annotate(this, name, ignore) def in(name: String, ignore: Set[String]) = FormulaFunctions.annotate(this, name, ignore)
def collect[T](coll: PartialFunction[Formula, List[T]]) = FormulaFunctions.collect(coll, this) def collect[T](coll: PartialFunction[Formula, List[T]]) = FormulaFunctions.collect(coll, this)
def opsize() = FormulaFunctions.opsize(this) def opsize() = FormulaFunctions.opsize(this)
def removeOTQuantifiers() = FormulaFunctions.removeOTQuantifiers(this)
def bracketed(): String = this match { def bracketed(): String = this match {
case _: BinOp => "(" + this + ")" case _: BinOp => "(" + this + ")"
......
...@@ -153,4 +153,15 @@ object FormulaFunctions extends LazyLogging { ...@@ -153,4 +153,15 @@ object FormulaFunctions extends LazyLogging {
frees.isEmpty frees.isEmpty
} }
def removeOTQuantifiers(f: Formula) = {
f.everywhere({
case ForallOtherThan(vars, otherthan, fp) => {
val eqs = for (x <- vars; y <- otherthan) yield {
Neg(Eq(x,y))
}
Forall(vars, And(And.make(eqs), fp))
}
})
}
} }
\ 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