Python API Documentation

Quickstart
Examples

Python Interface
- Classes
- Enums

Quickstart

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

    tm = TermManager()

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

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # Then, enable model generation.
    options.set(Option.PRODUCE_MODELS, True)
    # Now, for illustration purposes, we enable CaDiCaL as SAT solver
    # (CaDiCaL is already configured by default).
    # Note: This will silently fall back to one of the compiled in SAT solvers
    #       if the selected solver is not compiled in.
    options.set(Option.SAT_SOLVER, 'cadical')
    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create bit-vector sorts of size 4 and 8.
    sortbv4 = tm.mk_bv_sort(4)
    sortbv8 = tm.mk_bv_sort(8)
    # Create function sort.
    sortfun = tm.mk_fun_sort([sortbv8, sortbv4], sortbv8)
    # Create array sort.
    sortarr = tm.mk_array_sort(sortbv8, sortbv8)

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

    # (bvsdiv x (_ bv2 8))
    sdiv = tm.mk_term(Kind.BV_SDIV, [x, two])
    # (bvashr y (_ bv1 8))
    ashr = tm.mk_term(Kind.BV_ASHR, [y, one])
    # ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
    sdive = tm.mk_term(Kind.BV_EXTRACT, [sdiv], [3, 0])
    # ((_ extract 3 0) (bvashr x (_ bv1 8)))
    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 and then parsing the input file via bitwuzla.Parser.parse().

Note

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

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

    tm = TermManager()
    options = Options()
    # We will parse example file `smt2/quickstart.smt2`.
    # Create parser instance.
    parser = Parser(tm, options)
    res = parser.parse("../smt2/quickstart.smt2")
    assert not res

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.Bitwuzla.get_assertions():

    # Now we retrieve the set of asserted formulas and print them.
    assertions = parser.bitwuzla().get_assertions()
    print('Assertions:')
    print('{')
    for a in assertions:
        print(f' {a}')
    print('}')

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:

    parser.parse('(assert (distinct (select a x) y))', True, False)

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.
    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.parse_term():

    # Retrieve term representing 'b'.
    b = parser.parse_term('b')
    # Retrieve term representing 'c'.
    c = parser.parse_term('c')
    # Retrieve term representing 'd'.
    d = parser.parse_term('d')

Now, to parse in terms using these constants via bitwuzla.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().

    # (check-sat)
    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(). An example implementation illustrating how to print the current model via declared symbols (in this case x, y, f and a) is below:

    # Print model in SMT-LIBv2 format.
    print('Model:\n(')
    for term in [x, y, f, a]:
        sort = term.sort()
        symbol = term.symbol()
        print(f'  (define-fun {symbol if symbol else "@t" + term.id()} (',
              end = '')
        if sort.is_fun():
            value = bitwuzla.get_value(term)
            assert value.kind() == Kind.LAMBDA
            assert value.num_children() == 2
            while value[1].kind() == Kind.LAMBDA:
                assert value[0].is_variable()
                print(f'({value[0]} {value[0].sort()}) ',
                      end = '')
                value = value[1]
            assert value[0].is_variable()
            print(f'({value[0]} {value[0].sort()})) ' \
                  + f'{sort.fun_codomain()} {value[1]})')
        else:
            print(f') {sort} {bitwuzla.get_value(term)})')
    print(')')
    print()

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 a term via bitwuzla.Bitwuzla.get_value(); or as assignment via bitwuzla.Term.value(), which returns the string representation of bit-vector and floating-point values, the bitwuzla.RoundingMode value for RoundingMode values, and a bool value for Boolean values.

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.

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().
    print(f'value of x: {bitwuzla.get_value(x).value(2)}')
    print(f'value of y: {bitwuzla.get_value(y).value(2)}')

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().

    # 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().
    print('str() representation of value of f:')
    print(bitwuzla.get_value(f))
    print()
    print('str() representation of value of a:')
    print(bitwuzla.get_value(a))

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,

    print(f'str() representation of value of x: {bitwuzla.get_value(x)}')
    print(f'str() representation of value of y: {bitwuzla.get_value(y)}')

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:

    print(f'value of v = x * x: {v.value(2)}')

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/python/quickstart.py.

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

from bitwuzla import *

if __name__ == "__main__":

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # Then, enable model generation.
    options.set(Option.PRODUCE_MODELS, True)
    # Now, for illustration purposes, we enable CaDiCaL as SAT solver
    # (CaDiCaL is already configured by default).
    # Note: This will silently fall back to one of the compiled in SAT solvers
    #       if the selected solver is not compiled in.
    options.set(Option.SAT_SOLVER, 'cadical')
    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create bit-vector sorts of size 4 and 8.
    sortbv4 = tm.mk_bv_sort(4)
    sortbv8 = tm.mk_bv_sort(8)
    # Create function sort.
    sortfun = tm.mk_fun_sort([sortbv8, sortbv4], sortbv8)
    # Create array sort.
    sortarr = tm.mk_array_sort(sortbv8, sortbv8)

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

    # (bvsdiv x (_ bv2 8))
    sdiv = tm.mk_term(Kind.BV_SDIV, [x, two])
    # (bvashr y (_ bv1 8))
    ashr = tm.mk_term(Kind.BV_ASHR, [y, one])
    # ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
    sdive = tm.mk_term(Kind.BV_EXTRACT, [sdiv], [3, 0])
    # ((_ extract 3 0) (bvashr x (_ bv1 8)))
    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]))

    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # Print model in SMT-LIBv2 format.
    print('Model:\n(')
    for term in [x, y, f, a]:
        sort = term.sort()
        symbol = term.symbol()
        print(f'  (define-fun {symbol if symbol else "@t" + term.id()} (',
              end = '')
        if sort.is_fun():
            value = bitwuzla.get_value(term)
            assert value.kind() == Kind.LAMBDA
            assert value.num_children() == 2
            while value[1].kind() == Kind.LAMBDA:
                assert value[0].is_variable()
                print(f'({value[0]} {value[0].sort()}) ',
                      end = '')
                value = value[1]
            assert value[0].is_variable()
            print(f'({value[0]} {value[0].sort()})) ' \
                  + f'{sort.fun_codomain()} {value[1]})')
        else:
            print(f') {sort} {bitwuzla.get_value(term)})')
    print(')')
    print()

    # Print value for x, y, f and a.
    # Both x and y are bit-vector terms and their value is a bit-vector
    # value that can be printed via Term.value().
    print(f'value of x: {bitwuzla.get_value(x).value(2)}')
    print(f'value of y: {bitwuzla.get_value(y).value(2)}')
    print()
    # 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().
    print('str() representation of value of f:')
    print(bitwuzla.get_value(f))
    print()
    print('str() representation of value of a:')
    print(bitwuzla.get_value(a))
    print()
    # Note that the assignment string of bit-vector terms is given as the
    # pure assignment string, either in binary, hexadecimal or decimal format,
    # whereas Term.str() prints the value in SMT-LIB2 format (in the given
    # bit-vector output number format, binary by default).
    print(f'str() representation of value of x: {bitwuzla.get_value(x)}')
    print(f'str() representation of value of y: {bitwuzla.get_value(y)}')
    print()

    # Query value of bit-vector term that does not occur in the input formula
    v = bitwuzla.get_value(tm.mk_term(Kind.BV_MUL, [x, x]))
    print(f'value of v = x * x: {v.value(2)}')

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

from bitwuzla import *

if __name__ == "__main__":

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # Then, enable model generation.
    options.set(Option.PRODUCE_MODELS, True)
    # Now, for illustration purposes, we enable CaDiCaL as SAT solver
    # (CaDiCaL is already configured by default).
    # Note: This will silently fall back to one of the compiled in SAT solvers
    #       if the selected solver is not compiled in.
    options.set(Option.SAT_SOLVER, 'cadical')
    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create bit-vector sorts of size 4 and 8.
    sortbv4 = tm.mk_bv_sort(4)
    sortbv8 = tm.mk_bv_sort(8)
    # Create function sort.
    sortfun = tm.mk_fun_sort([sortbv8, sortbv4], sortbv8)
    # Create array sort.
    sortarr = tm.mk_array_sort(sortbv8, sortbv8)

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

    # (bvsdiv x (_ bv2 8))
    sdiv = tm.mk_term(Kind.BV_SDIV, [x, two])
    # (bvashr y (_ bv1 8))
    ashr = tm.mk_term(Kind.BV_ASHR, [y, one])
    # ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
    sdive = tm.mk_term(Kind.BV_EXTRACT, [sdiv], [3, 0])
    # ((_ extract 3 0) (bvashr x (_ bv1 8)))
    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]))

    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # Print model in SMT-LIBv2 format.
    print('Model:\n(')
    for term in [x, y, f, a]:
        sort = term.sort()
        symbol = term.symbol()
        print(f'  (define-fun {symbol if symbol else "@t" + term.id()} (',
              end = '')
        if sort.is_fun():
            value = bitwuzla.get_value(term)
            assert value.kind() == Kind.LAMBDA
            assert value.num_children() == 2
            while value[1].kind() == Kind.LAMBDA:
                assert value[0].is_variable()
                print(f'({value[0]} {value[0].sort()}) ',
                      end = '')
                value = value[1]
            assert value[0].is_variable()
            print(f'({value[0]} {value[0].sort()})) ' \
                  + f'{sort.fun_codomain()} {value[1]})')
        else:
            print(f') {sort} {bitwuzla.get_value(term)})')
    print(')')
    print()

    # Print value for x, y, f and a.
    # Both x and y are bit-vector terms and their value is a bit-vector
    # value that can be printed via Term.value().
    print(f'value of x: {bitwuzla.get_value(x).value(2)}')
    print(f'value of y: {bitwuzla.get_value(y).value(2)}')
    print()
    # 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().
    print('str() representation of value of f:')
    print(bitwuzla.get_value(f))
    print()
    print('str() representation of value of a:')
    print(bitwuzla.get_value(a))
    print()
    # Note that the assignment string of bit-vector terms is given as the
    # pure assignment string, either in binary, hexadecimal or decimal format,
    # whereas Term.str() prints the value in SMT-LIB2 format (in the given
    # bit-vector output number format, binary by default).
    print(f'str() representation of value of x: {bitwuzla.get_value(x)}')
    print(f'str() representation of value of y: {bitwuzla.get_value(y)}')
    print()

    # Query value of bit-vector term that does not occur in the input formula
    v = bitwuzla.get_value(tm.mk_term(Kind.BV_MUL, [x, x]))
    print(f'value of v = x * x: {v.value(2)}')

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

#include <assert.h>
#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  // First, create a term manager instance.
  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions *options = bitwuzla_options_new();
  // Then, enable model generation.
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
  // Now, for illustration purposes, we enable CaDiCaL as SAT solver
  // (CaDiCaL is already configured by default).
  // Note: This will silently fall back to one of the compiled in SAT solvers
  //       if the selected solver is not compiled in.
  bitwuzla_set_option_mode(options, BITWUZLA_OPT_SAT_SOLVER, "cadical");
  // Then, create a Bitwuzla instance.
  Bitwuzla *bitwuzla = bitwuzla_new(tm, options);

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

  // (check-sat)
  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);

  printf("Expect: sat\n");
  printf("Bitwuzla: %s\n\n", bitwuzla_result_to_string(result));

  // Print model in SMT-LIBv2 format.
  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");

  // Print value for x, y, f and a.
  // Note: The returned string of bitwuzla_term_value_get_str is only valid
  //       until the next call to bitwuzla_term_value_get_str
  // 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");
  // 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");
  // Note that the assignment string of bit-vector terms is given as the
  // pure assignment string, either in binary, hexadecimal or decimal format,
  // whereas bitwuzla_term_to_string() prints the value in SMT-LIB2 format
  // (in binary number format).
  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");

  // Query value of bit-vector term that does 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)));

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

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

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/python/options.py.

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a Bitwuzla options instance.
    options = Options()

    # Enable model generation, which expects a boolean configuration value.
    options.set(Option.PRODUCE_MODELS, True)

    # Increase the verbosity level, which expects an integer value.
    print(f'Previous verbosity level: {options.get(Option.VERBOSITY)}')
    options.set(Option.VERBOSITY, 2)
    print(f'Current verbosity level: {options.get(Option.VERBOSITY)}')

    # Now configure an option that has modes (a choice of configuration values).
    # First, query which bit-vector solver engine is set.
    print(f'Default bv solver: {options.get(Option.BV_SOLVER)}')
    # Then, select the propagation-based local search engine as solver engine.
    options.set(Option.BV_SOLVER, 'prop')
    print(f'Current engine: {options.get(Option.BV_SOLVER)}')

    # Now, create a Bitwuzla instance.
    tm = TermManager()
    bitwuzla = Bitwuzla(tm, options)
    # Check sat (nothing to solve, input formula is empty).
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a Bitwuzla options instance.
    options = Options()

    # Enable model generation, which expects a boolean configuration value.
    options.set(Option.PRODUCE_MODELS, True)

    # Increase the verbosity level, which expects an integer value.
    print(f'Previous verbosity level: {options.get(Option.VERBOSITY)}')
    options.set(Option.VERBOSITY, 2)
    print(f'Current verbosity level: {options.get(Option.VERBOSITY)}')

    # Now configure an option that has modes (a choice of configuration values).
    # First, query which bit-vector solver engine is set.
    print(f'Default bv solver: {options.get(Option.BV_SOLVER)}')
    # Then, select the propagation-based local search engine as solver engine.
    options.set(Option.BV_SOLVER, 'prop')
    print(f'Current engine: {options.get(Option.BV_SOLVER)}')

    # Now, create a Bitwuzla instance.
    tm = TermManager()
    bitwuzla = Bitwuzla(tm, options)
    # Check sat (nothing to solve, input formula is empty).
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

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

