FOTransformers.scala 10.8 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 com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
4
5
import de.tum.niwo.Utils
import de.tum.niwo.foltl.FOLTL._
6
import de.tum.niwo.invariants.InvProperties
Christian Müller's avatar
Christian Müller committed
7
import de.tum.niwo.toz3.Z3BSFO
Christian Müller's avatar
Christian Müller committed
8

Christian Müller's avatar
Christian Müller committed
9
object FOTransformers extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
10
  
Christian Müller's avatar
Christian Müller committed
11
  // Computes all possible tuples of signature types
Christian Müller's avatar
Christian Müller committed
12
13
14
15
16
17
  def comb[T](types:List[String], universe:Map[String, List[T]]):List[List[T]] = {
    types match {
      case List() => List(List())
      case t :: ts => {
        val subres = comb(ts, universe)
        if (!universe.isDefinedAt(t)) {
Christian Müller's avatar
Christian Müller committed
18
          logger.error(s"No variable for type $t in the universe.")
Christian Müller's avatar
Christian Müller committed
19
        }
Christian Müller's avatar
Christian Müller committed
20

Christian Müller's avatar
Christian Müller committed
21
22
        for (a <- universe(t); s <- subres) yield {
          a :: s
Christian Müller's avatar
Christian Müller committed
23
24
25
26
27
        }
      }
    }
  }
  
Christian Müller's avatar
Christian Müller committed
28
29
  def collectClauses(f:Formula):List[List[Formula]] = {
    def collectClause(f:Formula):List[Formula] = f collect {
Christian Müller's avatar
leaders    
Christian Müller committed
30
      case t:Equal => List(t)
Christian Müller's avatar
Christian Müller committed
31
32
33
34
35
36
37
38
      case t:Var => List(t)
      case t:Neg => List(t)
      case t:Fun => List(t)
      case Or(f1, f2) => collectClause(f1) ++ collectClause(f2)
    }
    
    def collectMultiClause(f:Formula):List[List[Formula]] = f collect {
      case And(t1, t2) => collectMultiClause(t1) ++ collectMultiClause(t2)
Christian Müller's avatar
Christian Müller committed
39
40
      case Quantifier(vars, make, t) => collectMultiClause(t)
      case t => List(collectClause(t))
Christian Müller's avatar
Christian Müller committed
41
    }
Christian Müller's avatar
Christian Müller committed
42
43
44
45
46
    f match {
      case True => List()
      case False => List(List())
      case _ => collectMultiClause(f)
    }
Christian Müller's avatar
Christian Müller committed
47
48
  }
  
Christian Müller's avatar
Christian Müller committed
49
  def eliminateDoubleQuantifiers(f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
50
51
52
53
54
55
    def elimSub(f:Formula, bound:Set[Var]):Formula = {
      f everywhere {
        // filter out all that are contained in bound
        case Quantifier(make, vars, inner) => make(vars.filterNot(bound.contains).distinct, elimSub(inner, bound ++ vars))
      }
    }
Christian Müller's avatar
Christian Müller committed
56
    elimSub(f.toNegNf, Set())
Christian Müller's avatar
Christian Müller committed
57
58
  }
  
Christian Müller's avatar
Christian Müller committed
59
  def eliminateAuxiliaryPredicate(f:Formula, AUX:String, props:InvProperties): Formula = {
Christian Müller's avatar
src    
Christian Müller committed
60

Christian Müller's avatar
Christian Müller committed
61
62
63
    val result = if (!props.approxElim || f.opsize < Utils.APPROXELIM_MINSIZE) {
      logger.debug(s"Eliminating universal second order predicate $AUX")
      val (quants, clauses) = FormulaFunctions.toCNFClauses(f)
Christian Müller's avatar
Christian Müller committed
64

Christian Müller's avatar
Christian Müller committed
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
      val updatedclauses = for (clause <- clauses) yield {
        val eqs = for (
          trace <- List(None, Some(Properties.T1), Some(Properties.T2));
          pos <- FormulaFunctions.getPositiveArguments(clause, AUX, trace);
          neg <- FormulaFunctions.getNegativeArguments(clause, AUX, trace)) yield {
          FormulaFunctions.eq(pos, neg)
        }
        if (eqs.nonEmpty) {
          logger.trace(s"Introducing equalities while eliminating $AUX")
        }
        clause ++ eqs
      }

      val updatedcnf = And.make(updatedclauses.map(Or.make))
      FormulaFunctions.rewrapQuantifiers(quants, updatedcnf)

    } else {
      logger.debug(s"Approximating elimination of universal second order predicate $AUX")
      // Saturated formula, no equalities anywhere
      f
    }

    val repld = result everywhere {
Christian Müller's avatar
Christian Müller committed
88
89
90
      case Neg(Fun(AUX, _, _)) => False
      case Fun(AUX, _, _) => False
    }
Christian Müller's avatar
Christian Müller committed
91
    repld.simplify
Christian Müller's avatar
src    
Christian Müller committed
92
93
  }

