Z3BSFO.scala 4.47 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 16 17 18 19 20 21 22 23 24 25 26 27
  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
28 29 30 31

  def checkAE(f: Formula) = {

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

Christian Müller's avatar
Christian Müller committed
34
      val neg = Neg(f).simplify
Christian Müller's avatar
Christian Müller committed
35 36 37 38 39 40 41

      // 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
42
      s.add(Z3FOEncoding.translate(neg, ctx))
Christian Müller's avatar
Christian Müller committed
43 44 45 46 47 48

      // 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
49

Christian Müller's avatar
Christian Müller committed
50 51
      (c, s)
    }
Christian Müller's avatar
src  
Christian Müller committed
52
    logger.debug(s"Z3-BSFO call took $time ms")
Christian Müller's avatar
Christian Müller committed
53 54 55
    res
  }

Christian Müller's avatar
Christian Müller committed
56 57
  def simplifyBS(f: Formula) = {

58 59
    val (ctx, _) = createContext()

Christian Müller's avatar
Christian Müller committed
60
    val simp = ctx.mkTactic("ctx-solver-simplify")
Christian Müller's avatar
src  
Christian Müller committed
61 62
    val simp2 = ctx.mkTactic("simplify")

Christian Müller's avatar
Christian Müller committed
63
    val params = ctx.mkParams()
Christian Müller's avatar
src  
Christian Müller committed
64 65 66 67
    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
68 69 70 71 72

    // 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
73 74

    val ar = tactics.apply(goal)
Christian Müller's avatar
Christian Müller committed
75 76 77 78 79 80 81 82 83 84 85

    val sub = ar.getSubgoals()
    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
86
    }
Christian Müller's avatar
Christian Müller committed
87 88
    mapped
  }
Christian Müller's avatar
Christian Müller committed
89

Christian Müller's avatar
src  
Christian Müller committed
90 91 92 93 94
  def toCNFUniversal(f:Formula) = {
    if (!f.isUniversal) {
      logger.error("Trying to get CNF of non-universal formula via Z3")
    }

Christian Müller's avatar
Christian Müller committed
95
    val f2 = f.toPrenex.simplify
Christian Müller's avatar
src  
Christian Müller committed
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110

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

  def toCNFClausesUniversal(f:Formula) = {
    if (!f.isUniversal) {
      logger.error("Trying to get CNF of non-universal formula via Z3")
    }

Christian Müller's avatar
Christian Müller committed
111
    val f2 = f.toPrenex.simplify
Christian Müller's avatar
src  
Christian Müller committed
112 113 114 115 116 117 118 119 120

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

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

  def toCNFQFreeClauses(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
121

122 123
    val (ctx, _) = createContext()

Christian Müller's avatar
src  
Christian Müller committed
124 125 126 127
    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
128 129 130 131 132 133
    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
134
    val ar = bothtactics.apply(goal)
Christian Müller's avatar
Christian Müller committed
135 136 137 138 139 140 141 142 143 144 145

    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
146
    }
Christian Müller's avatar
src  
Christian Müller committed
147 148
    val clauses = FOTransformers.collectClauses(mapped)
    clauses
Christian Müller's avatar
Christian Müller committed
149
  }
Christian Müller's avatar
Christian Müller committed
150

Christian Müller's avatar
Christian Müller committed
151
  def debugmodelBS(f:Formula):String = {
152 153 154 155 156 157 158 159 160 161 162 163 164
    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) {
      logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}")
Christian Müller's avatar
Christian Müller committed
165
      "No model found - Status unknown"
166 167 168
    } else if (c == Status.SATISFIABLE) {
      s.getModel.toString
    } else {
Christian Müller's avatar
Christian Müller committed
169
      "No model found - Status UNSAT"
170 171 172
    }
  }

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