#include <bitwuzla/c/bitwuzla.h>
#include <inttypes.h>
#include <stdio.h>

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

  // Enable model generation, which expects a boolean configuration value.
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);

  // Increase the verbosity level, which expects an integer value.
  printf("Previous verbosity level: %" PRIu64 "\n",
         bitwuzla_get_option(options, BITWUZLA_OPT_VERBOSITY));
  bitwuzla_set_option(options, BITWUZLA_OPT_VERBOSITY, 2);
  printf("Current verbosity level: %" PRIu64 "\n",
         bitwuzla_get_option(options, BITWUZLA_OPT_VERBOSITY));

  // Now configure an option that has modes (a choice of configuration values).
  // First, query which bit-vector solver engine is set.
  printf("Default bv solver: %s\n",
         bitwuzla_get_option_mode(options, BITWUZLA_OPT_BV_SOLVER));
  // Then, select the propagation-based local search engine as solver engine.
  bitwuzla_set_option_mode(options, BITWUZLA_OPT_BV_SOLVER, "prop");
  printf("Current engine: %s\n",
         bitwuzla_get_option_mode(options, BITWUZLA_OPT_BV_SOLVER));

  // Now, create a Bitwuzla instance.
  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
  // Check sat (nothing to solve, input formula is empty).
  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: sat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

(set-option :verbosity 2)
(set-option :bv-solver "prop")
(set-option :produce-models true)
(set-logic ALL)
(check-sat)

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/python/option_info.py.

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a Bitwuzla options instance.
    options = Options()

    # Set some options to illustrate current vs default value.
    options.set(Option.PRODUCE_MODELS, True)
    options.set(Option.VERBOSITY, 2)
    options.set(Option.BV_SOLVER, 'prop')

    # Then iterate over all available configuration options and extract info.
    for opt in Option:
        info = OptionInfo(options, opt)
        print(f'  long name:   {info.lng()}')
        print(f'  short name:  {info.shrt() if info.shrt() else "-"}')
        print('  kind:        ', end = '')
        if info.kind() == OptionInfoKind.BOOL:
            print('bool')
            print('  values:')
            print(f'  + current:   {info.cur()}')
            print(f'  + default:   {info.dflt()}')
        elif info.kind() == OptionInfoKind.NUMERIC:
            print('numeric')
            print('  values:')
            print(f'  + current:   {info.cur()}')
            print(f'  + default:   {info.dflt()}')
            print(f'  + min:       {info.min()}')
            print(f'  + max:       {info.max()}')
        else:
            print('modes')
            print('  values:')
            print(f'  + current:   {info.cur()}')
            print(f'  + default:   {info.dflt()}')
            print(f'  + modes:     {info.modes()}')
        print(f'  description: {info.description()}\n')

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

#include <bitwuzla/cpp/bitwuzla.h>

#include <iostream>

using namespace bitwuzla;

int
main()
{
  // First, create a Bitwuzla options instance.
  Options options;
  // Set some options to illustrate current vs default value.
  options.set(Option::PRODUCE_MODELS, true);
  options.set(Option::VERBOSITY, 2);
  options.set(Option::BV_SOLVER, "prop");

  // Then iterate over all available configuration options and extract info.
  for (int32_t i = 0; i < static_cast<int32_t>(Option::NUM_OPTS); ++i)
  {
    Option opt = static_cast<Option>(i);
    OptionInfo info(options, opt);
    std::cout << "- long name:   " << info.lng << std::endl;
    std::cout << "  short name:  " << (info.shrt ? info.shrt : "-")
              << std::endl;
    std::cout << "  kind:        ";
    if (info.kind == OptionInfo::Kind::BOOL)
    {
      std::cout << "bool" << std::endl;
      std::cout << "  values:" << std::endl;
      const auto& values = std::get<OptionInfo::Bool>(info.values);
      std::cout << "  + current:   " << (values.cur ? "true" : "false")
                << std::endl;
      std::cout << "  + default:   " << (values.dflt ? "true" : "false")
                << std::endl;
    }
    else if (info.kind == OptionInfo::Kind::NUMERIC)
    {
      std::cout << "numeric" << std::endl;
      std::cout << "  values:" << std::endl;
      const auto& values = std::get<OptionInfo::Numeric>(info.values);
      std::cout << "  + current:   " << values.dflt << std::endl;
      std::cout << "  + default:   " << values.cur << std::endl;
      std::cout << "  + min:       " << values.min << std::endl;
      std::cout << "  + max:       " << values.max << std::endl;
    }
    else
    {
      std::cout << "modes" << std::endl;
      std::cout << "  values:" << std::endl;
      const auto& values = std::get<OptionInfo::Mode>(info.values);
      std::cout << "  + current:   " << values.dflt << std::endl;
      std::cout << "  + default:   " << values.cur << std::endl;
      std::cout << "  + modes:     {";
      for (size_t i = 0, n = values.modes.size(); i < n; ++i)
      {
        std::cout << (i > 0 ? "," : "") << " " << values.modes[i];
      }
      std::cout << " }" << std::endl;
    }
    std::cout << "  description: " << info.description << std::endl;
    std::cout << std::endl;
  }
}

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

#include <bitwuzla/c/bitwuzla.h>
#include <inttypes.h>
#include <stdio.h>

int
main()
{
  // First, create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();
  // Set some options to illustrate current vs default value.
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
  bitwuzla_set_option(options, BITWUZLA_OPT_VERBOSITY, 2);
  bitwuzla_set_option_mode(options, BITWUZLA_OPT_BV_SOLVER, "prop");

  // Then iterate over all available configuration options and extract info.
  BitwuzlaOptionInfo info;
  for (uint32_t i = 0; i < BITWUZLA_OPT_NUM_OPTS; ++i)
  {
    BitwuzlaOption opt = (BitwuzlaOption) i;
    bitwuzla_get_option_info(options, opt, &info);
    printf("- long name:   %s\n", info.lng);
    printf("  short name:  %s\n", (info.shrt ? info.shrt : "-"));
    printf("  kind:        ");
    if (info.is_numeric)
    {
      printf("numeric\n");
      printf("  values:\n");
      printf("  + current:   %" PRIu64 "\n", info.numeric.cur);
      printf("  + default:   %" PRIu64 "\n", info.numeric.dflt);
      printf("  + min:       %" PRIu64 "\n", info.numeric.min);
      printf("  + max:       %" PRIu64 "\n", info.numeric.max);
    }
    else
    {
      printf("modes\n");
      printf("  values:\n");
      printf("  + current:   %s\n", info.mode.cur);
      printf("  + default:   %s\n", info.mode.dflt);
      printf("  + modes:     {");
      for (size_t i = 0, n = info.mode.num_modes; i < n; ++i)
      {
        printf("%s %s", (i > 0 ? "," : ""), info.mode.modes[i]);
      }
      printf(" }\n");
    }
    printf("  description: %s\n\n", info.description);
  }

  // Finally, delete options instance.
  bitwuzla_options_delete(options);
}

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/python/pushpop.py.

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

from bitwuzla import *

if __name__ == "__main__":

    # No options configured, create Bitwuzla instance with default options.
    tm = TermManager()
    bitwuzla = Bitwuzla(tm)

    # Create a bit-vector sort of size 1.
    sortbv1 = tm.mk_bv_sort(1)
    # Create a bit-vector sort of size 2.
    sortbv2 = tm.mk_bv_sort(2)

    # Create bit-vector variables.
    # (declare-const o0 (_ BitVec 1))
    o0 = tm.mk_const(sortbv1, 'o0')
    # (declare-const o1 (_ BitVec 1))
    o1 = tm.mk_const(sortbv1, 'o1')
    # (declare-const s0 (_ BitVec 2))
    s0 = tm.mk_const(sortbv2, 's0')
    # (declare-const s1 (_ BitVec 2))
    s1 = tm.mk_const(sortbv2, 's1')
    # (declare-const s2 (_ BitVec 2))
    s2 = tm.mk_const(sortbv2, 's2')
    # (declare-const goal (_ BitVec 2))
    goal = tm.mk_const(sortbv2, 'goal')

    # Create bit-vector values zero, one, three.
    zero  = tm.mk_bv_zero(sortbv2)
    one1  = tm.mk_bv_one(sortbv1)
    one2  = tm.mk_bv_one(sortbv2)
    three = tm.mk_bv_value(sortbv2, 3)

    # Add some assertions.
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s0, zero]))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [goal, three]))

    # Push, assert, check sat and pop.
    bitwuzla.push(1)
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s0, goal]))
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')
    bitwuzla.pop(1)

    # (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                    [s1,
                                     tm.mk_term(Kind.ITE,
                                             [tm.mk_term(Kind.EQUAL, [o0, one1]),
                                              tm.mk_term(Kind.BV_ADD, [s0, one2]),
                                              s0])]))

    # Push, assert, check sat and pop.
    bitwuzla.push(1)
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s1, goal]))
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')
    bitwuzla.pop(1)

    # (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                    [s2,
                                     tm.mk_term(Kind.ITE,
                                             [tm.mk_term(Kind.EQUAL, [o1, one1]),
                                              tm.mk_term(Kind.BV_ADD, [s1, one2]),
                                              s1])]))

    # Push, assert, check sat and pop.
    bitwuzla.push(1)
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s2, goal]))
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')
    bitwuzla.pop(1)

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

from bitwuzla import *

if __name__ == "__main__":

    # No options configured, create Bitwuzla instance with default options.
    tm = TermManager()
    bitwuzla = Bitwuzla(tm)

    # Create a bit-vector sort of size 1.
    sortbv1 = tm.mk_bv_sort(1)
    # Create a bit-vector sort of size 2.
    sortbv2 = tm.mk_bv_sort(2)

    # Create bit-vector variables.
    # (declare-const o0 (_ BitVec 1))
    o0 = tm.mk_const(sortbv1, 'o0')
    # (declare-const o1 (_ BitVec 1))
    o1 = tm.mk_const(sortbv1, 'o1')
    # (declare-const s0 (_ BitVec 2))
    s0 = tm.mk_const(sortbv2, 's0')
    # (declare-const s1 (_ BitVec 2))
    s1 = tm.mk_const(sortbv2, 's1')
    # (declare-const s2 (_ BitVec 2))
    s2 = tm.mk_const(sortbv2, 's2')
    # (declare-const goal (_ BitVec 2))
    goal = tm.mk_const(sortbv2, 'goal')

    # Create bit-vector values zero, one, three.
    zero  = tm.mk_bv_zero(sortbv2)
    one1  = tm.mk_bv_one(sortbv1)
    one2  = tm.mk_bv_one(sortbv2)
    three = tm.mk_bv_value(sortbv2, 3)

    # Add some assertions.
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s0, zero]))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [goal, three]))

    # Push, assert, check sat and pop.
    bitwuzla.push(1)
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s0, goal]))
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')
    bitwuzla.pop(1)

    # (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                    [s1,
                                     tm.mk_term(Kind.ITE,
                                             [tm.mk_term(Kind.EQUAL, [o0, one1]),
                                              tm.mk_term(Kind.BV_ADD, [s0, one2]),
                                              s0])]))

    # Push, assert, check sat and pop.
    bitwuzla.push(1)
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s1, goal]))
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')
    bitwuzla.pop(1)

    # (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                    [s2,
                                     tm.mk_term(Kind.ITE,
                                             [tm.mk_term(Kind.EQUAL, [o1, one1]),
                                              tm.mk_term(Kind.BV_ADD, [s1, one2]),
                                              s1])]))

    # Push, assert, check sat and pop.
    bitwuzla.push(1)
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s2, goal]))
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')
    bitwuzla.pop(1)

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

#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  // First, create a term manager instance.
  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();
  // Then, create a Bitwuzla instance.
  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);

  // Create a bit-vector sort of size 1.
  BitwuzlaSort sortbv1 = bitwuzla_mk_bv_sort(tm, 1);
  // Create a bit-vector sort of size 2.
  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);

  // Create bit-vector variables.
  // (declare-const o0 (_ BitVec 1))
  BitwuzlaTerm o0 = bitwuzla_mk_const(tm, sortbv1, "o0");
  // (declare-const o1 (_ BitVec 1))
  BitwuzlaTerm o1 = bitwuzla_mk_const(tm, sortbv1, "o1");
  // (declare-const s0 (_ BitVec 2))
  BitwuzlaTerm s0 = bitwuzla_mk_const(tm, sortbv2, "s0");
  // (declare-const s1 (_ BitVec 2))
  BitwuzlaTerm s1 = bitwuzla_mk_const(tm, sortbv2, "s1");
  // (declare-const s2 (_ BitVec 2))
  BitwuzlaTerm s2 = bitwuzla_mk_const(tm, sortbv2, "s2");
  // (declare-const goal (_ BitVec 2))
  BitwuzlaTerm goal = bitwuzla_mk_const(tm, sortbv2, "goal");

  // Create bit-vector values zero, one, three.
  BitwuzlaTerm zero  = bitwuzla_mk_bv_zero(tm, sortbv2);
  BitwuzlaTerm one1  = bitwuzla_mk_bv_one(tm, sortbv1);
  BitwuzlaTerm one2  = bitwuzla_mk_bv_one(tm, sortbv2);
  BitwuzlaTerm three = bitwuzla_mk_bv_value_uint64(tm, sortbv2, 3);

  // Add some assertions.
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, zero));
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, goal, three));

  // Push, assert, check sat and pop.
  bitwuzla_push(bitwuzla, 1);
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, goal));
  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
  bitwuzla_pop(bitwuzla, 1);

  // (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(
                      tm,
                      BITWUZLA_KIND_EQUAL,
                      s1,
                      bitwuzla_mk_term3(
                          tm,
                          BITWUZLA_KIND_ITE,
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o0, one1),
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s0, one2),
                          s0)));

  // Push, assert, check sat and pop.
  bitwuzla_push(bitwuzla, 1);
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s1, goal));
  result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
  bitwuzla_pop(bitwuzla, 1);

  // (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(
                      tm,
                      BITWUZLA_KIND_EQUAL,
                      s2,
                      bitwuzla_mk_term3(
                          tm,
                          BITWUZLA_KIND_ITE,
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o1, one1),
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s1, one2),
                          s1)));

  // Push, assert, check sat and pop.
  bitwuzla_push(bitwuzla, 1);
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s2, goal));
  result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
  bitwuzla_pop(bitwuzla, 1);

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

(set-logic QF_BV)

(declare-fun o0 () (_ BitVec 1))
(declare-fun o1 () (_ BitVec 1))
(declare-fun s0 () (_ BitVec 2))
(declare-fun s1 () (_ BitVec 2))
(declare-fun s2 () (_ BitVec 2))
(declare-fun goal () (_ BitVec 2))

(assert (= s0 (_ bv0 2)))
(assert (= goal (_ bv3 2)))
(push 1)
(assert (= s0 goal))
(check-sat)
(pop 1)

(assert (= s1 (ite (= o0 (_ bv1 1)) (bvadd s0 (_ bv1 2)) s0)))
(push 1)
(assert (= s1 goal))
(check-sat)
(pop 1)

(assert (= s2 (ite (= o1 (_ bv1 1)) (bvadd s1 (_ bv1 2)) s1)))
(push 1)
(assert (= s2 goal))
(check-sat)
(pop 1)

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/python/checksatassuming.py.

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

from bitwuzla import *

if __name__ == "__main__":

    # No options configured, create Bitwuzla instance with default options.
    tm = TermManager()
    bitwuzla = Bitwuzla(tm)

    # Create a bit-vector sort of size 1.
    sortbv1 = tm.mk_bv_sort(1)
    # Create a bit-vector sort of size 2
    sortbv2 = tm.mk_bv_sort(2)

    # Create bit-vector variables.
    # (declare-const o0 (_ BitVec 1))
    o0 = tm.mk_const(sortbv1, 'o0')
    # (declare-const o1 (_ BitVec 1))
    o1 = tm.mk_const(sortbv1, 'o1')
    # (declare-const s0 (_ BitVec 2))
    s0 = tm.mk_const(sortbv2, 's0')
    # (declare-const s1 (_ BitVec 2))
    s1 = tm.mk_const(sortbv2, 's1')
    # (declare-const s2 (_ BitVec 2))
    s2 = tm.mk_const(sortbv2, 's2')
    # (declare-const goal (_ BitVec 2))
    goal = tm.mk_const(sortbv2, 'goal')

    # Create bit-vector values zero, one, three.
    zero  = tm.mk_bv_zero(sortbv2)
    one1  = tm.mk_bv_one(sortbv1)
    one2  = tm.mk_bv_one(sortbv2)
    three = tm.mk_bv_value(sortbv2, 3)

    # Add some assertions.
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s0, zero]))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [goal, three]))

    # (check-sat-assuming ((= s0 goal)))
    result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s0, goal]))
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                    [s1,
                                     tm.mk_term(Kind.ITE,
                                             [tm.mk_term(Kind.EQUAL, [o0, one1]),
                                              tm.mk_term(Kind.BV_ADD, [s0, one2]),
                                              s0])]))

    # (check-sat-assuming ((= s1 goal)))
    result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s1, goal]))
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                     [s2,
                                      tm.mk_term(Kind.ITE,
                                              [tm.mk_term(Kind.EQUAL, [o1, one1]),
                                               tm.mk_term(Kind.BV_ADD, [s1, one2]),
                                               s1])]))

    # (check-sat-assuming ((= s2 goal)))
    result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s2, goal]))
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

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

from bitwuzla import *

if __name__ == "__main__":

    # No options configured, create Bitwuzla instance with default options.
    tm = TermManager()
    bitwuzla = Bitwuzla(tm)

    # Create a bit-vector sort of size 1.
    sortbv1 = tm.mk_bv_sort(1)
    # Create a bit-vector sort of size 2
    sortbv2 = tm.mk_bv_sort(2)

    # Create bit-vector variables.
    # (declare-const o0 (_ BitVec 1))
    o0 = tm.mk_const(sortbv1, 'o0')
    # (declare-const o1 (_ BitVec 1))
    o1 = tm.mk_const(sortbv1, 'o1')
    # (declare-const s0 (_ BitVec 2))
    s0 = tm.mk_const(sortbv2, 's0')
    # (declare-const s1 (_ BitVec 2))
    s1 = tm.mk_const(sortbv2, 's1')
    # (declare-const s2 (_ BitVec 2))
    s2 = tm.mk_const(sortbv2, 's2')
    # (declare-const goal (_ BitVec 2))
    goal = tm.mk_const(sortbv2, 'goal')

    # Create bit-vector values zero, one, three.
    zero  = tm.mk_bv_zero(sortbv2)
    one1  = tm.mk_bv_one(sortbv1)
    one2  = tm.mk_bv_one(sortbv2)
    three = tm.mk_bv_value(sortbv2, 3)

    # Add some assertions.
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s0, zero]))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [goal, three]))

    # (check-sat-assuming ((= s0 goal)))
    result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s0, goal]))
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                    [s1,
                                     tm.mk_term(Kind.ITE,
                                             [tm.mk_term(Kind.EQUAL, [o0, one1]),
                                              tm.mk_term(Kind.BV_ADD, [s0, one2]),
                                              s0])]))

    # (check-sat-assuming ((= s1 goal)))
    result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s1, goal]))
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
                                     [s2,
                                      tm.mk_term(Kind.ITE,
                                              [tm.mk_term(Kind.EQUAL, [o1, one1]),
                                               tm.mk_term(Kind.BV_ADD, [s1, one2]),
                                               s1])]))

    # (check-sat-assuming ((= s2 goal)))
    result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s2, goal]))
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

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

#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  BitwuzlaResult result;

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

  // Create a bit-vector sort of size 1.
  BitwuzlaSort sortbv1 = bitwuzla_mk_bv_sort(tm, 1);
  // Create a bit-vector sort of size 2
  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);

  // Create bit-vector variables.
  // (declare-const o0 (_ BitVec 1))
  BitwuzlaTerm o0 = bitwuzla_mk_const(tm, sortbv1, "o0");
  // (declare-const o1 (_ BitVec 1))
  BitwuzlaTerm o1 = bitwuzla_mk_const(tm, sortbv1, "o1");
  // (declare-const s0 (_ BitVec 2))
  BitwuzlaTerm s0 = bitwuzla_mk_const(tm, sortbv2, "s0");
  // (declare-const s1 (_ BitVec 2))
  BitwuzlaTerm s1 = bitwuzla_mk_const(tm, sortbv2, "s1");
  // (declare-const s2 (_ BitVec 2))
  BitwuzlaTerm s2 = bitwuzla_mk_const(tm, sortbv2, "s2");
  // (declare-const goal (_ BitVec 2))
  BitwuzlaTerm goal = bitwuzla_mk_const(tm, sortbv2, "goal");

  // Create bit-vector values zero, one, three.
  BitwuzlaTerm zero  = bitwuzla_mk_bv_zero(tm, sortbv2);
  BitwuzlaTerm one1  = bitwuzla_mk_bv_one(tm, sortbv1);
  BitwuzlaTerm one2  = bitwuzla_mk_bv_one(tm, sortbv2);
  BitwuzlaTerm three = bitwuzla_mk_bv_value_uint64(tm, sortbv2, 3);

  // Add some assertions.
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, zero));
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, goal, three));

  // (check-sat-assuming ((= s0 goal)))
  BitwuzlaTerm assumptions[1] = {
      bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, goal)};
  result = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(
                      tm,
                      BITWUZLA_KIND_EQUAL,
                      s1,
                      bitwuzla_mk_term3(
                          tm,
                          BITWUZLA_KIND_ITE,
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o0, one1),
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s0, one2),
                          s0)));

  // (check-sat-assuming ((= s1 goal)))
  assumptions[0] = bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s1, goal);
  result         = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(
                      tm,
                      BITWUZLA_KIND_EQUAL,
                      s2,
                      bitwuzla_mk_term3(
                          tm,
                          BITWUZLA_KIND_ITE,
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o1, one1),
                          bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s1, one2),
                          s1)));

  // (check-sat-assuming ((= s2 goal)))
  assumptions[0] = bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s2, goal);
  result         = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

(set-logic QF_BV)

(declare-fun o0 () (_ BitVec 1))
(declare-fun o1 () (_ BitVec 1))
(declare-fun s0 () (_ BitVec 2))
(declare-fun s1 () (_ BitVec 2))
(declare-fun s2 () (_ BitVec 2))
(declare-fun goal () (_ BitVec 2))

(assert (= s0 (_ bv0 2)))
(assert (= goal (_ bv3 2)))
(check-sat-assuming ((= s0 goal)))

(assert (= s1 (ite (= o0 (_ bv1 1)) (bvadd s0 (_ bv1 2)) s0)))
(check-sat-assuming ((= s1 goal)))

(assert (= s2 (ite (= o1 (_ bv1 1)) (bvadd s1 (_ bv1 2)) s1)))
(check-sat-assuming ((= s2 goal)))

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/python/unsatcore.py.

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # Then, enable unsat core extraction.
    # Note: Unsat core extraction is disabled by default.
    options.set(Option.PRODUCE_UNSAT_CORES, True)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create a bit-vector sort of size 2.
    sortbv2 = tm.mk_bv_sort(2)
    # Create a bit-vector sort of size 4.
    sortbv4 = tm.mk_bv_sort(4)
    # Create Float16 floatinf-point sort.
    sortfp16 = tm.mk_fp_sort(5, 11)

    # Create bit-vector variables.
    # (declare-const x0 (_ BitVec 4))
    x0 = tm.mk_const(sortbv4, 'x0')
    # (declare-const x1 (_ BitVec 2))
    x1 = tm.mk_const(sortbv2, 'x1')
    # (declare-const x2 (_ BitVec 2))
    x2 = tm.mk_const(sortbv2, 'x2')
    # (declare-const x3 (_ BitVec 2))
    x3 = tm.mk_const(sortbv2, 'x3')
    # (declare-const x4 Float16)
    x4 = tm.mk_const(sortfp16, 'x4')

    # Create FP positive zero.
    fpzero = tm.mk_fp_pos_zero(sortfp16)
    # Create BV zero of size 4.
    bvzero = tm.mk_bv_zero(sortbv4)

    # (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
    a_f0 = tm.mk_var(sortfp16, 'a_f0')
    f0 = tm.mk_term(Kind.LAMBDA, [a_f0, tm.mk_term(Kind.FP_GT, [a_f0, fpzero])])

    # (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
    a_f1 = tm.mk_var(sortfp16, 'a_f1')
    f1   = tm.mk_term(
        Kind.LAMBDA,
        [a_f1,
           tm.mk_term(Kind.ITE, [tm.mk_term(Kind.APPLY, [f0, a_f1]), x0, bvzero])])

    # (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
    a_f2 = tm.mk_var(sortfp16, 'a_f2')
    f2   = tm.mk_term(
        Kind.LAMBDA,
        [a_f2,
           tm.mk_term(Kind.BV_EXTRACT, [tm.mk_term(Kind.APPLY, [f1, a_f2])], [1, 0])])

    # (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
    a0 = tm.mk_term(Kind.BV_ULT, [x2, tm.mk_term(Kind.APPLY, [f2, fpzero])])
    bitwuzla.assert_formula(a0)

    # (assert (! (= x1 x2 x3) :named a1))
    a1 = tm.mk_term(Kind.EQUAL, [x1, x2, x3])
    bitwuzla.assert_formula(a1)

    # (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
    a2 = tm.mk_term(Kind.EQUAL,
                      [x4,
                       tm.mk_term(Kind.FP_TO_FP_FROM_UBV,
                               [tm.mk_rm_value(RoundingMode.RNE), x3],
                               [5, 11])])
    bitwuzla.assert_formula(a2)

    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (get-unsat-core)
    unsat_core = bitwuzla.get_unsat_core()
    print('Unsat Core:')
    print('{')
    for t in unsat_core:
        print(f' {t}')
    print('}')

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # Then, enable unsat core extraction.
    # Note: Unsat core extraction is disabled by default.
    options.set(Option.PRODUCE_UNSAT_CORES, True)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create a bit-vector sort of size 2.
    sortbv2 = tm.mk_bv_sort(2)
    # Create a bit-vector sort of size 4.
    sortbv4 = tm.mk_bv_sort(4)
    # Create Float16 floatinf-point sort.
    sortfp16 = tm.mk_fp_sort(5, 11)

    # Create bit-vector variables.
    # (declare-const x0 (_ BitVec 4))
    x0 = tm.mk_const(sortbv4, 'x0')
    # (declare-const x1 (_ BitVec 2))
    x1 = tm.mk_const(sortbv2, 'x1')
    # (declare-const x2 (_ BitVec 2))
    x2 = tm.mk_const(sortbv2, 'x2')
    # (declare-const x3 (_ BitVec 2))
    x3 = tm.mk_const(sortbv2, 'x3')
    # (declare-const x4 Float16)
    x4 = tm.mk_const(sortfp16, 'x4')

    # Create FP positive zero.
    fpzero = tm.mk_fp_pos_zero(sortfp16)
    # Create BV zero of size 4.
    bvzero = tm.mk_bv_zero(sortbv4)

    # (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
    a_f0 = tm.mk_var(sortfp16, 'a_f0')
    f0 = tm.mk_term(Kind.LAMBDA, [a_f0, tm.mk_term(Kind.FP_GT, [a_f0, fpzero])])

    # (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
    a_f1 = tm.mk_var(sortfp16, 'a_f1')
    f1   = tm.mk_term(
        Kind.LAMBDA,
        [a_f1,
           tm.mk_term(Kind.ITE, [tm.mk_term(Kind.APPLY, [f0, a_f1]), x0, bvzero])])

    # (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
    a_f2 = tm.mk_var(sortfp16, 'a_f2')
    f2   = tm.mk_term(
        Kind.LAMBDA,
        [a_f2,
           tm.mk_term(Kind.BV_EXTRACT, [tm.mk_term(Kind.APPLY, [f1, a_f2])], [1, 0])])

    # (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
    a0 = tm.mk_term(Kind.BV_ULT, [x2, tm.mk_term(Kind.APPLY, [f2, fpzero])])
    bitwuzla.assert_formula(a0)

    # (assert (! (= x1 x2 x3) :named a1))
    a1 = tm.mk_term(Kind.EQUAL, [x1, x2, x3])
    bitwuzla.assert_formula(a1)

    # (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
    a2 = tm.mk_term(Kind.EQUAL,
                      [x4,
                       tm.mk_term(Kind.FP_TO_FP_FROM_UBV,
                               [tm.mk_rm_value(RoundingMode.RNE), x3],
                               [5, 11])])
    bitwuzla.assert_formula(a2)

    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (get-unsat-core)
    unsat_core = bitwuzla.get_unsat_core()
    print('Unsat Core:')
    print('{')
    for t in unsat_core:
        print(f' {t}')
    print('}')

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

