CVCL::Theorem Class Reference

#include <theorem.h>

Collaboration diagram for CVCL::Theorem:

[legend]List of all members.

Public Member Functions

• void printDebug () const
• Theorem ()
• Theorem (const Theorem &th)
• Theorem & operator= (const Theorem &th)
• virtual ~Theorem ()
• bool isNull () const
• bool isRewrite () const
• bool isAssump () const
• const Expr & getExpr () const
• const Expr & getLHS () const
• const Expr & getRHS () const
• const Assumptions & getAssumptions () const
• void getLeafAssumptions (std::vector< Expr > &assumptions, bool negate=false) const
• const Assumptions & getAssumptionsRef () const
• Assumptions getAssumptionsCopy () const
• const Proof & getProof () const
• int getScope () const
• bool withProof () const
• bool withAssumptions () const
• std::string toString () const
• void printx () 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.
  

Private Member Functions

• 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 (TheoremManager *tm, const Expr &e, const Proof &pf)

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

• void recursivePrint (int &i) const
• void getAssumptionsRec (std::set< Expr > &assumptions) const

Private Attributes

• TheoremValue * d_thm

Friends

• class TheoremProducer
• class Theorem3
• 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 84 of file theorem.h.

---

Constructor & Destructor Documentation

CVCL::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 128 of file theorem.cpp. References CVCL::TheoremValue::d_refcount, d_thm, CVCL::TheoremManager::getMM(), CVCL::TheoremManager::getRWMM(), CVCL::Expr::isEq(), CVCL::Expr::isIff(), CVCL::Proof::isNull(), toString(), CVCL::TRACE, and withProof().

CVCL::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 141 of file theorem.cpp. References CVCL::TheoremValue::d_refcount, d_thm, CVCL::TheoremManager::getRWMM(), CVCL::Expr::getSimpFrom(), CVCL::Expr::hasLastIndex(), CVCL::Expr::hasSimpFrom(), CVCL::Proof::isNull(), toString(), CVCL::TRACE, and withProof().

CVCL::Theorem::Theorem (  TheoremManager *  tm, const Expr &  e, const Proof &  pf )  [private]

Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi. Definition at line 169 of file theorem.cpp. References CVCL::TheoremValue::d_refcount, d_thm, CVCL::TheoremManager::getReflMM(), CVCL::Proof::isNull(), toString(), CVCL::TRACE, and withProof().

CVCL::Theorem::Theorem (   )  [inline]

Definition at line 141 of file theorem.h.

CVCL::Theorem::Theorem (  const Theorem &  th  )

Definition at line 179 of file theorem.cpp. References CVCL::TheoremValue::d_refcount, d_thm, CVCL::int2string(), isNull(), and CVCL::TRACE.

CVCL::Theorem::~Theorem (   )  [virtual]

Definition at line 190 of file theorem.cpp. References CVCL::TheoremValue::d_refcount, d_thm, CVCL::MemoryManager::deleteData(), CVCL::TheoremValue::getMM(), CVCL::int2string(), isNull(), and CVCL::TRACE.

---

Member Function Documentation

void CVCL::Theorem::recursivePrint (  int &  i  )  const [private]

Definition at line 372 of file theorem.cpp. References CVCL::Assumptions::end(), std::endl(), getAssumptions(), getCachedValue(), getExpr(), getScope(), and isAssump(). Referenced by printDebug().

void CVCL::Theorem::getAssumptionsRec (  std::set< Expr > &  assumptions  )  const [private]

void CVCL::Theorem::printDebug (   )  const [inline]

Definition at line 130 of file theorem.h. References clearAllFlags(), recursivePrint(), setCachedValue(), and setFlag(). Referenced by CVCL::SearchEngineFast::analyzeUIPs(), checkAssump(), CVCL::SearchEngineFast::fixConflict(), and CVCL::Theorem3::printDebug().

Theorem & CVCL::Theorem::operator= (  const Theorem &  th  )

Definition at line 98 of file theorem.cpp. References CVCL::TheoremValue::d_refcount, d_thm, CVCL::MemoryManager::deleteData(), CVCL::TheoremValue::getMM(), IF_DEBUG(), CVCL::int2string(), isNull(), toString(), and CVCL::TRACE.

