how to check if a const in z3 is a variable or a value?

Question

just wondering in z3py , how do I check if a given constant expression is a variable or value ? For example

x = Int('x')
x_ = IntVal(7)
ColorVal, (White,Black)  = EnumSort("ColorVal",["While","Black"])
mycolor = Const("mycolor",ColorVal)

So x,mycolor would all be variables and x_,True,False,White,Black would be values and not variables .

z3py has is_var predicate but for different purpose. This is useful if I want to rename all variables in a formula to something else.

Answer 1

What you call variables are (technically) called uninterpreted constants in Z3. Values (such as 1, true, #x01) are called interpreted constants. So, in principle, a fast way to check whether a is a "variable" can be done using the following piece of code:

is_const(a) and a.decl().kind() == Z3_OP_UNINTERPRETED

This piece of code works for everything, but datatypes. After trying your example, I realized that Z3 is incorrectly returning Z3_OP_UNINTERPRETED for datatype constructors. I fixed that for Z3 4.2. In the meantime, you can use the following workaround where the function is_datatype_const_value(a) returns True is a is a constant constructor.

def is_datatype_sort(s):
  return s.kind() == Z3_DATATYPE_SORT

def is_datatype_constructor(x):
  s = x.sort()
  if is_datatype_sort(s):
    n = s.num_constructors()
    f = x.decl()
    for i in range(n):
      c = s.constructor(i)
      if eq(c, f):
        return True
  return False 

# Return True if x is a constant constructor, that is, a constructor without arguments.
def is_datatype_const_value(x):
  return is_const(x) and is_datatype_constructor(x)

Then, the following code catches all uninterpreted constants:

 is_const(a) and a.decl().kind() == Z3_OP_UNINTERPRETED and not is_datatype_const_value(a)

The following link contains a complete example. http://rise4fun.com/Z3Py/vjb