Christian Müller's avatar
Christian Müller committed
94
  def eliminateBPredicate(f:Formula, B:Fun): (Formula, Formula) = {
Christian Müller's avatar
Christian Müller committed
95
    val NAME = B.name
Christian Müller's avatar
ineq    
Christian Müller committed
96

Christian Müller's avatar
src    
Christian Müller committed
97
    // SOQE: \exists B. f <-> f'
Christian Müller's avatar
Christian Müller committed
98
    logger.debug(s"Eliminating existential second order predicate $B")
Christian Müller's avatar
src    
Christian Müller committed
99
100
101
102

    if (!f.isUniversal) {
      logger.error("Trying to use SOQE on a non-universal formula")
    }
Christian Müller's avatar
Christian Müller committed
103
    // This sets B(T1) and B(T2) to be the same relation
Christian Müller's avatar
Christian Müller committed
104
    // Use the best available simplification
Christian Müller's avatar
ineq    
Christian Müller committed
105
    val noannotation = Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, NAME))
Christian Müller's avatar
src    
Christian Müller committed
106

Christian Müller's avatar
Christian Müller committed
107
    val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(noannotation)
Christian Müller's avatar
src    
Christian Müller committed
108
109

    // Group clauses by positive/negative occurences
Christian Müller's avatar
Christian Müller committed
110
111
    val positiveBArguments = FormulaFunctions.getPositiveArguments(_, NAME, None)
    val negativeBArguments = FormulaFunctions.getNegativeArguments(_, NAME, None)
Christian Müller's avatar
Christian Müller committed
112

Christian Müller's avatar
src    
Christian Müller committed
113
    def ispositive(clause: List[Formula]) =
Christian Müller's avatar
Christian Müller committed
114
      positiveBArguments(clause).nonEmpty
Christian Müller's avatar
Christian Müller committed
115

Christian Müller's avatar
src    
Christian Müller committed
116
    def isnegative(clause: List[Formula]) =
Christian Müller's avatar
Christian Müller committed
117
      negativeBArguments(clause).nonEmpty
Christian Müller's avatar
src    
Christian Müller committed
118
119

    def pruneBs(clause: List[Formula]) = {
Christian Müller's avatar
Christian Müller committed
120
      clause filterNot {
Christian Müller's avatar
ineq    
Christian Müller committed
121
122
        case Neg(Fun(NAME, _, _)) => true
        case Fun(NAME, _, _) => true
Christian Müller's avatar
src    
Christian Müller committed
123
124
125
126
127
128
        case _ => false
      }
    }

    val E = clauses.filter(c => !ispositive(c) && !isnegative(c))
    val F = clauses.filter(c => ispositive(c) && !isnegative(c))
Christian Müller's avatar
Christian Müller committed
129
    //  F \/ B z_1 ... B z_r
Christian Müller's avatar
Christian Müller committed
130
    val Fargs = F.map(positiveBArguments)
Christian Müller's avatar
Christian Müller committed
131

Christian Müller's avatar
src    
Christian Müller committed
132
    val G = clauses.filter(c => isnegative(c) && !ispositive(c))
Christian Müller's avatar
Christian Müller committed
133
    // G \/ !B z'_1 ... !B z'_j
