1

Using C++ APIs, how can you extract the decimal value of a bit-vector constant from a model.

Shambo
  • 898
  • 1
  • 10
  • 17

1 Answers1

1

There are several C-Functions that allow you to extract different types of values, depending on the expected size of the numerals: Z3_get_numeral_int, Z3_get_numeral_uint, Z3_get_numeral_uint64, Z3_get_numeral_int64. For numbers that don't fit into those basic types, we can use the Z3_get_numeral_string function to get a string representation that can be parsed into your preferred big-int representation.

Note that these functions are C-functions, not C++ functions, but those two APIs mix nicely. (See e.g, also z3 C++ API & ite).

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • 2
    Thanks for the suggestion. Writing something like `int val; Z3_get_numeral_int(bv.ctx(), bv, &val);` did the job. – Shambo Apr 23 '14 at 15:22