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 getLeafAssumptions (std::vector< Expr > &assumptions, bool negate=false) const
• const Assumptions & getAssumptionsRef () const
• Proof getProof () const
• int getScope () const
• unsigned getQuantLevel () const

  Return quantification level for this theorem.
  

• 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 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
• 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 77 of file theorem.h.

---

Constructor & Destructor Documentation

CVC3::Theorem::Theorem

(

TheoremValue *

thm

)

[inline, private]

Constructor only used by TheoremValue for assumptions.

Definition at line 110 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 131 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, CVC3::TheoremManager::getRWMM(), CVC3::Proof::isNull(), RegTheoremValue, RWTheoremValue, thm(), 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 146 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, CVC3::TheoremManager::getRWMM(), 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 188 of file theorem.cpp.

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

CVC3::Theorem::Theorem

(

)

[inline]

Definition at line 149 of file theorem.h.

CVC3::Theorem::Theorem

(

const Theorem &

th

)

Definition at line 176 of file theorem.cpp.

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

CVC3::Theorem::~Theorem

(

)

Definition at line 194 of file theorem.cpp.

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

---

Member Function Documentation

void CVC3::Theorem::recursivePrint

(

int &

i

)

const [private]

Definition at line 405 of file theorem.cpp.

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

void CVC3::Theorem::getAssumptionsRec

(

std::set< Expr > &

assumptions

)

const [private]

Definition at line 265 of file theorem.cpp.

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

Referenced by getLeafAssumptions().

ExprValue* CVC3::Theorem::exprValue

(

)

const [inline, private]

Definition at line 130 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 131 of file theorem.h.

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

void CVC3::Theorem::printDebug

(

)

const [inline]

Definition at line 138 of file theorem.h.

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

Theorem & CVC3::Theorem::operator=

(

const Theorem &

th

)

Definition at line 90 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(), isNull(), isRefl(), thm(), and toString().

bool CVC3::Theorem::withProof

(

)

const

Definition at line 220 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 225 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 checkAssumpDebug(), print(), and CVC3::Theorem3::withAssumptions().

bool CVC3::Theorem::isNull

(

)

const [inline]

