如何使用z3 c api解决数组理论答案

【问题标题】：how to use z3 c api to solve array theory如何使用z3 c api解决数组理论
【发布时间】：2015-08-16 07:04:34
【问题描述】：

我想用z3 c api来解决这样的数组理论问题，一个数组中有五个元素，即array[5]，select(a,i,v1) = select(a,j,v2 )，v1 不等于 v2，i 等于 j，所以这应该是 z3 无法满足的。问题是如何表示v1不等于v2？ C api 中的示例仅给出了一个可满足的示例，当不满足的实例（例如在数组的同一索引中给出不同的值）时，我尝试使用无法编译的Z3_mk_neq(ctx, sel1, sel2),，有人知道该怎么做吗？

Z3_context ctx; Z3_sort int_sort, array_sort;

ctx = mk_context();
Z3_ast array[5];
for(i=0; i<5; i++){
Z3_symbol s = Z3_mk_int_symbol(ctx,i);
array[i] = Z3_mk_const(ctx,s,array_sort);
}
array[i]         = Z3_mk_store(ctx, array[i], i, v1);
array[j]         = Z3_mk_store(ctx, array[j], j, v2);

sel1        = Z3_mk_select(ctx, array[i], i);
sel2        = Z3_mk_select(ctx, array[j], j);
antecedent  = Z3_mk_eq(ctx, array[i], array[j]);
ds[0]       = Z3_mk_eq(ctx, i, i1);
ds[1]       = Z3_mk_eq(ctx, j, i1);
ds[2]       = Z3_mk_eq(ctx, sel1, sel2);
consequent  = Z3_mk_or(ctx, 3, ds);

【问题讨论】：

我觉得c++ api更适合解决这个问题。

标签： arrays theory z3

【解决方案1】：

最好使用 c++ api 解决它更容易。代码如下

context c;
unsigned i=0,j;
expr_vector T(c);
solver s(c);

for(; i<20; i++){
    std::stringstream Tname;
    Tname<<"Tname_"<<i;
    T.push_back(c.int_const(Tname.str().c_str()));
}

for(i=0; i<20; i++){
    for(j=0; j<20;j++){
        if(j == i){
            s.add(T[i] != T[j]);

        }
    }
}
std::cout<<s<<"\n"<<s.check()<<std::endl;

【讨论】：

【解决方案2】：

Z3_mk_const(ctx, s, array_sort)声明一个(Array Int Int)类型的变量，你在array[i]和array[j]上做select，这两个是不同的array。如果你想证明select(a,i,v1) = select (a,j,v2)，你应该使用相同的变量。

v1 不等于 v2，你可以试试这个：Z3_mk_not(ctx, Z3_mk_eq(ctx, v1, v2)); 以下代码证明结果是“unsat”。

(declare-const a (Array Int Int))
(declare-const i Int)
(declare-const j Int)
(declare-const v1 Int)
(declare-const v2 Int)
(assert (= i j))
(assert (not (= v1 v2)))
(assert (= (store a i v1) a))
(assert (= (store a j v2) a))
(assert (= (select a i) (select a j)))
(check-sat)

【讨论】：