Z3量化公式暗示给予不足

我还是Z3的新手，因此不确定为什么我不满足下面的公式;它应该至少适用于那些ts_var数组，每个数组元素（bitvector）（32个数组元素）在32位的不同位置上有1，而在所有其他位置上有0（所以bvxor结果将会不同）。那么对于我在做什么的任何建议或提示都是错误的？当我在exp4（（=> a！1 a！2））中以与代码中相反的方式做了暗示的时候，Z3产生了SAT！但这不是我想要的。我想找到一个数组，其中两个元素的不同组合在它们异或时会给出不同的结果。代码中的含义仍然不尽如人意。Z3量化公式暗示给予不足

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

我原来写使用C-API，它给了这个结果代码：

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

我也不能确定我是否有使用过变量的一些模式，比如这里建议：Does Z3 support variable-only patterns in quantified formulas?

但根据我在本教程中读到的内容http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf 这似乎确定只是不使用任何模式，对吧？

来源

2016-12-16 user3131978

您选择的方式k，l，m和n允许对称。例如：

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

满足您的条件a!1，但它显然无法挑选ts_var“独特”的元素;这使得a!2错误。因此，您的整个查询变为unsat。

您可以用下面的更换你的a!1的定义：

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

这将简洁地陈述这四个变量都是不同的。随着这一变化，z3确实找到了一个模型。

来源

2016-12-18 03:46:54

非常感谢！这做了我想要的。 – user3131978

感谢您指出我如何描述允许对称的情况的缺陷。 – user3131978

我想让条件对称，但不是你提到的。即我想允许k = 0，l = 1;例如m = 0，n = 2，所以我必须添加条件来防止您指出的情况，并且它现在完美无缺。 – user3131978

Z3量化公式暗示给予不足

回答

相关问题