Casting uma expressão inteira Z3 para um C / C ++ int
Sou novo no Z3 e procurei a resposta para minha pergunta aqui e no Google. Infelizmente, não fui bem sucedido.
Estou usando a API Z3 4.0 C / C ++. Eu declarei uma função indefinidad: (Int Int) Int, adicionou algumas afirmações e calculou um modelo. Até agora, isso funciona bem.
Agora, quero extrair certos valores da funçãod definido pelo modelo, digamosd (0,0). A instrução a seguir funciona, mas retorna uma expressão em vez do valor da função, ou seja, um inteiro, ded (0,0).
z3::expr args[] = {c.int_val(0), c.int_val(0)};
z3::expr result = m.eval(d(2, args));
A conta
result.is_int();
devolveverdade.
Minha (espero não muito estúpido) pergunta é como converter a expressão retornada para um C / C ++ int?
Ajuda é muito apreciada. Obrigado!