|
| string_refinementt (const infot &) |
|
std::string | decision_procedure_text () const override |
|
exprt | get (const exprt &expr) const override |
| Evaluates the given expression in the valuation found by string_refinementt::dec_solve. More...
|
|
void | set_to (const exprt &expr, bool value) override |
| Record the constraints to ensure that the expression is true when the boolean is true and false otherwise. More...
|
|
decision_proceduret::resultt | dec_solve () override |
| Main decision procedure of the solver. More...
|
|
| bv_refinementt (const infot &info) |
|
| bv_pointerst (const namespacet &_ns, propt &_prop) |
|
void | post_process () override |
|
| boolbvt (const namespacet &_ns, propt &_prop) |
|
virtual const bvt & | convert_bv (const exprt &expr, const optionalt< std::size_t > expected_width=nullopt) |
|
void | print_assignment (std::ostream &out) const override |
|
void | clear_cache () override |
|
virtual bool | literal (const exprt &expr, std::size_t bit, literalt &literal) const |
|
mp_integer | get_value (const bvt &bv) |
|
mp_integer | get_value (const bvt &bv, std::size_t offset, std::size_t width) |
|
const boolbv_mapt & | get_map () const |
|
| arrayst (const namespacet &_ns, propt &_prop) |
|
literalt | record_array_equality (const equal_exprt &expr) |
|
void | record_array_index (const index_exprt &expr) |
|
| equalityt (const namespacet &_ns, propt &_prop) |
|
virtual literalt | equality (const exprt &e1, const exprt &e2) |
|
void | post_process () override |
|
| prop_conv_solvert (const namespacet &_ns, propt &_prop) |
|
virtual | ~prop_conv_solvert ()=default |
|
void | print_assignment (std::ostream &out) const override |
|
virtual tvt | l_get (literalt a) const override |
|
void | set_frozen (literalt a) override |
|
bool | has_set_assumptions () const override |
|
void | set_all_frozen () override |
|
literalt | convert (const exprt &expr) override |
|
bool | is_in_conflict (literalt l) const override |
| determine whether a variable is in the final conflict More...
|
|
bool | has_is_in_conflict () const override |
|
bool | literal (const symbol_exprt &expr, literalt &literal) const |
|
const cachet & | get_cache () const |
|
const symbolst & | get_symbols () const |
|
void | set_time_limit_seconds (uint32_t lim) override |
|
virtual void | set_frozen (literalt a) |
|
virtual void | set_frozen (const bvt &) |
|
| prop_convt (const namespacet &_ns) |
|
virtual | ~prop_convt () |
|
literalt | operator() (const exprt &expr) |
|
virtual void | set_frozen (const bvt &) |
|
| decision_proceduret (const namespacet &_ns) |
|
virtual | ~decision_proceduret () |
|
void | set_to_true (const exprt &expr) |
|
void | set_to_false (const exprt &expr) |
|
resultt | operator() () |
|
virtual void | set_message_handler (message_handlert &_message_handler) |
|
message_handlert & | get_message_handler () |
|
| messaget () |
|
| messaget (const messaget &other) |
|
messaget & | operator= (const messaget &other) |
|
| messaget (message_handlert &_message_handler) |
|
virtual | ~messaget () |
|
mstreamt & | get_mstream (unsigned message_level) const |
|
mstreamt & | error () const |
|
mstreamt & | warning () const |
|
mstreamt & | result () const |
|
mstreamt & | status () const |
|
mstreamt & | statistics () const |
|
mstreamt & | progress () const |
|
mstreamt & | debug () const |
|
void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
| Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream . More...
|
|
|
enum | unbounded_arrayt { unbounded_arrayt::U_NONE,
unbounded_arrayt::U_ALL,
unbounded_arrayt::U_AUTO
} |
|
typedef equalityt | SUB |
|
typedef std::map< irep_idt, literalt > | symbolst |
|
typedef std::unordered_map< exprt, literalt, irep_hash > | cachet |
|
enum | resultt { resultt::D_SATISFIABLE,
resultt::D_UNSATISFIABLE,
resultt::D_ERROR
} |
|
enum | message_levelt {
M_ERROR =1,
M_WARNING =2,
M_RESULT =4,
M_STATUS =6,
M_STATISTICS =8,
M_PROGRESS =9,
M_DEBUG =10
} |
|
static unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
| Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
|
|
static commandt | command (unsigned c) |
| Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
|
|
unbounded_arrayt | unbounded_array |
|
boolbv_widtht | boolbv_width |
|
bool | use_cache = true |
|
bool | equality_propagation = true |
|
bool | freeze_all = false |
|
static eomt | eom |
|
static const commandt | reset |
| return to default formatting, as defined by the terminal More...
|
|
static const commandt | red |
| render text with red foreground color More...
|
|
static const commandt | green |
| render text with green foreground color More...
|
|
static const commandt | yellow |
| render text with yellow foreground color More...
|
|
static const commandt | blue |
| render text with blue foreground color More...
|
|
static const commandt | magenta |
| render text with magenta foreground color More...
|
|
static const commandt | cyan |
| render text with cyan foreground color More...
|
|
static const commandt | bright_red |
| render text with bright red foreground color More...
|
|
static const commandt | bright_green |
| render text with bright green foreground color More...
|
|
static const commandt | bright_yellow |
| render text with bright yellow foreground color More...
|
|
static const commandt | bright_blue |
| render text with bright blue foreground color More...
|
|
static const commandt | bright_magenta |
| render text with bright magenta foreground color More...
|
|
static const commandt | bright_cyan |
| render text with bright cyan foreground color More...
|
|
static const commandt | bold |
| render text with bold font More...
|
|
static const commandt | faint |
| render text with faint font More...
|
|
static const commandt | italic |
| render italic text More...
|
|
static const commandt | underline |
| render underlined text More...
|
|
typedef boolbvt | SUB |
|
typedef std::list< postponedt > | postponed_listt |
|
typedef arrayst | SUB |
|
typedef std::unordered_map< const exprt, bvt, irep_hash > | bv_cachet |
|
typedef std::list< quantifiert > | quantifier_listt |
|
typedef std::vector< std::size_t > | offset_mapt |
|
enum | lazy_typet {
lazy_typet::ARRAY_ACKERMANN,
lazy_typet::ARRAY_WITH,
lazy_typet::ARRAY_IF,
lazy_typet::ARRAY_OF,
lazy_typet::ARRAY_TYPECAST
} |
|
typedef std::list< array_equalityt > | array_equalitiest |
|
typedef std::set< exprt > | index_sett |
|
typedef std::map< std::size_t, index_sett > | index_mapt |
|
typedef std::unordered_map< const exprt, unsigned, irep_hash > | elementst |
|
typedef std::map< std::pair< unsigned, unsigned >, literalt > | equalitiest |
|
typedef std::map< unsigned, exprt > | elements_revt |
|
typedef std::unordered_map< const typet, typestructt, irep_hash > | typemapt |
|
void | post_process_arrays () override |
| generate array constraints More...
|
|
bvt | convert_mult (const mult_exprt &expr) override |
|
bvt | convert_div (const div_exprt &expr) override |
|
bvt | convert_mod (const mod_exprt &expr) override |
|
bvt | convert_floatbv_op (const exprt &expr) override |
|
void | set_assumptions (const bvt &_assumptions) override |
|
void | encode (std::size_t object, bvt &bv) |
|
virtual bvt | convert_pointer_type (const exprt &expr) |
|
virtual void | add_addr (const exprt &expr, bvt &bv) |
|
literalt | convert_rest (const exprt &expr) override |
|
bvt | convert_bitvector (const exprt &expr) override |
| Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit. More...
|
|
exprt | bv_get_rec (const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override |
|
bool | convert_address_of_rec (const exprt &expr, bvt &bv) |
|
void | offset_arithmetic (bvt &bv, const mp_integer &x) |
|
void | offset_arithmetic (bvt &bv, const mp_integer &factor, const exprt &index) |
|
void | offset_arithmetic (bvt &bv, const mp_integer &factor, const bvt &index_bv) |
|
void | do_postponed (const postponedt &postponed) |
|
virtual bool | boolbv_set_equality_to_true (const equal_exprt &expr) |
|
void | conversion_failed (const exprt &expr, bvt &bv) |
|
bvt | conversion_failed (const exprt &expr) |
|
bool | type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest) |
|
virtual literalt | convert_bv_rel (const exprt &expr) |
|
virtual literalt | convert_typecast (const typecast_exprt &expr) |
| conversion from bitvector types to boolean More...
|
|
virtual literalt | convert_reduction (const unary_exprt &expr) |
|
virtual literalt | convert_onehot (const unary_exprt &expr) |
|
virtual literalt | convert_extractbit (const extractbit_exprt &expr) |
|
virtual literalt | convert_overflow (const exprt &expr) |
|
virtual literalt | convert_equality (const equal_exprt &expr) |
|
virtual literalt | convert_verilog_case_equality (const binary_relation_exprt &expr) |
|
virtual literalt | convert_ieee_float_rel (const exprt &expr) |
|
virtual literalt | convert_quantifier (const quantifier_exprt &expr) |
|
virtual bvt | convert_index (const exprt &array, const mp_integer &index) |
| index operator with constant index More...
|
|
virtual bvt | convert_index (const index_exprt &expr) |
|
virtual bvt | convert_bswap (const bswap_exprt &expr) |
|
virtual bvt | convert_byte_extract (const byte_extract_exprt &expr) |
|
virtual bvt | convert_byte_update (const byte_update_exprt &expr) |
|
virtual bvt | convert_constraint_select_one (const exprt &expr) |
|
virtual bvt | convert_if (const if_exprt &expr) |
|
virtual bvt | convert_struct (const struct_exprt &expr) |
|
virtual bvt | convert_array (const exprt &expr) |
|
virtual bvt | convert_vector (const vector_exprt &expr) |
|
virtual bvt | convert_complex (const complex_exprt &expr) |
|
virtual bvt | convert_complex_real (const complex_real_exprt &expr) |
|
virtual bvt | convert_complex_imag (const complex_imag_exprt &expr) |
|
virtual bvt | convert_lambda (const exprt &expr) |
|
virtual bvt | convert_let (const let_exprt &) |
|
virtual bvt | convert_array_of (const array_of_exprt &expr) |
|
virtual bvt | convert_union (const union_exprt &expr) |
|
virtual bvt | convert_bv_typecast (const typecast_exprt &expr) |
|
virtual bvt | convert_add_sub (const exprt &expr) |
|
virtual bvt | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
|
virtual bvt | convert_member (const member_exprt &expr) |
|
virtual bvt | convert_with (const exprt &expr) |
|
virtual bvt | convert_update (const exprt &expr) |
|
virtual bvt | convert_case (const exprt &expr) |
|
virtual bvt | convert_cond (const cond_exprt &) |
|
virtual bvt | convert_shift (const binary_exprt &expr) |
|
virtual bvt | convert_bitwise (const exprt &expr) |
|
virtual bvt | convert_unary_minus (const unary_minus_exprt &expr) |
|
virtual bvt | convert_abs (const abs_exprt &expr) |
|
virtual bvt | convert_concatenation (const concatenation_exprt &expr) |
|
virtual bvt | convert_replication (const replication_exprt &expr) |
|
virtual bvt | convert_bv_literals (const exprt &expr) |
|
virtual bvt | convert_constant (const constant_exprt &expr) |
|
virtual bvt | convert_extractbits (const extractbits_exprt &expr) |
|
virtual bvt | convert_symbol (const exprt &expr) |
|
virtual bvt | convert_bv_reduction (const unary_exprt &expr) |
|
virtual bvt | convert_not (const not_exprt &expr) |
|
virtual bvt | convert_power (const binary_exprt &expr) |
|
virtual bvt | convert_function_application (const function_application_exprt &expr) |
|
virtual exprt | make_bv_expr (const typet &type, const bvt &bv) |
|
virtual exprt | make_free_bv_expr (const typet &type) |
|
void | convert_with (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
|
void | convert_with_bv (const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
|
void | convert_with_array (const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
|
void | convert_with_union (const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
|
void | convert_with_struct (const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
|
void | convert_update_rec (const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv) |
|
virtual exprt | bv_get_unbounded_array (const exprt &) const |
|
exprt | bv_get (const bvt &bv, const typet &type) const |
|
exprt | bv_get_cache (const exprt &expr) const |
|
bool | is_unbounded_array (const typet &type) const override |
|
void | post_process_quantifiers () |
|
offset_mapt | build_offset_map (const struct_typet &src) |
|
void | add_array_constraint (const lazy_constraintt &lazy, bool refine=true) |
| adds array constraints (refine=true...lazily for the refinement loop) More...
|
|
void | add_array_constraints () |
|
void | add_array_Ackermann_constraints () |
|
void | add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality) |
|
void | add_array_constraints (const index_sett &index_set, const exprt &expr) |
|
void | add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt) |
|
void | add_array_constraints_with (const index_sett &index_set, const with_exprt &expr) |
|
void | add_array_constraints_update (const index_sett &index_set, const update_exprt &expr) |
|
void | add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt) |
|
void | update_index_map (bool update_all) |
|
void | update_index_map (std::size_t i) |
| merge the indices into the root More...
|
|
void | collect_arrays (const exprt &a) |
|
void | collect_indices () |
|
void | collect_indices (const exprt &a) |
|
virtual literalt | equality2 (const exprt &e1, const exprt &e2) |
|
virtual void | add_equality_constraints () |
|
virtual void | add_equality_constraints (const typestructt &typestruct) |
|
virtual bool | get_bool (const exprt &expr, tvt &value) const |
| get a boolean value from counter example if not valid More...
|
|
virtual literalt | convert_bool (const exprt &expr) |
|
virtual bool | set_equality_to_true (const equal_exprt &expr) |
|
virtual literalt | get_literal (const irep_idt &symbol) |
|
virtual void | ignoring (const exprt &expr) |
|
configt | config_ |
|
pointer_logict | pointer_logic |
|
unsigned | object_bits |
|
unsigned | offset_bits |
|
unsigned | bits |
|
postponed_listt | postponed_list |
|
bv_utilst | bv_utils |
|
functionst | functions |
|
boolbv_mapt | map |
|
bv_cachet | bv_cache |
|
quantifier_listt | quantifier_list |
|
numbering< irep_idt > | string_numbering |
|
array_equalitiest | array_equalities |
|
union_find< exprt > | arrays |
|
index_mapt | index_map |
|
bool | lazy_arrays |
|
bool | incremental_cache |
|
std::list< lazy_constraintt > | lazy_array_constraints |
|
std::map< exprt, bool > | expr_map |
|
std::set< std::size_t > | update_indices |
|
typemapt | typemap |
|
bool | post_processing_done = false |
|
symbolst | symbols |
|
cachet | cache |
|
propt & | prop |
|
const namespacet & | ns |
|
message_handlert * | message_handler |
|
mstreamt | mstream |
|