Christian Müller's avatar
Christian Müller committed
134
    val Gargs = G.map(negativeBArguments)
Christian Müller's avatar
Christian Müller committed
135

Christian Müller's avatar
src    
Christian Müller committed
136
137
    val H = clauses.filter(c => ispositive(c) && isnegative(c))

Christian Müller's avatar
Christian Müller committed
138
    // H \/ B u_1 .. B u_l \/ !B v_1 ... ! B v_n
Christian Müller's avatar
Christian Müller committed
139
140
    val HPositiveargs = H.map(positiveBArguments)
    val HNegativeargs = H.map(negativeBArguments)
Christian Müller's avatar
Christian Müller committed
141

Christian Müller's avatar
src    
Christian Müller committed
142
    if (H.nonEmpty) {
Christian Müller's avatar
Christian Müller committed
143
      logger.debug("BSFO SOQE: H is not empty, Ackermann not applicable")
Christian Müller's avatar
src    
Christian Müller committed
144
145
146
    }

    val fE = And.make(E.map(c => Or.make(pruneBs(c))))
Christian Müller's avatar
Christian Müller committed
147
148
149
150
151
    val fis = F.map(c => Or.make(pruneBs(c)))
    val gks = G.map(c => Or.make(pruneBs(c)))
    val hls = H.map(c => Or.make(pruneBs(c)))

    val FGineq = for ((fi, fargs) <- fis.zip(Fargs); (gk, gargs) <- gks.zip(Gargs); farg <- gargs; garg <- gargs) yield {
Christian Müller's avatar
Christian Müller committed
152
      Or.make(fi, gk, FormulaFunctions.ineq(farg, garg))
Christian Müller's avatar
Christian Müller committed
153
154
155
156
157
    }
    val fFGineq = And.make(FGineq)
    val simpfFGineq = Z3BSFO.simplifyBS(fFGineq)  // FIXME: is this correct? there are no quantifiers binding stuff

    val GHineq = for ((hl, hargs) <- hls.zip(HPositiveargs); (gk, gargs) <- gks.zip(Gargs); harg <- hargs; garg <- gargs) yield {
Christian Müller's avatar
leaders    
Christian Müller committed
158
159
//      Or.make(hl, gk, ineq(harg, garg))
      Or.make(hl, gk).parallelRename(harg, garg)
Christian Müller's avatar
Christian Müller committed
160
161
162
163
164
    }
    val fGHineq = And.make(FGineq)
    val simpfGHineq = Z3BSFO.simplifyBS(fGHineq)

    val felim:Formula = fE land fFGineq land fGHineq
Christian Müller's avatar
Christian Müller committed
165
    val felimq = FormulaFunctions.rewrapQuantifiers(quantifiers, felim)
Christian Müller's avatar
ineq    
Christian Müller committed
166
167
168
169

    // Compute solution
    val bounds = gks.flatMap(_.freeVars) ++ gks.flatMap(_.boundVars)

Christian Müller's avatar
Christian Müller committed
170
    val freeparams = B.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
Christian Müller's avatar
ineq    
Christian Müller committed
171
    val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield {
172
      Or.make(gk, FormulaFunctions.ineq(garg, freeparams))
Christian Müller's avatar
ineq    
Christian Müller committed
173
    }
Christian Müller's avatar
leaders    
Christian Müller committed
174

175
176
177
178
179
    // Simplify equalities
    val boundvars = quantifiers.flatMap(_._2)
    val simpler = for (clause <- gkineq) yield FormulaFunctions.simplifyInequalitiesFromCNFClause(boundvars, clause)

    val fsol:Formula = And.make(simpler)
Christian Müller's avatar
Christian Müller committed
180
    val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
Christian Müller's avatar
Christian Müller committed
181

Christian Müller's avatar
src    
Christian Müller committed
182
    val z3fsolq = Z3BSFO.simplifyBS(fsolq)
Christian Müller's avatar
Christian Müller committed
183

