BitwuzlaParser

• typedef struct BitwuzlaParser

• bitwuzla_parser_new()

• bitwuzla_parser_delete()

• bitwuzla_parser_parse()

• bitwuzla_parser_get_bitwuzla()

typedef struct BitwuzlaParser BitwuzlaParser

A Bitwuzla parser.

BitwuzlaParser *bitwuzla_parser_new(BitwuzlaTermManager *tm, BitwuzlaOptions *options, const char *language, uint8_t base, const char *outfile_name)

Create a new Bitwuzla parser instance.

The returned instance must be deleted via bitwuzla_parser_delete().

See also

• bitwuzla_parser_delete

Note

The parser creates and owns the associated Bitwuzla instance.

Parameters:

• tm – The associated term manager instance.

• options – The associated options.

• language – The format of the input.

• base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal. Always ignored for Boolean and RoundingMode values.

• outfile_name – The output file name. If name is ‘<stdout>’, the parser writes to stdout.

Returns:

A pointer to the created Bitwuzla parser instance.

void bitwuzla_parser_delete(BitwuzlaParser *parser)

Delete a Bitwuzla parser instance.

The given instance must have been created via bitwuzla_parser_new().

See also

• bitwuzla_parser_new

Parameters:

parser – The Bitwuzla parser instance to delete.

void bitwuzla_parser_set_termination_callback(BitwuzlaParser *parser, int32_t (*fun)(void*), void *state)

Configure a termination callback function.

The state of the callback can be retrieved via bitwuzla_parser_get_termination_callback_state().

See also

• bitwuzla_terminate

• bitwuzla_get_termination_callback_state

Parameters:

• parser – The Bitwuzla parser instance.

• fun – The callback function, returns a value != 0 if bitwuzla should be terminated.

• state – The argument to the callback function.

void *bitwuzla_parser_get_termination_callback_state(BitwuzlaParser *parser)

Get the state of the termination callback function.

The returned object representing the state of the callback corresponds to the state configured as argument to the callback function via bitwuzla_set_termination_callback().

See also

• bitwuzla_terminate

• bitwuzla_set_termination_callback

Parameters:

parser – The Bitwuzla parser instance.

Returns:

The object passed as argument state to the callback function.

void bitwuzla_parser_configure_auto_print_model(BitwuzlaParser *parser, bool value)

Enable or disable the automatic printing of the model after each satisfiable query.

Enable to automatically print the model after every sat query. Must be enabled to automatically print models for BTOR2 input (does not provide a command to print the model like (get-model) in SMT-LIB2). False (default) configures the standard behavior for SMT-LIB2 input (print model only after a (get-model) command).

Note

By default, auto printing of the model is disabled.

Parameters:

• parser – The Bitwuzla parser instance.

• value – True to enable auto printing of the model.

void bitwuzla_parser_parse(BitwuzlaParser *parser, const char *input, bool parse_only, bool parse_file, const char **error_msg)

Parse input, either from a file or from a string.

Note

Parameter parse_only is redundant for BTOR2 input, its the only available mode for BTOR2 (due to the language not supporting “commands” as in SMT2).

Parameters:

• parser – The Bitwuzla parser instance.

• input – The name of the input file if parse_file is true, else a string with the input.

• parse_only – True to only parse without executing check-sat calls.

• parse_file – True to parse an input file with the given name input, false to parse from input as a string input.

• error_msg – Output parameter for the error message in case of a parse error, NULL if no error occurred.

BitwuzlaTerm bitwuzla_parser_parse_term(BitwuzlaParser *parser, const char *input, const char **error_msg)

Parse term from string.

Parameters:

• parser – The Bitwuzla parser instance.

• input – The input string.

• error_msg – Output parameter for the error message in case of a parse error, NULL if no error occurred.

Returns:

The resulting term.

BitwuzlaSort bitwuzla_parser_parse_sort(BitwuzlaParser *parser, const char *input, const char **error_msg)

Parse sort from string.

Parameters:

• parser – The Bitwuzla parser instance.

• input – The input string.

• error_msg – Output parameter for the error message in case of a parse error, NULL if no error occurred.

Returns:

The resulting sort.

BitwuzlaSort *bitwuzla_parser_get_declared_sorts(BitwuzlaParser *parser, size_t *size)

Get the current set of (user-)declared sort symbols.

Note

Corresponds to the sorts declared via SMT-LIB command declare-sort. Will always return an empty set for BTOR2 input.

Parameters:

• parser – The Bitwuzla parser instance.

• size – The size of the returned sort array.

Returns:

The declared sorts, NULL if empty.

BitwuzlaTerm *bitwuzla_parser_get_declared_funs(BitwuzlaParser *parser, size_t *size)

Get the current set of (user-)declared function symbols.

Note

Corresponds to the function symbols declared via SMT-LIB commands declare-const and declare-fun.

Parameters:

• parser – The Bitwuzla parser instance.

• size – The size of the returned sort array.

Returns:

The declared function symbols, NULL if empty.

const char *bitwuzla_parser_get_error_msg(BitwuzlaParser *parser)

Get the current error message.

Parameters:

parser – The Bitwuzla parser instance.

Returns:

The error message.

Bitwuzla *bitwuzla_parser_get_bitwuzla(BitwuzlaParser *parser)

Get the associated Bitwuzla instance.

Returns:

The Bitwuzla instance.

void bitwuzla_parser_get_statistics(BitwuzlaParser *parser, const char ***keys, const char ***values, size_t *size)

Get current parser statistics.

The statistics are retrieved as a mapping from statistic name (keys) to statistic value (values).

Note

Output parameters keys and values are only valid until the next call to bitwuzla_parser_get_statistics().

Parameters:

• parser – The Bitwuzla parser instance.

• keys – The resulting set of statistic names.

• values – The resulting set of statistic values.

• size – The resulting size of keys and values.