Z3如何处理所有包含未解释函数的命题

Question

假设我们有两个未解释函数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)).

我找不到原因，期待您的回答

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