CVC3  2.4.1
Public Types | Public Member Functions | Static Public Member Functions | Private Attributes | List of all members
SAT::Var Class Reference

#include <cnf.h>

Public Types

enum  Val { UNKNOWN = -1, FALSE_VAL, TRUE_VAL }
 

Public Member Functions

 Var ()
 
 Var (int index)
 
 operator int ()
 
bool isNull () const
 
void reset ()
 
int getIndex () const
 
bool isVar () const
 
bool operator== (const Var &var) const
 

Static Public Member Functions

static Val invertValue (Val)
 

Private Attributes

int d_index
 

Detailed Description

Definition at line 34 of file cnf.h.

Member Enumeration Documentation

Enumerator
UNKNOWN 
FALSE_VAL 
TRUE_VAL 

Definition at line 37 of file cnf.h.

Constructor & Destructor Documentation

SAT::Var::Var ( )
inline

Definition at line 39 of file cnf.h.

SAT::Var::Var ( int  index)
inline

Definition at line 40 of file cnf.h.

Member Function Documentation

Var::Val SAT::Var::invertValue ( Var::Val  v)
inlinestatic

Definition at line 48 of file cnf.h.

References UNKNOWN.

Referenced by CVC3::SearchSat::getValue().

SAT::Var::operator int ( )
inline

Definition at line 41 of file cnf.h.

References d_index.

bool SAT::Var::isNull ( ) const
inline

Definition at line 42 of file cnf.h.

References d_index.

Referenced by SAT::CNF_Manager::concreteVar(), SAT::Lit::Lit(), and CVC3::SearchSat::setValue().

void SAT::Var::reset ( )
inline

Definition at line 43 of file cnf.h.

References d_index.

int SAT::Var::getIndex ( ) const
inline

Definition at line 44 of file cnf.h.

References d_index.

Referenced by MiniSat::cvcToMiniSat().

bool SAT::Var::isVar ( ) const
inline

Definition at line 45 of file cnf.h.

References d_index.

Referenced by CVC3::SearchSat::getValue(), SAT::CNF_Manager::numFanins(), and SAT::CNF_Manager::numFanouts().

bool SAT::Var::operator== ( const Var var) const
inline

Definition at line 46 of file cnf.h.

References d_index.

Member Data Documentation

int SAT::Var::d_index
private

Definition at line 35 of file cnf.h.

Referenced by getIndex(), isNull(), isVar(), operator int(), operator==(), and reset().


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