toz3.scala 9.16 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
object toZ3 extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
13 14 15

  type VarCtx = Map[Var, (Option[Int], Expr, Sort)]

16 17 18 19 20 21 22
  def succ(ctx: Context, e: ArithExpr) = {
    val One = ctx.mkInt(1)
    ctx.mkAdd(e, One)
  }

  var counter = 0

Christian Müller's avatar
Christian Müller committed
23
  // TODO: how to not make this static?
24 25
  val fun_ctx = new HashMap[String, FuncDecl]()

Eugen Zalinescu's avatar
Eugen Zalinescu committed
26
  def new_tname() = {
27 28 29 30
    counter = counter + 1
    "t" + counter
  }

Christian Müller's avatar
Christian Müller committed
31
  def buildVarCtx(ctx: Context, var_ctx: VarCtx, vars: List[Var]): VarCtx = {
32 33 34
    val indices = (vars.size - 1) to 0 by -1
    val newexprs = (for ((v, i) <- vars.zip(indices)) yield {
      //    	count = count - 1;
35 36 37 38 39
      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
40
        ctx.mkFiniteDomainSort(v.typ, 1) // TODO: sort size?
Eugen Zalinescu's avatar
Eugen Zalinescu committed
41
      }
Christian Müller's avatar
Christian Müller committed
42
      v -> (Some(i), ctx.mkBound(i, sort), sort)
43 44
    }) toMap

Christian Müller's avatar
Christian Müller committed
45
    // if the index is defined, increment, otherwise use the expr (which is a constant f.e.)
46
    val oldvars = (for ((v, (i, e, s)) <- var_ctx) yield {
Christian Müller's avatar
Christian Müller committed
47 48 49 50 51 52 53
      if (i.isDefined) {
        val newi = i.get + vars.size
        val newbound = ctx.mkBound(newi, s)
        v -> (Some(newi), newbound, s)
      } else {
        v -> (i, e, s)
      }
54 55 56
    })

    newexprs ++ oldvars
Eugen Zalinescu's avatar
Eugen Zalinescu committed
57
  }
58

Christian Müller's avatar
Christian Müller committed
59
  def updateTime(texpr: ArithExpr, tvar: Option[Var], oldctx: VarCtx, newctx: VarCtx) = {
60 61 62
    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

  def unaryTemporalOperator(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var],
Christian Müller's avatar
Christian Müller committed
66
                            var_ctx: VarCtx) = {
Eugen Zalinescu's avatar
Eugen Zalinescu committed
67 68 69 70 71
    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]
72

Eugen Zalinescu's avatar
Eugen Zalinescu committed
73
    val e_formula = toZ3(ctx, f, new_texpr, Some(new_tvar), new_var_ctx)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
74

Eugen Zalinescu's avatar
Eugen Zalinescu committed
75 76 77
    // 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)
78

Eugen Zalinescu's avatar
Eugen Zalinescu committed
79 80 81
    (new_tsymbol, e_guard, e_formula)
  }

82
  def toZ3(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var],
Christian Müller's avatar
Christian Müller committed
83
           var_ctx: VarCtx): BoolExpr = {
Eugen Zalinescu's avatar
Eugen Zalinescu committed
84
    // texpr is an expression e with the form given by the following grammar: 
85
    //   e ::= 0 | t | succ(e)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
86
    // tvar is Some(t) if e contains t or None otherwise
87 88 89

    f match {
      case Fun(name, ind, params) => {
90 91 92 93 94
        val pi = if (ind.isDefined) "_" + ind.get else ""
        val indexedname = name + pi

        var fdecl = fun_ctx.get(indexedname)

95 96 97 98 99
        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]
100 101
          fdecl = ctx.mkFuncDecl(indexedname, new_sorts, ctx.getBoolSort())
          fun_ctx.put(indexedname, fdecl)
102 103 104
        }

        // all variables should be quantified, so they should be part of var_ctx
Eugen Zalinescu's avatar
Eugen Zalinescu committed
105
        // TODO: support constants/free variables
106 107 108 109 110 111 112 113 114
        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) => {
115
        val (new_tsymbol, e_guard, e_formula) =
Eugen Zalinescu's avatar
Eugen Zalinescu committed
116 117
          unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
        val body = ctx.mkImplies(e_guard, e_formula)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
118

119 120
        ctx.mkForall(Array(ctx.getIntSort()), Array(new_tsymbol), body,
          0, null, null, null, null)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
121
      }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
122

Eugen Zalinescu's avatar
Eugen Zalinescu committed
123
      case Finally(f1) => {
124
        val (new_tsymbol, e_guard, e_formula) =
Eugen Zalinescu's avatar
Eugen Zalinescu committed
125 126
          unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
        val body = ctx.mkAnd(e_guard, e_formula)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
127

128 129
        ctx.mkExists(Array(ctx.getIntSort()), Array(new_tsymbol), body,
          0, null, null, null, null)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
130
      }
131

Eugen Zalinescu's avatar
Eugen Zalinescu committed
132 133 134 135 136 137
      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]
138

Eugen Zalinescu's avatar
Eugen Zalinescu committed
139
        val ex_expr = toZ3(ctx, f2, ex_texpr, Some(ex_tvar), ex_var_ctx)
140

