2

(get-assignment) 命令应该返回一个符号列表以及它们的真/假值，如果它们是布尔类型的话。据我了解，这只能在 :produce-assignments 设置为 true 并且 (check-sat) 返回 sat 时完成。但是，当我在 Z3 上运行一个小脚本来测试它时， (get-assignment) 只返回 () - 空白。这是我的脚本：

(set-option :produce-assignments true)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= a b )) 
(check-sat)
(get-assignment)
4

1 回答 1

2

的语义get-assignment不直观。它显示子公式的值named。从SMT 2.0 参考（第 62 页）：

get-assignment 是 get-value 的轻量级和受限版本，它要求对一组选定的先前输入的公式进行真值分配。(29) 与已经讨论过的其他几个命令（例如，get-proof）类似，可以发出此命令仅当默认情况下为 false 的生产分配选项设置为 true 时（请参阅下面的第 5.1.7 节）。求解器不需要支持此选项。像 get-value 一样，它只能在报告 sat 的 check-sat 命令之后发出，或者也可以在报告未知的命令之后发出，而无需干预 assertion-set 命令。该命令返回所有对 (fb) 的序列，其中 b 为真或假，f 是所有断言集合中 (t 命名为 f) 形式的 (子) 项的标签，其中 t 为布尔型。与 get-value 类似，

这是使用两个命名子公式的相同示例（也可在此处在线获得）：

(set-option :produce-assignments true)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (! (= (! a :named a_val) b ) :named eq_val)) 
(check-sat)
(get-assignment)
于 2013-05-08T14:22:27.603 回答