C API Documentation

The C API of Bitwuzla is implemented as a thin wrapper around its C++ API, Bitwuzla’s 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 BitwuzlaTermManager instance that allows us to create sorts and terms later:

  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();

Then, create a BitwuzlaOptions instance:

  BitwuzlaOptions *options = bitwuzla_options_new();

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

  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);

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):

  bitwuzla_set_option_mode(options, BITWUZLA_OPT_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 = bitwuzla_new(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.
  BitwuzlaSort sortbv4 = bitwuzla_mk_bv_sort(tm, 4);
  BitwuzlaSort sortbv8 = bitwuzla_mk_bv_sort(tm, 8);
  // Create function sort.
  BitwuzlaSort domain[2] = {sortbv8, sortbv4};
  BitwuzlaSort sortfun   = bitwuzla_mk_fun_sort(tm, 2, domain, sortbv8);
  // Create array sort.
  BitwuzlaSort sortarr = bitwuzla_mk_array_sort(tm, sortbv8, sortbv8);

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

  // (bvsdiv x (_ bv2 8))
  BitwuzlaTerm sdiv = bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SDIV, x, two);
  // (bvashr y (_ bv1 8))
  BitwuzlaTerm ashr = bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ASHR, y, one);
  // ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
  BitwuzlaTerm sdive =
      bitwuzla_mk_term1_indexed2(tm, BITWUZLA_KIND_BV_EXTRACT, sdiv, 3, 0);
  // ((_ extract 3 0) (bvashr x (_ bv1 8)))
  BitwuzlaTerm ashre =
      bitwuzla_mk_term1_indexed2(tm, BITWUZLA_KIND_BV_EXTRACT, ashr, 3, 0);

  // (assert
  //     (distinct
  //         ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
  //         ((_ extract 3 0) (bvashr y (_ bv1 8)))))
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_DISTINCT, sdive, ashre));
  // (assert (= (f x ((_ extract 6 3) x)) y))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(
          tm,
          BITWUZLA_KIND_EQUAL,
          bitwuzla_mk_term3(tm,
                            BITWUZLA_KIND_APPLY,
                            f,
                            x,
                            bitwuzla_mk_term1_indexed2(
                                tm, BITWUZLA_KIND_BV_EXTRACT, x, 6, 3)),
          y));
  // (assert (= (select a x) y))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        bitwuzla_mk_term2(tm, BITWUZLA_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 via bitwuzla_parser_new() and then parsing the input file via bitwuzla_parser_parse().

Note

The input parser creates a Bitwuzla instance, which can be configured via the BitwuzlaOptions instance passed into the parser. This Bitwuzla instance can be retrieved via bitwuzla_parser_get_bitwuzla().

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

  // First, create a term manager instance.
  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();

  // We will parse example file `smt2/quickstart.smt2`.
  // Create parser instance.
  const char* infile_name = "../smt2/quickstart.smt2";
  BitwuzlaParser* parser =
      bitwuzla_parser_new(tm, options, "smt2", 2, "<stdout>");
  const char* error_msg;
  printf("Expect: sat\n");
  printf("Bitwuzla: ");
  bitwuzla_parser_parse(parser, infile_name, false, true, &error_msg);
  // We expect no error to occur.
  assert(!error_msg);

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_parse() as true.

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

  // Now we retrieve the set of asserted formulas and print them.
  size_t size;
  const BitwuzlaTerm* assertions =
      bitwuzla_get_assertions(bitwuzla_parser_get_bitwuzla(parser), &size);
  printf("Assertions:\n");
  printf("{\n");
  for (size_t i = 0; i < size; ++i)
  {
    printf("  %s\n", bitwuzla_term_to_string(assertions[i]));
  }
  printf("}\n");

Alternatively, Bitwuzla also supports parsing from strings via bitwuzla_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:

  bitwuzla_parser_parse(
      parser, "(assert (distinct (select a x) y))", true, false, &error_msg);
  // We expect no error to occur.
  assert(!error_msg);

Bitwuzla also supports parsing terms and sorts from strings via bitwuzla_parser_parse_term() and bitwuzla_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_parse(). Function bitwuzla_parser_parse_term() and bitwuzla_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.
  BitwuzlaSort bv16 =
      bitwuzla_parser_parse_sort(parser, "(_ BitVec 16)", &error_msg);
  // We expect no error to occur.
  assert(!error_msg);
  // Create bit-vector sort of size 16 and show that it corresponds to
  // its string representation '(_ BitVec16)'.
  assert(bv16 == bitwuzla_mk_bv_sort(tm, 16));

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

  bitwuzla_parser_parse(parser,
                        "(declare-const c Bool)(declare-const d Bool)",
                        true,
                        false,
                        &error_msg);
  // Declare bit-vector constant 'b'.
  bitwuzla_parser_parse(
      parser, "(declare-const b (_ BitVec 16))", true, false, &error_msg);
  // We expect no error to occur.
  assert(!error_msg);

These terms can be retrieved via bitwuzla_parser_parse_term():

  // Retrieve term representing 'b'.
  BitwuzlaTerm b = bitwuzla_parser_parse_term(parser, "b", &error_msg);
  // We expect no error to occur.
  assert(!error_msg);
  // Retrieve term representing 'c'.
  BitwuzlaTerm c = bitwuzla_parser_parse_term(parser, "c", &error_msg);
  // We expect no error to occur.
  assert(!error_msg);
  // Retrieve term representing 'd'.
  BitwuzlaTerm d = bitwuzla_parser_parse_term(parser, "d", &error_msg);
  // We expect no error to occur.
  assert(!error_msg);

Now, to parse in terms using these constants via bitwuzla_parser_parse_term():

  // Create xor over 'a' and 'c' and show that it corresponds to term
  // parsed in from its string representation '(xor c d)'.
  assert(bitwuzla_parser_parse_term(parser, "(xor c d)", &error_msg)
         == bitwuzla_mk_term2(tm, BITWUZLA_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(bitwuzla_parser_parse_term(
             parser, "(bvadd b #b1011111010001010)", &error_msg)
         == bitwuzla_mk_term2(
             tm,
             BITWUZLA_KIND_BV_ADD,
             b,

After parsing input and asserting formulas, satisfiability can be determined via bitwuzla_check_sat().

  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);

Formulas can also be assumed via bitwuzla_check_sat_assuming().

If the formula is satisfiable and model generation has been enabled, the resulting model can be printed via bitwuzla_get_value() and bitwuzla_term_to_string(). An example implementation illustrating how to print the current model via declared symbols (in this case x, y, f and a) is below:

  printf("Model:\n");
  BitwuzlaTerm decls[4] = {x, y, f, a};
  printf("(\n");
  for (uint32_t i = 0; i < 4; ++i)
  {
    BitwuzlaSort sort = bitwuzla_term_get_sort(decls[i]);
    printf("  (define-fun %s (", bitwuzla_term_get_symbol(decls[i]));
    if (bitwuzla_sort_is_fun(sort))
    {
      BitwuzlaTerm value = bitwuzla_get_value(bitwuzla, decls[i]);
      size_t size;
      BitwuzlaTerm *children = bitwuzla_term_get_children(value, &size);
      assert(size == 2);
      while (bitwuzla_term_get_kind(children[1]) == BITWUZLA_KIND_LAMBDA)
      {
        assert(bitwuzla_term_is_var(children[0]));
        printf("(%s %s) ",
               bitwuzla_term_to_string(children[0]),
               bitwuzla_sort_to_string(bitwuzla_term_get_sort(children[0])));
        value    = children[1];
        children = bitwuzla_term_get_children(value, &size);
      }
      assert(bitwuzla_term_is_var(children[0]));
      // Note: The returned string of bitwuzla_term_to_string and
      //       bitwuzla_sort_to_string does not have to be freed, but is only
      //       valid until the next call to the respective function. Thus we
      //       split printing into separate printf calls so that none of these
      //       functions is called more than once in one printf call.
      //       Alternatively, we could also first get and copy the strings, use
      //       a single printf call, and then free the copied strings.
      printf("(%s %s))",
             bitwuzla_term_to_string(children[0]),
             bitwuzla_sort_to_string(bitwuzla_term_get_sort(children[0])));
      printf(" %s",
             bitwuzla_sort_to_string(bitwuzla_sort_fun_get_codomain(sort)));
      printf(" %s)\n", bitwuzla_term_to_string(children[1]));
    }
    else
    {
      printf(") %s %s)\n",
             bitwuzla_sort_to_string(sort),
             bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, decls[i])));
    }
  }
  printf(")\n");
  printf("\n");

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_get_str(), or as a term via bitwuzla_get_value().

Additionally, for floating-point values, bitwuzla_term_value_get_fp_ieee() allows to retrieve the assignment split into assignment strings for the sign bit, the exponent and the significand. For Boolean and RoundingMode values, bitwuzla_term_value_get_bool() and bitwuzla_term_value_get_rm() allow the values as bool and BitwuzlaRoundingMode, respectively.

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 bitwuzla_term_value_get_str().
  printf("value of x: %s\n",
         bitwuzla_term_value_get_str(bitwuzla_get_value(bitwuzla, x)));
  printf("value of y: %s\n",
         bitwuzla_term_value_get_str(bitwuzla_get_value(bitwuzla, y)));
  printf("\n");

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_to_string():

  // 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
  // bitwuzla_term_value_get_str(), but we can print the value of the terms
  // via bitwuzla_term_to_string().
  printf("to_string representation of value of f:\n%s\n\n",
         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, f)));
  printf("to_string representation of value of a:\n%s\n",
         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, a)));
  printf("\n");

