位向量上的量词消除会产生过于复杂的结果
位向量上的量词消除会产生过于复杂的结果
提问于 2012-04-11 20:55:51
我正在使用Z3的ELIM_QUANTIFIERS特性来消除位向量上公式中的量词。我遇到了以下情况，Z3生成了一个正确但过于复杂的结果，我想知道是否有一种方法可以重写我的问题，或者可能有一个配置选项可以导致我期望的简单结果。
首先，这里是一个按预期工作的示例。它指出，对于长度为4的位向量，存在与其相等的位向量。
(set-option ELIM_QUANTIFIERS true)
(declare-fun a () BitVec[4])
(simplify (exists ((x BitVec[4]))
(= a x)))Z3为此示例生成以下输出。
success
success
true但是，如果我添加一个否定：
(set-option ELIM_QUANTIFIERS true)
(declare-fun a () BitVec[4])
(simplify (exists ((x BitVec[4]))
(not (= a x))))然后，Z3会生成以下输出，其中列出了向量值的所有可能值，而不仅仅是返回"true“。
success
success
(let (($x54 (= (_ bv0 4) a)))
(let (($x55 (not $x54)))
(let (($x61 (= (_ bv2 4) a)))
(let (($x62 (not $x61)))
(let (($x68 (= (_ bv6 4) a)))
(let (($x69 (not $x68)))
(let (($x75 (= (_ bv4 4) a)))
(let (($x76 (not $x75)))
(let (($x82 (= (_ bv12 4) a)))
(let (($x83 (not $x82)))
(let (($x89 (= (_ bv8 4) a)))
(let (($x90 (not $x89)))
(let (($x95 (= (_ bv1 4) a)))
(let (($x96 (not $x95)))
(let (($x102 (= (_ bv5 4) a)))
(let (($x103 (not $x102)))
(let (($x109 (= (_ bv13 4) a)))
(let (($x110 (not $x109)))
(let (($x116 (= (_ bv9 4) a)))
(let (($x117 (not $x116)))
(let (($x123 (= (_ bv3 4) a)))
(let (($x124 (not $x123)))
(let (($x130 (= (_ bv7 4) a)))
(let (($x131 (not $x130)))
(let (($x137 (= (_ bv14 4) a)))
(let (($x138 (not $x137)))
(let (($x144 (= (_ bv10 4) a)))
(let (($x145 (not $x144)))
(let (($x151 (= (_ bv11 4) a)))
(let (($x152 (not $x151)))
(let (($x158 (= (_ bv15 4) a)))
(let (($x159 (not $x158)))
(or $x159 $x152 $x145 $x138 $x131 $x124 $x117 $x110 $x103 $x96 $x90 $x83 $x76 $x69 $x62 $x55)))))))))))))))))))))))))))))))))对于更长的位向量，例如大小为32或更大的位向量，Z3不会在合理的时间内产生结果，因为它可能枚举了32位变量的所有可能值。
请注意，在这种特殊情况下，我可以只使用check -sat值来检查公式的有效性；但是，在一般情况下，我感兴趣的是获得与原始公式等效的无限定符表达式，而不仅仅是检查其有效性。
我使用的是LinuxV3.2版的Z3。
回答 1
Stack Overflow用户
回答已采纳
发布于 2012-04-12 13:12:16
感谢，这是一个很好的简单示例，显示了用于位向量的方法的局限性。它确实只适用于解的数量相对较少的公式。在以这种方式消除期间，无法切换位向量开/关。这是在Z3中需要改进的一个有效点。有几个潜在的解决办法:首先，布尔量词消除，虽然它也是初级的(它只枚举可满足的实例并消除布尔变量)，它确实产生了更简单的结果“true”。当你从这个例子中位爆你的位向量时。第二种方法是考虑是否可以在UFBV片段中重新制定您的问题，其中可满足性不需要量词消除。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/10106329
复制相关文章
相似问题
腾讯云开发者
