Python Interface

Classes

Options

class bitwuzla.Options

A Bitwuzla options configuration.

description(option: Option) → str

Get the description of this option.

Returns:

The description of this option.

get(option: Option)

Get the current value of the given option.

Parameters:

option – The option.

Returns:

The current value of the given option.

is_bool(option: Option)

Determine if given option is a Boolean option.

Parameters:

option – The option to query.

Returns:

True if option is a Boolean option.

is_mode(option: Option)

Determine if given option is an option with a mode.

Parameters:

option – The option to query.

Returns:

True if option is an option with a mode.

is_numeric(option: Option)

Determine if given option is a numeric option.

Parameters:

option – The option to query.

Returns:

True if option is a numeric option.

is_valid(name: str)

Determine if given string is a valid short or long option name. :param name: The name. :return: True if given string is a option name.

lng(option: Option) → str

Get the long name of this option.

Returns:

The long name of this option.

modes(option: Option) → list[str]

Get the modes of this option.

Returns:

The modes of this option.

option(name: str) → Option

Get the option associated to the given short or long option name.

Returns:

The option associated to the given short or long option name.

set(option, value)

Set option.

Parameters:

  • option – The option or the long or short name of an option.

  • value – The option value.

set_args(*args)

Set option via command-line.

Supports the following command line option format:

Short option names:

-short      ... ["-short"]
-short=val  ... ["-short=val"]
-short val  ... ["-short", "val"]

Long option names:

--long      ... ["--long"]
--long=val  ... ["--long=val"]
--long val  ... ["--long", "val"]
Parameters:

args – List of command line options.

shrt(option: Option) → str

Get the short name of this option.

Returns:

The short name of this option.

TermManager

class bitwuzla.TermManager

The term manager is responsible for the creation and management of sorts and terms. Sorts and terms are tied to a specific term manager instance and can be shared between multiple solver instances that have the same term manager.

__init__(*args, **kwargs)
mk_array_sort(index: Sort, elem: Sort) → Sort

Create array sort with given index and element sorts.

Parameters:

  • index – The sort of the array index.

  • elem – The sort of the array elements.

Returns:

Array sort.

mk_bool_sort() → Sort

Create a Boolean sort.

Returns:

Sort of type Boolean.

mk_bv_max_signed(sort)

Create a bit-vector maximum signed value.

Parameters:

sort (BitwuzlaSort) – Bit-vector sort.

Returns:

A term representing the bit-vector value of given sort where the MSB is set to 0 and all remaining bits are set to 1.

Return type:

BitwuzlaTerm

mk_bv_min_signed(sort)

Create a bit-vector minimum signed value.

Parameters:

sort (BitwuzlaSort) – Bit-vector sort.

Returns:

A term representing the bit-vector value of given sort where the MSB is set to 1 and all remaining bits are set to 0.

Return type:

BitwuzlaTerm

mk_bv_one(sort)

Create a bit-vector value one with sort.

Parameters:

sort (BitwuzlaSort) – Bit-vector sort.

Returns:

A term representing the bit-vector value one of given sort.

Return type:

BitwuzlaTerm

mk_bv_ones(sort)

Create a bit-vector value with sort where all bits are set to 1.

Parameters:

sort (BitwuzlaSort) – Bit-vector sort.

Returns:

A term representing the bit-vector value of given sort where all bits are set to 1.

Return type:

BitwuzlaTerm

mk_bv_sort(size: uint64_t) → Sort

Create bit-vector sort of size size.

Parameters:

size – Bit width.

Returns:

Bit-vector sort of size size.

mk_bv_value(sort: Sort, value: int) → Term
mk_bv_value(sort: Sort, value: str, base: int) → Term

Create bit-vector representing value of given sort.

Parameters:

  • sort (BitwuzlaSort) – Bit-vector sort.

  • value (int) – An integer representing the value.

Create bit-vector representing value of given sort and base.

