C++ API Documentation

The C++ API of Bitwuzla is its primary API. This section provides a quickstart guide to give an introduction on how to use the C++ API and a comprehensive set of examples to cover basic and common use cases. A comprehensive description of the interface is given here.

Quickstart

First, create a TermManager instance that allows us to create sorts and terms later:

  TermManager tm;

Then, create a bitwuzla::Options instance:

  Options options;

This instance can be configured via bitwuzla::Options::set(). For example, to enable model generation (SMT-LIB: (set-option :produce-models true)):

  options.set(Option::PRODUCE_MODELS, true);

Some options have modes, which can be configured via the string representation of their modes. For example, to enable CaDiCaL as back end SAT solver (this is for illustration purposes only, CaDiCaL is configured by default):

  options.set(Option::SAT_SOLVER, "cadical");

For more details on available options, see Options.

Then, create a Bitwuzla solver instance with a term manager and configured options (configuration options are now frozen and cannot be changed for this instance):

  Bitwuzla bitwuzla(tm, options);

Next, you will want to create some expressions via the term manager tm and assert formulas.

Note

Sorts and terms can be shared between multiple solver instances as long as these solvers use the same term manager.

For example, consider the following SMT-LIB input:

(set-logic QF_ABV)
(set-option :produce-models true)
(declare-const x (_ BitVec 8))
(declare-const y (_ BitVec 8))
(declare-fun f ((_ BitVec 8) (_ BitVec 4)) (_ BitVec 8))
(declare-const a (Array (_ BitVec 8) (_ BitVec 8)))
(assert
    (distinct
        ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
        ((_ extract 3 0) (bvashr y (_ bv1 8)))))
(assert (= (f x ((_ extract 6 3) x)) y))
(assert (= (select a x) y))
(check-sat)
(get-model)
(get-value (x y f a (bvmul x x)))
(exit)

This input is created and asserted as follows:

  // Create bit-vector sorts of size 4 and 8.
  Sort sortbv4 = tm.mk_bv_sort(4);
  Sort sortbv8 = tm.mk_bv_sort(8);
  // Create function sort.
  Sort sortfun = tm.mk_fun_sort({sortbv8, sortbv4}, sortbv8);
  // Create array sort.
  Sort sortarr = tm.mk_array_sort(sortbv8, sortbv8);

  // Create two bit-vector constants of that sort.
  Term x = tm.mk_const(sortbv8, "x");
  Term y = tm.mk_const(sortbv8, "y");
  // Create fun const.
  Term f = tm.mk_const(sortfun, "f");
  // Create array const.
  Term a = tm.mk_const(sortarr, "a");
  // Create bit-vector values one and two of the same sort.
  Term one = tm.mk_bv_one(sortbv8);
  // Alternatively, you can create bit-vector value one with:
  // Term one = tm.mk_bv_value(sortbv8, "1", 2);
  // Term one = tm.mk_bv_value_uint64(sortbv8, 1);
  Term two = tm.mk_bv_value_uint64(sortbv8, 2);

  // (bvsdiv x (_ bv2 8))
  Term sdiv = tm.mk_term(Kind::BV_SDIV, {x, two});
  // (bvashr y (_ bv1 8))
  Term ashr = tm.mk_term(Kind::BV_ASHR, {y, one});
  // ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
  Term sdive = tm.mk_term(Kind::BV_EXTRACT, {sdiv}, {3, 0});
  // ((_ extract 3 0) (bvashr x (_ bv1 8)))
  Term ashre = tm.mk_term(Kind::BV_EXTRACT, {ashr}, {3, 0});

  // (assert
  //     (distinct
  //         ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
  //         ((_ extract 3 0) (bvashr y (_ bv1 8)))))
  bitwuzla.assert_formula(tm.mk_term(Kind::DISTINCT, {sdive, ashre}));
  // (assert (= (f x ((_ extract 6 3) x)) y))
  bitwuzla.assert_formula(
      tm.mk_term(Kind::EQUAL,
                 {tm.mk_term(Kind::APPLY,
                             {f, x, tm.mk_term(Kind::BV_EXTRACT, {x}, {6, 3})}),
                  y}));
  // (assert (= (select a x) y))
  bitwuzla.assert_formula(
      tm.mk_term(Kind::EQUAL, {tm.mk_term(Kind::ARRAY_SELECT, {a, x}), y}));

Alternatively, you can parse an input file in BTOR2 format [NPWB18] or SMT-LIB v2 format [BFT17] by creating a parser bitwuzla::parser::Parser and then parsing the input file via bitwuzla::parser::Parser::parse().

Note

The input parser creates a Bitwuzla instance, which can be configured via the bitwuzla::Options instance passed into the parser. This Bitwuzla instance can be retrieved via bitwuzla::parser::Parser::bitwuzla().

For example, to parse an example file examples/smt2/quickstart.smt2 in SMT-LIB format:

  // 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
  {
    parser.parse("../smt2/quickstart.smt2");
  }
  catch (bitwuzla::parser::Exception& e)
  {
    // We expect no error to occur.
    std::cout << "unexpected parser exception" << std::endl;
  }

Note

If the input is given in SMT-LIB format, commands like check-sat or get-value will be executed while parsing if argument parse_only is passed into bitwuzla::parser::Parser::parse() as true.

After parsing from an input file, the parsed assertions can be retrieved via bitwuzla::Bitwuzla::get_assertions():

    // 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;

Alternatively, Bitwuzla also supports parsing from strings via bitwuzla::parser::Parser::parse(). The quickstart input above can be parsed as one huge input string, or any its subsets of commands.

Bitwuzla also allows to add onto input parsed from a file. For example, after parsing in examples/smt2/quickstart.smt2, which is satisfiable, we add an assertion (which now makes the input formula unsatisfiable) via parsing from string as follows:

    parser.parse("(assert (distinct (select a x) y))", true, false);

Bitwuzla also supports parsing terms and sorts from strings via bitwuzla::parser::Parser::parse_term() and bitwuzla::parser::Parser::parse_sort().

Note

Declarations like declare-const are commands (not terms) in the SMT-LIB language. Commands must be parsed in via bitwuzla::parser::Parser::parse(). Function bitwuzla::parser::Parser::parse_term() and bitwuzla::parser::Parser::parse_sort() only support parsing SMT-LIB terms and sorts, respectively.

For example, to parse a bit-vector sort of size 16 from string and show that it corresponds to the bit-vector sort of size 16 created via bitwuzla::mk_bv_sort():

    // 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));

Then, to declare Boolean constants c and d and a bit-vector constant b:

    parser.parse("(declare-const c Bool)(declare-const d Bool)", true, false);
    parser.parse("(declare-const b (_ BitVec 16))", true, false);

These terms can be retrieved via bitwuzla::parser::Parser::parse_term():

    // 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");

Now, to parse in terms using these constants via bitwuzla::parser::Parser::parse_term():

    // 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)}));

After parsing input and asserting formulas, satisfiability can be determined via bitwuzla::Bitwuzla::check_sat().

  Result result = bitwuzla.check_sat();

Formulas can also be assumed via passing a vector of assumptions into bitwuzla::Bitwuzla::check_sat().

If the formula is satisfiable and model generation has been enabled, the resulting model can be printed via bitwuzla::Bitwuzla::get_value() and bitwuzla::Term::str() (or bitwuzla::operator<<()). An example implementation illustrating how to print the current model via declared symbols (in this case x, y, f and a) is below:

  std::cout << "Model:" << std::endl << "(" << std::endl;
  for (const auto& term : {x, y, f, a})
  {
    Sort sort = term.sort();
    std::cout << "  (define-fun "
              << (term.symbol() ? *term.symbol()
                                : "@t" + std::to_string(term.id()))
              << " (";
    if (sort.is_fun())
    {
      bitwuzla::Term value = bitwuzla.get_value(term);
      assert(value.kind() == bitwuzla::Kind::LAMBDA);
      assert(value.num_children() == 2);
      while (value[1].kind() == bitwuzla::Kind::LAMBDA)
      {
        assert(value[0].is_variable());
        std::cout << "(" << value[0] << " " << value[0].sort() << ") ";
        value = value[1];
      }
      assert(value[0].is_variable());
      std::cout << "(" << value[0] << " " << value[0].sort() << ")) "
                << sort.fun_codomain() << " ";
      std::cout << value[1] << ")" << std::endl;
    }
    else
    {
      std::cout << ") " << sort << " " << bitwuzla.get_value(term) << ")"
                << std::endl;
    }
  }
  std::cout << ")" << std::endl << std::endl;