#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  // First, create a term manager instance.
  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions *options = bitwuzla_options_new();
  // Then, enable unsat core extraction.
  // Note: Unsat core extraction is disabled by default.
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_UNSAT_CORES, 1);
  // Then, create a Bitwuzla instance.
  Bitwuzla *bitwuzla = bitwuzla_new(tm, options);

  // Create a bit-vector sort of size 2.
  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
  // Create a bit-vector sort of size 4.
  BitwuzlaSort sortbv4 = bitwuzla_mk_bv_sort(tm, 4);
  // Create Float16 floatinf-point sort.
  BitwuzlaSort sortfp16 = bitwuzla_mk_fp_sort(tm, 5, 11);

  // Create bit-vector variables.
  // (declare-const x0 (_ BitVec 4))
  BitwuzlaTerm x0 = bitwuzla_mk_const(tm, sortbv4, "x0");
  // (declare-const x1 (_ BitVec 2))
  BitwuzlaTerm x1 = bitwuzla_mk_const(tm, sortbv2, "x1");
  // (declare-const x2 (_ BitVec 2))
  BitwuzlaTerm x2 = bitwuzla_mk_const(tm, sortbv2, "x2");
  // (declare-const x3 (_ BitVec 2))
  BitwuzlaTerm x3 = bitwuzla_mk_const(tm, sortbv2, "x3");
  // (declare-const x4 Float16)
  BitwuzlaTerm x4 = bitwuzla_mk_const(tm, sortfp16, "x4");

  // Create FP positive zero.
  BitwuzlaTerm fpzero = bitwuzla_mk_fp_pos_zero(tm, sortfp16);
  // Create BV zero of size 4.
  BitwuzlaTerm bvzero = bitwuzla_mk_bv_zero(tm, sortbv4);

  // (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
  BitwuzlaTerm a_f0 = bitwuzla_mk_var(tm, sortfp16, "a_f0");
  BitwuzlaTerm f0   = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_LAMBDA,
      a_f0,
      bitwuzla_mk_term2(tm, BITWUZLA_KIND_FP_GT, a_f0, fpzero));

  // (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
  BitwuzlaTerm a_f1 = bitwuzla_mk_var(tm, sortfp16, "a_f1");
  BitwuzlaTerm f1   = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_LAMBDA,
      a_f1,
      bitwuzla_mk_term3(tm,
                        BITWUZLA_KIND_ITE,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f0, a_f1),
                        x0,
                        bvzero));

  // (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
  BitwuzlaTerm a_f2 = bitwuzla_mk_var(tm, sortfp16, "a_f2");
  BitwuzlaTerm f2   = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_LAMBDA,
      a_f2,
      bitwuzla_mk_term1_indexed2(
          tm,
          BITWUZLA_KIND_BV_EXTRACT,
          bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f1, a_f2),
          1,
          0));

  // (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
  BitwuzlaTerm a0 =
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_BV_ULT,
                        x2,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f2, fpzero));
  bitwuzla_assert(bitwuzla, a0);

  // (assert (! (= x1 x2 x3) :named a1))
  BitwuzlaTerm a1 = bitwuzla_mk_term3(tm, BITWUZLA_KIND_EQUAL, x1, x2, x3);
  bitwuzla_assert(bitwuzla, a1);

  // (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
  BitwuzlaTerm a2 = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_EQUAL,
      x4,
      bitwuzla_mk_term2_indexed2(tm,
                                 BITWUZLA_KIND_FP_TO_FP_FROM_UBV,
                                 bitwuzla_mk_rm_value(tm, BITWUZLA_RM_RNE),
                                 x3,
                                 5,
                                 11));
  bitwuzla_assert(bitwuzla, a2);

  // (check-sat)
  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // (get-unsat-core)
  size_t unsat_core_size;
  BitwuzlaTerm *unsat_core =
      bitwuzla_get_unsat_core(bitwuzla, &unsat_core_size);
  printf("Unsat Core:\n{\n");
  for (uint32_t i = 0; i < unsat_core_size; ++i)
  {
    printf(" %s\n", bitwuzla_term_to_string(unsat_core[i]));
  }
  printf("}\n");

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

(set-logic ALL)
(set-option :produce-unsat-cores true)
(declare-const x0 (_ BitVec 4))
(declare-const x1 (_ BitVec 2))
(declare-const x2 (_ BitVec 2))
(declare-const x3 (_ BitVec 2))
(declare-const x4 Float16)
(define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
(define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
(define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
(assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
(assert (! (= x1 x2 x3) :named a1))
(assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
(check-sat)
(get-unsat-core)

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/python/unsatassumptions.py.

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # (set-option :produce-unsat-assumptions true)
    options.set(Option.PRODUCE_UNSAT_ASSUMPTIONS, True)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create Boolean sort.
    sortbool = tm.mk_bool_sort()
    # Create a bit-vector sort of size 2.
    sortbv2 = tm.mk_bv_sort(2)
    # Create a bit-vector sort of size 4.
    sortbv4 = tm.mk_bv_sort(4)
    # Create Float16 floatinf-point sort.
    sortfp16 = tm.mk_fp_sort(5, 11)
    # Create bit-vector variables.
    # (declare-const x0 (_ BitVec 4))
    x0 = tm.mk_const(sortbv4, 'x0')
    # (declare-const x1 (_ BitVec 2))
    x1 = tm.mk_const(sortbv2, 'x1')
    # (declare-const x2 (_ BitVec 2))
    x2 = tm.mk_const(sortbv2, 'x2')
    # (declare-const x3 (_ BitVec 2))
    x3 = tm.mk_const(sortbv2, 'x3')
    # (declare-const x4 Float16)
    x4 = tm.mk_const(sortfp16, 'x4')

    # Create FP positive zero.
    fpzero = tm.mk_fp_pos_zero(sortfp16)
    # Create BV zero of size 4.
    bvzero = tm.mk_bv_zero(sortbv4)

    # (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
    a_f0 = tm.mk_var(sortfp16, 'a_f0')
    f0 = tm.mk_term(Kind.LAMBDA, [a_f0, tm.mk_term(Kind.FP_GT, [a_f0, fpzero])])

    # (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
    a_f1 = tm.mk_var(sortfp16, 'a_f1')
    f1   = tm.mk_term(
        Kind.LAMBDA,
        [a_f1,
           tm.mk_term(Kind.ITE, [tm.mk_term(Kind.APPLY, [f0, a_f1]), x0, bvzero])])

    # (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
    a_f2 = tm.mk_var(sortfp16, 'a_f2')
    f2   = tm.mk_term(
        Kind.LAMBDA,
        [a_f2,
           tm.mk_term(Kind.BV_EXTRACT, [tm.mk_term(Kind.APPLY, [f1, a_f2])], [1, 0])])

    # (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
    a0 = tm.mk_const(sortbool, 'a0')
    assumption0 = tm.mk_term(Kind.BV_ULT, [x2, tm.mk_term(Kind.APPLY, [f2, fpzero])])
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [a0, assumption0]))
    # (assert (! (= x1 x2 x3) :named a1))
    a1          = tm.mk_const(sortbool, 'a1')
    assumption1 = tm.mk_term(Kind.EQUAL, [x1, x2, x3])
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [a1, assumption1]))
    # (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
    a2          = tm.mk_const(sortbool, 'a2')
    assumption2 = tm.mk_term(Kind.EQUAL,
                               [x4,
                                tm.mk_term(Kind.FP_TO_FP_FROM_UBV,
                                        [tm.mk_rm_value(RoundingMode.RNE), x3],
                                        [5, 11])])
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [a2, assumption2]))

    # (check-sat-assuming (assumption0 assumption1 assumption2))
    result = bitwuzla.check_sat(a0, a1, a2)
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (get-unsat-assumptions)
    unsat_assumptions = bitwuzla.get_unsat_assumptions()
    print('Unsat Assumptions: {', end = '')
    for a in unsat_assumptions:
        print(f' {a}', end = '')
    print(' }')

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # (set-option :produce-unsat-assumptions true)
    options.set(Option.PRODUCE_UNSAT_ASSUMPTIONS, True)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create Boolean sort.
    sortbool = tm.mk_bool_sort()
    # Create a bit-vector sort of size 2.
    sortbv2 = tm.mk_bv_sort(2)
    # Create a bit-vector sort of size 4.
    sortbv4 = tm.mk_bv_sort(4)
    # Create Float16 floatinf-point sort.
    sortfp16 = tm.mk_fp_sort(5, 11)
    # Create bit-vector variables.
    # (declare-const x0 (_ BitVec 4))
    x0 = tm.mk_const(sortbv4, 'x0')
    # (declare-const x1 (_ BitVec 2))
    x1 = tm.mk_const(sortbv2, 'x1')
    # (declare-const x2 (_ BitVec 2))
    x2 = tm.mk_const(sortbv2, 'x2')
    # (declare-const x3 (_ BitVec 2))
    x3 = tm.mk_const(sortbv2, 'x3')
    # (declare-const x4 Float16)
    x4 = tm.mk_const(sortfp16, 'x4')

    # Create FP positive zero.
    fpzero = tm.mk_fp_pos_zero(sortfp16)
    # Create BV zero of size 4.
    bvzero = tm.mk_bv_zero(sortbv4)

    # (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
    a_f0 = tm.mk_var(sortfp16, 'a_f0')
    f0 = tm.mk_term(Kind.LAMBDA, [a_f0, tm.mk_term(Kind.FP_GT, [a_f0, fpzero])])

    # (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
    a_f1 = tm.mk_var(sortfp16, 'a_f1')
    f1   = tm.mk_term(
        Kind.LAMBDA,
        [a_f1,
           tm.mk_term(Kind.ITE, [tm.mk_term(Kind.APPLY, [f0, a_f1]), x0, bvzero])])

    # (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
    a_f2 = tm.mk_var(sortfp16, 'a_f2')
    f2   = tm.mk_term(
        Kind.LAMBDA,
        [a_f2,
           tm.mk_term(Kind.BV_EXTRACT, [tm.mk_term(Kind.APPLY, [f1, a_f2])], [1, 0])])

    # (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
    a0 = tm.mk_const(sortbool, 'a0')
    assumption0 = tm.mk_term(Kind.BV_ULT, [x2, tm.mk_term(Kind.APPLY, [f2, fpzero])])
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [a0, assumption0]))
    # (assert (! (= x1 x2 x3) :named a1))
    a1          = tm.mk_const(sortbool, 'a1')
    assumption1 = tm.mk_term(Kind.EQUAL, [x1, x2, x3])
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [a1, assumption1]))
    # (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
    a2          = tm.mk_const(sortbool, 'a2')
    assumption2 = tm.mk_term(Kind.EQUAL,
                               [x4,
                                tm.mk_term(Kind.FP_TO_FP_FROM_UBV,
                                        [tm.mk_rm_value(RoundingMode.RNE), x3],
                                        [5, 11])])
    bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [a2, assumption2]))

    # (check-sat-assuming (assumption0 assumption1 assumption2))
    result = bitwuzla.check_sat(a0, a1, a2)
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (get-unsat-assumptions)
    unsat_assumptions = bitwuzla.get_unsat_assumptions()
    print('Unsat Assumptions: {', end = '')
    for a in unsat_assumptions:
        print(f' {a}', end = '')
    print(' }')

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

