FormulaFunctions.scala 23.5 KB
Newer Older
1
package de.tum.niwo.foltl
Christian Müller's avatar
Christian Müller committed
2 3

import FOLTL._
Christian Müller's avatar
Christian Müller committed
4
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
5
import de.tum.niwo.foltl.FOTransformers.logger
Christian Müller's avatar
src  
Christian Müller committed
6

Christian Müller's avatar
Christian Müller committed
7
import scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
8

9
object FormulaFunctions extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
10

11 12 13
  def freeVars(f: Formula): Set[Var] = {
    def free(g: Formula, bound: Set[Var]): Set[Var] = {
      g match {
Christian Müller's avatar
Christian Müller committed
14 15
        // Extractors
        // Exists, Forall
Christian Müller's avatar
Christian Müller committed
16
        case Quantifier(_, ps, t) => free(t, bound ++ ps)
17
        case UnOp(_, t)        => free(t, bound)
Christian Müller's avatar
Christian Müller committed
18
        // And, Or, Eq, Implies
Christian Müller's avatar
Christian Müller committed
19
        case BinOp(_, t1, t2)     => free(t1, bound) ++ free(t2, bound)
Christian Müller's avatar
Christian Müller committed
20

Christian Müller's avatar
Christian Müller committed
21 22
        //      TODO: path is not a free variable anymore
        //        case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
23
        case Fun(_, _, ps)        => ps.toSet -- bound
Christian Müller's avatar
Christian Müller committed
24
        case v: Var if !bound(v)  => Set(v)
25
        case _ => Set()
Christian Müller's avatar
Christian Müller committed
26 27
      }
    }
28
    free(f, Set())
Christian Müller's avatar
Christian Müller committed
29 30
  }

Christian Müller's avatar
ineq  
Christian Müller committed
31 32 33 34 35 36 37 38 39 40 41
  // @tailrec version?
  def boundVars(f:Formula): Set[Var] = {
    def boundInner(f: Formula): List[Var] = {
      f collect {
        case Quantifier(_, xs, sub) => xs ++ boundInner(sub)
      }
    }
    boundInner(f).toSet
  }


