Я новичок в Z3 и искал ответ на свой вопрос здесь и в Google. К сожалению, мне не удалось.

Я использую Z3 4.0 C / C ++ API. Я объявил неопределенную функциюd: (Int Int) Int, добавил некоторые утверждения и вычислил модель. Пока это работает отлично.

Теперь я хочу извлечь определенные значения функцииd определяется моделью, скажемd(0,0), Следующее утверждение работает, но возвращает выражение, а не значение функции, то есть целое числоd(0,0).

z3::expr args[] = {c.int_val(0), c.int_val(0)};
z3::expr result = m.eval(d(2, args));

Чек

result.is_int();

возвращаетсяtrue.

Мой (надеюсь, не слишком глупый) вопрос, как привести приведенное выражение к int C / C ++?

Помощь очень ценится. Спасибо!