FormulaFunctions.scala 18.8 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

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

Christian Müller's avatar
Christian Müller committed
20
21
22
23
24
        //      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
25
26
27
28
29
      }
    }
    free(t, Set())
  }

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

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

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

73
      // And Or
Christian Müller's avatar
Christian Müller committed
74
75
76
77
      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
78

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

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

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

      // Remove quantifiers if empty
89
      case Quantifier(_, xs, t) if xs.isEmpty => t
Christian Müller's avatar
Christian Müller committed
90
91
92
      case Quantifier(_, _, True) => True
      case Quantifier(_, _, False) => False

Christian Müller's avatar
Christian Müller committed
93
94
95
96
97
      // 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))
98

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

Christian Müller's avatar
Christian Müller committed
103
      // Remove variables from quantifiers if not used in the body: Caution - expensive
Christian Müller's avatar
Christian Müller committed
104
105
106
107
108
109
110
111
      //      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)
Christian Müller's avatar
Christian Müller committed
112
113
114

      // Declass seen often enough
      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
115
116
    }

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

Christian Müller's avatar
Christian Müller committed
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
  def pushQuantifiers(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
        !onlyleft.isEmpty || !onlyright.isEmpty
      } => {
        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(
            pushQuantifiers(Forall.make(onlyleft.toList, f1)),
            pushQuantifiers(Forall.make(onlyright.toList, f2))))
      }
    }
  }

Christian Müller's avatar
Christian Müller committed
149
  def eliminateImplication(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
150
    f everywhere {
Christian Müller's avatar
testing    
Christian Müller committed
151
152
153
      case Implies(f1, f2) => Or(Neg(eliminateImplication(f1)), eliminateImplication(f2))
    }
  }
Christian Müller's avatar
Christian Müller committed
154
155

  def eliminateEq(f: Formula): Formula = {
Christian Müller's avatar
testing    
Christian Müller committed
156
157
158
159
160
161
    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
162
163
    }
  }
Christian Müller's avatar
Christian Müller committed
164

Christian Müller's avatar
Christian Müller committed
165
166
167
168
169
170
171
172
173
174
  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))
        }
Christian Müller's avatar
Christian Müller committed
175
        case UnOp(make, t1) => {
Christian Müller's avatar
Christian Müller committed
176
177
178
          val sub = everywhereFP(trans, t1)
          (sub._1, make(sub._2))
        }
Christian Müller's avatar
Christian Müller committed
179
        case BinOp(make, t1, t2) => {
Christian Müller's avatar
Christian Müller committed
180
181
182
183
          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
184
        case x => (false, x)
Christian Müller's avatar
Christian Müller committed
185
186
      }
  }
Christian Müller's avatar
Christian Müller committed
187

188
  def everywhere(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
189
190
191
192
193
194
    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
195
        case UnOp(make, t1)          => make(everywhere(trans, t1))
Christian Müller's avatar
Christian Müller committed
196
197
198
199
        case BinOp(make, t1, t2)     => make(everywhere(trans, t1), everywhere(trans, t2))
        case x                       => x
      }
  }
Christian Müller's avatar
Christian Müller committed
200

201
  def everywhereBotUp(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
202
    // First apply trans to push negation inward etc
203
204
205
206
207
208
209
210
211
212
    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
      }
213
214
215
216
217
      // Applicable after inner transformation?
      if (trans.isDefinedAt(sub))
        trans(sub)
      else
        sub
218
219
    }
  }
220

221
  def opsize(t: Formula): Int = {
222
223
224
225
226
227
228
229
    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
230

Christian Müller's avatar
Christian Müller committed
231
  def collect[T](combine: (T*) => T)(coll: PartialFunction[Formula, T], t: Formula): T = {
Christian Müller's avatar
Christian Müller committed
232
233
234
235
236
    if (coll.isDefinedAt(t))
      coll(t)
    else
      t match {
        // Extractors
Christian Müller's avatar
Christian Müller committed
237
238
239
240
        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()
241
242
      }
  }
243

244
  def collect[T](coll: PartialFunction[Formula, List[T]], t: Formula): List[T] = {
245
246
247
248
249
250
251
252
253
    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
254
255
      }
  }
Christian Müller's avatar
Christian Müller committed
256

Christian Müller's avatar
Christian Müller committed
257
  def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula): Boolean = {
Christian Müller's avatar
Christian Müller committed
258
    def or(bs: Boolean*) = { bs.exists(identity) }
Christian Müller's avatar
Christian Müller committed
259
260
    collect(or)(coll, t)
  }
Christian Müller's avatar
Christian Müller committed
261
262
263
264
265
266
267
268
269
270
271
272
273
274

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

