Z3LTLQFreeTest.scala 2.53 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.workflows.tests
Christian Müller's avatar
Christian Müller committed
2 3 4 5 6 7 8

import org.scalatest.BeforeAndAfterEach
import com.typesafe.scalalogging.LazyLogging
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import com.microsoft.z3.Solver
import java.util.HashMap
Christian Müller's avatar
Christian Müller committed
9

Christian Müller's avatar
Christian Müller committed
10 11 12 13
import org.scalatest.FlatSpec
import com.microsoft.z3.Context
import de.tum.workflows.Implicits._
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
14
import de.tum.workflows.toz3.{Z3FOEncoding, Z3QFree}
Christian Müller's avatar
Christian Müller committed
15 16
import com.microsoft.z3.Status

Christian Müller's avatar
Christian Müller committed
17
  class Z3QFreeTest extends FlatSpec with LazyLogging with BeforeAndAfterEach {
Christian Müller's avatar
Christian Müller committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47

  var ctx: Context = null
  var s: Solver = null

  val TIMEOUT = 30000 // in milliseconds

  override def beforeEach() = {
    val cfg = new HashMap[String, String]()
    cfg.put("timeout", TIMEOUT.toString())

    val ctx = new Context(cfg)

    val qe = ctx.mkTactic("qe")
    val default = ctx.mkTactic("smt")
    val t = ctx.andThen(qe, default)

    val s = ctx.mkSolver(t)

    this.ctx = ctx
    this.s = s
  }
  
  def check(s: Solver, res: Status) = {
    val c = s.check()
    if (c == Status.UNKNOWN) {
      println(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
    
    c should be (res)
    if (res == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
48
      println(s"Z3 model:\n${Z3FOEncoding.printModel(s.getModel())}")
Christian Müller's avatar
Christian Müller committed
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
    }
  }
  
  "Z3QFree" should "check small things SAT" in {
    val easyForm = And("a", "b")

    s.add(Z3QFree.translate(easyForm, ctx))
    check(s, Status.SATISFIABLE)
  }
  
  it should "check small things UNSAT" in {
    val easyForm = And("a", Neg("a"))

    s.add(Z3QFree.translate(easyForm, ctx))
    check(s, Status.UNSATISFIABLE)
  }
  
  it should "check longer things SAT" in {
    val easyForm = Or(And("a", "b"), And("c",Or("d","e")))

    s.add(Z3QFree.translate(easyForm, ctx))
    check(s, Status.SATISFIABLE)
  }
Christian Müller's avatar
Christian Müller committed
72 73 74 75
  
  it should "simplify stuff" in {
    Z3QFree.simplifyQFree(And(Or(Fun("a", List()), Fun("b", List())), Fun("a", List()))) should be (Fun("a", List()))
  
Christian Müller's avatar
Christian Müller committed
76
    val eq = Equiv(Fun("A", List("x")), Fun("A", List("y")))
Christian Müller's avatar
Christian Müller committed
77 78 79
    Z3QFree.simplifyQFree(eq) 
    Z3QFree.simplifyQFree(False) should be (False)
  }
Christian Müller's avatar
Christian Müller committed
80

Christian Müller's avatar
Christian Müller committed
81 82
    // TODO: this is broken until Z3 can build interpolants again
    ignore should "build interpolants" in {
Christian Müller's avatar
Christian Müller committed
83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
      val f1 = And("a", "b")
      val f2 = Neg("b")

      val itp = Z3QFree.interpolate(f1, f2)

      itp should be (Some(Fun("b", List())))
    }

    it should "not build interpolants for sat things" in {
      val f1 = And("a", "b")
      val f2 = Neg("c")

      val itp = Z3QFree.interpolate(f1, f2)

      logger.info(s"Interpolant $itp")

      itp should be (None)
    }
Christian Müller's avatar
Christian Müller committed
101
}