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