toz3.scala 7.54 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
    counter = counter + 1
    "t" + counter
  }

  def buildVarCtx(ctx: Context, var_ctx: Map[Var, (Int, Expr, Sort)], vars: List[Var]) = {
Eugen Zalinescu's avatar
Eugen Zalinescu committed
28 29 30
    val indices = (vars.size - 1) to 0 by - 1
    val newexprs = (for ((v,i) <- vars.zip(indices)) yield {
//    	count = count - 1;
31 32 33 34 35
      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
36
        ctx.mkFiniteDomainSort(v.typ, 1) // TODO: sort size?
Eugen Zalinescu's avatar
Eugen Zalinescu committed
37
      }
38 39 40 41 42 43 44 45 46 47
      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
48 49
  }
  
Eugen Zalinescu's avatar
Eugen Zalinescu committed
50
  def updateTime(texpr:ArithExpr, tvar: Option[Var], oldctx:Map[Var, (Int, Expr, Sort)], newctx:Map[Var, (Int, Expr, Sort)]) = {
51 52 53
       if (tvar.isEmpty) { texpr } else {
        texpr.substitute(oldctx(tvar.get)._2, newctx(tvar.get)._2).asInstanceOf[ArithExpr]
      }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
54
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
55 56 57 58 59 60 61 62 63 64
  
  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
65

Eugen Zalinescu's avatar
Eugen Zalinescu committed
66 67 68 69 70 71 72 73 74 75
    // 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: 
76
    //   e ::= 0 | t | succ(e)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
77
    // tvar is Some(t) if e contains t or None otherwise
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92

    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
93
        // TODO: support constants/free variables
94 95 96 97 98 99 100 101 102
        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
103 104 105
        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
106

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

Eugen Zalinescu's avatar
Eugen Zalinescu committed
111 112 113 114
      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
115

Eugen Zalinescu's avatar
Eugen Zalinescu committed
116 117 118 119 120 121 122 123 124 125 126 127
        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)
128

Eugen Zalinescu's avatar
Eugen Zalinescu committed
129 130 131 132 133 134 135 136 137 138
        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)
139

Eugen Zalinescu's avatar
Eugen Zalinescu committed
140 141 142 143 144
        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)
145

Eugen Zalinescu's avatar
Eugen Zalinescu committed
146 147 148 149 150 151 152 153 154 155
        
        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)
156 157 158 159 160 161 162
      }

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

      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
213
  }
214 215 216 217 218 219 220 221 222 223 224 225

  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
226 227
  }
}