Tuesday, 13 August 2013

obtain the integer from a model after s.get_model()

obtain the integer from a model after s.get_model()

In Z3's C++ API, I can search for a model by "model m = s.get_model();"
Then "cout << m.eval(a);" will give me the value for a.
However, m.eval(a) returns an expr object but I want to store its value as
an integer in my program. How can I convert an expr to an int?
Thanks.

No comments:

Post a Comment