Definition at line 162 of file theorem.h.

Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryCore::buildModel(), clearAllFlags(), CVC3::compare(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRef(), CVC3::VCL::getAssumptionsUsed(), CVC3::SearchImplBase::getAssumptionsUsed(), getCachedValue(), CVC3::SearchImplBase::getCounterExample(), getExpandFlag(), getExpr(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), getLeafAssumptions(), getLHS(), getLitFlag(), getProof(), CVC3::SearchImplBase::getProof(), CVC3::VCL::getProofTCC(), getQuantLevel(), CVC3::TheoryCore::getQuantLevelForTerm(), getRHS(), getScope(), CVC3::VCL::getTCC(), isAssump(), isFlagged(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArithNew::isInteger(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::Theorem3::isNull(), isRewrite(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::operator<<(), operator=(), print(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::projectInequalities(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::Theory::rewriteCC(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::simplifyOp(), TheoremEq(), TheoremEq(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and CVC3::Theory::updateCC().

bool CVC3::Theorem::isRewrite

(

)

const

Definition at line 230 of file theorem.cpp.

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

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

bool CVC3::Theorem::isAssump

(

)

const

Definition at line 304 of file theorem.cpp.

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

Referenced by checkAssump(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), CVC3::Theorem3::isAssump(), CVC3::SearchEngineFast::newIntAssumption(), print(), and recursivePrint().

bool CVC3::Theorem::isRefl

(

)

const [inline]

Definition at line 169 of file theorem.h.

Referenced by CVC3::TheoryCore::assertFactCore(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), clearAllFlags(), CVC3::Theory::find(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), getAssumptionsRef(), getCachedValue(), getExpandFlag(), getExpr(), getLeafAssumptions(), getLHS(), getLitFlag(), getProof(), getQuantLevel(), getRHS(), getScope(), isAssump(), isFlagged(), isRewrite(), operator=(), print(), CVC3::TheoryBitvector::pushNegationRec(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), withAssumptions(), and withProof().

Expr CVC3::Theorem::getExpr

(

)

const

Definition at line 236 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 CVC3::SearchImplBase::addCNFFact(), CVC3::TheoryCore::addFact(), CVC3::SearchImplBase::addFact(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::SearchSat::addLemma(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::SearchImplBase::addToCNFCache(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::CommonTheoremProducer::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::TheoryArithOld::checkAssertEqInvariant(), checkAssump(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::Circuit::Circuit(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ClauseValue::ClauseValue(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::compare(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), SAT::CNF_Manager::convertLemma(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::SearchEngineFast::enqueueFact(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::SearchImplBase::findInCNFCache(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::SearchSat::getAssumptions(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), CVC3::Theorem3::getExpr(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), CVC3::SearchSat::getImpliedLiteral(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::VCL::getTCC(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::ArithTheoremProducerOld::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(), isAbsLiteral(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::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::TheoryCore::processEquality(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), processNode(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithOld::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::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryQuant::recInstantiate(), CVC3::SearchEngineFast::recordFact(), recursivePrint(), 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::TheoryCore::setFindLiteral(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), CVC3::VariableValue::setValue(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::SearchImplBase::simplify(), CVC3::CommonTheoremProducer::skolemize(), CVC3::TheoryCore::solve(), CVC3::TheoryArray::solve(), CVC3::SearchEngineFast::split(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), TheoremEq(), CVC3::SearchEngineFast::traceConflict(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExpr(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::QuantTheoremProducer::universalInst(), CVC3::TheoryBitvector::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and CVC3::CommonTheoremProducer::varIntroSkolem().

const Expr & CVC3::Theorem::getLHS

(

)

const

Definition at line 246 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::TheoryArithOld::assertFact(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::compare(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryArray::computeModel(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::Theory::find(), CVC3::SearchImplBase::findInCNFCache(), CVC3::Theory::findRef(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::Theorem3::getLHS(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::Expr::setFind(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::TheoryCore::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::TheoryDatatype::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and CVC3::Theory::updateHelper().

const Expr & CVC3::Theorem::getRHS

(

)

const

Definition at line 252 of file theorem.cpp.

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

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArithOld::assertFact(), 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::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith::canonThm(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::compare(), CVC3::TheoryBitvector::comparebv(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::Theory::computeTCC(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::Theory::find(), CVC3::Theory::findExpr(), CVC3::Theory::findReduced(), CVC3::Theory::findRef(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::Theorem3::getRHS(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::Theory::leavesAreSimp(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::ExprTransform::preprocess(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryArray::renameExpr(), CVC3::SearchImplBase::replaceITE(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryUF::rewrite(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::TheoryCore::rewriteN(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::TheoryArith::rewriteToDiff(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryRecords::setup(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::VCL::simplify(), CVC3::TheoryCore::simplify(), CVC3::Theory::simplifyExpr(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::VCL::simplifyThm(), CVC3::TheoryDatatype::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::SearchEngineFast::split(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::Theory::updateCC(), and CVC3::Theory::updateHelper().

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

Definition at line 280 of file theorem.cpp.

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

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

const Assumptions & CVC3::Theorem::getAssumptionsRef

(

)

const

Definition at line 294 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::CommonTheoremProducer::andElim(), CVC3::Assumptions::Assumptions(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::caseSplit(), checkAssump(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), CVC3::Theorem3::getAssumptionsRef(), CVC3::VCL::getAssumptionsTCC(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), print(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), recursivePrint(), CVC3::UFTheoremProducer::relToClosure(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::SearchEngineFast::traceConflict(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::SearchEngineTheoremProducer::verifyConflict().

Proof CVC3::Theorem::getProof

(

)

const

Definition at line 311 of file theorem.cpp.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CommonTheoremProducer::andElim(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::caseSplit(), 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::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::Theorem3::getProof(), CVC3::SearchImplBase::getProof(), CVC3::VCL::getProofTCC(), CVC3::ArithTheoremProducerOld::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::implMP(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::SearchEngineTheoremProducer::negIntro(), 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::CommonTheoremProducer::queryTCC(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::SearchEngineTheoremProducer::unitProp(), and CVC3::QuantTheoremProducer::universalInst().

int CVC3::Theorem::getScope

(

)

const

Definition at line 384 of file theorem.cpp.

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

Referenced by CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), 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 389 of file theorem.cpp.

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

Referenced by CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::CNF_TheoremProducer::learnedClause(), and CVC3::TheoryCore::setupTerm().

void CVC3::Theorem::setQuantLevel

(

unsigned

level

)

Set the quantification level for this theorem.

Definition at line 394 of file theorem.cpp.

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

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

size_t CVC3::Theorem::hash

(

)

const

Definition at line 400 of file theorem.cpp.

References d_thm.

Referenced by CVC3::ExprTheorem::computeHash(), and Hash::hash< CVC3::Theorem >::operator()().

std::string CVC3::Theorem::toString

(

)

const [inline]

Definition at line 387 of file theorem.h.

Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::CommonTheoremProducer::andElim(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), checkAssump(), CVC3::ClauseValue::ClauseValue(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducerOld::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::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), operator=(), print(), CVC3::Expr::printAST(), processNode(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::ExprTransform::pushNegationRec(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryArray::renameExpr(), CVC3::TheoryCore::rewriteCore(), CVC3::VariableValue::setValue(), Theorem(), and CVC3::SearchEngineTheoremProducer::unitProp().

void CVC3::Theorem::printx

(

)

const

Definition at line 213 of file theorem.cpp.

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

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

void CVC3::Theorem::printxnodag

(

)

const

Definition at line 214 of file theorem.cpp.

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

void CVC3::Theorem::pprintx

(

)

const

Definition at line 215 of file theorem.cpp.

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

void CVC3::Theorem::pprintxnodag

(

)

const

Definition at line 216 of file theorem.cpp.

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

void CVC3::Theorem::print

(

)

const

Definition at line 217 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 325 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(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), and processNode().

void CVC3::Theorem::clearAllFlags

(

)

const

Clear the flag attribute in all the theorems.

Definition at line 331 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(), checkAssumpDebug(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), getLeafAssumptions(), and CVC3::SearchEngineFast::traceConflict().

void CVC3::Theorem::setFlag

(

)

const

Set the flag attribute.

Definition at line 338 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(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), and processNode().

void CVC3::Theorem::setExpandFlag

(

bool

val

)

const

Set the "expand" attribute.

Definition at line 356 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 362 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 368 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 374 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 380 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(), and processNode().

bool CVC3::Theorem::refutes

(

const Expr &

e

)

const [inline]

Check if the flag attribute is set.

Definition at line 235 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 242 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 247 of file theorem.h.

void CVC3::Theorem::setCachedValue

(

int

value

)

const

Check if the flag attribute is set.

Definition at line 344 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(), and CVC3::SearchEngineFast::traceConflict().

int CVC3::Theorem::getCachedValue

(

)

const

Check if the flag attribute is set.

Definition at line 350 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 466 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 264 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 81 of file theorem.h.

friend class Theorem3 [friend]

Definition at line 83 of file theorem.h.

friend class RegTheoremValue [friend]

Definition at line 85 of file theorem.h.

Referenced by Theorem().

friend class RWTheoremValue [friend]

Definition at line 86 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 103 of file theorem.h.

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

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

Definition at line 106 of file theorem.h.

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

Definition at line 260 of file theorem.h.

---

Member Data Documentation

intptr_t CVC3::Theorem::d_thm [private]

Definition at line 92 of file theorem.h.

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

ExprValue* CVC3::Theorem::d_expr [private]

Definition at line 93 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

---