This will output a possible model, in this case:

(
  (define-fun x () (_ BitVec 8) #b10011111)
  (define-fun y () (_ BitVec 8) #b11111111)
  (define-fun f ((@bzla.var_74 (_ BitVec 8))  (@bzla.var_75 (_ BitVec 4))) (_ BitVec 8) (ite (and (= @bzla.var_74 #b10011111) (= @bzla.var_75 #b0011)) #b11111111 #b00000000))
  (define-fun a () (Array (_ BitVec 8) (_ BitVec 8)) (store ((as const (Array (_ BitVec 8) (_ BitVec 8))) #b00000000) #b10011111 #b11111111))
)

Alternatively, it is possible to query the value of terms as assignment string via bitwuzla::Term::value(), or as a term via bitwuzla::Bitwuzla::get_value().

Additionally, for floating-point values, bitwuzla::Term::value() allows to retrieve the assignment split into assignment strings for the sign bit, the exponent and the significand; for Boolean values as bool; and for RoundingMode values as BitwuzlaRoundingMode.

In our case, we can query the assignments of x and y, both bit-vector terms, as binary strings:

  // Both x and y are bit-vector terms and their value is a bit-vector
  // value that can be printed via Term::value().
  std::cout << "value of x: " << bitwuzla.get_value(x).value<std::string>(2)
            << std::endl;
  std::cout << "value of y: " << bitwuzla.get_value(y).value<std::string>(2)
            << std::endl;
  std::cout << std::endl;

This will print:

value of x: 10011111
value of y: 11111111

The value of f (a function term) and a (an array term), on the other hand, cannot be represented with a simple type. Thus, function values are given as bitwuzla::Kind::LAMBDA, and array values are given as bitwuzla::Kind::ARRAY_STORE. We can retrieve an SMT-LIB2 string representation of the values via bitwuzla::Term::str() (and bitwuzla::operator<<()):

  // f and a, on the other hand, are a function and array term, respectively.
  // The value of these terms is not a value term: for f, it is a lambda term,
  // and the value of a is represented as a store term. Thus we cannot use
  // Term::value(), but we can print the value of the terms via Term::str()
  // or operator<<.
  std::cout << "str() representation of value of f:" << std::endl
            << bitwuzla.get_value(f) << std::endl
            << std::endl;
  std::cout << "str() representation of value of a:" << std::endl
            << bitwuzla.get_value(a) << std::endl
            << std::endl;
  std::cout << std::endl;

This will print:

str() representation of value of f:
(lambda ((@bzla.var_74 (_ BitVec 8))) (lambda ((@bzla.var_75 (_ BitVec 4))) (ite (and (= @bzla.var_74 #b10011111) (= @bzla.var_75 #b0011)) #b11111111 #b00000000)))

str() representation of value of a:
(store ((as const (Array (_ BitVec 8) (_ BitVec 8))) #b00000000) #b10011111 #b11111111)

Note that the string representation of values representable as simple type (bit-vectors, boolean, floating-point, rounding mode) are given as pure value string (in the given number format) via bitwuzla::Term::value(). Their string representation retrieved via bitwuzla::Term::str(), however, is given in SMT-LIB2 format. For example,

  std::cout << "str() representation of value of x: " << bitwuzla.get_value(x)
            << std::endl;
  std::cout << "str() representation of value of y: " << bitwuzla.get_value(y)
            << std::endl;

This will print:

str() representation of value of x: #b10011111
str() representation of value of y: #b11111111

It is also possible to query the model value of expressions that do not occur in the input formula:

  Term v = bitwuzla.get_value(tm.mk_term(Kind::BV_MUL, {x, x}));
  std::cout << "value of v = x * x: " << v.value<std::string>(2) << std::endl;

This will print:

value of v = x * x: 11000001

Examples

All examples can be found in directory examples.
For instructions on how to build these examples, see examples/README.md.

Quickstart Example

The example used in the Quickstart guide.
The SMT-LIB input for this example can be found at examples/smt2/quickstart.smt2.
The source code for this example can be found at examples/cpp/quickstart.cpp.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
  5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
  6 *
  7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
  8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
  9 */
 10
 11#include <assert.h>
 12#include <bitwuzla/cpp/bitwuzla.h>
 13
 14#include <iostream>
 15
 16using namespace bitwuzla;
 17
 18int
 19main()
 20{
 21  // First, create a term manager instance.
 22  //! [docs-cpp-quickstart-0 start]
 23  TermManager tm;
 24  //! [docs-cpp-quickstart-0 end]
 25  // Create a Bitwuzla options instance.
 26  //! [docs-cpp-quickstart-1 start]
 27  Options options;
 28  //! [docs-cpp-quickstart-1 end]
 29  // Then, enable model generation.
 30  //! [docs-cpp-quickstart-2 start]
 31  options.set(Option::PRODUCE_MODELS, true);
 32  //! [docs-cpp-quickstart-2 end]
 33  // Now, for illustration purposes, we enable CaDiCaL as SAT solver
 34  // (CaDiCaL is already configured by default).
 35  // Note: This will silently fall back to one of the compiled in SAT solvers
 36  //       if the selected solver is not compiled in.
 37  //! [docs-cpp-quickstart-3 start]
 38  options.set(Option::SAT_SOLVER, "cadical");
 39  //! [docs-cpp-quickstart-3 end]
 40  // Then, create a Bitwuzla instance.
 41  //! [docs-cpp-quickstart-4 start]
 42  Bitwuzla bitwuzla(tm, options);
 43  //! [docs-cpp-quickstart-4 end]
 44
 45  //! [docs-cpp-quickstart-5 start]
 46  // Create bit-vector sorts of size 4 and 8.
 47  Sort sortbv4 = tm.mk_bv_sort(4);
 48  Sort sortbv8 = tm.mk_bv_sort(8);
 49  // Create function sort.
 50  Sort sortfun = tm.mk_fun_sort({sortbv8, sortbv4}, sortbv8);
 51  // Create array sort.
 52  Sort sortarr = tm.mk_array_sort(sortbv8, sortbv8);
 53
 54  // Create two bit-vector constants of that sort.
 55  Term x = tm.mk_const(sortbv8, "x");
 56  Term y = tm.mk_const(sortbv8, "y");
 57  // Create fun const.
 58  Term f = tm.mk_const(sortfun, "f");
 59  // Create array const.
 60  Term a = tm.mk_const(sortarr, "a");
 61  // Create bit-vector values one and two of the same sort.
 62  Term one = tm.mk_bv_one(sortbv8);
 63  // Alternatively, you can create bit-vector value one with:
 64  // Term one = tm.mk_bv_value(sortbv8, "1", 2);
 65  // Term one = tm.mk_bv_value_uint64(sortbv8, 1);
 66  Term two = tm.mk_bv_value_uint64(sortbv8, 2);
 67
 68  // (bvsdiv x (_ bv2 8))
 69  Term sdiv = tm.mk_term(Kind::BV_SDIV, {x, two});
 70  // (bvashr y (_ bv1 8))
 71  Term ashr = tm.mk_term(Kind::BV_ASHR, {y, one});
 72  // ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
 73  Term sdive = tm.mk_term(Kind::BV_EXTRACT, {sdiv}, {3, 0});
 74  // ((_ extract 3 0) (bvashr x (_ bv1 8)))
 75  Term ashre = tm.mk_term(Kind::BV_EXTRACT, {ashr}, {3, 0});
 76
 77  // (assert
 78  //     (distinct
 79  //         ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
 80  //         ((_ extract 3 0) (bvashr y (_ bv1 8)))))
 81  bitwuzla.assert_formula(tm.mk_term(Kind::DISTINCT, {sdive, ashre}));
 82  // (assert (= (f x ((_ extract 6 3) x)) y))
 83  bitwuzla.assert_formula(
 84      tm.mk_term(Kind::EQUAL,
 85                 {tm.mk_term(Kind::APPLY,
 86                             {f, x, tm.mk_term(Kind::BV_EXTRACT, {x}, {6, 3})}),
 87                  y}));
 88  // (assert (= (select a x) y))
 89  bitwuzla.assert_formula(
 90      tm.mk_term(Kind::EQUAL, {tm.mk_term(Kind::ARRAY_SELECT, {a, x}), y}));
 91  //! [docs-cpp-quickstart-5 end]
 92
 93  // (check-sat)
 94  //! [docs-cpp-quickstart-6 start]
 95  Result result = bitwuzla.check_sat();
 96  //! [docs-cpp-quickstart-6 end]
 97
 98  std::cout << "Expect: sat" << std::endl;
 99  std::cout << "Bitwuzla: " << result << std::endl;
100
101  // Print model in SMT-LIBv2 format.
102  //! [docs-cpp-quickstart-7 start]
103  std::cout << "Model:" << std::endl << "(" << std::endl;
104  for (const auto& term : {x, y, f, a})
105  {
106    Sort sort = term.sort();
107    std::cout << "  (define-fun "
108              << (term.symbol() ? *term.symbol()
109                                : "@t" + std::to_string(term.id()))
110              << " (";
111    if (sort.is_fun())
112    {
113      bitwuzla::Term value = bitwuzla.get_value(term);
114      assert(value.kind() == bitwuzla::Kind::LAMBDA);
115      assert(value.num_children() == 2);
116      while (value[1].kind() == bitwuzla::Kind::LAMBDA)
117      {
118        assert(value[0].is_variable());
119        std::cout << "(" << value[0] << " " << value[0].sort() << ") ";
120        value = value[1];
121      }
122      assert(value[0].is_variable());
123      std::cout << "(" << value[0] << " " << value[0].sort() << ")) "
124                << sort.fun_codomain() << " ";
125      std::cout << value[1] << ")" << std::endl;
126    }
127    else
128    {
129      std::cout << ") " << sort << " " << bitwuzla.get_value(term) << ")"
130                << std::endl;
131    }
132  }
133  std::cout << ")" << std::endl << std::endl;
134  //! [docs-cpp-quickstart-7 end]
135
136  // Print value for x, y, f and a.
137  // Note: The returned string of Term::value() is only valid until the next
138  //       call to Term::value().
139  //! [docs-cpp-quickstart-8 start]
140  // Both x and y are bit-vector terms and their value is a bit-vector
141  // value that can be printed via Term::value().
142  std::cout << "value of x: " << bitwuzla.get_value(x).value<std::string>(2)
143            << std::endl;
144  std::cout << "value of y: " << bitwuzla.get_value(y).value<std::string>(2)
145            << std::endl;
146  std::cout << std::endl;
147  //! [docs-cpp-quickstart-8 end]
148  //! [docs-cpp-quickstart-9 start]
149  // f and a, on the other hand, are a function and array term, respectively.
150  // The value of these terms is not a value term: for f, it is a lambda term,
151  // and the value of a is represented as a store term. Thus we cannot use
152  // Term::value(), but we can print the value of the terms via Term::str()
153  // or operator<<.
154  std::cout << "str() representation of value of f:" << std::endl
155            << bitwuzla.get_value(f) << std::endl
156            << std::endl;
157  std::cout << "str() representation of value of a:" << std::endl
158            << bitwuzla.get_value(a) << std::endl
159            << std::endl;
160  std::cout << std::endl;
161  //! [docs-cpp-quickstart-9 end]
162  // Note that the assignment string of bit-vector terms is given as the
163  // pure assignment string, either in binary, hexadecimal or decimal format,
164  // whereas Term::str() and operator<< print the value in SMT-LIB2 format
165  // ((in the configured bit-vector output number format, binary by default).
166  //! [docs-cpp-quickstart-10 start]
167  std::cout << "str() representation of value of x: " << bitwuzla.get_value(x)
168            << std::endl;
169  std::cout << "str() representation of value of y: " << bitwuzla.get_value(y)
170            << std::endl;
171  //! [docs-cpp-quickstart-10 end]
172  std::cout << std::endl;
173
174  // Query value of bit-vector term that does not occur in the input formula
175  //! [docs-cpp-quickstart-11 start]
176  Term v = bitwuzla.get_value(tm.mk_term(Kind::BV_MUL, {x, x}));
177  std::cout << "value of v = x * x: " << v.value<std::string>(2) << std::endl;
178  //! [docs-cpp-quickstart-11 end]
179
180  return 0;
181}

Options Example

An example for how to set and get options.
The SMT-LIB input for this example can be found at examples/smt2/options.smt2.
The source code for this example can be found at examples/cpp/options.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12
13#include <iostream>
14
15using namespace bitwuzla;
16
17int
18main()
19{
20  // First, create a Bitwuzla options instance.
21  Options options;
22
23  // Enable model generation, which expects a boolean configuration value.
24  options.set(Option::PRODUCE_MODELS, true);
25
26  // Increase the verbosity level, which expects an integer value.
27  std::cout << "Previous verbosity level: " << options.get(Option::VERBOSITY)
28            << std::endl;
29  options.set(Option::VERBOSITY, 2);
30  std::cout << "Current verbosity level: " << options.get(Option::VERBOSITY)
31            << std::endl;
32
33  // Now configure an option that has modes (a choice of configuration values).
34  // First, query which bit-vector solver engine is set.
35  std::cout << "Default bv solver: " << options.get_mode(Option::BV_SOLVER)
36            << std::endl;
37  // Then, select the propagation-based local search engine as solver engine.
38  options.set(Option::BV_SOLVER, "prop");
39  std::cout << "Current engine: " << options.get_mode(Option::BV_SOLVER)
40            << std::endl;
41
42  // Now, create a Bitwuzla instance with a new term manager.
43  TermManager tm;
44  Bitwuzla bitwuzla(tm, options);
45  // Check sat (nothing to solve, input formula is empty).
46  Result result = bitwuzla.check_sat();
47  std::cout << "Expect: sat" << std::endl;
48  std::cout << "Bitwuzla: " << result << std::endl;
49
50  return 0;
51}

Option Info Example

An example for how to get information about options via OptionInfo.
The source code for this example can be found at examples/cpp/option_info.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12
13#include <iostream>
14
15using namespace bitwuzla;
16
17int
18main()
19{
20  // First, create a Bitwuzla options instance.
21  Options options;
22  // Set some options to illustrate current vs default value.
23  options.set(Option::PRODUCE_MODELS, true);
24  options.set(Option::VERBOSITY, 2);
25  options.set(Option::BV_SOLVER, "prop");
26
27  // Then iterate over all available configuration options and extract info.
28  for (int32_t i = 0; i < static_cast<int32_t>(Option::NUM_OPTS); ++i)
29  {
30    Option opt = static_cast<Option>(i);
31    OptionInfo info(options, opt);
32    std::cout << "- long name:   " << info.lng << std::endl;
33    std::cout << "  short name:  " << (info.shrt ? info.shrt : "-")
34              << std::endl;
35    std::cout << "  kind:        ";
36    if (info.kind == OptionInfo::Kind::BOOL)
37    {
38      std::cout << "bool" << std::endl;
39      std::cout << "  values:" << std::endl;
40      const auto& values = std::get<OptionInfo::Bool>(info.values);
41      std::cout << "  + current:   " << (values.cur ? "true" : "false")
42                << std::endl;
43      std::cout << "  + default:   " << (values.dflt ? "true" : "false")
44                << std::endl;
45    }
46    else if (info.kind == OptionInfo::Kind::NUMERIC)
47    {
48      std::cout << "numeric" << std::endl;
49      std::cout << "  values:" << std::endl;
50      const auto& values = std::get<OptionInfo::Numeric>(info.values);
51      std::cout << "  + current:   " << values.dflt << std::endl;
52      std::cout << "  + default:   " << values.cur << std::endl;
53      std::cout << "  + min:       " << values.min << std::endl;
54      std::cout << "  + max:       " << values.max << std::endl;
55    }
56    else
57    {
58      std::cout << "modes" << std::endl;
59      std::cout << "  values:" << std::endl;
60      const auto& values = std::get<OptionInfo::Mode>(info.values);
61      std::cout << "  + current:   " << values.dflt << std::endl;
62      std::cout << "  + default:   " << values.cur << std::endl;
63      std::cout << "  + modes:     {";
64      for (size_t i = 0, n = values.modes.size(); i < n; ++i)
65      {
66        std::cout << (i > 0 ? "," : "") << " " << values.modes[i];
67      }
68      std::cout << " }" << std::endl;
69    }
70    std::cout << "  description: " << info.description << std::endl;
71    std::cout << std::endl;
72  }
73}

Incremental Example with push and pop

An incremental example with push and pop.
The SMT-LIB input for this example can be found at examples/smt2/pushpop.smt2.
The source code for this example can be found at examples/cpp/pushpop.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12
13#include <iostream>
14
15using namespace bitwuzla;
16
17int
18main()
19{
20  // First, create a term manager instance.
21  TermManager tm;
22  // Create a Bitwuzla options instance.
23  Options options;
24  // Then, create a Bitwuzla instance.
25  Bitwuzla bitwuzla(tm, options);
26
27  // Create a bit-vector sort of size 1.
28  Sort sortbv1 = tm.mk_bv_sort(1);
29  // Create a bit-vector sort of size 2.
30  Sort sortbv2 = tm.mk_bv_sort(2);
31
32  // Create bit-vector variables.
33  // (declare-const o0 (_ BitVec 1))
34  Term o0 = tm.mk_const(sortbv1, "o0");
35  // (declare-const o1 (_ BitVec 1))
36  Term o1 = tm.mk_const(sortbv1, "o1");
37  // (declare-const s0 (_ BitVec 2))
38  Term s0 = tm.mk_const(sortbv2, "s0");
39  // (declare-const s1 (_ BitVec 2))
40  Term s1 = tm.mk_const(sortbv2, "s1");
41  // (declare-const s2 (_ BitVec 2))
42  Term s2 = tm.mk_const(sortbv2, "s2");
43  // (declare-const goal (_ BitVec 2))
44  Term goal = tm.mk_const(sortbv2, "goal");
45
46  // Create bit-vector values zero, one, three.
47  Term zero  = tm.mk_bv_zero(sortbv2);
48  Term one1  = tm.mk_bv_one(sortbv1);
49  Term one2  = tm.mk_bv_one(sortbv2);
50  Term three = tm.mk_bv_value_uint64(sortbv2, 3);
51
52  // Add some assertions.
53  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {s0, zero}));
54  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {goal, three}));
55
56  // Push, assert, check sat and pop.
57  bitwuzla.push(1);
58  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {s0, goal}));
59  Result result = bitwuzla.check_sat();
60  std::cout << "Expect: unsat" << std::endl;
61  std::cout << "Bitwuzla: " << result << std::endl;
62  bitwuzla.pop(1);
63
64  // (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
65  bitwuzla.assert_formula(
66      tm.mk_term(Kind::EQUAL,
67                 {s1,
68                  tm.mk_term(Kind::ITE,
69                             {tm.mk_term(Kind::EQUAL, {o0, one1}),
70                              tm.mk_term(Kind::BV_ADD, {s0, one2}),
71                              s0})}));
72
73  // Push, assert, check sat and pop.
74  bitwuzla.push(1);
75  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {s1, goal}));
76  result = bitwuzla.check_sat();
77  std::cout << "Expect: unsat" << std::endl;
78  std::cout << "Bitwuzla: " << result << std::endl;
79  bitwuzla.pop(1);
80
81  // (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
82  bitwuzla.assert_formula(
83      tm.mk_term(Kind::EQUAL,
84                 {s2,
85                  tm.mk_term(Kind::ITE,
86                             {tm.mk_term(Kind::EQUAL, {o1, one1}),
87                              tm.mk_term(Kind::BV_ADD, {s1, one2}),
88                              s1})}));
89
90  // Push, assert, check sat and pop.
91  bitwuzla.push(1);
92  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {s2, goal}));
93  result = bitwuzla.check_sat();
94  std::cout << "Expect: unsat" << std::endl;
95  std::cout << "Bitwuzla: " << result << std::endl;
96  bitwuzla.pop(1);
97
98  return 0;
99}

Incremental Example with check-sat-assuming

This example shows how to implement the example above with check-sat-assuming.
The SMT-LIB input for this example can be found at examples/smt2/checksatassuming.smt2.
The source code for this example can be found at examples/cpp/checksatassuming.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12
13#include <iostream>
14
15using namespace bitwuzla;
16
17int
18main()
19{
20  Result result;
21
22  // First, create a term manager instance.
23  TermManager tm;
24  // Create a Bitwuzla options instance.
25  Options options;
26  // Then, create a Bitwuzla instance.
27  Bitwuzla bitwuzla(tm, options);
28
29  // Create a bit-vector sort of size 1.
30  Sort sortbv1 = tm.mk_bv_sort(1);
31  // Create a bit-vector sort of size 2
32  Sort sortbv2 = tm.mk_bv_sort(2);
33
34  // Create bit-vector variables.
35  // (declare-const o0 (_ BitVec 1))
36  Term o0 = tm.mk_const(sortbv1, "o0");
37  // (declare-const o1 (_ BitVec 1))
38  Term o1 = tm.mk_const(sortbv1, "o1");
39  // (declare-const s0 (_ BitVec 2))
40  Term s0 = tm.mk_const(sortbv2, "s0");
41  // (declare-const s1 (_ BitVec 2))
42  Term s1 = tm.mk_const(sortbv2, "s1");
43  // (declare-const s2 (_ BitVec 2))
44  Term s2 = tm.mk_const(sortbv2, "s2");
45  // (declare-const goal (_ BitVec 2))
46  Term goal = tm.mk_const(sortbv2, "goal");
47
48  // Create bit-vector values zero, one, three.
49  Term zero  = tm.mk_bv_zero(sortbv2);
50  Term one1  = tm.mk_bv_one(sortbv1);
51  Term one2  = tm.mk_bv_one(sortbv2);
52  Term three = tm.mk_bv_value_uint64(sortbv2, 3);
53
54  // Add some assertions.
55  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {s0, zero}));
56  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {goal, three}));
57
58  // (check-sat-assuming ((= s0 goal)))
59  result = bitwuzla.check_sat({tm.mk_term(Kind::EQUAL, {s0, goal})});
60  std::cout << "Expect: unsat" << std::endl;
61  std::cout << "Bitwuzla: " << result << std::endl;
62
63  // (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
64  bitwuzla.assert_formula(
65      tm.mk_term(Kind::EQUAL,
66                 {s1,
67                  tm.mk_term(Kind::ITE,
68                             {tm.mk_term(Kind::EQUAL, {o0, one1}),
69                              tm.mk_term(Kind::BV_ADD, {s0, one2}),
70                              s0})}));
71
72  // (check-sat-assuming ((= s1 goal)))
73  result = bitwuzla.check_sat({tm.mk_term(Kind::EQUAL, {s1, goal})});
74  std::cout << "Expect: unsat" << std::endl;
75  std::cout << "Bitwuzla: " << result << std::endl;
76
77  // (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
78  bitwuzla.assert_formula(
79      tm.mk_term(Kind::EQUAL,
80                 {s2,
81                  tm.mk_term(Kind::ITE,
82                             {tm.mk_term(Kind::EQUAL, {o1, one1}),
83                              tm.mk_term(Kind::BV_ADD, {s1, one2}),
84                              s1})}));
85
86  // (check-sat-assuming ((= s2 goal)))
87  result = bitwuzla.check_sat({tm.mk_term(Kind::EQUAL, {s2, goal})});
88  std::cout << "Expect: unsat" << std::endl;
89  std::cout << "Bitwuzla: " << result << std::endl;
90
91  return 0;
92}

Unsat Core Example

This example shows how to extract an unsat core. It creates bit-vector and floating-point terms and further illustrates how to create lambda terms (define-fun).

The SMT-LIB input for this example can be found at examples/smt2/unsatcore.smt2.
The source code for this example can be found at examples/cpp/unsatcore.cpp.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
  5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
  6 *
  7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
  8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
  9 */
 10
 11#include <bitwuzla/cpp/bitwuzla.h>
 12
 13using namespace bitwuzla;
 14
 15int
 16main()
 17{
 18  // First, create a term manager instance.
 19  TermManager tm;
 20  // Create a Bitwuzla options instance.
 21  Options options;
 22  // Then, enable unsat core extraction.
 23  // Note: Unsat core extraction is disabled by default.
 24  options.set(Option::PRODUCE_UNSAT_CORES, true);
 25  // Then, create a Bitwuzla instance.
 26  Bitwuzla bitwuzla(tm, options);
 27
 28  // Create a bit-vector sort of size 2.
 29  Sort sortbv2 = tm.mk_bv_sort(2);
 30  // Create a bit-vector sort of size 4.
 31  Sort sortbv4 = tm.mk_bv_sort(4);
 32  // Create Float16 floatinf-point sort.
 33  Sort sortfp16 = tm.mk_fp_sort(5, 11);
 34
 35  // Create bit-vector variables.
 36  // (declare-const x0 (_ BitVec 4))
 37  Term x0 = tm.mk_const(sortbv4, "x0");
 38  // (declare-const x1 (_ BitVec 2))
 39  Term x1 = tm.mk_const(sortbv2, "x1");
 40  // (declare-const x2 (_ BitVec 2))
 41  Term x2 = tm.mk_const(sortbv2, "x2");
 42  // (declare-const x3 (_ BitVec 2))
 43  Term x3 = tm.mk_const(sortbv2, "x3");
 44  // (declare-const x4 Float16)
 45  Term x4 = tm.mk_const(sortfp16, "x4");
 46
 47  // Create FP positive zero.
 48  Term fpzero = tm.mk_fp_pos_zero(sortfp16);
 49  // Create BV zero of size 4.
 50  Term bvzero = tm.mk_bv_zero(sortbv4);
 51
 52  // (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
 53  Term a_f0 = tm.mk_var(sortfp16, "a_f0");
 54  Term f0 =
 55      tm.mk_term(Kind::LAMBDA, {a_f0, tm.mk_term(Kind::FP_GT, {a_f0, fpzero})});
 56
 57  // (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
 58  Term a_f1 = tm.mk_var(sortfp16, "a_f1");
 59  Term f1   = tm.mk_term(
 60      Kind::LAMBDA,
 61      {a_f1,
 62         tm.mk_term(Kind::ITE,
 63                    {tm.mk_term(Kind::APPLY, {f0, a_f1}), x0, bvzero})});
 64
 65  // (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
 66  Term a_f2 = tm.mk_var(sortfp16, "a_f2");
 67  Term f2   = tm.mk_term(
 68      Kind::LAMBDA,
 69      {a_f2,
 70         tm.mk_term(
 71           Kind::BV_EXTRACT, {tm.mk_term(Kind::APPLY, {f1, a_f2})}, {1, 0})});
 72
 73  // (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
 74  Term a0 =
 75      tm.mk_term(Kind::BV_ULT, {x2, tm.mk_term(Kind::APPLY, {f2, fpzero})});
 76  bitwuzla.assert_formula(a0);
 77
 78  // (assert (! (= x1 x2 x3) :named a1))
 79  Term a1 = tm.mk_term(Kind::EQUAL, {x1, x2, x3});
 80  bitwuzla.assert_formula(a1);
 81
 82  // (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
 83  Term a2 = tm.mk_term(Kind::EQUAL,
 84                       {x4,
 85                        tm.mk_term(Kind::FP_TO_FP_FROM_UBV,
 86                                   {tm.mk_rm_value(RoundingMode::RNE), x3},
 87                                   {5, 11})});
 88  bitwuzla.assert_formula(a2);
 89
 90  // (check-sat)
 91  Result result = bitwuzla.check_sat();
 92  std::cout << "Expect: unsat" << std::endl;
 93  std::cout << "Bitwuzla: " << result << std::endl;
 94
 95  // (get-unsat-core)
 96  auto unsat_core = bitwuzla.get_unsat_core();
 97  std::cout << "Unsat Core:" << std::endl << "{" << std::endl;
 98  for (const auto& t : unsat_core)
 99  {
100    std::cout << " " << t << std::endl;
101  }
102  std::cout << "}" << std::endl;
103
104  return 0;
105}

Unsat Assumptions Example

This example shows how to implement the example above with get-unsat-assumptions.
The SMT-LIB input for this example can be found at examples/smt2/unsatassumptions.smt2.
The source code for this example can be found at examples/cpp/unsatassumptions.cpp.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
  5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
  6 *
  7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
  8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
  9 */
 10
 11#include <bitwuzla/cpp/bitwuzla.h>
 12
 13#include <iostream>
 14
 15using namespace bitwuzla;
 16
 17int
 18main()
 19{
 20  // First, create a term manager instance.
 21  TermManager tm;
 22  // Create a Bitwuzla options instance.
 23  Options options;
 24  // (set-option :produce-unsat-assumptions true)
 25  options.set(Option::PRODUCE_UNSAT_ASSUMPTIONS, true);
 26  // Then, create a Bitwuzla instance.
 27  Bitwuzla bitwuzla(tm, options);
 28
 29  // Create Boolean sort.
 30  Sort sortbool = tm.mk_bool_sort();
 31  // Create a bit-vector sort of size 2.
 32  Sort sortbv2 = tm.mk_bv_sort(2);
 33  // Create a bit-vector sort of size 4.
 34  Sort sortbv4 = tm.mk_bv_sort(4);
 35  // Create Float16 floatinf-point sort.
 36  Sort sortfp16 = tm.mk_fp_sort(5, 11);
 37  // Create bit-vector variables.
 38  // (declare-const x0 (_ BitVec 4))
 39  Term x0 = tm.mk_const(sortbv4, "x0");
 40  // (declare-const x1 (_ BitVec 2))
 41  Term x1 = tm.mk_const(sortbv2, "x1");
 42  // (declare-const x2 (_ BitVec 2))
 43  Term x2 = tm.mk_const(sortbv2, "x2");
 44  // (declare-const x3 (_ BitVec 2))
 45  Term x3 = tm.mk_const(sortbv2, "x3");
 46  // (declare-const x4 Float16)
 47  Term x4 = tm.mk_const(sortfp16, "x4");
 48
 49  // Create FP positive zero.
 50  Term fpzero = tm.mk_fp_pos_zero(sortfp16);
 51  // Create BV zero of size 4.
 52  Term bvzero = tm.mk_bv_zero(sortbv4);
 53
 54  // (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
 55  Term a_f0 = tm.mk_var(sortfp16, "a_f0");
 56  Term f0 =
 57      tm.mk_term(Kind::LAMBDA, {a_f0, tm.mk_term(Kind::FP_GT, {a_f0, fpzero})});
 58
 59  // (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
 60  Term a_f1 = tm.mk_var(sortfp16, "a_f1");
 61  Term f1   = tm.mk_term(
 62      Kind::LAMBDA,
 63      {a_f1,
 64         tm.mk_term(Kind::ITE,
 65                    {tm.mk_term(Kind::APPLY, {f0, a_f1}), x0, bvzero})});
 66
 67  // (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
 68  Term a_f2 = tm.mk_var(sortfp16, "a_f2");
 69  Term f2   = tm.mk_term(
 70      Kind::LAMBDA,
 71      {a_f2,
 72         tm.mk_term(
 73           Kind::BV_EXTRACT, {tm.mk_term(Kind::APPLY, {f1, a_f2})}, {1, 0})});
 74
 75  // (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
 76  Term a0 = tm.mk_const(sortbool, "a0");
 77  Term assumption0 =
 78      tm.mk_term(Kind::BV_ULT, {x2, tm.mk_term(Kind::APPLY, {f2, fpzero})});
 79  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {a0, assumption0}));
 80  // (assert (! (= x1 x2 x3) :named a1))
 81  Term a1          = tm.mk_const(sortbool, "a1");
 82  Term assumption1 = tm.mk_term(Kind::EQUAL, {x1, x2, x3});
 83  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {a1, assumption1}));
 84  // (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
 85  Term a2 = tm.mk_const(sortbool, "a2");
 86  Term assumption2 =
 87      tm.mk_term(Kind::EQUAL,
 88                 {x4,
 89                  tm.mk_term(Kind::FP_TO_FP_FROM_UBV,
 90                             {tm.mk_rm_value(RoundingMode::RNE), x3},
 91                             {5, 11})});
 92  bitwuzla.assert_formula(tm.mk_term(Kind::EQUAL, {a2, assumption2}));
 93
 94  // (check-sat-assuming (assumption0 assumption1 assumption2))
 95  Result result = bitwuzla.check_sat({a0, a1, a2});
 96  std::cout << "Expect: unsat" << std::endl;
 97  std::cout << "Bitwuzla: " << result << std::endl;
 98
 99  // (get-unsat-assumptions)
