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

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

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

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

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

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

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


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

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

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

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

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

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

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

97
98
99
100
      // Equality =
      case Equal(t1, t2) if t1 == t2 => True
      case Equal(v1:Var, v2:Var) if v1.name > v2.name => Equal(v2, v1)

101
      // Double Temporals
Christian Müller's avatar
Christian Müller committed
102
103
      case Finally(Finally(t)) => Finally(t)
      case Globally(Globally(t)) => Globally(t)
Christian Müller's avatar
Christian Müller committed
104
105

      // Remove quantifiers if empty
106
      case Quantifier(_, xs, t) if xs.isEmpty => t
Christian Müller's avatar
Christian Müller committed
107
108
109
      case Quantifier(_, _, True) => True
      case Quantifier(_, _, False) => False

Christian Müller's avatar
Christian Müller committed
110
      // Quantifiers binding same things
111
112
113
114
      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))
115

Christian Müller's avatar
Christian Müller committed
116
      // Gobble up equal quantifiers
117
118
      case Forall(vars1, Forall(vars2, t)) => Forall(vars1 ++ vars2, t)
      case Exists(vars1, Exists(vars2, t)) => Exists(vars1 ++ vars2, t)
119

Christian Müller's avatar
Christian Müller committed
120
      // Remove variables from quantifiers if not used in the body
Christian Müller's avatar
src    
Christian Müller committed
121
122
      case Quantifier(qmake, xs, t) if (xs.toSet -- t.freeVars).nonEmpty =>
        qmake(xs.toSet.intersect(t.freeVars).toList, t)
Christian Müller's avatar
Christian Müller committed
123
124
125
126
127
128
      //
      //      // 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
129
130

      // Declass seen often enough
131
      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
132
133
    }

Christian Müller's avatar
Christian Müller committed
134
135
    //    val (changed, t1) = everywhereFP(simp, t)
    //    if (!changed) t1 else simplify(t1)
136
    everywhereBotUp(simp, f)
Christian Müller's avatar
Christian Müller committed
137
  }
138

Christian Müller's avatar
src    
Christian Müller committed
139
140
141
142
143
144
145
146
147
148
  def pushUniversalQuantifiers(f: Formula): Formula = {
    def push(f:Formula):Formula = {

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

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

Christian Müller's avatar
Christian Müller committed
171
  def eliminateImplication(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
172
    f everywhere {
Christian Müller's avatar
testing    
Christian Müller committed
173
174
175
      case Implies(f1, f2) => Or(Neg(eliminateImplication(f1)), eliminateImplication(f2))
    }
  }
Christian Müller's avatar
Christian Müller committed
176
177

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

Christian Müller's avatar
Christian Müller committed
188
189
190
191
192
193
  def everywhereFP(trans: PartialFunction[Formula, Formula], t: Formula): (Boolean, Formula) = {
    if (trans.isDefinedAt(t))
      (true, trans(t))
    else
      t match {
        // Extractors
194
        case Quantifier(make, ps, t1) =>
Christian Müller's avatar
Christian Müller committed
195
196
          val sub = everywhereFP(trans, t1)
          (sub._1, make(ps, sub._2))
197
        case UnOp(make, t1) =>
Christian Müller's avatar
Christian Müller committed
198
199
          val sub = everywhereFP(trans, t1)
          (sub._1, make(sub._2))
200
        case BinOp(make, t1, t2) =>
Christian Müller's avatar
Christian Müller committed
201
202
203
          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
204
        case x => (false, x)
Christian Müller's avatar
Christian Müller committed
205
206
      }
  }
Christian Müller's avatar
Christian Müller committed
207

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

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

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

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

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

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

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

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

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

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

315
  def removeAnnotation(t:Formula, Funname:String): Formula = {
Christian Müller's avatar
Christian Müller committed
316
317
318
319
320
    t.everywhere({
      case Fun(Funname, _, xs) => Fun(Funname, None, xs)
    })
  }

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

327
  def annotate(t: Formula, name: String, ignore: Set[String]): Formula = {
328
    t.everywhere({
329
      case Fun(f, None, xs) if !(ignore contains f) => Fun(f, Some(name), xs)
330
331
    })
  }
332

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

Christian Müller's avatar
Christian Müller committed
341
342
    frees.isEmpty
  }
Christian Müller's avatar
Christian Müller committed
343
344

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

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

Christian Müller's avatar
Christian Müller committed
358
359
    parallelRename(f, repls)
  }
Christian Müller's avatar
Christian Müller committed
360
361
362

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

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

378
379
380
  def stripQuantifiers(f: Formula): Formula = {
    f everywhere {
      case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
Christian Müller's avatar
Christian Müller committed
381
    }
382
  }
Christian Müller's avatar
Christian Müller committed
383

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

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

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

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

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

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

428
  def isBS(f: Formula): Boolean = {
Christian Müller's avatar
Christian Müller committed
429
430
431
432
433
434
    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)
    }
435
  }
Christian Müller's avatar
Christian Müller committed
436

Christian Müller's avatar
src    
Christian Müller committed
437
438
  def isU(formula:Formula): Boolean = {
    !formula.toNegNf.hasSubFormula {
439
      case _:Exists => true
Christian Müller's avatar
src    
Christian Müller committed
440
441
442
    }
  }

Christian Müller's avatar
Christian Müller committed
443
444
  def isQFree(formula: Formula): Boolean = {
    !formula.hasSubFormula {
445
      case _: Quantifier => true
Christian Müller's avatar
Christian Müller committed
446
447
448
    }
  }

449
  def toNegNf(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
450
451
452
453
    //    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
454
    val noeq = eliminateEq(f)
Christian Müller's avatar
Christian Müller committed
455
    eliminateImplication(noeq).simplify
456
457
  }

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

460
    val chars = base.name.toCharArray
461
462
463
464
    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
465
    }
466
467
468
469
470
471
472
    val stream = Stream.from(start)

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

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

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

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

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


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

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

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

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

Christian Müller's avatar
Christian Müller committed
553
554
    val simp = fixBinding(negnf)
//    val simp = negnf
555

Christian Müller's avatar
Christian Müller committed
556
    // Simplify first to push negation inward
Christian Müller's avatar
Christian Müller committed
557
    val quantifiers = collectQuantifiers(simp)
Christian Müller's avatar
src    
Christian Müller committed
558
    val stripped = stripQuantifiers(simp)
559

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

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

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

580
  def toCNFClauses(f: Formula): (List[(Boolean, List[Var])], List[List[Formula]]) = {
Christian Müller's avatar
Christian Müller committed
581
    @tailrec
Christian Müller's avatar
Christian Müller committed
582
    def toCNFSub(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
583
      val (changed, sub) = everywhereFP({
Christian Müller's avatar
Christian Müller committed
584
585
        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
586
587
      }, f)
      if (!changed) sub else toCNFSub(sub)
Christian Müller's avatar
Christian Müller committed
588
589
    }

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

Christian Müller's avatar
Christian Müller committed
595
596
    val normalized = f.toPrenex.simplify
    logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
Christian Müller's avatar
Christian Müller committed
597

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

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

Christian Müller's avatar
Christian Müller committed
604
605
    // Inspect clauses
    val clauses = FOTransformers.collectClauses(cnf1)
Christian Müller's avatar
Christian Müller committed
606

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

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

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

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

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

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

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

    (quantifiers, dnfclauses)
  }

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

Christian Müller's avatar
Christian Müller committed
655
656
  /**
   * Resolves a universally quantified predicate
Christian Müller's avatar
src    
Christian Müller committed
657
   * Blows up the formula exponentially due to CNF
Christian Müller's avatar
Christian Müller committed
658
   */
659
  def eliminatePredicate(f: Formula, name: String): Formula = {
Christian Müller's avatar
Christian Müller committed
660
    def listFunsWithName(f: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
661
      f.collect({
Christian Müller's avatar
Christian Müller committed
662
        case Fun(n, ind, vars) if n == name      => List((Some(Fun(n, ind, vars)), None))
Christian Müller's avatar
Christian Müller committed
663
664
665
        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
666

Christian Müller's avatar
Christian Müller committed
667
    val norm = f.toCNF
Christian Müller's avatar
Christian Müller committed
668

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

Christian Müller's avatar
Christian Müller committed
674
675
        val positives = list.flatMap(_._1)
        val negatives = list.flatMap(_._2)
Christian Müller's avatar
Christian Müller committed
676
677

        val isSuperFluous = positives.exists { f1 =>
Christian Müller's avatar
Christian Müller committed
678
          negatives.contains(Neg(f1))
Christian Müller's avatar
Christian Müller committed
679
        }
Christian Müller's avatar
Christian Müller committed
680

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

Christian Müller's avatar
Christian Müller committed
693
    removed.simplify
Christian Müller's avatar
Christian Müller committed
694

Christian Müller's avatar
Christian Müller committed
695
  }
Christian Müller's avatar
Christian Müller committed
696

Christian Müller's avatar
Christian Müller committed
697
698
  // matches positive arguments of the function with the correct annotation
  def getPositiveArguments(clause: List[Formula], NAME:String, ANNOTATION:Option[String] = None):Set[List[Var]] = {
Christian Müller's avatar
Christian Müller committed
699
    clause flatMap {
Christian Müller's avatar
Christian Müller committed
700
      case Fun(NAME, ANNOTATION, vars) => List(vars)
Christian Müller's avatar
Christian Müller committed
701
702
703
      case _ => List()
    } toSet
  }
Christian Müller's avatar
Christian Müller committed
704
  def getNegativeArguments(clause: List[Formula], NAME:String, ANNOTATION:Option[String] = None):Set[List[Var]] = {
Christian Müller's avatar
Christian Müller committed
705
    clause flatMap {
Christian Müller's avatar
Christian Müller committed
706
      case Neg(Fun(NAME, ANNOTATION, vars))=> List(vars)
Christian Müller's avatar
Christian Müller committed
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
      case _ => List()
    } toSet
  }
  def ineq(l1:List[Var], l2:List[Var]): Formula = {
    if (l1.size != l2.size) {
      logger.warn("Trying to generate inequalities for different sized vectors")
    }
    val ineqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
      case (x, y) if x.name <= y.name => Neg(Equal(x,y))
      case (x, y)  => Neg(Equal(y,x))
    }.toSet
    Or.make(ineqs.toList)
  }
  def eq(l1:List[Var], l2:List[Var]):Formula = {
    if (l1.size != l2.size) {
      logger.warn("Trying to generate equalities for different sized vectors")
    }
    val eqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
      case (x, y) if x.name <= y.name => Equal(x,y)
      case (x, y)  => Equal(y,x)
    }.toSet
    And.make(eqs.toList)
  }
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756

  def simplifyInequalitiesFromCNFClause(univ:List[Var], clause:Formula): Formula = {

    @tailrec
    def simp(f: Formula): Formula = {
      // get equalities - second is always universally quantified
      val ineqs = f.collect {
        case Neg(Equal(v1: Var, v2: Var)) if univ.contains(v1) => List((v2, v1))
        case Neg(Equal(v1: Var, v2: Var)) if univ.contains(v2) => List((v1, v2))
      }

      if (ineqs.nonEmpty) {
        // pick the first one, replace v2 by v1
        val (v1, v2) = ineqs.head
        val repl = f.parallelRename(List(v2), List(v1))

        // after renaming, remove the inequalities
        val withouteq = repl.simplify
        // continue
        simp(withouteq)
      } else {
        f
      }
    }

    simp(clause)
  }
Christian Müller's avatar
Christian Müller committed
757
}