如何解决如何获得每个 Z3 查询的确认? 问题示例:实际问题
我正在使用远程 Z3 控制台,方法是通过标准输入发送查询并读取 stdout/err 以获取错误和响应。问题是我没有找到一种方法来合理地检查查询是否已成功执行而不会陷入数据竞争。
问题示例:
假设我发送了一个查询
(assert (= 1 1))
不返回任何输出。我应该如何检查那里是否有任何错误?如果我检查是否没有响应,我就无法区分成功的查询和仍在计算的操作。
实际问题
我想用 ok
或类似的东西让 Z3 回复每个通常不会成功的查询。这是可以实现的吗?如果没有,我该怎么做才能知道最近查询的状态?
解决方法
我认为 (set-option :print-success true)
应该这样做。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。