FOTransformers.scala 9.98 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 = {
60
    logger.debug(s"Eliminating universal second order predicate $AUX")
Christian Müller's avatar
src  
Christian Müller committed
61

62
    val cnf = if (!props.approxElim) f.toCNF else f.toNegNf
Christian Müller's avatar
Christian Müller committed
63

Christian Müller's avatar
src  
Christian Müller committed
64
    val repld = cnf everywhere {
Christian Müller's avatar
Christian Müller committed
65 66 67
      case Neg(Fun(AUX, _, _)) => False
      case Fun(AUX, _, _) => False
    }
Christian Müller's avatar
Christian Müller committed
68
    repld.simplify
Christian Müller's avatar
src  
Christian Müller committed
69 70
  }

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

Christian Müller's avatar
src  
Christian Müller committed
74
    // SOQE: \exists B. f <-> f'
Christian Müller's avatar
Christian Müller committed
75
    logger.debug(s"Eliminating existential second order predicate $B")
Christian Müller's avatar
src  
Christian Müller committed
76 77 78 79

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

Christian Müller's avatar
Christian Müller committed
84
    val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(noannotation)
Christian Müller's avatar
src  
Christian Müller committed
85 86

    // Group clauses by positive/negative occurences
Christian Müller's avatar
Christian Müller committed
87 88 89
    val getPositiveBArguments = FormulaFunctions.getPositiveArguments(_, NAME)
    val getNegativeBArguments = FormulaFunctions.getNegativeArguments(_, NAME)

Christian Müller's avatar
src  
Christian Müller committed
90
    def ispositive(clause: List[Formula]) =
Christian Müller's avatar
Christian Müller committed
91 92
      getPositiveBArguments(clause).nonEmpty

Christian Müller's avatar
src  
Christian Müller committed
93
    def isnegative(clause: List[Formula]) =
Christian Müller's avatar
Christian Müller committed
94
      getNegativeBArguments(clause).nonEmpty
Christian Müller's avatar
src  
Christian Müller committed
95 96

    def pruneBs(clause: List[Formula]) = {
97
      clause filterNot {
Christian Müller's avatar
ineq  
Christian Müller committed
98 99
        case Neg(Fun(NAME, _, _)) => true
        case Fun(NAME, _, _) => true
Christian Müller's avatar
src  
Christian Müller committed
100 101 102 103 104 105
        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
106
    //  F \/ B z_1 ... B z_r
107
    val Fargs = F.map(getPositiveBArguments)
Christian Müller's avatar
Christian Müller committed
108

Christian Müller's avatar
src  
Christian Müller committed
109
    val G = clauses.filter(c => isnegative(c) && !ispositive(c))
Christian Müller's avatar
Christian Müller committed
110
    // G \/ !B z'_1 ... !B z'_j
111
    val Gargs = G.map(getNegativeBArguments)
Christian Müller's avatar
Christian Müller committed
112

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

Christian Müller's avatar
Christian Müller committed
115
    // H \/ B u_1 .. B u_l \/ !B v_1 ... ! B v_n
116 117
    val HPositiveargs = H.map(getPositiveBArguments)
    val HNegativeargs = H.map(getNegativeBArguments)
Christian Müller's avatar
Christian Müller committed
118

Christian Müller's avatar
src  
Christian Müller committed
119
    if (H.nonEmpty) {
Christian Müller's avatar
Christian Müller committed
120
      logger.debug("BSFO SOQE: H is not empty, Ackermann not applicable")
Christian Müller's avatar
src  
Christian Müller committed
121 122 123
    }

    val fE = And.make(E.map(c => Or.make(pruneBs(c))))
124 125 126 127 128
    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
129
      Or.make(fi, gk, FormulaFunctions.ineq(farg, garg))
130 131 132 133 134
    }
    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
135 136
//      Or.make(hl, gk, ineq(harg, garg))
      Or.make(hl, gk).parallelRename(harg, garg)
137 138 139 140 141
    }
    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
142
    val felimq = FormulaFunctions.rewrapQuantifiers(quantifiers, felim)
Christian Müller's avatar
ineq  
Christian Müller committed
143 144 145 146

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

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

152 153 154 155 156
    // 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
157
    val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
158

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

Christian Müller's avatar
src  
Christian Müller committed
161
    if (Utils.DEBUG_MODE) {
Christian Müller's avatar
Christian Müller committed
162
      logger.info(s"BSFO SOQE: strategy for ${B.updatedParams(freeparams)}: $z3fsolq")
Christian Müller's avatar
src  
Christian Müller committed
163 164
    }

165
    (felimq, z3fsolq)
Christian Müller's avatar
Christian Müller committed
166 167
  }
  
168 169 170 171
  /**
   * Gobble up all outermost existential quantifiers
   * Needs to have non-conflicting bindings
   */
Christian Müller's avatar
Christian Müller committed
172
  def eliminateExistentials(t:Formula): (List[Var], Formula) = {
173
    
174
    def coll:PartialFunction[Formula, List[Var]] = {
Christian Müller's avatar
Christian Müller committed
175
      case Exists(a, term) => a ++ term.collect(coll)
176 177
      // don't go over Foralls
      case Forall(_, _) => List.empty
Christian Müller's avatar
Christian Müller committed
178
      case t:ForallOtherThan => List.empty
179 180 181
      // don't go over Globally
      case Globally(_) => List.empty
    }
Christian Müller's avatar
Christian Müller committed
182 183
    // TODO: this only works if the a's are not in scope of one another
    val agents = t.collect(coll).distinct
184
    
185
    def elim:PartialFunction[Formula, Formula] = {
186 187 188
      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
189
      case term:ForallOtherThan => term
190 191 192 193 194 195 196 197
      // 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
198 199

  // Instantiate all universals in a E*A* formula
200
  def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
Christian Müller's avatar
Christian Müller committed
201
    
Christian Müller's avatar
Christian Müller committed
202 203 204
//    if (agents.isEmpty) {
//      logger.warn("Agent list empty")
//    }
Christian Müller's avatar
Christian Müller committed
205
    val universe = agents.groupBy(_.typ)
Christian Müller's avatar
Christian Müller committed
206
    
207
    def instantiate(tup:List[Var],t:Formula,universe:Map[String,List[FOLTL.Var]]) = {
Christian Müller's avatar
Christian Müller committed
208 209
      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
210
//        logger.warn(s"Ignored ${Forall(tup, t)} (empty universe for at least one type)")
Christian Müller's avatar
Christian Müller committed
211 212 213 214 215 216 217 218 219
        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
220
            case v:Var => mapping.getOrElse(v,v)
Christian Müller's avatar
Christian Müller committed
221 222 223 224 225 226
          })
        }
        eliminateUniversals(And.make(terms), agents)
      }
    }
    
Christian Müller's avatar
Christian Müller committed
227
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
228 229 230
        case Exists(tup, term) => {
          Exists(tup, eliminateUniversals(term, agents ++ tup))
        }
Christian Müller's avatar
Christian Müller committed
231
        case Forall(tup, term) => {
Christian Müller's avatar
Christian Müller committed
232 233 234 235 236 237 238
          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
239 240 241 242
        }
    })
  }
  
243
  /**
Christian Müller's avatar
Christian Müller committed
244
   * Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x")
245
   */
Christian Müller's avatar
Christian Müller committed
246
  def eliminatePredicates(t: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
247
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
248
      case f:Fun => f.encodeToVar()
Christian Müller's avatar
Christian Müller committed
249 250 251
    })
  }
  
252 253
  /**
   * Instantiates universals in EA formulae.
Christian Müller's avatar
Christian Müller committed
254
   * Resulting formula is in E* with all existentials outermost and in NegNF
255
   */
Christian Müller's avatar
Christian Müller committed
256
  def instantiateUniversals(f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
257

258
    // Check fragment
Christian Müller's avatar
Christian Müller committed
259
    if (!f.isBS) {
260 261 262 263
      logger.error("Trying to instantiate Universals for wrong fragment")
      logger.error(s"Formula was $f")
    }
    
Christian Müller's avatar
Christian Müller committed
264
    val nf = f.toNegNf
Christian Müller's avatar
Christian Müller committed
265
    val (agents, inner) = FOTransformers.eliminateExistentials(nf)
266
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
267
    val constants = existbound.freeVars
Christian Müller's avatar
Christian Müller committed
268 269
    
    FOTransformers.eliminateUniversals(existbound, constants.toList)    
270 271 272
  }
  
  /**
Christian Müller's avatar
Christian Müller committed
273 274
   * Instantiates existentials in AE formulae.
   * Resulting formula is in NegNF
275
   */
Christian Müller's avatar
Christian Müller committed
276
  def abstractExistentials(f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
277
    val neg = Neg(f).toNegNf.simplify
Christian Müller's avatar
Christian Müller committed
278 279
    
    // Check fragment
Christian Müller's avatar
Christian Müller committed
280
    if (!neg.isBS) {
Christian Müller's avatar
Christian Müller committed
281 282
      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
283
    }
284
    
Christian Müller's avatar
Christian Müller committed
285 286
    val (agents, inner) = FOTransformers.eliminateExistentials(neg)
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
287
    val constants = neg.freeVars
Christian Müller's avatar
Christian Müller committed
288
    val res = FOTransformers.eliminateUniversals(existbound, constants.toList)
Christian Müller's avatar
Christian Müller committed
289
    Neg(res).simplify
290
  }
Christian Müller's avatar
Christian Müller committed
291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306

  /**
    * 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
307
    val neg = Neg(f).simplify
Christian Müller's avatar
Christian Müller committed
308 309
    val constants = neg.freeVars ++ universe
    val res = FOTransformers.eliminateUniversals(neg, constants.toList)
Christian Müller's avatar
Christian Müller committed
310
    Neg(res).simplify
Christian Müller's avatar
Christian Müller committed
311
  }
Christian Müller's avatar
Christian Müller committed
312
}