Christian Müller's avatar
src    
Christian Müller committed
184
    if (Utils.DEBUG_MODE) {
Christian Müller's avatar
Christian Müller committed
185
      logger.info(s"BSFO SOQE: strategy for ${B.updatedParams(freeparams)}: $z3fsolq")
Christian Müller's avatar
src    
Christian Müller committed
186
187
    }

Christian Müller's avatar
Christian Müller committed
188
    (felimq, z3fsolq)
Christian Müller's avatar
Christian Müller committed
189
190
  }
  
Christian Müller's avatar
Christian Müller committed
191
192
193
194
  /**
   * Gobble up all outermost existential quantifiers
   * Needs to have non-conflicting bindings
   */
Christian Müller's avatar
Christian Müller committed
195
  def eliminateExistentials(t:Formula): (List[Var], Formula) = {
196
    
197
    def coll:PartialFunction[Formula, List[Var]] = {
Christian Müller's avatar
Christian Müller committed
198
      case Exists(a, term) => a ++ term.collect(coll)
199
200
      // don't go over Foralls
      case Forall(_, _) => List.empty
Christian Müller's avatar
Christian Müller committed
201
      case t:ForallOtherThan => List.empty
202
203
204
      // don't go over Globally
      case Globally(_) => List.empty
    }
Christian Müller's avatar
Christian Müller committed
205
206
    // TODO: this only works if the a's are not in scope of one another
    val agents = t.collect(coll).distinct
207
    
208
    def elim:PartialFunction[Formula, Formula] = {
209
210
211
      case Exists(a, term) => term.everywhere(elim)
      // don't go over Foralls
      case term:Forall => term
Christian Müller's avatar
Christian Müller committed
212
      case term:ForallOtherThan => term
213
214
215
216
217
218
219
220
      // don't go over Globally
      case term:Globally => term
    }
    
    val res = t.everywhere(elim)
    
    (agents, res)
  }
Christian Müller's avatar
Christian Müller committed
221
222

  // Instantiate all universals in a E*A* formula
223
  def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
Christian Müller's avatar
Christian Müller committed
224
    
Christian Müller's avatar
Christian Müller committed
225
226
227
//    if (agents.isEmpty) {
//      logger.warn("Agent list empty")
//    }
Christian Müller's avatar
Christian Müller committed
228
    val universe = agents.groupBy(_.typ)
Christian Müller's avatar
Christian Müller committed
229
    
230
    def instantiate(tup:List[Var],t:Formula,universe:Map[String,List[FOLTL.Var]]) = {
Christian Müller's avatar
Christian Müller committed
231
232
      if(!tup.forall(v => universe.contains(v.typ))) {
        // everything is valid for quantifiers over empty sets
Christian Müller's avatar
Christian Müller committed
233
//        logger.warn(s"Ignored ${Forall(tup, t)} (empty universe for at least one type)")
Christian Müller's avatar
Christian Müller committed
234
235
236
237
238
239
240
241
242
        True
      } else {
        val replacements = comb(tup.map(_.typ), universe)
        val terms = for (repl <- replacements) yield {
          val mapping = tup.zip(repl) toMap

          t.everywhere({
            // do replacement
            case Fun(f, id, tup) => Fun(f, id, tup.map(a => mapping.getOrElse(a, a)))
Christian Müller's avatar
leaders    
Christian Müller committed
243
            case v:Var => mapping.getOrElse(v,v)
Christian Müller's avatar
Christian Müller committed
244
245
246
247
248
249
          })
        }
        eliminateUniversals(And.make(terms), agents)
      }
    }
    
Christian Müller's avatar
Christian Müller committed
250
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
251
252
253
        case Exists(tup, term) => {
          Exists(tup, eliminateUniversals(term, agents ++ tup))
        }
Christian Müller's avatar
Christian Müller committed
254
        case Forall(tup, term) => {
Christian Müller's avatar
Christian Müller committed
255
256
257
258
259
260
261
          instantiate(tup, term, universe)
        }
        case ForallOtherThan(tup, otherthan, term) => {
          val smalleruniverse = universe.map(t => {
            (t._1, t._2.filterNot(otherthan.contains(_)))
          })
          instantiate(tup, term, smalleruniverse)
Christian Müller's avatar
Christian Müller committed
262
263
264
265
        }
    })
  }
  