42
  def simplify(f: Formula): Formula = {
43
    val simp: PartialFunction[Formula, Formula] = {
Christian Müller's avatar
Christian Müller committed
44
      // Push negation inward
Christian Müller's avatar
Christian Müller committed
45 46 47 48 49 50 51 52
      case Neg(Or(t1, t2)) => And(Neg(t1), Neg(t2))
      case Neg(And(t1, t2)) => Or(Neg(t1), Neg(t2))
      case Neg(Globally(t)) => Finally(Neg(t))
      case Neg(Finally(t)) => Globally(Neg(t))
      case Neg(Next(t)) => Next(Neg(t))
      case Neg(Forall(vars, t)) => Exists(vars, Neg(t))
      case Neg(Exists(vars, t)) => Forall(vars, Neg(t))
      case Neg(Implies(t1, t2)) => And(t1, Neg(t2))
Christian Müller's avatar
Christian Müller committed
53 54

      // Simple laws
Christian Müller's avatar
Christian Müller committed
55 56 57
      case Neg(True) => False
      case Neg(False) => True
      case Neg(Neg(t)) => t
58 59
      case Or(True, _) => True
      case Or(_, True) => True
Christian Müller's avatar
Christian Müller committed
60 61
      case Or(False, t) => t
      case Or(t, False) => t
62 63
      case And(False, _) => False
      case And(_, False) => False
Christian Müller's avatar
Christian Müller committed
64 65
      case And(True, t) => t
      case And(t, True) => t
66
      case Implies(False, _) => True
Christian Müller's avatar
Christian Müller committed
67 68 69 70 71
      case Implies(True, t) => t
      case Or(Neg(t1), t2) if t1 == t2 => True
      case And(Neg(t1), t2) if t1 == t2 => False
      case Or(t1, Neg(t2)) if t1 == t2 => True
      case And(t1, Neg(t2)) if t1 == t2 => False
Christian Müller's avatar
Christian Müller committed
72 73

      // left-trees
Christian Müller's avatar
Christian Müller committed
74 75 76
      case And(And(t1, t2), t3) => And(t1, And(t2, t3))
      case Or(Or(t1, t2), t3) => Or(t1, Or(t2, t3))

Christian Müller's avatar
Christian Müller committed
77
      // equal things in tree
Christian Müller's avatar
Christian Müller committed
78 79
      case And(t1, t2) if t1 == t2 => t1
      case Or(t1, t2) if t1 == t2 => t1
80 81 82 83
      case And(t1, And(t2, t3)) if t1 == t2 => And(t1, t3)
      case And(t1, And(t2, t3)) if t1 == t3 => And(t1, t2)
      case Or(t1, Or(t2, t3)) if t1 == t2 => Or(t1, t3)
      case Or(t1, Or(t2, t3)) if t1 == t3 => Or(t1, t2)
Christian Müller's avatar
Christian Müller committed
84

85
      // And Or
86 87 88 89
      case And(t1, Or(_, t3)) if t1 == t3 => t1
      case And(t1, Or(t2, _)) if t1 == t2 => t1
      case And(Or(_, t3), t1) if t1 == t3 => t1
      case And(Or(t2, _), t1) if t1 == t2 => t1
90

Christian Müller's avatar
Christian Müller committed
91
      //      case Or(t1, Neg(t2)) if t1 == t2        => True
Christian Müller's avatar
Christian Müller committed
92

93
      // Equivalence
Christian Müller's avatar
Christian Müller committed
94 95
      case Equiv(t1, t2) if t1 == t2 => True
      case Equiv(v1:Var, v2:Var) if v1.name > v2.name => Equiv(v2, v1)
Christian Müller's avatar
Christian Müller committed
96

97
      // Double Temporals
Christian Müller's avatar
Christian Müller committed
98 99
      case Finally(Finally(t)) => Finally(t)
      case Globally(Globally(t)) => Globally(t)
Christian Müller's avatar
Christian Müller committed
100 101

      // Remove quantifiers if empty
102
      case Quantifier(_, xs, t) if xs.isEmpty => t
Christian Müller's avatar
Christian Müller committed
103 104 105
      case Quantifier(_, _, True) => True
      case Quantifier(_, _, False) => False

Christian Müller's avatar
Christian Müller committed
106
      // Quantifiers binding same things
107 108 109 110
      case And(Forall(vars1, t1), Forall(vars2, t2)) if vars1 == vars2 => Forall(vars1, And(t1, t2))
      case Or(Forall(vars1, t1), Forall(vars2, t2)) if vars1 == vars2 => Forall(vars1, Or(t1, t2))
      case And(Exists(vars1, t1), Exists(vars2, t2)) if vars1 == vars2 => Exists(vars1, And(t1, t2))
      case Or(Exists(vars1, t1), Exists(vars2, t2)) if vars1 == vars2 => Exists(vars1, Or(t1, t2))
111

112
      // Gobble up equal quantifiers
113 114
      case Forall(vars1, Forall(vars2, t)) => Forall(vars1 ++ vars2, t)
      case Exists(vars1, Exists(vars2, t)) => Exists(vars1 ++ vars2, t)
115

Christian Müller's avatar
Christian Müller committed
116
      // Remove variables from quantifiers if not used in the body
Christian Müller's avatar
src  
Christian Müller committed
117 118
      case Quantifier(qmake, xs, t) if (xs.toSet -- t.freeVars).nonEmpty =>
        qmake(xs.toSet.intersect(t.freeVars).toList, t)
Christian Müller's avatar
Christian Müller committed
119 120 121 122 123 124
      //
      //      // Split off binops from quantifiers
      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t1.freeVars().intersect(xs.toSet)).isEmpty =>
      //        make(t1, qmake(xs, t2))
      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t2.freeVars().intersect(xs.toSet)).isEmpty =>
      //        make(qmake(xs, t1), t2)
Christian Müller's avatar
Christian Müller committed
125 126

      // Declass seen often enough
127
      case And(Or(f1, f2), Or(f3, f4)) if f2 == f4 && f1 == Neg(f3).simplify => f2
Christian Müller's avatar
Christian Müller committed
128 129
    }

Christian Müller's avatar
Christian Müller committed
130 131
    //    val (changed, t1) = everywhereFP(simp, t)
    //    if (!changed) t1 else simplify(t1)
132
    everywhereBotUp(simp, f)
Christian Müller's avatar
Christian Müller committed
133
  }
134

Christian Müller's avatar
src  
Christian Müller committed
135 136 137 138 139 140 141 142 143 144
  def pushUniversalQuantifiers(f: Formula): Formula = {
    def push(f:Formula):Formula = {

      f everywhere {
        case Forall(vars, BinOp(make, f1, f2)) if {
          val leftvars = f1.freeVars
          val rightvars = f2.freeVars
          val varset = vars.toSet
          val onlyleft = leftvars.intersect(varset) -- rightvars
          val onlyright = rightvars.intersect(varset) -- leftvars
145 146
          onlyleft.nonEmpty || onlyright.nonEmpty
        } =>
Christian Müller's avatar
src  
Christian Müller committed
147 148 149 150 151 152 153 154 155 156 157
          val leftvars = f1.freeVars
          val rightvars = f2.freeVars
          val varset = vars.toSet
          val bothvars = leftvars.intersect(rightvars).intersect(varset)
          val onlyleft = leftvars.intersect(varset) -- rightvars
          val onlyright = rightvars.intersect(varset) -- leftvars
          Forall.make(
            bothvars.toList,
            make(
              push(Forall.make(onlyleft.toList, f1)),
              push(Forall.make(onlyright.toList, f2))))
Christian Müller's avatar
Christian Müller committed
158 159
      }
    }
Christian Müller's avatar
src  
Christian Müller committed
160 161 162 163

    if (!f.isUniversal) {
      logger.error("Trying to push universal quantifiers inside non-universal formula")
    }
Christian Müller's avatar
Christian Müller committed
164
    push(f).simplify
Christian Müller's avatar
Christian Müller committed
165 166
  }

Christian Müller's avatar
Christian Müller committed
167
  def eliminateImplication(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
168
    f everywhere {
Christian Müller's avatar
Christian Müller committed
169 170 171
      case Implies(f1, f2) => Or(Neg(eliminateImplication(f1)), eliminateImplication(f2))
    }
  }
Christian Müller's avatar
Christian Müller committed
172 173

  def eliminateEq(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
174
    f everywhere {
Christian Müller's avatar
Christian Müller committed
175 176
      // TODO: switch eq between funs to lra
      case Equiv(v1:Var, v2:Var) => Equiv(v1,v2)
177
      case Equiv(f1, f2) =>
Christian Müller's avatar
Christian Müller committed
178 179 180
        val e1 = eliminateEq(f1)
        val e2 = eliminateEq(f2)
        And(Implies(e1, e2), Implies(e2, e1))
Christian Müller's avatar
Christian Müller committed
181 182
    }
  }
Christian Müller's avatar
Christian Müller committed
183

Christian Müller's avatar
Christian Müller committed
184 185 186 187 188 189
  def everywhereFP(trans: PartialFunction[Formula, Formula], t: Formula): (Boolean, Formula) = {
    if (trans.isDefinedAt(t))
      (true, trans(t))
    else
      t match {
        // Extractors
190
        case Quantifier(make, ps, t1) =>
Christian Müller's avatar
Christian Müller committed
191 192
          val sub = everywhereFP(trans, t1)
          (sub._1, make(ps, sub._2))
193
        case UnOp(make, t1) =>
Christian Müller's avatar
Christian Müller committed
194 195
          val sub = everywhereFP(trans, t1)
          (sub._1, make(sub._2))
196
        case BinOp(make, t1, t2) =>
Christian Müller's avatar
Christian Müller committed
197 198 199
          val (c1, sub1) = everywhereFP(trans, t1)
          val (c2, sub2) = everywhereFP(trans, t2)
          (c1 || c2, make(sub1, sub2))
Christian Müller's avatar
Christian Müller committed
200
        case x => (false, x)
Christian Müller's avatar
Christian Müller committed
201 202
      }
  }
Christian Müller's avatar
Christian Müller committed
203

204 205 206
  def everywhere(trans: PartialFunction[Formula, Formula], f: Formula): Formula = {
    if (trans.isDefinedAt(f))
      trans(f)
Christian Müller's avatar
Christian Müller committed
207
    else
208
      f match {
Christian Müller's avatar
Christian Müller committed
209 210
        // Extractors
        case Quantifier(make, ps, t) => make(ps, everywhere(trans, t))
Christian Müller's avatar
Christian Müller committed
211
        case UnOp(make, t1)          => make(everywhere(trans, t1))
Christian Müller's avatar
Christian Müller committed
212 213 214 215
        case BinOp(make, t1, t2)     => make(everywhere(trans, t1), everywhere(trans, t2))
        case x                       => x
      }
  }
Christian Müller's avatar
Christian Müller committed
216

217
  def everywhereBotUp(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
218
    // First apply trans to push negation inward etc
219 220 221 222 223
    if (trans.isDefinedAt(t))
      everywhereBotUp(trans, trans(t))
    else {
      val sub = t match {
        // Extractors
224
        case Quantifier(make, ps, f) => make(ps, everywhereBotUp(trans, f))
225 226 227 228
        case UnOp(make, t1)          => make(everywhereBotUp(trans, t1))
        case BinOp(make, t1, t2)     => make(everywhereBotUp(trans, t1), everywhereBotUp(trans, t2))
        case x                       => x
      }
229 230 231 232 233
      // Applicable after inner transformation?
      if (trans.isDefinedAt(sub))
        trans(sub)
      else
        sub
234 235
    }
  }
236

237
  def opsize(t: Formula): Int = {
238 239
    t match {
      // Extractors
240 241
      case Quantifier(_, _, f) => 1 + f.opsize
      case UnOp(_, f)           => 1 + f.opsize
Christian Müller's avatar
Christian Müller committed
242
      case BinOp(_, t1, t2)     => 1 + t1.opsize + t2.opsize
243
      case _ => 1
244 245
    }
  }
Christian Müller's avatar
Christian Müller committed
246

247
  def collect[T](combine: (T*) => T)(coll: PartialFunction[Formula, T], t: Formula): T = {
Christian Müller's avatar
Christian Müller committed
248 249 250 251 252
    if (coll.isDefinedAt(t))
      coll(t)
    else
      t match {
        // Extractors
253 254 255 256
        case Quantifier(_, _, f) => combine(collect(combine)(coll, f))
        case UnOp(_, f)           => combine(collect(combine)(coll, f))
        case BinOp(_, t1, t2)     => combine(collect(combine)(coll, t1), collect(combine)(coll, t2))
        case _ => combine()
257 258
      }
  }
259

260
  def collect[T](coll: PartialFunction[Formula, List[T]], t: Formula): List[T] = {
261 262 263 264 265
    if (coll.isDefinedAt(t))
      coll(t)
    else
      t match {
        // Extractors
266 267 268 269
        case Quantifier(_, _, f) => collect(coll, f)
        case UnOp(_, f)           => collect(coll, f)
        case BinOp(_, t1, t2)     => List.concat(collect(coll, t1), collect(coll, t2))
        case _ => List.empty
Christian Müller's avatar
Christian Müller committed
270 271
      }
  }
Christian Müller's avatar
Christian Müller committed
272

Christian Müller's avatar
Christian Müller committed
273
  def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula): Boolean = {
Christian Müller's avatar
Christian Müller committed
274
    def or(bs: Boolean*) = { bs.exists(identity) }
275 276
    collect(or)(coll, t)
  }
Christian Müller's avatar
Christian Müller committed
277 278 279 280 281 282 283 284 285 286 287 288 289 290

  //  def hasSubFormula(check: (Formula => Boolean), t: Formula): Boolean = {
  //    if (check(t)) {
  //      true
  //    } else {
  //      t match {
  //        // Extractors
  //        case Quantifier(make, ps, t) => hasSubFormula(check, t)
  //        case UnOp(make, t)           => hasSubFormula(check, t)
  //        case BinOp(make, t1, t2)     => hasSubFormula(check, t1) || hasSubFormula(check, t2)
  //        case x                       => false
  //      }
  //    }
  //  }
291

292
  def assumeEmpty(t: Formula, name: String): Formula = {
Christian Müller's avatar
Christian Müller committed
293 294 295 296
    t.everywhere({
      case Fun(f, _, _) if f == name => False
    })
  }
297

298
  def assumeAllEmpty(f: Formula, names: List[String]): Formula = {
299
    // Assume all workflow relations empty
300
    val assumers = names.map(p => (f: Formula) => assumeEmpty(f, p))
Christian Müller's avatar
Christian Müller committed
301
    val allempty = assumers.foldLeft(f)((f, a) => a(f))
Christian Müller's avatar
Christian Müller committed
302
    allempty.simplify
303
  }
Christian Müller's avatar
Christian Müller committed
304

305
  def annotate(t: Formula, name: String): Formula = {
Christian Müller's avatar
Christian Müller committed
306 307 308 309
    t.everywhere({
      case Fun(f, None, xs) => Fun(f, Some(name), xs)
    })
  }
Christian Müller's avatar
Christian Müller committed
310

311
  def removeAnnotation(t:Formula, Funname:String): Formula = {
Christian Müller's avatar
Christian Müller committed
312 313 314 315 316
    t.everywhere({
      case Fun(Funname, _, xs) => Fun(Funname, None, xs)
    })
  }

317
  def annotateOverwrite(t: Formula, Name1: String, name: String): Formula = {
Christian Müller's avatar
Christian Müller committed
318 319 320 321
    t.everywhere({
      case Fun(f, Some(Name1), xs) => Fun(f, Some(name), xs)
    })
  }
322

323
  def annotate(t: Formula, name: String, ignore: Set[String]): Formula = {
324
    t.everywhere({
325
      case Fun(f, None, xs) if !(ignore contains f) => Fun(f, Some(name), xs)
326 327
    })
  }
328

329
  def checkSanity(t: Formula): Boolean = {
Christian Müller's avatar
Christian Müller committed
330 331
    // TODO add more things, f.e. existentials
    // T1, T2 can appear freely
Christian Müller's avatar
Christian Müller committed
332
    val frees = t.freeVars -- Set(Var(Properties.T1), Var(Properties.T2))
Christian Müller's avatar
Christian Müller committed
333
    if (frees.nonEmpty) {
Christian Müller's avatar
Christian Müller committed
334 335
      logger.warn(s"Sanity check failed: $frees appear free in the property.")
    }
336

Christian Müller's avatar
Christian Müller committed
337 338
    frees.isEmpty
  }
Christian Müller's avatar
Christian Müller committed
339 340

  def removeOTQuantifiers(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
341
    f.everywhere({
342
      case ForallOtherThan(vars, otherthan, fp) =>
Christian Müller's avatar
Christian Müller committed
343
        val eqs = for (x <- vars; y <- otherthan) yield {
Christian Müller's avatar
Christian Müller committed
344
          Neg(Equiv(x, y))
Christian Müller's avatar
Christian Müller committed
345
        }
Christian Müller's avatar
Christian Müller committed
346
        Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
Christian Müller's avatar
Christian Müller committed
347 348
    })
  }
Christian Müller's avatar
Christian Müller committed
349 350

  // f[newvars/vars]
