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

import com.typesafe.scalalogging.LazyLogging
4 5
import de.tum.niwo.Utils
import de.tum.niwo.foltl.FOLTL._
6
import de.tum.niwo.invariants.InvProperties
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
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
      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")
        }
Christian Müller's avatar
Christian Müller committed
75 76

        // TODO: add substitution for equalities
Christian Müller's avatar
Christian Müller committed
77 78 79 80 81 82 83
        clause ++ eqs
      }

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

    } else {
Christian Müller's avatar
Christian Müller committed
84
      logger.debug(s"Approximating elimination of universal second order predicate $AUX, not computing CNF")
Christian Müller's avatar
Christian Müller committed
85 86 87 88 89
      // Saturated formula, no equalities anywhere
      f
    }

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

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

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

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

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

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

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

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

    def pruneBs(clause: List[Formula]) = {
122
      clause filterNot {
Christian Müller's avatar
ineq  
Christian Müller committed
123 124
        case Neg(Fun(NAME, _, _)) => true
        case Fun(NAME, _, _) => true
Christian Müller's avatar
src  
Christian Müller committed
125 126 127 128 129 130
        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
131
    //  F \/ B z_1 ... B z_r
Christian Müller's avatar
Christian Müller committed
132
    val Fargs = F.map(positiveBArguments)
Christian Müller's avatar
Christian Müller committed
133

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

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

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

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

    val fE = And.make(E.map(c => Or.make(pruneBs(c))))
149 150 151 152 153
    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
154
      Or.make(fi, gk, FormulaFunctions.ineq(farg, garg))
155 156 157 158 159
    }
    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
Christian Müller committed
160 161
//      Or.make(hl, gk, ineq(harg, garg))
      Or.make(hl, gk).parallelRename(harg, garg)
162 163 164 165 166
    }
    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
167
    val felimq = FormulaFunctions.rewrapQuantifiers(quantifiers, felim)
Christian Müller's avatar
ineq  
Christian Müller committed
168 169 170 171

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

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

177 178 179 180 181
    // 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
182
    val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
183

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

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

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

  // Instantiate all universals in a E*A* formula
225
  def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
Christian Müller's avatar
Christian Müller committed
226
    
Christian Müller's avatar
Christian Müller committed
227 228 229
//    if (agents.isEmpty) {
//      logger.warn("Agent list empty")
//    }
Christian Müller's avatar
Christian Müller committed
230
    val universe = agents.groupBy(_.typ)
Christian Müller's avatar
Christian Müller committed
231
    
232
    def instantiate(tup:List[Var],t:Formula,universe:Map[String,List[FOLTL.Var]]) = {
Christian Müller's avatar
Christian Müller committed
233 234
      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
235
//        logger.warn(s"Ignored ${Forall(tup, t)} (empty universe for at least one type)")
Christian Müller's avatar
Christian Müller committed
236 237 238 239 240 241 242 243 244
        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
Christian Müller committed
245
            case v:Var => mapping.getOrElse(v,v)
Christian Müller's avatar
Christian Müller committed
246 247 248 249 250 251
          })
        }
        eliminateUniversals(And.make(terms), agents)
      }
    }
    
Christian Müller's avatar
Christian Müller committed
252
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
253 254 255
        case Exists(tup, term) => {
          Exists(tup, eliminateUniversals(term, agents ++ tup))
        }
Christian Müller's avatar
Christian Müller committed
256
        case Forall(tup, term) => {
Christian Müller's avatar
Christian Müller committed
257 258 259 260 261 262 263
          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
264 265 266
        }
    })
  }
Christian Müller's avatar
Christian Müller committed
267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313

  def eliminateQuantifiers(t:Formula, universe:Map[String,List[FOLTL.Var]]):Formula = {

    def instantiateE(tup:List[Var],t:Formula) = {
      if (!tup.forall(v => universe.contains(v.typ))) {
        False
      } 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, vars) => Fun(f, id, vars.map(a => mapping.getOrElse(a, a)))
            case v: Var => mapping.getOrElse(v, v)
          })
        }
        eliminateQuantifiers(Or.make(terms), universe)
      }
    }


    def instantiateA(tup:List[Var],t:Formula) = {
      if (!tup.forall(v => universe.contains(v.typ))) {
        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, vars) => Fun(f, id, vars.map(a => mapping.getOrElse(a, a)))
            case v: Var => mapping.getOrElse(v, v)
          })
        }
        eliminateQuantifiers(And.make(terms), universe)
      }
    }

    t everywhere {
      case Exists(tup, term) =>
        instantiateE(tup, term)
      case Forall(tup, term) =>
        instantiateA(tup, term)
    }
  }
Christian Müller's avatar
Christian Müller committed
314
  
315
  /**
Christian Müller's avatar
Christian Müller committed
316
   * Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x")
317
   */
Christian Müller's avatar
Christian Müller committed
318
  def eliminatePredicates(t: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
319
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
320
      case f:Fun => f.encodeToVar()
Christian Müller's avatar
Christian Müller committed
321 322 323
    })
  }
  
324 325
  /**
   * Instantiates universals in EA formulae.
Christian Müller's avatar
Christian Müller committed
326
   * Resulting formula is in E* with all existentials outermost and in NegNF
327
   */
Christian Müller's avatar
Christian Müller committed
328
  def instantiateUniversals(f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
329

330
    // Check fragment
Christian Müller's avatar
Christian Müller committed
331
    if (!f.isBS) {
332 333 334 335
      logger.error("Trying to instantiate Universals for wrong fragment")
      logger.error(s"Formula was $f")
    }
    
Christian Müller's avatar
Christian Müller committed
336
    val nf = f.toNegNf
Christian Müller's avatar
Christian Müller committed
337
    val (agents, inner) = FOTransformers.eliminateExistentials(nf)
338
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
339
    val constants = existbound.freeVars
Christian Müller's avatar
Christian Müller committed
340 341
    
    FOTransformers.eliminateUniversals(existbound, constants.toList)    
342 343 344
  }
  
  /**
Christian Müller's avatar
Christian Müller committed
345 346
   * Instantiates existentials in AE formulae.
   * Resulting formula is in NegNF
347
   */
Christian Müller's avatar
Christian Müller committed
348
  def abstractExistentials(f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
349
    val neg = Neg(f).toNegNf.simplify
Christian Müller's avatar
Christian Müller committed
350 351
    
    // Check fragment
Christian Müller's avatar
Christian Müller committed
352
    if (!neg.isBS) {
Christian Müller's avatar
Christian Müller committed
353 354
      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
355
    }
356
    
Christian Müller's avatar
Christian Müller committed
357 358
    val (agents, inner) = FOTransformers.eliminateExistentials(neg)
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
359
    val constants = neg.freeVars
Christian Müller's avatar
Christian Müller committed
360
    val res = FOTransformers.eliminateUniversals(existbound, constants.toList)
Christian Müller's avatar
Christian Müller committed
361
    Neg(res).simplify
362
  }
Christian Müller's avatar
Christian Müller committed
363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378

  /**
    * 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
379
    val neg = Neg(f).simplify
Christian Müller's avatar
Christian Müller committed
380 381
    val constants = neg.freeVars ++ universe
    val res = FOTransformers.eliminateUniversals(neg, constants.toList)
Christian Müller's avatar
Christian Müller committed
382
    Neg(res).simplify
Christian Müller's avatar
Christian Müller committed
383
  }
Christian Müller's avatar
Christian Müller committed
384
}