Commit 371fdd4b authored by Christian Müller's avatar Christian Müller

inference fix

parent 9987dadf
......@@ -20,11 +20,11 @@ object MainInvariantsInference extends App with LazyLogging {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
// InvariantGenerator.invariantNoninterSingleBS _
InvariantGenerator.invariantNoninterSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
(_:Spec) => Forall(List("x","p"), Fun("Assign", List("x", "p")) --> Neg(Fun("Conf", List("x", "p")))).in(Properties.T1)
// (_:Spec) => Forall(List("x","p"), Fun("Assign", List("x", "p")) --> Neg(Fun("Conf", List("x", "p")))).in(Properties.T1)
// TODO: Add single trace properties
......
......@@ -246,22 +246,25 @@ object FOLTL {
Some((binop.make, binop.t1, binop.t2))
}
def makeL(make: (Formula, Formula) => Formula, l: Seq[Formula], Empty: Formula): Formula = {
l.toList match {
case List(x) => x
case Empty :: xs => makeL(make, xs, Empty)
case x :: xs => make(x, makeL(make, xs, Empty))
case List() => Empty
}
// TODO: make list lefthanging?
@tailrec
def makeL(make: (Formula, Formula) => Formula, l: Seq[Formula], Empty: Formula, acc:Formula): Formula = {
l.toList match {
case Empty :: xs => makeL(make, xs, Empty, acc)
case x :: xs => if (acc == Empty)
makeL(make, xs, Empty, x) else
makeL(make, xs, Empty, make(acc, x))
case List() => acc
}
}
}
object Or {
def make(terms: List[Formula]) = {
BinOp.makeL(Or.apply, terms, False)
BinOp.makeL(Or.apply, terms, False, False)
}
def make(terms: Formula*) = {
BinOp.makeL(Or.apply, terms, False)
BinOp.makeL(Or.apply, terms, False, False)
}
}
......@@ -272,10 +275,10 @@ object FOLTL {
object And {
def make(terms: List[Formula]) = {
BinOp.makeL(And.apply, terms, True)
BinOp.makeL(And.apply, terms, True, True)
}
def make(terms: Formula*) = {
BinOp.makeL(And.apply, terms, True)
BinOp.makeL(And.apply, terms, True, True)
}
}
......@@ -290,10 +293,10 @@ object FOLTL {
}
object Eq {
def make(terms: List[Formula]) = {
BinOp.makeL(Eq.apply, terms, True)
BinOp.makeL(Eq.apply, terms, True, True)
}
def make(terms: Formula*) = {
BinOp.makeL(Eq.apply, terms, True)
BinOp.makeL(Eq.apply, terms, True, True)
}
}
......@@ -303,10 +306,10 @@ object FOLTL {
}
object Implies {
def make(terms: List[Formula]) = {
BinOp.makeL(Implies.apply, terms, True)
BinOp.makeL(Implies.apply, terms, True, True)
}
def make(terms: Formula*) = {
BinOp.makeL(Implies.apply, terms, True)
BinOp.makeL(Implies.apply, terms, True, True)
}
}
case class Neg(t: Formula) extends UnOp {
......
......@@ -82,15 +82,10 @@ object FOTransformers extends LazyLogging {
// Group clauses by positive/negative occurences
def ispositive(clause: List[Formula]) =
clause.exists {
case Fun(B, _, _) => true
case _ => false
}
getPositiveBArguments(clause).nonEmpty
def isnegative(clause: List[Formula]) =
clause.exists {
case Neg(Fun(B, _, _)) => true
case _ => false
}
getNegativeBArguments(clause).nonEmpty
def pruneBs(clause: List[Formula]) = {
clause.filterNot {
......@@ -99,12 +94,43 @@ object FOTransformers extends LazyLogging {
case _ => false
}
}
def getPositiveBArguments(clause: List[Formula]):List[List[Var]] = {
clause flatMap {
case Fun(B, _, vars) => List(vars)
case _ => List()
}
}
def getNegativeBArguments(clause: List[Formula]):List[List[Var]] = {
clause flatMap {
case Neg(Fun(B, _, vars))=> List(vars)
case _ => List()
}
}
def ineq(l1:List[Var], l2:List[Var]) = {
if (l1.size != l2.size) {
logger.warn("Trying to generate inequalities for different sized vectors")
}
Or.make(l1.zip(l2).map {
case (x, y) => Neg(Eq(x,y))
})
}
val E = clauses.filter(c => !ispositive(c) && !isnegative(c))
val F = clauses.filter(c => ispositive(c) && !isnegative(c))
// F \/ B z_1 ... B z_r
val Fargs = F.flatMap(getPositiveBArguments)
val G = clauses.filter(c => isnegative(c) && !ispositive(c))
// G \/ !B z'_1 ... !B z'_j
val Gargs = G.flatMap(getNegativeBArguments)
val H = clauses.filter(c => ispositive(c) && isnegative(c))
// H \/ B u_1 .. B u_l \/ !B v_1 ... ! B v_n
val HPositiveargs = H.flatMap(getPositiveBArguments)
val HNegativeargs = H.flatMap(getNegativeBArguments)
if (H.nonEmpty) {
logger.warn("BSFO SOQE: H is not empty, Ackermann not applicable")
}
......@@ -112,12 +138,20 @@ object FOTransformers extends LazyLogging {
val fE = And.make(E.map(c => Or.make(pruneBs(c))))
val fF = And.make(F.map(c => Or.make(pruneBs(c))))
val fG = And.make(G.map(c => Or.make(pruneBs(c))))
val fH = And.make(G.map(c => Or.make(pruneBs(c))))
val fFGineq = And.make(for (farg <- Fargs; garg <- Gargs) yield {
ineq(farg, garg)
})
val fGHineq = And.make(for (harg <- HPositiveargs; garg <- Gargs) yield {
ineq(harg, garg)
})
val felim:Formula = fE land (fF lor fG)
val felim:Formula = fE land (fF lor fG lor fFGineq) land (fH lor fGHineq lor fG)
// TODO: Add ineq with ys
val fsol:Formula = fG
// wrap quantifiers around
// FIXME: add equalities
val felimq = FormulaFunctions.rewrapQuantifiers(quantifiers, felim)
val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
val z3fsolq = Z3BSFO.simplifyBS(fsolq)
......
......@@ -33,6 +33,10 @@ class FOLTLTest extends FlatSpec {
And(t, t).simplify should be (t)
}
it should "make lists" in {
And.make("c", "d", "e", "d" lor "e").simplify() should be ("c" land ("d" land ("e" land ("d" lor "e"))).simplify())
}
it should "simplify double negation" in {
Neg(Neg(True)).simplify() should be(True)
......
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