Christian Müller's avatar
Christian Müller committed
351
  def parallelRename(f: Formula, vars: List[Var], newvars: List[Var]): Formula = {
352
    val repls = vars.zip(newvars).toMap
Christian Müller's avatar
Christian Müller committed
353

Christian Müller's avatar
Christian Müller committed
354 355
    parallelRename(f, repls)
  }
Christian Müller's avatar
Christian Müller committed
356 357 358

  def parallelRename(f: Formula, repls: Map[Var, Var]): Formula = {
    f everywhere {
Christian Müller's avatar
Christian Müller committed
359
      case v: Var if repls.contains(v) => repls(v)
360 361 362 363
      case Fun(fun, ind, params)         => Fun(fun, ind, params map (p => repls.getOrElse(p, p)))
      case Quantifier(make, xs, t) =>
        val rep = repls -- xs
        make(xs, parallelRename(t, rep))
Christian Müller's avatar
Christian Müller committed
364 365
    }
  }
Christian Müller's avatar
Christian Müller committed
366 367 368 369

  /**
   * Check if there exist quantifiers binding the same variable more than once
   */
370
  def hasDuplicateBindings(f: Formula): Boolean = {
Christian Müller's avatar
ineq  
Christian Müller committed
371
    boundVars(f).groupBy(n => n.name).exists(_._2.size > 1)
Christian Müller's avatar
Christian Müller committed
372 373
  }

374 375 376
  def stripQuantifiers(f: Formula): Formula = {
    f everywhere {
      case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
Christian Müller's avatar
Christian Müller committed
377
    }
378
  }
379

Christian Müller's avatar
Christian Müller committed
380
  def collectQuantifiers(f: Formula): List[(Boolean, List[Var])] = {
381 382
    def collectQ(inner:Formula):List[(Boolean, List[Var])] = {
      inner collect {
383 384
        case Exists(xs, fsub) => (true, xs) :: collectQ(fsub)
        case Forall(xs, fsub) => (false, xs) :: collectQ(fsub)
385
        case BinOp(_, f1, f2) =>
386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407
          val q1 = collectQ(f1)
          val q2 = collectQ(f2)

          // Merge while trying to stay in BS, if possible
          // TODO: could be improved to minimize quantifier alternations)
          // TODO: merge universals with same type by renaming
          val ex1 = q1.takeWhile(_._1)
          val rest1 = q1.drop(ex1.size)

          // filter out same bound variables on both sides
          // FIXME: make sure that fixBindings is used where neccessary
          val existbound = ex1.flatMap(_._2)
          val univbound = rest1.flatMap(_._2)

          val exset = existbound.toSet
          val univset = univbound.toSet

          val ex2 = q2.takeWhile(_._1).map(q =>
            (q._1, q._2.filterNot(exset.contains)))
          val rest2 = q2.drop(ex2.size).map(q =>
            (q._1, q._2.filterNot(univset.contains)))
          ex1 ++ ex2 ++ rest1 ++ rest2
Christian Müller's avatar
Christian Müller committed
408 409
      }
    }
410
    collectQ(f.toNegNf)
411
  }
Christian Müller's avatar
Christian Müller committed
412

413
  def checkBindings(f: Formula): Boolean = {
Christian Müller's avatar
Christian Müller committed
414 415
    def checkBindingsSub(f: Formula, bound: Set[Var]): List[Var] = {
      f collect {
416
        case Quantifier(_, xs, inner) =>
Christian Müller's avatar
Christian Müller committed
417 418 419
          val conflicts = xs.filter(bound.contains)
          conflicts ++ checkBindingsSub(inner, bound ++ xs)
      }
Christian Müller's avatar
Christian Müller committed
420 421
    }
    checkBindingsSub(f, Set()).isEmpty
422
  }
423

424
  def isBS(f: Formula): Boolean = {
Christian Müller's avatar
Christian Müller committed
425 426 427 428 429 430
    val quantprefix = collectQuantifiers(f.toNegNf)

    if (quantprefix.length < 2) true else {
      // has no forall exists in quantifier prefix
      !quantprefix.sliding(2).exists(list => !list.head._1 && list(1)._1)
    }
431
  }
432

Christian Müller's avatar
src  
Christian Müller committed
433 434
  def isU(formula:Formula): Boolean = {
    !formula.toNegNf.hasSubFormula {
435
      case _:Exists => true
Christian Müller's avatar
src  
Christian Müller committed
436 437 438
    }
  }

Christian Müller's avatar
Christian Müller committed
439 440
  def isQFree(formula: Formula): Boolean = {
    !formula.hasSubFormula {
441
      case _: Quantifier => true
Christian Müller's avatar
Christian Müller committed
442 443 444
    }
  }

445
  def toNegNf(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
446 447 448 449
    //    val bound = if (hasDuplicateBindings(f)) {
    //      //      logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
    //      FormulaFunctions.fixBinding(f, Set())._1
    //    } else f
Christian Müller's avatar
Christian Müller committed
450
    val noeq = eliminateEq(f)
Christian Müller's avatar
Christian Müller committed
451
    eliminateImplication(noeq).simplify
452 453
  }

