1

Z3新手的另一个问题。选项可以改变 Z3 的行为吗？我可能期望它们会影响终止，或者改变sat或unsat改变，unknown但不会sat改变，unsat反之亦然。

这个例子：

(set-option :smt.macro-finder true)

(declare-datatypes () ((Option (none) (some (Data Int)))))

(define-sort Set () (Array Option Option))
(declare-fun filter1 (Option) Option)
(declare-fun filter2 (Option) Option)

(declare-var s1 Set)
(declare-var s2 Set)
(declare-var x1 Option)
(declare-var x2 Option)
(declare-var x3 Option)
(declare-var x4 Option)

(assert (not (= x1 none)))
(assert (not (= x2 none)))
(assert (not (= x3 none)))
(assert (not (= x4 none)))
(assert (= (select s1 x1) x2))
(assert (= (select s2 x3) x4))

(assert (forall ((x Option)) (= (filter1 x) (ite (or (= none x) (= (Data x) 1)) x none))))
(assert (forall ((x Option)) (= (filter2 x) (ite (or (= none x) (= (Data x) 2)) x none))))

(assert (= ((_ map filter1) s1) s2))
(assert (= ((_ map filter2) s1) s2))
(check-sat)
(get-model)

返回sat第一行，unsat没有它。

这是一个错误还是我错过了一些基本的东西？

谢谢， N

4

1 回答 1

0

这是一个错误。这两个量词本质上是为filter1和提供“定义” filter2。
该选项smt.macro-finder用于通过扩展这些定义来消除函数符号。它本质上是在执行“宏观扩张”。但是，宏扩展器中有一个错误。它不会扩展地图结构中filter1和的出现：和。filter2(_ map filter1)(_ map filter2)

这个错误将被修复。同时，我们不应该同时使用map构造和smt.macro-finder选项。

于 2013-10-24T15:29:34.560 回答