CBMC
Public Types | Public Member Functions | Static Public Member Functions | Protected Attributes | List of all members
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 25 of file literal.h.

Member Typedef Documentation

◆ var_not

typedef unsigned literalt::var_not

Definition at line 31 of file literal.h.

Constructor & Destructor Documentation

◆ literalt() [1/2]

literalt::literalt ( )
inline

Definition at line 34 of file literal.h.

◆ literalt() [2/2]

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

Definition at line 39 of file literal.h.

Member Function Documentation

◆ clear()

void literalt::clear ( void  )
inline

Definition at line 135 of file literal.h.

◆ const_var_no()

static var_not literalt::const_var_no ( )
inlinestatic

Definition at line 171 of file literal.h.

◆ dimacs()

int literalt::dimacs ( ) const
inline

Definition at line 117 of file literal.h.

◆ from_dimacs()

void literalt::from_dimacs ( int  d)
inline

Definition at line 127 of file literal.h.

◆ get()

var_not literalt::get ( ) const
inline

Definition at line 103 of file literal.h.

◆ invert()

void literalt::invert ( )
inline

Definition at line 108 of file literal.h.

◆ is_constant()

bool literalt::is_constant ( ) const
inline

Definition at line 166 of file literal.h.

◆ is_false()

bool literalt::is_false ( ) const
inline

Definition at line 161 of file literal.h.

◆ is_true()

bool literalt::is_true ( ) const
inline

Definition at line 156 of file literal.h.

◆ make_false()

void literalt::make_false ( )
inline

Definition at line 151 of file literal.h.

◆ make_true()

void literalt::make_true ( )
inline

Definition at line 146 of file literal.h.

◆ operator!()

literalt literalt::operator! ( ) const
inline

Definition at line 69 of file literal.h.

◆ operator!=()

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

Definition at line 49 of file literal.h.

◆ operator<()

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

Definition at line 55 of file literal.h.

◆ operator==()

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

Definition at line 44 of file literal.h.

◆ operator^()

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

Definition at line 61 of file literal.h.

◆ operator^=()

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

Definition at line 76 of file literal.h.

◆ set() [1/2]

void literalt::set ( var_not  _l)
inline

Definition at line 93 of file literal.h.

◆ set() [2/2]

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

Definition at line 98 of file literal.h.

◆ sign()

bool literalt::sign ( ) const
inline

Definition at line 88 of file literal.h.

◆ swap()

void literalt::swap ( literalt &  x)
inline

Definition at line 140 of file literal.h.

◆ unused_var_no()

static var_not literalt::unused_var_no ( )
inlinestatic

Definition at line 176 of file literal.h.

◆ var_no()

var_not literalt::var_no ( ) const
inline

Definition at line 83 of file literal.h.

Member Data Documentation

◆ l

var_not literalt::l
protected

Definition at line 182 of file literal.h.

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