Parameters:

  • sort (BitwuzlaSort) – Bit-vector sort.

  • value (str) – A string representing the value.

  • base (int) – The numerical base of the string representation (2 for binary, 10 for decimal, 16 for hexadecimal).

Returns:

A term representing the bit-vector value.

Return type:

BitwuzlaTerm

mk_bv_zero(sort)

Create a bit-vector value zero with sort.

Parameters:

sort (BitwuzlaSort) – Bit-vector sort.

Returns:

A term representing the bit-vector value zero of given sort.

Return type:

BitwuzlaTerm

mk_const(sort: Sort, symbol: str = None) → Term

Create a (first-order) constant of given sort with given symbol.

Parameters:

  • sort – The sort of the constant.

  • symbol – The symbol of the constant.

Returns:

A term of kind CONSTANT, representing the constant.

mk_const_array(sort: Sort, term: Term) → Term

Create a one-dimensional constant array of given sort, initialized with given value.

Parameters:

  • sort – The sort of the array.

  • term – The term to initialize the elements of the array with.

Returns:

A term of kind CONST_ARRAY, representing a constant array of given sort.

mk_false()

Create false value.

Returns:

A term representing false.

Return type:

BitwuzlaTerm

mk_fp_nan(sort: Sort) → Term

Create a floating-point NaN value.

Parameters:

sort – Floating-point sort.

Returns:

A term representing the floating-point NaN value of given floating-point sort.

mk_fp_neg_inf(sort: Sort) → Term

Create a floating-point negative infinity value (SMT-LIB: -oo).

Parameters:

sort – Floating-point sort.

Returns:

A term representing the floating-point negative infinity value of given floating-point sort.

mk_fp_neg_zero(sort: Sort) → Term

Create a floating-point negative zero value (SMT-LIB: -zero).

Parameters:

sort – Floating-point sort.

Returns:

A term representing the floating-point negative zero value of given floating-point sort.

mk_fp_pos_inf(sort: Sort) → Term

Create a floating-point positive infinity value (SMT-LIB: +oo).

Parameters:

sort – Floating-point sort.

Returns:

A term representing the floating-point positive infinity value of given floating-point sort.

mk_fp_pos_zero(sort: Sort) → Term

Create a floating-point positive zero value (SMT-LIB: +zero).

Parameters:

sort – Floating-point sort.

Returns:

A term representing the floating-point positive zero value of given floating-point sort.

mk_fp_sort(exp_size: uint64_t, sig_size: uint64_t) → Sort

Create a floating-point sort with given exponent size exp_size and significand size sig_size.

Parameters:

  • exp_size – Exponent size.

  • sig_size – Significand size.

Returns:

Floating-point sort.

mk_fp_value(sign: Term, exponent: Term, significand: Term) → Term
mk_fp_value(sort: Sort, rm: Term, real: str) → Term
mk_fp_value(sort: Sort, rm: Term, num: str, den: str) → Term

Create a floating-point value from its IEEE 754 standard representation given as three bit-vector values representing the sign bit, the exponent and the significand.

Parameters:

  • sign – Bit-vector value term representing the sign bit.

  • exponent – Bit-vector value term representing the exponent.

  • significand – Bit-vector value term representing the significand.

Create a floating-point value from its real representation, given as a decimal string, with respect to given rounding mode.

Parameters:

  • sort – Floating-point sort.

  • rm – Rounding mode term.

  • real – The decimal string representing a real value

Create a floating-point value from its rational representation, given as a two decimal strings representing the numerator and denominator, with respect to given rounding mode.

Parameters:

  • sort – Floating-point sort.

  • rm – Rounding mode term.

  • num – The decimal string representing the numerator.

  • den – The decimal string representing the denominator.

Returns:

A term representing the floating-point value.

See also

mk_bv_value() for the supported value format for sign, exponent, and significand.

mk_fun_sort(domain: list[Sort], codomain: Sort) → Sort

Create function sort with given domain and codomain.

