cprover
|
TO_BE_DOCUMENTED. More...
#include <prop_conv.h>
Public Types | |
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 } |
Public Member Functions | |
prop_conv_solvert (const namespacet &_ns, propt &_prop) | |
virtual | ~prop_conv_solvert ()=default |
void | set_to (const exprt &expr, bool value) override |
decision_proceduret::resultt | dec_solve () override |
void | print_assignment (std::ostream &out) const override |
std::string | decision_procedure_text () const override |
exprt | get (const exprt &expr) const override |
virtual tvt | l_get (literalt a) const override |
void | set_frozen (literalt a) override |
void | set_assumptions (const bvt &_assumptions) 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 |
virtual void | clear_cache () |
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() () |
Public Attributes | |
bool | use_cache = true |
bool | equality_propagation = true |
bool | freeze_all = false |
Protected Member Functions | |
virtual void | post_process () |
virtual bool | get_bool (const exprt &expr, tvt &value) const |
get a boolean value from counter example if not valid More... | |
virtual literalt | convert_rest (const exprt &expr) |
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 | |
bool | post_processing_done = false |
symbolst | symbols |
cachet | cache |
propt & | prop |
![]() | |
const namespacet & | ns |
Additional Inherited Members |
TO_BE_DOCUMENTED.
Definition at line 70 of file prop_conv.h.
typedef std::unordered_map<exprt, literalt, irep_hash> prop_conv_solvert::cachet |
Definition at line 118 of file prop_conv.h.
typedef std::map<irep_idt, literalt> prop_conv_solvert::symbolst |
Definition at line 117 of file prop_conv.h.
|
inline |
Definition at line 73 of file prop_conv.h.
|
virtualdefault |
|
inlinevirtual |
Reimplemented in boolbvt.
Definition at line 115 of file prop_conv.h.
References cache.
Referenced by boolbvt::clear_cache().
Implements prop_convt.
Definition at line 162 of file prop_conv.cpp.
References cache, convert_bool(), freeze_all, irept::id(), literal(), prop, messaget::result(), propt::set_frozen(), and use_cache.
Referenced by arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraint(), arrayst::add_array_constraints_equality(), arrayst::add_array_constraints_if(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), string_refinementt::add_lemma(), bv_refinementt::arrays_overapproximated(), bv_pointerst::convert_address_of_rec(), boolbvt::convert_bitvector(), convert_bool(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), boolbvt::convert_cond(), boolbvt::convert_extractbit(), boolbvt::convert_if(), boolbvt::convert_index(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), set_equality_to_true(), and set_to().
Definition at line 195 of file prop_conv.cpp.
References const_literal(), convert(), convert_rest(), forall_expr, forall_operands, symbol_exprt::get_identifier(), literal_exprt::get_literal(), get_literal(), irept::id(), irept::id_string(), INVARIANT, exprt::is_constant(), exprt::is_false(), exprt::is_true(), propt::l_set_to_true(), propt::land(), propt::lequal(), propt::limplies(), propt::lor(), propt::lselect(), propt::lxor(), propt::new_variable(), exprt::operands(), PRECONDITION, irept::pretty(), prop, messaget::result(), let_exprt::symbol(), symbols, to_let_expr(), to_literal_expr(), to_symbol_expr(), exprt::type(), let_exprt::value(), and let_exprt::where().
Referenced by convert(), and boolbvt::post_process_quantifiers().
Reimplemented in boolbvt, and bv_pointerst.
Definition at line 331 of file prop_conv.cpp.
References ignoring(), propt::new_variable(), and prop.
Referenced by convert_bool(), boolbvt::convert_bv_rel(), boolbvt::convert_extractbit(), boolbvt::convert_ieee_float_rel(), boolbvt::convert_overflow(), boolbvt::convert_quantifier(), boolbvt::convert_rest(), and boolbvt::convert_typecast().
|
overridevirtual |
Implements decision_proceduret.
Reimplemented in string_refinementt, and bv_refinementt.
Definition at line 465 of file prop_conv.cpp.
References decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), propt::P_SATISFIABLE, propt::P_UNSATISFIABLE, post_process(), post_processing_done, prop, propt::prop_solve(), propt::solver_text(), and messaget::statistics().
|
inlineoverridevirtual |
Implements decision_proceduret.
Reimplemented in string_refinementt, and bv_refinementt.
Definition at line 83 of file prop_conv.h.
Implements decision_proceduret.
Reimplemented in string_refinementt.
Definition at line 485 of file prop_conv.cpp.
References get_bool(), tvt::get_value(), irept::id(), exprt::operands(), irept::swap(), tvt::TV_FALSE, tvt::TV_TRUE, tvt::TV_UNKNOWN, and exprt::type().
Referenced by boolbvt::get().
get a boolean value from counter example if not valid
Definition at line 74 of file prop_conv.cpp.
References cache, forall_operands, irept::id(), tvt::is_false(), exprt::is_false(), tvt::is_true(), exprt::is_true(), propt::l_get(), exprt::op0(), exprt::operands(), prop, messaget::result(), symbols, to_symbol_expr(), and exprt::type().
Referenced by get().
|
inline |
Definition at line 120 of file prop_conv.h.
References cache.
Definition at line 56 of file prop_conv.cpp.
References literal(), propt::new_variable(), prop, messaget::result(), propt::set_variable_name(), and symbols.
Referenced by convert_bool().
|
inline |
Definition at line 121 of file prop_conv.h.
References symbols.
Referenced by cbmc_dimacst::write_dimacs().
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 105 of file prop_conv.h.
References propt::has_is_in_conflict(), and prop.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 96 of file prop_conv.h.
References propt::has_set_assumptions(), and prop.
|
protectedvirtual |
Definition at line 454 of file prop_conv.cpp.
References messaget::eom(), irept::pretty(), and messaget::warning().
Referenced by boolbvt::conversion_failed(), and convert_rest().
|
inlineoverridevirtual |
determine whether a variable is in the final conflict
Reimplemented from prop_convt.
Definition at line 103 of file prop_conv.h.
References propt::is_in_conflict(), and prop.
Implements prop_convt.
Definition at line 89 of file prop_conv.h.
References propt::l_get(), and prop.
Definition at line 36 of file prop_conv.cpp.
References symbol_exprt::get_identifier(), irept::id(), messaget::result(), symbols, to_symbol_expr(), and exprt::type().
Referenced by convert(), get_literal(), and boolbvt::literal().
|
protectedvirtual |
Reimplemented in boolbvt, arrayst, equalityt, and bv_pointerst.
Definition at line 461 of file prop_conv.cpp.
Referenced by dec_solve(), and equalityt::post_process().
|
overridevirtual |
Implements decision_proceduret.
Definition at line 509 of file prop_conv.cpp.
References propt::l_get(), prop, and symbols.
Referenced by boolbvt::print_assignment().
|
inlineoverridevirtual |
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Reimplemented in bv_refinementt.
Definition at line 94 of file prop_conv.h.
References prop, and propt::set_assumptions().
|
protectedvirtual |
Definition at line 338 of file prop_conv.cpp.
References convert(), equality_propagation, irept::id(), binary_relation_exprt::lhs(), messaget::result(), binary_relation_exprt::rhs(), symbols, and to_symbol_expr().
Referenced by set_to().
void prop_convt::set_frozen |
Definition at line 24 of file prop_conv.cpp.
void prop_convt::set_frozen |
Definition at line 29 of file prop_conv.cpp.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 90 of file prop_conv.h.
References prop, and propt::set_frozen().
Referenced by bv_refinementt::add_approximation(), and boolbvt::boolbv_set_equality_to_true().
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 123 of file prop_conv.h.
References prop, and propt::set_time_limit_seconds().
|
overridevirtual |
Implements decision_proceduret.
Reimplemented in string_refinementt.
Definition at line 365 of file prop_conv.cpp.
References convert(), forall_operands, irept::id(), propt::l_set_to(), propt::lcnf(), exprt::op0(), exprt::op1(), exprt::operands(), PRECONDITION, prop, set_equality_to_true(), decision_proceduret::set_to_false(), decision_proceduret::set_to_true(), to_equal_expr(), and exprt::type().
Referenced by boolbvt::set_to().
|
protected |
Definition at line 147 of file prop_conv.h.
Referenced by clear_cache(), convert(), get_bool(), and get_cache().
bool prop_conv_solvert::equality_propagation = true |
Definition at line 112 of file prop_conv.h.
Referenced by boolbvt::boolbv_set_equality_to_true(), set_equality_to_true(), and string_refinementt::set_to().
bool prop_conv_solvert::freeze_all = false |
Definition at line 113 of file prop_conv.h.
Referenced by boolbvt::boolbv_set_equality_to_true(), convert(), boolbvt::convert_bv(), equalityt::equality2(), and set_all_frozen().
|
protected |
Definition at line 131 of file prop_conv.h.
Referenced by dec_solve().
|
protected |
Definition at line 152 of file prop_conv.h.
Referenced by bv_refinementt::add_approximation(), arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraint(), arrayst::add_array_constraints_equality(), arrayst::add_array_constraints_if(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), equalityt::add_equality_constraints(), string_refinementt::add_lemma(), bv_refinementt::arrays_overapproximated(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), bv_refinementt::bv_refinementt(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), arrayst::collect_arrays(), bv_refinementt::conflicts_with(), boolbvt::conversion_failed(), convert(), boolbvt::convert_abs(), boolbvt::convert_add_sub(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), convert_bool(), boolbvt::convert_bv(), boolbvt::convert_bv_reduction(), boolbvt::convert_bv_rel(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_constraint_select_one(), boolbvt::convert_equality(), boolbvt::convert_extractbit(), boolbvt::convert_floatbv_op(), boolbvt::convert_floatbv_typecast(), boolbvt::convert_function_application(), boolbvt::convert_ieee_float_rel(), boolbvt::convert_index(), bv_refinementt::convert_mult(), boolbvt::convert_not(), boolbvt::convert_onehot(), boolbvt::convert_overflow(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), boolbvt::convert_quantifier(), boolbvt::convert_reduction(), bv_pointerst::convert_rest(), boolbvt::convert_rest(), convert_rest(), boolbvt::convert_symbol(), boolbvt::convert_typecast(), boolbvt::convert_unary_minus(), boolbvt::convert_union(), boolbvt::convert_update_rec(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), bv_refinementt::dec_solve(), dec_solve(), bv_refinementt::decision_procedure_text(), string_refinementt::decision_procedure_text(), bv_pointerst::do_postponed(), equalityt::equality2(), bv_refinementt::freeze_lazy_constraints(), get_bool(), get_literal(), boolbvt::get_value(), has_is_in_conflict(), has_set_assumptions(), is_in_conflict(), l_get(), boolbvt::make_free_bv_expr(), boolbvt::post_process_quantifiers(), boolbvt::print_assignment(), print_assignment(), bv_refinementt::prop_solve(), arrayst::record_array_equality(), bv_refinementt::set_assumptions(), set_assumptions(), set_frozen(), set_time_limit_seconds(), set_to(), boolbvt::type_conversion(), and cbmc_dimacst::write_dimacs().
|
protected |
Definition at line 142 of file prop_conv.h.
Referenced by convert_bool(), bv_refinementt::freeze_lazy_constraints(), get_bool(), get_literal(), get_symbols(), literal(), print_assignment(), and set_equality_to_true().
bool prop_conv_solvert::use_cache = true |
Definition at line 111 of file prop_conv.h.
Referenced by convert().