cprover
equalityt Member List
This is the complete list of members for
equalityt
, including all inherited members.
add_equality_constraints
()
equalityt
protected
virtual
add_equality_constraints
(const typestructt &typestruct)
equalityt
protected
virtual
cache
prop_conv_solvert
protected
cachet
typedef
prop_conv_solvert
clear_cache
()
prop_conv_solvert
inline
virtual
convert
(const exprt &expr) override
prop_conv_solvert
virtual
convert_bool
(const exprt &expr)
prop_conv_solvert
protected
virtual
convert_rest
(const exprt &expr)
prop_conv_solvert
protected
virtual
debug
()
messaget
inline
dec_solve
() override
prop_conv_solvert
virtual
decision_procedure_text
() const override
prop_conv_solvert
inline
virtual
decision_proceduret
(const namespacet &_ns)
decision_proceduret
inline
explicit
elements_revt
typedef
equalityt
protected
elementst
typedef
equalityt
protected
endl
(mstreamt &m)
messaget
inline
static
eom
(mstreamt &m)
messaget
inline
static
equalitiest
typedef
equalityt
protected
equality
(const exprt &e1, const exprt &e2)
equalityt
virtual
equality2
(const exprt &e1, const exprt &e2)
equalityt
protected
virtual
equality_propagation
prop_conv_solvert
equalityt
(const namespacet &_ns, propt &_prop)
equalityt
inline
error
()
messaget
inline
freeze_all
prop_conv_solvert
get
(const exprt &expr) const override
prop_conv_solvert
virtual
get_bool
(const exprt &expr, tvt &value) const
prop_conv_solvert
protected
virtual
get_cache
() const
prop_conv_solvert
inline
get_literal
(const irep_idt &symbol)
prop_conv_solvert
protected
virtual
get_message_handler
()
messaget
inline
get_mstream
(unsigned message_level)
messaget
inline
get_symbols
() const
prop_conv_solvert
inline
has_is_in_conflict
() const override
prop_conv_solvert
inline
virtual
has_set_assumptions
() const override
prop_conv_solvert
inline
virtual
ignoring
(const exprt &expr)
prop_conv_solvert
protected
virtual
in_core
(const exprt &expr)
decision_proceduret
virtual
is_in_conflict
(literalt l) const override
prop_conv_solvert
inline
virtual
l_get
(literalt a) const override
prop_conv_solvert
inline
virtual
literal
(const exprt &expr, literalt &literal) const
prop_conv_solvert
virtual
M_DEBUG
enum value
messaget
M_ERROR
enum value
messaget
M_PROGRESS
enum value
messaget
M_RESULT
enum value
messaget
M_STATISTICS
enum value
messaget
M_STATUS
enum value
messaget
M_WARNING
enum value
messaget
message_handler
messaget
protected
message_levelt
enum name
messaget
messaget
()
messaget
inline
messaget
(const messaget &other)
messaget
inline
messaget
(message_handlert &_message_handler)
messaget
inline
explicit
mstream
messaget
protected
ns
decision_proceduret
protected
operator()
(const exprt &expr)
prop_convt
inline
decision_proceduret::operator()
()
decision_proceduret
inline
post_process
() override
equalityt
inline
virtual
post_processing_done
prop_conv_solvert
protected
print_assignment
(std::ostream &out) const override
prop_conv_solvert
virtual
progress
()
messaget
inline
prop
prop_conv_solvert
protected
prop_conv_solvert
(const namespacet &_ns, propt &_prop)
prop_conv_solvert
inline
prop_convt
(const namespacet &_ns)
prop_convt
inline
explicit
result
()
messaget
inline
resultt
enum name
decision_proceduret
set_all_frozen
() override
prop_conv_solvert
inline
virtual
set_assumptions
(const bvt &_assumptions) override
prop_conv_solvert
inline
virtual
set_equality_to_true
(const equal_exprt &expr)
prop_conv_solvert
protected
virtual
set_frozen
(literalt a) override
prop_conv_solvert
inline
virtual
set_frozen
(literalt a)
prop_conv_solvert
set_frozen
(const bvt &)
prop_conv_solvert
prop_convt::set_frozen
(const bvt &)
prop_convt
virtual
set_message_handler
(message_handlert &_message_handler)
messaget
inline
virtual
set_to
(const exprt &expr, bool value) override
prop_conv_solvert
virtual
set_to_false
(const exprt &expr)
decision_proceduret
inline
set_to_true
(const exprt &expr)
decision_proceduret
inline
statistics
()
messaget
inline
status
()
messaget
inline
symbols
prop_conv_solvert
protected
symbolst
typedef
prop_conv_solvert
typemap
equalityt
protected
typemapt
typedef
equalityt
protected
use_cache
prop_conv_solvert
warning
()
messaget
inline
~messaget
()
messaget
virtual
~prop_conv_solvert
()
prop_conv_solvert
inline
virtual
~prop_convt
()
prop_convt
inline
virtual
Generated by
1.8.14