toz3.scala 5.47 KB
Newer Older
Eugen Zalinescu's avatar
Eugen Zalinescu committed
1 2 3 4
package de.tum.workflows.toz3;

import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
5
import de.tum.workflows.foltl.FormulaFunctions._
Eugen Zalinescu's avatar
Eugen Zalinescu committed
6 7

import com.microsoft.z3._;
8
import java.util.concurrent.atomic.AtomicInteger
Eugen Zalinescu's avatar
Eugen Zalinescu committed
9
import java.util.HashMap
10
import com.typesafe.scalalogging.LazyLogging
Eugen Zalinescu's avatar
Eugen Zalinescu committed
11

12 13 14 15 16 17 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
object toZ3 extends LazyLogging {
  def succ(ctx: Context, e: ArithExpr) = {
    val One = ctx.mkInt(1)
    ctx.mkAdd(e, One)
  }

  var counter = 0

  val fun_ctx = new HashMap[String, FuncDecl]()

  def new_tvar(ctx: Context) = {
    counter = counter + 1
    "t" + counter
  }

  //  def getSort(ctx: Context, typ: String) = {
  //    if (!sort_ctx.isDefinedAt(typ)) {
  //      // TODO: size of the finite domain?!
  //      val s = ctx.mkFiniteDomainSort(typ, 2)
  //      sort_ctx += (typ -> s)           
  //    }
  //    sort_ctx(typ)
  //  }

  def buildVarCtx(ctx: Context, var_ctx: Map[Var, (Int, Expr, Sort)], vars: List[Var]) = {
    val newexprs = (for ((v, i) <- vars.zip(vars.size - 1 to 0)) yield {
      // TODO: size?
      val sort = if (v.typ.equals("Int")) {
        ctx.getIntSort()
      } else if (v.typ.equals("Bool")) {
        ctx.getBoolSort()
      } else {
        ctx.mkFiniteDomainSort(v.typ, 2)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
45
      }
46 47 48 49 50 51 52 53 54 55 56

      v -> (i, ctx.mkBound(i, sort), sort)
    }) toMap

    val oldvars = (for ((v, (i, e, s)) <- var_ctx) yield {
      val newi = i + vars.size
      val newbound = ctx.mkBound(newi, s)
      v -> (newi, newbound, s)
    })

    newexprs ++ oldvars
Eugen Zalinescu's avatar
Eugen Zalinescu committed
57 58
  }
  
59 60 61 62
  def updateTime(tvar: Option[Var], texpr:ArithExpr, oldctx:Map[Var, (Int, Expr, Sort)], newctx:Map[Var, (Int, Expr, Sort)]) = {
       if (tvar.isEmpty) { texpr } else {
        texpr.substitute(oldctx(tvar.get)._2, newctx(tvar.get)._2).asInstanceOf[ArithExpr]
      }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
63 64
  }

65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
  def toZ3(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var], var_ctx: Map[Var, (Int, Expr, Sort)]): BoolExpr = {
    // tvar can be an expression e with the form 
    // given by the following grammar: 
    //   e ::= 0 | t | succ(e)

    f match {
      //      case v: Var =>  // TODO

      case Fun(name, ind, params) => {
        var fdecl = fun_ctx.get(name)
        
        if (fdecl == null) {
          val pi = if (ind.isDefined) "_" + ind.get else ""
          val sorts = params.map(x => var_ctx(x)._3)
          // first sort is Int, as it stores time values
          val new_sorts = (ctx.getIntSort() :: sorts).toArray[Sort]
          fdecl = ctx.mkFuncDecl(name + pi, new_sorts, ctx.getBoolSort())
          fun_ctx.put(name, fdecl)
        }

        // all variables should be quantified, so they should be part of var_ctx
        val all_args = texpr :: params.map(x => var_ctx(x)._2)
        fdecl.apply(all_args: _*).asInstanceOf[BoolExpr]
      }

      case Next(f1) => {
        toZ3(ctx, f1, succ(ctx, texpr), tvar, var_ctx)
      }

      case Globally(f1) => {
        val newt = new_tvar(ctx)
        val quantifiername = "G" + counter
        val sortInt = ctx.getIntSort()
Eugen Zalinescu's avatar
Eugen Zalinescu committed
98

99
        val variable = Var(newt, "Int")
Eugen Zalinescu's avatar
Eugen Zalinescu committed
100

101
        val newctx = buildVarCtx(ctx, var_ctx, List(variable))
Eugen Zalinescu's avatar
Eugen Zalinescu committed
102

103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
        val new_texpr = newctx(variable)._2.asInstanceOf[ArithExpr]
        val e1 = toZ3(ctx, f1, new_texpr, Some(variable), newctx)

        // replace old timevar in old ctx by new timevar
        val old_texpr = updateTime(tvar, texpr, var_ctx, newctx)

        val e0 = ctx.mkLe(old_texpr, new_texpr.asInstanceOf[ArithExpr])
        val body = ctx.mkImplies(e0, e1)

        ctx.mkForall(Array(sortInt), Array(ctx.mkSymbol(newt)), body, 0, null, null,
          ctx.mkSymbol(quantifiername), null)
      }

      //      case Finally(f1) => {
      //        
      //      }
      //      
      //      case Until(f1, f2) => {
      //        
      //      }

      case FOLTL.Exists(vars, f1) => {
        val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)) toArray
        val newctx = buildVarCtx(ctx, var_ctx, vars)
        val sorts = vars.map(newctx(_)._3) toArray
        
        val upd_texpr = updateTime(tvar, texpr, var_ctx, newctx)
        
        val e1 = toZ3(ctx, f1, upd_texpr, tvar, newctx)

        ctx.mkExists(sorts, names, e1, 0, null, null, null, null)
      }

      case FOLTL.Forall(vars, f1) => {
        val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)) toArray
        val newctx = buildVarCtx(ctx, var_ctx, vars)
        val sorts = vars.map(newctx(_)._3) toArray
        
        val upd_texpr = updateTime(tvar, texpr, var_ctx, newctx)
        
        val e1 = toZ3(ctx, f1, upd_texpr, tvar, newctx)

        ctx.mkForall(sorts, names, e1, 0, null, null, null, null)
      }

      // TODO: forallotherthan

      case And(f1, f2) => {
        val e1 = toZ3(ctx, f1, texpr, tvar, var_ctx)
        val e2 = toZ3(ctx, f2, texpr, tvar, var_ctx)
        ctx.mkAnd(e1, e2)
      }

      case Or(f1, f2) => {
        val e1 = toZ3(ctx, f1, texpr, tvar, var_ctx)
        val e2 = toZ3(ctx, f2, texpr, tvar, var_ctx)
        ctx.mkOr(e1, e2)
      }

      case Implies(f1, f2) => {
        val e1 = toZ3(ctx, f1, texpr, tvar, var_ctx)
        val e2 = toZ3(ctx, f2, texpr, tvar, var_ctx)
        ctx.mkImplies(e1, e2)
      }

      case Neg(f1) => {
        val e = toZ3(ctx, f1, texpr, tvar, var_ctx)
        ctx.mkNot(e)
      }
    }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
173
  }
174 175 176 177 178 179 180 181 182 183 184 185

  def checkZ3(f: Formula) = {
    val cfg = new HashMap[String, String]();
    cfg.put("model", "true");
    val ctx = new Context(cfg);

    val expr = toZ3(ctx, f, ctx.mkInt(0), None, Map())
    logger.info(s"Checking Z3 expression:\n$expr")
    
    val s = ctx.mkSolver()
    s.add(expr)
    s
Eugen Zalinescu's avatar
Eugen Zalinescu committed
186 187
  }
}