#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  // First, create a term manager instance.
  BitwuzlaTermManager *tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions *options = bitwuzla_options_new();
  // (set-option :produce-unsat-assumptions true)
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS, 1);
  // Then, create a Bitwuzla instance.
  Bitwuzla *bitwuzla = bitwuzla_new(tm, options);

  // Create Boolean sort.
  BitwuzlaSort sortbool = bitwuzla_mk_bool_sort(tm);
  // Create a bit-vector sort of size 2.
  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
  // Create a bit-vector sort of size 4.
  BitwuzlaSort sortbv4 = bitwuzla_mk_bv_sort(tm, 4);
  // Create Float16 floatinf-point sort.
  BitwuzlaSort sortfp16 = bitwuzla_mk_fp_sort(tm, 5, 11);
  // Create bit-vector variables.
  // (declare-const x0 (_ BitVec 4))
  BitwuzlaTerm x0 = bitwuzla_mk_const(tm, sortbv4, "x0");
  // (declare-const x1 (_ BitVec 2))
  BitwuzlaTerm x1 = bitwuzla_mk_const(tm, sortbv2, "x1");
  // (declare-const x2 (_ BitVec 2))
  BitwuzlaTerm x2 = bitwuzla_mk_const(tm, sortbv2, "x2");
  // (declare-const x3 (_ BitVec 2))
  BitwuzlaTerm x3 = bitwuzla_mk_const(tm, sortbv2, "x3");
  // (declare-const x4 Float16)
  BitwuzlaTerm x4 = bitwuzla_mk_const(tm, sortfp16, "x4");

  // Create FP positive zero.
  BitwuzlaTerm fpzero = bitwuzla_mk_fp_pos_zero(tm, sortfp16);
  // Create BV zero of size 4.
  BitwuzlaTerm bvzero = bitwuzla_mk_bv_zero(tm, sortbv4);

  // (define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
  BitwuzlaTerm a_f0 = bitwuzla_mk_var(tm, sortfp16, "a_f0");
  BitwuzlaTerm f0   = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_LAMBDA,
      a_f0,
      bitwuzla_mk_term2(tm, BITWUZLA_KIND_FP_GT, a_f0, fpzero));

  // (define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
  BitwuzlaTerm a_f1 = bitwuzla_mk_var(tm, sortfp16, "a_f1");
  BitwuzlaTerm f1   = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_LAMBDA,
      a_f1,
      bitwuzla_mk_term3(tm,
                        BITWUZLA_KIND_ITE,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f0, a_f1),
                        x0,
                        bvzero));

  // (define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
  BitwuzlaTerm a_f2 = bitwuzla_mk_var(tm, sortfp16, "a_f2");
  BitwuzlaTerm f2   = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_LAMBDA,
      a_f2,
      bitwuzla_mk_term1_indexed2(
          tm,
          BITWUZLA_KIND_BV_EXTRACT,
          bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f1, a_f2),
          1,
          0));

  // (assert (! (bvult x2 (f2 (_ +zero 5 11))) :named a0))
  BitwuzlaTerm a0 = bitwuzla_mk_const(tm, sortbool, "a0");
  BitwuzlaTerm assumption0 =
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_BV_ULT,
                        x2,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, f2, fpzero));
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, a0, assumption0));
  // (assert (! (= x1 x2 x3) :named a1))
  BitwuzlaTerm a1 = bitwuzla_mk_const(tm, sortbool, "a1");
  BitwuzlaTerm assumption1 =
      bitwuzla_mk_term3(tm, BITWUZLA_KIND_EQUAL, x1, x2, x3);
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, a1, assumption1));
  // (assert (!(= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2))
  BitwuzlaTerm a2          = bitwuzla_mk_const(tm, sortbool, "a2");
  BitwuzlaTerm assumption2 = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_EQUAL,
      x4,
      bitwuzla_mk_term2_indexed2(tm,
                                 BITWUZLA_KIND_FP_TO_FP_FROM_UBV,
                                 bitwuzla_mk_rm_value(tm, BITWUZLA_RM_RNE),
                                 x3,
                                 5,
                                 11));
  bitwuzla_assert(bitwuzla,
                  bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, a2, assumption2));

  BitwuzlaTerm assumptions[3] = {a0, a1, a2};
  // (check-sat-assuming (assumption0 assumption1 assumption2))
  BitwuzlaResult result = bitwuzla_check_sat_assuming(bitwuzla, 3, assumptions);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // (get-unsat-assumptions)
  size_t unsat_assumptions_size;
  BitwuzlaTerm *unsat_assumptions =
      bitwuzla_get_unsat_assumptions(bitwuzla, &unsat_assumptions_size);
  printf("Unsat Assumptions: {");
  for (uint32_t i = 0; i < unsat_assumptions_size; ++i)
  {
    printf(" %s", bitwuzla_term_to_string(unsat_assumptions[i]));
  }
  printf(" }\n");

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

(set-logic ALL)
(set-option :produce-unsat-assumptions true)
(declare-const x0 (_ BitVec 4))
(declare-const x1 (_ BitVec 2))
(declare-const x2 (_ BitVec 2))
(declare-const x3 (_ BitVec 2))
(declare-const x4 Float16)
(define-fun f0 ((a Float16)) Bool (fp.gt a (_ +zero 5 11)))
(define-fun f1 ((a Float16)) (_ BitVec 4) (ite (f0 a) x0 #b0000))
(define-fun f2 ((a Float16)) (_ BitVec 2) ((_ extract 1 0) (f1 a)))
(check-sat-assuming
  (
   (! (bvult x2 (f2 (_ +zero 5 11))) :named a0)
   (! (= x1 x2 x3) :named a1)
   (! (= x4 ((_ to_fp_unsigned 5 11) RNE x3)) :named a2)
  )
)
(get-unsat-assumptions)

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/python/reset.py.

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # (set-option :produce-models true)
    options.set(Option.PRODUCE_MODELS, False)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create a bit-vector sort of size 3.
    sortbv3 = tm.mk_bv_sort(3)

    # (declare-const x (_ BitVec 3))
    x = tm.mk_const(sortbv3, 'x')

    # (assert (= x #b010))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 2)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # (set-option :produce-models true)
    options.set(Option.PRODUCE_MODELS, True)

    # (reset)
    # Note: Bitwuzla does not provide an explicit API function for reset since
    #       this is achieved by simply discarding the current Bitwuzla instance
    #       and creating a new one.
    bitwuzla = Bitwuzla(tm, options)

    # (declare-const a ( Array (_ BitVec 2) (_ BitVec 3)))
    sortbv2 = tm.mk_bv_sort(2)
    a       = tm.mk_const(tm.mk_array_sort(sortbv2, sortbv3), 'a')

    # (assert (= x #b011))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 3)]))
    # (assert (= x (select a #b01)))
    bitwuzla.assert_formula(tm.mk_term(
        Kind.EQUAL,
        [x, tm.mk_term(Kind.ARRAY_SELECT, [a, tm.mk_bv_value(sortbv2, 1)])]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')
    # (get-model)
    print('(')
    print(f'  (define-fun {x.symbol()} () {x.sort()} {bitwuzla.get_value(x)} )')
    print(f'  (define-fun {a.symbol()} () {a.sort()} {bitwuzla.get_value(a)} )')
    print(')')

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # (set-option :produce-models true)
    options.set(Option.PRODUCE_MODELS, False)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create a bit-vector sort of size 3.
    sortbv3 = tm.mk_bv_sort(3)

    # (declare-const x (_ BitVec 3))
    x = tm.mk_const(sortbv3, 'x')

    # (assert (= x #b010))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 2)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # (set-option :produce-models true)
    options.set(Option.PRODUCE_MODELS, True)

    # (reset)
    # Note: Bitwuzla does not provide an explicit API function for reset since
    #       this is achieved by simply discarding the current Bitwuzla instance
    #       and creating a new one.
    bitwuzla = Bitwuzla(tm, options)

    # (declare-const a ( Array (_ BitVec 2) (_ BitVec 3)))
    sortbv2 = tm.mk_bv_sort(2)
    a       = tm.mk_const(tm.mk_array_sort(sortbv2, sortbv3), 'a')

    # (assert (= x #b011))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 3)]))
    # (assert (= x (select a #b01)))
    bitwuzla.assert_formula(tm.mk_term(
        Kind.EQUAL,
        [x, tm.mk_term(Kind.ARRAY_SELECT, [a, tm.mk_bv_value(sortbv2, 1)])]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')
    # (get-model)
    print('(')
    print(f'  (define-fun {x.symbol()} () {x.sort()} {bitwuzla.get_value(x)} )')
    print(f'  (define-fun {a.symbol()} () {a.sort()} {bitwuzla.get_value(a)} )')
    print(')')

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

#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  BitwuzlaResult result;

  // First, create a term manager instance.
  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();
  // (set-option :produce-models false)
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 0);

  // Then, create a Bitwuzla instance.
  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);

  // Create a bit-vector sort of size 3.
  BitwuzlaSort sortbv3 = bitwuzla_mk_bv_sort(tm, 3);

  // (declare-const x (_ BitVec 3))
  BitwuzlaTerm x = bitwuzla_mk_const(tm, sortbv3, "x");

  // (assert (= x #b010))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        x,
                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 2)));
  // (check-sat)
  result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: sat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  bitwuzla_delete(bitwuzla);

  // (set-option :produce-models true)
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, true);

  // (reset)
  // Note: Bitwuzla does not provide an explicit API function for reset since
  //       this is achieved by simply discarding the current Bitwuzla instance
  //       and creating a new one.
  bitwuzla = bitwuzla_new(tm, options);

  // (declare-const a ( Array (_ BitVec 2) (_ BitVec 3)))
  BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
  BitwuzlaTerm a =
      bitwuzla_mk_const(tm, bitwuzla_mk_array_sort(tm, sortbv2, sortbv3), "a");

  // (assert (= x #b011))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        x,
                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 3)));
  // (assert (= x (select a #b01)))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(
          tm,
          BITWUZLA_KIND_EQUAL,
          x,
          bitwuzla_mk_term2(tm,
                            BITWUZLA_KIND_ARRAY_SELECT,
                            a,
                            bitwuzla_mk_bv_value_uint64(tm, sortbv2, 1))));
  // (check-sat)
  result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: sat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
  // (get-model)
  printf("(\n");
  printf("  (define-fun %s () ", bitwuzla_term_get_symbol(x));
  printf("%s ", bitwuzla_sort_to_string(bitwuzla_term_get_sort(x)));
  printf("%s)\n", bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, x)));
  printf("  (define-fun %s () ", bitwuzla_term_get_symbol(a));
  printf("%s ", bitwuzla_sort_to_string(bitwuzla_term_get_sort(a)));
  printf("%s)\n", bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, a)));
  printf(")\n");

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

(set-logic QF_BV)
(set-option :produce-models false)
(declare-const x (_ BitVec 3))
(assert (= x #b010))
(check-sat) ; expect sat

(reset)

(set-logic QF_ABV)
(set-option :produce-models true)
(declare-const x (_ BitVec 3))
(declare-const a ( Array (_ BitVec 2) (_ BitVec 3)))
(assert (= x #b011))
(assert (= x (select a #b01)))
(check-sat) ; expect sat
(get-model)

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/python/reset_assertions.py.

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # (set-option :produce-models true)
    options.set(Option.PRODUCE_MODELS, True)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create a bit-vector sort of size 3.
    sortbv3 = tm.mk_bv_sort(3)

    # (declare-const x (_ BitVec 3))
    x = tm.mk_const(sortbv3, 'x')

    # (assert (= x #b010))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 2)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # (assert (= x #b001))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 1)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (reset-assertions)
    # Note: Bitwuzla does not provide an explicit API function for
    #       reset-assertions since this is achieved by simply discarding
    #       the current Bitwuzla instance and creating a new one.
    bitwuzla = Bitwuzla(tm, options)

    # (assert (= x #b011))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 3)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # (get-model)
    print(f'(\n (define-fun {x.symbol()} () {x.sort()} {bitwuzla.get_value(x)} )\n)')

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

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    # (set-option :produce-models true)
    options.set(Option.PRODUCE_MODELS, True)

    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)

    # Create a bit-vector sort of size 3.
    sortbv3 = tm.mk_bv_sort(3)

    # (declare-const x (_ BitVec 3))
    x = tm.mk_const(sortbv3, 'x')

    # (assert (= x #b010))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 2)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # (assert (= x #b001))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 1)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: unsat')
    print(f'Bitwuzla: {result}')

    # (reset-assertions)
    # Note: Bitwuzla does not provide an explicit API function for
    #       reset-assertions since this is achieved by simply discarding
    #       the current Bitwuzla instance and creating a new one.
    bitwuzla = Bitwuzla(tm, options)

    # (assert (= x #b011))
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [x, tm.mk_bv_value(sortbv3, 3)]))
    # (check-sat)
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')

    # (get-model)
    print(f'(\n (define-fun {x.symbol()} () {x.sort()} {bitwuzla.get_value(x)} )\n)')

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

#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  BitwuzlaResult result;

  // First, create a term manager instance.
  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();
  // (set-option :produce-models true)
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);

  // Then, create a Bitwuzla instance.
  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);

  // Create a bit-vector sort of size 3.
  BitwuzlaSort sortbv3 = bitwuzla_mk_bv_sort(tm, 3);

  // (declare-const x (_ BitVec 3))
  BitwuzlaTerm x = bitwuzla_mk_const(tm, sortbv3, "x");

  // (assert (= x #b010))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        x,
                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 2)));
  // (check-sat)
  result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: sat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
  // (assert (= x #b001))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        x,
                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 1)));
  // (check-sat)
  result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // (reset-assertions)
  // Note: Bitwuzla does not provide an explicit API function for
  //       reset-assertions since this is achieved by simply discarding
  //       the current Bitwuzla instance and creating a new one.
  bitwuzla_delete(bitwuzla);
  bitwuzla = bitwuzla_new(tm, options);

  // (assert (= x #b011))
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        x,
                        bitwuzla_mk_bv_value_uint64(tm, sortbv3, 3)));
  // (check-sat)
  result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: sat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
  // (get-model)
  printf("(\n");
  printf("  (define-fun %s", bitwuzla_term_get_symbol(x));
  printf(" () %s", bitwuzla_sort_to_string(bitwuzla_term_get_sort(x)));
  printf(" %s)\n", bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, x)));
  printf(")\n");

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