454
  def generateName(base: Var, bound: Set[Var]): Var = {
455

456
    val chars = base.name.toCharArray
457 458 459 460
    val (basename, start) = if (chars.last.isDigit) {
      (base.name.dropRight(1), chars.last.toInt + 1)
    } else {
      (base.name, 1)
Christian Müller's avatar
Christian Müller committed
461
    }
462 463 464 465 466 467 468
    val stream = Stream.from(start)

    val droppedstream = stream.dropWhile(i => bound.contains(Var(basename + i, base.typ)))

    Var(basename + droppedstream.head, base.typ)
  }

Christian Müller's avatar
Christian Müller committed
469 470 471 472 473 474 475 476
  // TODO: This could be improved for the general case
  def fixBinding(f: Formula): Formula = {
    if (f.isUniversal) {
      fixUniversalBindings(f)._1
    } else {
      fixGeneralBindings(f)._1
    }
  }
477
  def fixBinding(f: Formula, bound:Set[Var]): Formula = {
Christian Müller's avatar
Christian Müller committed
478 479 480 481 482 483
    if (f.isUniversal) {
      fixUniversalBindings(f, bound)._1
    } else {
      fixGeneralBindings(f, bound)._1
    }
  }
Christian Müller's avatar
Christian Müller committed
484

485 486 487
  private def fixGeneralBindings(t:Formula, bound:Set[Var] = Set()):(Formula, Set[Var]) = {
    def fix(t: Formula, bound: Set[Var]): (Formula, Set[Var]) = t match {
      case UnOp(make, f1) =>
Christian Müller's avatar
Christian Müller committed
488
        val (newf, newbounds) = fix(f1, bound)
489
        (make(newf), newbounds)
490
      case BinOp(make, f1, f2) =>
Christian Müller's avatar
Christian Müller committed
491 492
        val (newf1, newbound) = fix(f1, bound)
        val (newf2, newbound2) = fix(f2, newbound)
493
        (make(newf1, newf2), newbound2)
494
      case Quantifier(make, vars, fsub) =>
Christian Müller's avatar
Christian Müller committed
495
        val alreadybounds = vars.filter(bound.contains)
496 497 498 499
        val newnames = alreadybounds.map(generateName(_, bound))
        val renamed = fsub.parallelRename(alreadybounds, newnames)
        val binding = (vars.toSet -- alreadybounds) ++ newnames

Christian Müller's avatar
Christian Müller committed
500
        val (fixedrename, newbound) = fix(renamed, bound ++ binding)
501 502 503 504
        val newf = make(binding.toList, fixedrename)
        (newf, newbound)
      // Functions, Variables
      case f => (f, bound)
Christian Müller's avatar
Christian Müller committed
505
    }
506
    logger.trace("Using fallback fixbindings method for general formulas.")
507
    fix(t, bound ++ t.freeVars)
Christian Müller's avatar
Christian Müller committed
508 509 510
  }


Christian Müller's avatar
Christian Müller committed
511
  private def fixUniversalBindings(f: Formula, bound:Set[Var] = Set()): (Formula, Set[Var]) = {
Christian Müller's avatar
Christian Müller committed
512 513
    def fix(f:Formula, bound: Set[Var]):(Formula, Set[Var]) = {
      f match {
514
        case UnOp(make, f1) =>
Christian Müller's avatar
Christian Müller committed
515 516
          val (newf, newbounds) = fix(f1, bound)
          (make(newf), newbounds)
517
        case Or(f1, f2) =>
Christian Müller's avatar
Christian Müller committed
518 519 520
          val (newf1, newbound) = fix(f1, bound)
          val (newf2, newbound2) = fix(f2, newbound)
          (Or(newf1, newf2), newbound2)
521
        case And(f1, f2) =>
Christian Müller's avatar
Christian Müller committed
522 523 524
          val (newf1, newbound) = fix(f1, bound)
          val (newf2, newbound2) = fix(f2, bound)
          (And(newf1, newf2), newbound ++ newbound2)
525
        case Quantifier(make, vars, fsub) =>
Christian Müller's avatar
Christian Müller committed
526 527 528 529 530 531 532 533 534
          val alreadybounds = vars.filter(bound.contains)
          val newnames = alreadybounds.map(generateName(_, bound))
          val renamed = fsub.parallelRename(alreadybounds, newnames)
          val binding = (vars.toSet -- alreadybounds) ++ newnames

          val (fixedrename, newbound) = fix(renamed, bound ++ binding)
          val newf = make(binding.toList, fixedrename)
          (newf, newbound)
        // Functions, Variables
535
        case t => (t, bound)
Christian Müller's avatar
Christian Müller committed
536 537 538 539 540 541
      }
    }

    if (!f.isUniversal) {
      logger.error("Trying to fix universal bindings of non-universal formula")
    }
Christian Müller's avatar
Christian Müller committed
542
    fix(f, bound ++ f.freeVars)
543 544
  }