Christian Müller's avatar
Christian Müller committed
266
  /**
Christian Müller's avatar
Christian Müller committed
267
   * Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x")
Christian Müller's avatar
Christian Müller committed
268
   */
Christian Müller's avatar
Christian Müller committed
269
  def eliminatePredicates(t: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
270
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
271
      case f:Fun => f.encodeToVar()
Christian Müller's avatar
Christian Müller committed
272
273
274
    })
  }
  
Christian Müller's avatar
Christian Müller committed
275
276
  /**
   * Instantiates universals in EA formulae.
Christian Müller's avatar
testing    
Christian Müller committed
277
   * Resulting formula is in E* with all existentials outermost and in NegNF
Christian Müller's avatar
Christian Müller committed
278
   */
Christian Müller's avatar
Christian Müller committed
279
  def instantiateUniversals(f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
280

Christian Müller's avatar
Christian Müller committed
281
    // Check fragment
Christian Müller's avatar
Christian Müller committed
282
    if (!f.isBS) {
Christian Müller's avatar
Christian Müller committed
283
284
285
286
      logger.error("Trying to instantiate Universals for wrong fragment")
      logger.error(s"Formula was $f")
    }
    
Christian Müller's avatar
Christian Müller committed
287
    val nf = f.toNegNf
Christian Müller's avatar
Christian Müller committed
288
    val (agents, inner) = FOTransformers.eliminateExistentials(nf)
Christian Müller's avatar
Christian Müller committed
289
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
290
    val constants = existbound.freeVars
Christian Müller's avatar
Christian Müller committed
291
292
    
    FOTransformers.eliminateUniversals(existbound, constants.toList)    
Christian Müller's avatar
Christian Müller committed
293
294
295
  }
  
  /**
Christian Müller's avatar
Christian Müller committed
296
297
   * Instantiates existentials in AE formulae.
   * Resulting formula is in NegNF
Christian Müller's avatar
Christian Müller committed
298
   */
Christian Müller's avatar
Christian Müller committed
299
  def abstractExistentials(f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
300
    val neg = Neg(f).toNegNf.simplify
Christian Müller's avatar
Christian Müller committed
301
302
    
    // Check fragment
Christian Müller's avatar
Christian Müller committed
303
    if (!neg.isBS) {
Christian Müller's avatar
Christian Müller committed
304
305
      logger.warn("Trying to instantiate Existentials for wrong fragment -- Termination not guaranteed")
//      logger.error(s"Formula was $f")
Christian Müller's avatar
Christian Müller committed
306
    }
Christian Müller's avatar
Christian Müller committed
307
    
Christian Müller's avatar
Christian Müller committed
308
309
    val (agents, inner) = FOTransformers.eliminateExistentials(neg)
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
310
    val constants = neg.freeVars
Christian Müller's avatar
Christian Müller committed
311
    val res = FOTransformers.eliminateUniversals(existbound, constants.toList)
Christian Müller's avatar
Christian Müller committed
312
    Neg(res).simplify
Christian Müller's avatar
Christian Müller committed
313
  }
Christian Müller's avatar
Christian Müller committed
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329

  /**
    * Instantiates existentials in E* formulas for a given universe to a disjunction

    * @param f Formula in E*
    * @param universe Set of variables
    * @return Formula without E
    */
  def instantiateExistentials(f:Formula, universe:Set[Var]): Formula = {

    if (f.hasSubFormula {
      case Forall(_, _) => true
    }) {
      logger.error("Trying to instantiate existentials for formula containing universals")
    }

Christian Müller's avatar
Christian Müller committed
330
    val neg = Neg(f).simplify
Christian Müller's avatar
Christian Müller committed
331
332
    val constants = neg.freeVars ++ universe
    val res = FOTransformers.eliminateUniversals(neg, constants.toList)
Christian Müller's avatar
Christian Müller committed
333
    Neg(res).simplify
Christian Müller's avatar
Christian Müller committed
334
  }
Christian Müller's avatar
Christian Müller committed
335
}