Eugen Zalinescu's avatar
Eugen Zalinescu committed
141 142
        val ex_upd_texpr = updateTime(texpr, tvar, var_ctx, ex_var_ctx)
        val ex_guard = ctx.mkLe(ex_upd_texpr, ex_texpr)
143

Eugen Zalinescu's avatar
Eugen Zalinescu committed
144 145 146 147 148
        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]
149

Eugen Zalinescu's avatar
Eugen Zalinescu committed
150
        val fa_expr = toZ3(ctx, f1, fa_texpr, Some(fa_tvar), fa_var_ctx)
151

Eugen Zalinescu's avatar
Eugen Zalinescu committed
152 153 154 155 156
        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)
157

Eugen Zalinescu's avatar
Eugen Zalinescu committed
158
        val fa_body = ctx.mkImplies(fa_guard, fa_expr)
159 160 161
        val fa_fa_expr = ctx.mkForall(Array(ctx.getIntSort()), Array(fa_tsymbol), fa_body,
          0, null, null, null, null)

Eugen Zalinescu's avatar
Eugen Zalinescu committed
162 163
        val ex_body1 = ctx.mkAnd(ex_expr, fa_fa_expr)
        val ex_body = ctx.mkAnd(ex_guard, ex_body1)
164 165 166

        ctx.mkExists(Array(ctx.getIntSort()), Array(ex_tsymbol), ex_body,
          0, null, null, null, null)
167 168 169 170 171 172
      }

      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
173

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
        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
185

Eugen Zalinescu's avatar
Eugen Zalinescu committed
186
        val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
187

188 189 190 191 192 193 194 195 196 197
        val e1 = toZ3(ctx, f1, upd_texpr, tvar, newctx)

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

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

Eugen Zalinescu's avatar
Eugen Zalinescu committed
199 200 201 202 203
      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)
      }
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220

      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)
      }
Christian Müller's avatar
Christian Müller committed
221

Christian Müller's avatar
Christian Müller committed
222 223 224 225 226 227
      case True => {
        ctx.mkTrue()
      }
      case False => {
        ctx.mkFalse()
      }
228
    }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
229
  }
230

Christian Müller's avatar
Christian Müller committed
231
  def translate(f: Formula, ctx: Context) = {
Christian Müller's avatar
Christian Müller committed
232 233
    //    logger.info(s"Using formula:\n$f")

Christian Müller's avatar
Christian Müller committed
234 235 236
    if (!f.freeVars().isEmpty) {
      logger.error(s"Cannot check - formula contains free variables ${f.freeVars()}")
    }
Christian Müller's avatar
Christian Müller committed
237

Christian Müller's avatar
Christian Müller committed
238
    fun_ctx.clear()
239
    val expr = toZ3(ctx, f, ctx.mkInt(0), None, Map())
Christian Müller's avatar
Christian Müller committed
240
    //    logger.info(s"Built Z3 expression:\n$expr")
Christian Müller's avatar
Christian Müller committed
241
    expr
242 243
  }

Christian Müller's avatar
Christian Müller committed
244
  def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
Christian Müller's avatar
Christian Müller committed
245 246
    //    logger.info(s"Using formula:\n${f.pretty()}")

Christian Müller's avatar
Christian Müller committed
247 248 249
    if (!f.freeVars().isEmpty) {
      logger.error(s"Cannot check - formula contains free variables ${f.freeVars()}")
    }
Christian Müller's avatar
Christian Müller committed
250

Christian Müller's avatar
Christian Müller committed
251
    fun_ctx.clear()
252
    val expr = toZ3(ctx, f, ctx.mkInt(0), None, varctx)
Christian Müller's avatar
Christian Müller committed
253
    //    logger.info(s"Built Z3 expression:\n$expr")
Christian Müller's avatar
Christian Müller committed
254
    expr
Eugen Zalinescu's avatar
Eugen Zalinescu committed
255
  }
Christian Müller's avatar
Christian Müller committed
256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273

  def printModel(model: Model) = {

    val sb = new StringBuilder()

    val consts = model.getConstDecls()

    val vals = consts.map(_.apply())
    val typedvals = vals.groupBy(_.getSort)

    sb ++= "Universe:\n"
    for ((k, v) <- typedvals) {
      sb ++= s"Type $k: ${v.mkString(",")}\n"
    }

    sb ++= "Evaluations:\n"
    val sorted = model.getFuncDecls().sortBy(_.getName.toString())
    for (f <- sorted) {
Christian Müller's avatar
Christian Müller committed
274 275
      sb ++= f.getName + f.getDomain.mkString("(",", ",")") + "\n"
      
Christian Müller's avatar
Christian Müller committed
276 277 278 279 280 281 282 283 284 285 286 287 288 289
      val interp = model.getFuncInterp(f)
      val entries = interp.getEntries
      for (e <- entries) {
        val args = for (arg <- e.getArgs.toList) yield {
          arg.getSort + " " + arg
        }
        sb ++= f.getName + args.mkString("(", ", ", ")") + " = " + e.getValue() + "\n"
      }

      val emptyargs = List.fill(f.getArity)("_")
      sb ++= f.getName + emptyargs.mkString("(", ", ", ")") + " = " + interp.getElse() + "\n\n"
    }
    sb.toString()
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
290
}