0

I'm using Z3_parse_smtlib2_string to parse a smtlib2 formula. The fomula looks like:

(set-logic QF_AUFBV)(declare-fun SymVar_0 () (_ BitVec 32))(declare-fun SymVar_1 () (_ BitVec 8))...

I parse it using:

Z3_ast ast = Z3_parse_smtlib2_string(ctx, (Z3_string)formula, 0, 0, 0, 0, 0, 0);

Let say that I want now to get the size of SymVar_0 (it should return 32). How can I do so?

Thank you

user1618465
  • 1,813
  • 2
  • 32
  • 58

1 Answers1

1

The function called Z3_get_bv_sort_size should do the job. Note that this is a C (not C++) function, so you have to supply the context as well.

In the interest of other users facing similar issues: There is no symbol table in Z3 that lets you look up the types of names. You can create one yourself by running over all the subexpressions and recording all the symbols and their types encountered while doing so. For an example in Python, see Z3py: how to get the list of variables from a formula?.

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • How can I specify that I want the size for the symbolic variable with name `SymVar_0` and not from other one? – user1618465 May 23 '16 at 06:00
  • The preferred way is to have that constant in an expression beforehand. As there is no symbol table, you can't look up the constants, but you can `cheat' by knowing the name and sort of the variable; that allows you to construct the same expression via mk_const, but it will only work if you get the name and sort exactly right. – Christoph Wintersteiger May 23 '16 at 11:12
  • Given some BV type, Z3_get_bv_sort_size(ctx, TYPE)); You need to know the name and the type of the variable, so you can just call the function on them. – Christoph Wintersteiger May 24 '16 at 14:44