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

import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
src  
Christian Müller committed
4
import de.tum.workflows.Utils
Christian Müller's avatar
Christian Müller committed
5
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
src  
Christian Müller committed
6
import de.tum.workflows.toz3.Z3BSFO
Christian Müller's avatar
Christian Müller committed
7

Christian Müller's avatar
Christian Müller committed
8
object FOTransformers extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
9
  
Christian Müller's avatar
Christian Müller committed
10
  // Computes all possible tuples of signature types
Christian Müller's avatar
Christian Müller committed
11 12 13 14 15 16
  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
17
          logger.error(s"No variable for type $t in the universe.")
Christian Müller's avatar
Christian Müller committed
18
        }
Christian Müller's avatar
Christian Müller committed
19

Christian Müller's avatar
Christian Müller committed
20 21
        for (a <- universe(t); s <- subres) yield {
          a :: s
Christian Müller's avatar
Christian Müller committed
22 23 24 25 26
        }
      }
    }
  }
  
Christian Müller's avatar
Christian Müller committed
27 28 29 30 31 32 33 34 35 36
  def collectClauses(f:Formula):List[List[Formula]] = {
    def collectClause(f:Formula):List[Formula] = f collect {
      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
37 38
      case Quantifier(vars, make, t) => collectMultiClause(t)
      case t => List(collectClause(t))
Christian Müller's avatar
Christian Müller committed
39
    }
Christian Müller's avatar
Christian Müller committed
40 41 42 43 44
    f match {
      case True => List()
      case False => List(List())
      case _ => collectMultiClause(f)
    }
Christian Müller's avatar
Christian Müller committed
45 46
  }
  
Christian Müller's avatar
Christian Müller committed
47 48 49 50 51 52 53
  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
54
    elimSub(f.toNegNf, Set())
Christian Müller's avatar
Christian Müller committed
55 56
  }
  
Christian Müller's avatar
Christian Müller committed
57
  def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
58
    logger.debug(s"Eliminating universal second order predicate $AUX")
Christian Müller's avatar
src  
Christian Müller committed
59 60

    val cnf = f.toCNF
Christian Müller's avatar
Christian Müller committed
61 62
    
    // TODO: add equalities?
Christian Müller's avatar
src  
Christian Müller committed
63
    val repld = cnf everywhere {
Christian Müller's avatar
Christian Müller committed
64 65 66
      case Neg(Fun(AUX, _, _)) => False
      case Fun(AUX, _, _) => False
    }
Christian Müller's avatar
Christian Müller committed
67
    repld.simplify
Christian Müller's avatar
src  
Christian Müller committed
68 69
  }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    val freeparams = b.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
    val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield {
Christian Müller's avatar
Christian Müller committed
167
      Or.make(gk, ineq(garg, freeparams))
Christian Müller's avatar
ineq  
Christian Müller committed
168 169
    }
    val fsol:Formula = And.make(gkineq)
Christian Müller's avatar
Christian Müller committed
170
    val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
171

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

Christian Müller's avatar
src  
Christian Müller committed
174
    if (Utils.DEBUG_MODE) {
Christian Müller's avatar
ineq  
Christian Müller committed
175
      logger.info(s"BSFO SOQE: strategy for ${b.updatedParams(freeparams)}: $z3fsolq")
Christian Müller's avatar
src  
Christian Müller committed
176 177
    }

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

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

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

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