cprover
bv_refinementt Class Reference

#include <bv_refinement.h>

+ Inheritance diagram for bv_refinementt:
+ Collaboration diagram for bv_refinementt:

Classes

struct  approximationt
 
struct  configt
 
struct  infot
 

Public Member Functions

 bv_refinementt (const infot &info)
 
decision_proceduret::resultt dec_solve () override
 Run the decision procedure to solve the problem. More...
 
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure. More...
 
- Public Member Functions inherited from bv_pointerst
 bv_pointerst (const namespacet &_ns, propt &_prop, message_handlert &message_handler)
 
void post_process () override
 
- Public Member Functions inherited from boolbvt
 boolbvt (const namespacet &_ns, propt &_prop, message_handlert &message_handler)
 
virtual const bvtconvert_bv (const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
 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...
 
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_maptget_map () const
 
- Public Member Functions inherited from arrayst
 arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler)
 
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 post_process () override
 
- Public Member Functions inherited from prop_conv_solvert
 prop_conv_solvert (propt &_prop, message_handlert &message_handler)
 
virtual ~prop_conv_solvert ()=default
 
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out. 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...
 
bool literal (const symbol_exprt &expr, literalt &literal) const
 
const cachetget_cache () const
 
const symbolstget_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...
 
- 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 &expr)
 For a Boolean expression expr, add the constraint 'expr'. More...
 
void set_to_false (const exprt &expr)
 For a Boolean expression expr, add the constraint 'not expr'. More...
 
resultt operator() ()
 Run the decision procedure to solve the problem. More...
 
virtual ~decision_proceduret ()
 
- Public Member Functions inherited from solver_resource_limitst
virtual ~solver_resource_limitst ()=default
 

Protected Member Functions

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
 
- Protected Member Functions inherited from bv_pointerst
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 exprt &expr, 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)
 
- Protected Member Functions inherited from boolbvt
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)
 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 exprt &expr)
 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_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)
 Flatten array. More...
 
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 lambda_exprt &expr)
 
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_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 with_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)
 
- Protected Member Functions inherited from arrayst
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 add_array_constraints_array_constant (const index_sett &index_set, const array_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)
 
- 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 optionalt< 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)
 

Protected Attributes

configt config_
 
- Protected Attributes inherited from bv_pointerst
pointer_logict pointer_logic
 
unsigned object_bits
 
unsigned offset_bits
 
unsigned bits
 
postponed_listt postponed_list
 
- Protected Attributes inherited from boolbvt
bv_utilst bv_utils
 
functionst functions
 
boolbv_mapt map
 
bv_cachet bv_cache
 
quantifier_listt quantifier_list
 
numbering< irep_idtstring_numbering
 
- Protected Attributes inherited from arrayst
const namespacetns
 
array_equalitiest array_equalities
 
union_find< exprtarrays
 
index_mapt index_map
 
bool lazy_arrays
 
bool incremental_cache
 
std::list< lazy_constrainttlazy_array_constraints
 
std::map< exprt, bool > expr_map
 
std::set< std::size_t > update_indices
 
- Protected Attributes inherited from equalityt
typemapt typemap
 
- Protected Attributes inherited from prop_conv_solvert
bool post_processing_done = false
 
symbolst symbols
 
cachet cache
 
proptprop
 
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...
 

Private Member Functions

resultt prop_solve ()
 
approximationtadd_approximation (const exprt &expr, bvt &bv)
 
bool conflicts_with (approximationt &approximation)
 check if an under-approximation is part of the conflict More...
 
void check_SAT (approximationt &approximation)
 inspect if satisfying assignment extends to original formula, otherwise refine overapproximation More...
 
void check_UNSAT (approximationt &approximation)
 inspect if proof holds on original formula, otherwise refine underapproximation More...
 
void initialize (approximationt &approximation)
 
void get_values (approximationt &approximation)
 
void check_SAT ()
 
void check_UNSAT ()
 
void arrays_overapproximated ()
 check whether counterexample is spurious More...
 
void freeze_lazy_constraints ()
 freeze symbols for incremental solving More...
 

Private Attributes

bool progress
 
std::list< approximationtapproximations
 

Additional Inherited Members

- Public Types inherited from boolbvt
enum  unbounded_arrayt { unbounded_arrayt::U_NONE, unbounded_arrayt::U_ALL, unbounded_arrayt::U_AUTO }
 
- Public Types inherited from arrayst
typedef equalityt SUB
 
- Public Types inherited from prop_conv_solvert
typedef std::map< irep_idt, literaltsymbolst
 
typedef std::unordered_map< exprt, literalt, irep_hashcachet
 
- Public Types inherited from decision_proceduret
enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 Result of running the decision procedure. More...
 
- Public Attributes inherited from boolbvt
unbounded_arrayt unbounded_array
 
boolbv_widtht boolbv_width
 
- Public Attributes inherited from prop_conv_solvert
bool use_cache = true
 
bool equality_propagation = true
 
bool freeze_all = false
 
- Protected Types inherited from bv_pointerst
typedef boolbvt SUB
 
typedef std::list< postponedtpostponed_listt
 
- Protected Types inherited from boolbvt
typedef arrayst SUB
 
typedef std::unordered_map< const exprt, bvt, irep_hashbv_cachet
 
typedef std::list< quantifiertquantifier_listt
 
typedef std::vector< std::size_t > offset_mapt
 
