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

import FOLTL._
Christian Müller's avatar
Christian Müller committed
4
import com.typesafe.scalalogging.LazyLogging
5
import de.tum.workflows.blocks.Workflow
Christian Müller's avatar
Christian Müller committed
6
import scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
7

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

Christian Müller's avatar
Christian Müller committed
10

11
12
  def freeVars(t: Formula) = {
    def free(t: Formula, bound: Set[Var]): Set[Var] = {
Christian Müller's avatar
Christian Müller committed
13
14
15
      t match {
        // Extractors
        // Exists, Forall
Christian Müller's avatar
Christian Müller committed
16
17
        case Quantifier(_, ps, t) => free(t, bound ++ ps)
        case UnOp(make, 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
23
24
25
        //      TODO: path is not a free variable anymore
        //        case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
        case Fun(_, _, ps)        => (ps.toSet -- bound)
        case v: Var if !bound(v)  => Set(v)
        case x                    => Set()
Christian Müller's avatar
Christian Müller committed
26
27
28
29
30
      }
    }
    free(t, Set())
  }

31
32
  def simplify(t: Formula): Formula = {
    val simp: PartialFunction[Formula, Formula] = {
Christian Müller's avatar
Christian Müller committed
33
      // Push negation inward
Christian Müller's avatar
Christian Müller committed
34
35
36
37
38
39
40
41
      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
42
43

      // Simple laws
Christian Müller's avatar
Christian Müller committed
44
45
46
47
48
49
50
51
52
53
54
      case Neg(True)                          => False
      case Neg(False)                         => True
      case Neg(Neg(t))                        => t
      case Or(True, t)                        => True
      case Or(t, True)                        => True
      case Or(False, t)                       => t
      case Or(t, False)                       => t
      case And(False, t)                      => False
      case And(t, False)                      => False
      case And(True, t)                       => t
      case And(t, True)                       => t
Christian Müller's avatar
Christian Müller committed
55
56
      case Implies(False, t)                  => True
      case Implies(True, t)                   => t
Christian Müller's avatar
Christian Müller committed
57
58
59
60
      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
61
62
63
64

      // left-trees
      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
65
      
Christian Müller's avatar
Christian Müller committed
66
67
68
69
70
71
72
73
      // equal things in tree
      case And(t1, t2) if t1 == t2            => t1
      case Or(t1, t2) if t1 == t2             => t1
      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)

74
75
76
77
78
79
80
      // And Or
      case And(t1, Or(t2, t3)) if (t1 == t3)  => t1
      case And(t1, Or(t2, t3)) if (t1 == t2)  => t1
      case And(Or(t2, t3), t1) if (t1 == t3)  => t1
      case And(Or(t2, t3), t1) if (t1 == t2)  => t1


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

83
      // Equivalence
Christian Müller's avatar
Christian Müller committed
84
      case Eq(t1, t2) if t1 == t2             => True
Christian Müller's avatar
Christian Müller committed
85

86
      // Double Temporals
Christian Müller's avatar
Christian Müller committed
87
88
      case Finally(Finally(t))                => Finally(t)
      case Globally(Globally(t))              => Globally(t)
Christian Müller's avatar
Christian Müller committed
89
90

      // Remove quantifiers if empty
91
      case Quantifier(_, xs, t) if xs.isEmpty => t
Christian Müller's avatar
Christian Müller committed
92
93
      case Quantifier(_, _, True)             => True
      case Quantifier(_, _, False)            => False
Christian Müller's avatar
Christian Müller committed
94
95
96
97
98
99
      
      // Quantifiers binding same things
      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))
100

Christian Müller's avatar
Christian Müller committed
101
102
103
      // Gobble up equal quantifiers
      case Forall(vars1, Forall(vars2, f))    => Forall(vars1 ++ vars2, f)
      case Exists(vars1, Exists(vars2, f))    => Exists(vars1 ++ vars2, f)
104

Christian Müller's avatar
Christian Müller committed
105
      // Remove variables from quantifiers if not used in the body: Caution - expensive
Christian Müller's avatar
Christian Müller committed
106
107
108
109
110
111
112
113
114
115
      //      case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
      //        qmake((xs.toSet.intersect(t.freeVars())).toList, t)
      //
      //      // 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)
    }

116
117
118
//    val (changed, t1) = everywhereFP(simp, t)
//    if (!changed) t1 else simplify(t1)
    everywhereBotUp(simp, t)
Christian Müller's avatar
Christian Müller committed
119
  }
120

