Expand description
Low-level bindings for the Bitwuzla SMT solver.
Please see the Bitwuzla C API documentation for function descriptions.
Structs§
- Bitwuzla
- Bitwuzla
Option Info - Bitwuzla
Option Info_ Mode Value - Bitwuzla
Option Info_ Numeric Value - Bitwuzla
Option Info_ String Value - Bitwuzla
Options - Bitwuzla
Term Manager
Constants§
- BITWUZLA_
KIND_ AND - BITWUZLA_
KIND_ APPLY - BITWUZLA_
KIND_ ARRAY_ SELECT - BITWUZLA_
KIND_ ARRAY_ STORE - BITWUZLA_
KIND_ BV_ ADD - BITWUZLA_
KIND_ BV_ AND - BITWUZLA_
KIND_ BV_ ASHR - BITWUZLA_
KIND_ BV_ COMP - BITWUZLA_
KIND_ BV_ CONCAT - BITWUZLA_
KIND_ BV_ DEC - BITWUZLA_
KIND_ BV_ EXTRACT - BITWUZLA_
KIND_ BV_ INC - BITWUZLA_
KIND_ BV_ MUL - BITWUZLA_
KIND_ BV_ NAND - BITWUZLA_
KIND_ BV_ NEG - BITWUZLA_
KIND_ BV_ NEG_ OVERFLOW - BITWUZLA_
KIND_ BV_ NOR - BITWUZLA_
KIND_ BV_ NOT - BITWUZLA_
KIND_ BV_ OR - BITWUZLA_
KIND_ BV_ REDAND - BITWUZLA_
KIND_ BV_ REDOR - BITWUZLA_
KIND_ BV_ REDXOR - BITWUZLA_
KIND_ BV_ REPEAT - BITWUZLA_
KIND_ BV_ ROL - BITWUZLA_
KIND_ BV_ ROLI - BITWUZLA_
KIND_ BV_ ROR - BITWUZLA_
KIND_ BV_ RORI - BITWUZLA_
KIND_ BV_ SADD_ OVERFLOW - BITWUZLA_
KIND_ BV_ SDIV - BITWUZLA_
KIND_ BV_ SDIV_ OVERFLOW - BITWUZLA_
KIND_ BV_ SGE - BITWUZLA_
KIND_ BV_ SGT - BITWUZLA_
KIND_ BV_ SHL - BITWUZLA_
KIND_ BV_ SHR - BITWUZLA_
KIND_ BV_ SIGN_ EXTEND - BITWUZLA_
KIND_ BV_ SLE - BITWUZLA_
KIND_ BV_ SLT - BITWUZLA_
KIND_ BV_ SMOD - BITWUZLA_
KIND_ BV_ SMUL_ OVERFLOW - BITWUZLA_
KIND_ BV_ SREM - BITWUZLA_
KIND_ BV_ SSUB_ OVERFLOW - BITWUZLA_
KIND_ BV_ SUB - BITWUZLA_
KIND_ BV_ UADD_ OVERFLOW - BITWUZLA_
KIND_ BV_ UDIV - BITWUZLA_
KIND_ BV_ UGE - BITWUZLA_
KIND_ BV_ UGT - BITWUZLA_
KIND_ BV_ ULE - BITWUZLA_
KIND_ BV_ ULT - BITWUZLA_
KIND_ BV_ UMUL_ OVERFLOW - BITWUZLA_
KIND_ BV_ UREM - BITWUZLA_
KIND_ BV_ USUB_ OVERFLOW - BITWUZLA_
KIND_ BV_ XNOR - BITWUZLA_
KIND_ BV_ XOR - BITWUZLA_
KIND_ BV_ ZERO_ EXTEND - BITWUZLA_
KIND_ CONSTANT - BITWUZLA_
KIND_ CONST_ ARRAY - BITWUZLA_
KIND_ DISTINCT - BITWUZLA_
KIND_ EQUAL - BITWUZLA_
KIND_ EXISTS - BITWUZLA_
KIND_ FORALL - BITWUZLA_
KIND_ FP_ ABS - BITWUZLA_
KIND_ FP_ ADD - BITWUZLA_
KIND_ FP_ DIV - BITWUZLA_
KIND_ FP_ EQUAL - BITWUZLA_
KIND_ FP_ FMA - BITWUZLA_
KIND_ FP_ FP - BITWUZLA_
KIND_ FP_ GEQ - BITWUZLA_
KIND_ FP_ GT - BITWUZLA_
KIND_ FP_ IS_ INF - BITWUZLA_
KIND_ FP_ IS_ NAN - BITWUZLA_
KIND_ FP_ IS_ NEG - BITWUZLA_
KIND_ FP_ IS_ NORMAL - BITWUZLA_
KIND_ FP_ IS_ POS - BITWUZLA_
KIND_ FP_ IS_ SUBNORMAL - BITWUZLA_
KIND_ FP_ IS_ ZERO - BITWUZLA_
KIND_ FP_ LEQ - BITWUZLA_
KIND_ FP_ LT - BITWUZLA_
KIND_ FP_ MAX - BITWUZLA_
KIND_ FP_ MIN - BITWUZLA_
KIND_ FP_ MUL - BITWUZLA_
KIND_ FP_ NEG - BITWUZLA_
KIND_ FP_ REM - BITWUZLA_
KIND_ FP_ RTI - BITWUZLA_
KIND_ FP_ SQRT - BITWUZLA_
KIND_ FP_ SUB - BITWUZLA_
KIND_ FP_ TO_ FP_ FROM_ BV - BITWUZLA_
KIND_ FP_ TO_ FP_ FROM_ FP - BITWUZLA_
KIND_ FP_ TO_ FP_ FROM_ SBV - BITWUZLA_
KIND_ FP_ TO_ FP_ FROM_ UBV - BITWUZLA_
KIND_ FP_ TO_ SBV - BITWUZLA_
KIND_ FP_ TO_ UBV - BITWUZLA_
KIND_ IFF - BITWUZLA_
KIND_ IMPLIES - BITWUZLA_
KIND_ ITE - BITWUZLA_
KIND_ LAMBDA - BITWUZLA_
KIND_ NOT - BITWUZLA_
KIND_ NUM_ KINDS - BITWUZLA_
KIND_ OR - BITWUZLA_
KIND_ VALUE - BITWUZLA_
KIND_ VARIABLE - BITWUZLA_
KIND_ XOR - BITWUZLA_
OPT_ ABSTRACTION - BITWUZLA_
OPT_ ABSTRACTION_ ASSERT - BITWUZLA_
OPT_ ABSTRACTION_ ASSERT_ REFS - BITWUZLA_
OPT_ ABSTRACTION_ BV_ ADD - BITWUZLA_
OPT_ ABSTRACTION_ BV_ MUL - BITWUZLA_
OPT_ ABSTRACTION_ BV_ SIZE - BITWUZLA_
OPT_ ABSTRACTION_ BV_ UDIV - BITWUZLA_
OPT_ ABSTRACTION_ BV_ UREM - BITWUZLA_
OPT_ ABSTRACTION_ EAGER_ REFINE - BITWUZLA_
OPT_ ABSTRACTION_ EQUAL - BITWUZLA_
OPT_ ABSTRACTION_ INC_ BITBLAST - BITWUZLA_
OPT_ ABSTRACTION_ INITIAL_ LEMMAS - BITWUZLA_
OPT_ ABSTRACTION_ ITE - BITWUZLA_
OPT_ ABSTRACTION_ VALUE_ LIMIT - BITWUZLA_
OPT_ ABSTRACTION_ VALUE_ ONLY - BITWUZLA_
OPT_ BV_ SOLVER - BITWUZLA_
OPT_ DBG_ CHECK_ MODEL - BITWUZLA_
OPT_ DBG_ CHECK_ UNSAT_ CORE - BITWUZLA_
OPT_ DBG_ PP_ NODE_ THRESH - BITWUZLA_
OPT_ DBG_ RW_ NODE_ THRESH - BITWUZLA_
OPT_ LOGLEVEL - BITWUZLA_
OPT_ MEMORY_ LIMIT - BITWUZLA_
OPT_ NTHREADS - BITWUZLA_
OPT_ NUM_ OPTS - BITWUZLA_
OPT_ PP_ CONTRADICTING_ ANDS - BITWUZLA_
OPT_ PP_ ELIM_ BV_ EXTRACTS - BITWUZLA_
OPT_ PP_ ELIM_ BV_ UDIV - BITWUZLA_
OPT_ PP_ EMBEDDED_ CONSTR - BITWUZLA_
OPT_ PP_ FLATTEN_ AND - BITWUZLA_
OPT_ PP_ NORMALIZE - BITWUZLA_
OPT_ PP_ SKELETON_ PREPROC - BITWUZLA_
OPT_ PP_ VARIABLE_ SUBST - BITWUZLA_
OPT_ PP_ VARIABLE_ SUBST_ NORM_ BV_ INEQ - BITWUZLA_
OPT_ PP_ VARIABLE_ SUBST_ NORM_ DISEQ - BITWUZLA_
OPT_ PP_ VARIABLE_ SUBST_ NORM_ EQ - BITWUZLA_
OPT_ PREPROCESS - BITWUZLA_
OPT_ PRODUCE_ MODELS - BITWUZLA_
OPT_ PRODUCE_ UNSAT_ ASSUMPTIONS - BITWUZLA_
OPT_ PRODUCE_ UNSAT_ CORES - BITWUZLA_
OPT_ PROP_ CONST_ BITS - BITWUZLA_
OPT_ PROP_ INFER_ INEQ_ BOUNDS - BITWUZLA_
OPT_ PROP_ NPROPS - BITWUZLA_
OPT_ PROP_ NUPDATES - BITWUZLA_
OPT_ PROP_ OPT_ LT_ CONCAT_ SEXT - BITWUZLA_
OPT_ PROP_ PATH_ SEL - BITWUZLA_
OPT_ PROP_ PROB_ RANDOM_ INPUT - BITWUZLA_
OPT_ PROP_ PROB_ USE_ INV_ VALUE - BITWUZLA_
OPT_ PROP_ SEXT - BITWUZLA_
OPT_ REWRITE_ LEVEL - BITWUZLA_
OPT_ SAT_ SOLVER - BITWUZLA_
OPT_ SEED - BITWUZLA_
OPT_ TIME_ LIMIT_ PER - BITWUZLA_
OPT_ VERBOSITY - BITWUZLA_
OPT_ WRITE_ AIGER - BITWUZLA_
OPT_ WRITE_ CNF - BITWUZLA_
RM_ MAX - BITWUZLA_
RM_ RNA - BITWUZLA_
RM_ RNE - BITWUZLA_
RM_ RTN - BITWUZLA_
RM_ RTP - BITWUZLA_
RM_ RTZ - BITWUZLA_
SAT - BITWUZLA_
UNKNOWN - BITWUZLA_
UNSAT
Functions§
- bitwuzla_
assert ⚠ - bitwuzla_
check_ ⚠sat - bitwuzla_
check_ ⚠sat_ assuming - bitwuzla_
copyright ⚠ - bitwuzla_
delete ⚠ - bitwuzla_
get_ ⚠assertions - bitwuzla_
get_ ⚠option - bitwuzla_
get_ ⚠option_ info - bitwuzla_
get_ ⚠option_ mode - bitwuzla_
get_ ⚠option_ string - bitwuzla_
get_ ⚠statistics - bitwuzla_
get_ ⚠term_ mgr - bitwuzla_
get_ ⚠termination_ callback_ state - bitwuzla_
get_ ⚠unsat_ assumptions - bitwuzla_
get_ ⚠unsat_ core - bitwuzla_
get_ ⚠value - bitwuzla_
git_ ⚠id - bitwuzla_
is_ ⚠unsat_ assumption - bitwuzla_
kind_ ⚠to_ string - bitwuzla_
mk_ ⚠array_ sort - bitwuzla_
mk_ ⚠bool_ sort - bitwuzla_
mk_ ⚠bv_ max_ signed - bitwuzla_
mk_ ⚠bv_ min_ signed - bitwuzla_
mk_ ⚠bv_ one - bitwuzla_
mk_ ⚠bv_ ones - bitwuzla_
mk_ ⚠bv_ sort - bitwuzla_
mk_ ⚠bv_ value - bitwuzla_
mk_ ⚠bv_ value_ int64 - bitwuzla_
mk_ ⚠bv_ value_ uint64 - bitwuzla_
mk_ ⚠bv_ zero - bitwuzla_
mk_ ⚠const - bitwuzla_
mk_ ⚠const_ array - bitwuzla_
mk_ ⚠false - bitwuzla_
mk_ ⚠fp_ from_ rational - bitwuzla_
mk_ ⚠fp_ from_ real - bitwuzla_
mk_ ⚠fp_ nan - bitwuzla_
mk_ ⚠fp_ neg_ inf - bitwuzla_
mk_ ⚠fp_ neg_ zero - bitwuzla_
mk_ ⚠fp_ pos_ inf - bitwuzla_
mk_ ⚠fp_ pos_ zero - bitwuzla_
mk_ ⚠fp_ sort - bitwuzla_
mk_ ⚠fp_ value - bitwuzla_
mk_ ⚠fun_ sort - bitwuzla_
mk_ ⚠rm_ sort - bitwuzla_
mk_ ⚠rm_ value - bitwuzla_
mk_ ⚠term - bitwuzla_
mk_ ⚠term1 - bitwuzla_
mk_ ⚠term2 - bitwuzla_
mk_ ⚠term3 - bitwuzla_
mk_ ⚠term1_ indexed1 - bitwuzla_
mk_ ⚠term1_ indexed2 - bitwuzla_
mk_ ⚠term2_ indexed1 - bitwuzla_
mk_ ⚠term2_ indexed2 - bitwuzla_
mk_ ⚠term_ indexed - bitwuzla_
mk_ ⚠true - bitwuzla_
mk_ ⚠uninterpreted_ sort - bitwuzla_
mk_ ⚠var - bitwuzla_
new ⚠ - bitwuzla_
option_ ⚠is_ mode - bitwuzla_
option_ ⚠is_ numeric - bitwuzla_
option_ ⚠is_ string - bitwuzla_
option_ ⚠is_ valid - bitwuzla_
options_ ⚠delete - bitwuzla_
options_ ⚠new - bitwuzla_
pop ⚠ - bitwuzla_
print_ ⚠formula - bitwuzla_
print_ ⚠unsat_ core - bitwuzla_
push ⚠ - bitwuzla_
result_ ⚠to_ string - bitwuzla_
rm_ ⚠to_ string - bitwuzla_
set_ ⚠abort_ callback - bitwuzla_
set_ ⚠option - bitwuzla_
set_ ⚠option_ mode - bitwuzla_
set_ ⚠option_ string - bitwuzla_
set_ ⚠termination_ callback - bitwuzla_
simplify ⚠ - bitwuzla_
simplify_ ⚠term - bitwuzla_
sort_ ⚠array_ get_ element - bitwuzla_
sort_ ⚠array_ get_ index - bitwuzla_
sort_ ⚠bv_ get_ size - bitwuzla_
sort_ ⚠copy - bitwuzla_
sort_ ⚠fp_ get_ exp_ size - bitwuzla_
sort_ ⚠fp_ get_ sig_ size - bitwuzla_
sort_ ⚠fun_ get_ arity - bitwuzla_
sort_ ⚠fun_ get_ codomain - bitwuzla_
sort_ ⚠fun_ get_ domain_ sorts - bitwuzla_
sort_ ⚠get_ uninterpreted_ symbol - bitwuzla_
sort_ ⚠hash - bitwuzla_
sort_ ⚠is_ array - bitwuzla_
sort_ ⚠is_ bool - bitwuzla_
sort_ ⚠is_ bv - bitwuzla_
sort_ ⚠is_ fp - bitwuzla_
sort_ ⚠is_ fun - bitwuzla_
sort_ ⚠is_ rm - bitwuzla_
sort_ ⚠is_ uninterpreted - bitwuzla_
sort_ ⚠print - bitwuzla_
sort_ ⚠release - bitwuzla_
sort_ ⚠to_ string - bitwuzla_
substitute_ ⚠term - bitwuzla_
substitute_ ⚠terms - bitwuzla_
term_ ⚠array_ get_ element_ sort - bitwuzla_
term_ ⚠array_ get_ index_ sort - bitwuzla_
term_ ⚠bv_ get_ size - bitwuzla_
term_ ⚠copy - bitwuzla_
term_ ⚠fp_ get_ exp_ size - bitwuzla_
term_ ⚠fp_ get_ sig_ size - bitwuzla_
term_ ⚠fp_ value_ to_ real_ string - bitwuzla_
term_ ⚠fun_ get_ arity - bitwuzla_
term_ ⚠fun_ get_ codomain_ sort - bitwuzla_
term_ ⚠fun_ get_ domain_ sorts - bitwuzla_
term_ ⚠get_ children - bitwuzla_
term_ ⚠get_ indices - bitwuzla_
term_ ⚠get_ kind - bitwuzla_
term_ ⚠get_ sort - bitwuzla_
term_ ⚠get_ symbol - bitwuzla_
term_ ⚠hash - bitwuzla_
term_ ⚠is_ array - bitwuzla_
term_ ⚠is_ bool - bitwuzla_
term_ ⚠is_ bv - bitwuzla_
term_ ⚠is_ bv_ value - bitwuzla_
term_ ⚠is_ bv_ value_ max_ signed - bitwuzla_
term_ ⚠is_ bv_ value_ min_ signed - bitwuzla_
term_ ⚠is_ bv_ value_ one - bitwuzla_
term_ ⚠is_ bv_ value_ ones - bitwuzla_
term_ ⚠is_ bv_ value_ zero - bitwuzla_
term_ ⚠is_ const - bitwuzla_
term_ ⚠is_ equal_ sort - bitwuzla_
term_ ⚠is_ false - bitwuzla_
term_ ⚠is_ fp - bitwuzla_
term_ ⚠is_ fp_ value - bitwuzla_
term_ ⚠is_ fp_ value_ nan - bitwuzla_
term_ ⚠is_ fp_ value_ neg_ inf - bitwuzla_
term_ ⚠is_ fp_ value_ neg_ zero - bitwuzla_
term_ ⚠is_ fp_ value_ pos_ inf - bitwuzla_
term_ ⚠is_ fp_ value_ pos_ zero - bitwuzla_
term_ ⚠is_ fun - bitwuzla_
term_ ⚠is_ indexed - bitwuzla_
term_ ⚠is_ rm - bitwuzla_
term_ ⚠is_ rm_ value - bitwuzla_
term_ ⚠is_ rm_ value_ rna - bitwuzla_
term_ ⚠is_ rm_ value_ rne - bitwuzla_
term_ ⚠is_ rm_ value_ rtn - bitwuzla_
term_ ⚠is_ rm_ value_ rtp - bitwuzla_
term_ ⚠is_ rm_ value_ rtz - bitwuzla_
term_ ⚠is_ true - bitwuzla_
term_ ⚠is_ uninterpreted - bitwuzla_
term_ ⚠is_ value - bitwuzla_
term_ ⚠is_ var - bitwuzla_
term_ ⚠manager_ delete - bitwuzla_
term_ ⚠manager_ new - bitwuzla_
term_ ⚠manager_ release - bitwuzla_
term_ ⚠print - bitwuzla_
term_ ⚠print_ fmt - bitwuzla_
term_ ⚠release - bitwuzla_
term_ ⚠to_ string - bitwuzla_
term_ ⚠to_ string_ fmt - bitwuzla_
term_ ⚠value_ get_ bool - bitwuzla_
term_ ⚠value_ get_ fp_ ieee - bitwuzla_
term_ ⚠value_ get_ rm - bitwuzla_
term_ ⚠value_ get_ str - bitwuzla_
term_ ⚠value_ get_ str_ fmt - bitwuzla_
version ⚠