How to check if a constant in z3 is a variable or value?

Question

just wondering in z3py how to check if a given constant expression is a variable or a value? for instance

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

So, mycolor will be variables, and x_, True, False, White, Black will be values, not variables.

z3py has the predicate is_var, but for different purposes. This is useful if I want to rename all variables in a formula to another.

Answer 1

One way to do this for integers is is_int and is_int_value :

 x = Int('x') print "x types" print is_int(x) # true, is of sort int print is_int_value(x) # false, not a "value" x_ = IntVal(7) print "x_ types" print is_int(x_) # true, is also of sort int print is_int_value(x_) # true, is a value 

For is_real , you can do this using is_real to check the sorting of variables and use (disjunction) is_algebraic_value and is_rational_value for values ​​(I have not seen a function like is_real_value in the API, but I think this disjunction will do this). For bitvectors, you can use is_bv_value for values ​​and is_bv for checking the sorting of variables.

The .NET API has Expr.IsNumeral , and you can see how they are implemented in the API here (for example, Expr.IsIntNum [Python equivalent is_int_value ]) if both Expr.IsNumeral and Expr.IsInt are true): http: // research .microsoft.com / en-us / um / redmond / projects / z3 / _expr_8cs_source.html

I did not immediately see a way to do this for custom enumeration sorts. As one of the alternatives, you can encode your enum using bitvectors and compare variables / values ​​with is_bv_value . However, as a rule, you need to use more general algebraic data types and their automatically generated “recognizers”. The Python API does not seem to correctly create recognizers if you declare them as sort enums. Here's one way to do this in order to efficiently sort the enumeration (but declared as a more general data type).

Z3Py encoding the following: http://rise4fun.com/Z3Py/ELtn

 ColorVal = Datatype('ColorVal') ColorVal.declare('white') ColorVal.declare('black') ColorVal = ColorVal.create() mycolor = Const("mycolor", ColorVal) print ColorVal.recognizer(0) # is_white print ColorVal.recognizer(1) # is_black print simplify(ColorVal.is_white(mycolor)) # returns is_white(mycolor) print simplify(ColorVal.is_black(mycolor)) # returns is_black(mycolor) mycolorVal = ColorVal.white # set to value white print simplify(ColorVal.is_white(mycolorVal)) # true print simplify(ColorVal.is_black(mycolorVal)) # false # compare "variable" versus "value" with return of is_white, is_black, etc.: if it gives a boolean value, it a value, if not, it a variable print "var vs. value" x = simplify(ColorVal.is_white(mycolor)) print is_true(x) or is_false(x) # returns false, since x is is_white(mycolor) y = simplify(ColorVal.is_white(mycolorVal)) print is_true(y) or is_false(y) # true ColorValEnum, (whiteEnum,blackEnum) = EnumSort("ColorValEnum",["whiteEnum","blackEnum"]) mycolorEnum = Const("mycolorEnum",ColorValEnum) print ColorValEnum.recognizer(0) # is_whiteEnum print ColorValEnum.recognizer(1) # is_blackEnum # it appears that declaring an enum does not properly create the recognizers in the Python API: #print simplify(ColorValEnum.is_whiteEnum(mycolorEnum)) # error: gives DatatypeSortRef instance has no attribute 'is_whiteEnum' #print simplify(ColorValEnum.is_blackEnum(mycolorEnum)) # error: gives DatatypeSortRef instance has no attribute 'is_blackEnum' 

Answer 2

What you call variables is (technically) called uninterpreted constants in Z3. Values ​​(such as 1 , true , #x01 ) are called interpreted constants. Thus, in principle, a quick way to check if a is a “variable” can be done using the following code snippet:

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

This piece of code works for everything but data types. Having tried my example, I realized that Z3 incorrectly returns Z3_OP_UNINTERPRETED for data type constructors. I fixed this for Z3 4.2. In the meantime, you can use the following workaround in which the is_datatype_const_value(a) function returns true 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