how to use z3 c api to solve array theory

0
votes

I'd like to use z3 c api to solve array theory question like this, there are five elements in one array, namely array[5], select(a,i,v1) = select(a,j,v2), v1 is not equal to v2 and i is equal to j, so this should be unsatisfiable solved by z3. the question is how to express v1 is not equal to v2? The example from C api just gives one satisfiable example, when unsatisfied instance such as in the same index of array giving different value, so I tried to use Z3_mk_neq(ctx, sel1, sel2), which cannot be compiled, anyone knows how to do that?

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);
2
arraystheoryz3
I think c++ api is better to solve this question. - Million

2 Answers

0
votes

Z3_mk_const(ctx, s, array_sort) declare a variable of type (Array Int Int),you make select on array[i] and array[j], these two are different array.If you want to prove select(a,i,v1) = select(a,j,v2), you should use same variable.

v1 is not equal to v2, you can try this: Z3_mk_not(ctx, Z3_mk_eq(ctx, v1, v2)); The following code to prove the result is "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)
0
votes

It is better to use the c++ api solving it easier. The code as below

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;