toz3.scala 7.87 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 = {
Christian Müller's avatar
Christian Müller committed
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
  }
Christian Müller's avatar
Christian Müller committed
58

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

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

Christian Müller's avatar
Christian Müller committed
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) => {
Christian Müller's avatar
Christian Müller committed
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]
Christian Müller's avatar
Christian Müller committed
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) => {
Christian Müller's avatar
Christian Müller committed
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

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

Christian Müller's avatar
Christian Müller committed
128 129
        ctx.mkExists(Array(ctx.getIntSort()), Array(new_tsymbol), body,
          0, null, null, null, null)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
130
      }
Christian Müller's avatar
Christian Müller committed
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]
Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
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]
Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
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
Christian Müller's avatar
Christian Müller committed
173

Eugen Zalinescu's avatar
Eugen Zalinescu committed
174
        val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
Christian Müller's avatar
Christian Müller committed
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
Christian Müller's avatar
Christian Müller committed
185

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

188 189 190 191 192 193 194 195 196 197 198 199
        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)
      }
Christian Müller's avatar
Christian Müller committed
200

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

      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
224
  }
225

Christian Müller's avatar
Christian Müller committed
226 227 228
  def translate(f: Formula, ctx: Context) = {
    logger.info(s"Using formula:\n$f")
    fun_ctx.clear()
229
    val expr = toZ3(ctx, f, ctx.mkInt(0), None, Map())
Christian Müller's avatar
Christian Müller committed
230 231
    logger.info(s"Built Z3 expression:\n$expr")
    expr
Christian Müller's avatar
Christian Müller committed
232 233
  }

Christian Müller's avatar
Christian Müller committed
234 235 236
  def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
    logger.info(s"Using formula:\n${f.pretty()}")
    fun_ctx.clear()
Christian Müller's avatar
Christian Müller committed
237
    val expr = toZ3(ctx, f, ctx.mkInt(0), None, varctx)
Christian Müller's avatar
Christian Müller committed
238 239
    logger.info(s"Built Z3 expression:\n$expr")
    expr
Eugen Zalinescu's avatar
Eugen Zalinescu committed
240 241
  }
}