FOTransformers.scala 10.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 50 51 52 53 54 55
  def eliminateDoubleQuantifiers(f:Formula) = {
    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
  }
  
59
  def eliminateAuxiliaryPredicate(f:Formula, AUX:String, props:InvProperties) = {
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 72
  def eliminateBPredicate(f:Formula, B:Fun) = {
    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 87

    // Group clauses by positive/negative occurences
    def ispositive(clause: List[Formula]) =
Christian Müller's avatar
Christian Müller committed
88 89
      getPositiveBArguments(clause).nonEmpty

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

    def pruneBs(clause: List[Formula]) = {
94
      clause filterNot {
Christian Müller's avatar
ineq  
Christian Müller committed
95 96
        case Neg(Fun(NAME, _, _)) => true
        case Fun(NAME, _, _) => true
Christian Müller's avatar
src  
Christian Müller committed
97 98 99
        case _ => false
      }
    }
100
    def getPositiveBArguments(clause: List[Formula]):Set[List[Var]] = {
Christian Müller's avatar
Christian Müller committed
101
      clause flatMap {
Christian Müller's avatar
ineq  
Christian Müller committed
102
        case Fun(NAME, _, vars) => List(vars)
Christian Müller's avatar
Christian Müller committed
103
        case _ => List()
104
      } toSet
Christian Müller's avatar
Christian Müller committed
105
    }
106
    def getNegativeBArguments(clause: List[Formula]):Set[List[Var]] = {
Christian Müller's avatar
Christian Müller committed
107
      clause flatMap {
Christian Müller's avatar
ineq  
Christian Müller committed
108
        case Neg(Fun(NAME, _, vars))=> List(vars)
Christian Müller's avatar
Christian Müller committed
109
        case _ => List()
110
      } toSet
Christian Müller's avatar
Christian Müller committed
111 112 113 114 115 116
    }

    def ineq(l1:List[Var], l2:List[Var]) = {
      if (l1.size != l2.size) {
        logger.warn("Trying to generate inequalities for different sized vectors")
      }
117
      val ineqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
Christian Müller's avatar
Christian Müller committed
118 119
        case (x, y) if x.name <= y.name => Neg(Equal(x,y))
        case (x, y)  => Neg(Equal(y,x))
120 121
      }.toSet
      Or.make(ineqs.toList)
Christian Müller's avatar
Christian Müller committed
122
    }
Christian Müller's avatar
src  
Christian Müller committed
123 124 125

    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
126
    //  F \/ B z_1 ... B z_r
127
    val Fargs = F.map(getPositiveBArguments)
Christian Müller's avatar
Christian Müller committed
128

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

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

Christian Müller's avatar
Christian Müller committed
135
    // H \/ B u_1 .. B u_l \/ !B v_1 ... ! B v_n
136 137
    val HPositiveargs = H.map(getPositiveBArguments)
    val HNegativeargs = H.map(getNegativeBArguments)
Christian Müller's avatar
Christian Müller committed
138

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

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

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

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

Christian Müller's avatar
ineq  
Christian Müller committed
173
    val fsol:Formula = And.make(gkineq)
Christian Müller's avatar
Christian Müller committed
174
    val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
175

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

Christian Müller's avatar
src  
Christian Müller committed
178
    if (Utils.DEBUG_MODE) {
Christian Müller's avatar
Christian Müller committed
179
      logger.info(s"BSFO SOQE: strategy for ${B.updatedParams(freeparams)}: $z3fsolq")
Christian Müller's avatar
src  
Christian Müller committed
180 181
    }

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

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

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

  /**
    * 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
324
    val neg = Neg(f).simplify
Christian Müller's avatar
Christian Müller committed
325 326
    val constants = neg.freeVars ++ universe
    val res = FOTransformers.eliminateUniversals(neg, constants.toList)
Christian Müller's avatar
Christian Müller committed
327
    Neg(res).simplify
Christian Müller's avatar
Christian Müller committed
328
  }
Christian Müller's avatar
Christian Müller committed
329
}