Use proper APIs to get or set bitvector type width

[tautschnig]

ID_width is an implementation detail, and even more so is whether the value is
stored as a string literal noting the decimal number or some other encoding of
the number.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: f7eba4a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96415387

[smowton]

Looks good, though it's a shame to see various string->int->string conversions introduced for tidiness' sake. Is there a plan already to use a tagged variant instead of a string for such things?

[tautschnig]

@smowton Very late response/request for clarification:

Is there a plan already to use a tagged variant instead of a string for such things?

What do you mean by "tagged variant?" Thanks!

[smowton]

@tautschnig something like

enum variant_kinds { V_STRING, V_INTEGER, V_FLOAT }; 
struct variant { union { char *s; int i; float f; } u; variant_kinds kind; }
int variant_to_int(const variant &v) {
  if(v.kind == V_INTEGER) return v.u.i;
  else if(v.kind == V_STRING) return atoi(v.u.s);
  else if(v.kind == V_FLOAT) return ...
}

(it might also update the variant with the format it just computed -- depends if you think get-with-set-kind of repeated-get-of-same-kind is more common)

[smowton]

That would also be useful for integers in ireps, since it would avoid all the tedious back and forth between string and integer representations

[tautschnig]

I understand your concern about converting back and forth, but I do not yet understand how the above proposal addresses the problem (within the current code base). Are you suggesting to replace the irept::dt::data field (currently an irep_idt) by the above struct variant?

[smowton]

In the end yes, so that integers can be stored in native form instead of an index into a string table containing their string representation, but cmdlinet and cousins seem like an obvious place to prototype it. They already have get_integer_option etc, which are ideal places to avoid conversion. Similarly you'd have some_irep.id().as_integer(), which would avoid conversion if possible.