文章/答案/技术大牛

发布

社区首页 >问答首页 >调整Z3量词实例化的指南(带有SMT接口)

问调整Z3量词实例化的指南(带有SMT接口)
EN

Stack Overflow用户

提问于 2020-06-10 13:12:41

回答 1查看 167关注 0票数 0

我试图在机器生成的问题上调优z3

proof

irrelevant
是不可满足的，
包含与quantifiers
where断言无关的断言，由于这些不相关的断言(手动删除这些断言)， z3无法找到不可满足的证据。

是否有处理这种情况的一般准则？

通过命令行选项，我想我可以尝试：

mbqi.id ( string )只对id以string开头的量词使用基于模型的实例化(默认值：)

然而，我不知道如何使用SMT-LIB语法将id附加到量词。有线索的人能和我分享吗？

smt

回答 1

Stack Overflow用户

发布于 2020-06-10 15:33:59

这里提到的id只是量化变量的名称。如果你有：

(declare-sort S 0)
(declare-fun gt (S S) bool)

(assert (forall ((inst_a S) (inst_b S))
          (or (gt inst_a inst_b) (gt inst_b inst_a))))

(check-sat)

然后你可以说：

z3 smt.mbqi=true smt.mbqi.id=inst a.smt2

不要忘记使用smt.mbqi=true来打开MBQI。如果使用此调用，则只有在上述示例中的量化变量以inst开头时，z3才会实例化一个模式。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/62304482

复制

相似问题

问调整Z3量词实例化的指南(带有SMT接口)
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问调整Z3量词实例化的指南(带有SMT接口)EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问调整Z3量词实例化的指南(带有SMT接口)
EN