Parameters:

  • domain – A list of all the function arguments’ sorts.

  • codomain – The sort of the function’s return value.

Returns:

Function sort, which maps domain to codomain.

mk_rm_sort() → Sort

Create a rounding mode sort.

Returns:

Rounding mode sort.

mk_rm_value(rm: RoundingMode) → Term

Create a rounding mode value.

Parameters:

rm – Rounding mode.

Returns:

A term representing the rounding mode value.

mk_term(kind: Kind, terms: list[Term], indices: list[int] = []) → Term

Create a term of given kind with the given argument terms.

Parameters:

  • kind – The operator kind.

  • terms – The argument terms.

  • indices – The indices of this term, empty if not indexed.

Returns:

A term representing an operation of given kind.

mk_true()

Create true value.

Returns:

A term representing true.

Return type:

BitwuzlaTerm

mk_uninterpreted_sort(symbol: str = None) → Sort

Create an uninterpreted sort.

Parameters:

symbol – The symbol of the sort.

Returns:

Uninterpreted Sort.

Note

Only 0-arity uninterpreted sorts are supported.

mk_var(sort: Sort, symbol: str = None) → Term

Create a (first-order) variable of given sort with given symbol.

Parameters:

  • sort – The sort of the variable.

  • symbol – The symbol of the variable.

Returns:

A term of kind VARIABLE, representing the variable.

substitute_term(term: Term, substs: dict[Term, Term]) → Term

Substitute a set terms in a given term. The substitutions to perform are represented as map from keys to be substituted with their corresponding values in the given term.

Parameters:

  • term – The term in which the terms are to be substituted.

  • substs – The substitution map.

Returns:

The resulting term from this substitution.

substitute_terms(terms: list[Term], substs: dict[Term, Term]) → list[Term]

Substitute a set of terms in a set of given terms. The substitutions to perform are represented as map from keys to be substituted with their corresponding values in the given terms.

The terms in terms are replaced with the terms resulting from these substitutions.

Parameters:

  • terms – The terms in which the terms are to be substituted.

  • substs – The substitution map.

Bitwuzla

class bitwuzla.Bitwuzla

A Bitwuzla solver instance.

__init__()

Constructor.

Parameters:

options – The options configuration of the solver instance.

assert_formula(*formulas: Term)

Assert one or more formulas.

Parameters:

formulas – One or more Boolean terms.

check_sat(*assumptions: Term) → Result

Check satisfiability of asserted formulas under possibly given assumptions.

Parameters:

assumptions – Zero or more Boolean terms.

Returns:

  • SAT if the input formula is satisfiable (under possibly given assumptions)

  • UNSAT if it is unsatisfiable

  • UNKNOWN otherwise

See also

assert_formula(), get_value(), get_unsat_core(), get_unsat_assumptions(),

configure_terminator(callback: callable)

Set a termination callback.

Use this function to force Bitwuzla to prematurely terminate if callback returns True. The callback object needs to be a callable, i.e., it is a function or class that implements the builtin method __call__().

For example:

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

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

bitwuzla = Bitwuzla()
bitwuzla.configure_terminator(lambda: True)            # immediately terminate
bitwuzla.configure_terminator(TimeLimitTerminator(1))  # terminate after 1s
bitwuzla.configure_terminator(TimeLimitTerminator(10)) # terminate after 10s
Parameters:

callback – A callable Python object.

get_assertions() → list[Term]

Get currently asserted formulas. :return: List of current assertions.

get_unsat_assumptions() → list[Term]

Return list of unsatisfiable assumptions previously added via check_sat().

Requires that the last check_sat() call returned ~bitwuzla.Result.UNSAT.

Returns:

List of unsatisfiable assumptions

get_unsat_core() → list[Term]

Return list of unsatisfiable assertions previously added via assert_formula().

Requires that the last check_sat() call returned UNSAT.

Returns:

list of unsatisfiable assertions

get_value(term: Term) → Term

