CVC3
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | Friends

CVC3::Theorem Class Reference

#include <theorem.h>

Collaboration diagram for CVC3::Theorem:
Collaboration graph
[legend]

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]

Constructor for a new theorem.

Definition at line 132 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, DebugAssert, and CVC3::Proof::isNull().

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

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

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

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

Definition at line 183 of file theorem.cpp.

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

Definition at line 151 of file theorem.h.

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

Definition at line 171 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, DebugAssert, CVC3::int2string(), and thm().

CVC3::Theorem::~Theorem ( )

Member Function Documentation

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

Definition at line 517 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.

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

Definition at line 133 of file theorem.h.

Referenced by getAssumptionsAndCongRec(), getAssumptionsRef(), Theorem(), and ~Theorem().

void CVC3::Theorem::printDebug ( ) const [inline]
Theorem & CVC3::Theorem::operator= ( const Theorem th)

Definition at line 92 of file theorem.cpp.

References CVC3::TheoremValue::d_refcount, and DebugAssert.

bool CVC3::Theorem::withProof ( ) const

Definition at line 215 of file theorem.cpp.

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

bool CVC3::Theorem::withAssumptions ( ) const

Definition at line 220 of file theorem.cpp.

Referenced by 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::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithOld::computeTermBounds(), SAT::CNF_Manager::concreteThm(), 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(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), getLeafAssumptions(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::getProof(), CVC3::Expr::hasFind(), CVC3::Expr::hasRep(), CVC3::Expr::hasSig(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), 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::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<<(), 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(), 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 225 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::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::Theory::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 231 of file theorem.cpp.

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::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(), 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::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(), CVC3::ExprTransform::preprocess(), printx(), printxnodag(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArith3::processBuffer(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), processNode(), CVC3::TheoryArithOld::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::DecisionEngine::pushDecision(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryQuant::recInstantiate(), CVC3::SearchEngineFast::recordFact(), 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(), and CVC3::TheoryArith3::update().

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

Definition at line 241 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::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::ArrayTheoremProducer::propagateIndexDiseq(), 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 247 of file theorem.cpp.

Referenced by 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::canonDivide(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), 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::TheoryUF::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::TheoryBitvector::comparebv(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArray::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::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::Theory::find(), CVC3::Theory::findExpr(), CVC3::Theory::findReduced(), CVC3::Theory::findRef(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::TheoryCore::getAssignment(), getAssumptionsAndCongRec(), CVC3::Theorem3::getRHS(), CVC3::TheoryCore::getValue(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::TheoryArithOld::inequalityToFind(), 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::Translator::preprocessRec(), 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::TheoryCore::registerAtom(), CVC3::Theory::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::TheoryCore::setFindLiteral(), CVC3::TheoryRecords::setup(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryCore::simplify(), CVC3::Theory::simplifyExpr(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::VCL::simplifyThm(), CVC3::TheoryDatatype::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::SearchEngineFast::split(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::TheoryQuant::synNewInst(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryQuant::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::Theory::updateCC(), CVC3::Theory::updateHelper(), and CVC3::TheoryBitvector::updateSubterms().

void CVC3::Theorem::GetSatAssumptions ( std::vector< Theorem > &  assumptions) const

Definition at line 310 of file theorem.cpp.

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

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

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

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

Definition at line 386 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::SearchImplBase::getAssumptionsUsed(), GetSatAssumptionsRec(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::implIntro(), 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(), 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 403 of file theorem.cpp.

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::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(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), 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 498 of file theorem.cpp.

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

Definition at line 512 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(), pprintxnodag(), 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::Theory::renameExpr(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::setupTerm(), CVC3::VariableValue::setValue(), and CVC3::SearchEngineTheoremProducer::unitProp().

void CVC3::Theorem::printx ( ) const

Definition at line 208 of file theorem.cpp.

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

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

void CVC3::Theorem::printxnodag ( ) const

Definition at line 209 of file theorem.cpp.

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

void CVC3::Theorem::pprintx ( ) const

Definition at line 210 of file theorem.cpp.

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

void CVC3::Theorem::pprintxnodag ( ) const

Definition at line 211 of file theorem.cpp.

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

void CVC3::Theorem::print ( ) const

Definition at line 212 of file theorem.cpp.

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

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

bool CVC3::Theorem::isSubst ( ) const

Is theorem an instance of substitution.

Definition at line 453 of file theorem.cpp.

Referenced by getAssumptionsAndCongRec().

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

Set the "expand" attribute.

Definition at line 459 of file theorem.cpp.

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

bool CVC3::Theorem::getExpandFlag ( ) const

Check the "expand" attribute.

Definition at line 465 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 471 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 477 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 436 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 442 of file theorem.cpp.

Referenced by processNode().

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

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

Definition at line 581 of file theorem.cpp.

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 46 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 66 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 84 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.

Definition at line 92 of file theorem.h.

union { ... } [private]

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