100  auto unsat_assumptions = bitwuzla.get_unsat_assumptions();
101  std::cout << "Unsat Assumptions: {";
102  for (const auto& a : unsat_assumptions)
103  {
104    std::cout << " " << a;
105  }
106  std::cout << " }" << std::endl;
107
108  return 0;
109}

Reset Example

This example shows how to reset the solver instance (SMT-LIB command reset).
The SMT-LIB input for this example can be found at examples/smt2/reset.smt2.
The source code for this example can be found at examples/cpp/reset.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12
13#include <iostream>
14
15using namespace bitwuzla;
16
17int
18main()
19{
20  Result result;
21
22  // First, create a term manager instance.
23  TermManager tm;
24  // Create a Bitwuzla options instance.
25  Options options;
26  // (set-option :produce-models false)
27  options.set(Option::PRODUCE_MODELS, false);
28
29  // Then, create a Bitwuzla instance.
30  std::unique_ptr<Bitwuzla> bitwuzla(new Bitwuzla(tm, options));
31
32  // Create a bit-vector sort of size 3.
33  Sort sortbv3 = tm.mk_bv_sort(3);
34
35  // (declare-const x (_ BitVec 3))
36  Term x = tm.mk_const(sortbv3, "x");
37
38  // (assert (= x #b010))
39  bitwuzla->assert_formula(
40      tm.mk_term(Kind::EQUAL, {x, tm.mk_bv_value_uint64(sortbv3, 2)}));
41  // (check-sat)
42  result = bitwuzla->check_sat();
43  std::cout << "Expect: sat" << std::endl;
44  std::cout << "Bitwuzla: " << result << std::endl;
45
46  // (set-option :produce-models true)
47  options.set(Option::PRODUCE_MODELS, true);
48
49  // (reset)
50  // Note: Bitwuzla does not provide an explicit API function for reset since
51  //       this is achieved by simply discarding the current Bitwuzla instance
52  //       and creating a new one.
53  bitwuzla.reset(new Bitwuzla(tm, options));
54
55  // (declare-const a ( Array (_ BitVec 2) (_ BitVec 3)))
56  Sort sortbv2 = tm.mk_bv_sort(2);
57  Term a       = tm.mk_const(tm.mk_array_sort(sortbv2, sortbv3), "a");
58
59  // (assert (= x #b011))
60  bitwuzla->assert_formula(
61      tm.mk_term(Kind::EQUAL, {x, tm.mk_bv_value_uint64(sortbv3, 3)}));
62  // (assert (= x (select a #b01)))
63  bitwuzla->assert_formula(
64      tm.mk_term(Kind::EQUAL,
65                 {x,
66                  tm.mk_term(Kind::ARRAY_SELECT,
67                             {a, tm.mk_bv_value_uint64(sortbv2, 1)})}));
68  // (check-sat)
69  result = bitwuzla->check_sat();
70  std::cout << "Expect: sat" << std::endl;
71  std::cout << "Bitwuzla: " << result << std::endl;
72  // (get-model)
73  std::cout << "(" << std::endl
74            << "  (define-fun " << x.symbol()->get() << " () " << x.sort()
75            << " " << bitwuzla->get_value(x) << ")" << std::endl
76            << "  (define-fun " << a.symbol()->get() << " () " << a.sort()
77            << " " << bitwuzla->get_value(a) << ")" << std::endl
78            << ")" << std::endl;
79
80  return 0;
81}

