Jestem nowym użytkownikiem Z3 i szukałem odpowiedzi na moje pytanie tutaj i w Google. Niestety nie udało mi się.

Używam API Z3 4.0 C / C ++. Zadeklarowałem niezdefiniowaną funkcjęd: (Int Int) Int, dodał kilka twierdzeń i obliczył model. Jak dotąd działa to dobrze.

Teraz chcę wyodrębnić pewne wartości funkcjid zdefiniowane przez model, powiedzmyd (0,0). Poniższa instrukcja działa, ale zwraca wyrażenie, a nie wartość funkcji, tj. Liczbę całkowitą, zd (0,0).

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

Rachunek

result.is_int();

zwracaprawdziwe.

Moje (miejmy nadzieję, że nie za głupie) pytanie brzmi: jak oddać zwrócone wyrażenie do int / C ++

Pomoc jest bardzo ceniona. Dziękuję Ci!