CVC3
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::Theorem Class Reference

#include <theorem.h>

Collaboration diagram for CVC3::Theorem:
Collaboration graph

Public Member Functions

void printDebug () const
 
 Theorem ()
 
 Theorem (const Theorem &th)
 
Theoremoperator= (const Theorem &th)
 
 ~Theorem ()
 
bool withProof () const
 
bool withAssumptions () const
 
bool isNull () const
 
bool isRewrite () const
 
bool isAssump () const
 
bool isRefl () const
 
Expr getExpr () const
 
const ExprgetLHS () const
 
const ExprgetRHS () const
 
void GetSatAssumptions (std::vector< Theorem > &assumptions) const
 
void getLeafAssumptions (std::vector< Expr > &assumptions, bool negate=false) const
 
void getAssumptionsAndCong (std::vector< Expr > &assumptions, std::vector< Expr > &congruences, bool negate=false) const
 
const AssumptionsgetAssumptionsRef () const
 
Proof getProof () const
 
int getScope () const
 
unsigned getQuantLevel () const
 Return quantification level for this theorem.
 
unsigned getQuantLevelDebug () const
 
void setQuantLevel (unsigned level)
 Set the quantification level for this theorem.
 
size_t hash () const
 
std::string toString () const
 
void printx () const
 
void printxnodag () const
 
void pprintx () const
 
void pprintxnodag () const
 
void print () const
 
std::ostream & print (std::ostream &os, const std::string &name) const
 Printing a theorem to a stream, calling it "name".
 
Methods for Theorem Attributes

Several attributes used in conflict analysis and assumptions graph traversals.

bool isFlagged () const
 Check if the flag attribute is set.
 
void clearAllFlags () const
 Clear the flag attribute in all the theorems.
 
void setFlag () const
 Set the flag attribute.
 
void setSubst () const
 Set flag stating that theorem is an instance of substitution.
 
bool isSubst () const
 Is theorem an instance of substitution.
 
void setExpandFlag (bool val) const
 Set the "expand" attribute.
 
bool getExpandFlag () const
 Check the "expand" attribute.
 
void setLitFlag (bool val) const
 Set the "literal" attribute.
 
bool getLitFlag () const
 Check the "literal" attribute.
 
bool isAbsLiteral () const
 Check if the theorem is a literal.
 
bool refutes (const Expr &e) const
 Check if the flag attribute is set.
 
bool proves (const Expr &e) const
 Check if the flag attribute is set.
 
bool matches (const Expr &e) const
 Check if the flag attribute is set.
 
void setCachedValue (int value) const
 Check if the flag attribute is set.
 
int getCachedValue () const
 Check if the flag attribute is set.
 

Static Public Member Functions

static bool TheoremEq (const Theorem &t1, const Theorem &t2)
 

Private Member Functions

 Theorem (TheoremValue *thm)
 Constructor only used by TheoremValue for assumptions.
 
 Theorem (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)
 Constructor for a new theorem.
 
 Theorem (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)
 Constructor for rewrite theorems.
 
 Theorem (const Expr &e)
 Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi.
 
void recursivePrint (int &i) const
 
void getAssumptionsRec (std::set< Expr > &assumptions) const
 
void getAssumptionsAndCongRec (std::set< Expr > &assumptions, std::vector< Expr > &congruences) const
 
void GetSatAssumptionsRec (std::vector< Theorem > &assumptions) const
 
ExprValueexprValue () const
 
TheoremValuethm () const
 

Private Attributes

union {
   intptr_t   d_thm
 
   ExprValue *   d_expr
 
}; 
 

Friends

class TheoremProducer
 
class Theorem3
 
class RegTheoremValue
 
class RWTheoremValue
 
int compare (const Theorem &t1, const Theorem &t2)
 Compare Theorems by their expressions. Return -1, 0, or 1.
 
int compare (const Theorem &t1, const Expr &e2)
 Compare a Theorem with an Expr (as if Expr is a Theorem)
 
int compareByPtr (const Theorem &t1, const Theorem &t2)
 Compare Theorems by TheoremValue pointers. Return -1, 0, or 1.
 
bool operator== (const Theorem &t1, const Theorem &t2)
 Equality is w.r.t. compare()
 
bool operator!= (const Theorem &t1, const Theorem &t2)
 Disequality is w.r.t. compare()
 
std::ostream & operator<< (std::ostream &os, const Theorem &t)
 

Detailed Description

Definition at line 76 of file theorem.h.

Constructor & Destructor Documentation