Get model value of term.

Requires that the last check_sat() call returned ~bitwuzla.Result.SAT.

Returns:

Term representing the model value of term.

is_unsat_assumption(term) → bool

Determine if given assumption is unsat.

Unsat assumptions are those assumptions that force an input formula to become unsatisfiable.

See check_sat().

Parameters:

term – Boolean term.

Returns:

True if assumption is unsat, False otherwise.

pop(nlevels: uint32_t = 1)

Pop assertion levels.

Parameters:

levels (int) – Number of assertion levels to pop.

print_formula(fmt: str = 'smt2', base=2) → str

Get the current input formula as a string.

Parameters:

  • fmt – The output format for printing the formula. Currently, only “smt2” for the SMT-LIB v2 format is supported.

  • base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal. Always ignored for Boolean and RoundingMode values.

Returns:

The current input formula as a string in the given format.

push(nlevels: uint32_t = 1)

Push new assertion levels.

Parameters:

levels (int) – Number of assertion levels to create.

simplify()

Simplify current set of input assertions.

Note

Each call to check_sat() simplifies the input formula as a preprocessing step. It is not necessary to call this function explicitly in the general case.

statistics() → dict[str, str]

Get current statistics.

Returns:

A map of strings of statistics entries, maps statistic name to value.

term_mgr() → TermManager

Sort

class bitwuzla.Sort

A Bitwuzla sort.

array_element() → Sort

Get the element sort of an array sort.

Requires that given sort is an array sort.

Returns:

The element sort of the array sort.

array_index() → Sort

Get the index sort of an array sort.

Requires that given sort is an array sort.

Returns:

The index sort of the array sort.

bv_size() → int

Get the size of a bit-vector sort.

Requires that given sort is a bit-vector sort.

Returns:

The size of the bit-vector sort.

fp_exp_size() → int

Get the exponent size of a floating-point sort.

Requires that given sort is a floating-point sort.

Returns:

The exponent size of the floating-point sort.

fp_sig_size() → int

Get the significand size of a floating-point sort.

Requires that given sort is a floating-point sort.

Returns:

The significand size of the floating-point sort.

fun_arity() → int

Get the arity of a function sort.

Returns:

The number of arguments of the function sort.

fun_codomain() → Sort

Get the codomain sort of a function sort.

Requires that given sort is a function sort.

Returns:

The codomain sort of the function sort.

fun_domain() → list[Sort]

Get the domain sorts of a function sort.

Requires that given sort is a function sort.

Returns:

The domain sorts of the function sort.

id() → int

Get the id of this sort.

Returns:

The sort id.

is_array() → bool

Determine if this sort is an array sort.

Returns:

True if this sort is an array sort.

is_bool() → bool

Determine if this sort is a Boolean sort.

Returns:

True if this sort is a Boolean sort.

is_bv() → bool

Determine if this sort is a bit-vector sort.

Returns:

True if sort is a bit-vector sort.

is_fp() → bool

Determine if this sort is a floating-point sort.

Returns:

True if this sort is a floating-point sort.

is_fun() → bool

Determine if this sort is a function sort.

Returns:

True if this sort is a function sort.

is_null() → bool

Determine if this sort is a null sort.

Returns:

True if this sort is a null sort.

is_rm() → bool

Determine if this sort is a Roundingmode sort.

Returns:

True if this sort is a Roundingmode sort.

is_uninterpreted() → bool

Determine if this sort is an uninterpreted sort.

Returns:

True if this sort is an uninterpreted sort.

uninterpreted_symbol() → str

Get the symbol of an uninterpreted sort.

Returns:

The symbol.

Term

class bitwuzla.Term

A Bitwuzla term.

children() → list[Term]

Get the child terms of this term.

Returns:

The children of this term as a vector of terms.

id() → int

Get the id of this term.

Returns:

The term id.

indices() → list[int]

Get the indices of an indexed term.

Requires that given term is an indexed term.

