BitwuzlaParser

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

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

Parameters:

parser – The Bitwuzla parser instance to delete.

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:

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:

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.