cprover
bv_dimacst Member List

This is the complete list of members for bv_dimacst, including all inherited members.

add_addr(const exprt &expr, bvt &bv)bv_pointerstprotectedvirtual
add_array_Ackermann_constraints()arraystprotected
add_array_constraint(const lazy_constraintt &lazy, bool refine=true)arraystprotected
add_array_constraints()arraystprotected
add_array_constraints(const index_sett &index_set, const exprt &expr)arraystprotected
add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)arraystprotected
add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)arraystprotected
add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)arraystprotected
add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)arraystprotected
add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)arraystprotected
add_equality_constraints()equalitytprotectedvirtual
add_equality_constraints(const typestructt &typestruct)equalitytprotectedvirtual
array_equalitiesarraystprotected
array_equalitiest typedefarraystprotected
arraysarraystprotected
arrayst(const namespacet &_ns, propt &_prop)arrayst
bitsbv_pointerstprotected
bluemessagetstatic
boldmessagetstatic
boolbv_set_equality_to_true(const equal_exprt &expr)boolbvtprotectedvirtual
boolbv_widthboolbvt
boolbvt(const namespacet &_ns, propt &_prop)boolbvtinline
bright_bluemessagetstatic
bright_cyanmessagetstatic
bright_greenmessagetstatic
bright_magentamessagetstatic
bright_redmessagetstatic
bright_yellowmessagetstatic
build_offset_map(const struct_typet &src)boolbvtprotected
bv_cacheboolbvtprotected
bv_cachet typedefboolbvtprotected
bv_dimacst(const namespacet &_ns, propt &_prop, const std::string &_filename)bv_dimacstinline
bv_get(const bvt &bv, const typet &type) constboolbvtprotected
bv_get_cache(const exprt &expr) constboolbvtprotected
bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const overridebv_pointerstprotectedvirtual
bv_get_unbounded_array(const exprt &) constboolbvtprotectedvirtual
bv_pointerst(const namespacet &_ns, propt &_prop)bv_pointerst
bv_utilsboolbvtprotected
cacheprop_conv_solvertprotected
cachet typedefprop_conv_solvert
clear_cache() overrideboolbvtinlinevirtual
collect_arrays(const exprt &a)arraystprotected
collect_indices()arraystprotected
collect_indices(const exprt &a)arraystprotected
command(unsigned c)messagetinlinestatic
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) constmessaget
conversion_failed(const exprt &expr, bvt &bv)boolbvtinlineprotected
conversion_failed(const exprt &expr)boolbvtprotected
convert(const exprt &expr) overrideprop_conv_solvertvirtual
convert_abs(const abs_exprt &expr)boolbvtprotectedvirtual
convert_add_sub(const exprt &expr)boolbvtprotectedvirtual
convert_address_of_rec(const exprt &expr, bvt &bv)bv_pointerstprotected
convert_array(const exprt &expr)boolbvtprotectedvirtual
convert_array_of(const array_of_exprt &expr)boolbvtprotectedvirtual
convert_bitvector(const exprt &expr) overridebv_pointerstprotectedvirtual
convert_bitwise(const exprt &expr)boolbvtprotectedvirtual
convert_bool(const exprt &expr)prop_conv_solvertprotectedvirtual
convert_bswap(const bswap_exprt &expr)boolbvtprotectedvirtual
convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)boolbvtvirtual
convert_bv_literals(const exprt &expr)boolbvtprotectedvirtual
convert_bv_reduction(const unary_exprt &expr)boolbvtprotectedvirtual
convert_bv_rel(const exprt &expr)boolbvtprotectedvirtual
convert_bv_typecast(const typecast_exprt &expr)boolbvtprotectedvirtual
convert_byte_extract(const byte_extract_exprt &expr)boolbvtprotectedvirtual
convert_byte_update(const byte_update_exprt &expr)boolbvtprotectedvirtual
convert_case(const exprt &expr)boolbvtprotectedvirtual
convert_complex(const complex_exprt &expr)boolbvtprotectedvirtual
convert_complex_imag(const complex_imag_exprt &expr)boolbvtprotectedvirtual
convert_complex_real(const complex_real_exprt &expr)boolbvtprotectedvirtual
convert_concatenation(const concatenation_exprt &expr)boolbvtprotectedvirtual
convert_cond(const cond_exprt &)boolbvtprotectedvirtual
convert_constant(const constant_exprt &expr)boolbvtprotectedvirtual
convert_constraint_select_one(const exprt &expr)boolbvtprotectedvirtual
convert_div(const div_exprt &expr)boolbvtprotectedvirtual
convert_equality(const equal_exprt &expr)boolbvtprotectedvirtual
convert_extractbit(const extractbit_exprt &expr)boolbvtprotectedvirtual
convert_extractbits(const extractbits_exprt &expr)boolbvtprotectedvirtual
convert_floatbv_op(const exprt &expr)boolbvtprotectedvirtual
convert_floatbv_typecast(const floatbv_typecast_exprt &expr)boolbvtprotectedvirtual
convert_function_application(const function_application_exprt &expr)boolbvtprotectedvirtual
convert_ieee_float_rel(const exprt &expr)boolbvtprotectedvirtual
convert_if(const if_exprt &expr)boolbvtprotectedvirtual
convert_index(const exprt &array, const mp_integer &index)boolbvtprotectedvirtual
convert_index(const index_exprt &expr)boolbvtprotectedvirtual
convert_lambda(const exprt &expr)boolbvtprotectedvirtual
convert_let(const let_exprt &)boolbvtprotectedvirtual
convert_member(const member_exprt &expr)boolbvtprotectedvirtual
convert_mod(const mod_exprt &expr)boolbvtprotectedvirtual
convert_mult(const mult_exprt &expr)boolbvtprotectedvirtual
convert_not(const not_exprt &expr)boolbvtprotectedvirtual
convert_onehot(const unary_exprt &expr)boolbvtprotectedvirtual
convert_overflow(const exprt &expr)boolbvtprotectedvirtual
convert_pointer_type(const exprt &expr)bv_pointerstprotectedvirtual
convert_power(const binary_exprt &expr)boolbvtprotectedvirtual
convert_quantifier(const quantifier_exprt &expr)boolbvtprotectedvirtual
convert_reduction(const unary_exprt &expr)boolbvtprotectedvirtual
convert_replication(const replication_exprt &expr)boolbvtprotectedvirtual
convert_rest(const exprt &expr) overridebv_pointerstprotectedvirtual
convert_shift(const binary_exprt &expr)boolbvtprotectedvirtual
convert_struct(const struct_exprt &expr)boolbvtprotectedvirtual
convert_symbol(const exprt &expr)boolbvtprotectedvirtual
convert_typecast(const typecast_exprt &expr)boolbvtprotectedvirtual
convert_unary_minus(const unary_minus_exprt &expr)boolbvtprotectedvirtual
convert_union(const union_exprt &expr)boolbvtprotectedvirtual
convert_update(const exprt &expr)boolbvtprotectedvirtual
convert_update_rec(const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)boolbvtprotected
convert_vector(const vector_exprt &expr)boolbvtprotectedvirtual
convert_verilog_case_equality(const binary_relation_exprt &expr)boolbvtprotectedvirtual
convert_with(const exprt &expr)boolbvtprotectedvirtual
convert_with(const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)boolbvtprotected
convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)boolbvtprotected
convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)boolbvtprotected
convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)boolbvtprotected
convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)boolbvtprotected
cyanmessagetstatic
debug() constmessagetinline
dec_solve() overrideprop_conv_solvertvirtual
decision_procedure_text() const overrideprop_conv_solvertinlinevirtual
decision_proceduret(const namespacet &_ns)decision_proceduretinlineexplicit
do_postponed(const postponedt &postponed)bv_pointerstprotected
elements_revt typedefequalitytprotected
elementst typedefequalitytprotected
encode(std::size_t object, bvt &bv)bv_pointerstprotected
eommessagetstatic
equalitiest typedefequalitytprotected
equality(const exprt &e1, const exprt &e2)equalitytvirtual
equality2(const exprt &e1, const exprt &e2)equalitytprotectedvirtual
equality_propagationprop_conv_solvert
equalityt(const namespacet &_ns, propt &_prop)equalitytinline
error() constmessagetinline
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)messagetstatic
expr_maparraystprotected
faintmessagetstatic
filenamebv_dimacstprotected
freeze_allprop_conv_solvert
functionsboolbvtprotected
get(const exprt &expr) const overrideboolbvtvirtual
get_bool(const exprt &expr, tvt &value) constprop_conv_solvertprotectedvirtual
get_cache() constprop_conv_solvertinline
get_literal(const irep_idt &symbol)prop_conv_solvertprotectedvirtual
get_map() constboolbvtinline
get_message_handler()messagetinline
get_mstream(unsigned message_level) constmessagetinline
get_symbols() constprop_conv_solvertinline
get_value(const bvt &bv)boolbvtinline
get_value(const bvt &bv, std::size_t offset, std::size_t width)boolbvt
greenmessagetstatic
has_is_in_conflict() const overrideprop_conv_solvertinlinevirtual
has_set_assumptions() const overrideprop_conv_solvertinlinevirtual
ignoring(const exprt &expr)prop_conv_solvertprotectedvirtual
incremental_cachearraystprotected
index_maparraystprotected
index_mapt typedefarraystprotected
index_sett typedefarraystprotected
is_in_conflict(literalt l) const overrideprop_conv_solvertinlinevirtual
is_unbounded_array(const typet &type) const overrideboolbvtprotectedvirtual
italicmessagetstatic
l_get(literalt a) const overrideprop_conv_solvertinlinevirtual
lazy_array_constraintsarraystprotected
lazy_arraysarraystprotected
lazy_typet enum namearraystprotected
literal(const exprt &expr, std::size_t bit, literalt &literal) constboolbvtvirtual
arrayst::literal(const symbol_exprt &expr, literalt &literal) constprop_conv_solvert
M_DEBUG enum valuemessaget
M_ERROR enum valuemessaget
M_PROGRESS enum valuemessaget
M_RESULT enum valuemessaget
M_STATISTICS enum valuemessaget
M_STATUS enum valuemessaget
M_WARNING enum valuemessaget
magentamessagetstatic
make_bv_expr(const typet &type, const bvt &bv)boolbvtprotectedvirtual
make_free_bv_expr(const typet &type)boolbvtprotectedvirtual
mapboolbvtprotected
message_handlermessagetprotected
message_levelt enum namemessaget
messaget()messagetinline
messaget(const messaget &other)messagetinline
messaget(message_handlert &_message_handler)messagetinlineexplicit
mstreammessagetmutableprotected
nsdecision_proceduretprotected
object_bitsbv_pointerstprotected
offset_arithmetic(bvt &bv, const mp_integer &x)bv_pointerstprotected
offset_arithmetic(bvt &bv, const mp_integer &factor, const exprt &index)bv_pointerstprotected
offset_arithmetic(bvt &bv, const mp_integer &factor, const bvt &index_bv)bv_pointerstprotected
offset_bitsbv_pointerstprotected
offset_mapt typedefboolbvtprotected
operator()(const exprt &expr)prop_convtinline
decision_proceduret::operator()()decision_proceduretinline
operator=(const messaget &other)messagetinline
pointer_logicbv_pointerstprotected
post_process() overridebv_pointerstvirtual
post_process_arrays()arraystinlineprotectedvirtual
post_process_quantifiers()boolbvtprotected
post_processing_doneprop_conv_solvertprotected
postponed_listbv_pointerstprotected
postponed_listt typedefbv_pointerstprotected
print_assignment(std::ostream &out) const overrideboolbvtvirtual
progress() constmessagetinline
propprop_conv_solvertprotected
prop_conv_solvert(const namespacet &_ns, propt &_prop)prop_conv_solvertinline
prop_convt(const namespacet &_ns)prop_convtinlineexplicit
quantifier_listboolbvtprotected
quantifier_listt typedefboolbvtprotected
record_array_equality(const equal_exprt &expr)arrayst
record_array_index(const index_exprt &expr)arrayst
redmessagetstatic
resetmessagetstatic
result() constmessagetinline
resultt enum namedecision_proceduret
set_all_frozen() overrideprop_conv_solvertinlinevirtual
set_assumptions(const bvt &_assumptions) overrideprop_conv_solvertinlinevirtual
set_equality_to_true(const equal_exprt &expr)prop_conv_solvertprotectedvirtual
set_frozen(literalt a) overrideprop_conv_solvertinlinevirtual
set_frozen(literalt a)prop_conv_solvert
set_frozen(const bvt &)prop_conv_solvert
prop_convt::set_frozen(const bvt &)prop_convtvirtual
set_message_handler(message_handlert &_message_handler)messagetinlinevirtual
set_time_limit_seconds(uint32_t lim) overrideprop_conv_solvertinlinevirtual
set_to(const exprt &expr, bool value) overrideboolbvtvirtual
set_to_false(const exprt &expr)decision_proceduretinline
set_to_true(const exprt &expr)decision_proceduretinline
statistics() constmessagetinline
status() constmessagetinline
string_numberingboolbvtprotected
SUB typedefbv_pointerstprotected
symbolsprop_conv_solvertprotected
symbolst typedefprop_conv_solvert
type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)boolbvtprotected
typemapequalitytprotected
typemapt typedefequalitytprotected
unbounded_arrayboolbvt
unbounded_arrayt enum nameboolbvt
underlinemessagetstatic
update_index_map(bool update_all)arraystprotected
update_index_map(std::size_t i)arraystprotected
update_indicesarraystprotected
use_cacheprop_conv_solvert
warning() constmessagetinline
write_dimacs(const std::string &filename)bv_dimacstprotected
write_dimacs(std::ostream &)bv_dimacstprotected
yellowmessagetstatic
~bv_dimacst()bv_dimacstinlinevirtual
~decision_proceduret()decision_proceduretvirtual
~messaget()messagetvirtual
~prop_conv_solvert()=defaultprop_conv_solvertvirtual
~prop_convt()prop_convtinlinevirtual