Reset Assertions Example

This example shows how to reset the currently asserted formulas of a solver instance (SMT-LIB command reset-assertions).
The SMT-LIB input for this example can be found at examples/smt2/reset_assertions.smt2.
The source code for this example can be found at examples/cpp/reset_assertions.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12
13#include <iostream>
14
15using namespace bitwuzla;
16
17int
18main()
19{
20  Result result;
21
22  // First, create a term manager instance.
23  TermManager tm;
24  // Create a Bitwuzla options instance.
25  Options options;
26  // (set-option :produce-models true)
27  options.set(Option::PRODUCE_MODELS, true);
28  // Then, create a Bitwuzla instance.
29  std::unique_ptr<Bitwuzla> bitwuzla(new Bitwuzla(tm, options));
30
31  // Create a bit-vector sort of size 3.
32  Sort sortbv3 = tm.mk_bv_sort(3);
33
34  // (declare-const x (_ BitVec 3))
35  Term x = tm.mk_const(sortbv3, "x");
36
37  // (assert (= x #b010))
38  bitwuzla->assert_formula(
39      tm.mk_term(Kind::EQUAL, {x, tm.mk_bv_value_uint64(sortbv3, 2)}));
40  // (check-sat)
41  result = bitwuzla->check_sat();
42  std::cout << "Expect: sat" << std::endl;
43  std::cout << "Bitwuzla: " << result << std::endl;
44
45  // (assert (= x #b001))
46  bitwuzla->assert_formula(
47      tm.mk_term(Kind::EQUAL, {x, tm.mk_bv_value_uint64(sortbv3, 1)}));
48  // (check-sat)
49  result = bitwuzla->check_sat();
50  std::cout << "Expect: unsat" << std::endl;
51  std::cout << "Bitwuzla: " << result << std::endl;
52
53  // (reset-assertions)
54  // Note: Bitwuzla does not provide an explicit API function for
55  //       reset-assertions since this is achieved by simply discarding
56  //       the current Bitwuzla instance and creating a new one.
57  bitwuzla.reset(new Bitwuzla(tm, options));
58
59  // (assert (= x #b011))
60  bitwuzla->assert_formula(
61      tm.mk_term(Kind::EQUAL, {x, tm.mk_bv_value_uint64(sortbv3, 3)}));
62  // (check-sat)
63  result = bitwuzla->check_sat();
64  std::cout << "Expect: sat" << std::endl;
65  std::cout << "Bitwuzla: " << result << std::endl;
66
67  // (get-model)
68  std::cout << "(" << std::endl
69            << "  (define-fun " << x.symbol()->get() << " () " << x.sort()
70            << " " << bitwuzla->get_value(x) << ")" << std::endl
71            << ")" << std::endl;
72
73  return 0;
74}

