CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | Friends
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


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

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

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

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

Definition at line 182 of file theorem.cpp.

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

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

Definition at line 151 of file theorem.h.

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

Member Function Documentation

void CVC3::Theorem::recursivePrint ( int &  i) const [private]
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]
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
bool CVC3::Theorem::isNull ( ) const [inline]

Definition at line 164 of file theorem.h.

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

bool CVC3::Theorem::isRewrite ( ) const

Definition at line 224 of file theorem.cpp.

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

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

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

Definition at line 230 of file theorem.cpp.

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

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

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

Definition at line 240 of file theorem.cpp.

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

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

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

Definition at line 246 of file theorem.cpp.

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

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

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

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

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

Definition at line 385 of file theorem.cpp.

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

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

Proof CVC3::Theorem::getProof ( ) const

Definition at line 402 of file theorem.cpp.

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

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

int CVC3::Theorem::getScope ( ) const
unsigned CVC3::Theorem::getQuantLevel ( ) const
unsigned CVC3::Theorem::getQuantLevelDebug ( ) const
void CVC3::Theorem::setQuantLevel ( unsigned  level)
size_t CVC3::Theorem::hash ( ) const

Definition at line 511 of file theorem.cpp.

References d_thm.

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

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

Definition at line 404 of file theorem.h.

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

void CVC3::Theorem::printx ( ) const

Definition at line 207 of file theorem.cpp.

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

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

void CVC3::Theorem::printxnodag ( ) const

Definition at line 208 of file theorem.cpp.

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

void CVC3::Theorem::pprintx ( ) const

Definition at line 209 of file theorem.cpp.

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

void CVC3::Theorem::pprintxnodag ( ) const

Definition at line 210 of file theorem.cpp.

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

void CVC3::Theorem::print ( ) const

Definition at line 211 of file theorem.cpp.

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

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

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

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

bool CVC3::Theorem::isSubst ( ) const

Is theorem an instance of substitution.

Definition at line 452 of file theorem.cpp.

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

Referenced by getAssumptionsAndCongRec(), and recursivePrint().

void CVC3::Theorem::setExpandFlag ( bool  val) const
bool CVC3::Theorem::getExpandFlag ( ) const
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 470 of file theorem.cpp.

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

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

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

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
int CVC3::Theorem::getCachedValue ( ) const
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().


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.

friend class RWTheoremValue [friend]

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

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

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

Definition at line 65 of file theorem.cpp.

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

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

Definition at line 83 of file theorem.cpp.

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

Equality is w.r.t. compare()

Definition at line 102 of file theorem.h.

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

Disequality is w.r.t. compare()

Definition at line 105 of file theorem.h.

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

Definition at line 277 of file theorem.h.


Member Data Documentation

Definition at line 91 of file theorem.h.

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

union { ... } [private]

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