cprover
dplib_convt Member List
This is the complete list of members for
dplib_convt
, including all inherited members.
array_index
(unsigned i)
dplib_convt
private
static
array_index_type
()
dplib_convt
private
static
bin_zero
(unsigned bits)
dplib_convt
private
static
convert
(const exprt &expr)=0
prop_convt
pure virtual
convert_address_of_rec
(const exprt &expr)
dplib_convt
protected
virtual
convert_array_index
(const exprt &expr)
dplib_convt
private
convert_array_value
(const exprt &expr)
dplib_convt
private
convert_as_bv
(const exprt &expr)
dplib_convt
private
convert_dplib_expr
(const exprt &expr)
dplib_convt
protected
virtual
convert_dplib_type
(const typet &type)
dplib_convt
protected
virtual
convert_identifier
(const std::string &identifier)
dplib_convt
private
convert_rest
(const exprt &expr)
dplib_convt
protected
virtual
debug
()
messaget
inline
dec_solve
()=0
decision_proceduret
pure virtual
decision_procedure_text
() const =0
decision_proceduret
pure virtual
decision_proceduret
(const namespacet &_ns)
decision_proceduret
inline
explicit
dplib_convt
(const namespacet &_ns, std::ostream &_out)
dplib_convt
inline
dplib_pointer_type
()
dplib_convt
private
static
endl
(mstreamt &m)
messaget
inline
static
eom
(mstreamt &m)
messaget
inline
static
error
()
messaget
inline
find_symbols
(const exprt &expr)
dplib_convt
private
find_symbols
(const typet &type)
dplib_convt
private
gen_array_index_type
()
dplib_convt
private
static
get
(const exprt &expr) const =0
decision_proceduret
pure virtual
get_message_handler
()
messaget
inline
get_mstream
(unsigned message_level)
messaget
inline
has_is_in_conflict
() const
prop_convt
inline
virtual
has_set_assumptions
() const
prop_convt
inline
virtual
identifier_map
dplib_convt
private
identifier_mapt
typedef
dplib_convt
private
in_core
(const exprt &expr)
decision_proceduret
virtual
is_in_conflict
(literalt l) const
prop_convt
virtual
l_get
(literalt a) const =0
prop_convt
pure 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
out
dplib_convt
protected
pointer_logic
dplib_convt
protected
print_assignment
(std::ostream &out) const =0
decision_proceduret
pure virtual
progress
()
messaget
inline
prop_convt
(const namespacet &_ns)
prop_convt
inline
explicit
result
()
messaget
inline
resultt
enum name
decision_proceduret
set_all_frozen
()
prop_convt
inline
virtual
set_assumptions
(const bvt &_assumptions)
prop_convt
virtual
set_frozen
(literalt a)
prop_convt
virtual
set_frozen
(const bvt &)
prop_convt
virtual
set_message_handler
(message_handlert &_message_handler)
messaget
inline
virtual
set_to
(const exprt &expr, bool value)
dplib_convt
protected
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
warning
()
messaget
inline
~dplib_convt
()
dplib_convt
inline
virtual
~messaget
()
messaget
virtual
~prop_convt
()
prop_convt
inline
virtual
Generated by
1.8.14