cprover
|
#include <threeval.h>
Public Types | |
enum | tv_enumt : unsigned char { tv_enumt::TV_FALSE, tv_enumt::TV_UNKNOWN, tv_enumt::TV_TRUE } |
Public Member Functions | |
bool | is_true () const |
bool | is_false () const |
bool | is_unknown () const |
bool | is_known () const |
const char * | to_string () const |
tv_enumt | get_value () const |
tvt () | |
tvt (bool b) | |
tvt (tv_enumt v) | |
bool | operator== (const tvt other) const |
bool | operator!= (const tvt other) const |
tvt | operator && (const tvt other) const |
tvt | operator|| (const tvt other) const |
tvt | operator! () const |
Static Public Member Functions | |
static tvt | unknown () |
Protected Attributes | |
tv_enumt | value |
Definition at line 19 of file threeval.h.
|
strong |
Enumerator | |
---|---|
TV_FALSE | |
TV_UNKNOWN | |
TV_TRUE |
Definition at line 23 of file threeval.h.
|
inline |
Definition at line 45 of file threeval.h.
Referenced by operator &&(), operator!(), operator||(), and unknown().
|
inlineexplicit |
Definition at line 49 of file threeval.h.
|
inlineexplicit |
Definition at line 53 of file threeval.h.
|
inline |
Definition at line 40 of file threeval.h.
References value.
Referenced by bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), prop_conv_solvert::get(), and boolbvt::get_value().
|
inline |
Definition at line 26 of file threeval.h.
References TV_FALSE, and value.
Referenced by prop_minimizet::fix_objectives(), prop_conv_solvert::get_bool(), counterexample_beautificationt::get_failed_property(), fault_localizationt::get_failed_property(), counterexample_beautificationt::get_minimization_list(), boolbv_mapt::map_entryt::get_value(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), custom_bitvector_domaint::is_bottom(), escape_domaint::is_bottom(), global_may_alias_domaint::is_bottom(), uninitialized_domaint::is_bottom(), invariant_set_domaint::is_bottom(), dep_graph_domaint::is_bottom(), rd_range_domaint::is_bottom(), is_failed_assertion_step(), is_failed_assumption_step(), invariant_set_domaint::merge(), escape_domaint::merge(), global_may_alias_domaint::merge(), custom_bitvector_domaint::merge(), uninitialized_domaint::merge(), rd_range_domaint::merge(), rd_range_domaint::merge_shared(), operator &&(), operator||(), escape_domaint::transform(), global_may_alias_domaint::transform(), uninitialized_domaint::transform(), and fault_localizationt::update_scores().
|
inline |
Definition at line 28 of file threeval.h.
References TV_FALSE, TV_TRUE, and value.
Referenced by symex_bmct::get_unwind(), symex_bmct::get_unwind_recursion(), custom_bitvector_domaint::output(), escape_domaint::output(), global_may_alias_domaint::output(), uninitialized_domaint::output(), invariant_set_domaint::output(), and rd_range_domaint::output().
|
inline |
Definition at line 25 of file threeval.h.
References TV_TRUE, and value.
Referenced by build_goto_trace(), float_utilst::get(), prop_conv_solvert::get_bool(), counterexample_beautificationt::get_failed_property(), fault_localizationt::get_failed_property(), symex_bmct::get_unwind(), symex_bmct::get_unwind_recursion(), boolbv_mapt::map_entryt::get_value(), uninitialized_domaint::is_top(), custom_bitvector_domaint::is_top(), escape_domaint::is_top(), global_may_alias_domaint::is_top(), invariant_set_domaint::is_top(), dep_graph_domaint::is_top(), rd_range_domaint::is_top(), cover_goalst::mark(), operator &&(), operator!(), operator||(), bmc_covert::satisfying_assignment(), java_bytecode_convert_methodt::save_stack_entries(), invariant_propagationt::simplify(), and fault_localizationt::update_scores().
|
inline |
Definition at line 27 of file threeval.h.
References TV_UNKNOWN, and value.
Referenced by symex_bmct::get_unwind(), symex_bmct::get_unwind_recursion(), operator!(), and java_bytecode_convert_methodt::save_stack_entries().
Definition at line 67 of file threeval.h.
References is_false(), is_true(), tvt(), and unknown().
|
inline |
Definition at line 87 of file threeval.h.
References is_true(), is_unknown(), tvt(), and unknown().
|
inline |
Definition at line 62 of file threeval.h.
References value.
|
inline |
Definition at line 57 of file threeval.h.
References value.
Definition at line 77 of file threeval.h.
References is_false(), is_true(), tvt(), and unknown().
const char * tvt::to_string | ( | ) | const |
Definition at line 13 of file threeval.cpp.
References TV_FALSE, TV_TRUE, TV_UNKNOWN, and value.
Referenced by operator<<(), custom_bitvector_domaint::output(), escape_domaint::output(), global_may_alias_domaint::output(), uninitialized_domaint::output(), invariant_set_domaint::output(), and rd_range_domaint::output().
|
inlinestatic |
Definition at line 33 of file threeval.h.
References TV_UNKNOWN, and tvt().
Referenced by invariant_sett::implies_rec(), invariant_sett::is_eq(), invariant_sett::is_le(), java_enum_static_init_unwind_handler(), qbf_quantort::l_get(), qbf_qube_coret::l_get(), cnf_clause_listt::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), dimacs_cnf_dumpt::l_get(), cnf_clause_list_assignmentt::l_get(), dep_graph_domaint::make_entry(), invariant_set_domaint::merge(), global_may_alias_domaint::merge(), escape_domaint::merge(), custom_bitvector_domaint::merge(), uninitialized_domaint::merge(), dep_graph_domaint::merge(), rd_range_domaint::merge(), rd_range_domaint::merge_shared(), simplify_exprt::objects_equal(), simplify_exprt::objects_equal_address_of(), operator &&(), operator!(), operator<=(), operator||(), java_bytecode_convert_methodt::save_stack_entries(), and dep_graph_domaint::transform().
|
protected |
Definition at line 98 of file threeval.h.
Referenced by get_value(), is_false(), is_known(), is_true(), is_unknown(), operator!=(), operator==(), and to_string().