bool CVCL::Theorem::isNull (   )  const [inline]

Definition at line 150 of file theorem.h. References d_thm. Referenced by CVCL::AssumptionsValue::add(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryBitvector::assertFact(), CVCL::VCL::assertFormula(), CVCL::TheoryBitvector::bitBlastTerm(), TheoryCore::buildModel(), CVCL::VCL::checkContinue(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchSimple::checkValidRec(), clearAllFlags(), CVCL::compare(), CVCL::Variable::deriveThmRec(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::TheoryQuant::findInstAssumptions(), CVCL::Assumptions::findTheorem(), getAssumptions(), getAssumptionsRef(), CVCL::SearchImplBase::getAssumptionsUsed(), getCachedValue(), CVCL::SearchEngine::getConcreteModel(), getExpandFlag(), getExpr(), CVCL::SearchSat::getImplication(), CVCL::VCL::getImpliedLiteral(), getLHS(), getLitFlag(), getProof(), CVCL::SearchImplBase::getProof(), CVCL::VCL::getProofTCC(), getRHS(), getScope(), CVCL::VCL::getTCC(), CVCL::Expr::hasFind(), CVCL::Expr::hasRep(), CVCL::Expr::hasSig(), CVCL::CommonTheoremProducer::implIntro(), isAssump(), isFlagged(), CVCL::TheoryArith::isInteger(), CVCL::TheoryArith::isIntegerDerive(), CVCL::Theorem3::isNull(), isRewrite(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryDatatype::mergeLabels(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::SearchImplBase::newUserAssumption(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::operator<<(), operator=(), CVCL::SearchImplBase::processResult(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::projectInequalities(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::Circuit::propagate(), CVCL::VCL::query(), CVCL::SearchImplBase::replaceITE(), CVCL::VCL::restart(), CVCL::TheoryArith::rewrite(), CVCL::TheoryBitvector::rewriteBoolean(), CVCL::TheoryBitvector::rewriteBV(), CVCL::Theory::rewriteCC(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), CVCL::TheoryRecords::setup(), CVCL::VariableValue::setValue(), TheoryCore::simplifyOp(), CVCL::TheoryBitvector::simplifyOp(), CVCL::VCL::simplifyThm(), TheoryCore::subtypePredicate(), Theorem(), TheoremEq(), CVCL::CommonTheoremProducer::transitivityRule(), CVCL::TheoryUF::update(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryArray::update(), CVCL::Theory::updateCC(), and ~Theorem().

bool CVCL::Theorem::isRewrite (   )  const

Definition at line 218 of file theorem.cpp. References d_thm, isNull(), and CVCL::TheoremValue::isRewrite(). Referenced by CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::applyCNFRules(), TheoryCore::assertEqualities(), CVCL::TheoryDatatype::assertFact(), CVCL::TheoryBitvector::assertFact(), TheoryCore::assignValue(), CVCL::compare(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::TheoryArith::doSolve(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::Theory::enqueueEquality(), TheoryCore::enqueueFact(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::SearchImplBase::findInCNFCache(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::Theorem3::isRewrite(), CVCL::TheoryArith::processIntEq(), CVCL::TheoryArith::processSimpleIntEq(), TheoryCore::processUpdates(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::ExprTransform::pushNegationRec(), CVCL::TheoryArray::renameExpr(), CVCL::SearchImplBase::replaceITE(), TheoryCore::rewriteCore(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::TheoryDatatype::solve(), CVCL::TheoryArith::substAndCanonize(), CVCL::CommonTheoremProducer::symmetryRule(), and CVCL::CommonTheoremProducer::transitivityRule().

bool CVCL::Theorem::isAssump (   )  const

Definition at line 296 of file theorem.cpp. References d_thm, CVCL::TheoremValue::isAssump(), and isNull(). Referenced by CVCL::AssumptionsValue::add(), CVCL::AssumptionsValue::AssumptionsValue(), checkAssump(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryQuant::findInstAssumptions(), getAssumptionsRef(), CVCL::CommonTheoremProducer::implIntro(), CVCL::Theorem3::isAssump(), CVCL::SearchEngineFast::newIntAssumption(), recursivePrint(), and CVCL::SearchEngineFast::traceConflict().

const Expr & CVCL::Theorem::getExpr (   )  const

Definition at line 224 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getExpr(), and isNull(). Referenced by SAT::CNF_Manager::addAssumption(), CVCL::SearchImplBase::addCNFFact(), TheoryCore::addFact(), CVCL::SearchImplBase::addFact(), CVCL::SearchSat::addLemma(), SAT::CNF_Manager::addLemma(), CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::TheoryArith::addToBuffer(), CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::CommonTheoremProducer::andElim(), CVCL::SearchImplBase::applyCNFRules(), TheoryCore::assertEqualities(), CVCL::TheoryUF::assertFact(), CVCL::TheoryRecords::assertFact(), CVCL::TheoryQuant::assertFact(), CVCL::TheoryDatatype::assertFact(), TheoryCore::assertFact(), CVCL::TheoryBitvector::assertFact(), CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), TheoryCore::assignValue(), CVCL::SearchEngineFast::bcp(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::TheoryArith::canonPred(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::SearchSat::check(), checkAssump(), CVCL::TheoryBitvector::checkSat(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchSimple::checkValidRec(), CVCL::Circuit::Circuit(), CVCL::ClauseValue::ClauseValue(), TheoryCore::collectBasicVars(), TheoryCore::collectModelValues(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::compare(), CVCL::TheoryBitvector::computeModel(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::CommonTheoremProducer::contradictionRule(), SAT::CNF_Manager::convertLemma(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::Variable::deriveThmRec(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::TheoryArith::doSolve(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::SearchImplBase::enqueueCNFrec(), TheoryCore::enqueueEquality(), TheoryCore::enqueueFact(), CVCL::SearchEngineFast::enqueueFact(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::SearchImplBase::findInCNFCache(), CVCL::TheoryQuant::findInstAssumptions(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::SearchEngineFast::fixConflict(), CVCL::Theorem3::getExpr(), CVCL::SearchSat::getImplication(), CVCL::VCL::getImpliedLiteral(), CVCL::SearchSat::getImpliedLiteral(), CVCL::VCL::getTCC(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffMP(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implMP(), CVCL::ArithTheoremProducer::intVarEqnConst(), isAbsLiteral(), CVCL::TheoryArith::isIntegerDerive(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::isStale(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::SearchImplBase::newIntAssumption(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::SearchSat::newUserAssumption(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryQuant::notifyInconsistent(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::CommonTheoremProducer::notToIff(), CVCL::operator<<(), CVCL::TheoryBitvector::padBVPlus(), CVCL::ExprTransform::preprocess(), printx(), CVCL::TheoryArith::processBuffer(), TheoryCore::processEquality(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processIntEq(), processNode(), CVCL::SearchImplBase::processResult(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::projectInequalities(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::Circuit::propagate(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), proves(), CVCL::DecisionEngine::pushDecision(), CVCL::ExprTransform::pushNegation1(), CVCL::CoreTheoremProducer::queryTCC(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::TheoryQuant::recInstantiate(), CVCL::SearchEngineFast::recordFact(), recursivePrint(), refutes(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), SAT::CNF_Manager::replaceITErec(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::TheoryRecords::rewriteAux(), CVCL::TheoryBitvector::rewriteBV(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::TheoryQuant::semInst(), TheoryCore::setupTerm(), CVCL::TheoryQuant::setupTriggers(), CVCL::VariableValue::setValue(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::SearchImplBase::simplify(), TheoryCore::simplifyOp(), CVCL::VCL::simplifyThm(), CVCL::CommonTheoremProducer::skolemize(), TheoryCore::solve(), CVCL::TheoryBitvector::solve(), CVCL::TheoryArray::solve(), CVCL::TheoryArith::solve(), CVCL::SearchEngineFast::split(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::TheoryArith::substAndCanonize(), TheoryCore::subtypePredicate(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::TheoryQuant::synInst(), TheoremEq(), CVCL::SearchEngineFast::traceConflict(), CVCL::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExpr(), CVCL::SearchEngineTheoremProducer::unitProp(), CVCL::SearchEngineFast::unitPropagation(), CVCL::TheoryBitvector::update(), CVCL::Theory::updateCC(), and CVCL::CommonTheoremProducer::varIntroSkolem().

const Expr & CVCL::Theorem::getLHS (   )  const

Definition at line 229 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getLHS(), and isNull(). Referenced by CVCL::RefinedArithTheoremProducer::addRCancel(), CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::applyCNFRules(), TheoryCore::assertEqualities(), CVCL::TheoryBitvector::assertFact(), TheoryCore::assignValue(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), TheoryCore::buildModel(), CVCL::TheoryArith::canon(), CVCL::TheoryArith::canonRec(), checkRewriteType(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryBitvector::checkSat(), CVCL::compare(), CVCL::BitvectorTheoremProducer::computeCarryPreComputed(), CVCL::TheoryUF::computeModel(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::Theory::find(), CVCL::SearchImplBase::findInCNFCache(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::Theorem3::getLHS(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::RefinedArithTheoremProducer::multZeroL(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), SAT::CNF_Manager::replaceITErec(), TheoryCore::rewrite(), CVCL::TheoryRecords::rewriteAux(), CVCL::TheoryBitvector::rewriteBoolean(), CVCL::TheoryBitvector::rewriteBV(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::Expr::setFind(), CVCL::TheoryBitvector::setupExpr(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::TheoryBitvector::signExtendBVLT(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), TheoryCore::simplifyOp(), CVCL::TheoryBitvector::simplifyOp(), CVCL::Theory::simplifyOp(), CVCL::TheoryDatatype::solve(), CVCL::TheoryBitvector::solve(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryBitvector::update(), CVCL::TheoryArith::update(), and CVCL::Theory::updateHelper().

const Expr & CVCL::Theorem::getRHS (   )  const

Definition at line 234 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getRHS(), and isNull(). Referenced by CVCL::RefinedArithTheoremProducer::addRCancel(), CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::applyCNFRules(), TheoryCore::assertEqualities(), TheoryCore::assignValue(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractSXRule(), TheoryCore::buildModel(), CVCL::TheoryArith::canon(), CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonDivide(), CVCL::ArithTheoremProducer::canonInvertMult(), CVCL::ArithTheoremProducer::canonMult(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::TheoryArith::canonPredEquiv(), CVCL::TheoryArith::canonRec(), CVCL::TheoryArith::canonSimplify(), checkRewriteType(), CVCL::TheoryDatatypeLazy::checkSat(), TheoryCore::checkSat(), CVCL::TheoryBitvector::checkSat(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), TheoryCore::collectBasicVars(), TheoryCore::collectModelValues(), CVCL::BitvectorTheoremProducer::collectOneTermOfPlus(), CVCL::compare(), CVCL::BitvectorTheoremProducer::computeCarryPreComputed(), CVCL::TheoryUF::computeModel(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryBitvector::computeModel(), CVCL::TheoryArray::computeModel(), TheoryCore::computeModelBasic(), CVCL::TheoryRecords::computeModelTerm(), CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryRecords::computeTCC(), TheoryCore::computeTCC(), CVCL::TheoryArray::computeTCC(), CVCL::Theory::computeTCC(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::TheoryArith::doSolve(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::equalLeaves1(), CVCL::ArithTheoremProducer::equalLeaves2(), CVCL::ArithTheoremProducer::equalLeaves3(), CVCL::ArithTheoremProducer::equalLeaves4(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::Theory::find(), CVCL::Theory::findExpr(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::Theorem3::getRHS(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::isStale(), CVCL::ExprTransform::ite_convert(), CVCL::ExprTransform::ite_simplify(), CVCL::Theory::leavesAreSimp(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryArith::normalize(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryBitvector::parseExprOp(), CVCL::ExprTransform::preprocess(), TheoryCore::processEquality(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), TheoryCore::processUpdates(), CVCL::ExprTransform::pushNegation1(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::ExprTransform::pushNegationRec(), TheoryCore::registerAtom(), CVCL::TheoryArray::renameExpr(), CVCL::SearchImplBase::replaceITE(), SAT::CNF_Manager::replaceITErec(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::TheoryUF::rewrite(), CVCL::TheoryRecords::rewrite(), CVCL::TheoryDatatype::rewrite(), TheoryCore::rewrite(), CVCL::TheoryArith::rewrite(), CVCL::TheoryBitvector::rewriteAtomic(), CVCL::TheoryRecords::rewriteAux(), CVCL::TheoryBitvector::rewriteBoolean(), CVCL::TheoryBitvector::rewriteBV(), TheoryCore::rewriteCore(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteThen(), TheoryCore::rewriteN(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::TheoryArith::rewriteToDiff(), CVCL::TheoryRecords::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::TheoryBitvector::signExtendBVLT(), CVCL::VCL::simplify(), TheoryCore::simplify(), CVCL::Theory::simplifyExpr(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), TheoryCore::simplifyOp(), CVCL::TheoryBitvector::simplifyOp(), CVCL::Theory::simplifyOp(), CVCL::VCL::simplifyThm(), CVCL::VCL::simplifyThm2(), CVCL::TheoryDatatype::solve(), CVCL::TheoryBitvector::solve(), CVCL::SearchEngineFast::split(), CVCL::TheoryArith::substAndCanonize(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVCL::RefinedArithTheoremProducer::uMinusToMult(), CVCL::TheoryUF::update(), CVCL::TheoryRecords::update(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryBitvector::update(), CVCL::TheoryArray::update(), CVCL::TheoryArith::update(), CVCL::Theory::updateCC(), and CVCL::Theory::updateHelper().

const Assumptions & CVCL::Theorem::getAssumptions (   )  const

Definition at line 240 of file theorem.cpp. References CVCL::Assumptions::add(), CVCL::TheoremValue::d_assump, d_thm, CVCL::Assumptions::empty(), getAssumptionsRef(), CVCL::Assumptions::init(), CVCL::TheoremValue::isAssump(), CVCL::Assumptions::isNull(), isNull(), CVCL::Assumptions::setConst(), and withAssumptions(). Referenced by CVCL::AssumptionsValue::add(), CVCL::CommonTheoremProducer::andElim(), CVCL::AssumptionsValue::AssumptionsValue(), CVCL::SearchEngineTheoremProducer::caseSplit(), checkAssump(), checkAssumpDebug(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::ArithTheoremProducer::equalLeaves1(), CVCL::ArithTheoremProducer::equalLeaves2(), CVCL::ArithTheoremProducer::equalLeaves3(), CVCL::ArithTheoremProducer::equalLeaves4(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::Assumptions::findTheorem(), CVCL::Theorem3::getAssumptions(), getAssumptionsCopy(), CVCL::SearchImplBase::getAssumptionsUsed(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::CommonTheoremProducer::notToIff(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::CoreTheoremProducer::queryTCC(), recursivePrint(), CVCL::UFTheoremProducer::relToClosure(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), and CVCL::SearchEngineTheoremProducer::verifyConflict().

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

Referenced by TheoryCore::buildModel(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngine::getConcreteModel(), CVCL::CNF_TheoremProducer::learnedClause(), and TheoryCore::refineCounterExample().

const Assumptions & CVCL::Theorem::getAssumptionsRef (   )  const

Definition at line 283 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getAssumptionsRef(), isAssump(), isNull(), and withAssumptions(). Referenced by CVCL::SearchEngineFast::analyzeUIPs(), CVCL::TheoryQuant::findInstAssumptions(), getAssumptions(), CVCL::Theorem3::getAssumptionsRef(), CVCL::CommonTheoremProducer::implIntro(), and CVCL::SearchEngineFast::traceConflict().

Assumptions CVCL::Theorem::getAssumptionsCopy (   )  const

Definition at line 304 of file theorem.cpp. References CVCL::Assumptions::copy(), and getAssumptions(). Referenced by CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::Theorem3::getAssumptionsCopy(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::ArithTheoremProducer::splitGrayShadow(), and CVCL::CommonTheoremProducer::symmetryRule().

const Proof & CVCL::Theorem::getProof (   )  const

Definition at line 309 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getProof(), isNull(), and withProof(). Referenced by CVCL::CommonTheoremProducer::andElim(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::equalLeaves1(), CVCL::ArithTheoremProducer::equalLeaves2(), CVCL::ArithTheoremProducer::equalLeaves3(), CVCL::ArithTheoremProducer::equalLeaves4(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::Theorem3::getProof(), CVCL::SearchImplBase::getProof(), CVCL::VCL::getProofTCC(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implMP(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::CommonTheoremProducer::notToIff(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), CVCL::CoreTheoremProducer::queryTCC(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), and CVCL::SearchEngineTheoremProducer::unitProp().

int CVCL::Theorem::getScope (   )  const

Definition at line 367 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getScope(), and isNull(). Referenced by CVCL::SearchImplBase::enqueueCNFrec(), TheoryCore::enqueueEquality(), TheoryCore::enqueueFact(), CVCL::SearchEngineFast::fixConflict(), CVCL::Theorem3::getScope(), CVCL::SearchEngineFast::recordFact(), recursivePrint(), CVCL::Literal::setValue(), CVCL::Variable::setValue(), and CVCL::SearchEngineFast::traceConflict().

bool CVCL::Theorem::withProof (   )  const

Definition at line 211 of file theorem.cpp. References d_thm, CVCL::TheoremValue::d_tm, and CVCL::TheoremManager::withProof(). Referenced by getProof(), Theorem(), and CVCL::Theorem3::withProof().

bool CVCL::Theorem::withAssumptions (   )  const

Definition at line 214 of file theorem.cpp. References d_thm, CVCL::TheoremValue::d_tm, and CVCL::TheoremManager::withAssumptions(). Referenced by checkAssumpDebug(), getAssumptions(), getAssumptionsRef(), and CVCL::Theorem3::withAssumptions().

std::string CVCL::Theorem::toString (   )  const [inline]

Definition at line 371 of file theorem.h. Referenced by CVCL::AssumptionsValue::add(), CVCL::SearchEngineFast::addLiteralFact(), CVCL::CommonTheoremProducer::andElim(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryRecords::assertFact(), CVCL::TheoryQuant::assertFact(), TheoryCore::assertFact(), TheoryCore::assertFormula(), TheoryCore::assignValue(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::TheoryArith::canonPred(), CVCL::TheoryArith::canonPredEquiv(), checkAssump(), checkRewriteType(), CVCL::ClauseValue::ClauseValue(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::Variable::deriveThmRec(), CVCL::TheoryArith::doSolve(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::Theory::enqueueEquality(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::CommonTheoremProducer::implMP(), CVCL::TheoryArith::isolateVariable(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::TheoryQuant::notifyInconsistent(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::CommonTheoremProducer::notToIff(), operator=(), print(), TheoryCore::processEquality(), processNode(), TheoryCore::processNotify(), CVCL::TheoryArith::processRealEq(), CVCL::SearchImplBase::processResult(), CVCL::TheoryArith::projectInequalities(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::ExprTransform::pushNegationRec(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::TheoryQuant::recInstantiate(), CVCL::TheoryArray::renameExpr(), CVCL::TheoryBitvector::rewriteAtomic(), TheoryCore::rewriteCore(), CVCL::TheoryQuant::semInst(), CVCL::VariableValue::setValue(), CVCL::TheoryQuant::synInst(), Theorem(), CVCL::SearchEngineFast::traceConflict(), CVCL::SearchEngineTheoremProducer::unitProp(), and CVCL::TheoryBitvector::update().

void CVCL::Theorem::printx (   )  const

Definition at line 206 of file theorem.cpp. References getExpr(), and CVCL::Expr::print(). Referenced by CVCL::Theorem3::printx().

void CVCL::Theorem::print (   )  const

Definition at line 208 of file theorem.cpp. References std::endl(), and toString(). Referenced by CVCL::Theorem3::print().

bool CVCL::Theorem::isFlagged (   )  const

Check if the flag attribute is set. Definition at line 318 of file theorem.cpp. References d_thm, CVCL::TheoremValue::isFlagged(), and isNull(). Referenced by CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryQuant::findInstAssumptions(), processNode(), and CVCL::SearchEngineFast::traceConflict().

void CVCL::Theorem::clearAllFlags (   )  const

Clear the flag attribute in all the theorems. Definition at line 323 of file theorem.cpp. References CVCL::TheoremValue::clearAllFlags(), d_thm, and isNull(). Referenced by CVCL::SearchEngineFast::analyzeUIPs(), checkAssumpDebug(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::TheoryQuant::notifyInconsistent(), printDebug(), and CVCL::SearchEngineFast::traceConflict().

void CVCL::Theorem::setFlag (   )  const

Set the flag attribute. Definition at line 328 of file theorem.cpp. References d_thm, isNull(), and CVCL::TheoremValue::setFlag(). Referenced by CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryQuant::findInstAssumptions(), CVCL::Assumptions::findTheorem(), printDebug(), processNode(), and CVCL::SearchEngineFast::traceConflict().

void CVCL::Theorem::setExpandFlag (  bool  val  )  const

Set the "expand" attribute. Definition at line 343 of file theorem.cpp. References d_thm, isNull(), and CVCL::TheoremValue::setExpandFlag(). Referenced by CVCL::SearchEngineFast::traceConflict().

bool CVCL::Theorem::getExpandFlag (   )  const

Check the "expand" attribute. Definition at line 348 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getExpandFlag(), and isNull(). Referenced by processNode().

void CVCL::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 353 of file theorem.cpp. References d_thm, isNull(), and CVCL::TheoremValue::setLitFlag(). Referenced by CVCL::SearchEngineFast::traceConflict().

bool CVCL::Theorem::getLitFlag (   )  const

Check the "literal" attribute. The expression of this theorem will be added as a conflict clause literal Definition at line 358 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getLitFlag(), and isNull(). Referenced by processNode().

bool CVCL::Theorem::isAbsLiteral (   )  const

Check if the theorem is a literal. Definition at line 363 of file theorem.cpp. References getExpr(), and CVCL::Expr::isAbsLiteral(). Referenced by CVCL::SearchImplBase::addCNFFact(), CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchEngineFast::enqueueFact(), CVCL::Theorem3::isAbsLiteral(), processNode(), CVCL::SearchEngineFast::traceConflict(), and CVCL::SearchEngineFast::unitPropagation().

bool CVCL::Theorem::refutes (  const Expr &  e  )  const [inline]

Check if the flag attribute is set. Definition at line 219 of file theorem.h. References getExpr(), and CVCL::Expr::isNot(). Referenced by CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), matches(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), and CVCL::SearchEngineTheoremProducer::propIterThen().

bool CVCL::Theorem::proves (  const Expr &  e  )  const [inline]

Check if the flag attribute is set. Definition at line 226 of file theorem.h. References getExpr(). Referenced by CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), matches(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), and CVCL::SearchEngineTheoremProducer::propIterThen().

bool CVCL::Theorem::matches (  const Expr &  e  )  const [inline]

Check if the flag attribute is set. Definition at line 231 of file theorem.h. References proves(), and refutes().

void CVCL::Theorem::setCachedValue (  int  value  )  const

Check if the flag attribute is set. Definition at line 333 of file theorem.cpp. References d_thm, isNull(), and CVCL::TheoremValue::setCachedValue(). Referenced by printDebug(), processNode(), and CVCL::SearchEngineFast::traceConflict().

int CVCL::Theorem::getCachedValue (   )  const

Check if the flag attribute is set. Definition at line 338 of file theorem.cpp. References d_thm, CVCL::TheoremValue::getCachedValue(), and isNull(). Referenced by processNode(), recursivePrint(), and CVCL::SearchEngineFast::traceConflict().

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

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

---

Friends And Related Function Documentation

friend class TheoremProducer [friend]

Definition at line 88 of file theorem.h.

friend class Theorem3 [friend]

Definition at line 90 of file theorem.h.

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 53 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 73 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 91 of file theorem.cpp.

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

Equality is w.r.t. compare(). Definition at line 101 of file theorem.h.

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

Disequality is w.r.t. compare(). Definition at line 104 of file theorem.h.

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

Definition at line 244 of file theorem.h.

---

Member Data Documentation

TheoremValue* CVCL::Theorem::d_thm [private]

Definition at line 92 of file theorem.h. Referenced by clearAllFlags(), CVCL::compare(), CVCL::compareByPtr(), getAssumptions(), getAssumptionsRef(), getCachedValue(), getExpandFlag(), getExpr(), getLHS(), getLitFlag(), getProof(), getRHS(), getScope(), isAssump(), isFlagged(), isNull(), isRewrite(), operator=(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), Theorem(), withAssumptions(), withProof(), and ~Theorem().

---

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

• theorem.h
• theorem.cpp

---