Christian Müller's avatar
Christian Müller committed
121
  def eliminateImplication(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
122
    f everywhere {
Christian Müller's avatar
testing    
Christian Müller committed
123
124
125
      case Implies(f1, f2) => Or(Neg(eliminateImplication(f1)), eliminateImplication(f2))
    }
  }
Christian Müller's avatar
Christian Müller committed
126
127

  def eliminateEq(f: Formula): Formula = {
Christian Müller's avatar
testing    
Christian Müller committed
128
129
130
131
132
133
    f everywhere {
      case Eq(f1, f2) => {
        val e1 = eliminateEq(f1)
        val e2 = eliminateEq(f2)
        And(Implies(e1, e2), Implies(e2, e1))
      }
Christian Müller's avatar
Christian Müller committed
134
135
    }
  }
Christian Müller's avatar
Christian Müller committed
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
  
  def everywhereFP(trans: PartialFunction[Formula, Formula], t: Formula): (Boolean, Formula) = {
    if (trans.isDefinedAt(t))
      (true, trans(t))
    else
      t match {
        // Extractors
        case Quantifier(make, ps, t1) => {
          val sub = everywhereFP(trans, t1)
          (sub._1, make(ps, sub._2))
        }
        case UnOp(make, t1)          => {
          val sub = everywhereFP(trans, t1)
          (sub._1, make(sub._2))
        }
        case BinOp(make, t1, t2)     => {
          val (c1, sub1) = everywhereFP(trans, t1)
          val (c2, sub2) = everywhereFP(trans, t2)
          (c1 || c2, make(sub1, sub2))
        }
        case x                       => (false, x)
      }
  }
Christian Müller's avatar
Christian Müller committed
159

160
  def everywhere(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
161
162
163
164
165
166
    if (trans.isDefinedAt(t))
      trans(t)
    else
      t match {
        // Extractors
        case Quantifier(make, ps, t) => make(ps, everywhere(trans, t))
Christian Müller's avatar
Christian Müller committed
167
        case UnOp(make, t1)          => make(everywhere(trans, t1))
Christian Müller's avatar
Christian Müller committed
168
169
170
171
        case BinOp(make, t1, t2)     => make(everywhere(trans, t1), everywhere(trans, t2))
        case x                       => x
      }
  }
172
173
  
  def everywhereBotUp(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
174
    // First apply trans to push negation inward etc
175
176
177
178
179
180
181
182
183
184
    if (trans.isDefinedAt(t))
      everywhereBotUp(trans, trans(t))
    else {
      val sub = t match {
        // Extractors
        case Quantifier(make, ps, t) => make(ps, everywhereBotUp(trans, t))
        case UnOp(make, t1)          => make(everywhereBotUp(trans, t1))
        case BinOp(make, t1, t2)     => make(everywhereBotUp(trans, t1), everywhereBotUp(trans, t2))
        case x                       => x
      }
185
186
187
188
189
      // Applicable after inner transformation?
      if (trans.isDefinedAt(sub))
        trans(sub)
      else
        sub
190
191
    }
  }
192

193
  def opsize(t: Formula): Int = {
194
195
196
197
198
199
200
201
    t match {
      // Extractors
      case Quantifier(_, ps, t) => 1 + t.opsize()
      case UnOp(_, t)           => 1 + t.opsize()
      case BinOp(_, t1, t2)     => 1 + t1.opsize() + t2.opsize()
      case x                    => 1
    }
  }
Christian Müller's avatar
Christian Müller committed
202

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

216
  def collect[T](coll: PartialFunction[Formula, List[T]], t: Formula): List[T] = {
217
218
219
220
221
222
223
224
225
    if (coll.isDefinedAt(t))
      coll(t)
    else
      t match {
        // Extractors
        case Quantifier(make, ps, t) => collect(coll, t)
        case UnOp(make, t)           => collect(coll, t)
        case BinOp(make, t1, t2)     => List.concat(collect(coll, t1), collect(coll, t2))
        case x                       => List.empty
Christian Müller's avatar
Christian Müller committed
226
227
      }
  }
Christian Müller's avatar
Christian Müller committed
228

Christian Müller's avatar
Christian Müller committed
229
  def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula):Boolean = {
Christian Müller's avatar
Christian Müller committed
230
    def or(bs: Boolean*) = { bs.exists(identity) }
Christian Müller's avatar
Christian Müller committed
231
232
    collect(or)(coll, t)
  }
Christian Müller's avatar
Christian Müller committed
233
234
235
236
237
238
239
240
241
242
243
244
245
246

  //  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
  //      }
  //    }
  //  }
247

248
  def assumeEmpty(t: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
249
250
251
252
    t.everywhere({
      case Fun(f, _, _) if f == name => False
    })
  }
