z3 - 是否存在不可解释函数的理论(同余分析)？

Question

我有一组符号变量:

int a, b, c, d, e;

一组未知函数，受许多公理约束:

f1(a, b) = f2(c, b)
f1(d, e) = f1(e, d)
f3(b, c, e) = f1(b, e)
c = f1(a, b)
b = d

这里的函数f1、f2、f3未知，但已修复。所以它不是一个未解释函数的理论。

我想证明以下断言的有效性:

c = f2(f1(a, b), b)
f3(d, f2(c, b), e) = f1(e, b)

使用基于上述公理等式的替换。

是否有一种理论，对于此类定理，仅使用提供的等式来尝试组合答案，而不是对函数提出解释？

如果是，该理论的名称是什么？哪种 SMT 求解器支持该理论？

它可以与其他理论(例如线性算术)混合吗？

Answer 1

这仍然是未解释的函数，因为如果存在满足您的公理的函数，那么这将属于未解释的函数理论。类似地，如果这样的函数不存在，那么 this 在未解释的函数中是不饱和的。因此，当且仅当未解释函数中的问题可满足时，您所描绘的才是可满足的，因此这两个理论是同构的，即相同的。

鉴于您试图根据公理证明某些定理是有效的，求解器如何表示可满足的结果并不重要，因为 sat 结果对应于无效模型。要使用 SMT 求解器证明您的定理，您应该断言您的公理，断言定理的否定，然后寻找不可满足的结果。请参阅this question了解可满足性和有效性之间联系的更详细解释。

要使用 Z3 证明您的第一个定理，SMT-LIB 2 中的以下内容就足够了:

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(declare-fun f1 (Int Int) Int)
(declare-fun f2 (Int Int) Int)

(assert (= (f1 a b) (f2 c b)))
(assert (= c (f1 a b)))
(assert (not (= c (f2 (f1 a b) b))))

(check-sat)