CVC3::Theorem Class Reference

#include <theorem.h>

Collaboration diagram for CVC3::Theorem:

[legend]

List of all members.

Public Member Functions

• void printDebug () const
• Theorem ()
• Theorem (const Theorem &th)
• Theorem & operator= (const Theorem &th)
• ~Theorem ()
• bool withProof () const
• bool withAssumptions () const
• bool isNull () const
• bool isRewrite () const
• bool isAssump () const
• bool isRefl () const
• Expr getExpr () const
• const Expr & getLHS () const
• const Expr & getRHS () const
• void GetSatAssumptions (std::vector< Theorem > &assumptions) const
• void getLeafAssumptions (std::vector< Expr > &assumptions, bool negate=false) const
• void getAssumptionsAndCong (std::vector< Expr > &assumptions, std::vector< Expr > &congruences, bool negate=false) const
• const Assumptions & getAssumptionsRef () const
• Proof getProof () const
• int getScope () const
• unsigned getQuantLevel () const

  Return quantification level for this theorem.
  

• unsigned getQuantLevelDebug () const
• void setQuantLevel (unsigned level)

  Set the quantification level for this theorem.
  

• size_t hash () const
• std::string toString () const
• void printx () const
• void printxnodag () const
• void pprintx () const
• void pprintxnodag () const
• void print () const
• std::ostream & print (std::ostream &os, const std::string &name) const

  Printing a theorem to a stream, calling it "name".
  

Methods for Theorem Attributes

Several attributes used in conflict analysis and assumptions graph traversals.

• bool isFlagged () const

  Check if the flag attribute is set.
  

• void clearAllFlags () const

  Clear the flag attribute in all the theorems.
  

• void setFlag () const

  Set the flag attribute.
  

• void setSubst () const

  Set flag stating that theorem is an instance of substitution.
  

• bool isSubst () const

  Is theorem an instance of substitution.
  

• void setExpandFlag (bool val) const

  Set the "expand" attribute.
  

• bool getExpandFlag () const

  Check the "expand" attribute.
  

• void setLitFlag (bool val) const

  Set the "literal" attribute.
  

• bool getLitFlag () const

  Check the "literal" attribute.
  

• bool isAbsLiteral () const

  Check if the theorem is a literal.
  

• bool refutes (const Expr &e) const

  Check if the flag attribute is set.
  

• bool proves (const Expr &e) const

  Check if the flag attribute is set.
  

• bool matches (const Expr &e) const

  Check if the flag attribute is set.
  

• void setCachedValue (int value) const

  Check if the flag attribute is set.
  

• int getCachedValue () const

  Check if the flag attribute is set.
  

Static Public Member Functions

• static bool TheoremEq (const Theorem &t1, const Theorem &t2)

Private Member Functions

• Theorem (TheoremValue *thm)

  Constructor only used by TheoremValue for assumptions.
  

• Theorem (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)

  Constructor for a new theorem.
  

• Theorem (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)

  Constructor for rewrite theorems.
  

• Theorem (const Expr &e)

  Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi.
  

• void recursivePrint (int &i) const
• void getAssumptionsRec (std::set< Expr > &assumptions) const
• void getAssumptionsAndCongRec (std::set< Expr > &assumptions, std::vector< Expr > &congruences) const
• void GetSatAssumptionsRec (std::vector< Theorem > &assumptions) const
• ExprValue * exprValue () const
• TheoremValue * thm () const

Private Attributes

• union {
  •    intptr_t    d_thm
  •    ExprValue *    d_expr
• };

Friends

• class TheoremProducer
• class Theorem3
• class RegTheoremValue
• class RWTheoremValue
• int compare (const Theorem &t1, const Theorem &t2)

  Compare Theorems by their expressions. Return -1, 0, or 1.
  

• int compare (const Theorem &t1, const Expr &e2)

  Compare a Theorem with an Expr (as if Expr is a Theorem).
  

• int compareByPtr (const Theorem &t1, const Theorem &t2)

  Compare Theorems by TheoremValue pointers. Return -1, 0, or 1.
  