Christian Müller's avatar
Christian Müller committed
545
  // TODO: make sure no quantifiers in scope of others with same name
Christian Müller's avatar
Christian Müller committed
546
  def toPrenex(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
547
    val negnf = f.toNegNf.simplify
Christian Müller's avatar
src  
Christian Müller committed
548

Christian Müller's avatar
Christian Müller committed
549 550
    val simp = fixBinding(negnf)
//    val simp = negnf
551

Christian Müller's avatar
Christian Müller committed
552
    // Simplify first to push negation inward
Christian Müller's avatar
Christian Müller committed
553
    val quantifiers = collectQuantifiers(simp)
Christian Müller's avatar
src  
Christian Müller committed
554
    val stripped = stripQuantifiers(simp)
555

Christian Müller's avatar
Christian Müller committed
556 557 558 559
    // Not using rewrapQuantifiers since that one pushes quantifiers inward again
    //    val wrapped = rewrapQuantifiers(quants, stripped)
    quantifiers.foldRight(stripped)((quant, inner) => {
      if (quant._1) Exists(quant._2, inner) else Forall(quant._2, inner)
Christian Müller's avatar
Christian Müller committed
560
    }).simplify
Christian Müller's avatar
src  
Christian Müller committed
561 562
  }

563
  def rewrapQuantifiers(quantifiers: List[(Boolean, List[Var])], f:Formula): Formula = {
Christian Müller's avatar
src  
Christian Müller committed
564
    val wrapped = quantifiers.foldRight(f)((quant, inner) => {
Christian Müller's avatar
Christian Müller committed
565
      if (quant._1) Exists(quant._2, inner) else Forall(quant._2, inner)
Christian Müller's avatar
Christian Müller committed
566
    }).simplify
Christian Müller's avatar
src  
Christian Müller committed
567 568 569 570 571 572 573

    // if all universal, push them inward
    if (quantifiers.forall(!_._1)) {
      FormulaFunctions.pushUniversalQuantifiers(wrapped)
    } else {
      wrapped
    }
Christian Müller's avatar
Christian Müller committed
574
  }
575

576
  def toCNFClauses(f: Formula): (List[(Boolean, List[Var])], List[List[Formula]]) = {
Christian Müller's avatar
Christian Müller committed
577
    @tailrec
578
    def toCNFSub(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
579
      val (changed, sub) = everywhereFP({
Christian Müller's avatar
Christian Müller committed
580 581
        case Or(And(f1, f2), f3) => And(Or(f1, f3), Or(f2, f3))
        case Or(f1, And(f2, f3)) => And(Or(f1, f2), Or(f1, f3))
Christian Müller's avatar
Christian Müller committed
582 583
      }, f)
      if (!changed) sub else toCNFSub(sub)
584 585
    }

Christian Müller's avatar
Christian Müller committed
586 587 588
//    if (f.isUniversal) {
//        Z3BSFO.toCNFClausesUniversal(f)
//    } else {
589
//      logger.warn("Using internal CNF conversion - may blow up")
590

Christian Müller's avatar
Christian Müller committed
591 592 593
    // FIXME: can we do it without prenex? may be expensive later on
    val normalized = f.toPrenex.simplify
    logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
594

Christian Müller's avatar
Christian Müller committed
595
    val quantifiers = FormulaFunctions.collectQuantifiers(normalized)
596

Christian Müller's avatar
Christian Müller committed
597 598 599
    // normalized is now Quantifiers, then only And/Or with Negation inside
    // no simplification here
    val cnf1 = toCNFSub(normalized)
Christian Müller's avatar
Christian Müller committed
600

Christian Müller's avatar
Christian Müller committed
601 602
    // Inspect clauses
    val clauses = FOTransformers.collectClauses(cnf1)
Christian Müller's avatar
Christian Müller committed
603

Christian Müller's avatar
Christian Müller committed
604 605 606
    // Simplify clauses
    // TODO: improve, don't sort by tostring
    val sorted = clauses.map(c => c.sortBy(_.toString())).sortBy(f => f.toString())
Christian Müller's avatar
Christian Müller committed
607

Christian Müller's avatar
Christian Müller committed
608 609 610 611
    // Remove trivial clauses
    val notrivials = sorted.filterNot(c => {
      c.exists(f => c.contains(Neg(f)))
    })
Christian Müller's avatar
Christian Müller committed
612

Christian Müller's avatar
Christian Müller committed
613 614 615 616 617 618
    // TODO improve runtime
    val simped = notrivials.filterNot(c => notrivials.exists(c2 => {
      // check if c is superset of c2
      //      c != c2 && c.startsWith(c2)
      c != c2 && c.forall(f => c2.contains(f))
    }))
619
//      logger.debug(s"After simplification ${simped.size} unsubsumed clauses remaining.")
Christian Müller's avatar
Christian Müller committed
620 621
    logger.debug(s"Resulting CNF has ${sorted.size} clauses")
    (quantifiers, simped)
Christian Müller's avatar
Christian Müller committed
622
//    }
Christian Müller's avatar
Christian Müller committed
623
  }
