(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)