smtlib 代码有问题

发布于 2025-01-08 09:26:55 字数 441 浏览 4 评论 0原文

我有以下代码

(set-logic QF_LIA)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (> x y))
(assert (> y z))
(push 1)
(assert (> z x))
(check-sat) ; unsat
(get-info :statistics)
(pop 1)
(push 1)
(check-sat (= x w)) ; sat

代码应该在第一个（check-sat）上返回unsat并在第二个（check-sat）上返回sat，但我不知道。

有人可以告诉我有什么问题吗？我正在使用 Windows 7，jSMTLIB 使用 cygwin

谢谢赛义夫

原文

I have this following code

(set-logic QF_LIA)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (> x y))
(assert (> y z))
(push 1)
(assert (> z x))
(check-sat) ; unsat
(get-info :statistics)
(pop 1)
(push 1)
(check-sat (= x w)) ; sat

The code should return unsat on first (check-sat) and sat on second (check-sat), but I get unknown.

Can someone please tell me what's the problem. I am using windows 7, jSMTLIB using cygwin

Thanks
Saif

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

星光不落少年眉 2025-01-15 09:26:55

我不知道你使用 jSMTLIB 中的哪个后端来解决这个问题。然而，(check-sat (= xw)) 在 SMT-LIB v2 中甚至不合法。

当我将该行更改为：时

(assert (= x w))
(check-sat)

，我从 Z3 Web 界面获取 unsat 和 sat，这符合我们的预期。

请注意，(get-info :statistics) 也是不正确的；正确的选项是(get-info :all-statistics)。您可以在他们的文档中阅读有关 SMT-LIB v2 标准的更多信息。

I don't know which backend in jSMTLIB you used for solving this. However, (check-sat (= x w)) is not even legal in SMT-LIB v2.

When I change that line to:

(assert (= x w))
(check-sat)

I get unsat and sat from Z3 web interface, which is of our expectation.

Note that (get-info :statistics) is also incorrect; the correct option is (get-info :all-statistics). You can read more about SMT-LIB v2 standard in their documentation.

回复收藏 0 原文

~没有更多了~