This will print:

to_string 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)))

to_string 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_get_str(). Their string representation retrieved via bitwuzla_term_to_string(), however, is given in SMT-LIB2 format. For example,

  printf("to_string representation of value of x: %s\n",
         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, x)));
  printf("to_string representation of value of y: %s\n",
         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, y)));
  printf("\n");

This will print:

to_string representation of value of x: #b10011111
to_string 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:

  BitwuzlaTerm v = bitwuzla_get_value(
      bitwuzla, bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, x, x));
  printf("value of v = x * x: %s\n",
         bitwuzla_term_value_get_str(bitwuzla_get_value(bitwuzla, v)));

This will print:

value of v = x * x: 11000001

Finally, we delete the Bitwuzla, BitwuzlaOptions, and BitwuzlaTermManager instances.

  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

Note

Make sure to delete the term manager last since the solver instance relies on it. Further, when the term manager is deleted, it will automatically release all created sorts and terms. For a more fine-grained control on when sorts and terms are released you can use bitwuzla_sort_copy(), bitwuzla_sort_release(), bitwuzla_term_copy(), bitwuzla_term_release(), and bitwuzla_term_manager_release().

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/c/quickstart.c.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2021 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/c/bitwuzla.h>
 13#include <stdio.h>
 14
 15int
 16main()
 17{
 18  // First, create a term manager instance.
 19  //! [docs-c-quickstart-0 start]
 20  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();
 21  //! [docs-c-quickstart-0 end]
 22  // Create a Bitwuzla options instance.
 23  //! [docs-c-quickstart-1 start]
 24  BitwuzlaOptions *options = bitwuzla_options_new();
 25  //! [docs-c-quickstart-1 end]
 26  // Then, enable model generation.
 27  //! [docs-c-quickstart-2 start]
 28  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
 29  //! [docs-c-quickstart-2 end]
 30  // Now, for illustration purposes, we enable CaDiCaL as SAT solver
 31  // (CaDiCaL is already configured by default).
 32  // Note: This will silently fall back to one of the compiled in SAT solvers
 33  //       if the selected solver is not compiled in.
 34  //! [docs-c-quickstart-3 start]
 35  bitwuzla_set_option_mode(options, BITWUZLA_OPT_SAT_SOLVER, "cadical");
 36  //! [docs-c-quickstart-3 end]
 37  // Then, create a Bitwuzla instance.
 38  //! [docs-c-quickstart-4 start]
 39  Bitwuzla *bitwuzla = bitwuzla_new(tm, options);
 40  //! [docs-c-quickstart-4 end]
 41
 42  //! [docs-c-quickstart-5 start]
 43  // Create bit-vector sorts of size 4 and 8.
 44  BitwuzlaSort sortbv4 = bitwuzla_mk_bv_sort(tm, 4);
 45  BitwuzlaSort sortbv8 = bitwuzla_mk_bv_sort(tm, 8);
 46  // Create function sort.
 47  BitwuzlaSort domain[2] = {sortbv8, sortbv4};
 48  BitwuzlaSort sortfun   = bitwuzla_mk_fun_sort(tm, 2, domain, sortbv8);
 49  // Create array sort.
 50  BitwuzlaSort sortarr = bitwuzla_mk_array_sort(tm, sortbv8, sortbv8);
 51
 52  // Create two bit-vector constants of that sort.
 53  BitwuzlaTerm x = bitwuzla_mk_const(tm, sortbv8, "x");
 54  BitwuzlaTerm y = bitwuzla_mk_const(tm, sortbv8, "y");
 55  // Create fun const.
 56  BitwuzlaTerm f = bitwuzla_mk_const(tm, sortfun, "f");
 57  // Create array const.
 58  BitwuzlaTerm a = bitwuzla_mk_const(tm, sortarr, "a");
 59  // Create bit-vector values one and two of the same sort.
 60  BitwuzlaTerm one = bitwuzla_mk_bv_one(tm, sortbv8);
 61  // Alternatively, you can create bit-vector value one with:
 62  // BitwuzlaTerm one = bitwuzla_mk_bv_value(tm, sortbv8, "1", 2);
 63  // BitwuzlaTerm one = bitwuzla_mk_bv_value_uint64(tm, sortbv8, 1);
 64  BitwuzlaTerm two = bitwuzla_mk_bv_value_uint64(tm, sortbv8, 2);
 65
 66  // (bvsdiv x (_ bv2 8))
 67  BitwuzlaTerm sdiv = bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_SDIV, x, two);
 68  // (bvashr y (_ bv1 8))
 69  BitwuzlaTerm ashr = bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ASHR, y, one);
 70  // ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
 71  BitwuzlaTerm sdive =
 72      bitwuzla_mk_term1_indexed2(tm, BITWUZLA_KIND_BV_EXTRACT, sdiv, 3, 0);
 73  // ((_ extract 3 0) (bvashr x (_ bv1 8)))
 74  BitwuzlaTerm ashre =
 75      bitwuzla_mk_term1_indexed2(tm, BITWUZLA_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(bitwuzla,
 82                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_DISTINCT, sdive, ashre));
 83  // (assert (= (f x ((_ extract 6 3) x)) y))
 84  bitwuzla_assert(
 85      bitwuzla,
 86      bitwuzla_mk_term2(
 87          tm,
 88          BITWUZLA_KIND_EQUAL,
 89          bitwuzla_mk_term3(tm,
 90                            BITWUZLA_KIND_APPLY,
 91                            f,
 92                            x,
 93                            bitwuzla_mk_term1_indexed2(
 94                                tm, BITWUZLA_KIND_BV_EXTRACT, x, 6, 3)),
 95          y));
 96  // (assert (= (select a x) y))
 97  bitwuzla_assert(
 98      bitwuzla,
 99      bitwuzla_mk_term2(tm,
100                        BITWUZLA_KIND_EQUAL,
101                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_ARRAY_SELECT, a, x),
102                        y));
103  //! [docs-c-quickstart-5 end]
104
105  // (check-sat)
106  //! [docs-c-quickstart-6 start]
107  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
108  //! [docs-c-quickstart-6 end]
109
110  printf("Expect: sat\n");
111  printf("Bitwuzla: %s\n\n", bitwuzla_result_to_string(result));
112
113  // Print model in SMT-LIBv2 format.
114  //! [docs-c-quickstart-7 start]
115  printf("Model:\n");
116  BitwuzlaTerm decls[4] = {x, y, f, a};
117  printf("(\n");
118  for (uint32_t i = 0; i < 4; ++i)
119  {
120    BitwuzlaSort sort = bitwuzla_term_get_sort(decls[i]);
121    printf("  (define-fun %s (", bitwuzla_term_get_symbol(decls[i]));
122    if (bitwuzla_sort_is_fun(sort))
123    {
124      BitwuzlaTerm value = bitwuzla_get_value(bitwuzla, decls[i]);
125      size_t size;
126      BitwuzlaTerm *children = bitwuzla_term_get_children(value, &size);
127      assert(size == 2);
128      while (bitwuzla_term_get_kind(children[1]) == BITWUZLA_KIND_LAMBDA)
129      {
130        assert(bitwuzla_term_is_var(children[0]));
131        printf("(%s %s) ",
132               bitwuzla_term_to_string(children[0]),
133               bitwuzla_sort_to_string(bitwuzla_term_get_sort(children[0])));
134        value    = children[1];
135        children = bitwuzla_term_get_children(value, &size);
136      }
137      assert(bitwuzla_term_is_var(children[0]));
138      // Note: The returned string of bitwuzla_term_to_string and
139      //       bitwuzla_sort_to_string does not have to be freed, but is only
140      //       valid until the next call to the respective function. Thus we
141      //       split printing into separate printf calls so that none of these
142      //       functions is called more than once in one printf call.
143      //       Alternatively, we could also first get and copy the strings, use
144      //       a single printf call, and then free the copied strings.
145      printf("(%s %s))",
146             bitwuzla_term_to_string(children[0]),
147             bitwuzla_sort_to_string(bitwuzla_term_get_sort(children[0])));
148      printf(" %s",
149             bitwuzla_sort_to_string(bitwuzla_sort_fun_get_codomain(sort)));
150      printf(" %s)\n", bitwuzla_term_to_string(children[1]));
151    }
152    else
153    {
154      printf(") %s %s)\n",
155             bitwuzla_sort_to_string(sort),
156             bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, decls[i])));
157    }
158  }
159  printf(")\n");
160  printf("\n");
161  //! [docs-c-quickstart-7 end]
162
163  // Print value for x, y, f and a.
164  // Note: The returned string of bitwuzla_term_value_get_str is only valid
165  //       until the next call to bitwuzla_term_value_get_str
166  //! [docs-c-quickstart-8 start]
167  // Both x and y are bit-vector terms and their value is a bit-vector
168  // value that can be printed via bitwuzla_term_value_get_str().
169  printf("value of x: %s\n",
170         bitwuzla_term_value_get_str(bitwuzla_get_value(bitwuzla, x)));
171  printf("value of y: %s\n",
172         bitwuzla_term_value_get_str(bitwuzla_get_value(bitwuzla, y)));
173  printf("\n");
174  //! [docs-c-quickstart-8 end]
175  //! [docs-c-quickstart-9 start]
176  // f and a, on the other hand, are a function and array term, respectively.
177  // The value of these terms is not a value term: for f, it is a lambda term,
178  // and the value of a is represented as a store term. Thus we cannot use
179  // bitwuzla_term_value_get_str(), but we can print the value of the terms
180  // via bitwuzla_term_to_string().
181  printf("to_string representation of value of f:\n%s\n\n",
182         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, f)));
183  printf("to_string representation of value of a:\n%s\n",
184         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, a)));
185  printf("\n");
186  //! [docs-c-quickstart-9 end]
187  // Note that the assignment string of bit-vector terms is given as the
188  // pure assignment string, either in binary, hexadecimal or decimal format,
189  // whereas bitwuzla_term_to_string() prints the value in SMT-LIB2 format
190  // (in binary number format).
191  //! [docs-c-quickstart-10 start]
192  printf("to_string representation of value of x: %s\n",
193         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, x)));
194  printf("to_string representation of value of y: %s\n",
195         bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, y)));
196  printf("\n");
197  //! [docs-c-quickstart-10 end]
198
199  // Query value of bit-vector term that does not occur in the input formula
200  //! [docs-c-quickstart-11 start]
201  BitwuzlaTerm v = bitwuzla_get_value(
202      bitwuzla, bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, x, x));
203  printf("value of v = x * x: %s\n",
204         bitwuzla_term_value_get_str(bitwuzla_get_value(bitwuzla, v)));
205  //! [docs-c-quickstart-11 end]
206
207  // Finally, delete the Bitwuzla solver, options, and term manager instances.
208  //! [docs-c-quickstart-12 start]
209  bitwuzla_delete(bitwuzla);
210  bitwuzla_options_delete(options);
211  bitwuzla_term_manager_delete(tm);
212  //! [docs-c-quickstart-12 end]
213
214  return 0;
215}

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/c/options.c.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2021 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/c/bitwuzla.h>
12#include <inttypes.h>
13#include <stdio.h>
14
15int
16main()
17{
18  // First, create a term manager instance.
19  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
20  // Create a Bitwuzla options instance.
21  BitwuzlaOptions* options = bitwuzla_options_new();
22
23  // Enable model generation, which expects a boolean configuration value.
24  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
25
26  // Increase the verbosity level, which expects an integer value.
27  printf("Previous verbosity level: %" PRIu64 "\n",
28         bitwuzla_get_option(options, BITWUZLA_OPT_VERBOSITY));
29  bitwuzla_set_option(options, BITWUZLA_OPT_VERBOSITY, 2);
30  printf("Current verbosity level: %" PRIu64 "\n",
31         bitwuzla_get_option(options, BITWUZLA_OPT_VERBOSITY));
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  printf("Default bv solver: %s\n",
36         bitwuzla_get_option_mode(options, BITWUZLA_OPT_BV_SOLVER));
37  // Then, select the propagation-based local search engine as solver engine.
38  bitwuzla_set_option_mode(options, BITWUZLA_OPT_BV_SOLVER, "prop");
39  printf("Current engine: %s\n",
40         bitwuzla_get_option_mode(options, BITWUZLA_OPT_BV_SOLVER));
41
42  // Now, create a Bitwuzla instance.
43  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
44  // Check sat (nothing to solve, input formula is empty).
45  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
46  printf("Expect: sat\n");
47  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
48
49  // Finally, delete the Bitwuzla solver, options, and term manager instances.
50  bitwuzla_delete(bitwuzla);
51  bitwuzla_options_delete(options);
52  bitwuzla_term_manager_delete(tm);
53
54  return 0;
55}

