Z3: Java API for quantified formulas

Question

I am trying to use the JAVA API of Z3 to construct the following formula

    (assert (forall ((x_0 fcn_sort_2) (x_1 fcn_sort_2))
                    (=> (and (= (domain x_0) 
                                (domain x_1))
                             (forall ((y Int))
                                     (= (alpha x_0 y) 
                                        (alpha x_1 y))))))
                        (= x_0 x_1)))))

by the following code

Sort[] types1 = new Sort[2]; // for x_0 and x_1
Expr[] xs1 = new Expr[2];        
for (int j = 0; j < 2; j++) {
    types1[j] = this.getZ3Sort("fcn_sort_2");        
    xs1[j] = ctx.mkConst(ctx.mkSymbol("x_" + Integer.toString(j)), types1[j]);        
}    
Sort[] types2 = new Sort[1]; // for y
Expr[] xs2 = new Expr[1];    
types2[0] = ctx.mkIntSort();
xs2[0] = ctx.mkConst(ctx.mkSymbol("y"), types2[0]);
FuncDecl alpha_fcn = this.getFuncSymbol("alpha");
Expr[] arg0 = new Expr[] { xs1[0], xs2[0] };
Expr[] arg1 = new Expr[] { xs1[1], xs2[0] };
BoolExpr 
    // (= (alpha x_0 y) (alpha x_1 y))
    body2 = ctx.mkEq(ctx.mkApp(alpha_fcn, arg0), ctx.mkApp(alpha_fcn, arg1)), 
    // forall ((y Int)) ...
    bf2 = ctx.mkForall(xs2, body2, 1, null, null, null, null); 
FuncDecl domain_fcn = this.getFuncSymbol("domain");
BoolExpr
    // (= x_0 x_1)
    eqX = ctx.mkEq(xs1[0], xs1[1]), 
    // (= (domain x_0) (domain x_1))
    eqDo = ctx.mkEq(ctx.mkApp(domain_fcn, new Expr[] {xs1[0]}), ctx.mkApp(domain_fcn, new Expr[] {xs1[1]})), 
    // (and ...)
    andNode = ctx.mkAnd(eqDo, bf2),         
    // (=> ...)
    body1 = ctx.mkImplies(andNode, eqX),
    // (forall ((x_0 ...) (x_1 ...))
    bf1 = ctx.mkForall(xs1, body1, 1, null, null, null, null);

where getFuncSymbol is my own function to get a FuncDecl which is declared before.

Unfortunately, I have the wrong result with "let" and "a!1"

(assert (forall ((x_0 fcn_sort_2) (x_1 fcn_sort_2))
  (let ((a!1 (and (= (domain_fcn_sort_2 x_0) (domain_fcn_sort_2 x_1))
                  (forall ((y Int))
                    (= (alpha_fcn_sort_2 x_0 y) (alpha_fcn_sort_2 x_1 y))))))
    (=> a!1 (= x_0 x_1)))))

I found that something wrong, "let ((a!1", happens at the line

    body1 = ctx.mkImplies(andNode, eqX)

Am I missing something? Thank you

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2016-01-25T19:56:38

let-expressions are introduced during pretty-printing in an attempt to make the output more concise. Here, it simply means that whenever the name a!1 occurs in the output, you can replace it with (and ...). Semantically, this doesn't make a difference.

Z3: Java API for quantified formulas

1 Answers