Z3BSFO.scala 5.13 KB
Newer Older
1
package de.tum.niwo.toz3
Christian Müller's avatar
Christian Müller committed
2 3 4 5

import com.typesafe.scalalogging.LazyLogging
import java.util

6
import de.tum.niwo.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
7
import com.microsoft.z3._
8 9
import de.tum.niwo.Utils
import de.tum.niwo.foltl.{FOTransformers, FormulaFunctions}
Christian Müller's avatar
Christian Müller committed
10 11 12

object Z3BSFO extends LazyLogging {

13 14 15
  var aechecks = 0
  var simplifications = 0

16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
  def createContext():(Context, Solver) = {
    // Set up Z3
    val cfg = new util.HashMap[String, String]()
    cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
    val ctx = new Context(cfg)
    val params = ctx.mkParams()
    params.add("mbqi", true)
    //    params.add("mbqi.trace", true)

    val s = ctx.mkSolver()
    s.setParameters(params)

    (ctx, s)
  }

Christian Müller's avatar
Christian Müller committed
31

32 33 34
  def checkAE(f: Formula): (Status, Solver) = {
    aechecks += 1
    logger.trace(s"Checking a formula with ${f.opsize} operators.")
Christian Müller's avatar
Christian Müller committed
35 36

    val (time, res) = Utils.time {
37
      val (ctx, s) = createContext()
Christian Müller's avatar
Christian Müller committed
38

Christian Müller's avatar
Christian Müller committed
39
      val neg = Neg(f).simplify
Christian Müller's avatar
Christian Müller committed
40

41
      // Can only check AE things
Christian Müller's avatar
Christian Müller committed
42 43 44 45 46
      if (!neg.isBS) {
        logger.error("Z3-BSFO: Trying to encode formula not in Bernays-Schönfinkel")
      }

      // neg is now in E*A*, so can be solved by bounded instantiation
Christian Müller's avatar
Christian Müller committed
47
      s.add(Z3FOEncoding.translate(neg, ctx))
Christian Müller's avatar
Christian Müller committed
48 49 50 51 52 53

      // Send to z3
      val c = s.check()
      if (c == Status.UNKNOWN) {
        logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}")
      }
Christian Müller's avatar
src  
Christian Müller committed
54

Christian Müller's avatar
Christian Müller committed
55 56
      (c, s)
    }
57 58 59
    if (time > 1000) {
      logger.debug(s"Z3-BSFO call took $time ms")
    }
Christian Müller's avatar
Christian Müller committed
60 61 62
    res
  }

63 64 65 66
  def simplifyAE(f: Formula): Formula = {
    Neg(simplifyBS(Neg(f))).simplify
  }

67 68 69
  def simplifyBS(f: Formula): Formula = {
    simplifications += 1
    logger.trace(s"Simplifying a formula with ${f.opsize} operators.")
Christian Müller's avatar
Christian Müller committed
70

71 72 73 74 75
    // Can only simplify BS things
    if (!f.isBS) {
      logger.error("Z3-BSFO: Trying to simplify formula not in Bernays-Schönfinkel")
    }

76 77
    val (ctx, _) = createContext()

78 79 80
    val tactics = if (Utils.Z3CONTEXTELIM) {
      val simp = ctx.mkTactic("ctx-solver-simplify")
      val simp2 = ctx.mkTactic("simplify")
Christian Müller's avatar
src  
Christian Müller committed
81

82 83 84 85 86 87 88 89
      val params = ctx.mkParams()
      params.add("mbqi", true)
      params.add("mbqi.trace", true)
      simp.getSolver.setParameters(params)
      ctx.andThen(simp, simp2)
    } else {
      ctx.mkTactic("simplify")
    }
Christian Müller's avatar
Christian Müller committed
90 91 92 93 94

    // mkGoal (produce models, produce unsat cores, produce proofs)
    val goal = ctx.mkGoal(false, false, false)
    val z3expr = Z3FOEncoding.translate(f, ctx)
    goal.add(z3expr)
Christian Müller's avatar
src  
Christian Müller committed
95 96

    val ar = tactics.apply(goal)
Christian Müller's avatar
Christian Müller committed
97

98
    val sub = ar.getSubgoals
Christian Müller's avatar
Christian Müller committed
99 100 101 102 103 104 105 106 107
    val mapped = if (sub.isEmpty) {
      True
    } else if (sub.size > 1) {
      logger.error("Simplification Error: Returned several goals")
      False
    } else {
      val form = sub.head.AsBoolExpr()
      Z3FOEncoding.mapback(form)
//      Z3FOEncoding.mapback(z3expr)
Christian Müller's avatar
Christian Müller committed
108
    }
Christian Müller's avatar
Christian Müller committed
109 110
    mapped
  }
