Z3 如何处理包含未解释函数的 forall 命题？

Posted 2023-03-28

【中文标题】Z3 如何处理包含未解释函数的 forall 命题？

【英文标题】：How does Z3 deal with forall proposition with uninterpreted functions in it?

【发布时间】：2013-01-06 11:19:59

【问题描述】：

假设我们有两个未解释的函数 func1 和 func2：

stuct_sort func1(struct_sort);
stuct_sort func2(struct_sort ,int).

他们有关系：

func2(p,n)=func1(p)  if n==1
func2(p,n)=func1(func2(p,n-1))  if n>1

我想知道的是，如果以下命题：

((forall i:[1,m].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,m-1].func2(q,i)==Z)

可以在Z3中证明是真的吗？ 在我的程序中，证明结果是Z3_L_UNDEF。

当我给 m 赋值比如 3 时，现在的命题是

((forall i:[1,3].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,3-1].func2(q,i)==Z);

结果是Z3_L_UNDEF。 但是当我如下单独重写案例（不使用forall）时，结果是true。

(func2(p,1)==Z)&&(func2(p,2)==Z)&&(func2(p,3)==Z)&&(q==func1(p)) implies (func2(q,1))&&(func2(q,2)).

找不到原因，期待你的回答

【参考方案1】：

我使用 Z3 Python 接口对您的问题进行了编码，Z3 解决了它。它为猜想找到了一个反例。 当然，我在编码问题时可能犯了一个错误。 Python 代码在文章末尾。我们可以在rise4fun 在线试用。顺便说一句，您使用的是哪个版本的 Z3？我假设您使用的是 C API。如果是这样，您能否提供用于创建 Z3 公式的 C 代码？另一种可能性是创建一个日志来记录您的应用程序和 Z3 的交互。要创建日志文件，我们必须在执行任何其他 Z3 API 之前执行 Z3_open_log("z3.log");。我们可以使用日志文件来回放您的应用程序与 Z3 之间的所有交互。

from z3 import *
# Declare stuct_sort 
S = DeclareSort('stuct_sort')
I = IntSort()
# Declare functions func1 and func2
func1 = Function('func1', S, S)
func2 = Function('func2', S, I, S)

# More declarations
p = Const('p', S)
n = Int('n')
m = Int('m')
i = Int('i')
q = Const('q', S)
Z = Const('Z', S)

# Encoding of the relations 
#    func2(p,n)=func1(p)  if n==1
#    func2(p,n)=func1(func2(p,n-1))  if n>1
Relations = And(func2(p, 1) == func1(p), 
                ForAll([n], Implies(n > 1, func2(p, n) == func1(func2(p, n - 1)))))

# Increase the maximum line width for the Z3 Python formula pretty printer
set_option(max_width=120)
print Relations

# Encoding of the conjecture
# ((forall i:[1,m].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,m-1].func2(q,i)==Z)
Conjecture = Implies(And(q == func1(p), ForAll([i], Implies(And(1 <= i, i <= m), func2(p, i) == Z))),
                     ForAll([i], Implies(And(1 <= i, i <= m - 1), func2(q, i) == Z)))
print Conjecture

prove(Implies(Relations, Conjecture))

【讨论】：

我使用 C api 再次测试了最新的 Z3，输入如下但仍未定义：(implies (and (= (func2 pp 1) (func1 pp)) (forall (ii Int) (implies (> ii 1) (= (func2 pp ii) (func1 (func2 pp (+ ii (* -1 1)))))))) (implies (and (= q (func1 p)) (forall (i Int) (implies (and (>= i 1) (<= i m)) (= (func2 p i) Z)))) (forall (i Int) (implies (and (>= i 1) (<= i (+ m (* -1 1)))) (= (func2 q i) Z)))))

代码可以在这里找到：https://gist.github.com/4491662

您的代码使用了已弃用的函数，例如 Z3_check_and_get_model。顺便说一句，C++ API 更容易使用。文件examples/c++/example.cpp 包含许多使用 C++ 和新求解器 API 的示例。这是此文件的链接：z3.codeplex.com/SourceControl/changeset/view/…

C++ API 非常好用，我已经用它解决了问题。非常感谢您的耐心和建议。