(set-logic QF_BV)
(set-option :global-declarations true)
(set-option :produce-models true)
(declare-const x (_ BitVec 3))
(assert (= x #b010))
(check-sat) ; expect sat
(assert (= x #b001))
(check-sat) ; expect unsat

(reset-assertions)

(assert (= x #b011))
(check-sat) ; expect sat
(get-model)

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/python/parse.py.

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

import sys

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()

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

    # Now parse the input file.
    print('Expect: sat')
    print('Bitwuzla: ', end='')
    sys.stdout.flush()
    res = parser.parse("../smt2/quickstart.smt2")
    # We expect no error to occur.
    assert not res

    # Now we retrieve the set of asserted formulas and print them.
    assertions = parser.bitwuzla().get_assertions()
    print('Assertions:')
    print('{')
    for a in assertions:
        print(f' {a}')
    print('}')

    # Now we add an assertion via parsing from string.
    parser.parse('(assert (distinct (select a x) y))', True, False)
    # Now the formula is unsat.
    print('Expect: unsat')
    print(f'Bitwuzla: {parser.bitwuzla().check_sat()}')

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

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

    # Declare Boolean constants 'c' and 'd'.
    # Note: Declarations are commands (not terms) in the SMT-LIB language.
    #       Commands must be parsed in via Parser.parse(),
    #       Parser::parse_term() only supports parsing SMT-LIB terms.
    parser.parse("(declare-const c Bool)(declare-const d Bool)", True, False)
    # Declare bit-vector constant 'b'.
    parser.parse('(declare-const b (_ BitVec 16))', True, False)
    # Retrieve term representing 'b'.
    b = parser.parse_term('b')
    # Retrieve term representing 'c'.
    c = parser.parse_term('c')
    # Retrieve term representing 'd'.
    d = parser.parse_term('d')
    # Create xor over 'c' and 'd' and show that it corresponds to term
    # parsed in from its string representation '(xor c d)'.
    assert parser.parse_term('(xor c d)') == tm.mk_term(Kind.XOR, [c, d])
    # Create bit-vector addition over 'b' and bit-vector value
    # '1011111010001010' and show that it corresponds to the term parsed in
    # from its string representation '(bvadd b #b1011111010001010)'.
    assert parser.parse_term('(bvadd b #b1011111010001010)') \
           == tm.mk_term(Kind.BV_ADD,
                      [b, tm.mk_bv_value(bv16, '1011111010001010', 2)])

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

import sys

from bitwuzla import *

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()

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

    # Now parse the input file.
    print('Expect: sat')
    print('Bitwuzla: ', end='')
    sys.stdout.flush()
    res = parser.parse("../smt2/quickstart.smt2")
    # We expect no error to occur.
    assert not res

    # Now we retrieve the set of asserted formulas and print them.
    assertions = parser.bitwuzla().get_assertions()
    print('Assertions:')
    print('{')
    for a in assertions:
        print(f' {a}')
    print('}')

    # Now we add an assertion via parsing from string.
    parser.parse('(assert (distinct (select a x) y))', True, False)
    # Now the formula is unsat.
    print('Expect: unsat')
    print(f'Bitwuzla: {parser.bitwuzla().check_sat()}')

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

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

    # Declare Boolean constants 'c' and 'd'.
    # Note: Declarations are commands (not terms) in the SMT-LIB language.
    #       Commands must be parsed in via Parser.parse(),
    #       Parser::parse_term() only supports parsing SMT-LIB terms.
    parser.parse("(declare-const c Bool)(declare-const d Bool)", True, False)
    # Declare bit-vector constant 'b'.
    parser.parse('(declare-const b (_ BitVec 16))', True, False)
    # Retrieve term representing 'b'.
    b = parser.parse_term('b')
    # Retrieve term representing 'c'.
    c = parser.parse_term('c')
    # Retrieve term representing 'd'.
    d = parser.parse_term('d')
    # Create xor over 'c' and 'd' and show that it corresponds to term
    # parsed in from its string representation '(xor c d)'.
    assert parser.parse_term('(xor c d)') == tm.mk_term(Kind.XOR, [c, d])
    # Create bit-vector addition over 'b' and bit-vector value
    # '1011111010001010' and show that it corresponds to the term parsed in
    # from its string representation '(bvadd b #b1011111010001010)'.
    assert parser.parse_term('(bvadd b #b1011111010001010)') \
           == tm.mk_term(Kind.BV_ADD,
                      [b, tm.mk_bv_value(bv16, '1011111010001010', 2)])

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

#include <assert.h>
#include <bitwuzla/c/bitwuzla.h>
#include <bitwuzla/c/parser.h>
#include <stdlib.h>

int
main()
{
  // 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>");

  // Now parse the input file.
  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);

  // Now we retrieve the set of asserted formulas and print them.
  size_t size;
  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");

  // Now we add an assertion via parsing from string.
  bitwuzla_parser_parse(
      parser, "(assert (distinct (select a x) y))", true, false, &error_msg);
  // We expect no error to occur.
  assert(!error_msg);
  // Now the formula is unsat.
  BitwuzlaResult result =
      bitwuzla_check_sat(bitwuzla_parser_get_bitwuzla(parser));

  printf("Expect: unsat\n");
  printf("Bitwuzla: %s\n\n", bitwuzla_result_to_string(result));

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

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

  // Declare Boolean constants 'c' and 'd'.
  // Note: Declarations are commands (not terms) in the SMT-LIB language.
  //       Commands must be parsed in via bitwuzla_parser_parse(),
  //       bitwuzla_parser_parse_term() only supports parsing SMT-LIB terms.
  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);
  // 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);
  // 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,
             bitwuzla_mk_bv_value(tm, bv16, "1011111010001010", 2)));
  // Finally, delete Bitwuzla parser, options, and term manager instance.
  bitwuzla_parser_delete(parser);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

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/python/print.py.

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

from bitwuzla import *

if __name__ == "__main__":

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    options.set(Option.PRODUCE_MODELS, True)
    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)
    # Create some sorts.
    bv8  = tm.mk_bv_sort(8)
    bv32 = tm.mk_bv_sort(32)
    fp16 = tm.mk_fp_sort(5, 11)
    # Create terms.
    b     = tm.mk_const(tm.mk_bool_sort(), "b")
    bv    = tm.mk_const(bv8, "bv")
    fp    = tm.mk_const(fp16, "fp")
    rm    = tm.mk_const(tm.mk_rm_sort(), "rm")
    fun   = tm.mk_const(tm.mk_fun_sort([bv8, fp16, bv32], fp16), "fun")
    zero  = tm.mk_bv_zero(bv8)
    ones  = tm.mk_bv_ones(tm.mk_bv_sort(23))
    z     = tm.mk_var(bv8, "z")
    q     = tm.mk_var(bv8, "q")
    lambd = tm.mk_term(Kind.LAMBDA, [z, tm.mk_term(Kind.BV_ADD, [z, bv])])
    fpleq = tm.mk_term(
        Kind.FP_LEQ,
        [tm.mk_term(Kind.APPLY,
                  [fun, bv, fp, tm.mk_term(Kind.BV_ZERO_EXTEND, [ones], [9])]),
          fp])
    exists = tm.mk_term(
        Kind.EXISTS,
        [q, tm.mk_term(Kind.EQUAL, [zero, tm.mk_term(Kind.BV_MUL, [bv, q])])])
    # Assert formulas.
    bitwuzla.assert_formula(b)
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [tm.mk_term(Kind.APPLY, [lambd, bv]), zero]))
    bitwuzla.assert_formula(exists)
    bitwuzla.assert_formula(fpleq)

    # Print sort.
    print('Print bit-vector sort of size 32:')
    print('---------------------------------')
    print(f'str(): {bv32}')
    print()

    # Print terms.
    # Note: Hexadecimal bv output format is ignored if the value is not of size
    #       divisible by 4.
    print('Print term:')
    print('-----------')
    print(f'str()      [default]:       {rm}')
    print(f'str()      [bin (ignored)]: {rm.str(2)}')
    print(f'str()      [dec (ignored)]: {rm.str(10)}')
    print(f'str(16)    [hex (ignored)]: {rm.str(16)}')
    print()
    print(f'str()      [default]: {zero}')
    print(f'str()      [bin]:     {zero.str(2)}')
    print(f'str(10)    [dec]:     {zero.str(10)}')
    print(f'str(16)    [hex]:     {zero.str(16)}')
    print()
    print(f'str()      [default]:       {fpleq}')
    print(f'str()      [bin]:           {fpleq.str()}')
    print(f'str(10)    [dec]:           {fpleq.str(10)}')
    print(f'str(16)    [hex (ignored)]: {fpleq.str(16)}')
    print()

    # Print asserted formulas.
    # Note: This uses the default bit-vector output format (binary).
    expected_smt2 = \
            '(set-logic UFBVFP)\n' \
            + '(declare-const b Bool)\n' \
            + '(declare-const bv (_ BitVec 8))\n' \
            + '(declare-const fp (_ FloatingPoint 5 11))\n' \
            + '(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) ' \
            + '(_ BitVec 32)) (_ FloatingPoint 5 11))\n' \
            + '(assert b)\n' \
            + '(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) ' \
            + '#b00000000))\n' \
            + '(assert (exists ((q (_ BitVec 8))) (= #b00000000 ' \
            + '(bvmul bv q))))\n' \
            + '(assert (fp.leq (fun bv fp ((_ zero_extend 9) ' \
            + '#b11111111111111111111111)) fp))\n' \
            + '(check-sat)\n' \
            + '(exit)\n'
    res = bitwuzla.print_formula()
    assert res == expected_smt2
    print('Print formula [default (binary) bv output format]:')
    print('--------------------------------------------------')
    print(res)

    # Print asserted formulas using hexadecimal bit-vector output format.
    expected_smt2 = \
            '(set-logic UFBVFP)\n' \
            + '(declare-const b Bool)\n' \
            + '(declare-const bv (_ BitVec 8))\n' \
            + '(declare-const fp (_ FloatingPoint 5 11))\n' \
            + '(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) ' \
            + '(_ BitVec 32)) (_ FloatingPoint 5 11))\n' \
            + '(assert b)\n' \
            + '(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) ' \
            + '#x00))\n' \
            + '(assert (exists ((q (_ BitVec 8))) (= #x00 (bvmul bv q))))\n' \
            + '(assert (fp.leq (fun bv fp ((_ zero_extend 9) ' \
            + '#b11111111111111111111111)) fp))\n' \
            + '(check-sat)\n' \
            + '(exit)\n'
    res = bitwuzla.print_formula("smt2", 16)
    assert res == expected_smt2
    print('Print formula [hexadecimal bv output format]:')
    print('--------------------------------------------------')
    print(res)

    # Print asserted formulas using decimal bit-vector output format.
    expected_smt2 = \
            '(set-logic UFBVFP)\n' \
            + '(declare-const b Bool)\n' \
            + '(declare-const bv (_ BitVec 8))\n' \
            + '(declare-const fp (_ FloatingPoint 5 11))\n' \
            + '(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) ' \
            + '(_ BitVec 32)) (_ FloatingPoint 5 11))\n' \
            + '(assert b)\n' \
            + '(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) ' \
            + '(_ bv0 8)))\n' \
            + '(assert (exists ((q (_ BitVec 8))) (= (_ bv0 8) ' \
            + '(bvmul bv q))))\n' \
            + '(assert (fp.leq (fun bv fp ((_ zero_extend 9) ' \
            + '(_ bv8388607 23))) fp))\n' \
            + '(check-sat)\n' \
            + '(exit)\n'
    res = bitwuzla.print_formula("smt2", 10)
    assert res == expected_smt2
    print('Print formula [decimal bv output format]:')
    print('---------------------------------------------')
    print(res)

    bitwuzla.check_sat()

    # Print values.
    print('Print value of Boolean predicate:')
    print('---------------------------------')
    fpleq_val = bitwuzla.get_value(fpleq).value()
    print(f'{fpleq}: {fpleq_val} [bool]')
    print()

    print('Print value of bv const:')
    print('------------------------')
    print(f'{bv}: {bitwuzla.get_value(bv).value():>8} [str] (bin)')
    print(f'{bv}: {bitwuzla.get_value(bv).value(10):>8} [str] (dec)')
    print(f'{bv}: {bitwuzla.get_value(bv).value(16):>8} [str] (hex)')
    print()

    print('Print value of RoundingMode const:')
    print('----------------------------------')
    print(f'{rm}: {bitwuzla.get_value(rm).value()} [RoundingMode]')
    print()

    fp_val = bitwuzla.get_value(fp)

    print('Print value of fp const as single bit-vector (base ignored):')
    print('------------------------------------------------------------')
    assert fp_val.value(2, False) == fp_val.value(10, False)
    assert fp_val.value(2, False) == fp_val.value(16, False)
    print(f'{fp}: {fp_val.value(2, False):>16} [str] (bin)')
    print(f'{fp}: {fp_val.value(10, False):>16} [str] (dec [ignored])')
    print(f'{fp}: {fp_val.value(16, False):>16} [str] (hex [ignored])')
    print()

    print('Print value of fp const as list of component bit-vectors:')
    print('---------------------------------------------------------')
    val = fp_val.value(2)
    print(f'{fp}: [{val[0]}, {val[1]:>5}, {val[2]:>11}] [str] (bin)')
    val = fp_val.value(10)
    print(f'{fp}: [{val[0]}, {val[1]:>5}, {val[2]:>11}] [str] (dec)')
    val = fp_val.value(16)
    print(f'{fp}: [{val[0]}, {val[1]:>5}, {val[2]:>11}] [str] (hex)')
    print()

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

