首页
学习
活动
专区
圈层
工具
发布
首页
学习
活动
专区
圈层
工具
MCP广场
社区首页 >问答首页 >断言0除以0为1时,z3返回unknown

断言0除以0为1时,z3返回unknown
EN

Stack Overflow用户
提问于 2019-05-29 02:19:41
回答 1查看 50关注 0票数 0

我在尝试Z3: a tutorial这篇文章中的例子。有一个例子说明所有的函数都是合计的,包括"div":

代码语言:javascript
运行
复制
(push)
(assert (= 1 (div 0 0))) 
(check-sat)
;sat (pop)

我注意到z3版本4.8.5根据用户是否使用"push“返回不同的结果。

使用以下代码,z3将返回未知:

代码语言:javascript
运行
复制
(get-info :version)
;(push)
(assert (= 1 (div 0 0)))
(check-sat)

z3的输出为:

代码语言:javascript
运行
复制
(:version "4.8.5 - build hashcode 8c085f1a1850")
unknown

相比之下,使用以下代码,z3将返回sat:

代码语言:javascript
运行
复制
(get-info :version)
(push)
(assert (= 1 (div 0 0)))
(check-sat)
(get-model)

z3的输出为:

代码语言:javascript
运行
复制
(:version "4.8.5 - build hashcode 8c085f1a1850")
sat
(model 
)

rise4fun教程中,它说“命令push通过保存当前堆栈大小创建一个新的作用域”,似乎"push“的使用在这里不应该导致不同的结果,因为只有一个断言?

EN

Stack Overflow用户

发布于 2019-05-29 13:43:07

严格地说,unknownsat并不矛盾:求解器可以随时退出并说unknown。例如,如果您显式地使用策略,就会发生这种行为。

但是你是绝对正确的,奇怪的push导致了这种差异。请在z3 github issues站点:https://github.com/Z3Prover/z3/issues提交罚单,并让我们知道您发现了什么!

票数 0
EN
查看全部 1 条回答
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/56348003

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档