276
  def assumeEmpty(t: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
277
278
279
280
    t.everywhere({
      case Fun(f, _, _) if f == name => False
    })
  }
Christian Müller's avatar
Christian Müller committed
281
282

  def assumeAllEmpty(f: Formula, names: List[String]) = {
283
    // Assume all workflow relations empty
Christian Müller's avatar
Christian Müller committed
284
    val assumers = names.map(p => (f: Formula) => assumeEmpty(f, p))
Christian Müller's avatar
Christian Müller committed
285
    val allempty = assumers.foldLeft(f)((f, a) => a(f))
286
287
    allempty.simplify()
  }
Christian Müller's avatar
Christian Müller committed
288

289
  def annotate(t: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
290
291
292
293
    t.everywhere({
      case Fun(f, None, xs) => Fun(f, Some(name), xs)
    })
  }
Christian Müller's avatar
Christian Müller committed
294
295

  def annotateOverwrite(t: Formula, Name1: String, name: String) = {
Christian Müller's avatar
Christian Müller committed
296
297
298
299
    t.everywhere({
      case Fun(f, Some(Name1), xs) => Fun(f, Some(name), xs)
    })
  }
300

301
  def annotate(t: Formula, name: String, ignore: Set[String]) = {
302
303
304
305
    t.everywhere({
      case Fun(f, None, xs) if (!(ignore contains f)) => Fun(f, Some(name), xs)
    })
  }
306

307
  def checkSanity(t: Formula) = {
Christian Müller's avatar
Christian Müller committed
308
309
310
    // 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
311
    if (frees.nonEmpty) {
Christian Müller's avatar
Christian Müller committed
312
313
      logger.warn(s"Sanity check failed: $frees appear free in the property.")
    }
314

Christian Müller's avatar
Christian Müller committed
315
316
    frees.isEmpty
  }
Christian Müller's avatar
Christian Müller committed
317
318

  def removeOTQuantifiers(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
319
320
321
    f.everywhere({
      case ForallOtherThan(vars, otherthan, fp) => {
        val eqs = for (x <- vars; y <- otherthan) yield {
Christian Müller's avatar
Christian Müller committed
322
          Neg(Eq(x, y))
Christian Müller's avatar
Christian Müller committed
323
        }
Christian Müller's avatar
Christian Müller committed
324
        Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
Christian Müller's avatar
Christian Müller committed
325
326
327
      }
    })
  }
Christian Müller's avatar
Christian Müller committed
328
329

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

Christian Müller's avatar
Christian Müller committed
333
334
    parallelRename(f, repls)
  }
