CVC3::Literal Class Reference

#include <variable.h>

Collaboration diagram for CVC3::Literal:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Attributes

Friends


Detailed Description

Definition at line 120 of file variable.h.


Constructor & Destructor Documentation

CVC3::Literal::Literal ( const Variable v,
bool  positive = true 
) [inline]

Definition at line 126 of file variable.h.

CVC3::Literal::Literal (  )  [inline]

Definition at line 129 of file variable.h.

CVC3::Literal::Literal ( VariableManager vm,
const Expr e 
) [inline]

Definition at line 132 of file variable.h.


Member Function Documentation

Variable& CVC3::Literal::getVar (  )  [inline]

Definition at line 134 of file variable.h.

References d_var.

Referenced by getScope(), CVC3::operator!(), CVC3::operator<<(), and CVC3::printLit().

const Variable& CVC3::Literal::getVar (  )  const [inline]

Definition at line 135 of file variable.h.

References d_var.

bool CVC3::Literal::isPositive (  )  const [inline]

Definition at line 136 of file variable.h.

References d_negative.

bool CVC3::Literal::isNegative (  )  const [inline]

Definition at line 137 of file variable.h.

References d_negative.

Referenced by CVC3::operator!(), CVC3::operator<<(), CVC3::printLit(), and CVC3::SearchEngineFast::recordFact().

bool CVC3::Literal::isNull (  )  const [inline]

Definition at line 138 of file variable.h.

References d_var, and CVC3::Variable::isNull().

const Expr& CVC3::Literal::getExpr (  )  const [inline]

Definition at line 140 of file variable.h.

References d_negative, d_var, CVC3::Variable::getExpr(), and CVC3::Variable::getNegExpr().

Referenced by CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchEngineFast::propagate(), and CVC3::SearchEngineFast::recordFact().

int CVC3::Literal::getValue (  )  const [inline]

Definition at line 144 of file variable.h.

References d_negative, d_var, and CVC3::Variable::getValue().

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::printLit(), CVC3::SearchEngineFast::propagate(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::recordFact(), and CVC3::SearchEngineFast::split().

int CVC3::Literal::getScope (  )  const [inline]

Definition at line 148 of file variable.h.

References CVC3::Variable::getScope(), and getVar().

Referenced by CVC3::printLit(), and CVC3::SearchEngineFast::recordFact().

void CVC3::Literal::setValue ( const Theorem thm  )  [inline]

Definition at line 153 of file variable.h.

References d_var, CVC3::Theorem::getScope(), and CVC3::Variable::setValue().

Referenced by CVC3::SearchEngineFast::newIntAssumption(), and CVC3::SearchEngineFast::recordFact().

void CVC3::Literal::setValue ( const Theorem thm,
int  scope 
) [inline]

Definition at line 156 of file variable.h.

References d_var, and CVC3::Variable::setValue().

const Theorem& CVC3::Literal::getTheorem (  )  const [inline]

Definition at line 159 of file variable.h.

References d_var, and CVC3::Variable::getTheorem().

Referenced by CVC3::Circuit::propagate().

Theorem CVC3::Literal::deriveTheorem (  )  const [inline]

Definition at line 164 of file variable.h.

References d_var, and CVC3::Variable::deriveTheorem().

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::recordFact(), and CVC3::SearchEngineFast::split().

unsigned& CVC3::Literal::count (  )  [inline]

Definition at line 166 of file variable.h.

References CVC3::Variable::count(), d_negative, and d_var.

Referenced by CVC3::ClauseValue::ClauseValue(), CVC3::operator<<(), CVC3::SearchImplBase::Splitter::operator=(), CVC3::SearchImplBase::Splitter::Splitter(), and CVC3::SearchImplBase::Splitter::~Splitter().

unsigned& CVC3::Literal::countPrev (  )  [inline]

Definition at line 167 of file variable.h.

References CVC3::Variable::countPrev(), d_negative, and d_var.

int& CVC3::Literal::score (  )  [inline]

Definition at line 168 of file variable.h.

References d_negative, d_var, and CVC3::Variable::score().

Referenced by compareLits(), and CVC3::operator<<().

bool& CVC3::Literal::added (  )  [inline]

Definition at line 169 of file variable.h.

References CVC3::Variable::added(), d_negative, and d_var.

unsigned CVC3::Literal::count (  )  const [inline]

Definition at line 171 of file variable.h.

References CVC3::Variable::count(), d_negative, and d_var.

unsigned CVC3::Literal::countPrev (  )  const [inline]

Definition at line 172 of file variable.h.

References CVC3::Variable::countPrev(), d_negative, and d_var.

int CVC3::Literal::score (  )  const [inline]

Definition at line 173 of file variable.h.

References d_negative, d_var, and CVC3::Variable::score().

bool CVC3::Literal::added (  )  const [inline]

Definition at line 174 of file variable.h.

References CVC3::Variable::added(), d_negative, and d_var.

std::vector<std::pair<Clause, int> >& CVC3::Literal::wp (  )  const [inline]

Definition at line 176 of file variable.h.

References d_negative, d_var, and CVC3::Variable::wp().

Referenced by CVC3::SearchEngineFast::wp().

string CVC3::Literal::toString (  )  const

Definition at line 211 of file variable.cpp.

Referenced by CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::newIntAssumption(), and CVC3::SearchEngineFast::split().


Friends And Related Function Documentation

std::ostream& operator<< ( std::ostream &  os,
const Literal l 
) [friend]

bool operator== ( const Literal l1,
const Literal l2 
) [friend]

Definition at line 182 of file variable.h.


Member Data Documentation

Variable CVC3::Literal::d_var [private]

Definition at line 122 of file variable.h.

Referenced by added(), count(), countPrev(), deriveTheorem(), getExpr(), getTheorem(), getValue(), getVar(), isNull(), score(), setValue(), and wp().

bool CVC3::Literal::d_negative [private]

Definition at line 123 of file variable.h.

Referenced by added(), count(), countPrev(), getExpr(), getValue(), isNegative(), isPositive(), score(), and wp().


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:17:23 2009 for CVC3 by  doxygen 1.5.2