are z3 variables with same name in z3 python API always treated as equals?

user2952903 0
Viewed 18

In following examples z3 assumes that 2 symbols with same name are equal.

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

returns: "no solution"

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

returns:"[x = 3]"

Can I assume that z3 always treats symbols with same name and type as equals? For example if I have an equation with variable Int type variable z - can replace "z" with "Int('z')" everywhere in the equation and be sure that output will be the same?

Can I assume that z3 always treats function-symbols with same name and same type of arguments as equals like in following example:

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

returns:"no solution"

Can I assume that z3 never treats function-symbols with same name, but different type or number of arguments as equals like in following example:

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

returns:"

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

"

z3py
1 Answers

In Z3 variables are identified by name and sort. So, if two variables have the same name and sort then they are the same. Correspondingly, if they either have different names OR sorts, then they are different. The sort is the type and for function names the type is a function type. (i.e. there’s no special treatment for function names. You can think of ordinary variables as functions that take 0 arguments.)

In particular, two different variables can have the same name so long as they have different sorts. This can be rather confusing, however, since when z3 prints the corresponding SMTLib or models, you won’t have an obvious indication showing which one is which. So I’d advise against using the same name even if the sorts differ.

useroBV30
Related