Christian Müller's avatar
Christian Müller committed
335
336
337

  def parallelRename(f: Formula, repls: Map[Var, Var]): Formula = {
    f everywhere {
Christian Müller's avatar
Christian Müller committed
338
      case v: Var if repls.contains(v) => repls(v)
Christian Müller's avatar
Christian Müller committed
339
      case Fun(f, ind, params)         => Fun(f, ind, params map (p => repls.getOrElse(p, p)))
Christian Müller's avatar
Christian Müller committed
340
341
342
343
344
345
      case Quantifier(make, xs, f) => {
        val rep = repls -- (xs)
        make(xs, parallelRename(f, rep))
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
346
347
348
349
350
351
352
353
354
355
356
357
358

  /**
   * 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)
  }

359
360
361
  def stripQuantifiers(f: Formula): Formula = {
    f everywhere {
      case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
Christian Müller's avatar
Christian Müller committed
362
    }
363
  }
Christian Müller's avatar
Christian Müller committed
364

Christian Müller's avatar
Christian Müller committed
365
  def collectQuantifiers(f: Formula): List[(Boolean, List[Var])] = {
366
    f collect {
Christian Müller's avatar
Christian Müller committed
367
368
      case Exists(xs, fsub) => (true, xs) :: collectQuantifiers(fsub)
      case Forall(xs, fsub) => (false, xs) :: collectQuantifiers(fsub)
369
      case BinOp(make, f1, f2) => {
Christian Müller's avatar
Christian Müller committed
370
371
        val q1 = collectQuantifiers(f1)
        val q2 = collectQuantifiers(f2)
372

Christian Müller's avatar
Christian Müller committed
373
        // Merge while trying to stay in BS, if possible
374
        // TODO: could be improved to minimize quantifier alternations)
Christian Müller's avatar
Christian Müller committed
375
        // TODO: merge universals with same type by renaming
376
377
        val ex1 = q1.takeWhile(_._1)
        val rest1 = q1.drop(ex1.size)
Christian Müller's avatar
Christian Müller committed
378

Christian Müller's avatar
Christian Müller committed
379
380
381
        // filter out same bound variables (TODO: could be improved if different names)
        val existbound = ex1.flatMap(_._2)
        val univbound = rest1.flatMap(_._2)
Christian Müller's avatar
Christian Müller committed
382

Christian Müller's avatar
Christian Müller committed
383
384
        val exset = existbound.toSet
        val univset = univbound.toSet
Christian Müller's avatar
Christian Müller committed
385

Christian Müller's avatar
Christian Müller committed
386
        val ex2 = q2.takeWhile(_._1).map(q =>
Christian Müller's avatar
Christian Müller committed
387
          (q._1, q._2.filterNot(exset.contains)))
Christian Müller's avatar
Christian Müller committed
388
        val rest2 = q2.drop(ex2.size).map(q =>
Christian Müller's avatar
Christian Müller committed
389
          (q._1, q._2.filterNot(univset.contains)))
390
        ex1 ++ ex2 ++ rest1 ++ rest2
Christian Müller's avatar
Christian Müller committed
391
392
      }
    }
393
  }
Christian Müller's avatar
Christian Müller committed
394
395
396
397
398
399
400

  def checkBindings(f: Formula) = {
    def checkBindingsSub(f: Formula, bound: Set[Var]): List[Var] = {
      f collect {
        case Quantifier(make, xs, inner) => {
          val conflicts = xs.filter(bound.contains)
          conflicts ++ checkBindingsSub(inner, bound ++ xs)
Christian Müller's avatar
Christian Müller committed
401
        }
Christian Müller's avatar
Christian Müller committed
402
      }
Christian Müller's avatar
Christian Müller committed
403
404
    }
    checkBindingsSub(f, Set()).isEmpty
405
  }
Christian Müller's avatar
Christian Müller committed
406
407

  def isBS(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
408
409
410
411
412
413
    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)
    }
414
  }
Christian Müller's avatar
Christian Müller committed
415

Christian Müller's avatar
Christian Müller committed
416
417
  def isQFree(formula: Formula): Boolean = {
    !formula.hasSubFormula {
Christian Müller's avatar
Christian Müller committed
418
      case q: Quantifier => true
Christian Müller's avatar
Christian Müller committed
419
420
421
    }
  }

Christian Müller's avatar
Christian Müller committed
422
  def toNegNf(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
423
424
425
426
    //    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
427
    val noeq = eliminateEq(f)
Christian Müller's avatar
testing    
Christian Müller committed
428
    eliminateImplication(noeq).simplify()
429
430
431
432
433
434
435
436
437
  }

  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
438
    }
439
440
441
442
443
444
445
446
447
448
449
450
    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
451
      }
452
453
454
455
456
457
      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
458
        val alreadybounds = vars.filter(bound.contains)
459
460
461
462
463
464
465
466
467
468
        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
469
    }
470
471
  }

Christian Müller's avatar
Christian Müller committed
472
  // TODO: make sure no quantifiers in scope of others with same name
Christian Müller's avatar
Christian Müller committed
473
  def toPrenex(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
474
    val negnf = f.toNegNf
Christian Müller's avatar
Christian Müller committed
475
    //    val (simp, boundVars) = fixBinding(negnf, Set())
476

Christian Müller's avatar
Christian Müller committed
477
    // Simplify first to push negation inward
Christian Müller's avatar
Christian Müller committed
478
479
    val quants = collectQuantifiers(negnf)
    val stripped = stripQuantifiers(negnf)
480

Christian Müller's avatar
Christian Müller committed
481
482
    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
483
    }).simplify()
Christian Müller's avatar
Christian Müller committed
484
  }
Christian Müller's avatar
Christian Müller committed
485

Christian Müller's avatar
Christian Müller committed
486
  def toCNFClauses(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
487
    @tailrec
Christian Müller's avatar
Christian Müller committed
488
    def toCNFSub(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
489
      val (changed, sub) = everywhereFP({
Christian Müller's avatar
Christian Müller committed
490
491
        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
492
493
      }, f)
      if (!changed) sub else toCNFSub(sub)
Christian Müller's avatar
Christian Müller committed
494
495
496
    }

    // FIXME: can we do it without prenex? may be expensive later on
Christian Müller's avatar
Christian Müller committed
497
    val normalized = f.toNegNf.toPrenex.simplify()
Christian Müller's avatar
Christian Müller committed
498
499

    // normalized is now Quantifiers, then only And/Or with Negation inside
Christian Müller's avatar
Christian Müller committed
500
    // no simplification here
501
502
503
504
505
    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
506

507
    val quantifiers = FormulaFunctions.collectQuantifiers(cnf1)
Christian Müller's avatar
Christian Müller committed
508

Christian Müller's avatar
Christian Müller committed
509
    // Inspect clauses
510
    val clauses = FOTransformers.collectClauses(cnf1)
Christian Müller's avatar
Christian Müller committed
511
512
513
514
515
516
517
518
519
520
521

    // TODO: improve, don't sort by tostring
    val sorted = clauses.map(c => c.sortBy(_.toString())).sortBy(f => f.toString())

    logger.debug(s"Computing CNF of a formula with ${sorted.size} clauses")

    // Remove trivial clauses
    val notrivials = sorted.filterNot(c => {
      c.exists(f => c.contains(Neg(f)))
    })

Christian Müller's avatar
Christian Müller committed
522
    // TODO improve runtime
Christian Müller's avatar
Christian Müller committed
523
    val simped = notrivials.filterNot(c => notrivials.exists(c2 => {
Christian Müller's avatar
Christian Müller committed
524
      // check if c is superset of c2
Christian Müller's avatar
Christian Müller committed
525
526
      //      c != c2 && c.startsWith(c2)
      c != c2 && c.forall(f => c2.contains(f))
Christian Müller's avatar
Christian Müller committed
527
    }))
Christian Müller's avatar
Christian Müller committed
528
529
530
    logger.debug(s"After simplification ${simped.size} unsubsumed clauses remaining.")

    (quantifiers, simped)
Christian Müller's avatar
Christian Müller committed
531
  }
Christian Müller's avatar
Christian Müller committed
532
533
534

  def toCNF(f: Formula) = {
    val (quantifiers, clauses) = toCNFClauses(f)
Christian Müller's avatar
Christian Müller committed
535
    val form = And.make(clauses.map(Or.make))
Christian Müller's avatar
Christian Müller committed
536
    val newform = quantifiers.foldRight(form)((q, inner) => if (q._1) Exists(q._2, inner) else Forall(q._2, inner))
Christian Müller's avatar
Christian Müller committed
537
    newform
Christian Müller's avatar
Christian Müller committed
538
  }
Christian Müller's avatar
Christian Müller committed
539

Christian Müller's avatar
Christian Müller committed
540
541
542
543
  /**
   * Resolves a universally quantified predicate
   * Blows up the formula linearly due to CNF
   */
Christian Müller's avatar
Christian Müller committed
544
545
  def eliminatePredicate(f: Formula, name: String) = {
    def listFunsWithName(f: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
546
      f.collect({
Christian Müller's avatar
Christian Müller committed
547
        case Fun(n, ind, vars) if n == name      => List((Some(Fun(n, ind, vars)), None))
Christian Müller's avatar
Christian Müller committed
548
549
550
        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
551

Christian Müller's avatar
Christian Müller committed
552
    val norm = f.toCNF
Christian Müller's avatar
Christian Müller committed
553

Christian Müller's avatar
Christian Müller committed
554
555
    val removed = norm.everywhere({
      // find top-level ORs in CNF
Christian Müller's avatar
Christian Müller committed
556
      case inner: Or => {
Christian Müller's avatar
Christian Müller committed
557
        val list = listFunsWithName(inner, name)
Christian Müller's avatar
Christian Müller committed
558

Christian Müller's avatar
Christian Müller committed
559
560
        val positives = list.flatMap(_._1)
        val negatives = list.flatMap(_._2)
Christian Müller's avatar
Christian Müller committed
561
562

        val isSuperFluous = positives.exists { f1 =>
Christian Müller's avatar
Christian Müller committed
563
          negatives.contains(Neg(f1))
Christian Müller's avatar
Christian Müller committed
564
        }
Christian Müller's avatar
Christian Müller committed
565

Christian Müller's avatar
Christian Müller committed
566
567
568
569
570
        if (isSuperFluous) {
          // Remove clause
          True
        } else {
          // Remove predicate both in positive and negative
Christian Müller's avatar
Christian Müller committed
571
          inner.everywhere({
Christian Müller's avatar
Christian Müller committed
572
            case Neg(Fun(n, ind, vars)) if n == name => False
Christian Müller's avatar
Christian Müller committed
573
            case Fun(n, ind, vars) if n == name      => False
Christian Müller's avatar
Christian Müller committed
574
575
576
577
          })
        }
      }
    })
Christian Müller's avatar
Christian Müller committed
578

Christian Müller's avatar
Christian Müller committed
579
    removed.simplify()
Christian Müller's avatar
Christian Müller committed
580

Christian Müller's avatar
Christian Müller committed
581
  }
Christian Müller's avatar
Christian Müller committed
582
}