Parser

class bitwuzla::parser::Parser
Example

namespace bitwuzla::parser {

class Parser

The Bitwuzla parser.

Public Functions

Parser(TermManager &tm, Options &options, const std::string &language = "smt2", std::ostream *out = &std::cout)

Constructor.

Note

The parser creates and owns the associated Bitwuzla instance.

Note

It is not safe to reuse a parser instance after a parse error. Subsequent parse queries after a parse error will return with an error.

Parameters:

tm – The associated term manager instance.
options – The configuration options for the Bitwuzla instance (created by the parser).
language – The format of the input.
out – The output stream.

~Parser(): Destructor.

void configure_auto_print_model(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:: value – True to enable auto printing of the model.

void parse(const std::string &input, bool parse_only = false, bool parse_file = true)

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:

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 issuing calls to check_sat.
parse_file – True to parse an input file with the given name input, false to parse from input as a string input.

Throws:

Exception – on error.

void parse(const std::string &infile_name, std::istream &input, bool parse_only = false)

Parse input from an input stream.

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:

infile_name – The name of the input file. This is required for error message printing only. Use ‘<stdin>’ if the input stream is std::cin, and ‘<string>’ if the input stream was created from a string.
input – The input stream.
parse_only – True to only parse without issuing calls to check_sat.

Throws:

Exception – on parse error.

Term parse_term(const std::string &input)

Parse term from string.

Parameters:: input – The input string.
Throws:: Exception – on parse error.
Returns:: The parsed term.

Sort parse_sort(const std::string &input)

Parse sort from string.

Parameters:: input – The input string.
Throws:: Exception – on parse error.
Returns:: The parsed sort.

std::vector<Sort> get_declared_sorts() const

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.

Returns:: The declared sorts.

std::vector<Term> get_declared_funs() const

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.

Returns:: The declared function symbols.

std::shared_ptr<bitwuzla::Bitwuzla> bitwuzla()

Get the associated Bitwuzla instance.

Returns:: The Bitwuzla instance.

}

Example

The source code for this example can be found at examples/c/parse.cpp.

/***
 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 *
 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 *
 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 */

#include <bitwuzla/cpp/bitwuzla.h>
#include <bitwuzla/cpp/parser.h>

#include <cassert>
#include <iostream>

using namespace bitwuzla;

int
main()
{
  // First, create a term manager instance.
  TermManager tm;
  // Create a Bitwuzla options instance.
  Options options;

  // We will parse example file `smt2/quickstart.smt2`.
  // Create parser instance.
  parser::Parser parser(tm, options);

  try
  {
    // Now parse the input file.
    std::cout << "Expect: sat" << std::endl;
    std::cout << "Bitwuzla: ";
    parser.parse("../smt2/quickstart.smt2");

    // Now we retrieve the set of asserted formulas and print them.
    auto assertions = parser.bitwuzla()->get_assertions();
    std::cout << "Assertions:" << std::endl << "{" << std::endl;
    for (const auto& a : assertions)
    {
      std::cout << "  " << a << std::endl;
    }
    std::cout << "}" << std::endl;

    // Now we add an assertion via parsing from string.
    parser.parse("(assert (distinct (select a x) y))", true, false);
    // Now the formula is unsat.
    Result result = parser.bitwuzla()->check_sat();

    std::cout << "Expect: unsat" << std::endl;
    std::cout << "Bitwuzla: " << result << std::endl;

    // For illustration purposes, we now parse in some declarations and terms
    // and sorts from string.

    // Declare bit-vector sort of size 16.
    Sort bv16 = parser.parse_sort("(_ BitVec 16)");
    // Create bit-vector sort of size 16 and show that it corresponds to
    // its string representation '(_ BitVec16)'.
    assert(bv16 == tm.mk_bv_sort(16));

    // Declare Boolean constants 'c' and 'd'.
    // Note: Declarations are commands (not terms) in the SMT-LIB language.
    //       Commands must be parsed in via Parser::parse(),
    //       Parser::parse_term() only supports parsing SMT-LIB terms.
    parser.parse("(declare-const c Bool)(declare-const d Bool)", true, false);
    // Declare bit-vector constant 'b'.
    parser.parse("(declare-const b (_ BitVec 16))", true, false);
    // Retrieve term representing 'b'.
    Term b = parser.parse_term("b");
    // Retrieve term representing 'c'.
    Term c = parser.parse_term("c");
    // Retrieve term representing 'd'.
    Term d = parser.parse_term("d");
    // Create xor over 'c' and 'd' and show that it corresponds to term
    // parsed in from its string representation '(xor c d)'.
    assert(parser.parse_term("(xor c d)") == tm.mk_term(Kind::XOR, {c, d}));
    // Create bit-vector addition over 'b' and bit-vector value
    // '1011111010001010' and show that it corresponds to the term parsed in
    // from its string representation '(bvadd b #b1011111010001010)'.
    assert(parser.parse_term("(bvadd b #b1011111010001010)")
           == tm.mk_term(Kind::BV_ADD,
                         {b, tm.mk_bv_value(bv16, "1011111010001010", 2)}));
  }
  catch (bitwuzla::parser::Exception& e)
  {
    // We expect no error to occur.
    std::cout << "unexpected parser exception" << std::endl;
  }
  return 0;
}