- Protected Types inherited from arrayst
enum  lazy_typet {
  lazy_typet::ARRAY_ACKERMANN, lazy_typet::ARRAY_WITH, lazy_typet::ARRAY_IF, lazy_typet::ARRAY_OF,
  lazy_typet::ARRAY_TYPECAST, lazy_typet::ARRAY_CONSTANT
}
 
typedef std::list< array_equalitytarray_equalitiest
 
typedef std::set< exprtindex_sett
 
typedef std::map< std::size_t, index_settindex_mapt
 
- Protected Types inherited from equalityt
typedef std::unordered_map< const exprt, unsigned, irep_hashelementst
 
typedef std::map< std::pair< unsigned, unsigned >, literaltequalitiest
 
typedef std::map< unsigned, exprtelements_revt
 
typedef std::unordered_map< const typet, typestructt, irep_hashtypemapt
 
- Static Protected Attributes inherited from prop_conv_solvert
static const char * context_prefix = "prop_conv::context$"
 

Detailed Description

Definition at line 19 of file bv_refinement.h.

Constructor & Destructor Documentation

◆ bv_refinementt()

bv_refinementt::bv_refinementt ( const infot info)
explicit

Definition at line 13 of file bv_refinement_loop.cpp.

Member Function Documentation

◆ add_approximation()

bv_refinementt::approximationt & bv_refinementt::add_approximation ( const exprt expr,
bvt bv 
)
private

Definition at line 484 of file refine_arithmetic.cpp.

◆ arrays_overapproximated()

void bv_refinementt::arrays_overapproximated ( )
private

check whether counterexample is spurious

Definition at line 36 of file refine_arrays.cpp.

◆ check_SAT() [1/2]

void bv_refinementt::check_SAT ( approximationt approximation)
private

inspect if satisfying assignment extends to original formula, otherwise refine overapproximation

Definition at line 158 of file refine_arithmetic.cpp.

◆ check_SAT() [2/2]

void bv_refinementt::check_SAT ( )
private

Definition at line 120 of file bv_refinement_loop.cpp.

◆ check_UNSAT() [1/2]

void bv_refinementt::check_UNSAT ( approximationt approximation)
private

inspect if proof holds on original formula, otherwise refine underapproximation

Definition at line 366 of file refine_arithmetic.cpp.

◆ check_UNSAT() [2/2]

void bv_refinementt::check_UNSAT ( )
private

Definition at line 130 of file bv_refinement_loop.cpp.

◆ conflicts_with()

bool bv_refinementt::conflicts_with ( approximationt approximation)
private

check if an under-approximation is part of the conflict

Definition at line 454 of file refine_arithmetic.cpp.

◆ convert_div()

bvt bv_refinementt::convert_div ( const div_exprt expr)
overrideprotectedvirtual

Reimplemented from boolbvt.

Definition at line 97 of file refine_arithmetic.cpp.

◆ convert_floatbv_op()

bvt bv_refinementt::convert_floatbv_op ( const exprt expr)
overrideprotectedvirtual

Reimplemented from boolbvt.

Definition at line 36 of file refine_arithmetic.cpp.

◆ convert_mod()

bvt bv_refinementt::convert_mod ( const mod_exprt expr)
overrideprotectedvirtual

Reimplemented from boolbvt.

Definition at line 115 of file refine_arithmetic.cpp.

◆ convert_mult()

bvt bv_refinementt::convert_mult ( const mult_exprt expr)
overrideprotectedvirtual

Reimplemented from boolbvt.

Definition at line 49 of file refine_arithmetic.cpp.

◆ dec_solve()

decision_proceduret::resultt bv_refinementt::dec_solve ( )
overridevirtual

Run the decision procedure to solve the problem.

Reimplemented from prop_conv_solvert.

Reimplemented in string_refinementt.

Definition at line 24 of file bv_refinement_loop.cpp.

◆ decision_procedure_text()

std::string bv_refinementt::decision_procedure_text ( ) const
inlineoverridevirtual

Return a textual description of the decision procedure.

Reimplemented from prop_conv_solvert.

Reimplemented in string_refinementt.

Definition at line 44 of file bv_refinement.h.

◆ freeze_lazy_constraints()

void bv_refinementt::freeze_lazy_constraints ( )
private

freeze symbols for incremental solving

Definition at line 107 of file refine_arrays.cpp.

◆ get_values()

void bv_refinementt::get_values ( approximationt approximation)
private

Definition at line 133 of file refine_arithmetic.cpp.

◆ initialize()

void bv_refinementt::initialize ( approximationt approximation)
private

Definition at line 468 of file refine_arithmetic.cpp.

◆ post_process_arrays()

void bv_refinementt::post_process_arrays ( )
overrideprotectedvirtual

generate array constraints

Reimplemented from arrayst.

Definition at line 21 of file refine_arrays.cpp.

◆ prop_solve()

decision_proceduret::resultt bv_refinementt::prop_solve ( )
private

Definition at line 87 of file bv_refinement_loop.cpp.

Member Data Documentation

◆ approximations

std::list<approximationt> bv_refinementt::approximations
private

Definition at line 108 of file bv_refinement.h.

◆ config_

configt bv_refinementt::config_
protected

Definition at line 112 of file bv_refinement.h.

◆ progress

bool bv_refinementt::progress
private

Definition at line 107 of file bv_refinement.h.


The documentation for this class was generated from the following files: