Z3 quantifizierte Formel mit der Implikation gibt unsättigt

Question

Ich bin noch neu zu Z3, und deshalb bin ich nicht sicher, warum ich für die folgende Formel ungeeignet bin; es sollte zumindest für diese ts_var-Arrays gesessen werden, von denen jedes Array-Element (Bitvektor) (von den 32 Array-Elementen) 1 an einer anderen Position der 32 Bits und Nullen in allen anderen Positionen hat (also das bvxor-Ergebnis wird anders sein)). Also irgendwelche Ratschläge oder Hinweise darüber, was ich falsch mache?

UPDATE: Wenn ich die Implikation in exp4 ((=> a! 1 a! 2)) in der umgekehrten Weise gemacht habe, wie es im Code ist, produzierte Z3 SAT! Aber das ist nicht was ich will. Ich möchte ein Array finden, dessen unterschiedliche Kombinationen von zwei Elementen zu einem unterschiedlichen Ergebnis führen, wenn sie XOR-verknüpft sind. Was ist die Implikation in dem Code, der immer noch Ungesunde gibt?

(assert (exists ((ts_var (Array (_ BitVec 5) (_ BitVec 32)))) 
    (forall ((k (_ BitVec 5)) (l (_ BitVec 5)) (m (_ BitVec 5)) (n (_ BitVec 5))) 
    (let ((a!1 (and (not (= k l)) 
        (not (= n m)) 
        (=> (= k m) (not (= l n))) 
        (=> (= l n) (not (= k m))))) 
      (a!2 (not (= (bvxor (select ts_var k) (select ts_var l)) 
         (bvxor (select ts_var m) (select ts_var n)))))) 
     (=> a!1 a!2) 
    ) 
    ) 
) 
) 
(check-sat) 

Ich schrieb ursprünglich den Code, die dieses Ergebnis mit dem C-API gab:

Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty) 
{ 
    Z3_symbol s = Z3_mk_string_symbol(ctx, name); 
    return Z3_mk_const(ctx, s, ty); 
} 
bv_w_sort  = Z3_mk_bv_sort (ctx, 32); 
index_w_sort  = Z3_mk_bv_sort (ctx, 5); 
array_sort  = Z3_mk_array_sort(ctx, index_w_sort, bv_w_sort); 

    ts_var = mk_var(ctx, "ts_var" , array_sort); 
    fp1 = mk_var(ctx, "fp1" , bv_w_sort); 
    fp2 = mk_var(ctx, "fp2" , bv_w_sort); 

fp1 = Z3_mk_bvxor(ctx, Z3_mk_select(ctx, ts_var, k) , Z3_mk_select(ctx, ts_var, l)); 
fp2 = Z3_mk_bvxor(ctx, Z3_mk_select(ctx, ts_var, m) , Z3_mk_select(ctx, ts_var, n)); 

cond_uniq = Z3_mk_not (ctx,Z3_mk_eq (ctx, fp1, fp2)); 

cond_k_neq_l = Z3_mk_not (ctx,Z3_mk_eq (ctx, k, l)); 
cond_n_neq_m = Z3_mk_not (ctx,Z3_mk_eq (ctx, n, m)); 

cond_l_neq_n = Z3_mk_not (ctx,Z3_mk_eq (ctx, l, n)); 
cond_k_neq_m = Z3_mk_not (ctx,Z3_mk_eq (ctx, k, m)); 

cond_k_eq_m = Z3_mk_eq (ctx, k, m); 
cond_l_eq_n = Z3_mk_eq (ctx, l, n); 

cond_imply1 = Z3_mk_implies (ctx, cond_k_eq_m, cond_l_neq_n); 
cond_imply2 = Z3_mk_implies (ctx, cond_l_eq_n, cond_k_neq_m); 

args[0]= cond_k_neq_l; 
args[1]= cond_n_neq_m; 
args[2]= cond_imply1; 
args[3]= cond_imply2; 
exp4 = Z3_mk_and(ctx, 4, args); 

bound[0] = (Z3_app) k; 
bound[1] = (Z3_app) l; 
bound[2] = (Z3_app) m; 
bound[3] = (Z3_app) n; 
bound4[0]= (Z3_app)ts_var; 
exp2 = Z3_mk_implies(ctx, exp4, cond_uniq); 
exp1 = Z3_mk_forall_const(ctx, 0, 4, bound, 0, 0, exp2); 
q = Z3_mk_exists_const(ctx, 0, 1, bound4, 0, 0, exp1); 
Z3_solver_assert(ctx, s, q); 

Ich bin auch nicht sicher, ob ich einige Muster über Variablen verwenden, wie hier vorgeschlagen: Does Z3 support variable-only patterns in quantified formulas?

Aber nach was ich in diesem Tutorial http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf gelesen habe Es scheint OK, nur keine Muster zu verwenden, oder?

Answer 1

Die Art und Weise Sie k holen, l, m und n ermöglicht Symmetrien. Zum Beispiel:

k = 0 
l = 1 
m = 1 
n = 0 

erfüllt Ihre Bedingung a!1, aber es funktioniert nicht offensichtlich „distinct“ Elemente für ts_var zu holen; was macht a!2 falsch. Daher wird Ihre gesamte Abfrage unsat.

Sie können die Definition Ihrer a!1 mit folgenden ersetzen:

(a!1 (distinct k l m n)) 

, die knapp diese vier Variablen sind alle unterschiedlich angeben würde. Mit dieser Änderung findet z3 tatsächlich ein Modell.