Expand description
Low-level bindings for the Boolector SMT solver.
Please see the Boolector C API documentation for function descriptions.
Re-exports§
pub use self::BtorOptQuantSynth as BtorOptQuantSynt;
Structs§
Constants§
- BTOR_
BETA_ REDUCE_ ALL - BTOR_
BETA_ REDUCE_ FUN - BTOR_
BETA_ REDUCE_ NONE - BTOR_
DP_ QSORT_ ASC - BTOR_
DP_ QSORT_ DESC - BTOR_
DP_ QSORT_ JUST - BTOR_
ENGINE_ AIGPROP - BTOR_
ENGINE_ FUN - BTOR_
ENGINE_ PROP - BTOR_
ENGINE_ QUANT - BTOR_
ENGINE_ SLS - BTOR_
FUN_ EAGER_ LEMMAS_ ALL - BTOR_
FUN_ EAGER_ LEMMAS_ CONF - BTOR_
FUN_ EAGER_ LEMMAS_ NONE - BTOR_
INCREMENTAL_ SMT1_ BASIC - BTOR_
INCREMENTAL_ SMT1_ CONTINUE - BTOR_
INPUT_ FORMAT_ BTOR - BTOR_
INPUT_ FORMAT_ BTOR2 - BTOR_
INPUT_ FORMAT_ NONE - BTOR_
INPUT_ FORMAT_ SMT1 - BTOR_
INPUT_ FORMAT_ SMT2 - BTOR_
JUST_ HEUR_ BRANCH_ LEFT - BTOR_
JUST_ HEUR_ BRANCH_ MIN_ APP - BTOR_
JUST_ HEUR_ BRANCH_ MIN_ DEP - BTOR_
OPT_ ACKERMANN - BTOR_
OPT_ AIGPROP_ USE_ BANDIT - BTOR_
OPT_ AIGPROP_ USE_ RESTARTS - BTOR_
OPT_ AUTO_ CLEANUP - BTOR_
OPT_ AUTO_ CLEANUP_ INTERNAL - BTOR_
OPT_ BETA_ REDUCE - BTOR_
OPT_ CHK_ FAILED_ ASSUMPTIONS - BTOR_
OPT_ CHK_ MODEL - BTOR_
OPT_ CHK_ UNCONSTRAINED - BTOR_
OPT_ DECLSORT_ BV_ WIDTH - BTOR_
OPT_ ELIMINATE_ SLICES - BTOR_
OPT_ ENGINE - BTOR_
OPT_ EXIT_ CODES - BTOR_
OPT_ EXTRACT_ LAMBDAS - BTOR_
OPT_ FUN_ DUAL_ PROP - BTOR_
OPT_ FUN_ DUAL_ PROP_ QSORT - BTOR_
OPT_ FUN_ EAGER_ LEMMAS - BTOR_
OPT_ FUN_ JUST - BTOR_
OPT_ FUN_ JUST_ HEURISTIC - BTOR_
OPT_ FUN_ LAZY_ SYNTHESIZE - BTOR_
OPT_ FUN_ PREPROP - BTOR_
OPT_ FUN_ PRESLS - BTOR_
OPT_ FUN_ STORE_ LAMBDAS - BTOR_
OPT_ INCREMENTAL - BTOR_
OPT_ INCREMENTAL_ SMT1 - BTOR_
OPT_ INPUT_ FORMAT - BTOR_
OPT_ LOGLEVEL - BTOR_
OPT_ MERGE_ LAMBDAS - BTOR_
OPT_ MODEL_ GEN - BTOR_
OPT_ NONDESTR_ SUBST - BTOR_
OPT_ NORMALIZE - BTOR_
OPT_ NORMALIZE_ ADD - BTOR_
OPT_ NUM_ OPTS - BTOR_
OPT_ OUTPUT_ FORMAT - BTOR_
OPT_ OUTPUT_ NUMBER_ FORMAT - BTOR_
OPT_ PARSE_ INTERACTIVE - BTOR_
OPT_ PRETTY_ PRINT - BTOR_
OPT_ PRINT_ DIMACS - BTOR_
OPT_ PROP_ FLIP_ COND_ CONST_ DELTA - BTOR_
OPT_ PROP_ FLIP_ COND_ CONST_ NPATHSEL - BTOR_
OPT_ PROP_ NO_ MOVE_ ON_ CONFLICT - BTOR_
OPT_ PROP_ NPROPS - BTOR_
OPT_ PROP_ PATH_ SEL - BTOR_
OPT_ PROP_ PROB_ AND_ FLIP - BTOR_
OPT_ PROP_ PROB_ CONC_ FLIP - BTOR_
OPT_ PROP_ PROB_ EQ_ FLIP - BTOR_
OPT_ PROP_ PROB_ FLIP_ COND - BTOR_
OPT_ PROP_ PROB_ FLIP_ COND_ CONST - BTOR_
OPT_ PROP_ PROB_ SLICE_ FLIP - BTOR_
OPT_ PROP_ PROB_ SLICE_ KEEP_ DC - BTOR_
OPT_ PROP_ PROB_ USE_ INV_ VALUE - BTOR_
OPT_ PROP_ USE_ BANDIT - BTOR_
OPT_ PROP_ USE_ RESTARTS - BTOR_
OPT_ QUANT_ CER - BTOR_
OPT_ QUANT_ DER - BTOR_
OPT_ QUANT_ DUAL_ SOLVER - BTOR_
OPT_ QUANT_ FIXSYNTH - BTOR_
OPT_ QUANT_ MINISCOPE - BTOR_
OPT_ QUANT_ SYNTH - BTOR_
OPT_ QUANT_ SYNTH_ ITE_ COMPLETE - BTOR_
OPT_ QUANT_ SYNTH_ LIMIT - BTOR_
OPT_ QUANT_ SYNTH_ QI - BTOR_
OPT_ REWRITE_ LEVEL - BTOR_
OPT_ RW_ ZERO_ LOWER_ SLICE - BTOR_
OPT_ SAT_ ENGINE - BTOR_
OPT_ SAT_ ENGINE_ CADICAL_ FREEZE - BTOR_
OPT_ SAT_ ENGINE_ LGL_ FORK - BTOR_
OPT_ SAT_ ENGINE_ N_ THREADS - BTOR_
OPT_ SEED - BTOR_
OPT_ SIMPLIFY_ CONSTRAINTS - BTOR_
OPT_ SIMP_ NORMAMLIZE_ ADDERS - BTOR_
OPT_ SKELETON_ PREPROC - BTOR_
OPT_ SLS_ JUST - BTOR_
OPT_ SLS_ MOVE_ GW - BTOR_
OPT_ SLS_ MOVE_ INC_ MOVE_ TEST - BTOR_
OPT_ SLS_ MOVE_ PROP - BTOR_
OPT_ SLS_ MOVE_ PROP_ FORCE_ RW - BTOR_
OPT_ SLS_ MOVE_ PROP_ N_ PROP - BTOR_
OPT_ SLS_ MOVE_ PROP_ N_ SLS - BTOR_
OPT_ SLS_ MOVE_ RAND_ ALL - BTOR_
OPT_ SLS_ MOVE_ RAND_ RANGE - BTOR_
OPT_ SLS_ MOVE_ RAND_ WALK - BTOR_
OPT_ SLS_ MOVE_ RANGE - BTOR_
OPT_ SLS_ MOVE_ SEGMENT - BTOR_
OPT_ SLS_ NFLIPS - BTOR_
OPT_ SLS_ PROB_ MOVE_ RAND_ WALK - BTOR_
OPT_ SLS_ STRATEGY - BTOR_
OPT_ SLS_ USE_ BANDIT - BTOR_
OPT_ SLS_ USE_ RESTARTS - BTOR_
OPT_ SORT_ AIG - BTOR_
OPT_ SORT_ AIGVEC - BTOR_
OPT_ SORT_ EXP - BTOR_
OPT_ UCOPT - BTOR_
OPT_ VAR_ SUBST - BTOR_
OPT_ VERBOSITY - BTOR_
OUTPUT_ BASE_ BIN - BTOR_
OUTPUT_ BASE_ DEC - BTOR_
OUTPUT_ BASE_ HEX - BTOR_
OUTPUT_ FORMAT_ AIGER_ ASCII - BTOR_
OUTPUT_ FORMAT_ AIGER_ BINARY - BTOR_
OUTPUT_ FORMAT_ BTOR - BTOR_
OUTPUT_ FORMAT_ NONE - BTOR_
OUTPUT_ FORMAT_ SMT2 - BTOR_
PROP_ PATH_ SEL_ CONTROLLING - BTOR_
PROP_ PATH_ SEL_ ESSENTIAL - BTOR_
PROP_ PATH_ SEL_ RANDOM - BTOR_
QUANT_ SYNTH_ EL - BTOR_
QUANT_ SYNTH_ ELMC - BTOR_
QUANT_ SYNTH_ ELMR - BTOR_
QUANT_ SYNTH_ EL_ ELMC - BTOR_
QUANT_ SYNTH_ NONE - BTOR_
SAT_ ENGINE_ CADICAL - BTOR_
SAT_ ENGINE_ CMS - BTOR_
SAT_ ENGINE_ LINGELING - BTOR_
SAT_ ENGINE_ MINISAT - BTOR_
SAT_ ENGINE_ PICOSAT - BTOR_
SLS_ STRAT_ ALWAYS_ PROP - BTOR_
SLS_ STRAT_ BEST_ MOVE - BTOR_
SLS_ STRAT_ BEST_ SAME_ MOVE - BTOR_
SLS_ STRAT_ FIRST_ BEST_ MOVE - BTOR_
SLS_ STRAT_ RAND_ WALK - Btor
Solver Result_ BTOR_ RESULT_ SAT - Btor
Solver Result_ BTOR_ RESULT_ UNKNOWN - Btor
Solver Result_ BTOR_ RESULT_ UNSAT
Functions§
- boolector_
add ⚠ - boolector_
and ⚠ - boolector_
apply ⚠ - boolector_
array ⚠ - boolector_
array_ ⚠assignment - boolector_
array_ ⚠sort - boolector_
assert ⚠ - boolector_
assume ⚠ - boolector_
bitvec_ ⚠sort - boolector_
bitvec_ ⚠sort_ get_ width - boolector_
bool_ ⚠sort - boolector_
bv_ ⚠assignment - boolector_
clone ⚠ - boolector_
concat ⚠ - boolector_
cond ⚠ - boolector_
const ⚠ - boolector_
const_ ⚠array - boolector_
constd ⚠ - boolector_
consth ⚠ - boolector_
copy ⚠ - boolector_
copy_ ⚠sort - boolector_
copyright ⚠ - boolector_
dec ⚠ - boolector_
delete ⚠ - boolector_
dump_ ⚠aiger_ ascii - boolector_
dump_ ⚠aiger_ binary - boolector_
dump_ ⚠btor - boolector_
dump_ ⚠btor_ node - boolector_
dump_ ⚠smt2 - boolector_
dump_ ⚠smt2_ node - boolector_
eq ⚠ - boolector_
exists ⚠ - boolector_
failed ⚠ - boolector_
false ⚠ - boolector_
first_ ⚠opt - boolector_
fixate_ ⚠assumptions - boolector_
forall ⚠ - boolector_
free_ ⚠array_ assignment - boolector_
free_ ⚠bits - boolector_
free_ ⚠bv_ assignment - boolector_
free_ ⚠uf_ assignment - boolector_
fun ⚠ - boolector_
fun_ ⚠get_ codomain_ sort - boolector_
fun_ ⚠get_ domain_ sort - boolector_
fun_ ⚠sort - boolector_
fun_ ⚠sort_ check - boolector_
get_ ⚠bits - boolector_
get_ ⚠btor - boolector_
get_ ⚠failed_ assumptions - boolector_
get_ ⚠fun_ arity - boolector_
get_ ⚠index_ width - boolector_
get_ ⚠node_ id - boolector_
get_ ⚠opt - boolector_
get_ ⚠opt_ desc - boolector_
get_ ⚠opt_ dflt - boolector_
get_ ⚠opt_ lng - boolector_
get_ ⚠opt_ max - boolector_
get_ ⚠opt_ min - boolector_
get_ ⚠opt_ shrt - boolector_
get_ ⚠refs - boolector_
get_ ⚠sort - boolector_
get_ ⚠symbol - boolector_
get_ ⚠trapi - boolector_
get_ ⚠value - boolector_
get_ ⚠width - boolector_
git_ ⚠id - boolector_
has_ ⚠opt - boolector_
iff ⚠ - boolector_
implies ⚠ - boolector_
inc ⚠ - boolector_
int ⚠ - boolector_
is_ ⚠array - boolector_
is_ ⚠array_ sort - boolector_
is_ ⚠array_ var - boolector_
is_ ⚠bitvec_ sort - boolector_
is_ ⚠bound_ param - boolector_
is_ ⚠bv_ const_ max_ signed - boolector_
is_ ⚠bv_ const_ min_ signed - boolector_
is_ ⚠bv_ const_ one - boolector_
is_ ⚠bv_ const_ ones - boolector_
is_ ⚠bv_ const_ zero - boolector_
is_ ⚠const - boolector_
is_ ⚠equal_ sort - boolector_
is_ ⚠fun - boolector_
is_ ⚠fun_ sort - boolector_
is_ ⚠param - boolector_
is_ ⚠uf - boolector_
is_ ⚠var - boolector_
limited_ ⚠sat - boolector_
match_ ⚠node - boolector_
match_ ⚠node_ by_ id - boolector_
match_ ⚠node_ by_ symbol - boolector_
max_ ⚠signed - boolector_
min_ ⚠signed - boolector_
mul ⚠ - boolector_
nand ⚠ - boolector_
ne ⚠ - boolector_
neg ⚠ - boolector_
new ⚠ - boolector_
next_ ⚠opt - boolector_
nor ⚠ - boolector_
not ⚠ - boolector_
one ⚠ - boolector_
ones ⚠ - boolector_
or ⚠ - boolector_
param ⚠ - boolector_
parse ⚠ - boolector_
parse_ ⚠btor - boolector_
parse_ ⚠btor2 - boolector_
parse_ ⚠smt1 - boolector_
parse_ ⚠smt2 - boolector_
pop ⚠ - boolector_
print_ ⚠model - boolector_
print_ ⚠stats - boolector_
push ⚠ - boolector_
read ⚠ - boolector_
redand ⚠ - boolector_
redor ⚠ - boolector_
redxor ⚠ - boolector_
release ⚠ - boolector_
release_ ⚠all - boolector_
release_ ⚠sort - boolector_
repeat ⚠ - boolector_
reset_ ⚠assumptions - boolector_
reset_ ⚠stats - boolector_
reset_ ⚠time - boolector_
rol ⚠ - boolector_
roli ⚠ - boolector_
ror ⚠ - boolector_
rori ⚠ - boolector_
saddo ⚠ - boolector_
sat ⚠ - boolector_
sdiv ⚠ - boolector_
sdivo ⚠ - boolector_
set_ ⚠abort - boolector_
set_ ⚠msg_ prefix - boolector_
set_ ⚠opt - boolector_
set_ ⚠sat_ solver - boolector_
set_ ⚠symbol - boolector_
set_ ⚠term - boolector_
set_ ⚠trapi - boolector_
sext ⚠ - boolector_
sgt ⚠ - boolector_
sgte ⚠ - boolector_
simplify ⚠ - boolector_
slice ⚠ - boolector_
sll ⚠ - boolector_
slt ⚠ - boolector_
slte ⚠ - boolector_
smod ⚠ - boolector_
smulo ⚠ - boolector_
sra ⚠ - boolector_
srem ⚠ - boolector_
srl ⚠ - boolector_
ssubo ⚠ - boolector_
sub ⚠ - boolector_
terminate ⚠ - boolector_
true ⚠ - boolector_
uaddo ⚠ - boolector_
udiv ⚠ - boolector_
uext ⚠ - boolector_
uf ⚠ - boolector_
uf_ ⚠assignment - boolector_
ugt ⚠ - boolector_
ugte ⚠ - boolector_
ult ⚠ - boolector_
ulte ⚠ - boolector_
umulo ⚠ - boolector_
unsigned_ ⚠int - boolector_
urem ⚠ - boolector_
usubo ⚠ - boolector_
var ⚠ - boolector_
version ⚠ - boolector_
write ⚠ - boolector_
xnor ⚠ - boolector_
xor ⚠ - boolector_
zero ⚠