toz3.scala 7.31 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
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]()

Eugen Zalinescu's avatar
Eugen Zalinescu committed
22
  def new_tname() = {
23 24 25 26 27 28 29 30 31 32 33
    counter = counter + 1
    "t" + counter
  }

  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 {
      val sort = if (v.typ.equals("Int")) {
        ctx.getIntSort()
      } else if (v.typ.equals("Bool")) {
        ctx.getBoolSort()
      } else {
Eugen Zalinescu's avatar
Eugen Zalinescu committed
34
        ctx.mkFiniteDomainSort(v.typ, 10) // TODO: sort size?
Eugen Zalinescu's avatar
Eugen Zalinescu committed
35
      }
36 37 38 39 40 41 42 43 44 45 46

      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
47 48
  }
  
Eugen Zalinescu's avatar
Eugen Zalinescu committed
49
  def updateTime(texpr:ArithExpr, tvar: Option[Var], oldctx:Map[Var, (Int, Expr, Sort)], newctx:Map[Var, (Int, Expr, Sort)]) = {
50 51 52
       if (tvar.isEmpty) { texpr } else {
        texpr.substitute(oldctx(tvar.get)._2, newctx(tvar.get)._2).asInstanceOf[ArithExpr]
      }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
53
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
54 55 56 57 58 59 60 61 62 63
  
  def unaryTemporalOperator(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var], 
      var_ctx: Map[Var, (Int, Expr, Sort)]) = {
    val new_tvar_name = new_tname()
    val new_tsymbol = ctx.mkSymbol(new_tvar_name)
    val new_tvar = Var(new_tvar_name, "Int")
    val new_var_ctx = buildVarCtx(ctx, var_ctx, List(new_tvar))
    val new_texpr = new_var_ctx(new_tvar)._2.asInstanceOf[ArithExpr]
        
    val e_formula = toZ3(ctx, f, new_texpr, Some(new_tvar), new_var_ctx)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
64

Eugen Zalinescu's avatar
Eugen Zalinescu committed
65 66 67 68 69 70 71 72 73 74
    // replace old tvar in old texpr using old ctx by new timevar
    val upd_texpr = updateTime(texpr, tvar, var_ctx, new_var_ctx)
    val e_guard = ctx.mkLe(upd_texpr, new_texpr)
    
    (new_tsymbol, e_guard, e_formula)
  }

  def toZ3(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var], 
      var_ctx: Map[Var, (Int, Expr, Sort)]): BoolExpr = {
    // texpr is an expression e with the form given by the following grammar: 
75
    //   e ::= 0 | t | succ(e)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
76
    // tvar is Some(t) if e contains t or None otherwise
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91

    f match {
      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
Eugen Zalinescu's avatar
Eugen Zalinescu committed
92
        // TODO: support constants/free variables
93 94 95 96 97 98 99 100 101
        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) => {
Eugen Zalinescu's avatar
Eugen Zalinescu committed
102 103 104
        val (new_tsymbol, e_guard, e_formula) = 
          unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
        val body = ctx.mkImplies(e_guard, e_formula)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
105

Eugen Zalinescu's avatar
Eugen Zalinescu committed
106 107 108
        ctx.mkForall(Array(ctx.getIntSort()), Array(new_tsymbol), body, 
            0, null, null, null, null)
      }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
109

Eugen Zalinescu's avatar
Eugen Zalinescu committed
110 111 112 113
      case Finally(f1) => {
        val (new_tsymbol, e_guard, e_formula) = 
          unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
        val body = ctx.mkAnd(e_guard, e_formula)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
114

Eugen Zalinescu's avatar
Eugen Zalinescu committed
115 116 117 118 119 120 121 122 123 124 125 126
        ctx.mkExists(Array(ctx.getIntSort()), Array(new_tsymbol), body, 
            0, null, null, null, null)           
      }
            
      case Until(f1, f2) => {
        val ex_tvar_name = new_tname()
        val ex_tsymbol = ctx.mkSymbol(ex_tvar_name)
        val ex_tvar = Var(ex_tvar_name, "Int")
        val ex_var_ctx = buildVarCtx(ctx, var_ctx, List(ex_tvar))
        val ex_texpr = ex_var_ctx(ex_tvar)._2.asInstanceOf[ArithExpr]
        
        val ex_expr = toZ3(ctx, f2, ex_texpr, Some(ex_tvar), ex_var_ctx)
127

Eugen Zalinescu's avatar
Eugen Zalinescu committed
128 129 130 131 132 133 134 135 136 137
        val ex_upd_texpr = updateTime(texpr, tvar, var_ctx, ex_var_ctx)
        val ex_guard = ctx.mkLe(ex_upd_texpr, ex_texpr)
        
        val fa_tvar_name = new_tname()
        val fa_tsymbol = ctx.mkSymbol(fa_tvar_name)
        val fa_tvar = Var(fa_tvar_name, "Int")
        val fa_var_ctx = buildVarCtx(ctx, ex_var_ctx, List(fa_tvar))
        val fa_texpr = fa_var_ctx(fa_tvar)._2.asInstanceOf[ArithExpr]
        
        val fa_expr = toZ3(ctx, f1, fa_texpr, Some(fa_tvar), fa_var_ctx)
138

Eugen Zalinescu's avatar
Eugen Zalinescu committed
139 140 141 142 143
        val fa_upd_texpr = updateTime(ex_upd_texpr, tvar, ex_var_ctx, fa_var_ctx)
        val fa_g1 = ctx.mkLe(fa_upd_texpr, fa_texpr)
        val upd_ex_texpr = updateTime(ex_texpr, Some(ex_tvar), ex_var_ctx, fa_var_ctx)
        val fa_g2 = ctx.mkLt(fa_texpr, upd_ex_texpr)
        val fa_guard = ctx.mkAnd(fa_g1, fa_g2)
144

Eugen Zalinescu's avatar
Eugen Zalinescu committed
145 146 147 148 149 150 151 152 153 154
        
        val fa_body = ctx.mkImplies(fa_guard, fa_expr)
        val fa_fa_expr = ctx.mkForall(Array(ctx.getIntSort()), Array(fa_tsymbol), fa_body, 
            0, null, null, null, null)
            
        val ex_body1 = ctx.mkAnd(ex_expr, fa_fa_expr)
        val ex_body = ctx.mkAnd(ex_guard, ex_body1)
        
        ctx.mkExists(Array(ctx.getIntSort()), Array(ex_tsymbol), ex_body, 
            0, null, null, null, null)
155 156 157 158 159 160 161
      }

      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
        
Eugen Zalinescu's avatar
Eugen Zalinescu committed
162
        val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
163 164 165 166 167 168 169 170 171 172 173
        
        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
        
Eugen Zalinescu's avatar
Eugen Zalinescu committed
174
        val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
        
        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
206
  }
207 208 209 210 211 212 213 214 215 216 217 218

  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
219 220
  }
}