首页 文章

Z3 MBQI针对同一模型的API和SMT-LIB之间的不同行为

提问于
浏览 次
1

我正在使用Z3来检查一些量化的公式 . 如果我通过Z3的Java API断言公式，如果公式不合格，MBQI引擎可能不会收敛 . 我知道我的公式不是FOL的片段，已知它是可判定的，但是如果我通过Z3的smt-lib接口输入相同的公式，它会很快产生答案 . 我怀疑某些选项不是通过通常使用正常SMTLIB输入激活的API设置的，或者我没有通过API向公式添加重要的元信息 .

以下SMTLIB会话中的断言直接来自BoolExpr的toString，我通过API断言：

(set-option :smt.mbqi true)
(set-option :smt.pull-nested-quantifiers true)
(set-option :smt.mbqi.trace true)
(declare-fun R (Int Int) Bool)
(declare-const |'x| Int)
(declare-const |'y| Int)
(assert 
  (let ((a!1 (forall ((|'x0| Int) (|'y0| Int))
         (= (R |'x0| |'y0|)
            (and (forall ((|'y1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'y0| 0) (= |'y1| 1))
                                       (and (= |'y0| 1) (= |'y1| 3))
                                       (and (= |'y0| 2) (= |'y1| 3))
                                       (and (= |'y0| 0) (= |'y1| 2)))))
                         (a!2 (exists ((|'x1| Int))
                                (and (or (and (= |'x0| 3) (= |'x1| 0))
                                         (and (= |'x0| 1) (= |'x1| 3))
                                         (and (= |'x0| 1) (= |'x1| 2))
                                         (and (= |'x0| 2) (= |'x1| 0))
                                         (and (= |'x0| 0) (= |'x1| 1)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2)))
                 (forall ((|'x1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'x0| 3) (= |'x1| 0))
                                       (and (= |'x0| 1) (= |'x1| 3))
                                       (and (= |'x0| 1) (= |'x1| 2))
                                       (and (= |'x0| 2) (= |'x1| 0))
                                       (and (= |'x0| 0) (= |'x1| 1)))))
                         (a!2 (exists ((|'y1| Int))
                                (and (or (and (= |'y0| 0) (= |'y1| 1))
                                         (and (= |'y0| 1) (= |'y1| 3))
                                         (and (= |'y0| 2) (= |'y1| 3))
                                         (and (= |'y0| 0) (= |'y1| 2)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2))))))))
 (and (= |'x| 0) (= |'y| 0) (R |'x| |'y|) a!1)))
(check-sat)

有趣的是，当我通过Z3的SMTLIB接口运行上述内容时，MBQI跟踪很短，看起来像这样：

(smt.mbqi "started")
(smt.mbqi :checking k!37)
(smt.mbqi :failed k!37)
(smt.mbqi :num-failures 1)
...
(smt.mbqi "started")
(smt.mbqi :checking k!37)
(smt.mbqi :failed k!37)
(smt.mbqi :num-failures 1)
unsat

但是，通过API运行时的跟踪（以及相同的求解器选项）如下所示：

(smt.mbqi "started")
(smt.mbqi :failed null)
(smt.mbqi :num-failures 1)
(smt.mbqi "started")
(smt.mbqi :failed null)
(smt.mbqi :num-failures 1)

“null”引用是否表明我在API方面做错了什么？

z3

1 回答

  • 1

    我在复制失败行为方面遇到了一些麻烦 . 以下是我如何模拟API行为：

    from z3 import *

spec = """
(declare-fun R (Int Int) Bool)
(declare-const |'x| Int)
(declare-const |'y| Int)
(assert 
  (let ((a!1 (forall ((|'x0| Int) (|'y0| Int))
         (= (R |'x0| |'y0|)
            (and (forall ((|'y1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'y0| 0) (= |'y1| 1))
                                       (and (= |'y0| 1) (= |'y1| 3))
                                       (and (= |'y0| 2) (= |'y1| 3))
                                       (and (= |'y0| 0) (= |'y1| 2)))))
                         (a!2 (exists ((|'x1| Int))
                                (and (or (and (= |'x0| 3) (= |'x1| 0))
                                         (and (= |'x0| 1) (= |'x1| 3))
                                         (and (= |'x0| 1) (= |'x1| 2))
                                         (and (= |'x0| 2) (= |'x1| 0))
                                         (and (= |'x0| 0) (= |'x1| 1)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2)))
                 (forall ((|'x1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'x0| 3) (= |'x1| 0))
                                       (and (= |'x0| 1) (= |'x1| 3))
                                       (and (= |'x0| 1) (= |'x1| 2))
                                       (and (= |'x0| 2) (= |'x1| 0))
                                       (and (= |'x0| 0) (= |'x1| 1)))))
                         (a!2 (exists ((|'y1| Int))
                                (and (or (and (= |'y0| 0) (= |'y1| 1))
                                         (and (= |'y0| 1) (= |'y1| 3))
                                         (and (= |'y0| 2) (= |'y1| 3))
                                         (and (= |'y0| 0) (= |'y1| 2)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2))))))))
 (and (= |'x| 0) (= |'y| 0) (R |'x| |'y|) a!1)))
"""


spec = parse_smt2_string(spec)

#set_option(verbose=10)
set_option('smt.mbqi', True)
set_option('smt.pull_nested_quantifiers', True)
set_option('smt.mbqi.trace', True)

s = Solver()
s.add(spec)
print s.check()

    在我的情况下，Z3迅速返回，答案不满意 . 与行为相关的主要方法是使用详细跟踪 . 详细描述将显示调用的策略 . 您可以使用SMT-LIB中的详细跟踪（从命令行传递选项-v：10或类似的数字） .

    回复于

相关问题