Parsing Example

This example shows how to parse an input file via the API.
The source code for this example can be found at examples/cpp/parse.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12#include <bitwuzla/cpp/parser.h>
13
14#include <cassert>
15#include <iostream>
16
17using namespace bitwuzla;
18
19int
20main()
21{
22  // First, create a term manager instance.
23  TermManager tm;
24  // Create a Bitwuzla options instance.
25  Options options;
26
27  // We will parse example file `smt2/quickstart.smt2`.
28  // Create parser instance.
29  parser::Parser parser(tm, options);
30
31  try
32  {
33    // Now parse the input file.
34    std::cout << "Expect: sat" << std::endl;
35    std::cout << "Bitwuzla: ";
36    parser.parse("../smt2/quickstart.smt2");
37
38    // Now we retrieve the set of asserted formulas and print them.
39    auto assertions = parser.bitwuzla()->get_assertions();
40    std::cout << "Assertions:" << std::endl << "{" << std::endl;
41    for (const auto& a : assertions)
42    {
43      std::cout << "  " << a << std::endl;
44    }
45    std::cout << "}" << std::endl;
46
47    // Now we add an assertion via parsing from string.
48    parser.parse("(assert (distinct (select a x) y))", true, false);
49    // Now the formula is unsat.
50    Result result = parser.bitwuzla()->check_sat();
51
52    std::cout << "Expect: unsat" << std::endl;
53    std::cout << "Bitwuzla: " << result << std::endl;
54
55    // For illustration purposes, we now parse in some declarations and terms
56    // and sorts from string.
57
58    // Declare bit-vector sort of size 16.
59    Sort bv16 = parser.parse_sort("(_ BitVec 16)");
60    // Create bit-vector sort of size 16 and show that it corresponds to
61    // its string representation '(_ BitVec16)'.
62    assert(bv16 == tm.mk_bv_sort(16));
63
64    // Declare Boolean constants 'c' and 'd'.
65    // Note: Declarations are commands (not terms) in the SMT-LIB language.
66    //       Commands must be parsed in via Parser::parse(),
67    //       Parser::parse_term() only supports parsing SMT-LIB terms.
68    parser.parse("(declare-const c Bool)(declare-const d Bool)", true, false);
69    // Declare bit-vector constant 'b'.
70    parser.parse("(declare-const b (_ BitVec 16))", true, false);
71    // Retrieve term representing 'b'.
72    Term b = parser.parse_term("b");
73    // Retrieve term representing 'c'.
74    Term c = parser.parse_term("c");
75    // Retrieve term representing 'd'.
76    Term d = parser.parse_term("d");
77    // Create xor over 'c' and 'd' and show that it corresponds to term
78    // parsed in from its string representation '(xor c d)'.
79    assert(parser.parse_term("(xor c d)") == tm.mk_term(Kind::XOR, {c, d}));
80    // Create bit-vector addition over 'b' and bit-vector value
81    // '1011111010001010' and show that it corresponds to the term parsed in
82    // from its string representation '(bvadd b #b1011111010001010)'.
83    assert(parser.parse_term("(bvadd b #b1011111010001010)")
84           == tm.mk_term(Kind::BV_ADD,
85                         {b, tm.mk_bv_value(bv16, "1011111010001010", 2)}));
86  }
87  catch (bitwuzla::parser::Exception& e)
88  {
89    // We expect no error to occur.
90    std::cout << "unexpected parser exception" << std::endl;
91  }
92  return 0;
93}