Christian Müller's avatar
Christian Müller committed
624

625
  def toCNF(f: Formula): Formula = {
Christian Müller's avatar
src  
Christian Müller committed
626 627 628 629
      val (quantifiers, clauses) = toCNFClauses(f)
      val form = And.make(clauses.map(Or.make))
      val newform = rewrapQuantifiers(quantifiers, form)
      newform
630
  }
Christian Müller's avatar
Christian Müller committed
631

Christian Müller's avatar
Christian Müller committed
632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
  def toDNFClauses(f:Formula):(List[(Boolean, List[Var])], List[List[Formula]]) = {
    val simp = f.toPrenex.simplify
    val quantifiers = collectQuantifiers(simp)
    val stripped = stripQuantifiers(simp)

    val (_, cnfclauses) = toCNFClauses(Neg(stripped))

    // Negate all single valued
    val dnfclauses = cnfclauses.map(_.map(Neg(_).simplify))

    (quantifiers, dnfclauses)
  }

  def toDNF(f: Formula): Formula = {
    val (quantifiers, clauses) = toDNFClauses(f)
    val form = Or.make(clauses.map(And.make))
    val newform = rewrapQuantifiers(quantifiers, form)
    newform
  }

652 653
  /**
   * Resolves a universally quantified predicate
Christian Müller's avatar
src  
Christian Müller committed
654
   * Blows up the formula exponentially due to CNF
655
   */
656
  def eliminatePredicate(f: Formula, name: String): Formula = {
Christian Müller's avatar
Christian Müller committed
657
    def listFunsWithName(f: Formula, name: String) = {
658
      f.collect({
Christian Müller's avatar
Christian Müller committed
659
        case Fun(n, ind, vars) if n == name      => List((Some(Fun(n, ind, vars)), None))
660 661 662
        case Neg(Fun(n, ind, vars)) if n == name => List((None, Some(Neg(Fun(n, ind, vars)))))
      })
    }
Christian Müller's avatar
Christian Müller committed
663

Christian Müller's avatar
Christian Müller committed
664
    val norm = f.toCNF
Christian Müller's avatar
Christian Müller committed
665

666 667
    val removed = norm.everywhere({
      // find top-level ORs in CNF
668
      case inner: Or =>
669
        val list = listFunsWithName(inner, name)
Christian Müller's avatar
Christian Müller committed
670

Christian Müller's avatar
Christian Müller committed
671 672
        val positives = list.flatMap(_._1)
        val negatives = list.flatMap(_._2)
Christian Müller's avatar
Christian Müller committed
673 674

        val isSuperFluous = positives.exists { f1 =>
Christian Müller's avatar
Christian Müller committed
675
          negatives.contains(Neg(f1))
676
        }
Christian Müller's avatar
Christian Müller committed
677

678 679 680 681 682
        if (isSuperFluous) {
          // Remove clause
          True
        } else {
          // Remove predicate both in positive and negative
Christian Müller's avatar
Christian Müller committed
683
          inner.everywhere({
684 685
            case Neg(Fun(n, _, _)) if n == name => False
            case Fun(n, _, _) if n == name      => False
686 687 688
          })
        }
    })
Christian Müller's avatar
Christian Müller committed
689

Christian Müller's avatar
Christian Müller committed
690
    removed.simplify
Christian Müller's avatar
Christian Müller committed
691

692
  }
Christian Müller's avatar
Christian Müller committed
693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725

  def getPositiveArguments(clause: List[Formula], NAME:String):Set[List[Var]] = {
    clause flatMap {
      case Fun(NAME, _, vars) => List(vars)
      case _ => List()
    } toSet
  }
  def getNegativeArguments(clause: List[Formula], NAME:String):Set[List[Var]] = {
    clause flatMap {
      case Neg(Fun(NAME, _, vars))=> List(vars)
      case _ => List()
    } toSet
  }
  def ineq(l1:List[Var], l2:List[Var]): Formula = {
    if (l1.size != l2.size) {
      logger.warn("Trying to generate inequalities for different sized vectors")
    }
    val ineqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
      case (x, y) if x.name <= y.name => Neg(Equal(x,y))
      case (x, y)  => Neg(Equal(y,x))
    }.toSet
    Or.make(ineqs.toList)
  }
  def eq(l1:List[Var], l2:List[Var]):Formula = {
    if (l1.size != l2.size) {
      logger.warn("Trying to generate equalities for different sized vectors")
    }
    val eqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
      case (x, y) if x.name <= y.name => Equal(x,y)
      case (x, y)  => Equal(y,x)
    }.toSet
    And.make(eqs.toList)
  }
Christian Müller's avatar
Christian Müller committed
726
}