Christian Müller's avatar
Christian Müller committed
111

112
  def toCNFUniversal(f:Formula): Formula = {
Christian Müller's avatar
src  
Christian Müller committed
113 114 115 116
    if (!f.isUniversal) {
      logger.error("Trying to get CNF of non-universal formula via Z3")
    }

Christian Müller's avatar
Christian Müller committed
117
    val f2 = f.toPrenex.simplify
Christian Müller's avatar
src  
Christian Müller committed
118 119 120 121 122 123 124 125 126 127

    val quantifiers = FormulaFunctions.collectQuantifiers(f2)
    val stripped = FormulaFunctions.stripQuantifiers(f2)

    val clauses = toCNFQFreeClauses(stripped)
    val cnf = And.make(clauses.map(Or.make))
    val simped = simplifyBS(FormulaFunctions.rewrapQuantifiers(quantifiers, cnf))
    FormulaFunctions.pushUniversalQuantifiers(simped)
  }

128
  def toCNFClausesUniversal(f:Formula): (List[(Boolean, List[Var])], List[List[Formula]]) = {
Christian Müller's avatar
src  
Christian Müller committed
129 130 131 132
    if (!f.isUniversal) {
      logger.error("Trying to get CNF of non-universal formula via Z3")
    }

Christian Müller's avatar
Christian Müller committed
133
    val f2 = f.toPrenex.simplify
Christian Müller's avatar
src  
Christian Müller committed
134 135 136 137 138 139 140 141

    val quantifiers = FormulaFunctions.collectQuantifiers(f2)
    val stripped = FormulaFunctions.stripQuantifiers(f2)

    val clauses = toCNFQFreeClauses(stripped)
    (quantifiers, clauses)
  }

142
  def toCNFQFreeClauses(f: Formula): List[List[Formula]] = {
Christian Müller's avatar
Christian Müller committed
143

144 145
    val (ctx, _) = createContext()

Christian Müller's avatar
src  
Christian Müller committed
146 147 148 149
    val cnftactic = ctx.mkTactic("tseitin-cnf")
    val simptactic = ctx.mkTactic("ctx-solver-simplify")
    val bothtactics = ctx.andThen(cnftactic, simptactic)

Christian Müller's avatar
Christian Müller committed
150 151 152 153 154 155
    val params = ctx.mkParams()

    // mkGoal (produce models, produce unsat cores, produce proofs)
    val goal = ctx.mkGoal(false, false, false)
    val z3expr = Z3FOEncoding.translate(f, ctx)
    goal.add(z3expr)
Christian Müller's avatar
src  
Christian Müller committed
156
    val ar = bothtactics.apply(goal)
Christian Müller's avatar
Christian Müller committed
157 158 159 160 161 162 163 164 165 166 167

    val sub = ar.getSubgoals()
    val mapped = if (sub.isEmpty) {
      True
    } else if (sub.size > 1) {
      logger.error("Z3BSFO-CNF: Returned several goals")
      False
    } else {
      val form = sub.head.AsBoolExpr()
      Z3FOEncoding.mapback(form)
      //      Z3FOEncoding.mapback(z3expr)
Christian Müller's avatar
Christian Müller committed
168
    }
Christian Müller's avatar
src  
Christian Müller committed
169 170
    val clauses = FOTransformers.collectClauses(mapped)
    clauses
Christian Müller's avatar
Christian Müller committed
171
  }
Christian Müller's avatar
Christian Müller committed
172

Christian Müller's avatar
Christian Müller committed
173
  def debugmodelBS(f:Formula):String = {
174 175 176 177 178 179 180 181 182 183 184 185
    val (ctx, s) = createContext()

    // Can only check universal things
    if (!f.isBS) {
      logger.error("Z3-BSFO: Trying to encode formula not in Bernays-Schönfinkel")
    }

    s.add(Z3FOEncoding.translate(f.simplify, ctx))

    // Send to z3
    val c = s.check()
    if (c == Status.UNKNOWN) {
186
      logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown}")
Christian Müller's avatar
Christian Müller committed
187
      "No model found - Status unknown"
188 189 190
    } else if (c == Status.SATISFIABLE) {
      s.getModel.toString
    } else {
Christian Müller's avatar
Christian Müller committed
191
      "No model found - Status UNSAT"
192 193 194
    }
  }

Christian Müller's avatar
Christian Müller committed
195
}