Z3: API Java pour les formules quantifiées

Question

Je tente d'utiliser l'API JAVA de Z3 pour construire la formule suivante

(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))))) 

par le code suivant

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); 

où getFuncSymbol est ma propre fonction obtenir un FuncDecl qui est déclaré avant.

Malheureusement, je le mauvais résultat avec "laisser" et "un! 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))))) 

Je trouve que quelque chose de mal, "laisser ((un! 1", qui arrive à la ligne

body1 = ctx.mkImplies(andNode, eqX) 

Suis-je manque quelque chose? Merci

Answer 1

let-expressions sont introduites au cours d'impression assez pour tenter de rendre la sortie plus concise. ici, cela signifie simplement que chaque fois que le nom a!1 se produit dans la sortie, vous pouvez le remplacer par (and ...). Sémantiquement, cela ne fait pas de différence.