CVC3::Theorem Class Reference

#include <theorem.h>

List of all members.

Public Member Functions

Methods for Theorem Attributes

Several attributes used in conflict analysis and assumptions graph traversals.

Static Public Member Functions

Private Member Functions

Private Attributes

Friends


Detailed Description

Definition at line 76 of file theorem.h.


Constructor & Destructor Documentation

CVC3::Theorem::Theorem ( TheoremValue thm  )  [inline, private]

Constructor only used by TheoremValue for assumptions.

Definition at line 109 of file theorem.h.

CVC3::Theorem::Theorem ( TheoremManager tm,
const Expr thm,
const Assumptions assump,
const Proof pf,
bool  isAssump = false,
int  scope = -1 
) [private]
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 150 of file theorem.cpp.

CVC3::Theorem::Theorem ( const Expr e  )  [private]

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

Definition at line 180 of file theorem.cpp.

CVC3::Theorem::Theorem (  )  [inline]

Definition at line 151 of file theorem.h.

CVC3::Theorem::Theorem ( const Theorem th  ) 
CVC3::Theorem::~Theorem (  ) 

Member Function Documentation

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

Definition at line 514 of file theorem.cpp.

void CVC3::Theorem::getAssumptionsRec ( std::set< Expr > &  assumptions  )  const [private]
void CVC3::Theorem::getAssumptionsAndCongRec ( std::set< Expr > &  assumptions,
std::vector< Expr > &  congruences 
) const [private]
void CVC3::Theorem::GetSatAssumptionsRec ( std::vector< Theorem > &  assumptions  )  const [private]
ExprValue* CVC3::Theorem::exprValue (  )  const [inline, private]

Definition at line 132 of file theorem.h.

Referenced by getExpr(), getProof(), operator=(), Theorem(), withProof(), and ~Theorem().

TheoremValue* CVC3::Theorem::thm (  )  const [inline, private]
void CVC3::Theorem::printDebug (  )  const [inline]
Theorem & CVC3::Theorem::operator= ( const Theorem th  ) 
bool CVC3::Theorem::withProof (  )  const
bool CVC3::Theorem::withAssumptions (  )  const

Definition at line 217 of file theorem.cpp.

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

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

Definition at line 164 of file theorem.h.

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

bool CVC3::Theorem::isRewrite (  )  const

Definition at line 222 of file theorem.cpp.

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

bool CVC3::Theorem::isAssump (  )  const
bool CVC3::Theorem::isRefl (  )  const [inline]
Expr CVC3::Theorem::getExpr (  )  const

Definition at line 228 of file theorem.cpp.

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

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

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

Definition at line 238 of file theorem.cpp.

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

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

Definition at line 244 of file theorem.cpp.

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

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

Definition at line 368 of file theorem.cpp.

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

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

Definition at line 383 of file theorem.cpp.

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

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

Proof CVC3::Theorem::getProof (  )  const

Definition at line 400 of file theorem.cpp.

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

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

int CVC3::Theorem::getScope (  )  const
unsigned CVC3::Theorem::getQuantLevel (  )  const
unsigned CVC3::Theorem::getQuantLevelDebug (  )  const

Definition at line 495 of file theorem.cpp.

void CVC3::Theorem::setQuantLevel ( unsigned  level  ) 
size_t CVC3::Theorem::hash (  )  const

Definition at line 509 of file theorem.cpp.

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

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

Definition at line 404 of file theorem.h.

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

void CVC3::Theorem::printx (  )  const

Definition at line 205 of file theorem.cpp.

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

void CVC3::Theorem::printxnodag (  )  const

Definition at line 206 of file theorem.cpp.

void CVC3::Theorem::pprintx (  )  const

Definition at line 207 of file theorem.cpp.

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

void CVC3::Theorem::pprintxnodag (  )  const

Definition at line 208 of file theorem.cpp.

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

void CVC3::Theorem::print (  )  const

Definition at line 209 of file theorem.cpp.

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

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

bool CVC3::Theorem::isFlagged (  )  const
void CVC3::Theorem::clearAllFlags (  )  const
void CVC3::Theorem::setFlag (  )  const
void CVC3::Theorem::setSubst (  )  const

Set flag stating that theorem is an instance of substitution.

Definition at line 445 of file theorem.cpp.

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

bool CVC3::Theorem::isSubst (  )  const

Is theorem an instance of substitution.

Definition at line 450 of file theorem.cpp.

Referenced by getAssumptionsAndCongRec().

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

Set the "expand" attribute.

Definition at line 456 of file theorem.cpp.

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

bool CVC3::Theorem::getExpandFlag (  )  const

Check the "expand" attribute.

Definition at line 462 of file theorem.cpp.

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 468 of file theorem.cpp.

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 474 of file theorem.cpp.

Referenced by processNode().

bool CVC3::Theorem::isAbsLiteral (  )  const
bool CVC3::Theorem::refutes ( const Expr e  )  const [inline]
bool CVC3::Theorem::proves ( const Expr e  )  const [inline]
bool CVC3::Theorem::matches ( const Expr e  )  const [inline]

Check if the flag attribute is set.

Definition at line 264 of file theorem.h.

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

Check if the flag attribute is set.

Definition at line 433 of file theorem.cpp.

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

int CVC3::Theorem::getCachedValue (  )  const

Check if the flag attribute is set.

Definition at line 439 of file theorem.cpp.

Referenced by processNode().

ostream & CVC3::Theorem::print ( std::ostream &  os,
const std::string &  name 
) const
static bool CVC3::Theorem::TheoremEq ( const Theorem t1,
const Theorem t2 
) [inline, static]

Definition at line 281 of file theorem.h.

References DebugAssert, and isNull().

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


Friends And Related Function Documentation

friend class TheoremProducer [friend]

Definition at line 80 of file theorem.h.

friend class Theorem3 [friend]

Definition at line 82 of file theorem.h.

friend class RegTheoremValue [friend]

Definition at line 84 of file theorem.h.

Referenced by Theorem().

friend class RWTheoremValue [friend]

Definition at line 85 of file theorem.h.

Referenced by Theorem().

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

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

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

Definition at line 43 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 63 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 81 of file theorem.cpp.

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

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

Definition at line 102 of file theorem.h.

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

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

Definition at line 105 of file theorem.h.

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

Definition at line 277 of file theorem.h.


Member Data Documentation

Definition at line 91 of file theorem.h.

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

Definition at line 92 of file theorem.h.

Referenced by Theorem().

union { ... } [private]

The documentation for this class was generated from the following files:
Generated by  doxygen 1.6.2-20100208