Can the mkOr(Expr<BoolSort> ... t) fuction in the Z3 Java Api get a list as input?

user_8627180 0
Viewed 49

Unfortunately, I cannot post the entire code here, because i am programming (modelling) in a DSL that is build on top of Java. The question does not necessary require that though:

I am trying to create a longer Or-Expression like: p == 1 Or p==2 Or p==3 and so on. I have a list of BoolExpr, which contains the list of those EQ-expressions (i.e. p==1, etc).

In python i could now just give this list of expressions to the mkOr method of the API and that was it. My code snippet below though complains that list is not a subtype of BoolExpr.

list<BoolExpr> eqExprList = new arraylist<BoolExpr>;

// populate this list with p==1, p==2 etc.

MyContext.mkOr(eqExrList); // this produces the error

So the question is basically, whether it should normally (in a real java) work like this or whether I am misunderstanding the API documentation: https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_context.html#aea714fc46f4c625ecc15397522099330

smt z3 solver java
1 Answers

Yes you can, but it has to be a regular array; not an ArrayList. So, you should first convert it to an array:

import com.microsoft.z3.*;
import java.util.*;

public class Z3Test {

  public static void main(String[] args) {
      Context ctx = new Context();

      IntExpr x = ctx.mkIntConst("x");
      IntExpr y = ctx.mkIntConst("y");
      IntExpr z = ctx.mkIntConst("z");

      ArrayList<BoolExpr> eqExprList = new ArrayList<BoolExpr>();
      eqExprList.add(ctx.mkEq(x, y));
      eqExprList.add(ctx.mkEq(y, z));

      Solver s = ctx.mkSolver();
      s.add(ctx.mkOr(eqExprList.toArray(new BoolExpr[eqExprList.size()])));

      System.out.println(s);
  }
}

This prints:

(declare-fun z () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(assert (or (= x y) (= y z)))

So the part you're missing is:

ctx.mkOr(eqExprList.toArray(new BoolExpr[eqExprList.size()]))

which makes a regular array out of an ArrayList, which can then be fed to the mkOr function.

user_9363100
Related