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_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.

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.