Количественная формула Z3 с предполагаемым значением unsat

Я все еще новичок в Z3 и, следовательно, не уверен, почему меня не устраивает приведенная ниже формула; он должен быть установлен, по крайней мере, для тех массивов ts_var, из которых каждый элемент массива (bitvector) (из 32 элементов массива) имеет 1 в другой позиции из 32 бит и нули во всех других позициях (поэтому результат bvxor будет другим ). Итак, какие-нибудь советы или намеки на то, что я делаю не так?

ОБНОВЛЕНИЕ: когда я сделал импликацию в exp4 ((=> a! 1 a! 2)) способом, противоположным тому, что в коде, Z3 произвел SAT! Но я не этого хочу. Я хочу найти массив, различные комбинации из двух элементов которого дают разные результаты, когда они объединяются вместе с помощью XOR. Что подразумевается в коде, который все еще дает unsat.

(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 Кажется, нормально просто не использовать какие-либо шаблоны, верно?


arrays z3 quantifiers
person user3131978    schedule 16.12.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

То, как вы выбираете 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 действительно нашел модель.

person alias    schedule 18.12.2016
comment
Большое спасибо! Это сделало именно то, что я хотел. - person user3131978; 19.12.2016
comment
И спасибо, что указали на недостаток в том, как я описал условие, допускающее симметрию. - person user3131978; 19.12.2016
comment
Я хотел разрешить условную симметрию, но не ту, которую вы упомянули. т.е. я хочу, чтобы k = 0, l = 1; m = 0, n = 2, например, поэтому мне пришлось добавить условия, чтобы предотвратить случай, который вы указали, и теперь он работает идеально. - person user3131978; 19.12.2016
comment
@ user3131978 Совершенно верно! Ваши четкие ограничения, вероятно, слабее, чем требование, чтобы все четыре были разными. Но да, в конечном итоге, первоначальная проблема была unsat потому, что она была слишком либеральной. - person alias; 20.12.2016