如何解决有没有办法在 SMTLIB 中表达“当且仅当”?
和 SMTLIB 中的 define
一样吗?或者是我自己定义函数的唯一方法?如果 z3 有办法通过它的 python 绑定来做到这一点,这也适用于我。
解决方法
在 SMTLib 中,iff
只是布尔值上的 =
:
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= a b))
在 z3py 中,您可以使用常规的相等比较:
from z3 import *
a,b = Bools('a b')
s = Solver()
s.add(a == b)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。