[−][src]Crate boolector_sys

Low-level bindings for the Boolector SMT solver.

Please see the Boolector C API documentation for function descriptions.

Structs

BoolectorAnonymous
BoolectorNode
Btor
BtorAbortCallback
BtorNode
_IO_FILE
_IO_marker

Constants

BtorOption_BTOR_OPT_ACKERMANN
BtorOption_BTOR_OPT_AIGPROP_USE_BANDIT
BtorOption_BTOR_OPT_AIGPROP_USE_RESTARTS
BtorOption_BTOR_OPT_AUTO_CLEANUP
BtorOption_BTOR_OPT_AUTO_CLEANUP_INTERNAL
BtorOption_BTOR_OPT_BETA_REDUCE_ALL
BtorOption_BTOR_OPT_CHK_FAILED_ASSUMPTIONS
BtorOption_BTOR_OPT_CHK_MODEL
BtorOption_BTOR_OPT_CHK_UNCONSTRAINED
BtorOption_BTOR_OPT_DECLSORT_BV_WIDTH
BtorOption_BTOR_OPT_DEFAULT_TO_CADICAL
BtorOption_BTOR_OPT_ELIMINATE_SLICES
BtorOption_BTOR_OPT_ENGINE
BtorOption_BTOR_OPT_EXIT_CODES
BtorOption_BTOR_OPT_EXTRACT_LAMBDAS
BtorOption_BTOR_OPT_FUN_DUAL_PROP
BtorOption_BTOR_OPT_FUN_DUAL_PROP_QSORT
BtorOption_BTOR_OPT_FUN_EAGER_LEMMAS
BtorOption_BTOR_OPT_FUN_JUST
BtorOption_BTOR_OPT_FUN_JUST_HEURISTIC
BtorOption_BTOR_OPT_FUN_LAZY_SYNTHESIZE
BtorOption_BTOR_OPT_FUN_PREPROP
BtorOption_BTOR_OPT_FUN_PRESLS
BtorOption_BTOR_OPT_FUN_STORE_LAMBDAS
BtorOption_BTOR_OPT_INCREMENTAL
BtorOption_BTOR_OPT_INCREMENTAL_RW
BtorOption_BTOR_OPT_INCREMENTAL_SMT1
BtorOption_BTOR_OPT_INPUT_FORMAT
BtorOption_BTOR_OPT_LOGLEVEL
BtorOption_BTOR_OPT_MERGE_LAMBDAS
BtorOption_BTOR_OPT_MODEL_GEN
BtorOption_BTOR_OPT_NORMALIZE
BtorOption_BTOR_OPT_NORMALIZE_ADD
BtorOption_BTOR_OPT_NUM_OPTS
BtorOption_BTOR_OPT_OUTPUT_FORMAT
BtorOption_BTOR_OPT_OUTPUT_NUMBER_FORMAT
BtorOption_BTOR_OPT_PARSE_INTERACTIVE
BtorOption_BTOR_OPT_PRETTY_PRINT
BtorOption_BTOR_OPT_PROP_FLIP_COND_CONST_DELTA
BtorOption_BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL
BtorOption_BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT
BtorOption_BTOR_OPT_PROP_NPROPS
BtorOption_BTOR_OPT_PROP_PATH_SEL
BtorOption_BTOR_OPT_PROP_PROB_AND_FLIP
BtorOption_BTOR_OPT_PROP_PROB_CONC_FLIP
BtorOption_BTOR_OPT_PROP_PROB_EQ_FLIP
BtorOption_BTOR_OPT_PROP_PROB_FLIP_COND
BtorOption_BTOR_OPT_PROP_PROB_FLIP_COND_CONST
BtorOption_BTOR_OPT_PROP_PROB_SLICE_FLIP
BtorOption_BTOR_OPT_PROP_PROB_SLICE_KEEP_DC
BtorOption_BTOR_OPT_PROP_PROB_USE_INV_VALUE
BtorOption_BTOR_OPT_PROP_USE_BANDIT
BtorOption_BTOR_OPT_PROP_USE_RESTARTS
BtorOption_BTOR_OPT_QUANT_CER
BtorOption_BTOR_OPT_QUANT_DER
BtorOption_BTOR_OPT_QUANT_DUAL_SOLVER
BtorOption_BTOR_OPT_QUANT_FIXSYNTH
BtorOption_BTOR_OPT_QUANT_MINISCOPE
BtorOption_BTOR_OPT_QUANT_SYNTH
BtorOption_BTOR_OPT_QUANT_SYNTH_ITE_COMPLETE
BtorOption_BTOR_OPT_QUANT_SYNTH_LIMIT
BtorOption_BTOR_OPT_QUANT_SYNTH_QI
BtorOption_BTOR_OPT_REWRITE_LEVEL
BtorOption_BTOR_OPT_SAT_ENGINE
BtorOption_BTOR_OPT_SAT_ENGINE_LGL_FORK
BtorOption_BTOR_OPT_SEED
BtorOption_BTOR_OPT_SIMPLIFY_CONSTRAINTS
BtorOption_BTOR_OPT_SKELETON_PREPROC
BtorOption_BTOR_OPT_SLS_JUST
BtorOption_BTOR_OPT_SLS_MOVE_GW
BtorOption_BTOR_OPT_SLS_MOVE_INC_MOVE_TEST
BtorOption_BTOR_OPT_SLS_MOVE_PROP
BtorOption_BTOR_OPT_SLS_MOVE_PROP_FORCE_RW
BtorOption_BTOR_OPT_SLS_MOVE_PROP_N_PROP
BtorOption_BTOR_OPT_SLS_MOVE_PROP_N_SLS
BtorOption_BTOR_OPT_SLS_MOVE_RAND_ALL
BtorOption_BTOR_OPT_SLS_MOVE_RAND_RANGE
BtorOption_BTOR_OPT_SLS_MOVE_RAND_WALK
BtorOption_BTOR_OPT_SLS_MOVE_RANGE
BtorOption_BTOR_OPT_SLS_MOVE_SEGMENT
BtorOption_BTOR_OPT_SLS_NFLIPS
BtorOption_BTOR_OPT_SLS_PROB_MOVE_RAND_WALK
BtorOption_BTOR_OPT_SLS_STRATEGY
BtorOption_BTOR_OPT_SLS_USE_BANDIT
BtorOption_BTOR_OPT_SLS_USE_RESTARTS
BtorOption_BTOR_OPT_SORT_AIG
BtorOption_BTOR_OPT_SORT_AIGVEC
BtorOption_BTOR_OPT_SORT_EXP
BtorOption_BTOR_OPT_UCOPT
BtorOption_BTOR_OPT_VAR_SUBST
BtorOption_BTOR_OPT_VERBOSITY
BtorSolverResult_BTOR_RESULT_SAT
BtorSolverResult_BTOR_RESULT_UNKNOWN
BtorSolverResult_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_bool_sort ^⚠
boolector_bv_assignment ^⚠
boolector_clone ^⚠
boolector_concat ^⚠
boolector_cond ^⚠
boolector_const ^⚠
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_node ^⚠
boolector_dump_smt2 ^⚠
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_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_ror ^⚠
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 ^⚠

Type Definitions

BoolectorSort
BtorOption
BtorSolverResult
FILE
_IO_lock_t
__int32_t
__off64_t
__off_t
__uint32_t