Christian Müller's avatar
Christian Müller committed
253
254

  def assumeAllEmpty(f: Formula, names: List[String]) = {
255
    // Assume all workflow relations empty
Christian Müller's avatar
Christian Müller committed
256
    val assumers = names.map(p => (f: Formula) => assumeEmpty(f, p))
Christian Müller's avatar
Christian Müller committed
257
    val allempty = assumers.foldLeft(f)((f, a) => a(f))
258
259
    allempty.simplify()
  }
Christian Müller's avatar
Christian Müller committed
260

261
  def annotate(t: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
262
263
264
265
    t.everywhere({
      case Fun(f, None, xs) => Fun(f, Some(name), xs)
    })
  }
Christian Müller's avatar
Christian Müller committed
266
267

  def annotateOverwrite(t: Formula, Name1: String, name: String) = {
Christian Müller's avatar
Christian Müller committed
268
269
270
271
    t.everywhere({
      case Fun(f, Some(Name1), xs) => Fun(f, Some(name), xs)
    })
  }
272

273
  def annotate(t: Formula, name: String, ignore: Set[String]) = {
274
275
276
277
    t.everywhere({
      case Fun(f, None, xs) if (!(ignore contains f)) => Fun(f, Some(name), xs)
    })
  }
278

279
  def checkSanity(t: Formula) = {
Christian Müller's avatar
Christian Müller committed
280
281
282
    // TODO add more things, f.e. existentials
    // T1, T2 can appear freely
    val frees = t.freeVars() -- Set(Var(Properties.T1), Var(Properties.T2))
Christian Müller's avatar
Christian Müller committed
283
    if (frees.nonEmpty) {
Christian Müller's avatar
Christian Müller committed
284
285
      logger.warn(s"Sanity check failed: $frees appear free in the property.")
    }
286

Christian Müller's avatar
Christian Müller committed
287
288
    frees.isEmpty
  }
Christian Müller's avatar
Christian Müller committed
289
290

  def removeOTQuantifiers(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
291
292
293
    f.everywhere({
      case ForallOtherThan(vars, otherthan, fp) => {
        val eqs = for (x <- vars; y <- otherthan) yield {
Christian Müller's avatar
Christian Müller committed
294
          Neg(Eq(x, y))
Christian Müller's avatar
Christian Müller committed
295
        }
Christian Müller's avatar
Christian Müller committed
296
        Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
Christian Müller's avatar
Christian Müller committed
297
298
299
      }
    })
  }
Christian Müller's avatar
Christian Müller committed
300
301

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

Christian Müller's avatar
Christian Müller committed
305
306
    parallelRename(f, repls)
  }
Christian Müller's avatar
Christian Müller committed
307
308
309

  def parallelRename(f: Formula, repls: Map[Var, Var]): Formula = {
    f everywhere {
Christian Müller's avatar
Christian Müller committed
310
      case v: Var if repls.contains(v) => repls(v)
Christian Müller's avatar
Christian Müller committed
311
      case Fun(f, ind, params)         => Fun(f, ind, params map (p => repls.getOrElse(p, p)))
Christian Müller's avatar
Christian Müller committed
312
313
314
315
316
317
      case Quantifier(make, xs, f) => {
        val rep = repls -- (xs)
        make(xs, parallelRename(f, rep))
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
318
319
320
321
322
323
324
325
326
327
328
329
330

  /**
   * Check if there exist quantifiers binding the same variable more than once
   */
  def hasDuplicateBindings(f: Formula) = {
    def boundNames(f: Formula): List[Var] = {
      f collect {
        case Quantifier(make, xs, sub) => xs ++: boundNames(sub)
      }
    }
    boundNames(f).groupBy(n => n).exists(_._2.length > 1)
  }

331
332
333
  def stripQuantifiers(f: Formula): Formula = {
    f everywhere {
      case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
Christian Müller's avatar
Christian Müller committed
334
    }
335
  }
Christian Müller's avatar
Christian Müller committed
336

Christian Müller's avatar
Christian Müller committed
337
  def collectQuantifiers(f: Formula): List[(Boolean, List[Var])] = {
338
    f collect {
Christian Müller's avatar
Christian Müller committed
339
340
      case Exists(xs, fsub) => (true, xs) :: collectQuantifiers(fsub)
      case Forall(xs, fsub) => (false, xs) :: collectQuantifiers(fsub)
341
      case BinOp(make, f1, f2) => {
Christian Müller's avatar
Christian Müller committed
342
343
        val q1 = collectQuantifiers(f1)
        val q2 = collectQuantifiers(f2)
344

Christian Müller's avatar
Christian Müller committed
345
        // Merge while trying to stay in BS, if possible
346
        // TODO: could be improved to minimize quantifier alternations)
Christian Müller's avatar
Christian Müller committed
347
        // TODO: merge universals with same type by renaming
348
349
        val ex1 = q1.takeWhile(_._1)
        val rest1 = q1.drop(ex1.size)
Christian Müller's avatar
Christian Müller committed
350
351
352
353
354
355
356
357
358
        
        // filter out same bound variables (TODO: could be improved if different names)
        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 =>
Christian Müller's avatar
Christian Müller committed
359
          (q._1, q._2.filterNot(exset.contains))
Christian Müller's avatar
Christian Müller committed
360
        )
Christian Müller's avatar
Christian Müller committed
361
        val rest2 = q2.drop(ex2.size).map(q =>
Christian Müller's avatar
Christian Müller committed
362
          (q._1, q._2.filterNot(univset.contains))
Christian Müller's avatar
Christian Müller committed
363
        )
364
        ex1 ++ ex2 ++ rest1 ++ rest2
Christian Müller's avatar
Christian Müller committed
365
366
      }
    }
367
  }
Christian Müller's avatar
Christian Müller committed
368
369
370
371
372
  
  def checkBindings(f:Formula) = {
    def checkBindingsSub(f: Formula, bound:Set[Var]):List[Var] = {
        f collect {
          case Quantifier(make, xs, inner) => {
Christian Müller's avatar
Christian Müller committed
373
            val conflicts = xs.filter(bound.contains)
Christian Müller's avatar
Christian Müller committed
374
375
376
377
378
            conflicts ++ checkBindingsSub(inner, bound ++ xs)
          }
        }
    }
    checkBindingsSub(f, Set()).isEmpty
379
  }
Christian Müller's avatar
Christian Müller committed
380
381

  def isBS(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
382
383
384
385
386
387
    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)
    }
388
  }
