FormulaFunctions.scala 18.9 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
  def pushQuantifiers(f: Formula): Formula = {

    f everywhere {
      case Forall(vars, BinOp(make, f1, f2)) if {
Christian Müller's avatar
Christian Müller committed
126
127
        val leftvars = f1.freeVars
        val rightvars = f2.freeVars
Christian Müller's avatar
Christian Müller committed
128
129
130
131
132
        val varset = vars.toSet
        val onlyleft = leftvars.intersect(varset) -- rightvars
        val onlyright = rightvars.intersect(varset) -- leftvars
        !onlyleft.isEmpty || !onlyright.isEmpty
      } => {
Christian Müller's avatar
Christian Müller committed
133
134
        val leftvars = f1.freeVars
        val rightvars = f2.freeVars
Christian Müller's avatar
Christian Müller committed
135
136
137
138
139
140
141
142
143
144
145
146
147
148
        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
    t match {
      // Extractors
Christian Müller's avatar
Christian Müller committed
224
225
226
      case Quantifier(_, ps, t) => 1 + t.opsize
      case UnOp(_, t)           => 1 + t.opsize
      case BinOp(_, t1, t2)     => 1 + t1.opsize + t2.opsize
227
228
229
      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
    // TODO add more things, f.e. existentials
    // T1, T2 can appear freely
Christian Müller's avatar
Christian Müller committed
310
    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

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

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

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

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

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

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

  def toCNF(f: Formula) = {
    val (quantifiers, clauses) = toCNFClauses(f)
Christian Müller's avatar
Christian Müller committed
537
    val form = And.make(clauses.map(Or.make))
Christian Müller's avatar
Christian Müller committed
538
    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
539
    newform
Christian Müller's avatar
Christian Müller committed
540
  }
Christian Müller's avatar
Christian Müller committed
541

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

Christian Müller's avatar
Christian Müller committed
554
    val norm = f.toCNF
Christian Müller's avatar
Christian Müller committed
555

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

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

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

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

Christian Müller's avatar
Christian Müller committed
581
    removed.simplify()
Christian Müller's avatar
Christian Müller committed
582

Christian Müller's avatar
Christian Müller committed
583
  }
Christian Müller's avatar
Christian Müller committed
584
}