как проверить, является ли const в z3 переменной или значением?

Один из способов сделать это для целых чисел — с помощью is_int и 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

На самом деле, вы можете сделать это, используя is_real для проверки сортировки переменных, и использовать (дизъюнкт) is_algebraic_value и is_rational_value для значений (я не видел такой функции, как is_real_value в API, но я думаю, что этот дизъюнкт сделает это ). Для битовых векторов вы можете использовать is_bv_value для значений и is_bv для проверки сортировки переменных.

В .NET API есть Expr.IsNumeral, и вы можете увидеть, как они реализованы в API здесь (например, Expr.IsIntNum [эквивалент Python is_int_value] проверяет, верны ли оба Expr.IsNumeral и Expr.IsInt): http://research.microsoft.com/en-us/um/redmond/projects/z3/_expr_8cs_source.html

Я не сразу увидел способ сделать это для определяемых пользователем сортировок перечислением. В качестве альтернативы вы можете закодировать перечисление с помощью битовых векторов и сравнить переменные/значения с помощью is_bv_value. Однако в качестве лучшего обходного пути вам, похоже, нужно использовать более общие алгебраические типы данных и их автоматически созданные «распознаватели». Python API, похоже, неправильно создает распознаватели, если вы объявляете их как сортировки перечисления. Вот один из способов сделать это для того, что фактически является перечислением (но объявлено как более общий тип данных).

Z3Py кодирует следующее: 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's a value, if not, it's 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'

То, что вы называете переменными, (технически) называется неинтерпретируемыми константами в Z3. Значения (такие как 1, true, #x01) называются интерпретируемыми константами. Так что, в принципе, быстрый способ проверить, является ли a "переменной", можно сделать с помощью следующего фрагмента кода:

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

Этот фрагмент кода работает для всего, кроме типов данных. Попробовав ваш пример, я понял, что Z3 неправильно возвращает Z3_OP_UNINTERPRETED для конструкторов типов данных. Я исправил это для Z3 4.2. Тем временем вы можете использовать следующий обходной путь, когда функция is_datatype_const_value(a) возвращает True is a и является константным конструктором.

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)

Затем следующий код перехватывает все неинтерпретированные константы:

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

Следующая ссылка содержит полный пример. http://rise4fun.com/Z3Py/vjb