Christian Müller's avatar
Christian Müller committed
389

Christian Müller's avatar
Christian Müller committed
390
391
392
393
394
395
396
  def isQFree(formula: Formula): Boolean = {
    !formula.hasSubFormula {
      case q:Quantifier => true
    }
  }


Christian Müller's avatar
Christian Müller committed
397
  def toNegNf(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
398
399
400
401
402
//    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
    val noeq = eliminateEq(f)
Christian Müller's avatar
testing    
Christian Müller committed
403
    eliminateImplication(noeq).simplify()
404
405
406
407
408
409
410
411
412
  }

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

    val chars = base.name.toCharArray()
    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
413
    }
414
415
416
417
418
419
420
421
422
423
424
425
    val stream = Stream.from(start)

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

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

  def fixBinding(f: Formula, bound: Set[Var]): (Formula, Set[Var]) = {
    f match {
      case UnOp(make, f1) => {
        val (newf, newbounds) = fixBinding(f1, bound)
        (make(newf), newbounds)
Christian Müller's avatar
Christian Müller committed
426
      }
427
428
429
430
431
432
      case BinOp(make, f1, f2) => {
        val (newf1, newbound) = fixBinding(f1, bound)
        val (newf2, newbound2) = fixBinding(f2, newbound)
        (make(newf1, newf2), newbound2)
      }
      case Quantifier(make, vars, fsub) => {
Christian Müller's avatar
Christian Müller committed
433
        val alreadybounds = vars.filter(bound.contains)
434
435
436
437
438
439
440
441
442
443
        val newnames = alreadybounds.map(generateName(_, bound))
        val renamed = fsub.parallelRename(alreadybounds, newnames)
        val binding = (vars.toSet -- alreadybounds) ++ newnames

        val (fixedrename, newbound) = fixBinding(renamed, bound ++ binding)
        val newf = make(binding.toList, fixedrename)
        (newf, newbound)
      }
      // Functions, Variables
      case f => (f, bound)
Christian Müller's avatar
Christian Müller committed
444
    }
445
446
  }

Christian Müller's avatar
Christian Müller committed
447
448
  // TODO: make sure no quantifiers in scope of others with same name
  def toPrenex(f: Formula):Formula = {
Christian Müller's avatar
Christian Müller committed
449
    val negnf = f.toNegNf
Christian Müller's avatar
Christian Müller committed
450
//    val (simp, boundVars) = fixBinding(negnf, Set())
451

Christian Müller's avatar
Christian Müller committed
452
    // Simplify first to push negation inward
Christian Müller's avatar
Christian Müller committed
453
454
    val quants = collectQuantifiers(negnf)
    val stripped = stripQuantifiers(negnf)
455

Christian Müller's avatar
Christian Müller committed
456
457
    quants.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
458
    }).simplify()
