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 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::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;
}