cprover
|
#include <bv_refinement.h>
Classes | |
struct | approximationt |
struct | configt |
struct | infot |
Public Member Functions | |
bv_refinementt (const infot &info) | |
decision_proceduret::resultt | dec_solve () override |
std::string | decision_procedure_text () const override |
![]() | |
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) |
exprt | get (const exprt &expr) const override |
void | set_to (const exprt &expr, bool value) override |
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 | set_to (const exprt &expr, bool value) override |
void | print_assignment (std::ostream &out) const override |
exprt | get (const exprt &expr) 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 |
virtual bool | literal (const 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() () |
Protected Member Functions | |
void | post_process_arrays () override |
generate array constraints More... | |
bvt | convert_mult (const 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 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 exprt &expr) |
virtual bvt | convert_complex (const exprt &expr) |
virtual bvt | convert_complex_real (const exprt &expr) |
virtual bvt | convert_complex_imag (const 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 exprt &expr) |
virtual bvt | convert_shift (const binary_exprt &expr) |
virtual bvt | convert_bitwise (const exprt &expr) |
virtual bvt | convert_unary_minus (const unary_exprt &expr) |
virtual bvt | convert_abs (const abs_exprt &expr) |
virtual bvt | convert_concatenation (const 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) |
Protected Attributes | |
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 |
Private Member Functions | |
resultt | prop_solve () |
approximationt & | add_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< approximationt > | approximations |
bvt | parent_assumptions |
Additional Inherited Members | |
![]() | |
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 } |
![]() | |
unbounded_arrayt | unbounded_array |
boolbv_widtht | boolbv_width |
![]() | |
bool | use_cache = true |
bool | equality_propagation = true |
bool | freeze_all = false |
![]() | |
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 |
Definition at line 21 of file bv_refinement.h.
|
explicit |
Definition at line 15 of file bv_refinement_loop.cpp.
References propt::has_is_in_conflict(), propt::has_set_assumptions(), propt::has_set_to(), PRECONDITION, and prop_conv_solvert::prop.
|
private |
Definition at line 484 of file refine_arithmetic.cpp.
References approximations, boolbvt::boolbv_width, boolbvt::convert_bv(), bv_refinementt::approximationt::expr, initialize(), propt::new_variables(), bv_refinementt::approximationt::no_operands, exprt::op0(), bv_refinementt::approximationt::op0_bv, exprt::op1(), bv_refinementt::approximationt::op1_bv, exprt::op2(), bv_refinementt::approximationt::op2_bv, exprt::operands(), PRECONDITION, prop_conv_solvert::prop, bv_refinementt::approximationt::result_bv, prop_conv_solvert::set_frozen(), exprt::type(), and UNREACHABLE.
Referenced by convert_div(), convert_floatbv_op(), convert_mod(), and convert_mult().
|
private |
check whether counterexample is spurious
Definition at line 37 of file refine_arrays.cpp.
References config_, prop_conv_solvert::convert(), decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, DATA_INVARIANT, messaget::debug(), messaget::eom(), messaget::error(), irept::id(), INVARIANT, propt::l_set_to_true(), arrayst::lazy_array_constraints, decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::operands(), messaget::progress(), prop_conv_solvert::prop, bv_refinementt::configt::refine_arrays, solver(), string_refinement_invariantt, to_implies_expr(), to_or_expr(), and boolbvt::U_ALL.
Referenced by check_SAT().
|
private |
inspect if satisfying assignment extends to original formula, otherwise refine overapproximation
Definition at line 162 of file refine_arithmetic.cpp.
References float_utilst::add(), bv_refinementt::approximationt::as_string(), float_utilst::build_constant(), boolbvt::bv_utils, CHECK_RETURN, config_, messaget::debug(), float_utilst::div(), bv_utilst::divider(), messaget::eom(), bv_utilst::equal(), bv_refinementt::approximationt::expr, namespace_baset::follow(), get_values(), irept::id(), integer2binary(), integer2ulong(), INVARIANT, propt::l_set_to_true(), propt::land(), propt::limplies(), bv_refinementt::configt::max_node_refinement, MAX_STATE, float_utilst::mul(), bv_utilst::multiplier(), decision_proceduret::ns, bv_refinementt::approximationt::op0_bv, bv_refinementt::approximationt::op0_value, bv_refinementt::approximationt::op1_bv, bv_refinementt::approximationt::op1_value, exprt::op2(), exprt::operands(), bv_refinementt::approximationt::over_assumptions, bv_refinementt::approximationt::over_state, messaget::progress(), prop_conv_solvert::prop, r, bv_utilst::remainder(), messaget::result(), bv_refinementt::approximationt::result_bv, bv_refinementt::approximationt::result_value, ieee_floatt::rounding_mode, float_utilst::rounding_mode_bits, float_utilst::rounding_mode_bitst::set(), bv_utilst::set_equal(), bv_utilst::SIGNED, float_utilst::spec, messaget::status(), string_refinement_invariantt, float_utilst::sub(), to_floatbv_type(), to_integer(), TODO, exprt::type(), bv_arithmetict::unpack(), ieee_floatt::unpack(), UNREACHABLE, bv_utilst::UNSIGNED, and ieee_float_spect::width().
|
private |
Definition at line 115 of file bv_refinement_loop.cpp.
References approximations, arrays_overapproximated(), and messaget::progress().
Referenced by dec_solve().
|
private |
inspect if proof holds on original formula, otherwise refine underapproximation
Definition at line 371 of file refine_arithmetic.cpp.
References bv_refinementt::approximationt::add_under_assumption(), bv_refinementt::approximationt::as_string(), conflicts_with(), messaget::eom(), bv_refinementt::approximationt::expr, float_utilst::get_fraction(), irept::id(), MAX_FLOAT_UNDERAPPROX, MAX_INTEGER_UNDERAPPROX, bv_refinementt::approximationt::op0_bv, bv_refinementt::approximationt::op1_bv, PRECONDITION, messaget::progress(), prop_conv_solvert::prop, bv_refinementt::approximationt::result_bv, float_utilst::spec, messaget::status(), to_floatbv_type(), exprt::type(), bv_refinementt::approximationt::under_assumptions, and bv_refinementt::approximationt::under_state.
|
private |
Definition at line 125 of file bv_refinement_loop.cpp.
References approximations, and messaget::progress().
Referenced by dec_solve().
|
private |
check if an under-approximation is part of the conflict
Definition at line 459 of file refine_arithmetic.cpp.
References propt::is_in_conflict(), prop_conv_solvert::prop, and bv_refinementt::approximationt::under_assumptions.
Referenced by check_UNSAT().
Reimplemented from boolbvt.
Definition at line 101 of file refine_arithmetic.cpp.
References add_approximation(), config_, irept::id(), exprt::is_constant(), exprt::op1(), exprt::operands(), PRECONDITION, bv_refinementt::configt::refine_arithmetic, and exprt::type().
Reimplemented from boolbvt.
Definition at line 39 of file refine_arithmetic.cpp.
References add_approximation(), config_, namespace_baset::follow(), decision_proceduret::ns, exprt::operands(), bv_refinementt::configt::refine_arithmetic, and exprt::type().
Reimplemented from boolbvt.
Definition at line 119 of file refine_arithmetic.cpp.
References add_approximation(), config_, irept::id(), exprt::is_constant(), exprt::op1(), exprt::operands(), PRECONDITION, bv_refinementt::configt::refine_arithmetic, and exprt::type().
Reimplemented from boolbvt.
Definition at line 53 of file refine_arithmetic.cpp.
References add_approximation(), boolbvt::bv_utils, config_, bv_utilst::equal(), namespace_baset::follow(), irept::id(), bv_utilst::is_one(), bv_utilst::is_zero(), propt::l_set_to_true(), propt::limplies(), propt::lor(), make_binary(), decision_proceduret::ns, bv_refinementt::approximationt::op0_bv, bv_refinementt::approximationt::op1_bv, exprt::operands(), PRECONDITION, prop_conv_solvert::prop, bv_refinementt::configt::refine_arithmetic, bv_refinementt::approximationt::result_bv, and exprt::type().
|
overridevirtual |
Reimplemented from prop_conv_solvert.
Reimplemented in string_refinementt.
Definition at line 26 of file bv_refinement_loop.cpp.
References check_SAT(), check_UNSAT(), config_, decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, xmlt::data, messaget::debug(), messaget::eom(), bv_pointerst::post_process(), messaget::progress(), prop_conv_solvert::prop, prop_solve(), propt::solver_text(), messaget::status(), to_string(), bv_refinementt::configt::ui, xml(), and ui_message_handlert::XML_UI.
Referenced by string_refinementt::dec_solve().
|
inlineoverridevirtual |
Reimplemented from prop_conv_solvert.
Reimplemented in string_refinementt.
Definition at line 45 of file bv_refinement.h.
References prop_conv_solvert::prop, and propt::solver_text().
|
private |
freeze symbols for incremental solving
Definition at line 118 of file refine_arrays.cpp.
References boolbvt::convert_bv(), find_symbols(), forall_literals, arrayst::lazy_array_constraints, arrayst::lazy_arrays, prop_conv_solvert::prop, propt::set_frozen(), and prop_conv_solvert::symbols.
Referenced by post_process_arrays().
|
private |
Definition at line 137 of file refine_arithmetic.cpp.
References bv_refinementt::approximationt::expr, boolbvt::get_value(), bv_refinementt::approximationt::op0_bv, bv_refinementt::approximationt::op0_value, bv_refinementt::approximationt::op1_bv, bv_refinementt::approximationt::op1_value, bv_refinementt::approximationt::op2_bv, bv_refinementt::approximationt::op2_value, exprt::operands(), bv_refinementt::approximationt::result_bv, bv_refinementt::approximationt::result_value, and UNREACHABLE.
Referenced by check_SAT().
|
private |
Definition at line 468 of file refine_arithmetic.cpp.
References bv_refinementt::approximationt::add_under_assumption(), bv_refinementt::approximationt::op0_bv, bv_refinementt::approximationt::op1_bv, bv_refinementt::approximationt::over_state, bv_refinementt::approximationt::under_assumptions, and bv_refinementt::approximationt::under_state.
Referenced by add_approximation().
|
overrideprotectedvirtual |
generate array constraints
Reimplemented from arrayst.
Definition at line 22 of file refine_arrays.cpp.
References arrayst::add_array_constraints(), arrayst::collect_indices(), config_, freeze_lazy_constraints(), arrayst::lazy_arrays, bv_refinementt::configt::refine_arrays, and arrayst::update_index_map().
|
private |
Definition at line 86 of file bv_refinement_loop.cpp.
References approximations, decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, propt::P_SATISFIABLE, propt::P_UNSATISFIABLE, parent_assumptions, prop_conv_solvert::prop, propt::prop_solve(), messaget::result(), and propt::set_assumptions().
Referenced by dec_solve().
|
overrideprotectedvirtual |
Reimplemented from prop_conv_solvert.
Definition at line 133 of file bv_refinement_loop.cpp.
References parent_assumptions, prop_conv_solvert::prop, and propt::set_assumptions().
|
private |
Definition at line 111 of file bv_refinement.h.
Referenced by add_approximation(), check_SAT(), check_UNSAT(), and prop_solve().
|
protected |
Definition at line 115 of file bv_refinement.h.
Referenced by arrays_overapproximated(), check_SAT(), convert_div(), convert_floatbv_op(), convert_mod(), convert_mult(), dec_solve(), and post_process_arrays().
|
private |
Definition at line 112 of file bv_refinement.h.
Referenced by prop_solve(), and set_assumptions().
|
private |
Definition at line 110 of file bv_refinement.h.