Z3 Python API中同名符号是否始终被视为等价？

一、同名且同类型的变量符号是否始终等价？ #

先看两个示例：

solve(Int('z') < Int('z'))

返回："no solution"

from z3 import *
x1=Int('x')
x2=Int('x')
x3=Int('x')
solve(x1*x2*x3==27)

返回："[x = 3]"

结论：是的，Z3始终将同名且同类型的变量符号视为完全等价。

把等式中所有z替换为Int('z')的操作，完全不会改变求解结果——因为每次调用Int('z')生成的都是同一个符号，Z3内部会对同名同类型的符号做统一标识，不会区分它们的创建时机或变量名（比如x1、x2、x3本质都是同一个Int('x')符号）。

二、同名且参数类型一致的函数符号是否始终等价？ #

示例代码：

from z3 import *
S1 = DeclareSort('S1')
S2 = DeclareSort('S2')
x1=Const("x",S1)
x2=Const("x",S2)
f1=Function('F', S1, S1,S2,IntSort())
f2=Function('F', S1, S1,S2,IntSort())
solve(f1(x1,x1,x2) < f2(x1,x1,x2))

返回："no solution"

结论：是的，Z3会将同名且参数类型（包括参数数量、每个参数的排序类型、返回值类型）完全一致的函数符号视为等价。

这个例子里f1和f2的函数签名完全相同，Z3会把它们当成同一个函数，所以f1(...) < f2(...)相当于同一个函数的输出小于自身，显然无解。

三、同名但参数类型/数量不同的函数符号是否绝不会等价？ #

示例代码：

from z3 import *
S1 = DeclareSort('S1')
S2 = DeclareSort('S2')
x1=Const("x",S1)
x2=Const("x",S2)
f1=Function('F', S1, S1,S2,IntSort())
f2=Function('F', S1, S2,S2,IntSort())
solve(f1(x1,x1,x2) < f2(x1,x2,x2))

返回：

[x = S2!val!0,
 x = S1!val!0,
 F = [else -> 1],
 F = [else -> 0]]

结论：是的，Z3绝不会将这类函数符号视为等价。

这里f1和f2的参数类型不同（第二个参数分别是S1和S2），属于不同的函数符号，Z3会把它们当作两个独立的函数处理。求解器可以给这两个"F"分配不同的默认值让不等式成立，也说明它们是完全独立的符号。

内容的提问来源于stack exchange，提问作者user2952903