cprover
|
#include <literal.h>
Public Types | |
typedef unsigned | var_not |
Public Member Functions | |
literalt () | |
literalt (var_not v, bool sign) | |
bool | operator== (const literalt other) const |
bool | operator!= (const literalt other) const |
bool | operator< (const literalt other) const |
literalt | operator^ (const bool b) const |
literalt | operator! () const |
literalt | operator^= (const bool a) |
var_not | var_no () const |
bool | sign () const |
void | set (var_not _l) |
void | set (var_not v, bool sign) |
var_not | get () const |
void | invert () |
int | dimacs () const |
void | from_dimacs (int d) |
void | clear () |
void | swap (literalt &x) |
void | make_true () |
void | make_false () |
bool | is_true () const |
bool | is_false () const |
bool | is_constant () const |
Static Public Member Functions | |
static var_not | const_var_no () |
static var_not | unused_var_no () |
Protected Attributes | |
var_not | l |
typedef unsigned literalt::var_not |
|
inline |
|
inline |
|
inlinestatic |
Definition at line 170 of file literal.h.
Referenced by const_literal(), is_constant(), make_false(), and make_true().
|
inline |
Definition at line 116 of file literal.h.
References sign(), and var_no().
Referenced by qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), satcheck_picosatt::is_in_conflict(), satcheck_lingelingt::is_in_conflict(), satcheck_picosatt::l_get(), satcheck_lingelingt::l_get(), pbs_dimacs_cnft::l_get(), and satcheck_lingelingt::set_frozen().
|
inline |
|
inline |
Definition at line 102 of file literal.h.
References l.
Referenced by read_dimacs_cnf(), and literal_exprt::set_literal().
|
inline |
|
inline |
Definition at line 165 of file literal.h.
References const_var_no(), and var_no().
Referenced by bv_minimizet::add_objective(), bv_refinementt::approximationt::add_over_assumption(), bv_refinementt::approximationt::add_under_assumption(), bv_utilst::carry(), aig_prop_solvert::compute_phase(), prop_conv_solvert::convert(), equalityt::equality2(), bv_utilst::full_adder(), aigt::get_terminals_rec(), satcheck_glucose_simplifiert::is_eliminated(), satcheck_minisat_simplifiert::is_eliminated(), is_false(), satcheck_picosatt::is_in_conflict(), satcheck_lingelingt::is_in_conflict(), is_true(), satcheck_lingelingt::l_get(), satcheck_picosatt::l_get(), satcheck_precosatt::l_get(), cnft::lselect(), operator<<(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), satcheck_lingelingt::set_frozen(), satcheck_minisat_simplifiert::set_frozen(), satcheck_glucose_simplifiert::set_frozen(), boolbv_mapt::set_literals(), satcheck_glucose_baset< Glucose::SimpSolver >::set_polarity(), and satcheck_minisat2_baset< Minisat::Solver >::set_polarity().
|
inline |
Definition at line 160 of file literal.h.
References is_constant(), and sign().
Referenced by satcheck_limmatt::l_get(), satcheck_booleforce_baset::l_get(), satcheck_smvsatt::l_get(), satcheck_minisat1_baset::l_get(), satcheck_zchaff_baset::l_get(), qbf_squolem_coret::l_get(), cvc_convt::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), smt1_propt::l_get(), smt2_propt::l_get(), smt1_convt::l_get(), cnf_clause_list_assignmentt::l_get(), smt2_convt::l_get(), cnft::land(), aig_prop_baset::land(), cnft::lor(), aig_prop_baset::lselect(), cnft::lxor(), aig_prop_baset::lxor(), prop_minimizet::operator()(), aigt::output_dot_edge(), smt1_propt::set_assignment(), smt2_propt::set_assignment(), and bv_utilst::unsigned_divider().
|
inline |
Definition at line 155 of file literal.h.
References is_constant(), and sign().
Referenced by bv_utilst::full_adder(), satcheck_limmatt::l_get(), satcheck_booleforce_baset::l_get(), satcheck_smvsatt::l_get(), satcheck_minisat1_baset::l_get(), satcheck_zchaff_baset::l_get(), qbf_squolem_coret::l_get(), cvc_convt::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), smt1_propt::l_get(), smt2_propt::l_get(), smt1_convt::l_get(), cnf_clause_list_assignmentt::l_get(), smt2_convt::l_get(), cnft::land(), aig_prop_baset::land(), cnft::lor(), aig_prop_baset::lselect(), cnft::lxor(), aig_prop_baset::lxor(), operator<<(), aigt::output_dot_edge(), smt1_propt::set_assignment(), smt2_propt::set_assignment(), float_utilst::to_integer(), and bv_utilst::unsigned_divider().
|
inline |
Definition at line 150 of file literal.h.
References const_var_no().
|
inline |
Definition at line 145 of file literal.h.
References const_var_no().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 92 of file literal.h.
References l.
Referenced by cnf_clause_list_assignmentt::copy_assignment_from(), cvc_propt::def_cvc_literal(), dplib_propt::def_dplib_literal(), smt2_propt::define_new_variable(), literal_exprt::get_literal(), aig_nodet::make_var(), aigt::new_node(), cnft::new_variable(), smt1_propt::new_variable(), smt2_propt::new_variable(), cvc_propt::new_variable(), dplib_propt::new_variable(), aigt::print(), and read_dimacs_cnf().
|
inline |
|
inline |
Definition at line 87 of file literal.h.
References l.
Referenced by aig_prop_solvert::compute_phase(), cvc_convt::convert_literal(), smt1_convt::convert_literal(), smt2_convt::convert_literal(), aig_prop_solvert::convert_node(), cvc_propt::cvc_literal(), dimacs(), dplib_propt::dplib_literal(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), from_dimacs(), is_false(), is_true(), satcheck_limmatt::l_get(), satcheck_booleforce_baset::l_get(), satcheck_picosatt::l_get(), satcheck_lingelingt::l_get(), satcheck_precosatt::l_get(), satcheck_smvsatt::l_get(), satcheck_zchaff_baset::l_get(), satcheck_minisat1_baset::l_get(), qbf_qube_coret::l_get(), cvc_convt::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), qbf_bdd_certificatet::l_get(), smt1_propt::l_get(), smt2_propt::l_get(), cvc_propt::l_get(), dplib_propt::l_get(), smt1_convt::l_get(), cnf_clause_list_assignmentt::l_get(), smt2_convt::l_get(), literalt(), qbf_bdd_coret::lor(), cnft::lselect(), operator<<(), aigt::output_dot_edge(), aigt::print(), set(), satcheck_zchaff_baset::set_assignment(), satcheck_minisat1_baset::set_assignment(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), smt1_propt::smt1_literal(), smt2_propt::smt2_literal(), and aig_prop_solvert::usage_count().
|
inlinestatic |
Definition at line 175 of file literal.h.
Referenced by boolbvt::convert_bv(), aig_nodet::is_and(), aig_nodet::is_var(), literalt(), aig_nodet::make_var(), and cnft::process_clause().
|
inline |
Definition at line 82 of file literal.h.
References l.
Referenced by aig_prop_solvert::compute_phase(), cvc_convt::convert_literal(), smt1_convt::convert_literal(), smt2_convt::convert_literal(), aig_prop_solvert::convert_node(), cvc_propt::cvc_literal(), dimacs(), dplib_propt::dplib_literal(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), qdimacs_cnft::find_quantifier(), aigt::get_node(), aigt::get_terminals_rec(), aig_nodet::is_and(), is_constant(), satcheck_glucose_simplifiert::is_eliminated(), satcheck_minisat_simplifiert::is_eliminated(), satcheck_minisat1_baset::is_in_conflict(), satcheck_glucose_baset< Glucose::SimpSolver >::is_in_conflict(), satcheck_minisat2_baset< Minisat::Solver >::is_in_conflict(), satcheck_zcoret::is_in_core(), qbf_squolem_coret::is_in_core(), satcheck_booleforce_coret::is_in_core(), satcheck_smvsat_coret::is_in_core(), satcheck_minisat1_coret::is_in_core(), qdimacs_cnft::is_quantified(), aig_nodet::is_var(), satcheck_limmatt::l_get(), satcheck_booleforce_baset::l_get(), satcheck_lingelingt::l_get(), satcheck_picosatt::l_get(), satcheck_smvsatt::l_get(), satcheck_precosatt::l_get(), satcheck_zchaff_baset::l_get(), satcheck_minisat1_baset::l_get(), qbf_qube_coret::l_get(), qbf_squolem_coret::l_get(), cvc_convt::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), qbf_bdd_certificatet::l_get(), smt1_propt::l_get(), smt2_propt::l_get(), cvc_propt::l_get(), dplib_propt::l_get(), smt1_convt::l_get(), cnf_clause_list_assignmentt::l_get(), smt2_convt::l_get(), qbf_bdd_coret::lor(), qbf_squolem_coret::m_get(), qbf_bdd_coret::new_variable(), operator<<(), aigt::output_dot_edge(), aigt::print(), satcheck_zchaff_baset::set_assignment(), satcheck_minisat1_baset::set_assignment(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), smt1_propt::set_assignment(), smt2_propt::set_assignment(), satcheck_glucose_simplifiert::set_frozen(), satcheck_minisat_simplifiert::set_frozen(), boolbv_mapt::set_literals(), satcheck_glucose_baset< Glucose::SimpSolver >::set_polarity(), satcheck_minisat2_baset< Minisat::Solver >::set_polarity(), qbf_squolemt::set_quantifier(), qbf_squolem_coret::set_quantifier(), qdimacs_cnft::set_quantifier(), smt1_propt::smt1_literal(), smt2_propt::smt2_literal(), and aig_prop_solvert::usage_count().
|
protected |
Definition at line 181 of file literal.h.
Referenced by clear(), get(), boolbv_mapt::get_literals(), invert(), operator!=(), operator<(), operator==(), operator^(), operator^=(), boolbvt::post_process_quantifiers(), set(), sign(), swap(), and var_no().