Z3中的获取任务

（获取分配）命令应该返回符号列表以及它们的真/假值，如果它们是Bool类型的。根据我的理解，这只能在以下情况下完成：produce-assignments设置为true，并且（check-sat）返回时。但是，当我运行一个小脚本在Z3上测试这个时，（get-assignment）只返回（） - 空白。这里是我的脚本：Z3中的获取任务

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

来源

2013-05-03 user2345614

对于它的价值，我可以证实这种行为Z3 [4.3.2版 - 64位 - 编译哈希码96f4606a7f2d]。有趣的是，将'（set-option：produce-models true）'放入前导中并在'（check-sat）'后放置'（get-value（ab））'产生'（（false）（b false）） '，所以该作业似乎可用（请参阅http://rise4fun.com/Z3/zGH7）。它看起来好像'（get-assignment）'不被支持，并且好像使用它不会引发错误。 – 2013-05-03 06:57:19

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

get-assignment 是一种重量轻，并获得价值的受限版本，要求针对选定的一组以前真值赋值进入公式（29）同样的几个。其他已经讨论过的命令（例如，get-proof），只有当产生分配选项（默认为false）被设置为真时（参见下面的第5.1.7节）时才能发出该命令。求解器不需要支持这个选项。像get-value一样，只有在检查sat命令后，才会发出该命令，或者可选地还会报告未知的命令，而不会插入断言集命令。命令返回所有对（fb）的序列，其中b为真或假并且f是所有断言的集合中的形式（t命名为f）的（子）项的标签，其中t排序布尔。与获取值类似，当最近一次check-sat命令的响应为sat，并且只有时，所有断言的集合都保证具有与返回的真值分配一致的模型（在逻辑中）。

下面是使用两个命名的子式（也可在网上here）相同的例子：

(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-08 14:22:27

Z3中的获取任务

回答

相关问题