CBMC
equalityt Member List
This is the complete list of members for
equalityt
, including all inherited members.
add_constraints_to_prop
(const exprt &expr, bool value)
prop_conv_solvert
private
add_equality_constraints
()
equalityt
protected
virtual
add_equality_constraints
(const typestructt &typestruct)
equalityt
protected
virtual
assumption_stack
prop_conv_solvert
protected
cache
prop_conv_solvert
protected
cachet
typedef
prop_conv_solvert
clear_cache
()
prop_conv_solvert
inline
virtual
context_literal_counter
prop_conv_solvert
protected
context_prefix
prop_conv_solvert
protected
static
context_size_stack
prop_conv_solvert
protected
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
dec_solve
(const exprt &) override
prop_conv_solvert
virtual
decision_procedure_text
() const override
prop_conv_solvert
virtual
elements_revt
typedef
equalityt
protected
elementst
typedef
equalityt
protected
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
(propt &_prop, message_handlert &message_handler)
equalityt
inline
finish_eager_conversion
() override
equalityt
inline
virtual
freeze_all
prop_conv_solvert
get
(const exprt &expr) const override
prop_conv_solvert
virtual
get_bool
(const exprt &expr) const
prop_conv_solvert
protected
virtual
get_cache
() const
prop_conv_solvert
inline
get_hardness_collector
()
prop_conv_solvert
inline
get_literal
(const irep_idt &symbol)
prop_conv_solvert
protected
virtual
get_number_of_solver_calls
() const override
prop_conv_solvert
virtual
get_symbols
() const
prop_conv_solvert
inline
handle
(const exprt &expr) override
prop_conv_solvert
virtual
ignoring
(const exprt &expr)
prop_conv_solvert
protected
virtual
is_in_conflict
(const exprt &expr) const override
prop_conv_solvert
virtual
l_get
(literalt a) const override
prop_conv_solvert
inline
virtual
log
prop_conv_solvert
protected
operator()
()
decision_proceduret
operator()
(const exprt &assumption)
decision_proceduret
pop
() override
prop_conv_solvert
virtual
post_processing_done
prop_conv_solvert
protected
print_assignment
(std::ostream &out) const override
prop_conv_solvert
virtual
prop
prop_conv_solvert
protected
prop_conv_solvert
(propt &_prop, message_handlert &message_handler)
prop_conv_solvert
inline
push
() override
prop_conv_solvert
virtual
push
(const std::vector< exprt > &assumptions) override
prop_conv_solvert
virtual
resultt
enum name
decision_proceduret
set_all_frozen
()
prop_conv_solvert
set_equality_to_true
(const equal_exprt &expr)
prop_conv_solvert
protected
virtual
set_frozen
(literalt)
prop_conv_solvert
set_frozen
(const bvt &)
prop_conv_solvert
set_time_limit_seconds
(uint32_t lim) override
prop_conv_solvert
inline
virtual
set_to
(const exprt &expr, bool value) override
prop_conv_solvert
virtual
set_to_false
(const exprt &)
decision_proceduret
set_to_true
(const exprt &)
decision_proceduret
SUB
typedef
equalityt
symbols
prop_conv_solvert
protected
symbolst
typedef
prop_conv_solvert
typemap
equalityt
protected
typemapt
typedef
equalityt
protected
use_cache
prop_conv_solvert
~conflict_providert
()=default
conflict_providert
virtual
~decision_proceduret
()
decision_proceduret
virtual
~prop_conv_solvert
()=default
prop_conv_solvert
virtual
~prop_convt
()
prop_convt
inline
virtual
~solver_resource_limitst
()=default
solver_resource_limitst
virtual
~stack_decision_proceduret
()=default
stack_decision_proceduret
virtual
Generated by
1.9.1