cprover
literalt Class Reference

#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
 

Detailed Description

Definition at line 24 of file literal.h.

Member Typedef Documentation

◆ var_not

typedef unsigned literalt::var_not

Definition at line 30 of file literal.h.

Constructor & Destructor Documentation

◆ literalt() [1/2]

literalt::literalt ( )
inline

Definition at line 33 of file literal.h.

References unused_var_no().

◆ literalt() [2/2]

literalt::literalt ( var_not  v,
bool  sign 
)
inline

Definition at line 38 of file literal.h.

References sign().

Member Function Documentation

◆ clear()

void literalt::clear ( void  )
inline

Definition at line 134 of file literal.h.

References l.

◆ const_var_no()

static var_not literalt::const_var_no ( )
inlinestatic

Definition at line 170 of file literal.h.

Referenced by const_literal(), is_constant(), make_false(), and make_true().

◆ dimacs()

◆ from_dimacs()

void literalt::from_dimacs ( int  d)
inline

Definition at line 126 of file literal.h.

References sign().

◆ get()

var_not literalt::get ( ) const
inline

Definition at line 102 of file literal.h.

References l.

Referenced by read_dimacs_cnf(), and literal_exprt::set_literal().

◆ invert()

void literalt::invert ( )
inline

Definition at line 107 of file literal.h.

References l.

Referenced by operator!().

◆ is_constant()

◆ is_false()

◆ is_true()

◆ make_false()

void literalt::make_false ( )
inline

Definition at line 150 of file literal.h.

References const_var_no().

◆ make_true()

void literalt::make_true ( )
inline

Definition at line 145 of file literal.h.

References const_var_no().

◆ operator!()

literalt literalt::operator! ( ) const
inline

Definition at line 68 of file literal.h.

References invert().

◆ operator!=()

bool literalt::operator!= ( const literalt  other) const
inline

Definition at line 48 of file literal.h.

References l.

◆ operator<()

bool literalt::operator< ( const literalt  other) const
inline

Definition at line 54 of file literal.h.

References l.

◆ operator==()

bool literalt::operator== ( const literalt  other) const
inline

Definition at line 43 of file literal.h.

References l.

◆ operator^()

literalt literalt::operator^ ( const bool  b) const
inline

Definition at line 60 of file literal.h.

References l.

◆ operator^=()

literalt literalt::operator^= ( const bool  a)
inline

Definition at line 75 of file literal.h.

References l.

◆ set() [1/2]

◆ set() [2/2]

void literalt::set ( var_not  v,
bool  sign 
)
inline

Definition at line 97 of file literal.h.

References l, and sign().

◆ sign()

◆ swap()

void literalt::swap ( literalt x)
inline

Definition at line 139 of file literal.h.

References l.

◆ unused_var_no()

static var_not literalt::unused_var_no ( )
inlinestatic

◆ var_no()

var_not literalt::var_no ( ) const
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().

Member Data Documentation

◆ l


The documentation for this class was generated from the following file: