cprover
string_refinementt Member List

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

add_addr(const exprt &expr, bvt &bv)bv_pointerstprotectedvirtual
add_approximation(const exprt &expr, bvt &bv)bv_refinementtprotected
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
add_instantiations()string_refinementtprivate
add_lemma(const exprt &lemma, bool add_to_index_set=true)string_refinementtprivate
approximationsbv_refinementtprotected
approximationst typedefbv_refinementtprotected
array_equalitiesarraystprotected
array_equalitiest typedefarraystprotected
arraysarraystprotected
arrays_overapproximated()bv_refinementtprotected
arrayst(const namespacet &_ns, propt &_prop)arrayst
bitsbv_pointerstprotected
boolbv_set_equality_to_true(const equal_exprt &expr)string_refinementtprivatevirtual
boolbv_widthboolbvt
boolbvt(const namespacet &_ns, propt &_prop)boolbvtinline
build_offset_map(const struct_typet &src, offset_mapt &dest)boolbvtprotected
bv_cacheboolbvtprotected
bv_cachet typedefboolbvtprotected
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_refinementt(const namespacet &_ns, propt &_prop)bv_refinementt
bv_utilsboolbvtprotected
cacheprop_conv_solvertprotected
cachet typedefprop_conv_solvert
check_axioms()string_refinementtprivate
check_SAT(approximationt &approximation)bv_refinementtprotected
check_SAT()bv_refinementtprotectedvirtual
check_UNSAT(approximationt &approximation)bv_refinementtprotected
check_UNSAT()bv_refinementtprotectedvirtual
clear_cache() overrideboolbvtinlinevirtual
collect_arrays(const exprt &a)arraystprotected
collect_indices()arraystprotected
collect_indices(const exprt &a)arraystprotected
compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)string_refinementtprivate
conversion_failed(const exprt &expr, bvt &bv)boolbvtinlineprotected
conversion_failed(const exprt &expr)boolbvtprotected
convert(const exprt &expr) overrideprop_conv_solvertvirtual
convert_abs(const 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_bool_bv(const exprt &boole, const exprt &orig)string_refinementtprotected
convert_bv(const exprt &expr)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 exprt &expr)boolbvtprotectedvirtual
convert_complex_imag(const exprt &expr)boolbvtprotectedvirtual
convert_complex_real(const exprt &expr)boolbvtprotectedvirtual
convert_concatenation(const exprt &expr)boolbvtprotectedvirtual
convert_cond(const exprt &expr)boolbvtprotectedvirtual
convert_constant(const constant_exprt &expr)boolbvtprotectedvirtual
convert_constraint_select_one(const exprt &expr)boolbvtprotectedvirtual
convert_div(const div_exprt &expr)bv_refinementtprotectedvirtual
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)bv_refinementtprotectedvirtual
convert_floatbv_typecast(const floatbv_typecast_exprt &expr)boolbvtprotectedvirtual
convert_function_application(const function_application_exprt &expr)string_refinementtprotectedvirtual
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_member(const member_exprt &expr)boolbvtprotectedvirtual
convert_mod(const mod_exprt &expr)bv_refinementtprotectedvirtual
convert_mult(const exprt &expr)bv_refinementtprotectedvirtual
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 exprt &expr)boolbvtprotectedvirtual
convert_reduction(const unary_exprt &expr)boolbvtprotectedvirtual
convert_replication(const replication_exprt &expr)boolbvtprotectedvirtual
convert_rest(const exprt &expr)string_refinementtprivatevirtual
convert_shift(const binary_exprt &expr)boolbvtprotectedvirtual
convert_struct(const struct_exprt &expr)boolbvtprotectedvirtual
convert_symbol(const exprt &expr)string_refinementtprotectedvirtual
convert_typecast(const typecast_exprt &expr)boolbvtprotectedvirtual
convert_unary_minus(const unary_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 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 typet &type, 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 &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)boolbvtprotected
curstring_refinementtprivate
current_index_setstring_refinementtprivate
debug()messagetinline
dec_solve()string_refinementtprotectedvirtual
decision_procedure_text() conststring_refinementtinlinevirtual
decision_proceduret(const namespacet &_ns)decision_proceduretinlineexplicit
display_index_set()string_refinementtprivate
do_arithmetic_refinementbv_refinementt
do_array_refinementbv_refinementt
do_postponed(const postponedt &postponed)bv_pointerstprotected
elements_revt typedefequalitytprotected
elementst typedefequalitytprotected
encode(std::size_t object, bvt &bv)bv_pointerstprotected
endl(mstreamt &m)messagetinlinestatic
eom(mstreamt &m)messagetinlinestatic
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()messagetinline
expr_maparraystprotected
expr_sett typedefstring_refinementtprotected
freeze_allprop_conv_solvert
freeze_lazy_constraints()bv_refinementtprotected
functionsboolbvtprotected
generatorstring_refinementtprivate
get(const exprt &expr) const overrideboolbvtvirtual
get_array(const exprt &arr, const exprt &size)string_refinementtprivate
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)messagetinline
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
get_values(approximationt &approximation)bv_refinementtprotected
has_is_in_conflict() const overrideprop_conv_solvertinlinevirtual
has_set_assumptions() const overrideprop_conv_solvertinlinevirtual
ignoring(const exprt &expr)prop_conv_solvertprotectedvirtual
in_core(const exprt &expr)decision_proceduretvirtual
incremental_cachearraystprotected
index_maparraystprotected
index_mapt typedefarraystprotected
index_setstring_refinementtprivate
index_sett typedefarraystprotected
initial_index_set(const string_constraintt &axiom)string_refinementtprivate
initial_index_set(const std::vector< string_constraintt > &string_axioms)string_refinementtprivate
initial_loop_boundstring_refinementtprivate
initialize(approximationt &approximation)bv_refinementtprotected
instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)string_refinementtprivate
instantiate_not_contains(const string_not_contains_constraintt &axiom, std::list< exprt > &new_lemmas)string_refinementtprivate
is_in_conflict(approximationt &approximation)bv_refinementtprotected
bv_pointerst::is_in_conflict(literalt l) const overrideprop_conv_solvertinlinevirtual
is_positive(const exprt &x)string_refinementtstatic
is_ptr(const typet &type)bv_pointerstinlineprotectedstatic
is_unbounded_array(const typet &type) const overrideboolbvtprotectedvirtual
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 exprt &expr, literalt &literal) constprop_conv_solvertvirtual
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
make_bv_expr(const typet &type, const bvt &bv, exprt &dest)boolbvtprotectedvirtual
make_free_bv_expr(const typet &type, exprt &dest)boolbvtprotectedvirtual
mapboolbvtprotected
map_representation_of_sum(const exprt &f) conststring_refinementtprivate
max_node_refinementbv_refinementt
message_handlermessagetprotected
message_levelt enum namemessaget
messaget()messagetinline
messaget(const messaget &other)messagetinline
messaget(message_handlert &_message_handler)messagetinlineexplicit
mstreammessagetprotected
not_contains_axiomsstring_refinementtprivate
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
parent_assumptionsbv_refinementtprotected
pointer_logicbv_pointerstprotected
post_process() overridebv_pointerstvirtual
post_process_arrays()bv_refinementtprotectedvirtual
post_process_quantifiers()boolbvtprotected
post_processing_doneprop_conv_solvertprotected
postponed_listbv_pointerstprotected
postponed_listt typedefbv_pointerstprotected
print_assignment(std::ostream &out) const overrideboolbvtvirtual
progressbv_refinementtprotected
bv_pointerst::progress()messagetinline
propprop_conv_solvertprotected
prop_conv_solvert(const namespacet &_ns, propt &_prop)prop_conv_solvertinline
prop_convt(const namespacet &_ns)prop_convtinlineexplicit
prop_solve()bv_refinementtprotected
quantifier_listboolbvtprotected
quantifier_listt typedefboolbvtprotected
record_array_equality(const equal_exprt &expr)arrayst
record_array_index(const index_exprt &expr)arrayst
result()messagetinline
resultt enum namedecision_proceduret
seen_instancesstring_refinementtprivate
set_all_frozen() overrideprop_conv_solvertinlinevirtual
set_assumptions(const bvt &_assumptions)bv_refinementtprotectedvirtual
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_mode()string_refinementt
set_to(const exprt &expr, bool value)bv_refinementtprotectedvirtual
set_to_false(const exprt &expr)decision_proceduretinline
set_to_true(const exprt &expr)decision_proceduretinline
set_ui(language_uit::uit _ui)bv_refinementtinline
simplify_sum(const exprt &f) conststring_refinementtprivate
statistics()messagetinline
status()messagetinline
string_numberingboolbvtprotected
string_of_array(const exprt &arr, const exprt &size) conststring_refinementtprivate
string_refinementt(const namespacet &_ns, propt &_prop, unsigned refinement_bound)string_refinementt
SUB typedefbv_refinementt
sum_over_map(std::map< exprt, int > &m, bool negated=false) conststring_refinementtprivate
supert typedefstring_refinementtprivate
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
uibv_refinementtprotected
unbounded_arrayboolbvt
unbounded_arrayt enum nameboolbvt
universal_axiomsstring_refinementtprivate
update_index_map(bool update_all)arraystprotected
update_index_map(std::size_t i)arraystprotected
update_index_set(const exprt &formula)string_refinementtprivate
update_index_set(const std::vector< exprt > &cur)string_refinementtprivate
update_indicesarraystprotected
use_cacheprop_conv_solvert
use_counter_examplestring_refinementt
warning()messagetinline
~bv_refinementt()bv_refinementt
~messaget()messagetvirtual
~prop_conv_solvert()prop_conv_solvertinlinevirtual
~prop_convt()prop_convtinlinevirtual