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 |
Definition at line 33 of file literal.h.
References unused_var_no().
|
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 |
|
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(), equalityt::equality2(), bv_utilst::full_adder(), 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(), cnft::lselect(), operator<<(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), satcheck_lingelingt::set_frozen(), satcheck_glucose_simplifiert::set_frozen(), satcheck_minisat_simplifiert::set_frozen(), boolbv_mapt::set_literals(), satcheck_minisat2_baset< Minisat::Solver >::set_polarity(), and satcheck_glucose_baset< Glucose::SimpSolver >::set_polarity().
|
inline |
Definition at line 160 of file literal.h.
References is_constant(), and sign().
Referenced by is_false(), satcheck_booleforce_baset::l_get(), satcheck_minisat1_baset::l_get(), satcheck_zchaff_baset::l_get(), qbf_squolem_coret::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), cnf_clause_list_assignmentt::l_get(), smt2_convt::l_get(), cnft::land(), cnft::lor(), cnft::lxor(), prop_minimizet::operator()(), 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(), is_true(), satcheck_booleforce_baset::l_get(), satcheck_minisat1_baset::l_get(), satcheck_zchaff_baset::l_get(), qbf_squolem_coret::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), cnf_clause_list_assignmentt::l_get(), smt2_convt::l_get(), cnft::land(), cnft::lor(), cnft::lxor(), operator<<(), 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(), literal_exprt::get_literal(), and cnft::new_variable().
|
inline |
|
inline |
Definition at line 87 of file literal.h.
References l.
Referenced by smt2_convt::convert_literal(), dimacs(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), from_dimacs(), is_false(), is_true(), satcheck_booleforce_baset::l_get(), satcheck_lingelingt::l_get(), satcheck_picosatt::l_get(), satcheck_minisat1_baset::l_get(), satcheck_zchaff_baset::l_get(), qbf_qube_coret::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), qbf_bdd_certificatet::l_get(), cnf_clause_list_assignmentt::l_get(), smt2_convt::l_get(), literalt(), qbf_bdd_coret::lor(), cnft::lselect(), operator<<(), set(), satcheck_zchaff_baset::set_assignment(), satcheck_minisat1_baset::set_assignment(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), and satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment().
|
inlinestatic |
Definition at line 175 of file literal.h.
Referenced by boolbvt::convert_bv(), literalt(), and cnft::process_clause().
|
inline |
Definition at line 82 of file literal.h.
References l.
Referenced by smt2_convt::convert_literal(), dimacs(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), qdimacs_cnft::find_quantifier(), 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_minisat1_coret::is_in_core(), qdimacs_cnft::is_quantified(), satcheck_booleforce_baset::l_get(), satcheck_picosatt::l_get(), satcheck_lingelingt::l_get(), satcheck_zchaff_baset::l_get(), satcheck_minisat1_baset::l_get(), qbf_qube_coret::l_get(), qbf_squolem_coret::l_get(), satcheck_minisat2_baset< Minisat::Solver >::l_get(), satcheck_glucose_baset< Glucose::SimpSolver >::l_get(), qbf_bdd_certificatet::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<<(), satcheck_zchaff_baset::set_assignment(), satcheck_minisat1_baset::set_assignment(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), satcheck_glucose_simplifiert::set_frozen(), satcheck_minisat_simplifiert::set_frozen(), boolbv_mapt::set_literals(), satcheck_minisat2_baset< Minisat::Solver >::set_polarity(), satcheck_glucose_baset< Glucose::SimpSolver >::set_polarity(), qbf_squolemt::set_quantifier(), qbf_squolem_coret::set_quantifier(), and qdimacs_cnft::set_quantifier().
|
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().