有没有办法在 SMTLIB 中表达“当且仅当”？

【问题标题】：is there a way to express "if and only if" in SMTLIB?有没有办法在 SMTLIB 中表达“当且仅当”？
【发布时间】：2021-06-29 22:03:43
【问题描述】：

和SMTLIB中的define一样吗？或者是我自己定义函数的唯一方法？如果 z3 有办法通过它的 python 绑定来做到这一点，那也对我有用。

【问题讨论】：

标签： z3 smt

【解决方案1】：

在 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)

【讨论】：