Z3: Parse Term from String

Question

Is there a Z3 C API call that parses a general (non-Boolean) term? E.g. something like this: (+ a b)? As far as I see it, the Z3_parse_smtlib2_string function parses only formulas in assertions, which are exclusively of Boolean type.

Answer 1

The parser (Z3_parse_smtlib2_string) parses SMT-LIB2 benchmarks. Benchmarks in this format define a logical formula. This formula is "true" if the input does not contain any assertions. This is why the parser returns "true" in your case. Z3 doesn't expose parsing facilities for terms. You can work around this by creating a special predicate "MyHolds" that takes a term of the suitable type. You then create a benchmark that has the assertion "(assert (MyHolds ))" as the only assertion. You can then remove the MyHolds from the result of the parser to get back your term.