Printing Example

This example shows how to print sorts, terms and formulas via the API.
The source code for this example can be found at examples/cpp/print.cpp.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
  5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
  6 *
  7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
  8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
  9 */
 10
 11#include <bitwuzla/cpp/bitwuzla.h>
 12
 13#include <cassert>
 14#include <iomanip>
 15#include <iostream>
 16#include <sstream>
 17
 18using namespace bitwuzla;
 19
 20int
 21main()
 22{
 23  // First, create a term manager instance.
 24  TermManager tm;
 25  // Create a Bitwuzla options instance.
 26  Options options;
 27  options.set(Option::PRODUCE_MODELS, true);
 28  // Then, create a Bitwuzla instance.
 29  Bitwuzla bitwuzla(tm, options);
 30  // Create some sorts.
 31  Sort bv8  = tm.mk_bv_sort(8);
 32  Sort bv32 = tm.mk_bv_sort(32);
 33  Sort fp16 = tm.mk_fp_sort(5, 11);
 34  // Create terms.
 35  Term b    = tm.mk_const(tm.mk_bool_sort(), "b");
 36  Term bv   = tm.mk_const(bv8, "bv");
 37  Term fp   = tm.mk_const(fp16, "fp");
 38  Term rm   = tm.mk_const(tm.mk_rm_sort(), "rm");
 39  Term fun  = tm.mk_const(tm.mk_fun_sort({bv8, fp16, bv32}, fp16), "fun");
 40  Term zero = tm.mk_bv_zero(bv8);
 41  Term ones = tm.mk_bv_ones(tm.mk_bv_sort(23));
 42  Term z    = tm.mk_var(bv8, "z");
 43  Term q    = tm.mk_var(bv8, "q");
 44  Term lambda =
 45      tm.mk_term(Kind::LAMBDA, {z, tm.mk_term(Kind::BV_ADD, {z, bv})});
 46  Term fpleq = tm.mk_term(
 47      Kind::FP_LEQ,
 48      {tm.mk_term(Kind::APPLY,
 49                  {fun, bv, fp, tm.mk_term(Kind::BV_ZERO_EXTEND, {ones}, {9})}),
 50       fp});
 51  Term exists = tm.mk_term(
 52      Kind::EXISTS,
 53      {q, tm.mk_term(Kind::EQUAL, {zero, tm.mk_term(Kind::BV_MUL, {bv, q})})});
 54  // Assert formulas.
 55  bitwuzla.assert_formula(b);
 56  bitwuzla.assert_formula(
 57      tm.mk_term(Kind::EQUAL, {tm.mk_term(Kind::APPLY, {lambda, bv}), zero}));
 58  bitwuzla.assert_formula(exists);
 59  bitwuzla.assert_formula(fpleq);
 60
 61  // Print sort.
 62  std::cout << "Print bit-vector sort of size 32:" << std::endl;
 63  std::cout << "---------------------------------" << std::endl;
 64  std::cout << "operator<<: " << bv32 << std::endl;
 65  std::cout << "str():      " << bv32.str() << std::endl << std::endl;
 66
 67  // Print terms.
 68  // Note: Hexadecimal bv output format is ignored if the value is not of size
 69  //       divisible by 4.
 70  std::cout << "Print term:" << std::endl;
 71  std::cout << "-----------" << std::endl;
 72  std::cout << "operator<<:                 " << rm << std::endl;
 73  std::cout << "operator<< [dec (ignored)]: " << set_bv_format(10) << rm
 74            << std::endl;
 75  std::cout << "str()      [bin]:           " << rm.str() << std::endl;
 76  std::cout << "str(16)    [hex (ignored)]: " << rm.str(16) << std::endl
 77            << std::endl;
 78  std::cout << "operator<< [bin]: " << set_bv_format(2) << zero << std::endl;
 79  std::cout << "operator<< [dec]: " << set_bv_format(10) << zero << std::endl;
 80  std::cout << "operator<< [hex]: " << set_bv_format(16) << zero << std::endl;
 81  std::cout << "str()      [bin]: " << zero.str() << std::endl;
 82  std::cout << "str(10)    [dec]: " << zero.str(10) << std::endl;
 83  std::cout << "str(16)    [hex]: " << zero.str(16) << std::endl << std::endl;
 84  std::cout << "operator<< [bin]:           " << set_bv_format(2) << fpleq
 85            << std::endl;
 86  std::cout << "operator<< [dec]:           " << set_bv_format(10) << fpleq
 87            << std::endl;
 88  std::cout << "operator<< [hex (ignored)]: " << set_bv_format(16) << fpleq
 89            << std::endl;
 90  std::cout << "str()      [bin]:           " << fpleq.str() << std::endl;
 91  std::cout << "str(10)    [dec]:           " << fpleq.str(10) << std::endl;
 92  std::cout << "str(16)    [hex (ignored)]: " << fpleq.str(16) << std::endl
 93            << std::endl;
 94
 95  // Print asserted formulas.
 96  // Note: This uses the default bit-vector output format (binary).
 97  {
 98    std::stringstream expected_smt2;
 99    expected_smt2
100        << "(set-logic UFBVFP)" << std::endl
101        << "(declare-const b Bool)" << std::endl
102        << "(declare-const bv (_ BitVec 8))" << std::endl
103        << "(declare-const fp (_ FloatingPoint 5 11))" << std::endl
104        << "(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) (_ BitVec "
105           "32)) (_ FloatingPoint 5 11))"
106        << std::endl
107        << "(assert b)" << std::endl
108        << "(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) "
109           "#b00000000))"
110        << std::endl
111        << "(assert (exists ((q (_ BitVec 8))) (= #b00000000 (bvmul bv q))))"
112        << std::endl
113        << "(assert (fp.leq (fun bv fp ((_ zero_extend 9) "
114           "#b11111111111111111111111)) fp))"
115        << std::endl
116        << "(check-sat)" << std::endl
117        << "(exit)" << std::endl;
118    std::stringstream ss;
119    bitwuzla.print_formula(ss, "smt2");
120    assert(ss.str() == expected_smt2.str());
121    std::cout << "Print formula [default (binary) bv output format]:"
122              << std::endl;
123    std::cout << "--------------------------------------------------"
124              << std::endl;
125    std::cout << ss.str() << std::endl;
126  }
127
128  // Print asserted formulas using hexadecimal bit-vector output format.
129  {
130    std::stringstream expected_smt2;
131    expected_smt2
132        << "(set-logic UFBVFP)" << std::endl
133        << "(declare-const b Bool)" << std::endl
134        << "(declare-const bv (_ BitVec 8))" << std::endl
135        << "(declare-const fp (_ FloatingPoint 5 11))" << std::endl
136        << "(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) (_ BitVec "
137           "32)) (_ FloatingPoint 5 11))"
138        << std::endl
139        << "(assert b)" << std::endl
140        << "(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) "
141           "#x00))"
142        << std::endl
143        << "(assert (exists ((q (_ BitVec 8))) (= #x00 (bvmul bv q))))"
144        << std::endl
145        << "(assert (fp.leq (fun bv fp ((_ zero_extend 9) "
146           "#b11111111111111111111111)) fp))"
147        << std::endl
148        << "(check-sat)" << std::endl
149        << "(exit)" << std::endl;
150    std::stringstream ss;
151    // configure output stream with hexadecimal bv output format
152    ss << set_bv_format(16);
153    bitwuzla.print_formula(ss, "smt2");
154    assert(ss.str() == expected_smt2.str());
155    std::cout << "Print formula [hexadecimal bv output format]:" << std::endl;
156    std::cout << "---------------------------------------------" << std::endl;
157    std::cout << ss.str() << std::endl;
158  }
159
160  // Print asserted formulas using decimal bit-vector output format.
161  {
162    std::stringstream expected_smt2;
163    expected_smt2
164        << "(set-logic UFBVFP)" << std::endl
165        << "(declare-const b Bool)" << std::endl
166        << "(declare-const bv (_ BitVec 8))" << std::endl
167        << "(declare-const fp (_ FloatingPoint 5 11))" << std::endl
168        << "(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) (_ BitVec "
169           "32)) (_ FloatingPoint 5 11))"
170        << std::endl
171        << "(assert b)" << std::endl
172        << "(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) "
173           "(_ bv0 8)))"
174        << std::endl
175        << "(assert (exists ((q (_ BitVec 8))) (= (_ bv0 8) (bvmul bv q))))"
176        << std::endl
177        << "(assert (fp.leq (fun bv fp ((_ zero_extend 9) "
178           "(_ bv8388607 23))) fp))"
179        << std::endl
180        << "(check-sat)" << std::endl
181        << "(exit)" << std::endl;
182    std::stringstream ss;
183    // configure output stream with decimal bv output format
184    ss << set_bv_format(10);
185    bitwuzla.print_formula(ss, "smt2");
186    assert(ss.str() == expected_smt2.str());
187    std::cout << "Print formula [decimal bv output format]:" << std::endl;
188    std::cout << "---------------------------------------------" << std::endl;
189    std::cout << ss.str() << std::endl;
190  }
191
192  bitwuzla.check_sat();
193
194  // Print values.
195  std::cout << "Print value of Boolean predicate:" << std::endl
196            << "---------------------------------" << std::endl;
197  bool fpleq_val            = bitwuzla.get_value(fpleq).value<bool>();
198  std::string fpleq_val_str = bitwuzla.get_value(fpleq).value<std::string>();
199  std::cout << fpleq << ": " << std::setw(4) << fpleq_val << " [bool]"
200            << std::endl
201            << fpleq << ": " << std::setw(4) << fpleq_val_str
202            << " [std::string]" << std::endl
203            << std::endl;
204
205  std::cout << "Print value of bv const:" << std::endl
206            << "------------------------" << std::endl;
207  std::cout << bv << ": " << std::setw(8)
208            << bitwuzla.get_value(bv).value<std::string>()
209            << " [std::string] (bin)" << std::endl;
210  std::cout << bv << ": " << std::setw(8)
211            << bitwuzla.get_value(bv).value<std::string>(10)
212            << " [std::string] (dec)" << std::endl;
213  std::cout << bv << ": " << std::setw(8)
214            << bitwuzla.get_value(bv).value<std::string>(16)
215            << " [std::string] (dec)" << std::endl
216            << std::endl;
217
218  std::cout << "Print value of RoundingMode const:" << std::endl
219            << "----------------------------------" << std::endl;
220  RoundingMode rm_val    = bitwuzla.get_value(rm).value<RoundingMode>();
221  std::string rm_val_str = bitwuzla.get_value(rm).value<std::string>();
222  std::cout << rm << ": " << rm_val << " [RoundingMode]" << std::endl
223            << rm << ": " << rm_val_str << " [std::string]" << std::endl
224            << std::endl;
225
226  Term fp_val = bitwuzla.get_value(fp);
227
228  std::cout << "Print value of fp const as std::string (base ignored):"
229            << std::endl
230            << "------------------------------------------------------"
231            << std::endl;
232  assert(fp_val.value<std::string>() == fp_val.value<std::string>(10));
233  assert(fp_val.value<std::string>() == fp_val.value<std::string>(16));
234  std::cout << fp << ": " << std::setw(16) << fp_val.value<std::string>()
235            << " [std::string] (bin)" << std::endl;
236  std::cout << fp << ": " << std::setw(16) << fp_val.value<std::string>(10)
237            << " [std::string] (dec [ignored])" << std::endl;
238  std::cout << fp << ": " << std::setw(16) << fp_val.value<std::string>(16)
239            << " [std::string] (hex [ignored])" << std::endl
240            << std::endl;
241
242  std::cout << "Print value of fp const as tuple of std::string:" << std::endl
243            << "------------------------------------------------" << std::endl;
244  auto fp_val_tup =
245      fp_val.value<std::tuple<std::string, std::string, std::string>>();
246  std::cout << fp << ": (" << std::get<0>(fp_val_tup) << ", " << std::setw(5)
247            << std::get<1>(fp_val_tup) << ", " << std::setw(11)
248            << std::get<2>(fp_val_tup) << ")"
249            << " [std::tuple<std::string, std::string, std::string>] (bin)"
250            << std::endl;
251  fp_val_tup =
252      fp_val.value<std::tuple<std::string, std::string, std::string>>(10);
253  std::cout << fp << ": (" << std::get<0>(fp_val_tup) << ", " << std::setw(5)
254            << std::get<1>(fp_val_tup) << ", " << std::setw(11)
255            << std::get<2>(fp_val_tup) << ")"
256            << " [std::tuple<std::string, std::string, std::string>] (dec)"
257            << std::endl;
258  fp_val_tup =
259      fp_val.value<std::tuple<std::string, std::string, std::string>>(16);
260  std::cout << fp << ": (" << std::get<0>(fp_val_tup) << ", " << std::setw(5)
261            << std::get<1>(fp_val_tup) << ", " << std::setw(11)
262            << std::get<2>(fp_val_tup) << ")"
263            << " [std::tuple<std::string, std::string, std::string>] (hex)"
264            << std::endl;
265
266  return 0;
267}