from bitwuzla import *

if __name__ == "__main__":

    # First, create a term manager instance.
    tm = TermManager()
    # Create a Bitwuzla options instance.
    options = Options()
    options.set(Option.PRODUCE_MODELS, True)
    # Then, create a Bitwuzla instance.
    bitwuzla = Bitwuzla(tm, options)
    # Create some sorts.
    bv8  = tm.mk_bv_sort(8)
    bv32 = tm.mk_bv_sort(32)
    fp16 = tm.mk_fp_sort(5, 11)
    # Create terms.
    b     = tm.mk_const(tm.mk_bool_sort(), "b")
    bv    = tm.mk_const(bv8, "bv")
    fp    = tm.mk_const(fp16, "fp")
    rm    = tm.mk_const(tm.mk_rm_sort(), "rm")
    fun   = tm.mk_const(tm.mk_fun_sort([bv8, fp16, bv32], fp16), "fun")
    zero  = tm.mk_bv_zero(bv8)
    ones  = tm.mk_bv_ones(tm.mk_bv_sort(23))
    z     = tm.mk_var(bv8, "z")
    q     = tm.mk_var(bv8, "q")
    lambd = tm.mk_term(Kind.LAMBDA, [z, tm.mk_term(Kind.BV_ADD, [z, bv])])
    fpleq = tm.mk_term(
        Kind.FP_LEQ,
        [tm.mk_term(Kind.APPLY,
                  [fun, bv, fp, tm.mk_term(Kind.BV_ZERO_EXTEND, [ones], [9])]),
          fp])
    exists = tm.mk_term(
        Kind.EXISTS,
        [q, tm.mk_term(Kind.EQUAL, [zero, tm.mk_term(Kind.BV_MUL, [bv, q])])])
    # Assert formulas.
    bitwuzla.assert_formula(b)
    bitwuzla.assert_formula(
        tm.mk_term(Kind.EQUAL, [tm.mk_term(Kind.APPLY, [lambd, bv]), zero]))
    bitwuzla.assert_formula(exists)
    bitwuzla.assert_formula(fpleq)

    # Print sort.
    print('Print bit-vector sort of size 32:')
    print('---------------------------------')
    print(f'str(): {bv32}')
    print()

    # Print terms.
    # Note: Hexadecimal bv output format is ignored if the value is not of size
    #       divisible by 4.
    print('Print term:')
    print('-----------')
    print(f'str()      [default]:       {rm}')
    print(f'str()      [bin (ignored)]: {rm.str(2)}')
    print(f'str()      [dec (ignored)]: {rm.str(10)}')
    print(f'str(16)    [hex (ignored)]: {rm.str(16)}')
    print()
    print(f'str()      [default]: {zero}')
    print(f'str()      [bin]:     {zero.str(2)}')
    print(f'str(10)    [dec]:     {zero.str(10)}')
    print(f'str(16)    [hex]:     {zero.str(16)}')
    print()
    print(f'str()      [default]:       {fpleq}')
    print(f'str()      [bin]:           {fpleq.str()}')
    print(f'str(10)    [dec]:           {fpleq.str(10)}')
    print(f'str(16)    [hex (ignored)]: {fpleq.str(16)}')
    print()

    # Print asserted formulas.
    # Note: This uses the default bit-vector output format (binary).
    expected_smt2 = \
            '(set-logic UFBVFP)\n' \
            + '(declare-const b Bool)\n' \
            + '(declare-const bv (_ BitVec 8))\n' \
            + '(declare-const fp (_ FloatingPoint 5 11))\n' \
            + '(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) ' \
            + '(_ BitVec 32)) (_ FloatingPoint 5 11))\n' \
            + '(assert b)\n' \
            + '(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) ' \
            + '#b00000000))\n' \
            + '(assert (exists ((q (_ BitVec 8))) (= #b00000000 ' \
            + '(bvmul bv q))))\n' \
            + '(assert (fp.leq (fun bv fp ((_ zero_extend 9) ' \
            + '#b11111111111111111111111)) fp))\n' \
            + '(check-sat)\n' \
            + '(exit)\n'
    res = bitwuzla.print_formula()
    assert res == expected_smt2
    print('Print formula [default (binary) bv output format]:')
    print('--------------------------------------------------')
    print(res)

    # Print asserted formulas using hexadecimal bit-vector output format.
    expected_smt2 = \
            '(set-logic UFBVFP)\n' \
            + '(declare-const b Bool)\n' \
            + '(declare-const bv (_ BitVec 8))\n' \
            + '(declare-const fp (_ FloatingPoint 5 11))\n' \
            + '(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) ' \
            + '(_ BitVec 32)) (_ FloatingPoint 5 11))\n' \
            + '(assert b)\n' \
            + '(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) ' \
            + '#x00))\n' \
            + '(assert (exists ((q (_ BitVec 8))) (= #x00 (bvmul bv q))))\n' \
            + '(assert (fp.leq (fun bv fp ((_ zero_extend 9) ' \
            + '#b11111111111111111111111)) fp))\n' \
            + '(check-sat)\n' \
            + '(exit)\n'
    res = bitwuzla.print_formula("smt2", 16)
    assert res == expected_smt2
    print('Print formula [hexadecimal bv output format]:')
    print('--------------------------------------------------')
    print(res)

    # Print asserted formulas using decimal bit-vector output format.
    expected_smt2 = \
            '(set-logic UFBVFP)\n' \
            + '(declare-const b Bool)\n' \
            + '(declare-const bv (_ BitVec 8))\n' \
            + '(declare-const fp (_ FloatingPoint 5 11))\n' \
            + '(declare-fun fun ((_ BitVec 8) (_ FloatingPoint 5 11) ' \
            + '(_ BitVec 32)) (_ FloatingPoint 5 11))\n' \
            + '(assert b)\n' \
            + '(assert (= ((lambda ((z (_ BitVec 8))) (bvadd z bv)) bv) ' \
            + '(_ bv0 8)))\n' \
            + '(assert (exists ((q (_ BitVec 8))) (= (_ bv0 8) ' \
            + '(bvmul bv q))))\n' \
            + '(assert (fp.leq (fun bv fp ((_ zero_extend 9) ' \
            + '(_ bv8388607 23))) fp))\n' \
            + '(check-sat)\n' \
            + '(exit)\n'
    res = bitwuzla.print_formula("smt2", 10)
    assert res == expected_smt2
    print('Print formula [decimal bv output format]:')
    print('---------------------------------------------')
    print(res)

    bitwuzla.check_sat()

    # Print values.
    print('Print value of Boolean predicate:')
    print('---------------------------------')
    fpleq_val = bitwuzla.get_value(fpleq).value()
    print(f'{fpleq}: {fpleq_val} [bool]')
    print()

    print('Print value of bv const:')
    print('------------------------')
    print(f'{bv}: {bitwuzla.get_value(bv).value():>8} [str] (bin)')
    print(f'{bv}: {bitwuzla.get_value(bv).value(10):>8} [str] (dec)')
    print(f'{bv}: {bitwuzla.get_value(bv).value(16):>8} [str] (hex)')
    print()

    print('Print value of RoundingMode const:')
    print('----------------------------------')
    print(f'{rm}: {bitwuzla.get_value(rm).value()} [RoundingMode]')
    print()

    fp_val = bitwuzla.get_value(fp)

    print('Print value of fp const as single bit-vector (base ignored):')
    print('------------------------------------------------------------')
    assert fp_val.value(2, False) == fp_val.value(10, False)
    assert fp_val.value(2, False) == fp_val.value(16, False)
    print(f'{fp}: {fp_val.value(2, False):>16} [str] (bin)')
    print(f'{fp}: {fp_val.value(10, False):>16} [str] (dec [ignored])')
    print(f'{fp}: {fp_val.value(16, False):>16} [str] (hex [ignored])')
    print()

    print('Print value of fp const as list of component bit-vectors:')
    print('---------------------------------------------------------')
    val = fp_val.value(2)
    print(f'{fp}: [{val[0]}, {val[1]:>5}, {val[2]:>11}] [str] (bin)')
    val = fp_val.value(10)
    print(f'{fp}: [{val[0]}, {val[1]:>5}, {val[2]:>11}] [str] (dec)')
    val = fp_val.value(16)
    print(f'{fp}: [{val[0]}, {val[1]:>5}, {val[2]:>11}] [str] (hex)')
    print()

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

#include <assert.h>
#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>