Christian Müller's avatar
Christian Müller committed
459
  }
Christian Müller's avatar
Christian Müller committed
460

Christian Müller's avatar
Christian Müller committed
461
  def toCNFClauses(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
462
    @tailrec
Christian Müller's avatar
Christian Müller committed
463
    def toCNFSub(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
464
      val (changed, sub) = everywhereFP({
Christian Müller's avatar
Christian Müller committed
465
466
        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
467
468
      }, f)
      if (!changed) sub else toCNFSub(sub)
Christian Müller's avatar
Christian Müller committed
469
470
    }

471

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

    // normalized is now Quantifiers, then only And/Or with Negation inside
Christian Müller's avatar
Christian Müller committed
477
    // no simplification here
478
479
480
481
482
    val cnf1 = toCNFSub(normalized)
    val cnf2 = everywhereBotUp({
      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))
    }, normalized)
Christian Müller's avatar
Christian Müller committed
483
            
484
    val quantifiers = FormulaFunctions.collectQuantifiers(cnf1)
Christian Müller's avatar
Christian Müller committed
485
486
    
    // Inspect clauses
487
    val clauses = FOTransformers.collectClauses(cnf1)
Christian Müller's avatar
Christian Müller committed
488
489
490
491
492
493
494
495
496
497
498
499
        
    // TODO improve runtime
    val simpedset = clauses.toSet
    val simped = simpedset.filterNot(c => simpedset.exists(c2 => {
      // check if c is superset of c2
      c != c2 && c.startsWith(c2)
    }))
    (quantifiers, clauses)  
  }
  
  def toCNF(f:Formula) = {
    val (quantifiers, clauses)  = toCNFClauses(f)
Christian Müller's avatar
Christian Müller committed
500
    val form = And.make(clauses.map(Or.make))
Christian Müller's avatar
Christian Müller committed
501
502
    val newform = quantifiers.foldRight(form)((q, inner) => if(q._1) Exists(q._2, inner) else Forall(q._2, inner))
    newform
Christian Müller's avatar
Christian Müller committed
503
  }
Christian Müller's avatar
Christian Müller committed
504

Christian Müller's avatar
Christian Müller committed
505
506
507
508
  /**
   * Resolves a universally quantified predicate
   * Blows up the formula linearly due to CNF
   */
Christian Müller's avatar
Christian Müller committed
509
510
  def eliminatePredicate(f: Formula, name: String) = {
    def listFunsWithName(f: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
511
      f.collect({
Christian Müller's avatar
Christian Müller committed
512
        case Fun(n, ind, vars) if n == name      => List((Some(Fun(n, ind, vars)), None))
Christian Müller's avatar
Christian Müller committed
513
514
515
        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
516

Christian Müller's avatar
Christian Müller committed
517
    val norm = f.toCNF
Christian Müller's avatar
Christian Müller committed
518

Christian Müller's avatar
Christian Müller committed
519
520
    val removed = norm.everywhere({
      // find top-level ORs in CNF
Christian Müller's avatar
Christian Müller committed
521
      case inner: Or => {
Christian Müller's avatar
Christian Müller committed
522
        val list = listFunsWithName(inner, name)
Christian Müller's avatar
Christian Müller committed
523

Christian Müller's avatar
Christian Müller committed
524
525
        val positives = list.flatMap(_._1)
        val negatives = list.flatMap(_._2)
Christian Müller's avatar
Christian Müller committed
526
527

        val isSuperFluous = positives.exists { f1 =>
Christian Müller's avatar
Christian Müller committed
528
          negatives.contains(Neg(f1))
Christian Müller's avatar
Christian Müller committed
529
        }
Christian Müller's avatar
Christian Müller committed
530

Christian Müller's avatar
Christian Müller committed
531
532
533
534
535
        if (isSuperFluous) {
          // Remove clause
          True
        } else {
          // Remove predicate both in positive and negative
Christian Müller's avatar
Christian Müller committed
536
          inner.everywhere({
Christian Müller's avatar
Christian Müller committed
537
            case Neg(Fun(n, ind, vars)) if n == name => False
Christian Müller's avatar
Christian Müller committed
538
            case Fun(n, ind, vars) if n == name      => False
Christian Müller's avatar
Christian Müller committed
539
540
541
542
          })
        }
      }
    })
Christian Müller's avatar
Christian Müller committed
543

Christian Müller's avatar
Christian Müller committed
544
    removed.simplify()
Christian Müller's avatar
Christian Müller committed
545

Christian Müller's avatar
Christian Müller committed
546
  }
Christian Müller's avatar
Christian Müller committed
547
}