Termination Callback Example

This example shows how to configure a termination callback.
The source code for this example can be found at examples/cpp/terminator.cpp.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2023 by the authors listed in the AUTHORS file at
 5 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 6 *
 7 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 8 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 9 */
10
11#include <bitwuzla/cpp/bitwuzla.h>
12
13#include <chrono>
14#include <iostream>
15
16using namespace bitwuzla;
17using namespace std::chrono;
18
19class TestTerminator : public Terminator
20{
21 public:
22  TestTerminator(uint32_t time_limit_ms)
23      : Terminator(),
24        time_limit_ms(time_limit_ms),
25        start(high_resolution_clock::now())
26  {
27  }
28  bool terminate() override
29  {
30    if (duration_cast<milliseconds>(high_resolution_clock::now() - start)
31            .count()
32        >= time_limit_ms)
33    {
34      return true;
35    }
36    return false;
37  }
38  uint32_t time_limit_ms = 0;
39  high_resolution_clock::time_point start;
40};
41
42int
43main()
44{
45  // First, create a term manager instance.
46  TermManager tm;
47  // Create a Bitwuzla options instance.
48  Options options;
49  // Then, create a Bitwuzla instance.
50  Bitwuzla bitwuzla(tm, options);
51
52  Sort bv = tm.mk_bv_sort(32);
53
54  Term x = tm.mk_const(bv);
55  Term s = tm.mk_const(bv);
56  Term t = tm.mk_const(bv);
57
58  Term a = tm.mk_term(
59      Kind::DISTINCT,
60      {tm.mk_term(Kind::BV_MUL, {s, tm.mk_term(Kind::BV_MUL, {x, t})}),
61       tm.mk_term(Kind::BV_MUL, {tm.mk_term(Kind::BV_MUL, {s, x}), t})});
62
63  // Now, we check that the following formula is unsat.
64  // (assert (distinct (bvmul s (bvmul x t)) (bvmul (bvmul s x) t)))
65  std::cout << "> Without terminator (with preprocessing):" << std::endl;
66  std::cout << "Expect: unsat" << std::endl;
67  std::cout << "Result: " << bitwuzla.check_sat({a}) << std::endl;
68
69  // Now, for illustration purposes, we disable preprocessing, which will
70  // significantly increase solving time, and connect a terminator instance
71  // that terminates after a certain time limit.
72  options.set(Option::PREPROCESS, false);
73  // Create new Bitwuzla instance with reconfigured options.
74  Bitwuzla bitwuzla2(tm, options);
75  // Configure and connect terminator.
76  TestTerminator tt(1000);
77  bitwuzla2.configure_terminator(&tt);
78
79  // Now, we expect Bitwuzla to be terminated during the check-sat call.
80  std::cout << "> With terminator (no preprocessing):" << std::endl;
81  std::cout << "Expect: unknown" << std::endl;
82  std::cout << "Result: " << bitwuzla2.check_sat({a}) << std::endl;
83
84  return 0;
85}