int
main()
{
  // First, create a term manager instance.
  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
  // Then, create a Bitwuzla instance.
  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
  // Create some sorts.
  BitwuzlaSort bv8           = bitwuzla_mk_bv_sort(tm, 8);
  BitwuzlaSort bv32          = bitwuzla_mk_bv_sort(tm, 32);
  BitwuzlaSort fp16          = bitwuzla_mk_fp_sort(tm, 5, 11);
  BitwuzlaSort fun_domain[3] = {bv8, fp16, bv32};
  BitwuzlaSort fun_sort      = bitwuzla_mk_fun_sort(tm, 3, fun_domain, fp16);
  // Create terms.
  BitwuzlaTerm b    = bitwuzla_mk_const(tm, bitwuzla_mk_bool_sort(tm), "b");
  BitwuzlaTerm bv   = bitwuzla_mk_const(tm, bv8, "bv");
  BitwuzlaTerm fp   = bitwuzla_mk_const(tm, fp16, "fp");
  BitwuzlaTerm rm   = bitwuzla_mk_const(tm, bitwuzla_mk_rm_sort(tm), "rm");
  BitwuzlaTerm fun  = bitwuzla_mk_const(tm, fun_sort, "fun");
  BitwuzlaTerm zero = bitwuzla_mk_bv_zero(tm, bv8);
  BitwuzlaTerm ones = bitwuzla_mk_bv_ones(tm, bitwuzla_mk_bv_sort(tm, 23));
  BitwuzlaTerm z    = bitwuzla_mk_var(tm, bv8, "z");
  BitwuzlaTerm q    = bitwuzla_mk_var(tm, bv8, "q");
  BitwuzlaTerm lambda =
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_LAMBDA,
                        z,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, z, bv));
  BitwuzlaTerm args[4] = {
      fun,
      bv,
      fp,
      bitwuzla_mk_term1_indexed1(tm, BITWUZLA_KIND_BV_ZERO_EXTEND, ones, 9)};
  BitwuzlaTerm fpleq =
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_FP_LEQ,
                        bitwuzla_mk_term(tm, BITWUZLA_KIND_APPLY, 4, args),
                        fp);
  BitwuzlaTerm exists = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_EXISTS,
      q,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        zero,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, bv, q)));
  // Assert formulas.
  bitwuzla_assert(bitwuzla, b);
  bitwuzla_assert(
      bitwuzla,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_EQUAL,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_APPLY, lambda, bv),
                        zero));
  bitwuzla_assert(bitwuzla, exists);
  bitwuzla_assert(bitwuzla, fpleq);

  // Print sort.
  printf("Print bit-vector sort of size 32:\n");
  printf("---------------------------------\n");
  printf("bitwuzla_sort_print():     ");
  bitwuzla_sort_print(bv32, stdout);
  printf("\n");
  printf("bitwuzla_sort_to_string(): %s\n\n", bitwuzla_sort_to_string(bv32));

  // Print terms.
  // Note: Hexadecimal bv output format is ignored if the value is not of size
  //       divisible by 4.
  printf("Print term:\n");
  printf("-----------\n");
  printf("bitwuzla_term_print():                         ");
  bitwuzla_term_print(rm, stdout);
  printf("\n");
  printf("bitwuzla_term_print_fmt()     [dec (ignored)]: ");
  bitwuzla_term_print_fmt(rm, stdout, 10);
  printf("\n");
  printf("bitwuzla_term_to_string():                     %s\n",
         bitwuzla_term_to_string(rm));
  printf("bitwuzla_term_to_string_fmt() [hex (ignored)]: %s\n",
         bitwuzla_term_to_string_fmt(rm, 10));
  printf("\n");
  printf("bitwuzla_term_print()         [bin]: ");
  bitwuzla_term_print(zero, stdout);
  printf("\n");
  printf("bitwuzla_term_print_fmt()     [dec]: ");
  bitwuzla_term_print_fmt(zero, stdout, 10);
  printf("\n");
  printf("bitwuzla_term_print_fmt()     [hex]: ");
  bitwuzla_term_print_fmt(zero, stdout, 16);
  printf("\n");
  printf("bitwuzla_term_to_string()     [bin]: %s\n",
         bitwuzla_term_to_string(zero));
  printf("bitwuzla_term_to_string_fmt() [dec]: %s\n",
         bitwuzla_term_to_string_fmt(zero, 10));
  printf("bitwuzla_term_to_string_fmt() [hex]: %s\n",
         bitwuzla_term_to_string_fmt(zero, 16));
  printf("\n");
  printf("bitwuzla_term_print_fmt()     [bin]:           ");
  bitwuzla_term_print_fmt(fpleq, stdout, 2);
  printf("\n");
  printf("bitwuzla_term_print_fmt()     [dec]:           ");
  bitwuzla_term_print_fmt(fpleq, stdout, 10);
  printf("\n");
  printf("bitwuzla_term_print_fmt()     [hex (ignored)]: ");
  bitwuzla_term_print_fmt(fpleq, stdout, 16);
  printf("\n");
  printf("bitwuzla_term_to_string_fmt() [bin]:           %s\n",
         bitwuzla_term_to_string_fmt(fpleq, 2));
  printf("bitwuzla_term_to_string_fmt() [dec]:           %s\n",
         bitwuzla_term_to_string_fmt(fpleq, 10));
  printf("bitwuzla_term_to_string_fmt() [hex (ignored)]: %s\n",
         bitwuzla_term_to_string_fmt(fpleq, 16));
  printf("\n");

  // Print asserted formulas using binary bit-vector output format.
  {
    printf("Print formula [binary bv output format]:\n");
    printf("----------------------------------------\n");
    bitwuzla_print_formula(bitwuzla, "smt2", stdout, 2);
    printf("\n");
  }

  // Print asserted formulas using hexadecimal bit-vector output format.
  {
    printf("Print formula [hexadecimal bv output format]:\n");
    printf("----------------------------------------\n");
    bitwuzla_print_formula(bitwuzla, "smt2", stdout, 16);
    printf("\n");
  }

  // Print asserted formulas using decimal bit-vector output format.
  {
    printf("Print formula [decimal bv output format]:\n");
    printf("----------------------------------------\n");
    bitwuzla_print_formula(bitwuzla, "smt2", stdout, 10);
    printf("\n");
  }

  bitwuzla_check_sat(bitwuzla);

  // Print values.
  printf("Print value of Boolean predicate:\n");
  printf("---------------------------------\n");
  BitwuzlaTerm fpleq_val    = bitwuzla_get_value(bitwuzla, fpleq);
  bool fpleq_val_bool       = bitwuzla_term_value_get_bool(fpleq_val);
  const char* fpleq_val_str = bitwuzla_term_value_get_str(fpleq_val);
  printf("%s: %*u [bool]\n", bitwuzla_term_to_string(fpleq), 4, fpleq_val_bool);
  printf("%s: %*s [const char*]\n\n",
         bitwuzla_term_to_string(fpleq),
         4,
         fpleq_val_str);

  printf("Print value of bv const:\n");
  printf("------------------------\n");
  BitwuzlaTerm bv_val = bitwuzla_get_value(bitwuzla, bv);
  printf("%s: %*s [const char*] (bin)\n",
         bitwuzla_term_to_string(bv),
         8,
         bitwuzla_term_value_get_str(bv_val));
  printf("%s: %*s [const char*] (dec)\n",
         bitwuzla_term_to_string(bv),
         8,
         bitwuzla_term_value_get_str_fmt(bv_val, 10));
  printf("%s: %*s [const char*] (hex)\n\n",
         bitwuzla_term_to_string(bv),
         8,
         bitwuzla_term_value_get_str_fmt(bv_val, 16));

  printf("Print value of RoundingMode const:\n");
  printf("----------------------------------\n");
  BitwuzlaTerm rm_val = bitwuzla_get_value(bitwuzla, rm);
  BitwuzlaRoundingMode rm_val_rm = bitwuzla_term_value_get_rm(rm_val);
  const char* rm_val_str         = bitwuzla_term_value_get_str(rm_val);
  printf("%s: %s [BitwuzlaRoundingMode]\n",
         bitwuzla_term_to_string(rm),
         bitwuzla_rm_to_string(rm_val_rm));
  printf("%s: %s [const char*]\n\n", bitwuzla_term_to_string(rm), rm_val_str);

  BitwuzlaTerm fp_val = bitwuzla_get_value(bitwuzla, fp);

  printf("Print value of fp const via bitwuzla_term_value_get_str(_fmt):\n");
  printf("--------------------------------------------------------------\n");
  printf("%s: %*s [const char*] (bin) \n",
         bitwuzla_term_to_string(fp),
         16,
         bitwuzla_term_value_get_str(fp_val));
  printf("%s: %*s [const char*] (dec [ignored]) \n",
         bitwuzla_term_to_string(fp),
         16,
         bitwuzla_term_value_get_str_fmt(fp_val, 10));
  printf("%s: %*s [const char*] (hex [ignored]) \n\n",
         bitwuzla_term_to_string(fp),
         16,
         bitwuzla_term_value_get_str_fmt(fp_val, 16));

  printf("Print value of fp const via bitwuzla_term_value_get_fp_ieee():\n");
  printf("--------------------------------------------------------------\n");
  const char* sign;
  const char* exponent;
  const char* significand;
  bitwuzla_term_value_get_fp_ieee(fp_val, &sign, &exponent, &significand, 2);
  printf("%s: (%s %*s %*s) (bin)\n",
         bitwuzla_term_to_string(fp),
         sign,
         5,
         exponent,
         11,
         significand);
  bitwuzla_term_value_get_fp_ieee(fp_val, &sign, &exponent, &significand, 10);
  printf("%s: (%s %*s %*s) (dec)\n",
         bitwuzla_term_to_string(fp),
         sign,
         5,
         exponent,
         11,
         significand);
  bitwuzla_term_value_get_fp_ieee(fp_val, &sign, &exponent, &significand, 16);
  printf("%s: (%s %*s %*s) (hex)\n",
         bitwuzla_term_to_string(fp),
         sign,
         5,
         exponent,
         11,
         significand);

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);
  return 0;
}

Termination Callback Example

This example shows how to configure a termination callback.

The source code for this example can be found at examples/python/terminator.py.

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

import time

from bitwuzla import *

class TestTerminator:
    def __init__(self, time_limit):
        self.start_time = time.time()
        self.time_limit = time_limit

    def __call__(self):
        # Terminate after self.time_limit ms passed
        return (time.time() - self.start_time) * 1000 > self.time_limit

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # No options configured, create Bitwuzla instance with default options.
    bitwuzla = Bitwuzla(tm)

    bv = tm.mk_bv_sort(32)

    x = tm.mk_const(bv)
    s = tm.mk_const(bv)
    t = tm.mk_const(bv)

    a = tm.mk_term(Kind.DISTINCT,
                     [tm.mk_term(Kind.BV_MUL, [s, tm.mk_term(Kind.BV_MUL, [x, t])]),
                      tm.mk_term(Kind.BV_MUL, [tm.mk_term(Kind.BV_MUL, [s, x]), t])])

    # Now, we check that the following formula is unsat.
    # (assert (distinct (bvmul s (bvmul x t)) (bvmul (bvmul s x) t)))
    print('> Without terminator (with preprocessing):')
    print('Expect: unsat')
    print(f'Bitwuzla: {bitwuzla.check_sat(a)}')

    # Now, for illustration purposes, we disable preprocessing, which will
    # significantly increase solving time, and connect a terminator instance
    # that terminates after a certain time limit.
    options = Options()
    options.set(Option.PREPROCESS, False)
    # Create new Bitwuzla instance with reconfigured options.
    bitwuzla2 = Bitwuzla(tm, options)
    # Configure and connect terminator.
    tt = TestTerminator(1)
    bitwuzla2.configure_terminator(tt)

    # Now, we expect Bitwuzla to be terminated during the check-sat call.
    print('> With terminator (no preprocessing):')
    print('Expect: unsat')
    print(f'Bitwuzla: {bitwuzla2.check_sat(a)}')

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

import time

from bitwuzla import *

class TestTerminator:
    def __init__(self, time_limit):
        self.start_time = time.time()
        self.time_limit = time_limit

    def __call__(self):
        # Terminate after self.time_limit ms passed
        return (time.time() - self.start_time) * 1000 > self.time_limit

if __name__ == '__main__':

    # First, create a term manager instance.
    tm = TermManager()
    # No options configured, create Bitwuzla instance with default options.
    bitwuzla = Bitwuzla(tm)

    bv = tm.mk_bv_sort(32)

    x = tm.mk_const(bv)
    s = tm.mk_const(bv)
    t = tm.mk_const(bv)

    a = tm.mk_term(Kind.DISTINCT,
                     [tm.mk_term(Kind.BV_MUL, [s, tm.mk_term(Kind.BV_MUL, [x, t])]),
                      tm.mk_term(Kind.BV_MUL, [tm.mk_term(Kind.BV_MUL, [s, x]), t])])

    # Now, we check that the following formula is unsat.
    # (assert (distinct (bvmul s (bvmul x t)) (bvmul (bvmul s x) t)))
    print('> Without terminator (with preprocessing):')
    print('Expect: unsat')
    print(f'Bitwuzla: {bitwuzla.check_sat(a)}')

    # Now, for illustration purposes, we disable preprocessing, which will
    # significantly increase solving time, and connect a terminator instance
    # that terminates after a certain time limit.
    options = Options()
    options.set(Option.PREPROCESS, False)
    # Create new Bitwuzla instance with reconfigured options.
    bitwuzla2 = Bitwuzla(tm, options)
    # Configure and connect terminator.
    tt = TestTerminator(1)
    bitwuzla2.configure_terminator(tt)

    # Now, we expect Bitwuzla to be terminated during the check-sat call.
    print('> With terminator (no preprocessing):')
    print('Expect: unsat')
    print(f'Bitwuzla: {bitwuzla2.check_sat(a)}')

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

#include <bitwuzla/c/bitwuzla.h>
#include <stdint.h>
#include <stdio.h>
#include <sys/time.h>

struct terminator_state
{
  struct timeval start;
  uint32_t time_limit_ms;
};

static int32_t
test_terminate(void* state)
{
  struct terminator_state* tstate = (struct terminator_state*) state;
  struct timeval now;
  gettimeofday(&now, NULL);
  if (((now.tv_sec - tstate->start.tv_sec) * 1000
       + (now.tv_usec - tstate->start.tv_usec) / 1000)
      >= tstate->time_limit_ms)
  {
    return 1;
  }
  return 0;
}

int
main()
{
  // First, create a term manager instance.
  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();
  // Then, create a Bitwuzla instance.
  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);

  BitwuzlaSort bv = bitwuzla_mk_bv_sort(tm, 32);

  BitwuzlaTerm x = bitwuzla_mk_const(tm, bv, "x");
  BitwuzlaTerm s = bitwuzla_mk_const(tm, bv, "s");
  BitwuzlaTerm t = bitwuzla_mk_const(tm, bv, "t");

  BitwuzlaTerm a = bitwuzla_mk_term2(
      tm,
      BITWUZLA_KIND_DISTINCT,
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_BV_MUL,
                        s,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, x, t)),
      bitwuzla_mk_term2(tm,
                        BITWUZLA_KIND_BV_MUL,
                        bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_MUL, s, x),
                        t));

  // Now, we check that the following formula is unsat.
  // (assert (distinct (bvmul s (bvmul x t)) (bvmul (bvmul s x) t)))
  BitwuzlaTerm assumptions[1] = {a};
  printf("> Without terminator (with preprocessing):\n");
  printf("Expect: unsat\n");
  printf("Result: %s\n",
         bitwuzla_result_to_string(
             bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions)));

  // Now, for illustration purposes, we disable preprocessing, which will
  // significantly increase solving time, and connect a terminator instance
  // that terminates after a certain time limit.
  bitwuzla_set_option(options, BITWUZLA_OPT_PREPROCESS, 0);
  // Create new Bitwuzla instance with reconfigured options.
  Bitwuzla* bitwuzla2 = bitwuzla_new(tm, options);
  // Configure termination callback.
  struct terminator_state state;
  gettimeofday(&state.start, NULL);
  state.time_limit_ms = 1000;
  bitwuzla_set_termination_callback(bitwuzla2, test_terminate, &state);

  // Now, we expect Bitwuzla to be terminated during the check-sat call.
  printf("> With terminator (no preprocessing):\n");
  printf("Expect: unknown\n");
  printf("Result: %s\n",
         bitwuzla_result_to_string(
             bitwuzla_check_sat_assuming(bitwuzla2, 1, assumptions)));

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_delete(bitwuzla2);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}