CVC3: SAT::Clause Class Reference

CVC3

#include <cnf.h>

Collaboration diagram for SAT::Clause:

Collaboration graph

Public Types
typedef std::vector< Lit > ::const_iterator	const_iterator

Public Member Functions
	Clause ()

	Clause (const Clause &clause)

const_iterator	begin () const

const_iterator	end () const

void	clear ()

unsigned	size () const

void	addLiteral (Lit l)

unsigned	getMaxVar () const

bool	isSatisfied () const

bool	isUnit () const

bool	isNull () const

void	setSatisfied ()

void	setUnit ()

void	print () const

void	setClauseTheorem (CVC3::Theorem thm)

CVC3::Theorem	getClauseTheorem () const

Private Attributes
int	d_satisfied:1

int	d_unit:1

std::vector< Lit >	d_lits

CVC3::Theorem	d_reason

Detailed Description

Definition at line 78 of file cnf.h.

Member Typedef Documentation

typedef std::vector<Lit>::const_iterator SAT::Clause::const_iterator

Definition at line 90 of file cnf.h.

Constructor & Destructor Documentation

SAT::Clause::Clause ( )

inline

Definition at line 86 of file cnf.h.

SAT::Clause::Clause ( const Clause & clause )

inline

Definition at line 88 of file cnf.h.

Member Function Documentation

const_iterator SAT::Clause::begin ( ) const

inline

Definition at line 93 of file cnf.h.

References d_lits.

Referenced by SAT::DPLLTBasic::addNewClause(), MiniSat::cvcToMiniSat(), and SAT::CNF_Formula::operator+=().

const_iterator SAT::Clause::end ( ) const

inline

Definition at line 94 of file cnf.h.

References d_lits.

Referenced by SAT::DPLLTBasic::addNewClause(), MiniSat::cvcToMiniSat(), and SAT::CNF_Formula::operator+=().

void SAT::Clause::clear ( )

inline

Definition at line 96 of file cnf.h.

References d_lits, d_satisfied, and d_unit.

unsigned SAT::Clause::size ( ) const

inline

Definition at line 97 of file cnf.h.

References d_lits.

Referenced by SAT::DPLLTBasic::addNewClause().

void SAT::Clause::addLiteral ( Lit l )

inline

Definition at line 98 of file cnf.h.

References d_lits, and d_satisfied.

Referenced by SAT::CNF_Formula::addLiteral().

unsigned SAT::Clause::getMaxVar ( ) const

Definition at line 30 of file cnf.cpp.

References DebugAssert, and CVC3::max().

Referenced by SAT::DPLLTBasic::addNewClause().

bool SAT::Clause::isSatisfied ( ) const

inline

Definition at line 100 of file cnf.h.

References d_satisfied.

bool SAT::Clause::isUnit ( ) const

inline

Definition at line 101 of file cnf.h.

References d_unit.

Referenced by SAT::CNF_Formula::operator+=().

bool SAT::Clause::isNull ( ) const

inline

Definition at line 102 of file cnf.h.

References d_lits.

void SAT::Clause::setSatisfied ( )

inline

Definition at line 103 of file cnf.h.

References d_satisfied.

void SAT::Clause::setUnit ( )

inline

Definition at line 104 of file cnf.h.

References d_unit.

void SAT::Clause::print ( ) const

Definition at line 42 of file cnf.cpp.

References std::endl().

Referenced by SAT::CNF_Formula::print().

void SAT::Clause::setClauseTheorem ( CVC3::Theorem thm )

inline

Definition at line 106 of file cnf.h.

References d_reason.

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().

CVC3::Theorem SAT::Clause::getClauseTheorem ( ) const

inline

Definition at line 108 of file cnf.h.

References d_reason.

Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::cvcToMiniSat(), and SAT::CNF_Formula::operator+=().

Member Data Documentation

int SAT::Clause::d_satisfied

private

Definition at line 79 of file cnf.h.

Referenced by addLiteral(), clear(), isSatisfied(), and setSatisfied().

int SAT::Clause::d_unit

private

Definition at line 80 of file cnf.h.

Referenced by clear(), isUnit(), and setUnit().

std::vector<Lit> SAT::Clause::d_lits

private

Definition at line 81 of file cnf.h.

Referenced by addLiteral(), begin(), clear(), end(), isNull(), and size().

CVC3::Theorem SAT::Clause::d_reason

private

Definition at line 82 of file cnf.h.

Referenced by getClauseTheorem(), and setClauseTheorem().

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