• bool operator== (const Theorem &t1, const Theorem &t2)

  Equality is w.r.t. compare().
  

• bool operator!= (const Theorem &t1, const Theorem &t2)

  Disequality is w.r.t. compare().
  

• std::ostream & operator<< (std::ostream &os, const Theorem &t)

---

Detailed Description

Definition at line 76 of file theorem.h.

---

Constructor & Destructor Documentation

CVC3::Theorem::Theorem

(

TheoremValue *

thm

)

[inline, private]

Constructor only used by TheoremValue for assumptions.

Definition at line 109 of file theorem.h.

CVC3::Theorem::Theorem	(	TheoremManager *	tm,
		const Expr &	thm,
		const Assumptions &	assump,
		const Proof &	pf,
		bool	isAssump = false,
		int	scope = -1
	)			[private]

Constructor for a new theorem.

Definition at line 130 of file theorem.cpp.

References CVC3::Expr::d_expr, d_expr, CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, CVC3::TheoremManager::getMM(), CVC3::TheoremManager::getRWMM(), CVC3::ExprValue::incRefcount(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::Proof::isNull(), RegTheoremValue, RWTheoremValue, toString(), and withProof().

CVC3::Theorem::Theorem	(	TheoremManager *	tm,
		const Expr &	lhs,
		const Expr &	rhs,
		const Assumptions &	assump,
		const Proof &	pf,
		bool	isAssump = false,
		int	scope = -1
	)			[private]

Constructor for rewrite theorems.

These use a special efficient subclass of TheoremValue for theorems which represent rewrites: A |- t = t' or A |- phi<=>phi'

Definition at line 151 of file theorem.cpp.

References CVC3::Expr::d_expr, d_expr, CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, CVC3::TheoremManager::getRWMM(), CVC3::ExprValue::incRefcount(), CVC3::Proof::isNull(), RWTheoremValue, toString(), and withProof().

CVC3::Theorem::Theorem

(

const Expr &

e

)

[private]

Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi.

Definition at line 181 of file theorem.cpp.

References d_expr, and CVC3::ExprValue::incRefcount().

CVC3::Theorem::Theorem

(

)

[inline]

Definition at line 151 of file theorem.h.

CVC3::Theorem::Theorem

(

const Theorem &

th

)

Definition at line 169 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, exprValue(), CVC3::ExprValue::incRefcount(), CVC3::int2string(), and thm().

CVC3::Theorem::~Theorem

(

)

Definition at line 187 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, d_thm, CVC3::ExprValue::decRefcount(), CVC3::MemoryManager::deleteData(), exprValue(), FatalAssert, CVC3::TheoremValue::getMM(), IF_DEBUG, CVC3::int2string(), and thm().

---

Member Function Documentation

void CVC3::Theorem::recursivePrint

(

int &

i

)

const [private]

Definition at line 515 of file theorem.cpp.

References CVC3::Assumptions::begin(), CVC3::Assumptions::end(), std::endl(), getAssumptionsRef(), getCachedValue(), getExpr(), getScope(), isAssump(), isSubst(), and setCachedValue().

void CVC3::Theorem::getAssumptionsRec

(

std::set< Expr > &

assumptions

)

const [private]

Definition at line 258 of file theorem.cpp.

References CVC3::Assumptions::begin(), CVC3::Assumptions::end(), getAssumptionsRef(), getExpr(), isAssump(), isFlagged(), isRefl(), and setFlag().

Referenced by getLeafAssumptions().

void CVC3::Theorem::getAssumptionsAndCongRec	(	std::set< Expr > &	assumptions,
		std::vector< Expr > &	congruences
	)			const [private]

Definition at line 319 of file theorem.cpp.

References CVC3::Assumptions::begin(), CVC3::Assumptions::end(), getAssumptionsAndCongRec(), getAssumptionsRef(), getExpr(), getLHS(), getRHS(), isAssump(), CVC3::Expr::isAtomic(), CVC3::Expr::isAtomicFormula(), isFlagged(), isRefl(), isRewrite(), isSubst(), CVC3::Expr::isTerm(), CVC3::OR, setFlag(), CVC3::Assumptions::size(), and thm().

Referenced by getAssumptionsAndCong(), and getAssumptionsAndCongRec().

void CVC3::Theorem::GetSatAssumptionsRec

(

std::vector< Theorem > &

assumptions

)

const [private]

Definition at line 287 of file theorem.cpp.

References CVC3::Assumptions::begin(), DebugAssert, CVC3::Assumptions::end(), getAssumptionsRef(), getExpr(), CVC3::Expr::isAbsLiteral(), isAssump(), isFlagged(), CVC3::Expr::isNot(), isRefl(), CVC3::Expr::isRegisteredAtom(), and setFlag().

ExprValue* CVC3::Theorem::exprValue

(

)

const [inline, private]

Definition at line 132 of file theorem.h.

Referenced by clearAllFlags(), getCachedValue(), getExpandFlag(), getExpr(), getLitFlag(), getProof(), isFlagged(), operator=(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), Theorem(), withAssumptions(), withProof(), and ~Theorem().

TheoremValue* CVC3::Theorem::thm

(

)

const [inline, private]

Definition at line 133 of file theorem.h.

Referenced by clearAllFlags(), getAssumptionsAndCongRec(), getAssumptionsRef(), getCachedValue(), getExpandFlag(), getExpr(), getLHS(), getLitFlag(), getProof(), getQuantLevel(), getQuantLevelDebug(), getRHS(), getScope(), isAssump(), isFlagged(), isRewrite(), isSubst(), operator=(), print(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), setSubst(), Theorem(), withAssumptions(), withProof(), and ~Theorem().

void CVC3::Theorem::printDebug

(

)

const [inline]

Definition at line 140 of file theorem.h.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theorem3::printDebug(), and CVC3::SearchEngineFast::traceConflict().

Theorem & CVC3::Theorem::operator=

(

const Theorem &

th

)

Definition at line 91 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, CVC3::ExprValue::decRefcount(), CVC3::MemoryManager::deleteData(), exprValue(), CVC3::TheoremValue::getMM(), CVC3::ExprValue::incRefcount(), and thm().

bool CVC3::Theorem::withProof

(

)

const

Definition at line 213 of file theorem.cpp.

References CVC3::ExprValue::d_em, CVC3::TheoremValue::d_tm, exprValue(), CVC3::ExprManager::getTM(), isRefl(), thm(), and CVC3::TheoremManager::withProof().

Referenced by getProof(), print(), Theorem(), and CVC3::Theorem3::withProof().

bool CVC3::Theorem::withAssumptions

(

)

const

Definition at line 218 of file theorem.cpp.

References CVC3::ExprValue::d_em, CVC3::TheoremValue::d_tm, exprValue(), CVC3::ExprManager::getTM(), isRefl(), thm(), and CVC3::TheoremManager::withAssumptions().

Referenced by print(), and CVC3::Theorem3::withAssumptions().

bool CVC3::Theorem::isNull

(

)

const [inline]

Definition at line 164 of file theorem.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryCore::buildModel(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::checkSat(), clearAllFlags(), CVC3::compare(), CVC3::TheoryArithOld::computeTermBounds(), MiniSat::Derivation::createProof(), CVC3::TheoryArith3::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), generateSatProof(), getAssumptionsAndCong(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRef(), CVC3::VCL::getAssumptionsUsed(), CVC3::SearchImplBase::getAssumptionsUsed(), getCachedValue(), CVC3::SearchSat::getCounterExample(), CVC3::SearchImplBase::getCounterExample(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), getExpandFlag(), getExpr(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), getLeafAssumptions(), getLHS(), getLitFlag(), getProof(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::getProof(), CVC3::VCL::getProofTCC(), getQuantLevel(), getQuantLevelDebug(), getRHS(), getScope(), CVC3::VCL::getTCC(), CVC3::Expr::hasFind(), CVC3::Expr::hasRep(), CVC3::Expr::hasSig(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), isAssump(), CVC3::TheoryArithOld::isConstrained(), isFlagged(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArithNew::isInteger(), CVC3::TheoryArith3::isInteger(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArith3::isIntegerDerive(), SAT::SatProofNode::isLeaf(), CVC3::Theorem3::isNull(), isRewrite(), isSubst(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::isUnsat(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::multMatchChild(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::operator<<(), print(), printSatProof(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::Circuit::propagate(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::SearchImplBase::replaceITE(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::Theory::rewriteCC(), SAT::SatProofNode::SatProofNode(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), setSubst(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::simplifyOp(), TheoremEq(), TheoremEq(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and CVC3::Theory::updateCC().

bool CVC3::Theorem::isRewrite

(

)

const

Definition at line 223 of file theorem.cpp.

References DebugAssert, isNull(), isRefl(), CVC3::TheoremValue::isRewrite(), and thm().

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assignValue(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::compare(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchImplBase::findInCNFCache(), CVC3::BitvectorTheoremProducer::generalIneqn(), getAssumptionsAndCongRec(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::Theorem3::isRewrite(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::operator<(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryCore::processUpdates(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArray::renameExpr(), CVC3::SearchImplBase::replaceITE(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryDatatype::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), and CVC3::CommonTheoremProducer::transitivityRule().

bool CVC3::Theorem::isAssump

(

)

const

Definition at line 394 of file theorem.cpp.

References DebugAssert, CVC3::TheoremValue::isAssump(), isNull(), isRefl(), and thm().

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryQuant::findInstAssumptions(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), GetSatAssumptionsRec(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::Theorem3::isAssump(), CVC3::SearchEngineFast::newIntAssumption(), print(), and recursivePrint().

bool CVC3::Theorem::isRefl

(

)

const [inline]

Definition at line 171 of file theorem.h.

Referenced by CVC3::TheoryArray::checkSat(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), clearAllFlags(), CVC3::Theory::find(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Theory::findReduce(), getAssumptionsAndCong(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), getAssumptionsRef(), getCachedValue(), getExpandFlag(), getExpr(), getLeafAssumptions(), getLHS(), getLitFlag(), getProof(), getQuantLevel(), getQuantLevelDebug(), getRHS(), GetSatAssumptions(), GetSatAssumptionsRec(), getScope(), isAssump(), isFlagged(), isRewrite(), isSubst(), CVC3::ExprTransform::newPPrec(), CVC3::ExprTransform::preprocess(), print(), CVC3::TheoryBitvector::pushNegationRec(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), setSubst(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::TheoryArray::update(), withAssumptions(), and withProof().

Expr CVC3::Theorem::getExpr

(

)

const

Definition at line 229 of file theorem.cpp.

References DebugAssert, CVC3::Expr::eqExpr(), exprValue(), CVC3::TheoremValue::getExpr(), CVC3::Expr::iffExpr(), isNull(), isRefl(), CVC3::Expr::isTerm(), and thm().

Referenced by SAT::CNF_Manager::addAssumption(), CVC3::SearchImplBase::addCNFFact(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryCore::addFact(), CVC3::SearchImplBase::addFact(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::SearchSat::addLemma(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::SearchImplBase::addToCNFCache(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::CommonTheoremProducer::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryCore::checkEquation(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryCore::checkSolved(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::Circuit::Circuit(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ClauseValue::ClauseValue(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::compare(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::enqueueFact(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::SearchImplBase::findInCNFCache(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::SearchEngineFast::fixConflict(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::SearchSat::getAssumptions(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), CVC3::Theorem3::getExpr(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), CVC3::SearchSat::getImpliedLiteral(), CVC3::TheoryArithNew::getLowerBoundExplanation(), GetSatAssumptionsRec(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::VCL::getTCC(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implMP(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), isAbsLiteral(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArith3::isStale(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::operator<(), CVC3::operator<<(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::pivotRule(), pprintx(), pprintxnodag(), CVC3::ExprTransform::preprocess(), print(), printx(), printxnodag(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArith3::processBuffer(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), processNode(), CVC3::TheoryArithOld::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::DecisionEngine::pushDecision(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryQuant::recInstantiate(), CVC3::SearchEngineFast::recordFact(), recursivePrint(), CVC3::TheoryArithOld::registerAtom(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryCore::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBV(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryQuant::sendInstNew(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::setInconsistent(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), CVC3::VariableValue::setValue(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::SearchImplBase::simplify(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::CompleteInstPreProcessor::simplifyQuant(), CVC3::CommonTheoremProducer::skolemize(), CVC3::TheoryCore::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArray::solve(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), TheoremEq(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::SearchEngineFast::traceConflict(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExpr(), CVC3::VCL::tryModelGeneration(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::SearchEngineFast::unitPropagation(), CVC3::QuantTheoremProducer::universalInst(), CVC3::TheoryQuant::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), and CVC3::CommonTheoremProducer::varIntroSkolem().

const Expr & CVC3::Theorem::getLHS

(

)

const

Definition at line 239 of file theorem.cpp.

References d_expr, DebugAssert, CVC3::TheoremValue::getLHS(), isNull(), isRefl(), and thm().

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assignValue(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::TheoryCore::buildModel(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::compare(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::Theory::find(), CVC3::SearchImplBase::findInCNFCache(), CVC3::Theory::findRef(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::BitvectorTheoremProducer::generalIneqn(), getAssumptionsAndCongRec(), CVC3::Theorem3::getLHS(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryCore::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryDatatype::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryQuant::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::Theory::updateHelper(), and CVC3::TheoryBitvector::updateSubterms().

const Expr & CVC3::Theorem::getRHS

(

)

const

Definition at line 245 of file theorem.cpp.

References d_expr, DebugAssert, CVC3::TheoremValue::getRHS(), isNull(), isRefl(), and thm().

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::addToBuffer(), CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractSXRule(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::callTheoryPreprocess(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer3::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArith::canonThm(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::compare(), CVC3::TheoryBitvector::comparebv(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::Theory::computeTCC(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::TheoryQuant::debug(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::TheoryArith3::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::Theory::find(), CVC3::Theory::findExpr(), CVC3::Theory::findReduced(), CVC3::Theory::findRef(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::BitvectorTheoremProducer::generalIneqn(), getAssumptionsAndCongRec(), CVC3::Theorem3::getRHS(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArith3::isStale(), CVC3::Theory::leavesAreSimp(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::multMatchChild(), CVC3::ExprTransform::newPP(), CVC3::ExprTransform::newPPrec(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::operator<(), CVC3::ExprTransform::preprocess(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryArith::recursiveCanonSimpCheck(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryArray::renameExpr(), CVC3::SearchImplBase::replaceITE(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryUF::rewrite(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::TheoryArith::rewriteToDiff(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryRecords::setup(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::VCL::simplify(), CVC3::TheoryCore::simplify(), CVC3::Theory::simplifyExpr(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::VCL::simplifyThm(), CVC3::TheoryDatatype::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::SearchEngineFast::split(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::TheoryQuant::synNewInst(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryQuant::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::Theory::updateCC(), CVC3::Theory::updateHelper(), and CVC3::TheoryBitvector::updateSubterms().

void CVC3::Theorem::GetSatAssumptions

(

std::vector< Theorem > &

assumptions

)

const

Definition at line 308 of file theorem.cpp.

References CVC3::Assumptions::begin(), DebugAssert, CVC3::Assumptions::end(), getAssumptionsRef(), isFlagged(), isRefl(), and setFlag().

Referenced by CVC3::CNF_TheoremProducer::getSmartClauses().

void CVC3::Theorem::getLeafAssumptions	(	std::vector< Expr > &	assumptions,
		bool	negate = false
	)			const

Definition at line 273 of file theorem.cpp.

References clearAllFlags(), getAssumptionsRec(), isNull(), and isRefl().

Referenced by CVC3::TheoryCore::buildModel(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::VCL::getAssumptionsUsed(), CVC3::SearchEngine::getConcreteModel(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryCore::refineCounterExample(), and CVC3::VCL::tryModelGeneration().

void CVC3::Theorem::getAssumptionsAndCong	(	std::vector< Expr > &	assumptions,
		std::vector< Expr > &	congruences,
		bool	negate = false
	)			const

Definition at line 369 of file theorem.cpp.

References clearAllFlags(), getAssumptionsAndCongRec(), isNull(), and isRefl().

const Assumptions & CVC3::Theorem::getAssumptionsRef

(

)

const

Definition at line 384 of file theorem.cpp.

References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::TheoremValue::getAssumptionsRef(), isNull(), isRefl(), and thm().

Referenced by CVC3::Assumptions::add(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::Assumptions::Assumptions(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), CVC3::Theorem3::getAssumptionsRef(), CVC3::VCL::getAssumptionsTCC(), CVC3::SearchImplBase::getAssumptionsUsed(), GetSatAssumptions(), GetSatAssumptionsRec(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::implIntro(), CVC3::VCL::inconsistent(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), print(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), recursivePrint(), CVC3::UFTheoremProducer::relToClosure(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::SearchEngineFast::traceConflict(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::SearchEngineTheoremProducer::verifyConflict().

Proof CVC3::Theorem::getProof

(

)

const

Definition at line 401 of file theorem.cpp.

References DebugAssert, exprValue(), CVC3::TheoremValue::getProof(), isNull(), isRefl(), CVC3::PF_APPLY, thm(), and withProof().

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CommonTheoremProducer::andElim(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), generateSatProof(), CVC3::Theorem3::getProof(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::getProof(), CVC3::VCL::getProofTCC(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), print(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::SearchEngineTheoremProducer::unitProp(), and CVC3::QuantTheoremProducer::universalInst().

int CVC3::Theorem::getScope

(

)

const

Definition at line 485 of file theorem.cpp.

References DebugAssert, CVC3::TheoremValue::getScope(), isNull(), isRefl(), and thm().

Referenced by CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theorem3::getScope(), print(), CVC3::SearchEngineFast::recordFact(), recursivePrint(), CVC3::Literal::setValue(), CVC3::Variable::setValue(), and CVC3::SearchEngineFast::traceConflict().

unsigned CVC3::Theorem::getQuantLevel

(

)

const

Return quantification level for this theorem.

Definition at line 490 of file theorem.cpp.

References DebugAssert, CVC3::TheoremValue::getQuantLevel(), isNull(), isRefl(), thm(), and CVC3::TRACE.

Referenced by CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryCore::setupTerm(), and CVC3::QuantTheoremProducer::universalInst().

unsigned CVC3::Theorem::getQuantLevelDebug

(

)

const

Definition at line 496 of file theorem.cpp.

References DebugAssert, CVC3::TheoremValue::getQuantLevelDebug(), isNull(), isRefl(), thm(), and CVC3::TRACE.

void CVC3::Theorem::setQuantLevel

(

unsigned

level

)

Set the quantification level for this theorem.

Definition at line 503 of file theorem.cpp.

References DebugAssert, isNull(), isRefl(), CVC3::TheoremValue::setQuantLevel(), and thm().

Referenced by CVC3::SearchSat::assertLit(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::SearchImplBase::newIntAssumption(), CVC3::QuantTheoremProducer::partialUniversalInst(), and CVC3::QuantTheoremProducer::universalInst().

size_t CVC3::Theorem::hash

(

)

const

Definition at line 510 of file theorem.cpp.

References d_thm.

Referenced by Hash::hash< CVC3::Theorem >::operator()().

std::string CVC3::Theorem::toString

(

)

const [inline]

Definition at line 404 of file theorem.h.

Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::CommonTheoremProducer::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::ClauseValue::ClauseValue(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::VCL::getAssumptionsRec(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implMP(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), print(), CVC3::Expr::printAST(), processNode(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::TheoryArithNew::propagateTheory(), CVC3::ExprTransform::pushNegationRec(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryArray::renameExpr(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::setupTerm(), CVC3::VariableValue::setValue(), Theorem(), and CVC3::SearchEngineTheoremProducer::unitProp().

void CVC3::Theorem::printx

(

)

const

Definition at line 206 of file theorem.cpp.

References getExpr(), and CVC3::Expr::print().

Referenced by CVC3::Theorem3::printx().

void CVC3::Theorem::printxnodag

(

)

const

Definition at line 207 of file theorem.cpp.

References getExpr(), and CVC3::Expr::printnodag().

void CVC3::Theorem::pprintx

(

)

const

Definition at line 208 of file theorem.cpp.

References getExpr(), and CVC3::Expr::pprint().

void CVC3::Theorem::pprintxnodag

(

)

const

Definition at line 209 of file theorem.cpp.

References getExpr(), and CVC3::Expr::pprintnodag().

void CVC3::Theorem::print

(

)

const

Definition at line 210 of file theorem.cpp.

References std::endl(), and toString().

Referenced by CVC3::Theorem3::print().

bool CVC3::Theorem::isFlagged

(

)

const

Check if the flag attribute is set.

Definition at line 415 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), CVC3::TheoremValue::isFlagged(), CVC3::TheoremManager::isFlagged(), isNull(), isRefl(), and thm().

Referenced by CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryQuant::findInstAssumptions(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), GetSatAssumptions(), GetSatAssumptionsRec(), and processNode().

void CVC3::Theorem::clearAllFlags

(

)

const

Clear the flag attribute in all the theorems.

Definition at line 421 of file theorem.cpp.

References CVC3::TheoremValue::clearAllFlags(), CVC3::TheoremManager::clearAllFlags(), CVC3::ExprValue::d_em, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), getAssumptionsAndCong(), getLeafAssumptions(), CVC3::CNF_TheoremProducer::getSmartClauses(), and CVC3::SearchEngineFast::traceConflict().

void CVC3::Theorem::setFlag

(

)

const

Set the flag attribute.

Definition at line 428 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setFlag(), CVC3::TheoremManager::setFlag(), and thm().

Referenced by CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), GetSatAssumptions(), GetSatAssumptionsRec(), and processNode().

void CVC3::Theorem::setSubst

(

)

const

Set flag stating that theorem is an instance of substitution.

Definition at line 446 of file theorem.cpp.

References DebugAssert, isNull(), isRefl(), CVC3::TheoremValue::setSubst(), and thm().

Referenced by CVC3::CommonTheoremProducer::substitutivityRule().

bool CVC3::Theorem::isSubst

(

)

const

Is theorem an instance of substitution.

Definition at line 451 of file theorem.cpp.

References DebugAssert, isNull(), isRefl(), CVC3::TheoremValue::isSubst(), and thm().

Referenced by getAssumptionsAndCongRec(), and recursivePrint().

void CVC3::Theorem::setExpandFlag

(

bool

val

)

const

Set the "expand" attribute.

Definition at line 457 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setExpandFlag(), CVC3::TheoremManager::setExpandFlag(), and thm().

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

bool CVC3::Theorem::getExpandFlag

(

)

const

Check the "expand" attribute.

Definition at line 463 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::TheoremValue::getExpandFlag(), CVC3::TheoremManager::getExpandFlag(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().

Referenced by processNode().

void CVC3::Theorem::setLitFlag

(

bool

val

)

const

Set the "literal" attribute.

The expression of this theorem will be added as a conflict clause literal

Definition at line 469 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setLitFlag(), CVC3::TheoremManager::setLitFlag(), and thm().

bool CVC3::Theorem::getLitFlag

(

)

const

Check the "literal" attribute.

The expression of this theorem will be added as a conflict clause literal

Definition at line 475 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::TheoremValue::getLitFlag(), CVC3::TheoremManager::getLitFlag(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().

Referenced by processNode().

bool CVC3::Theorem::isAbsLiteral

(

)

const

Check if the theorem is a literal.

Definition at line 481 of file theorem.cpp.

References getExpr(), and CVC3::Expr::isAbsLiteral().

Referenced by CVC3::SearchImplBase::addCNFFact(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::enqueueFact(), CVC3::Theorem3::isAbsLiteral(), processNode(), and CVC3::SearchEngineFast::unitPropagation().

bool CVC3::Theorem::refutes

(

const Expr &

e

)

const [inline]

Check if the flag attribute is set.

Definition at line 252 of file theorem.h.

References CVC3::Expr::isNot().

Referenced by CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), and CVC3::SearchEngineTheoremProducer::propIterThen().

bool CVC3::Theorem::proves

(

const Expr &

e

)

const [inline]

Check if the flag attribute is set.

Definition at line 259 of file theorem.h.

Referenced by CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), and CVC3::SearchEngineTheoremProducer::propIterThen().

bool CVC3::Theorem::matches

(

const Expr &

e

)

const [inline]

Check if the flag attribute is set.

Definition at line 264 of file theorem.h.

void CVC3::Theorem::setCachedValue

(

int

value

)

const

Check if the flag attribute is set.

Definition at line 434 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setCachedValue(), CVC3::TheoremManager::setCachedValue(), and thm().

Referenced by processNode(), recursivePrint(), and CVC3::SearchEngineFast::traceConflict().

int CVC3::Theorem::getCachedValue

(

)

const

Check if the flag attribute is set.

Definition at line 440 of file theorem.cpp.

References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::TheoremValue::getCachedValue(), CVC3::TheoremManager::getCachedValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().

Referenced by processNode(), and recursivePrint().

ostream & CVC3::Theorem::print	(	std::ostream &	os,
		const std::string &	name
	)			const

Printing a theorem to a stream, calling it "name".

Definition at line 579 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, getAssumptionsRef(), CVC3::Expr::getEM(), getExpr(), getProof(), getScope(), CVC3::ExprManager::incIndent(), CVC3::ExprManager::indent(), CVC3::ExprManager::isActive(), isAssump(), isNull(), isRefl(), thm(), withAssumptions(), and withProof().

static bool CVC3::Theorem::TheoremEq	(	const Theorem &	t1,
		const Theorem &	t2
	)			[inline, static]

Definition at line 281 of file theorem.h.

References DebugAssert, and isNull().

Referenced by CVC3::Assumptions::Assumptions().

---

Friends And Related Function Documentation

friend class TheoremProducer [friend]

Definition at line 80 of file theorem.h.

friend class Theorem3 [friend]

Definition at line 82 of file theorem.h.

friend class RegTheoremValue [friend]

Definition at line 84 of file theorem.h.

Referenced by Theorem().

friend class RWTheoremValue [friend]

Definition at line 85 of file theorem.h.

Referenced by Theorem().

int compare	(	const Theorem &	t1,
		const Theorem &	t2
	)			[friend]

Compare Theorems by their expressions. Return -1, 0, or 1.

This is an arbitrary total ordering on Theorems. For simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to be smaller than other theorems.

Definition at line 45 of file theorem.cpp.

int compare	(	const Theorem &	t1,
		const Expr &	e2
	)			[friend]

Compare a Theorem with an Expr (as if Expr is a Theorem).

Definition at line 65 of file theorem.cpp.

int compareByPtr	(	const Theorem &	t1,
		const Theorem &	t2
	)			[friend]

Compare Theorems by TheoremValue pointers. Return -1, 0, or 1.

Definition at line 83 of file theorem.cpp.

bool operator==	(	const Theorem &	t1,
		const Theorem &	t2
	)			[friend]

Equality is w.r.t. compare().

Definition at line 102 of file theorem.h.

bool operator!=	(	const Theorem &	t1,
		const Theorem &	t2
	)			[friend]

Disequality is w.r.t. compare().

Definition at line 105 of file theorem.h.

std::ostream& operator<<	(	std::ostream &	os,
		const Theorem &	t
	)			[friend]

Definition at line 277 of file theorem.h.

---

Member Data Documentation

intptr_t CVC3::Theorem::d_thm

Definition at line 91 of file theorem.h.

Referenced by CVC3::compare(), CVC3::compareByPtr(), hash(), operator=(), Theorem(), and ~Theorem().

ExprValue* CVC3::Theorem::d_expr

Definition at line 92 of file theorem.h.

Referenced by getCachedValue(), getExpandFlag(), getLHS(), getLitFlag(), getRHS(), isFlagged(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), and Theorem().

union { ... } [private]

---

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

• theorem.h
• theorem.cpp