我对Z3还是陌生的,因此不确定为什么我对下面的公式感到不满意。至少应为那些ts_var数组坐下,其中(32个数组元素中的)每个数组元素(位向量)在32位的不同位置具有1,在所有其他位置具有零(因此bvxor结果将不同) )。那么关于我在做什么错的任何建议或提示?
更新:当我以相反的方式在exp4((=> a!1 a!2))中进行隐式运算时,Z3产生了SAT!但这不是我想要的。我想找到一个数组,当两个元素XOR在一起时,它的2个元素的不同组合给出不同的结果。这仍然是代码中的隐含含义。
(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);
我也不确定是否必须对变量使用某些模式,如此处建议的那样:Z3是否支持量化公式中的仅变量模式?
但是根据我在本教程中所读的内容,http://citeseerx.ist.psu.edu/viewdoc/download?doi = 10.1.1.225.8231&rep = rep1&type = pdf似乎不使用任何模式似乎还可以,对吗?
您选择的方式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确实找到了一个模型。
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句