CVC3::Theorem::Theorem ( TheoremValue thm)
inlineprivate

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::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 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
inlineprivate
TheoremValue* CVC3::Theorem::thm ( ) const
inlineprivate
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::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryCore::buildModel(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), clearAllFlags(), CVC3::compare(), 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::SearchImplBase::getAssumptionsUsed(), CVC3::VCL::getAssumptionsUsed(), getCachedValue(), CVC3::SearchImplBase::getCounterExample(), CVC3::SearchSat::getCounterExample(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), getExpandFlag(), getExpr(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), getLeafAssumptions(), getLHS(), getLitFlag(), getProof(), CVC3::SearchImplBase::getProof(), CVC3::SearchSat::getProof(), getQuantLevel(), getQuantLevelDebug(), getRHS(), getScope(), CVC3::Expr::hasFind(), CVC3::Expr::hasRep(), CVC3::Expr::hasSig(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), isAssump(), CVC3::TheoryArithOld::isConstrained(), isFlagged(), CVC3::TheoryArithNew::isInteger(), CVC3::TheoryArith3::isInteger(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithOld::isIntegerDerive(), SAT::SatProofNode::isLeaf(), CVC3::Theorem3::isNull(), isRewrite(), isSubst(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::multMatchChild(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::operator<<(), print(), printSatProof(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::Circuit::propagate(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::SearchImplBase::replaceITE(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::Theory::rewriteCC(), SAT::SatProofNode::SatProofNode(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), setSubst(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::simplifyOp(), TheoremEq(), TheoremEq(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and CVC3::Theory::updateCC().

bool CVC3::Theorem::isRewrite ( ) const

Definition at line 224 of file theorem.cpp.

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

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assignValue(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::compare(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::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::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::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::TheoryArithNew::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::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 230 of file theorem.cpp.

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

Referenced by SAT::CNF_Manager::addAssumption(), CVC3::SearchImplBase::addCNFFact(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::SearchImplBase::addFact(), CVC3::TheoryCore::addFact(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::SearchSat::addLemma(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArithOld::addToBuffer(), CVC3::SearchImplBase::addToCNFCache(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::CommonTheoremProducer::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryUF::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryQuant::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::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArithOld::canonPred(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::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::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ClauseValue::ClauseValue(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::compare(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::enqueueFact(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::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::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::Assumptions::findExpr(), CVC3::Assumptions::findExprs(), CVC3::SearchImplBase::findInCNFCache(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::SearchEngineFast::fixConflict(), CVC3::TheoryBitvector::generalBitBlast(), getAssumptionsAndCongRec(), getAssumptionsRec(), CVC3::VCL::getAssumptionsRec(), CVC3::Theorem3::getExpr(), CVC3::SearchSat::getImplication(), CVC3::SearchSat::getImpliedLiteral(), CVC3::VCL::getImpliedLiteral(), CVC3::TheoryArithNew::getLowerBoundExplanation(), GetSatAssumptionsRec(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implMP(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), isAbsLiteral(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isStale(), CVC3::TheoryArithOld::isStale(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducerOld::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::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::operator<<(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::pivotRule(), pprintx(), pprintxnodag(), CVC3::ExprTransform::preprocess(), print(), printx(), printxnodag(), CVC3::TheoryArith3::processBuffer(), CVC3::TheoryArithOld::processBuffer(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processIntEq(), processNode(), CVC3::TheoryArithOld::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::DecisionEngine::pushDecision(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::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(), recursivePrint(), 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::TheoryArray::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::TheoryArithOld::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::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::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryQuant::update().

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

Definition at line 240 of file theorem.cpp.

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

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::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::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::compare(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::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::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::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::TheoryArithNew::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryCore::solve(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryQuant::update(), CVC3::Theory::updateHelper(), and CVC3::TheoryBitvector::updateSubterms().

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

Definition at line 246 of file theorem.cpp.

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

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::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::TheoryArithOld::canon(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArith::canonThm(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::compare(), CVC3::TheoryBitvector::comparebv(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::Theory::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::TheoryQuant::debug(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducerOld::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::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::ExprTransform::preprocess(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryArray::pullIndex(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryBitvector::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::TheoryRecords::rewrite(), CVC3::TheoryUF::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::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::TheoryBitvector::simplifyOp(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::VCL::simplifyThm(), CVC3::TheoryDatatype::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::solve(), CVC3::SearchEngineFast::split(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::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::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryCore::update(), CVC3::TheoryQuant::update(), CVC3::Theory::updateCC(), CVC3::Theory::updateHelper(), and CVC3::TheoryBitvector::updateSubterms().

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

Definition at line 370 of file theorem.cpp.

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

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

Definition at line 385 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::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::Assumptions::findExpr(), CVC3::Assumptions::findExprs(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), getAssumptionsAndCongRec(), getAssumptionsRec(), CVC3::VCL::getAssumptionsRec(), CVC3::Theorem3::getAssumptionsRef(), CVC3::SearchImplBase::getAssumptionsUsed(), GetSatAssumptions(), GetSatAssumptionsRec(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::implIntro(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), print(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), recursivePrint(), CVC3::UFTheoremProducer::relToClosure(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducerOld::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 402 of file theorem.cpp.

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

Referenced by CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::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::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::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::SearchImplBase::getProof(), CVC3::SearchSat::getProof(), CVC3::Theorem3::getProof(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), print(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::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::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducerOld::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
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::SearchEngineFast::addLiteralFact(), CVC3::CommonTheoremProducer::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryQuant::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::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::ClauseValue::ClauseValue(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::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::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), print(), processNode(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::TheoryArithNew::propagateTheory(), CVC3::ExprTransform::pushNegationRec(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducerOld::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 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 std::endl(), and toString().

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(), CVC3::TheoremValue::setSubst(), and thm().

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(), CVC3::TheoremValue::isSubst(), and thm().

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 CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremManager::setLitFlag(), CVC3::TheoremValue::setLitFlag(), and thm().

bool CVC3::Theorem::getLitFlag ( ) const

Check the "literal" attribute.

The expression of this theorem will be added as a conflict clause literal

Definition at line 476 of file theorem.cpp.

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

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 
)
inlinestatic

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

intptr_t CVC3::Theorem::d_thm

Definition at line 91 of file theorem.h.

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

ExprValue* CVC3::Theorem::d_expr
union { ... }

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