Returns:

The indices of this term as a vector of indices.

is_bv_value_max_signed() → bool

Determine if this term is a bit-vector maximum signed value.

Returns:

True if this term is a bit-vector value with the most significant bit set to 0 and all other bits set to 1.

is_bv_value_min_signed() → bool

Determine if this term is a bit-vector minimum signed value.

Returns:

True if this term is a bit-vector value with the most significant bit set to 1 and all other bits set to 0.

is_bv_value_one() → bool

Determine if this term is a bit-vector value representing one.

Returns:

True if this term is a bit-vector one value.

is_bv_value_ones() → bool

Determine if this term is a bit-vector value with all bits set to one.

Returns:

True if this term is a bit-vector value with all bits set to one.

is_bv_value_zero() → bool

Determine if this term is a bit-vector value representing zero.

Returns:

True if this term is a bit-vector zero value.

is_const() → bool

Determine if this term is a constant.

Returns:

True if this term is a constant.

is_false() → bool

Determine if this term is Boolean value false.

Returns:

True if this term is Boolean value false.

is_fp_value_nan() → bool

Determine if this term is a floating-point NaN value.

Returns:

True if this term is a floating-point NaN value.

is_fp_value_neg_inf() → bool

Determine if this term is a floating-point negative infinity (-oo) value.

Returns:

True if this term is a floating-point -oo value.

is_fp_value_neg_zero() → bool

Determine if this term is a floating-point value negative zero (-zero).

Returns:

True if this term is a floating-point -zero.

is_fp_value_pos_inf() → bool

Determine if this term is a floating-point positive infinity (+oo) value.

Returns:

True if this term is a floating-point +oo value.

is_fp_value_pos_zero() → bool

Determine if this term is a floating-point positive zero (+zero) value.

Returns:

True if this term is a floating-point +zero value.

is_null() → bool

Determine if this term is a null term.

Returns:

True if this term is a null term.

is_rm_value_rna() → bool

Determine if this term is a rounding mode RNA value.

Returns:

True if this term is a roundindg mode RNA value.

is_rm_value_rne() → bool

Determine if this term is a rounding mode RNE value.

Returns:

True if this term is a rounding mode RNE value.

is_rm_value_rtn() → bool

Determine if this term is a rounding mode RTN value.

Returns:

True if this term is a rounding mode RTN value.

is_rm_value_rtp() → bool

Determine if this term is a rounding mode RTP value.

Returns:

True if this term is a rounding mode RTP value.

is_rm_value_rtz() → bool

Determine if this term is a rounding mode RTZ value.

Returns:

True if this term is a rounding mode RTZ value.

is_true() → bool

Determine if this term is Boolean value true.

Returns:

True if this term is Boolean value true.

is_value() → bool

Determine if this term is a value.

Returns:

True if this term is a value.

is_variable() → bool

Determine if this term is a variable.

Returns:

True if this term is a variable.

kind() → Kind

Get the kind of this term.

Returns:

The kind.

num_children() → int

Get the number of child terms of this term.

Returns:

The number of children of this term.

num_indices() → int

Get the number of indices of this term.

Returns:

The number of indices of this term.

sort() → Sort

Get the sort of this term.

Returns:

The sort of the term.

str(base=2) → str

Get the SMT-LIB v2 string representation of this term.

Parameters:

base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal. Always ignored for Boolean and RoundingMode values.

Returns:

A string representation of this term.

symbol() → str

Get the symbol of this term.

Returns:

The symbol of this term. None if no symbol is defined.

value(base=2, fp_as_tuple=True)

Get value from value term.

This function is instantiated for types - bool for Boolean values - RoundingMode for rounding mode values - string for bit-vector and floating-point values

In case of string representations of values this returns the raw value string (as opposed to str(), which returns the SMT-LIB v2 representation of a term). For example, this function returns "010" for a bit-vector value 2 of size 3, while str() returns "#b010".

Note:

The returned string for floating-point values is always the binary IEEE-754 representation of the value (parameter base is ignored). Parameter base always configures the numeric base for bit-vector values, and for floating-point values in case of the tuple of strings instantiation. It is always ignored for Boolean and RoundingMode values.

Parameters:

  • base – The numeric base for bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal.

  • fp_as_tuple – True if a floating-point value is to be represented as a tuple of raw string representations of the sign, exponent and significand bit-vectors. False to represent as the binary IEEE-754 string representation of a single bit-vector.

Parser

class bitwuzla.Parser

The Bitwuzla parser.

__init__()

Constructor.

Note:

The parser creates and owns the associated Bitwuzla instance.

Parameters:

  • options – The configuration options for the Bitwuzla instance (created by the parser).

  • language – The format of the input.

  • base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal. Always ignored for Boolean and RoundingMode values.

bitwuzla() → Bitwuzla

Get the associated Bitwuzla instance.

Returns:

The Bitwuzla instance.

parse(iinput, parse_only: bool = False, parse_file: bool = True) → bool

Parse input, either from a file or from a string.

Parameters:

  • input – The name of the input file if parse_file is True, else a string with the input.

  • parse_only – True to only parse without issuing calls to check_sat.

  • parse_file – True to parse an input file with the given name iinput, False to parse from iinput as a string input.

Raises:

BitwuzlaException – On parse error.

Note:

Parameter parse_only is redundant for BTOR2 input, its the only available mode for BTOR2 (due to the language not supporting “commands” as in SMT2).

parse_sort(iinput) → Sort

Parse sort from string.

Parameters:

input – The input string.

Returns:

The parsed sort.

Raises:

BitwuzlaException – On parse error.

parse_term(iinput) → Term

Parse term from string.

Parameters:

input – The input string.

Returns:

The parsed term.

Raises:

BitwuzlaException – On parse error.

OptionInfo

class bitwuzla.OptionInfo

The class holding all information about an option.

cur()

Get the current value of an option. :return: The current default value.

description()

Get the description of an option. :return: The description.

dflt()

Get the default value of an option. :return: The default value.

kind() → OptionInfoKind

Get the kind of this OptionInfo. :return: The kind.

lng()

Get the long name of an option. :return: The long name of an option.

max()

Get the maximum value of a numeric option. :return: The maximum value.

min()

Get the minimum value of a numeric option. :return: The minimum value.

modes()

Get the available modes of an option with modes. :return: The modes.

shrt()

Get the short name of an option. :return: The short name, if any, else None.

Enums

Option

class bitwuzla.Option(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)

Configuration options supported by Bitwuzla. For more information on options see Options.

BV_SOLVER = 8
DBG_CHECK_MODEL = 35
DBG_CHECK_UNSAT_CORE = 36
DBG_PP_NODE_THRESH = 34
DBG_RW_NODE_THRESH = 33
LOGLEVEL = 0
MEMORY_LIMIT = 7
PP_CONTRADICTING_ANDS = 22
PP_ELIM_BV_EXTRACTS = 23
PP_EMBEDDED_CONSTR = 24
PP_FLATTEN_AND = 25
PP_NORMALIZE = 26
PP_NORMALIZE_SHARE_AWARE = 27
PP_SKELETON_PREPROC = 28
PP_VARIABLE_SUBST = 29
PP_VARIABLE_SUBST_NORM_BV_INEQ = 32
PP_VARIABLE_SUBST_NORM_DISEQ = 31
PP_VARIABLE_SUBST_NORM_EQ = 30
PREPROCESS = 21
PRODUCE_MODELS = 1
PRODUCE_UNSAT_ASSUMPTIONS = 2
PRODUCE_UNSAT_CORES = 3
PROP_CONST_BITS = 11
PROP_INFER_INEQ_BOUNDS = 12
PROP_NORMALIZE = 20
PROP_NPROPS = 13
PROP_NUPDATES = 14
PROP_OPT_LT_CONCAT_SEXT = 15
PROP_PATH_SEL = 16
PROP_PROB_RANDOM_INPUT = 17
PROP_PROB_USE_INV_VALUE = 18
PROP_SEXT = 19
REWRITE_LEVEL = 9
SAT_SOLVER = 10
SEED = 4
TIME_LIMIT_PER = 6
VERBOSITY = 5

