получить целое число из модели после s.get_model ()
В API C ++ Z3, Я могу искать модель по
model m = s.get_model();
Затем:
cout << m.eval(A);
даст мне значение для A,
Тем не мение, m.eval(A) возвращает объект expr, но я хочу сохранить AЗначение как целое число в моей программе. Как я могу конвертировать expr в int?
Решение
Другие решения
C API предоставляет методы для получения целочисленных значений из выражений, которые являются целыми числами.
Наиболее общий API это:
/**
\brief Return numeral value, as a string of a numeric constant term
\pre Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST
def_API('Z3_get_numeral_string', STRING, (_in(CONTEXT), _in(AST)))
*/
Z3_string Z3_API Z3_get_numeral_string(__in Z3_context c, __in Z3_ast a);
Возвращает string (char*). Это позволяет возвращать бигнумы (цифры, которые не помещаются в 64 битах).
Z3 выставляет множество других Z3_get_numeral варианты для особых случаев. Они описаны в z3_api.h или смотрите: http://research.microsoft.com/en-us/um/redmond/projects/z3/code/group__capi.html
Возможный пример с использованием Z3py
x= Int('x')
s = Solver()
s.add(x + 3 == 5)
print s.check()
m = s.model()
print m
y = (m.evaluate(x))
z = y + 4
print simplify(z)
Выход:
sat
[x = 2]
6