如何解决Z3 : 为什么 MBQI 实例化了这个量词而 e-matching 没有?
在以下代码中,z3
似乎没有实例化量词 nil-cons
:
(set-option :auto-config false)
(set-option :smt.mbqi false)
(set-option :smt.ematching true)
(set-option :smt.qi.profile true)
(declare-sort Lis 0)
(declare-sort Elem 0)
(declare-const nil Lis)
(declare-fun cons (Elem Lis) Lis)
(assert
(forall
((x Elem) (xs Lis))
(! (not
(=
nil
(cons x xs)
)
)
:pattern ((cons x xs))
:qid nil-cons
)
)
)
(declare-const global_x Elem)
(declare-const global_xs Lis)
(assert
(=
nil
(cons global_x global_xs)
)
)
(check-sat)
但是,启用 mbqi 后,量词似乎已被实例化。
结果是ematching,z3
返回unknown
,使用mbqi返回unsat
(对应nil-cons
公理与最终未量化断言的矛盾) .
有谁知道为什么 nil-cons
公理没有通过 ematching 实例化?在我看来,模式应该匹配。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。