bv_minimizing_dect Class Reference
#include <bv_minimize.h>
Inheritance diagram for bv_minimizing_dect: Collaboration diagram for bv_minimizing_dect:Public Member Functions | |
| virtual const std::string | description () |
| bv_minimizing_dect (const namespacet &_ns, message_handlert &message_handler) | |
| void | minimize (const minimization_listt &objectives) |
| Public Member Functions inherited from bv_pointerst | |
| bv_pointerst (const namespacet &, propt &, message_handlert &, bool get_array_constraints=false) | |
| void | finish_eager_conversion () override |
| endianness_mapt | endianness_map (const typet &, bool little_endian) const override |
| Public Member Functions inherited from boolbvt | |
| boolbvt (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false) | |
| virtual const bvt & | convert_bv (const exprt &expr, const std::optional< std::size_t > expected_width={}) |
| Convert expression to vector of literalts, using an internal cache to speed up conversion if available. More... | |
| exprt | get (const exprt &expr) const override |
Return expr with variables replaced by values from satisfying assignment if available. More... | |
| void | set_to (const exprt &expr, bool value) override |
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'. More... | |
| void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out. More... | |
| exprt | handle (const exprt &) override |
| Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to. More... | |
| void | clear_cache () override |
| 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 |
| virtual std::size_t | boolbv_width (const typet &type) const |
| virtual endianness_mapt | endianness_map (const typet &type) const |
| Public Member Functions inherited from arrayst | |
| arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false) | |
| literalt | record_array_equality (const equal_exprt &expr) |
| void | record_array_index (const index_exprt &expr) |
| Public Member Functions inherited from equalityt | |
| equalityt (propt &_prop, message_handlert &message_handler) | |
| virtual literalt | equality (const exprt &e1, const exprt &e2) |
| void | finish_eager_conversion () override |
| Public Member Functions inherited from prop_conv_solvert | |
| prop_conv_solvert (propt &_prop, message_handlert &message_handler) | |
| virtual | ~prop_conv_solvert ()=default |
| decision_proceduret::resultt | dec_solve (const exprt &) override |
| Implementation of the decision procedure. More... | |
| void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out. More... | |
| std::string | decision_procedure_text () const override |
| Return a textual description of the decision procedure. More... | |
| exprt | get (const exprt &expr) const override |
Return expr with variables replaced by values from satisfying assignment if available. More... | |
| tvt | l_get (literalt a) const override |
Return value of literal l from satisfying assignment. More... | |
| exprt | handle (const exprt &expr) override |
| Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to. More... | |
| void | set_frozen (literalt) |
| void | set_frozen (const bvt &) |
| void | set_all_frozen () |
| literalt | convert (const exprt &expr) override |
| Convert a Boolean expression and return the corresponding literal. More... | |
| bool | is_in_conflict (const exprt &expr) const override |
| Returns true if an expression is in the final conflict leading to UNSAT. More... | |
| void | set_to (const exprt &expr, bool value) override |
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true, otherwise add 'current_context => not expr'. More... | |
| void | push () override |
| Push a new context on the stack This context becomes a child context nested in the current context. More... | |
| void | push (const std::vector< exprt > &assumptions) override |
Push assumptions in form of literal_exprt More... | |
| void | pop () override |
| Pop whatever is on top of the stack. More... | |
| const cachet & | get_cache () const |
| const symbolst & | get_symbols () const |
| void | set_time_limit_seconds (uint32_t lim) override |
| Set the limit for the solver to time out in seconds. More... | |
| std::size_t | get_number_of_solver_calls () const override |
| Return the number of incremental solver calls. More... | |
| hardness_collectort * | get_hardness_collector () |
| Public Member Functions inherited from conflict_providert | |
| virtual | ~conflict_providert ()=default |
| Public Member Functions inherited from prop_convt | |
| virtual | ~prop_convt () |
| Public Member Functions inherited from stack_decision_proceduret | |
| virtual | ~stack_decision_proceduret ()=default |
| Public Member Functions inherited from decision_proceduret | |
| void | set_to_true (const exprt &) |
For a Boolean expression expr, add the constraint 'expr'. More... | |
| void | set_to_false (const exprt &) |
For a Boolean expression expr, add the constraint 'not expr'. More... | |
| resultt | operator() () |
| Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. More... | |
| resultt | operator() (const exprt &assumption) |
| Run the decision procedure to solve the problem under the given assumption. More... | |
| virtual | ~decision_proceduret () |
| Public Member Functions inherited from solver_resource_limitst | |
| virtual | ~solver_resource_limitst ()=default |
Public Attributes | |
| satcheckt | satcheck |
| messaget | log |
| Public Attributes inherited from boolbvt | |
| unbounded_arrayt | unbounded_array |
| Public Attributes inherited from prop_conv_solvert | |
| bool | use_cache = true |
| bool | equality_propagation = true |
| bool | freeze_all = false |
Additional Inherited Members | |
| Public Types inherited from boolbvt | |
| enum class | unbounded_arrayt { U_NONE , U_ALL , U_AUTO } |
| Public Types inherited from arrayst | |
| typedef equalityt | SUB |
| Public Types inherited from equalityt | |
| using | SUB = prop_conv_solvert |
| Public Types inherited from prop_conv_solvert | |
| typedef std::map< irep_idt, literalt > | symbolst |
| typedef std::unordered_map< exprt, literalt, irep_hash > | cachet |
| Public Types inherited from decision_proceduret | |
| enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
| Result of running the decision procedure. More... | |
| Protected Types inherited from bv_pointerst | |
| typedef boolbvt | SUB |
| typedef std::list< postponedt > | postponed_listt |
| Protected Types inherited from boolbvt | |
| 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 |
| Protected Types inherited from arrayst | |
| enum class | lazy_typet { ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF , ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_LET } |
| enum class | constraint_typet { ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF , ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_EQUALITY , ARRAY_LET } |
| 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::map< constraint_typet, size_t > | array_constraint_countt |
| Protected Types inherited from equalityt | |
| 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 |
| Protected Member Functions inherited from bv_pointerst | |
| std::size_t | get_object_width (const pointer_typet &) const |
| std::size_t | get_offset_width (const pointer_typet &) const |
| std::size_t | get_address_width (const pointer_typet &) const |
| bvt | encode (const mp_integer &object, const pointer_typet &) const |
| virtual bvt | convert_pointer_type (const exprt &) |
| virtual bvt | add_addr (const exprt &) |
| literalt | convert_rest (const exprt &) override |
| bvt | convert_bitvector (const exprt &) 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 exprt &, const bvt &, std::size_t offset) const override |
| std::optional< bvt > | convert_address_of_rec (const exprt &) |
| bvt | offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &) |
| bvt | offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const exprt &index) |
| bvt | offset_arithmetic (const pointer_typet &type, const bvt &bv, const exprt &factor, const exprt &index) |
| bvt | offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const bvt &index_bv) |
| std::pair< exprt, exprt > | prepare_postponed_is_dynamic_object (std::vector< symbol_exprt > &placeholders) const |
Create Boolean functions describing all dynamic and all not-dynamic object encodings over placeholders as input Boolean variables representing object bits. More... | |
| std::unordered_map< exprt, exprt, irep_hash > | prepare_postponed_object_size (std::vector< symbol_exprt > &placeholders) const |
Create Boolean functions describing all objects of each known object size over placeholders as input Boolean variables representing object bits. More... | |
| bvt | object_literals (const bvt &bv, const pointer_typet &type) const |
Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to. More... | |
| bvt | offset_literals (const bvt &bv, const pointer_typet &type) const |
Given a pointer encoded in bv, extract the literals representing the offset into an object that the pointer points to. More... | |
| Protected Member Functions inherited from boolbvt | |
| virtual bool | boolbv_set_equality_to_true (const equal_exprt &expr) |
| bvt | conversion_failed (const exprt &expr) |
| Print that the expression of x has failed conversion, then return a vector of x's width. More... | |
| bool | type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest) |
| virtual literalt | convert_bv_rel (const binary_relation_exprt &) |
| Flatten <, >, <= and >= expressions. More... | |
| 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_binary_overflow (const binary_overflow_exprt &expr) |
| virtual literalt | convert_unary_overflow (const unary_overflow_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 binary_relation_exprt &) |
| 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) |
| Flatten array. More... | |
| 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_array_comprehension (const array_comprehension_exprt &) |
| virtual bvt | convert_let (const let_exprt &) |
| virtual bvt | convert_array_of (const array_of_exprt &expr) |
| Flatten arrays constructed from a single element. More... | |
| virtual bvt | convert_union (const union_exprt &expr) |
| virtual bvt | convert_empty_union (const empty_union_exprt &expr) |
| virtual bvt | convert_bv_typecast (const typecast_exprt &expr) |
| virtual bvt | convert_add_sub (const exprt &expr) |
| virtual bvt | convert_mult (const mult_exprt &expr) |
| virtual bvt | convert_div (const div_exprt &expr) |
| virtual bvt | convert_mod (const mod_exprt &expr) |
| virtual bvt | convert_floatbv_op (const ieee_float_op_exprt &) |
| virtual bvt | convert_floatbv_mod_rem (const binary_exprt &) |
| virtual bvt | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
| virtual bvt | convert_member (const member_exprt &expr) |
| virtual bvt | convert_with (const with_exprt &expr) |
| virtual bvt | convert_update (const update_exprt &) |
| virtual bvt | convert_update_bit (const update_bit_exprt &) |
| virtual bvt | convert_update_bits (const update_bits_exprt &) |
| 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_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 bvt | convert_bitreverse (const bitreverse_exprt &expr) |
| virtual bvt | convert_saturating_add_sub (const binary_exprt &expr) |
| virtual bvt | convert_overflow_result (const overflow_result_exprt &expr) |
| bvt | convert_update_bits (bvt src, const exprt &index, const bvt &new_value) |
| void | convert_with (const typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
| void | convert_with_bv (const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
| void | convert_with_array (const array_typet &type, const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
| void | convert_with_union (const union_typet &type, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
| void | convert_with_struct (const struct_typet &type, const exprt &where, const exprt &new_value, 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 | finish_eager_conversion_quantifiers () |
| offset_mapt | build_offset_map (const struct_typet &src) |
| binding_exprt::variablest | fresh_binding (const binding_exprt &) |
| create new, unique variables for the given binding More... | |
| Protected Member Functions inherited from arrayst | |
| virtual void | finish_eager_conversion_arrays () |
| void | add_array_constraint (const lazy_constraintt &lazy, bool refine=true) |
| adds array constraints (refine=true...lazily for the refinement loop) More... | |
| void | display_array_constraint_count () |
| std::string | enum_to_string (constraint_typet) |
| 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 | add_array_constraints_array_constant (const index_sett &index_set, const array_exprt &exprt) |
| void | add_array_constraints_comprehension (const index_sett &index_set, const array_comprehension_exprt &expr) |
| 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) |
| Protected Member Functions inherited from equalityt | |
| virtual literalt | equality2 (const exprt &e1, const exprt &e2) |
| virtual void | add_equality_constraints () |
| virtual void | add_equality_constraints (const typestructt &typestruct) |
| Protected Member Functions inherited from prop_conv_solvert | |
| virtual std::optional< bool > | get_bool (const exprt &expr) const |
| Get a boolean value from the model if the formula is satisfiable. 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) |
| Static Protected Member Functions inherited from bv_pointerst | |
| static bvt | object_offset_encoding (const bvt &object, const bvt &offset) |
Construct a pointer encoding from given encodings of object and offset. More... | |
| Protected Attributes inherited from bv_pointerst | |
| pointer_logict | pointer_logic |
| postponed_listt | postponed_list |
| Protected Attributes inherited from boolbvt | |
| boolbv_widtht | bv_width |
| bv_utilst | bv_utils |
| functionst | functions |
| boolbv_mapt | map |
| bv_cachet | bv_cache |
| quantifier_listt | quantifier_list |
| numberingt< irep_idt > | string_numbering |
| std::size_t | scope_counter = 0 |
| Protected Attributes inherited from arrayst | |
| const namespacet & | ns |
| messaget | log |
| message_handlert & | message_handler |
| array_equalitiest | array_equalities |
| union_find< exprt, irep_hash > | arrays |
| index_mapt | index_map |
| bool | lazy_arrays |
| bool | incremental_cache |
| bool | get_array_constraints |
| std::list< lazy_constraintt > | lazy_array_constraints |
| std::map< exprt, bool > | expr_map |
| array_constraint_countt | array_constraint_count |
| std::set< std::size_t > | update_indices |
| std::unordered_set< irep_idt > | array_comprehension_args |
| Protected Attributes inherited from equalityt | |
| typemapt | typemap |
| Protected Attributes inherited from prop_conv_solvert | |
| bool | post_processing_done = false |
| symbolst | symbols |
| cachet | cache |
| propt & | prop |
| messaget | log |
| bvt | assumption_stack |
| Assumptions on the stack. More... | |
| std::size_t | context_literal_counter = 0 |
| To generate unique literal names for contexts. More... | |
| std::vector< size_t > | context_size_stack |
assumption_stack is segmented in contexts; Number of assumptions in each context on the stack More... | |
| Static Protected Attributes inherited from prop_conv_solvert | |
| static const char * | context_prefix = "prop_conv::context$" |
Detailed Description
Definition at line 44 of file bv_minimize.h.
Constructor & Destructor Documentation
◆ bv_minimizing_dect()
|
inline |
Definition at line 52 of file bv_minimize.h.
Member Function Documentation
◆ description()
|
inlinevirtual |
Definition at line 47 of file bv_minimize.h.
◆ minimize()
|
inline |
Definition at line 59 of file bv_minimize.h.
Member Data Documentation
◆ log
| messaget bv_minimizing_dect::log |
Definition at line 66 of file bv_minimize.h.
◆ satcheck
| satcheckt bv_minimizing_dect::satcheck |
Definition at line 65 of file bv_minimize.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/solvers/flattening/bv_minimize.h
