CVC3::Literal Class Reference

#include <variable.h>

Collaboration diagram for CVC3::Literal:

[legend]

List of all members.

Public Member Functions

• Literal (const Variable &v, bool positive=true)
• Literal ()
• Literal (VariableManager *vm, const Expr &e)
• Variable & getVar ()
• const Variable & getVar () const
• bool isPositive () const
• bool isNegative () const
• bool isNull () const
• const Expr & getExpr () const
• int getValue () const
• int getScope () const
• void setValue (const Theorem &thm)
• void setValue (const Theorem &thm, int scope)
• const Theorem & getTheorem () const
• Theorem deriveTheorem () const
• unsigned & count ()
• unsigned & countPrev ()
• int & score ()
• bool & added ()
• unsigned count () const
• unsigned countPrev () const
• int score () const
• bool added () const
• std::vector< std::pair< Clause,
  int > > & wp () const
• std::string toString () const

Private Attributes

• Variable d_var
• bool d_negative

Friends

• std::ostream & operator<< (std::ostream &os, const Literal &l)
• bool operator== (const Literal &l1, const Literal &l2)

---

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::bcp(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::recordFact(), and CVC3::SearchEngineFast::updateLitCounts().

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::bcp(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::printLit(), CVC3::SearchEngineFast::propagate(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::split(), and CVC3::SearchEngineFast::traceConflict().

int CVC3::Literal::getScope

(

)

const [inline]

Definition at line 148 of file variable.h.

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

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

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::SearchImplBase::Splitter::operator=(), CVC3::SearchImplBase::SearchImplBase::Splitter::Splitter(), and CVC3::SearchImplBase::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(), CVC3::SearchEngineFast::findSplitter(), 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.

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

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::bcp(), 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:

• variable.h
• variable.cpp