Опитвам се да реша ограничения, използвайки Z3 SMT решаващ инструмент в python. Ограниченията включват както цели числа, така и битови вектори. Преобразувам BitVec в Int с помощта на Z3_mk_bv2int. Вярвам, че следните ограничения са незадоволими, но получавам SAT от Z3 Solver. Не съм сигурен дали го конвертирам правилно или не. Ако обаче заменя променливите на BitVecs с ограничени целочислени променливи, тогава преобразуването не е необходимо и получавам очакваните резултати.
Пример:
def get_int(var):
ctx = var.ctx
return ArithRef(Z3_mk_bv2int(ctx.ref(), var.as_ast(), 0), ctx)
def main():
var1 = BitVec('var1', 6)
var2 = Int('var2')
solve(var2 == get_int(var1)- var2, var2 > 32)
if __name__ == "__main__": main()
Резултати: [var1 = 0, var2 = 33]
Аз съм нов в SMT решавачите. Моля, помогнете ми да разбера грешката или алтернативно решение.