Option Info Example

An example for how to get information about options via BitwuzlaOptionInfo.
The source code for this example can be found at examples/c/option_info.c.
 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/c/bitwuzla.h>
12#include <inttypes.h>
13#include <stdio.h>
14
15int
16main()
17{
18  // First, create a Bitwuzla options instance.
19  BitwuzlaOptions* options = bitwuzla_options_new();
20  // Set some options to illustrate current vs default value.
21  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
22  bitwuzla_set_option(options, BITWUZLA_OPT_VERBOSITY, 2);
23  bitwuzla_set_option_mode(options, BITWUZLA_OPT_BV_SOLVER, "prop");
24
25  // Then iterate over all available configuration options and extract info.
26  BitwuzlaOptionInfo info;
27  for (uint32_t i = 0; i < BITWUZLA_OPT_NUM_OPTS; ++i)
28  {
29    BitwuzlaOption opt = (BitwuzlaOption) i;
30    bitwuzla_get_option_info(options, opt, &info);
31    printf("- long name:   %s\n", info.lng);
32    printf("  short name:  %s\n", (info.shrt ? info.shrt : "-"));
33    printf("  kind:        ");
34    if (info.is_numeric)
35    {
36      printf("numeric\n");
37      printf("  values:\n");
38      printf("  + current:   %" PRIu64 "\n", info.numeric.cur);
39      printf("  + default:   %" PRIu64 "\n", info.numeric.dflt);
40      printf("  + min:       %" PRIu64 "\n", info.numeric.min);
41      printf("  + max:       %" PRIu64 "\n", info.numeric.max);
42    }
43    else
44    {
45      printf("modes\n");
46      printf("  values:\n");
47      printf("  + current:   %s\n", info.mode.cur);
48      printf("  + default:   %s\n", info.mode.dflt);
49      printf("  + modes:     {");
50      for (size_t i = 0, n = info.mode.num_modes; i < n; ++i)
51      {
52        printf("%s %s", (i > 0 ? "," : ""), info.mode.modes[i]);
53      }
54      printf(" }\n");
55    }
56    printf("  description: %s\n\n", info.description);
57  }
58
59  // Finally, delete options instance.
60  bitwuzla_options_delete(options);
61}

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/c/pushpop.c.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2021 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/c/bitwuzla.h>
 12#include <stdio.h>
 13
 14int
 15main()
 16{
 17  // First, create a term manager instance.
 18  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
 19  // Create a Bitwuzla options instance.
 20  BitwuzlaOptions* options = bitwuzla_options_new();
 21  // Then, create a Bitwuzla instance.
 22  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
 23
 24  // Create a bit-vector sort of size 1.
 25  BitwuzlaSort sortbv1 = bitwuzla_mk_bv_sort(tm, 1);
 26  // Create a bit-vector sort of size 2.
 27  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
 28
 29  // Create bit-vector variables.
 30  // (declare-const o0 (_ BitVec 1))
 31  BitwuzlaTerm o0 = bitwuzla_mk_const(tm, sortbv1, "o0");
 32  // (declare-const o1 (_ BitVec 1))
 33  BitwuzlaTerm o1 = bitwuzla_mk_const(tm, sortbv1, "o1");
 34  // (declare-const s0 (_ BitVec 2))
 35  BitwuzlaTerm s0 = bitwuzla_mk_const(tm, sortbv2, "s0");
 36  // (declare-const s1 (_ BitVec 2))
 37  BitwuzlaTerm s1 = bitwuzla_mk_const(tm, sortbv2, "s1");
 38  // (declare-const s2 (_ BitVec 2))
 39  BitwuzlaTerm s2 = bitwuzla_mk_const(tm, sortbv2, "s2");
 40  // (declare-const goal (_ BitVec 2))
 41  BitwuzlaTerm goal = bitwuzla_mk_const(tm, sortbv2, "goal");
 42
 43  // Create bit-vector values zero, one, three.
 44  BitwuzlaTerm zero  = bitwuzla_mk_bv_zero(tm, sortbv2);
 45  BitwuzlaTerm one1  = bitwuzla_mk_bv_one(tm, sortbv1);
 46  BitwuzlaTerm one2  = bitwuzla_mk_bv_one(tm, sortbv2);
 47  BitwuzlaTerm three = bitwuzla_mk_bv_value_uint64(tm, sortbv2, 3);
 48
 49  // Add some assertions.
 50  bitwuzla_assert(bitwuzla,
 51                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, zero));
 52  bitwuzla_assert(bitwuzla,
 53                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, goal, three));
 54
 55  // Push, assert, check sat and pop.
 56  bitwuzla_push(bitwuzla, 1);
 57  bitwuzla_assert(bitwuzla,
 58                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, goal));
 59  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
 60  printf("Expect: unsat\n");
 61  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
 62  bitwuzla_pop(bitwuzla, 1);
 63
 64  // (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
 65  bitwuzla_assert(bitwuzla,
 66                  bitwuzla_mk_term2(
 67                      tm,
 68                      BITWUZLA_KIND_EQUAL,
 69                      s1,
 70                      bitwuzla_mk_term3(
 71                          tm,
 72                          BITWUZLA_KIND_ITE,
 73                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o0, one1),
 74                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s0, one2),
 75                          s0)));
 76
 77  // Push, assert, check sat and pop.
 78  bitwuzla_push(bitwuzla, 1);
 79  bitwuzla_assert(bitwuzla,
 80                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s1, goal));
 81  result = bitwuzla_check_sat(bitwuzla);
 82  printf("Expect: unsat\n");
 83  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
 84  bitwuzla_pop(bitwuzla, 1);
 85
 86  // (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
 87  bitwuzla_assert(bitwuzla,
 88                  bitwuzla_mk_term2(
 89                      tm,
 90                      BITWUZLA_KIND_EQUAL,
 91                      s2,
 92                      bitwuzla_mk_term3(
 93                          tm,
 94                          BITWUZLA_KIND_ITE,
 95                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o1, one1),
 96                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s1, one2),
 97                          s1)));
 98
 99  // Push, assert, check sat and pop.
