Различные результаты между Z3 двоичного и Z3 API

Question

Я пробую Z3 с примерами квантификаторов из http://rise4fun.com/Z3/tutorial/guide.

Два примера отлично работают с онлайн-версией Z3 (думаю, это будет Z3 4.0) .

(set-option :auto-config false) ; disable automatic self configuration
(set-option :mbqi false) ; disable model-based quantifier instantiation
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (forall ((x Int))
                (! (= (f (g x)) x)
                   :pattern ((f (g x))))))
(assert (= (g a) c))
(assert (= (g b) c))
(assert (not (= a b)))
(check-sat)

а также

(set-option :auto-config false) ; disable automatic self configuration
(set-option :mbqi false) ; disable model-based quantifier instantiation
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int) 
(assert (forall ((x Int))
            (! (= (f (g x)) x)
               :pattern ((g x)))))
(assert (= (g a) c))
(assert (= (g b) c))
(assert (not (= a b)))
(check-sat)

Разница в том, что мы использовали шаблон для "полного утверждения". Результат должен быть "неизвестным" и "ненасыщенным".

Я использую версию Z3 3.2 для Linux с http://research.microsoft.com/projects/z3/z3-3.2.tar.gz

Я попробовал два примера через бинарный z3

./z3 -smt2 ex1.smt

./z3 -smt2 ex2.smt

Результат верный.

Тем не менее, когда я использовал ocaml api, оба примера являются "неизвестными".

Я пробовал:

Z3.parse_smtlib2_file ctx "ex2.smt" [||] [||] [||] [||];;

а также

let mk_unary_app ctx f x = Z3.mk_app ctx f [|x|];;
let example () = 
  let ctx = Z3.mk_context_x [|("MBQI","false")|] in 
  let int = Z3.mk_int_sort ctx in 
  let f = Z3.mk_func_decl ctx (Z3.mk_string_symbol ctx "f") [|int|] int in
  let g = Z3.mk_func_decl ctx (Z3.mk_string_symbol ctx "g") [|int|] int in
  let a = Z3.mk_const ctx (Z3.mk_string_symbol ctx "a") int in 
  let b = Z3.mk_const ctx (Z3.mk_string_symbol ctx "b") int in 
  let c = Z3.mk_const ctx (Z3.mk_string_symbol ctx "c") int in 
  let sym = Z3.mk_int_symbol ctx 0 in
  let bv = Z3.mk_bound ctx 0 int in
  let pat = Z3.mk_pattern ctx [| Z3.mk_app ctx g [| bv |]  |]  in
  let forall = Z3.mk_forall ctx 0 [| pat |] [|int|] [|sym|] 
    (Z3.mk_not ctx (Z3.mk_eq ctx (Z3.mk_app ctx f [|Z3.mk_app ctx g [|bv|]|]) bv)) in 
  Z3.assert_cnstr ctx forall;
  Z3.assert_cnstr ctx (Z3.mk_eq ctx (mk_unary_app ctx g a) c);
  Z3.assert_cnstr ctx (Z3.mk_eq ctx (mk_unary_app ctx g b) c);
  Z3.assert_cnstr ctx (Z3.mk_not ctx (Z3.mk_eq ctx a b));
  Z3.check ctx ;;

Спасибо!

Answer 1

В коде OCaml есть опечатка.

let forall = Z3.mk_forall ctx 0 [| pat |] [| int |] [| sym |]

(Z3.mk_not ctx (Z3.mk_eq ctx (Z3.mk_app ctx f [|Z3.mk_app ctx g [|bv|]|]) bv))

Проблема заключается в Z3.mk_not, ! на входе SMT нет отрицания. В SMT 2.0 ! используется для "прикрепления" атрибутов к формулам. В приведенном выше примере атрибут является шаблоном.