z3バイナリとz3 apiの結果が異なります

Question

私はhttp://rise4fun.com/Z3/tutorial/guideから数量化の例でZ3を試しています。

この2つの例は、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) 

の違いは、 "FORALL" アサーションに使用するパターンです。結果は、 "unknow"と "unsat"にする必要があります。

私はZ3バイナリ

./z3 -smt2 ex1.smt

./z3介して2つの例を試みhttp://research.microsoft.com/projects/z3/z3-3.2.tar.gz

からZ3 3.2のLinuxバージョンを使用しています - smt2 ex2.smt

結果は正しいです。

しかし、私がocaml apiを使用していたとき、2つの例はどちらも「不明」です。

私が試してみた：

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 [|パット|] [| 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では、属性を数式に「アタッチ」するのに!が使用されます。上記の例では、属性はパターンです。