100  bitwuzla_push(bitwuzla, 1);
101  bitwuzla_assert(bitwuzla,
102                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s2, goal));
103  result = bitwuzla_check_sat(bitwuzla);
104  printf("Expect: unsat\n");
105  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
106  bitwuzla_pop(bitwuzla, 1);
107
108  // Finally, delete the Bitwuzla solver, options, and term manager instances.
109  bitwuzla_delete(bitwuzla);
110  bitwuzla_options_delete(options);
111  bitwuzla_term_manager_delete(tm);
112
113  return 0;
114}

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/c/checksatassuming.c.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2021 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/c/bitwuzla.h>
 12#include <stdio.h>
 13
 14int
 15main()
 16{
 17  BitwuzlaResult result;
 18
 19  // First, create a term manager instance.
 20  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
 21  // Create a Bitwuzla options instance.
 22  BitwuzlaOptions* options = bitwuzla_options_new();
 23  // Then, create a Bitwuzla instance.
 24  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
 25
 26  // Create a bit-vector sort of size 1.
 27  BitwuzlaSort sortbv1 = bitwuzla_mk_bv_sort(tm, 1);
 28  // Create a bit-vector sort of size 2
 29  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
 30
 31  // Create bit-vector variables.
 32  // (declare-const o0 (_ BitVec 1))
 33  BitwuzlaTerm o0 = bitwuzla_mk_const(tm, sortbv1, "o0");
 34  // (declare-const o1 (_ BitVec 1))
 35  BitwuzlaTerm o1 = bitwuzla_mk_const(tm, sortbv1, "o1");
 36  // (declare-const s0 (_ BitVec 2))
 37  BitwuzlaTerm s0 = bitwuzla_mk_const(tm, sortbv2, "s0");
 38  // (declare-const s1 (_ BitVec 2))
 39  BitwuzlaTerm s1 = bitwuzla_mk_const(tm, sortbv2, "s1");
 40  // (declare-const s2 (_ BitVec 2))
 41  BitwuzlaTerm s2 = bitwuzla_mk_const(tm, sortbv2, "s2");
 42  // (declare-const goal (_ BitVec 2))
 43  BitwuzlaTerm goal = bitwuzla_mk_const(tm, sortbv2, "goal");
 44
 45  // Create bit-vector values zero, one, three.
 46  BitwuzlaTerm zero  = bitwuzla_mk_bv_zero(tm, sortbv2);
 47  BitwuzlaTerm one1  = bitwuzla_mk_bv_one(tm, sortbv1);
 48  BitwuzlaTerm one2  = bitwuzla_mk_bv_one(tm, sortbv2);
 49  BitwuzlaTerm three = bitwuzla_mk_bv_value_uint64(tm, sortbv2, 3);
 50
 51  // Add some assertions.
 52  bitwuzla_assert(bitwuzla,
 53                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, zero));
 54  bitwuzla_assert(bitwuzla,
 55                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, goal, three));
 56
 57  // (check-sat-assuming ((= s0 goal)))
 58  BitwuzlaTerm assumptions[1] = {
 59      bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, goal)};
 60  result = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
 61  printf("Expect: unsat\n");
 62  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
 63
 64  // (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
 65  bitwuzla_assert(bitwuzla,
 66                  bitwuzla_mk_term2(
 67                      tm,
 68                      BITWUZLA_KIND_EQUAL,
 69                      s1,
 70                      bitwuzla_mk_term3(
 71                          tm,
 72                          BITWUZLA_KIND_ITE,
 73                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o0, one1),
 74                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s0, one2),
 75                          s0)));
 76
 77  // (check-sat-assuming ((= s1 goal)))
 78  assumptions[0] = bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s1, goal);
 79  result         = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
 80  printf("Expect: unsat\n");
 81  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
 82
 83  // (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
 84  bitwuzla_assert(bitwuzla,
 85                  bitwuzla_mk_term2(
 86                      tm,
 87                      BITWUZLA_KIND_EQUAL,
 88                      s2,
 89                      bitwuzla_mk_term3(
 90                          tm,
 91                          BITWUZLA_KIND_ITE,
 92                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o1, one1),
 93                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s1, one2),
 94                          s1)));
 95
 96  // (check-sat-assuming ((= s2 goal)))
 97  assumptions[0] = bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s2, goal);
 98  result         = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
 99  printf("Expect: unsat\n");
