2
我正在尝试Z3与从http://rise4fun.com/Z3/tutorial/guide量词的例子。z3二进制和z3 api之间的不同结果
这两个例子适用于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” 断言模式。结果应该是“未知”和“不可接受”。
我使用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 ;;
谢谢!
非常感谢。但是,这里仍然存在混淆。使用解析器的结果是“未知”,应该是“不”。并且,以我的打字稿为例,打开“MBQI”后“不合格”。你能提出一篇关于基于模型的量词实例的论文吗? – Naituida
您的问题中的两个示例来自Z3指南。第一个例子的目的是证明基于模式的启发式量词实例化的局限性。也就是说,当模式'(f(g x))'被提供并且MBQI被禁止时,Z3将不能证明公式不成立。未知的答案是预期的答案。关于MBQI论文,在http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf中提供了一个简介,实际的算法基于以下理论思想:http:// research.microsoft.com/en-us/um/people/leonardo/ci.pdf –