OptionInfoKind

class bitwuzla.OptionInfoKind(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)

The kind of an OptionInfo.

BOOL = 0
MODE = 2
NUMERIC = 1

Kind

class bitwuzla.Kind(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)

BitwuzlaTerm kinds. For more information on term kinds see bitwuzla::Kind.

AND = 4
APPLY = 15
ARRAY_SELECT = 17
ARRAY_STORE = 18
BV_ADD = 19
BV_AND = 20
BV_ASHR = 21
BV_COMP = 22
BV_CONCAT = 23
BV_DEC = 24
BV_EXTRACT = 63
BV_INC = 25
BV_MUL = 26
BV_NAND = 27
BV_NEG = 28
BV_NEG_OVERFLOW = 29
BV_NOR = 30
BV_NOT = 31
BV_OR = 32
BV_REDAND = 33
BV_REDOR = 34
BV_REDXOR = 35
BV_REPEAT = 64
BV_ROL = 36
BV_ROLI = 65
BV_ROR = 37
BV_RORI = 66
BV_SADD_OVERFLOW = 38
BV_SDIV = 40
BV_SDIV_OVERFLOW = 39
BV_SGE = 41
BV_SGT = 42
BV_SHL = 43
BV_SHR = 44
BV_SIGN_EXTEND = 67
BV_SLE = 45
BV_SLT = 46
BV_SMOD = 47
BV_SMUL_OVERFLOW = 48
BV_SREM = 49
BV_SSUB_OVERFLOW = 50
BV_SUB = 51
BV_UADD_OVERFLOW = 52
BV_UDIV = 53
BV_UGE = 54
BV_UGT = 55
BV_ULE = 56
BV_ULT = 57
BV_UMUL_OVERFLOW = 58
BV_UREM = 59
BV_USUB_OVERFLOW = 60
BV_XNOR = 61
BV_XOR = 62
BV_ZERO_EXTEND = 68
CONSTANT = 0
CONST_ARRAY = 1
DISTINCT = 5
EQUAL = 6
EXISTS = 13
FORALL = 14
FP_ABS = 69
FP_ADD = 70
FP_DIV = 71
FP_EQUAL = 72
FP_FMA = 73
FP_FP = 74
FP_GEQ = 75
FP_GT = 76
FP_IS_INF = 77
FP_IS_NAN = 78
FP_IS_NEG = 79
FP_IS_NORMAL = 80
FP_IS_POS = 81
FP_IS_SUBNORMAL = 82
FP_IS_ZERO = 83
FP_LEQ = 84
FP_LT = 85
FP_MAX = 86
FP_MIN = 87
FP_MUL = 88
FP_NEG = 89
FP_REM = 90
FP_RTI = 91
FP_SQRT = 92
FP_SUB = 93
FP_TO_FP_FROM_BV = 94
FP_TO_FP_FROM_FP = 95
FP_TO_FP_FROM_SBV = 96
FP_TO_FP_FROM_UBV = 97
FP_TO_SBV = 98
FP_TO_UBV = 99
IFF = 7
IMPLIES = 8
ITE = 12
LAMBDA = 16
NOT = 9
OR = 10
VALUE = 2
VARIABLE = 3
XOR = 11

Result

class bitwuzla.Result(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)

Satisfiability result.

SAT = 10
UNKNOWN = 0
UNSAT = 20

RoundingMode

class bitwuzla.RoundingMode(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)

Floating-point rounding mode.

RNA = 1
RNE = 0
RTN = 2
RTP = 3
RTZ = 4