有没有办法在 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)