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 回答