FOTransformers.scala 6.5 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 4 5

import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOLTL._

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

Christian Müller's avatar
Christian Müller committed
18 19
        for (a <- universe(t); s <- subres) yield {
          a :: s
Christian Müller's avatar
Christian Müller committed
20 21 22 23 24
        }
      }
    }
  }
  
Christian Müller's avatar
Christian Müller committed
25 26 27 28 29 30 31 32 33 34
  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
35 36
      case Quantifier(vars, make, t) => collectMultiClause(t)
      case t => List(collectClause(t))
Christian Müller's avatar
Christian Müller committed
37 38 39 40 41
    }
    
    collectMultiClause(f)
  }
  
Christian Müller's avatar
Christian Müller committed
42 43 44 45 46 47 48
  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
49
    elimSub(f.toNegNf, Set())
Christian Müller's avatar
Christian Müller committed
50 51
  }
  
Christian Müller's avatar
Christian Müller committed
52
  def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
Christian Müller's avatar
Christian Müller committed
53
    val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(f)
Christian Müller's avatar
Christian Müller committed
54 55 56 57 58 59 60 61 62 63 64
    
    // Inspect clauses
    val simped = 
      for (c <- clauses;
        removeclause = (for (c1 <- c if (c.contains(Neg(c1)))) yield true)
        if (removeclause.isEmpty)
      ) yield {
        c
      }
    
    // TODO: improve
Christian Müller's avatar
Christian Müller committed
65
    val form = And.make(simped.map(Or.make))
Christian Müller's avatar
Christian Müller committed
66 67 68 69 70 71 72 73 74 75 76
    val newform = quantifiers.foldRight(form)((q, inner) => if(q._1) Exists(q._2, inner) else Forall(q._2, inner))
    
    // TODO: add equalities?
    val repld = newform everywhere {
      case Neg(Fun(AUX, _, _)) => False
      case Fun(AUX, _, _) => False
    }
    
    repld.simplify()
  }
  
77 78 79 80
  /**
   * Gobble up all outermost existential quantifiers
   * Needs to have non-conflicting bindings
   */
81
  def eliminateExistentials(t:Formula) = {
82
    
83
    def coll:PartialFunction[Formula, List[Var]] = {
Christian Müller's avatar
Christian Müller committed
84
      case Exists(a, term) => a ++ term.collect(coll)
85 86
      // don't go over Foralls
      case Forall(_, _) => List.empty
Christian Müller's avatar
Christian Müller committed
87
      case t:ForallOtherThan => List.empty
88 89 90
      // don't go over Globally
      case Globally(_) => List.empty
    }
Christian Müller's avatar
Christian Müller committed
91 92
    // TODO: this only works if the a's are not in scope of one another
    val agents = t.collect(coll).distinct
93
    
94
    def elim:PartialFunction[Formula, Formula] = {
95 96 97
      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
98
      case term:ForallOtherThan => term
99 100 101 102 103 104 105 106
      // 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
107 108

  // Instantiate all universals in a E*A* formula
109
  def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
Christian Müller's avatar
Christian Müller committed
110
    
Christian Müller's avatar
Christian Müller committed
111 112 113
//    if (agents.isEmpty) {
//      logger.warn("Agent list empty")
//    }
Christian Müller's avatar
Christian Müller committed
114
    val universe = agents.groupBy(_.typ)
Christian Müller's avatar
Christian Müller committed
115
    
116
    def instantiate(tup:List[Var],t:Formula,universe:Map[String,List[FOLTL.Var]]) = {
Christian Müller's avatar
Christian Müller committed
117 118
      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
119
//        logger.warn(s"Ignored ${Forall(tup, t)} (empty universe for at least one type)")
Christian Müller's avatar
Christian Müller committed
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
        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)))
          })
        }
        eliminateUniversals(And.make(terms), agents)
      }
    }
    
Christian Müller's avatar
Christian Müller committed
135
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
136 137 138
        case Exists(tup, term) => {
          Exists(tup, eliminateUniversals(term, agents ++ tup))
        }
Christian Müller's avatar
Christian Müller committed
139
        case Forall(tup, term) => {
Christian Müller's avatar
Christian Müller committed
140 141 142 143 144 145 146
          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
147 148 149 150
        }
    })
  }
  
151
  /**
Christian Müller's avatar
Christian Müller committed
152
   * Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x")
153
   */
154
  def eliminatePredicates(t: Formula) = {
Christian Müller's avatar
Christian Müller committed
155
    t.everywhere({
Christian Müller's avatar
Christian Müller committed
156
      case f:Fun => f.encodeToVar()
Christian Müller's avatar
Christian Müller committed
157 158 159
    })
  }
  
160 161
  /**
   * Instantiates universals in EA formulae.
Christian Müller's avatar
Christian Müller committed
162
   * Resulting formula is in E* with all existentials outermost and in NegNF
163 164
   */
  def instantiateUniversals(f:Formula) = {
Christian Müller's avatar
Christian Müller committed
165

166
    // Check fragment
Christian Müller's avatar
Christian Müller committed
167
    if (!f.isBS) {
168 169 170 171
      logger.error("Trying to instantiate Universals for wrong fragment")
      logger.error(s"Formula was $f")
    }
    
Christian Müller's avatar
Christian Müller committed
172
    val nf = f.toNegNf
Christian Müller's avatar
Christian Müller committed
173
    val (agents, inner) = FOTransformers.eliminateExistentials(nf)
174
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
175 176 177
    val constants = existbound.freeVars()
    
    FOTransformers.eliminateUniversals(existbound, constants.toList)    
178 179 180
  }
  
  /**
Christian Müller's avatar
Christian Müller committed
181 182
   * Instantiates existentials in AE formulae.
   * Resulting formula is in NegNF
183
   */
Christian Müller's avatar
Christian Müller committed
184
  def abstractExistentials(f:Formula) = {
Christian Müller's avatar
Christian Müller committed
185
    val neg = Neg(f).toNegNf.simplify
Christian Müller's avatar
Christian Müller committed
186 187
    
    // Check fragment
Christian Müller's avatar
Christian Müller committed
188
    if (!neg.isBS) {
Christian Müller's avatar
Christian Müller committed
189 190
      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
191
    }
192
    
Christian Müller's avatar
Christian Müller committed
193 194
    val (agents, inner) = FOTransformers.eliminateExistentials(neg)
    val existbound = Exists(agents, inner)
Christian Müller's avatar
Christian Müller committed
195
    val constants = neg.freeVars
Christian Müller's avatar
Christian Müller committed
196
    val res = FOTransformers.eliminateUniversals(existbound, constants.toList)
Christian Müller's avatar
Christian Müller committed
197
    Neg(res).simplify()
198
  }
Christian Müller's avatar
Christian Müller committed
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219

  /**
    * 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")
    }

    val neg = Neg(f).simplify()
    val constants = neg.freeVars ++ universe
    val res = FOTransformers.eliminateUniversals(neg, constants.toList)
    Neg(res).simplify()
  }
Christian Müller's avatar
Christian Müller committed
220
}