Z3BSFO.scala 4.83 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 42 43 44 45 46

      // Can only check universal things
      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
  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
66

67 68
    val (ctx, _) = createContext()

Christian Müller's avatar
Christian Müller committed
69
    val simp = ctx.mkTactic("ctx-solver-simplify")
Christian Müller's avatar
src  
Christian Müller committed
70 71
    val simp2 = ctx.mkTactic("simplify")

Christian Müller's avatar
Christian Müller committed
72
    val params = ctx.mkParams()
Christian Müller's avatar
src  
Christian Müller committed
73 74 75 76
    params.add("mbqi", true)
    //    params.add("mbqi.trace", true)
    val tactics = ctx.andThen(simp, simp2)
    simp.getSolver.setParameters(params)
Christian Müller's avatar
Christian Müller committed
77 78 79 80 81

    // 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
82 83

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

85
    val sub = ar.getSubgoals
Christian Müller's avatar
Christian Müller committed
86 87 88 89 90 91 92 93 94
    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
95
    }
Christian Müller's avatar
Christian Müller committed
96 97
    mapped
  }
Christian Müller's avatar
Christian Müller committed
98

99
  def toCNFUniversal(f:Formula): Formula = {
Christian Müller's avatar
src  
Christian Müller committed
100 101 102 103
    if (!f.isUniversal) {
      logger.error("Trying to get CNF of non-universal formula via Z3")
    }

Christian Müller's avatar
Christian Müller committed
104
    val f2 = f.toPrenex.simplify
Christian Müller's avatar
src  
Christian Müller committed
105 106 107 108 109 110 111 112 113 114

    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)
  }

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

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

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

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

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

131 132
    val (ctx, _) = createContext()

Christian Müller's avatar
src  
Christian Müller committed
133 134 135 136
    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
137 138 139 140 141 142
    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
143
    val ar = bothtactics.apply(goal)
Christian Müller's avatar
Christian Müller committed
144 145 146 147 148 149 150 151 152 153 154

    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
155
    }
Christian Müller's avatar
src  
Christian Müller committed
156 157
    val clauses = FOTransformers.collectClauses(mapped)
    clauses
Christian Müller's avatar
Christian Müller committed
158
  }
Christian Müller's avatar
Christian Müller committed
159

Christian Müller's avatar
Christian Müller committed
160
  def debugmodelBS(f:Formula):String = {
161 162 163 164 165 166 167 168 169 170 171 172
    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) {
173
      logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown}")
Christian Müller's avatar
Christian Müller committed
174
      "No model found - Status unknown"
175 176 177
    } else if (c == Status.SATISFIABLE) {
      s.getModel.toString
    } else {
Christian Müller's avatar
Christian Müller committed
178
      "No model found - Status UNSAT"
179 180 181
    }
  }

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