100  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
101
102  // Finally, delete the Bitwuzla solver, options, and term manager instances.
103  bitwuzla_delete(bitwuzla);
104  bitwuzla_options_delete(options);
105  bitwuzla_term_manager_delete(tm);
106
107  return 0;
108}

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/c/unsatcore.c.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2021 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/c/bitwuzla.h>
 12#include <stdio.h>
 13
 14int
 15main()
 16{
 17  // First, create a term manager instance.
 18  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();
 19  // Create a Bitwuzla options instance.
 20  BitwuzlaOptions *options = bitwuzla_options_new();
 21  // Then, enable unsat core extraction.
 22  // Note: Unsat core extraction is disabled by default.
 23  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_UNSAT_CORES, 1);
 24  // Then, create a Bitwuzla instance.
 25  Bitwuzla *bitwuzla = bitwuzla_new(tm, options);
 26
 27  // Create a bit-vector sort of size 2.
 28  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
 29  // Create a bit-vector sort of size 4.
 30  BitwuzlaSort sortbv4 = bitwuzla_mk_bv_sort(tm, 4);
 31  // Create Float16 floatinf-point sort.
 32  BitwuzlaSort sortfp16 = bitwuzla_mk_fp_sort(tm, 5, 11);
 33
 34  // Create bit-vector variables.
 35  // (declare-const x0 (_ BitVec 4))
 36  BitwuzlaTerm x0 = bitwuzla_mk_const(tm, sortbv4, "x0");
 37  // (declare-const x1 (_ BitVec 2))
 38  BitwuzlaTerm x1 = bitwuzla_mk_const(tm, sortbv2, "x1");
 39  // (declare-const x2 (_ BitVec 2))
 40  BitwuzlaTerm x2 = bitwuzla_mk_const(tm, sortbv2, "x2");
 41  // (declare-const x3 (_ BitVec 2))
 42  BitwuzlaTerm x3 = bitwuzla_mk_const(tm, sortbv2, "x3");
 43  // (declare-const x4 Float16)
 44  BitwuzlaTerm x4 = bitwuzla_mk_const(tm, sortfp16, "x4");
 45
 46  // Create FP positive zero.
 47  BitwuzlaTerm fpzero = bitwuzla_mk_fp_pos_zero(tm, sortfp16);
 48  // Create BV zero of size 4.
 49  BitwuzlaTerm bvzero = bitwuzla_mk_bv_zero(tm, sortbv4);
 50
 51  // (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
 52  BitwuzlaTerm a_f0 = bitwuzla_mk_var(tm, sortfp16, "a_f0");
 53  BitwuzlaTerm f0   = bitwuzla_mk_term2(
 54      tm,
 55      BITWUZLA_KIND_LAMBDA,
 56      a_f0,
 57      bitwuzla_mk_term2(tm, BITWUZLA_KIND_FP_GT, a_f0, fpzero));
 58
 59  // (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
 60  BitwuzlaTerm a_f1 = bitwuzla_mk_var(tm, sortfp16, "a_f1");
 61  BitwuzlaTerm f1   = bitwuzla_mk_term2(
 62      tm,
 63      BITWUZLA_KIND_LAMBDA,
 64      a_f1,
 65      bitwuzla_mk_term3(tm,
 66                        BITWUZLA_KIND_ITE,
 67                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f0, a_f1),
 68                        x0,
 69                        bvzero));
 70
 71  // (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
 72  BitwuzlaTerm a_f2 = bitwuzla_mk_var(tm, sortfp16, "a_f2");
 73  BitwuzlaTerm f2   = bitwuzla_mk_term2(
 74      tm,
 75      BITWUZLA_KIND_LAMBDA,
 76      a_f2,
 77      bitwuzla_mk_term1_indexed2(
 78          tm,
 79          BITWUZLA_KIND_BV_EXTRACT,
 80          bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f1, a_f2),
 81          1,
 82          0));
 83
 84  // (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
 85  BitwuzlaTerm a0 =
 86      bitwuzla_mk_term2(tm,
 87                        BITWUZLA_KIND_BV_ULT,
 88                        x2,
 89                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f2, fpzero));
 90  bitwuzla_assert(bitwuzla, a0);
 91
 92  // (assert (! (= x1 x2 x3) :named a1))
 93  BitwuzlaTerm a1 = bitwuzla_mk_term3(tm, BITWUZLA_KIND_EQUAL, x1, x2, x3);
 94  bitwuzla_assert(bitwuzla, a1);
 95
 96  // (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
 97  BitwuzlaTerm a2 = bitwuzla_mk_term2(
 98      tm,
 99      BITWUZLA_KIND_EQUAL,
100      x4,
101      bitwuzla_mk_term2_indexed2(tm,
102                                 BITWUZLA_KIND_FP_TO_FP_FROM_UBV,
103                                 bitwuzla_mk_rm_value(tm, BITWUZLA_RM_RNE),
104                                 x3,
105                                 5,
106                                 11));
107  bitwuzla_assert(bitwuzla, a2);
108
109  // (check-sat)
110  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
111  printf("Expect: unsat\n");
112  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
113
114  // (get-unsat-core)
115  size_t unsat_core_size;
116  const BitwuzlaTerm *unsat_core =
117      bitwuzla_get_unsat_core(bitwuzla, &unsat_core_size);
118  printf("Unsat Core:\n{\n");
119  for (uint32_t i = 0; i < unsat_core_size; ++i)
120  {
121    printf(" %s\n", bitwuzla_term_to_string(unsat_core[i]));
122  }
123  printf("}\n");
124
125  // Finally, delete the Bitwuzla solver, options, and term manager instances.
126  bitwuzla_delete(bitwuzla);
127  bitwuzla_options_delete(options);
128  bitwuzla_term_manager_delete(tm);
129
130  return 0;
131}

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/c/unsatassumptions.c.
  1/***
  2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
  3 *
  4 * Copyright (C) 2021 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/c/bitwuzla.h>
 12#include <stdio.h>
 13
 14int
 15main()
 16{
 17  // First, create a term manager instance.
 18  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();
 19  // Create a Bitwuzla options instance.
 20  BitwuzlaOptions *options = bitwuzla_options_new();
 21  // (set-option :produce-unsat-assumptions true)
 22  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS, 1);
 23  // Then, create a Bitwuzla instance.
 24  Bitwuzla *bitwuzla = bitwuzla_new(tm, options);
 25
 26  // Create Boolean sort.
 27  BitwuzlaSort sortbool = bitwuzla_mk_bool_sort(tm);
 28  // Create a bit-vector sort of size 2.
 29  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
 30  // Create a bit-vector sort of size 4.
 31  BitwuzlaSort sortbv4 = bitwuzla_mk_bv_sort(tm, 4);
 32  // Create Float16 floatinf-point sort.
 33  BitwuzlaSort sortfp16 = bitwuzla_mk_fp_sort(tm, 5, 11);
 34  // Create bit-vector variables.
 35  // (declare-const x0 (_ BitVec 4))
 36  BitwuzlaTerm x0 = bitwuzla_mk_const(tm, sortbv4, "x0");
 37  // (declare-const x1 (_ BitVec 2))
 38  BitwuzlaTerm x1 = bitwuzla_mk_const(tm, sortbv2, "x1");
 39  // (declare-const x2 (_ BitVec 2))
 40  BitwuzlaTerm x2 = bitwuzla_mk_const(tm, sortbv2, "x2");
 41  // (declare-const x3 (_ BitVec 2))
 42  BitwuzlaTerm x3 = bitwuzla_mk_const(tm, sortbv2, "x3");
 43  // (declare-const x4 Float16)
 44  BitwuzlaTerm x4 = bitwuzla_mk_const(tm, sortfp16, "x4");
 45
 46  // Create FP positive zero.
 47  BitwuzlaTerm fpzero = bitwuzla_mk_fp_pos_zero(tm, sortfp16);
 48  // Create BV zero of size 4.
 49  BitwuzlaTerm bvzero = bitwuzla_mk_bv_zero(tm, sortbv4);
 50
 51  // (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
 52  BitwuzlaTerm a_f0 = bitwuzla_mk_var(tm, sortfp16, "a_f0");
 53  BitwuzlaTerm f0   = bitwuzla_mk_term2(
 54      tm,
 55      BITWUZLA_KIND_LAMBDA,
 56      a_f0,
 57      bitwuzla_mk_term2(tm, BITWUZLA_KIND_FP_GT, a_f0, fpzero));
 58
 59  // (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
 60  BitwuzlaTerm a_f1 = bitwuzla_mk_var(tm, sortfp16, "a_f1");
 61  BitwuzlaTerm f1   = bitwuzla_mk_term2(
 62      tm,
 63      BITWUZLA_KIND_LAMBDA,
 64      a_f1,
 65      bitwuzla_mk_term3(tm,
 66                        BITWUZLA_KIND_ITE,
 67                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f0, a_f1),
 68                        x0,
 69                        bvzero));
 70
 71  // (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
 72  BitwuzlaTerm a_f2 = bitwuzla_mk_var(tm, sortfp16, "a_f2");
 73  BitwuzlaTerm f2   = bitwuzla_mk_term2(
 74      tm,
 75      BITWUZLA_KIND_LAMBDA,
 76      a_f2,
 77      bitwuzla_mk_term1_indexed2(
 78          tm,
 79          BITWUZLA_KIND_BV_EXTRACT,
 80          bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f1, a_f2),
 81          1,
 82          0));
 83
 84  // (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
 85  BitwuzlaTerm a0 = bitwuzla_mk_const(tm, sortbool, "a0");
 86  BitwuzlaTerm assumption0 =
 87      bitwuzla_mk_term2(tm,
 88                        BITWUZLA_KIND_BV_ULT,
 89                        x2,
 90                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f2, fpzero));
 91  bitwuzla_assert(bitwuzla,
 92                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, a0, assumption0));
 93  // (assert (! (= x1 x2 x3) :named a1))
 94  BitwuzlaTerm a1 = bitwuzla_mk_const(tm, sortbool, "a1");
 95  BitwuzlaTerm assumption1 =
 96      bitwuzla_mk_term3(tm, BITWUZLA_KIND_EQUAL, x1, x2, x3);
 97  bitwuzla_assert(bitwuzla,
 98                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, a1, assumption1));
 99  // (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
100  BitwuzlaTerm a2          = bitwuzla_mk_const(tm, sortbool, "a2");
101  BitwuzlaTerm assumption2 = bitwuzla_mk_term2(
102      tm,
103      BITWUZLA_KIND_EQUAL,
104      x4,
105      bitwuzla_mk_term2_indexed2(tm,
106                                 BITWUZLA_KIND_FP_TO_FP_FROM_UBV,
107                                 bitwuzla_mk_rm_value(tm, BITWUZLA_RM_RNE),
108                                 x3,
109                                 5,
110                                 11));
111  bitwuzla_assert(bitwuzla,
112                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, a2, assumption2));
113
114  BitwuzlaTerm assumptions[3] = {a0, a1, a2};
115  // (check-sat-assuming (assumption0 assumption1 assumption2))
116  BitwuzlaResult result = bitwuzla_check_sat_assuming(bitwuzla, 3, assumptions);
117  printf("Expect: unsat\n");
118  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
119
120  // (get-unsat-assumptions)
121  size_t unsat_assumptions_size;
122  const BitwuzlaTerm *unsat_assumptions =
123      bitwuzla_get_unsat_assumptions(bitwuzla, &unsat_assumptions_size);
124  printf("Unsat Assumptions: {");
125  for (uint32_t i = 0; i < unsat_assumptions_size; ++i)
126  {
127    printf(" %s", bitwuzla_term_to_string(unsat_assumptions[i]));
128  }
129  printf(" }\n");
130
131  // Finally, delete the Bitwuzla solver, options, and term manager instances.
132  bitwuzla_delete(bitwuzla);
133  bitwuzla_options_delete(options);
134  bitwuzla_term_manager_delete(tm);
135
136  return 0;
137}

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/c/reset.c.
  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/c/bitwuzla.h>
 12#include <stdio.h>
 13
 14int
 15main()
 16{
 17  BitwuzlaResult result;
 18
 19  // First, create a term manager instance.
 20  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
 21  // Create a Bitwuzla options instance.
 22  BitwuzlaOptions* options = bitwuzla_options_new();
 23  // (set-option :produce-models false)
 24  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 0);
 25
 26  // Then, create a Bitwuzla instance.
 27  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
 28
 29  // Create a bit-vector sort of size 3.
 30  BitwuzlaSort sortbv3 = bitwuzla_mk_bv_sort(tm, 3);
 31
 32  // (declare-const x (_ BitVec 3))
 33  BitwuzlaTerm x = bitwuzla_mk_const(tm, sortbv3, "x");
 34
 35  // (assert (= x #b010))
 36  bitwuzla_assert(
 37      bitwuzla,
 38      bitwuzla_mk_term2(tm,
 39                        BITWUZLA_KIND_EQUAL,
 40                        x,
 41                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 2)));
 42  // (check-sat)
 43  result = bitwuzla_check_sat(bitwuzla);
 44  printf("Expect: sat\n");
 45  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
 46
 47  bitwuzla_delete(bitwuzla);
 48
 49  // (set-option :produce-models true)
 50  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, true);
 51
 52  // (reset)
 53  // Note: Bitwuzla does not provide an explicit API function for reset since
 54  //       this is achieved by simply discarding the current Bitwuzla instance
 55  //       and creating a new one.
 56  bitwuzla = bitwuzla_new(tm, options);
 57
 58  // (declare-const a ( Array (_ BitVec 2) (_ BitVec 3)))
 59  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
 60  BitwuzlaTerm a =
 61      bitwuzla_mk_const(tm, bitwuzla_mk_array_sort(tm, sortbv2, sortbv3), "a");
 62
 63  // (assert (= x #b011))
 64  bitwuzla_assert(
 65      bitwuzla,
 66      bitwuzla_mk_term2(tm,
 67                        BITWUZLA_KIND_EQUAL,
 68                        x,
 69                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 3)));
 70  // (assert (= x (select a #b01)))
 71  bitwuzla_assert(
 72      bitwuzla,
 73      bitwuzla_mk_term2(
 74          tm,
 75          BITWUZLA_KIND_EQUAL,
 76          x,
 77          bitwuzla_mk_term2(tm,
 78                            BITWUZLA_KIND_ARRAY_SELECT,
 79                            a,
 80                            bitwuzla_mk_bv_value_uint64(tm, sortbv2, 1))));
 81  // (check-sat)
 82  result = bitwuzla_check_sat(bitwuzla);
 83  printf("Expect: sat\n");
 84  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
 85  // (get-model)
 86  printf("(\n");
 87  printf("  (define-fun %s () ", bitwuzla_term_get_symbol(x));
 88  printf("%s ", bitwuzla_sort_to_string(bitwuzla_term_get_sort(x)));
 89  printf("%s)\n", bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, x)));
 90  printf("  (define-fun %s () ", bitwuzla_term_get_symbol(a));
 91  printf("%s ", bitwuzla_sort_to_string(bitwuzla_term_get_sort(a)));
 92  printf("%s)\n", bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, a)));
 93  printf(")\n");
 94
 95  // Finally, delete the Bitwuzla solver, options, and term manager instances.
 96  bitwuzla_delete(bitwuzla);
 97  bitwuzla_options_delete(options);
 98  bitwuzla_term_manager_delete(tm);
 99
100  return 0;
101}

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/c/reset_assertions.c.
 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/c/bitwuzla.h>
12#include <stdio.h>
13
14int
15main()
16{
17  BitwuzlaResult result;
18
19  // First, create a term manager instance.
20  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
21  // Create a Bitwuzla options instance.
22  BitwuzlaOptions* options = bitwuzla_options_new();
23  // (set-option :produce-models true)
24  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
25
26  // Then, create a Bitwuzla instance.
27  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
28
29  // Create a bit-vector sort of size 3.
30  BitwuzlaSort sortbv3 = bitwuzla_mk_bv_sort(tm, 3);
31
32  // (declare-const x (_ BitVec 3))
33  BitwuzlaTerm x = bitwuzla_mk_const(tm, sortbv3, "x");
34
35  // (assert (= x #b010))
36  bitwuzla_assert(
37      bitwuzla,
38      bitwuzla_mk_term2(tm,
39                        BITWUZLA_KIND_EQUAL,
40                        x,
41                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 2)));
42  // (check-sat)
43  result = bitwuzla_check_sat(bitwuzla);
44  printf("Expect: sat\n");
45  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
46  // (assert (= x #b001))
47  bitwuzla_assert(
48      bitwuzla,
49      bitwuzla_mk_term2(tm,
50                        BITWUZLA_KIND_EQUAL,
51                        x,
52                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 1)));
53  // (check-sat)
54  result = bitwuzla_check_sat(bitwuzla);
55  printf("Expect: unsat\n");
56  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
57
58  // (reset-assertions)
59  // Note: Bitwuzla does not provide an explicit API function for
60  //       reset-assertions since this is achieved by simply discarding
61  //       the current Bitwuzla instance and creating a new one.
62  bitwuzla_delete(bitwuzla);
63  bitwuzla = bitwuzla_new(tm, options);
64
65  // (assert (= x #b011))
66  bitwuzla_assert(
67      bitwuzla,
68      bitwuzla_mk_term2(tm,
69                        BITWUZLA_KIND_EQUAL,
70                        x,
71                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 3)));
72  // (check-sat)
73  result = bitwuzla_check_sat(bitwuzla);
74  printf("Expect: sat\n");
75  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
76  // (get-model)
77  printf("(\n");
78  printf("  (define-fun %s", bitwuzla_term_get_symbol(x));
79  printf(" () %s", bitwuzla_sort_to_string(bitwuzla_term_get_sort(x)));
80  printf(" %s)\n", bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, x)));
81  printf(")\n");
82
83  // Finally, delete the Bitwuzla solver, options, and term manager instances.
84  bitwuzla_delete(bitwuzla);
85  bitwuzla_options_delete(options);
86  bitwuzla_term_manager_delete(tm);
87
88  return 0;
89}

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/c/parse.c.
  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/c/bitwuzla.h>
 13#include <bitwuzla/c/parser.h>
 14#include <stdlib.h>
 15
 16int
 17main()
 18{
 19  // First, create a term manager instance.
 20  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
 21  // Create a Bitwuzla options instance.
 22  BitwuzlaOptions* options = bitwuzla_options_new();
 23
 24  // We will parse example file `smt2/quickstart.smt2`.
 25  // Create parser instance.
 26  const char* infile_name = "../smt2/quickstart.smt2";
 27  BitwuzlaParser* parser =
 28      bitwuzla_parser_new(tm, options, "smt2", 2, "<stdout>");
 29
 30  // Now parse the input file.
 31  const char* error_msg;
 32  printf("Expect: sat\n");
 33  printf("Bitwuzla: ");
 34  bitwuzla_parser_parse(parser, infile_name, false, true, &error_msg);
 35  // We expect no error to occur.
 36  assert(!error_msg);
 37
 38  // Now we retrieve the set of asserted formulas and print them.
 39  size_t size;
 40  const BitwuzlaTerm* assertions =
 41      bitwuzla_get_assertions(bitwuzla_parser_get_bitwuzla(parser), &size);
 42  printf("Assertions:\n");
 43  printf("{\n");
 44  for (size_t i = 0; i < size; ++i)
 45  {
 46    printf("  %s\n", bitwuzla_term_to_string(assertions[i]));
 47  }
 48  printf("}\n");
 49
 50  // Now we add an assertion via parsing from string.
 51  bitwuzla_parser_parse(
 52      parser, "(assert (distinct (select a x) y))", true, false, &error_msg);
 53  // We expect no error to occur.
 54  assert(!error_msg);
 55  // Now the formula is unsat.
 56  BitwuzlaResult result =
 57      bitwuzla_check_sat(bitwuzla_parser_get_bitwuzla(parser));
 58
 59  printf("Expect: unsat\n");
 60  printf("Bitwuzla: %s\n\n", bitwuzla_result_to_string(result));
 61
 62  // For illustration purposes, we now parse in some declarations and terms 
 63  // and sorts from string.
 64
 65  // Declare bit-vector sort of size 16.
 66  BitwuzlaSort bv16 =
 67      bitwuzla_parser_parse_sort(parser, "(_ BitVec 16)", &error_msg);
 68  // We expect no error to occur.
 69  assert(!error_msg);
 70  // Create bit-vector sort of size 16 and show that it corresponds to
 71  // its string representation '(_ BitVec16)'.
 72  assert(bv16 == bitwuzla_mk_bv_sort(tm, 16));
 73
 74  // Declare Boolean constants 'c' and 'd'.
 75  // Note: Declarations are commands (not terms) in the SMT-LIB language.
 76  //       Commands must be parsed in via bitwuzla_parser_parse(),
 77  //       bitwuzla_parser_parse_term() only supports parsing SMT-LIB terms.
 78  bitwuzla_parser_parse(parser,
 79                        "(declare-const c Bool)(declare-const d Bool)",
 80                        true,
 81                        false,
 82                        &error_msg);
 83  // Declare bit-vector constant 'b'.
 84  bitwuzla_parser_parse(
 85      parser, "(declare-const b (_ BitVec 16))", true, false, &error_msg);
 86  // We expect no error to occur.
 87  assert(!error_msg);
 88  // Retrieve term representing 'b'.
 89  BitwuzlaTerm b = bitwuzla_parser_parse_term(parser, "b", &error_msg);
 90  // We expect no error to occur.
 91  assert(!error_msg);
 92  // Retrieve term representing 'c'.
 93  BitwuzlaTerm c = bitwuzla_parser_parse_term(parser, "c", &error_msg);
 94  // We expect no error to occur.
 95  assert(!error_msg);
 96  // Retrieve term representing 'd'.
 97  BitwuzlaTerm d = bitwuzla_parser_parse_term(parser, "d", &error_msg);
 98  // We expect no error to occur.
 99  assert(!error_msg);
100  // Create xor over 'a' and 'c' and show that it corresponds to term
101  // parsed in from its string representation '(xor c d)'.
102  assert(bitwuzla_parser_parse_term(parser, "(xor c d)", &error_msg)
103         == bitwuzla_mk_term2(tm, BITWUZLA_KIND_XOR, c, d));
104  // Create bit-vector addition over 'b' and bit-vector value
105  // '1011111010001010' and show that it corresponds to the term parsed in
106  // from its string representation '(bvadd b #b1011111010001010)'.
107  assert(bitwuzla_parser_parse_term(
108             parser, "(bvadd b #b1011111010001010)", &error_msg)
109         == bitwuzla_mk_term2(
110             tm,
111             BITWUZLA_KIND_BV_ADD,
112             b,
113             bitwuzla_mk_bv_value(tm, bv16, "1011111010001010", 2)));
114  // Finally, delete Bitwuzla parser, options, and term manager instance.
115  bitwuzla_parser_delete(parser);
116  bitwuzla_options_delete(options);
117  bitwuzla_term_manager_delete(tm);
118
119  return 0;
120}

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/c/print.c.
  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/c/bitwuzla.h>
 13#include <stdio.h>
 14
 15int
 16main()
 17{
 18  // First, create a term manager instance.
 19  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
 20  // Create a Bitwuzla options instance.
 21  BitwuzlaOptions* options = bitwuzla_options_new();
 22  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
 23  // Then, create a Bitwuzla instance.
 24  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
 25  // Create some sorts.
 26  BitwuzlaSort bv8           = bitwuzla_mk_bv_sort(tm, 8);
 27  BitwuzlaSort bv32          = bitwuzla_mk_bv_sort(tm, 32);
 28  BitwuzlaSort fp16          = bitwuzla_mk_fp_sort(tm, 5, 11);
 29  BitwuzlaSort fun_domain[3] = {bv8, fp16, bv32};
 30  BitwuzlaSort fun_sort      = bitwuzla_mk_fun_sort(tm, 3, fun_domain, fp16);
 31  // Create terms.
 32  BitwuzlaTerm b    = bitwuzla_mk_const(tm, bitwuzla_mk_bool_sort(tm), "b");
 33  BitwuzlaTerm bv   = bitwuzla_mk_const(tm, bv8, "bv");
 34  BitwuzlaTerm fp   = bitwuzla_mk_const(tm, fp16, "fp");
 35  BitwuzlaTerm rm   = bitwuzla_mk_const(tm, bitwuzla_mk_rm_sort(tm), "rm");
 36  BitwuzlaTerm fun  = bitwuzla_mk_const(tm, fun_sort, "fun");
 37  BitwuzlaTerm zero = bitwuzla_mk_bv_zero(tm, bv8);
 38  BitwuzlaTerm ones = bitwuzla_mk_bv_ones(tm, bitwuzla_mk_bv_sort(tm, 23));
 39  BitwuzlaTerm z    = bitwuzla_mk_var(tm, bv8, "z");
 40  BitwuzlaTerm q    = bitwuzla_mk_var(tm, bv8, "q");
 41  BitwuzlaTerm lambda =
 42      bitwuzla_mk_term2(tm,
 43                        BITWUZLA_KIND_LAMBDA,
 44                        z,
 45                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, z, bv));
 46  BitwuzlaTerm args[4] = {
 47      fun,
 48      bv,
 49      fp,
 50      bitwuzla_mk_term1_indexed1(tm, BITWUZLA_KIND_BV_ZERO_EXTEND, ones, 9)};
 51  BitwuzlaTerm fpleq =
 52      bitwuzla_mk_term2(tm,
 53                        BITWUZLA_KIND_FP_LEQ,
 54                        bitwuzla_mk_term(tm, BITWUZLA_KIND_APPLY, 4, args),
 55                        fp);
 56  BitwuzlaTerm exists = bitwuzla_mk_term2(
 57      tm,
 58      BITWUZLA_KIND_EXISTS,
 59      q,
 60      bitwuzla_mk_term2(tm,
 61                        BITWUZLA_KIND_EQUAL,
 62                        zero,
 63                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, bv, q)));
 64  // Assert formulas.
 65  bitwuzla_assert(bitwuzla, b);
 66  bitwuzla_assert(
 67      bitwuzla,
 68      bitwuzla_mk_term2(tm,
 69                        BITWUZLA_KIND_EQUAL,
 70                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, lambda, bv),
 71                        zero));
 72  bitwuzla_assert(bitwuzla, exists);
 73  bitwuzla_assert(bitwuzla, fpleq);
 74
 75  // Print sort.
 76  printf("Print bit-vector sort of size 32:\n");
 77  printf("---------------------------------\n");
 78  printf("bitwuzla_sort_print():     ");
 79  bitwuzla_sort_print(bv32, stdout);
 80  printf("\n");
 81  printf("bitwuzla_sort_to_string(): %s\n\n", bitwuzla_sort_to_string(bv32));
 82
 83  // Print terms.
 84  // Note: Hexadecimal bv output format is ignored if the value is not of size
 85  //       divisible by 4.
 86  printf("Print term:\n");
 87  printf("-----------\n");
 88  printf("bitwuzla_term_print():                         ");
 89  bitwuzla_term_print(rm, stdout);
 90  printf("\n");
 91  printf("bitwuzla_term_print_fmt()     [dec (ignored)]: ");
 92  bitwuzla_term_print_fmt(rm, stdout, 10);
 93  printf("\n");
 94  printf("bitwuzla_term_to_string():                     %s\n",
 95         bitwuzla_term_to_string(rm));
 96  printf("bitwuzla_term_to_string_fmt() [hex (ignored)]: %s\n",
 97         bitwuzla_term_to_string_fmt(rm, 10));
 98  printf("\n");
 99  printf("bitwuzla_term_print()         [bin]: ");
100  bitwuzla_term_print(zero, stdout);
101  printf("\n");
102  printf("bitwuzla_term_print_fmt()     [dec]: ");
103  bitwuzla_term_print_fmt(zero, stdout, 10);
104  printf("\n");
105  printf("bitwuzla_term_print_fmt()     [hex]: ");
106  bitwuzla_term_print_fmt(zero, stdout, 16);
107  printf("\n");
108  printf("bitwuzla_term_to_string()     [bin]: %s\n",
109         bitwuzla_term_to_string(zero));
110  printf("bitwuzla_term_to_string_fmt() [dec]: %s\n",
111         bitwuzla_term_to_string_fmt(zero, 10));
112  printf("bitwuzla_term_to_string_fmt() [hex]: %s\n",
113         bitwuzla_term_to_string_fmt(zero, 16));
114  printf("\n");
115  printf("bitwuzla_term_print_fmt()     [bin]:           ");
116  bitwuzla_term_print_fmt(fpleq, stdout, 2);
117  printf("\n");
118  printf("bitwuzla_term_print_fmt()     [dec]:           ");
119  bitwuzla_term_print_fmt(fpleq, stdout, 10);
120  printf("\n");
121  printf("bitwuzla_term_print_fmt()     [hex (ignored)]: ");
122  bitwuzla_term_print_fmt(fpleq, stdout, 16);
123  printf("\n");
124  printf("bitwuzla_term_to_string_fmt() [bin]:           %s\n",
125         bitwuzla_term_to_string_fmt(fpleq, 2));
126  printf("bitwuzla_term_to_string_fmt() [dec]:           %s\n",
127         bitwuzla_term_to_string_fmt(fpleq, 10));
128  printf("bitwuzla_term_to_string_fmt() [hex (ignored)]: %s\n",
129         bitwuzla_term_to_string_fmt(fpleq, 16));
130  printf("\n");
131
132  // Print asserted formulas using binary bit-vector output format.
133  {
134    printf("Print formula [binary bv output format]:\n");
135    printf("----------------------------------------\n");
136    bitwuzla_print_formula(bitwuzla, "smt2", stdout, 2);
137    printf("\n");
138  }
139
140  // Print asserted formulas using hexadecimal bit-vector output format.
141  {
142    printf("Print formula [hexadecimal bv output format]:\n");
143    printf("----------------------------------------\n");
144    bitwuzla_print_formula(bitwuzla, "smt2", stdout, 16);
145    printf("\n");
146  }
147
148  // Print asserted formulas using decimal bit-vector output format.
149  {
150    printf("Print formula [decimal bv output format]:\n");
151    printf("----------------------------------------\n");
152    bitwuzla_print_formula(bitwuzla, "smt2", stdout, 10);
153    printf("\n");
154  }
155
156  bitwuzla_check_sat(bitwuzla);
157
158  // Print values.
159  printf("Print value of Boolean predicate:\n");
160  printf("---------------------------------\n");
161  BitwuzlaTerm fpleq_val    = bitwuzla_get_value(bitwuzla, fpleq);
162  bool fpleq_val_bool       = bitwuzla_term_value_get_bool(fpleq_val);
163  const char* fpleq_val_str = bitwuzla_term_value_get_str(fpleq_val);
164  printf("%s: %*u [bool]\n", bitwuzla_term_to_string(fpleq), 4, fpleq_val_bool);
165  printf("%s: %*s [const char*]\n\n",
166         bitwuzla_term_to_string(fpleq),
167         4,
168         fpleq_val_str);
169
170  printf("Print value of bv const:\n");
171  printf("------------------------\n");
172  BitwuzlaTerm bv_val = bitwuzla_get_value(bitwuzla, bv);
173  printf("%s: %*s [const char*] (bin)\n",
174         bitwuzla_term_to_string(bv),
175         8,
176         bitwuzla_term_value_get_str(bv_val));
177  printf("%s: %*s [const char*] (dec)\n",
178         bitwuzla_term_to_string(bv),
179         8,
180         bitwuzla_term_value_get_str_fmt(bv_val, 10));
181  printf("%s: %*s [const char*] (hex)\n\n",
182         bitwuzla_term_to_string(bv),
183         8,
184         bitwuzla_term_value_get_str_fmt(bv_val, 16));
185
186  printf("Print value of RoundingMode const:\n");
187  printf("----------------------------------\n");
188  BitwuzlaTerm rm_val = bitwuzla_get_value(bitwuzla, rm);
189  BitwuzlaRoundingMode rm_val_rm = bitwuzla_term_value_get_rm(rm_val);
190  const char* rm_val_str         = bitwuzla_term_value_get_str(rm_val);
191  printf("%s: %s [BitwuzlaRoundingMode]\n",
192         bitwuzla_term_to_string(rm),
193         bitwuzla_rm_to_string(rm_val_rm));
194  printf("%s: %s [const char*]\n\n", bitwuzla_term_to_string(rm), rm_val_str);
195
196  BitwuzlaTerm fp_val = bitwuzla_get_value(bitwuzla, fp);
197
198  printf("Print value of fp const via bitwuzla_term_value_get_str(_fmt):\n");
199  printf("--------------------------------------------------------------\n");
200  printf("%s: %*s [const char*] (bin) \n",
201         bitwuzla_term_to_string(fp),
202         16,
203         bitwuzla_term_value_get_str(fp_val));
204  printf("%s: %*s [const char*] (dec [ignored]) \n",
205         bitwuzla_term_to_string(fp),
206         16,
207         bitwuzla_term_value_get_str_fmt(fp_val, 10));
208  printf("%s: %*s [const char*] (hex [ignored]) \n\n",
209         bitwuzla_term_to_string(fp),
210         16,
211         bitwuzla_term_value_get_str_fmt(fp_val, 16));
212
213  printf("Print value of fp const via bitwuzla_term_value_get_fp_ieee():\n");
214  printf("--------------------------------------------------------------\n");
215  const char* sign;
216  const char* exponent;
217  const char* significand;
218  bitwuzla_term_value_get_fp_ieee(fp_val, &sign, &exponent, &significand, 2);
219  printf("%s: (%s %*s %*s) (bin)\n",
220         bitwuzla_term_to_string(fp),
221         sign,
222         5,
223         exponent,
224         11,
225         significand);
226  bitwuzla_term_value_get_fp_ieee(fp_val, &sign, &exponent, &significand, 10);
227  printf("%s: (%s %*s %*s) (dec)\n",
228         bitwuzla_term_to_string(fp),
229         sign,
230         5,
231         exponent,
232         11,
233         significand);
234  bitwuzla_term_value_get_fp_ieee(fp_val, &sign, &exponent, &significand, 16);
235  printf("%s: (%s %*s %*s) (hex)\n",
236         bitwuzla_term_to_string(fp),
237         sign,
238         5,
239         exponent,
240         11,
241         significand);
242
243  // Finally, delete the Bitwuzla solver, options, and term manager instances.
244  bitwuzla_delete(bitwuzla);
245  bitwuzla_options_delete(options);
246  bitwuzla_term_manager_delete(tm);
247  return 0;
248}

Termination Callback Example

This example shows how to configure a termination callback.
The source code for this example can be found at examples/c/terminator.c.
  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/c/bitwuzla.h>
 12#include <stdint.h>
 13#include <stdio.h>
 14#include <sys/time.h>
 15
 16struct terminator_state
 17{
 18  struct timeval start;
 19  uint32_t time_limit_ms;
 20};
 21
 22static int32_t
 23test_terminate(void* state)
 24{
 25  struct terminator_state* tstate = (struct terminator_state*) state;
 26  struct timeval now;
 27  gettimeofday(&now, NULL);
 28  if (((now.tv_sec - tstate->start.tv_sec) * 1000
 29       + (now.tv_usec - tstate->start.tv_usec) / 1000)
 30      >= tstate->time_limit_ms)
 31  {
 32    return 1;
 33  }
 34  return 0;
 35}
 36
 37int
 38main()
 39{
 40  // First, create a term manager instance.
 41  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
 42  // Create a Bitwuzla options instance.
 43  BitwuzlaOptions* options = bitwuzla_options_new();
 44  // Then, create a Bitwuzla instance.
 45  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
 46
 47  BitwuzlaSort bv = bitwuzla_mk_bv_sort(tm, 32);
 48
 49  BitwuzlaTerm x = bitwuzla_mk_const(tm, bv, "x");
 50  BitwuzlaTerm s = bitwuzla_mk_const(tm, bv, "s");
 51  BitwuzlaTerm t = bitwuzla_mk_const(tm, bv, "t");
 52
 53  BitwuzlaTerm a = bitwuzla_mk_term2(
 54      tm,
 55      BITWUZLA_KIND_DISTINCT,
 56      bitwuzla_mk_term2(tm,
 57                        BITWUZLA_KIND_BV_MUL,
 58                        s,
 59                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, x, t)),
 60      bitwuzla_mk_term2(tm,
 61                        BITWUZLA_KIND_BV_MUL,
 62                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, s, x),
 63                        t));
 64
 65  // Now, we check that the following formula is unsat.
 66  // (assert (distinct (bvmul s (bvmul x t)) (bvmul (bvmul s x) t)))
 67  BitwuzlaTerm assumptions[1] = {a};
 68  printf("> Without terminator (with preprocessing):\n");
 69  printf("Expect: unsat\n");
 70  printf("Result: %s\n",
 71         bitwuzla_result_to_string(
 72             bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions)));
 73
 74  // Now, for illustration purposes, we disable preprocessing, which will
 75  // significantly increase solving time, and connect a terminator instance
 76  // that terminates after a certain time limit.
 77  bitwuzla_set_option(options, BITWUZLA_OPT_PREPROCESS, 0);
 78  // Create new Bitwuzla instance with reconfigured options.
 79  Bitwuzla* bitwuzla2 = bitwuzla_new(tm, options);
 80  // Configure termination callback.
 81  struct terminator_state state;
 82  gettimeofday(&state.start, NULL);
 83  state.time_limit_ms = 1000;
 84  bitwuzla_set_termination_callback(bitwuzla2, test_terminate, &state);
 85
 86  // Now, we expect Bitwuzla to be terminated during the check-sat call.
 87  printf("> With terminator (no preprocessing):\n");
 88  printf("Expect: unknown\n");
 89  printf("Result: %s\n",
 90         bitwuzla_result_to_string(
 91             bitwuzla_check_sat_assuming(bitwuzla2, 1, assumptions)));
 92
 93  // Finally, delete the Bitwuzla solver, options, and term manager instances.
 94  bitwuzla_delete(bitwuzla);
 95  bitwuzla_delete(bitwuzla2);
 96  bitwuzla_options_delete(options);
 97  bitwuzla_term_manager_delete(tm);
 98
 99  return 0;
100}

Manual Reference Counting of Sort and Terms Example

This example shows how to use the manual reference counting functions for
sorts and terms.
The source code for this example can be found at examples/c/manual_reference_counting.c.
 1/***
 2 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 3 *
 4 * Copyright (C) 2024 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/c/bitwuzla.h>
12#include <stdio.h>
13#include <assert.h>
14
15int
16main()
17{
18  // First, create a term manager instance.
19  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();
20  // Create a Bitwuzla options instance.
21  BitwuzlaOptions *options = bitwuzla_options_new();
22  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
23  // Then, create a Bitwuzla instance.
24  Bitwuzla *bitwuzla = bitwuzla_new(tm, options);
25
26  BitwuzlaSort sortb = bitwuzla_mk_bool_sort(tm);
27  BitwuzlaTerm a = bitwuzla_mk_const(tm, sortb, "a");
28  BitwuzlaTerm b = bitwuzla_mk_const(tm, sortb, "b");
29
30  // Release sort reference.
31  bitwuzla_sort_release(sortb);
32
33  BitwuzlaTerm dis = bitwuzla_mk_term2(tm, BITWUZLA_KIND_DISTINCT, a, b);
34  bitwuzla_assert(bitwuzla, dis);
35  bitwuzla_check_sat(bitwuzla);
36
37  // Release term reference.
38  bitwuzla_term_release(dis);
39
40  BitwuzlaTerm val_a = bitwuzla_get_value(bitwuzla, a);
41  BitwuzlaTerm val_b = bitwuzla_get_value(bitwuzla, b);
42
43  assert(val_a != val_b);
44  printf("value a: %s\n", bitwuzla_term_to_string(val_a));
45  printf("value b: %s\n", bitwuzla_term_to_string(val_b));
46
47  // Release remaining term references.
48  bitwuzla_term_release(val_a);
49  bitwuzla_term_release(val_b);
50  bitwuzla_term_release(a);
51  bitwuzla_term_release(b);
52
53  // At this point all sort and term references have been released. If all sort
54  // and term references should be released at once we can also use the
55  // following function.
56  bitwuzla_term_manager_release(tm);
57
58  // Finally, delete the Bitwuzla solver, options, and term manager instances.
59  bitwuzla_delete(bitwuzla);
60  bitwuzla_options_delete(options);
61  // Note: All sorts and terms not released until now will be released when
62  // deleting the term manager.
63  bitwuzla_term_manager_delete(tm);
64
65  return 0;
66}
67