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