CVC3
2.4.1
|
#include <theorem.h>
Several attributes used in conflict analysis and assumptions graph traversals.
CVC3::Theorem::Theorem | ( | TheoremValue * | thm | ) | [inline, private] |
Constructor only used by TheoremValue for assumptions.
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 131 of file theorem.cpp.
References CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::Expr::d_expr, CVC3::ExprValue::incRefcount(), CVC3::TheoremManager::getRWMM(), CVC3::TheoremManager::getMM(), 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 152 of file theorem.cpp.
References CVC3::Expr::d_expr, CVC3::ExprValue::incRefcount(), CVC3::TheoremManager::getRWMM(), CVC3::TheoremValue::d_refcount, DebugAssert, and CVC3::Proof::isNull().
CVC3::Theorem::Theorem | ( | const Expr & | e | ) | [private] |
Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi.
Definition at line 182 of file theorem.cpp.
References d_expr, and CVC3::ExprValue::incRefcount().
CVC3::Theorem::Theorem | ( | const Theorem & | th | ) |
Definition at line 170 of file theorem.cpp.
References d_thm, DebugAssert, thm(), CVC3::int2string(), CVC3::TheoremValue::d_refcount, exprValue(), and CVC3::ExprValue::incRefcount().
CVC3::Theorem::~Theorem | ( | ) |
Definition at line 188 of file theorem.cpp.
References d_thm, thm(), IF_DEBUG, FatalAssert, CVC3::TheoremValue::d_refcount, CVC3::int2string(), CVC3::TheoremValue::getMM(), CVC3::MemoryManager::deleteData(), exprValue(), and CVC3::ExprValue::decRefcount().
void CVC3::Theorem::recursivePrint | ( | int & | i | ) | const [private] |
Definition at line 516 of file theorem.cpp.
References getAssumptionsRef(), CVC3::Assumptions::end(), CVC3::Assumptions::begin(), isAssump(), setCachedValue(), getCachedValue(), getScope(), std::endl(), getExpr(), and isSubst().
Definition at line 259 of file theorem.cpp.
References isRefl(), isFlagged(), setFlag(), isAssump(), getExpr(), getAssumptionsRef(), CVC3::Assumptions::begin(), and CVC3::Assumptions::end().
Referenced by getLeafAssumptions().
void CVC3::Theorem::getAssumptionsAndCongRec | ( | std::set< Expr > & | assumptions, |
std::vector< Expr > & | congruences | ||
) | const [private] |
Definition at line 320 of file theorem.cpp.
References isRefl(), isFlagged(), setFlag(), isAssump(), getExpr(), getAssumptionsRef(), isSubst(), CVC3::Assumptions::size(), thm(), CVC3::Assumptions::begin(), getAssumptionsAndCongRec(), isRewrite(), getLHS(), CVC3::Expr::isTerm(), CVC3::Expr::isAtomic(), getRHS(), CVC3::Expr::isAtomicFormula(), OR, and CVC3::Assumptions::end().
Referenced by getAssumptionsAndCongRec(), and getAssumptionsAndCong().
void CVC3::Theorem::GetSatAssumptionsRec | ( | std::vector< Theorem > & | assumptions | ) | const [private] |
Definition at line 288 of file theorem.cpp.
References DebugAssert, isRefl(), isFlagged(), setFlag(), getExpr(), CVC3::Expr::isAbsLiteral(), isAssump(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isNot(), getAssumptionsRef(), CVC3::Assumptions::begin(), and CVC3::Assumptions::end().
ExprValue* CVC3::Theorem::exprValue | ( | ) | const [inline, private] |
Definition at line 132 of file theorem.h.
Referenced by operator=(), Theorem(), ~Theorem(), withProof(), withAssumptions(), getExpr(), getProof(), isFlagged(), clearAllFlags(), setFlag(), setCachedValue(), getCachedValue(), setExpandFlag(), getExpandFlag(), setLitFlag(), and getLitFlag().
TheoremValue* CVC3::Theorem::thm | ( | ) | const [inline, private] |
Definition at line 133 of file theorem.h.
Referenced by Theorem(), ~Theorem(), withProof(), withAssumptions(), isRewrite(), getExpr(), getLHS(), getRHS(), getAssumptionsAndCongRec(), getAssumptionsRef(), isAssump(), getProof(), isFlagged(), clearAllFlags(), setFlag(), setCachedValue(), getCachedValue(), setSubst(), isSubst(), setExpandFlag(), getExpandFlag(), setLitFlag(), getLitFlag(), getScope(), getQuantLevel(), getQuantLevelDebug(), setQuantLevel(), and print().
void CVC3::Theorem::printDebug | ( | ) | const [inline] |
Definition at line 140 of file theorem.h.
Referenced by CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::traceConflict(), and CVC3::Theorem3::printDebug().
Definition at line 91 of file theorem.cpp.
References d_thm, DebugAssert, CVC3::TheoremValue::d_refcount, exprValue(), CVC3::ExprValue::incRefcount(), CVC3::TheoremValue::getMM(), and CVC3::MemoryManager::deleteData().
bool CVC3::Theorem::withProof | ( | ) | const |
Definition at line 214 of file theorem.cpp.
References isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::withProof(), thm(), and CVC3::TheoremValue::d_tm.
Referenced by getProof(), print(), and CVC3::Theorem3::withProof().
bool CVC3::Theorem::withAssumptions | ( | ) | const |
Definition at line 219 of file theorem.cpp.
References isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::withAssumptions(), thm(), and CVC3::TheoremValue::d_tm.
Referenced by print(), and CVC3::Theorem3::withAssumptions().
bool CVC3::Theorem::isNull | ( | ) | const [inline] |
Definition at line 164 of file theorem.h.
Referenced by CVC3::Assumptions::findTheorem(), CVC3::Circuit::propagate(), SAT::CNF_Manager::concreteThm(), SAT::CNF_Manager::translateExprRec(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::CommonTheoremProducer::implIntro(), generateSatProof(), printSatProof(), MiniSat::Derivation::createProof(), SAT::SatProofNode::SatProofNode(), SAT::SatProofNode::isLeaf(), TheoremEq(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchImplBase::getCounterExample(), CVC3::SearchImplBase::getProof(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchImplBase::processResult(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::replaceITE(), CVC3::SearchSat::getImplication(), CVC3::compare(), isRewrite(), getExpr(), getLHS(), getRHS(), getLeafAssumptions(), getAssumptionsAndCong(), getAssumptionsRef(), isAssump(), getProof(), isFlagged(), clearAllFlags(), setFlag(), setCachedValue(), getCachedValue(), setSubst(), isSubst(), setExpandFlag(), getExpandFlag(), setLitFlag(), getLitFlag(), getScope(), getQuantLevel(), getQuantLevelDebug(), setQuantLevel(), print(), TheoremEq(), CVC3::Theorem3::isNull(), CVC3::Theory::updateCC(), CVC3::Theory::rewriteCC(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArith3::isInteger(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryArithNew::isInteger(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheoryArithOld::isConstrained(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArray::update(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryCore::buildModel(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryDatatype::update(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryQuant::multMatchChild(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::TheoryRecords::setup(), CVC3::TheoryUF::checkSat(), CVC3::TheoryUF::update(), CVC3::operator<<(), CVC3::VCL::getAssumptionsRec(), CVC3::VCL::getImpliedLiteral(), and CVC3::VCL::getAssumptionsUsed().
bool CVC3::Theorem::isRewrite | ( | ) | const |
Definition at line 224 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), thm(), and CVC3::TheoremValue::isRewrite().
Referenced by CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ExprTransform::pushNegationRec(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchImplBase::replaceITE(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::compare(), getAssumptionsAndCongRec(), CVC3::Theorem3::isRewrite(), CVC3::Theory::renameExpr(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArith3::solve(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryBitvector::solve(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::solve(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryDatatype::assertFact(), and CVC3::TheoryDatatype::solve().
bool CVC3::Theorem::isAssump | ( | ) | const |
Definition at line 395 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), thm(), and CVC3::TheoremValue::isAssump().
Referenced by CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::implIntro(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), getAssumptionsRec(), GetSatAssumptionsRec(), getAssumptionsAndCongRec(), recursivePrint(), print(), CVC3::Theorem3::isAssump(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryQuant::findInstAssumptions(), and CVC3::VCL::getAssumptionsRec().
bool CVC3::Theorem::isRefl | ( | ) | const [inline] |
Definition at line 171 of file theorem.h.
Referenced by SAT::CNF_Manager::replaceITErec(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::ExprTransform::preprocess(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::newPPrec(), CVC3::ExprTransform::substitute(), CVC3::ExprTransform::simplifyWithCare(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), withProof(), withAssumptions(), isRewrite(), getExpr(), getLHS(), getRHS(), getAssumptionsRec(), getLeafAssumptions(), GetSatAssumptionsRec(), GetSatAssumptions(), getAssumptionsAndCongRec(), getAssumptionsAndCong(), getAssumptionsRef(), isAssump(), getProof(), isFlagged(), clearAllFlags(), setFlag(), setCachedValue(), getCachedValue(), setSubst(), isSubst(), setExpandFlag(), getExpandFlag(), setLitFlag(), getLitFlag(), getScope(), getQuantLevel(), getQuantLevelDebug(), setQuantLevel(), print(), CVC3::Theory::simplifyOp(), CVC3::Theory::find(), CVC3::Theory::findReduce(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArray::update(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::rewrite(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryQuant::findInstAssumptions(), and CVC3::VCL::getAssumptionsRec().
Expr CVC3::Theorem::getExpr | ( | ) | const |
Definition at line 230 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::Expr::isTerm(), CVC3::Expr::eqExpr(), CVC3::Expr::iffExpr(), thm(), and CVC3::TheoremValue::getExpr().
Referenced by CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::Circuit::Circuit(), CVC3::Circuit::propagate(), CVC3::ClauseValue::ClauseValue(), SAT::CNF_Manager::replaceITErec(), SAT::CNF_Manager::translateExpr(), SAT::CNF_Manager::addAssumption(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::implMP(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CommonTheoremProducer::skolemize(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::DecisionEngine::pushDecision(), CVC3::ExprTransform::preprocess(), CVC3::QuantTheoremProducer::universalInst(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchEngineFast::split(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::unitPropagation(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::enqueueFact(), TheoremEq(), processNode(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::addFact(), CVC3::SearchImplBase::processResult(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchImplBase::simplify(), CVC3::SearchSat::addLemma(), CVC3::SearchSat::getImplication(), CVC3::SearchSat::getImpliedLiteral(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchSimple::checkValidRec(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::compare(), printx(), printxnodag(), pprintx(), pprintxnodag(), getAssumptionsRec(), GetSatAssumptionsRec(), getAssumptionsAndCongRec(), isAbsLiteral(), recursivePrint(), print(), CVC3::Theorem3::getExpr(), CVC3::operator<<(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArith3::solvedForm(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArith3::processBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArith3::isStale(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArith3::update(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithNew::update(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArray::solve(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryBitvector::update(), CVC3::TheoryBitvector::solve(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::assertFact(), CVC3::TheoryCore::rewrite(), CVC3::TheoryCore::checkEquation(), CVC3::TheoryCore::checkSolved(), CVC3::TheoryCore::solve(), CVC3::TheoryCore::addFact(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryCore::setInconsistent(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryQuant::update(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::sendInstNew(), CVC3::CompleteInstPreProcessor::simplifyQuant(), CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryUF::assertFact(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::Variable::deriveThmRec(), CVC3::VariableValue::setValue(), CVC3::VCL::getAssumptionsRec(), CVC3::VCL::getImpliedLiteral(), and CVC3::VCL::tryModelGeneration().
const Expr & CVC3::Theorem::getLHS | ( | ) | const |
Definition at line 240 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), d_expr, thm(), and CVC3::TheoremValue::getLHS().
Referenced by CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::Expr::setFind(), CVC3::Expr::setEqNext(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::compare(), getAssumptionsAndCongRec(), CVC3::Theorem3::getLHS(), CVC3::Theory::findRef(), CVC3::Theory::find(), CVC3::Theory::updateHelper(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArith3::update(), CVC3::TheoryArith3::solve(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::update(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArray::update(), CVC3::TheoryArray::computeModel(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryBitvector::update(), CVC3::TheoryBitvector::updateSubterms(), CVC3::TheoryBitvector::solve(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::rewrite(), CVC3::TheoryCore::solve(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryDatatype::update(), CVC3::TheoryDatatype::solve(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryQuant::update(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryRecords::computeModel(), and CVC3::TheoryUF::computeModel().
const Expr & CVC3::Theorem::getRHS | ( | ) | const |
Definition at line 246 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), d_expr, thm(), and CVC3::TheoremValue::getRHS().
Referenced by CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::BitvectorTheoremProducer::bitExtractSXRule(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::BitvectorTheoremProducer::canonBVMult(), SAT::CNF_Manager::translateExprRec(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ExprTransform::preprocess(), CVC3::ExprTransform::pushNegationRec(), CVC3::ExprTransform::newPP(), CVC3::ExprTransform::newPPrec(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchEngineFast::split(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::replaceITE(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::compare(), getAssumptionsAndCongRec(), CVC3::Theorem3::getRHS(), CVC3::Theory::computeTCC(), CVC3::Theory::findRef(), CVC3::Theory::find(), CVC3::Theory::findReduced(), CVC3::Theory::updateHelper(), CVC3::Theory::updateCC(), CVC3::Theory::leavesAreSimp(), CVC3::Theory::renameExpr(), CVC3::Theory::simplifyExpr(), CVC3::Theory::findExpr(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArith::canonThm(), CVC3::TheoryArith3::canon(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArith3::update(), CVC3::TheoryArith3::solve(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithNew::update(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArray::update(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryBitvector::update(), CVC3::TheoryBitvector::updateSubterms(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::callTheoryPreprocess(), CVC3::TheoryCore::rewrite(), CVC3::TheoryCore::update(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryCore::getAssignment(), CVC3::TheoryCore::getValue(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryDatatype::update(), CVC3::TheoryDatatype::solve(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryQuant::debug(), CVC3::TheoryQuant::update(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::multMatchChild(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryRecords::setup(), CVC3::TheoryRecords::update(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::checkSat(), CVC3::TheoryUF::rewrite(), CVC3::TheoryUF::update(), CVC3::TheoryUF::computeModel(), CVC3::TheoryUF::computeTCC(), CVC3::Translator::preprocessRec(), and CVC3::VCL::simplifyThm().
void CVC3::Theorem::GetSatAssumptions | ( | std::vector< Theorem > & | assumptions | ) | const |
Definition at line 309 of file theorem.cpp.
References DebugAssert, isRefl(), isFlagged(), setFlag(), getAssumptionsRef(), CVC3::Assumptions::begin(), and CVC3::Assumptions::end().
Referenced by CVC3::CNF_TheoremProducer::getSmartClauses().
void CVC3::Theorem::getLeafAssumptions | ( | std::vector< Expr > & | assumptions, |
bool | negate = false |
||
) | const |
Definition at line 274 of file theorem.cpp.
References isNull(), isRefl(), clearAllFlags(), and getAssumptionsRec().
Referenced by CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::SearchEngine::getConcreteModel(), CVC3::SearchEngineFast::checkValidMain(), CVC3::TheoryCore::refineCounterExample(), CVC3::TheoryCore::buildModel(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::VCL::getAssumptionsUsed(), and CVC3::VCL::tryModelGeneration().
void CVC3::Theorem::getAssumptionsAndCong | ( | std::vector< Expr > & | assumptions, |
std::vector< Expr > & | congruences, | ||
bool | negate = false |
||
) | const |
Definition at line 370 of file theorem.cpp.
References isNull(), isRefl(), clearAllFlags(), and getAssumptionsAndCongRec().
const Assumptions & CVC3::Theorem::getAssumptionsRef | ( | ) | const |
Definition at line 385 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), thm(), CVC3::TheoremValue::getAssumptionsRef(), and CVC3::Assumptions::emptyAssump().
Referenced by CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::Assumptions::findTheorem(), CVC3::Assumptions::Assumptions(), CVC3::Assumptions::add(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::QuantTheoremProducer::universalInst(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::SearchEngineTheoremProducer::verifyConflict(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::SearchEngineTheoremProducer::opCNFRule(), getAssumptionsRec(), GetSatAssumptionsRec(), GetSatAssumptions(), getAssumptionsAndCongRec(), recursivePrint(), print(), CVC3::Theorem3::getAssumptionsRef(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::UFTheoremProducer::relToClosure(), and CVC3::VCL::getAssumptionsRec().
Proof CVC3::Theorem::getProof | ( | ) | const |
Definition at line 402 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), PF_APPLY, exprValue(), withProof(), thm(), and CVC3::TheoremValue::getProof().
Referenced by CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::implMP(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::DatatypeTheoremProducer::decompose(), generateSatProof(), CVC3::QuantTheoremProducer::universalInst(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchImplBase::getProof(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::SearchEngineTheoremProducer::opCNFRule(), print(), CVC3::Theorem3::getProof(), CVC3::UFTheoremProducer::relToClosure(), and CVC3::UFTheoremProducer::relTrans().
int CVC3::Theorem::getScope | ( | ) | const |
Definition at line 486 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), thm(), and CVC3::TheoremValue::getScope().
Referenced by CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchImplBase::enqueueCNFrec(), recursivePrint(), print(), CVC3::Theorem3::getScope(), CVC3::TheoryCore::enqueueFact(), CVC3::Variable::setValue(), and CVC3::Literal::setValue().
unsigned CVC3::Theorem::getQuantLevel | ( | ) | const |
Return quantification level for this theorem.
Definition at line 491 of file theorem.cpp.
References DebugAssert, isNull(), TRACE, isRefl(), thm(), and CVC3::TheoremValue::getQuantLevel().
Referenced by CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::QuantTheoremProducer::universalInst(), CVC3::QuantTheoremProducer::partialUniversalInst(), and CVC3::TheoryCore::setupTerm().
unsigned CVC3::Theorem::getQuantLevelDebug | ( | ) | const |
Definition at line 497 of file theorem.cpp.
References DebugAssert, isNull(), TRACE, isRefl(), thm(), and CVC3::TheoremValue::getQuantLevelDebug().
void CVC3::Theorem::setQuantLevel | ( | unsigned | level | ) |
Set the quantification level for this theorem.
Definition at line 504 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), thm(), and CVC3::TheoremValue::setQuantLevel().
Referenced by CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::QuantTheoremProducer::universalInst(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::SearchImplBase::newIntAssumption(), and CVC3::SearchSat::assertLit().
size_t CVC3::Theorem::hash | ( | ) | const |
Definition at line 511 of file theorem.cpp.
References d_thm.
Referenced by Hash::hash< CVC3::Theorem >::operator()().
std::string CVC3::Theorem::toString | ( | ) | const [inline] |
Definition at line 404 of file theorem.h.
Referenced by CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ClauseValue::ClauseValue(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::implMP(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::ExprTransform::pushNegationRec(), processNode(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchImplBase::processResult(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::SearchEngineTheoremProducer::conflictRule(), print(), CVC3::Theory::renameExpr(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assertFact(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryRecords::assertFact(), CVC3::Variable::deriveThmRec(), CVC3::VariableValue::setValue(), and CVC3::VCL::getAssumptionsRec().
void CVC3::Theorem::printx | ( | ) | const |
Definition at line 207 of file theorem.cpp.
References getExpr(), and CVC3::Expr::print().
Referenced by CVC3::Theorem3::printx().
void CVC3::Theorem::printxnodag | ( | ) | const |
Definition at line 208 of file theorem.cpp.
References getExpr(), and CVC3::Expr::printnodag().
void CVC3::Theorem::pprintx | ( | ) | const |
Definition at line 209 of file theorem.cpp.
References getExpr(), and CVC3::Expr::pprint().
void CVC3::Theorem::pprintxnodag | ( | ) | const |
Definition at line 210 of file theorem.cpp.
References getExpr(), and CVC3::Expr::pprintnodag().
void CVC3::Theorem::print | ( | ) | const |
Definition at line 211 of file theorem.cpp.
References toString(), and std::endl().
Referenced by CVC3::Theorem3::print().
bool CVC3::Theorem::isFlagged | ( | ) | const |
Check if the flag attribute is set.
Definition at line 416 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::isFlagged(), d_expr, thm(), and CVC3::TheoremValue::isFlagged().
Referenced by processNode(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), getAssumptionsRec(), GetSatAssumptionsRec(), GetSatAssumptions(), getAssumptionsAndCongRec(), CVC3::TheoryQuant::findInstAssumptions(), and CVC3::VCL::getAssumptionsRec().
void CVC3::Theorem::clearAllFlags | ( | ) | const |
Clear the flag attribute in all the theorems.
Definition at line 422 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::clearAllFlags(), thm(), and CVC3::TheoremValue::clearAllFlags().
Referenced by CVC3::Assumptions::operator[](), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), getLeafAssumptions(), and getAssumptionsAndCong().
void CVC3::Theorem::setFlag | ( | ) | const |
Set the flag attribute.
Definition at line 429 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::setFlag(), d_expr, thm(), and CVC3::TheoremValue::setFlag().
Referenced by CVC3::Assumptions::findTheorem(), processNode(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), getAssumptionsRec(), GetSatAssumptionsRec(), GetSatAssumptions(), getAssumptionsAndCongRec(), CVC3::TheoryQuant::findInstAssumptions(), and CVC3::VCL::getAssumptionsRec().
void CVC3::Theorem::setSubst | ( | ) | const |
Set flag stating that theorem is an instance of substitution.
Definition at line 447 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), thm(), and CVC3::TheoremValue::setSubst().
Referenced by CVC3::CommonTheoremProducer::substitutivityRule().
bool CVC3::Theorem::isSubst | ( | ) | const |
Is theorem an instance of substitution.
Definition at line 452 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), thm(), and CVC3::TheoremValue::isSubst().
Referenced by getAssumptionsAndCongRec(), and recursivePrint().
void CVC3::Theorem::setExpandFlag | ( | bool | val | ) | const |
Set the "expand" attribute.
Definition at line 458 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::setExpandFlag(), d_expr, thm(), and CVC3::TheoremValue::setExpandFlag().
Referenced by CVC3::SearchEngineFast::traceConflict().
bool CVC3::Theorem::getExpandFlag | ( | ) | const |
Check the "expand" attribute.
Definition at line 464 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::getExpandFlag(), d_expr, thm(), and CVC3::TheoremValue::getExpandFlag().
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 470 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::setLitFlag(), d_expr, thm(), and CVC3::TheoremValue::setLitFlag().
bool CVC3::Theorem::getLitFlag | ( | ) | const |
Check the "literal" attribute.
The expression of this theorem will be added as a conflict clause literal
Definition at line 476 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::getLitFlag(), d_expr, thm(), and CVC3::TheoremValue::getLitFlag().
Referenced by processNode().
bool CVC3::Theorem::isAbsLiteral | ( | ) | const |
Check if the theorem is a literal.
Definition at line 482 of file theorem.cpp.
References getExpr(), and CVC3::Expr::isAbsLiteral().
Referenced by CVC3::SearchEngineFast::unitPropagation(), CVC3::SearchEngineFast::enqueueFact(), processNode(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::Theorem3::isAbsLiteral().
bool CVC3::Theorem::refutes | ( | const Expr & | e | ) | const [inline] |
Check if the flag attribute is set.
Definition at line 252 of file theorem.h.
References CVC3::Expr::isNot().
Referenced by CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), and CVC3::SearchEngineTheoremProducer::confIterIfThen().
bool CVC3::Theorem::proves | ( | const Expr & | e | ) | const [inline] |
Check if the flag attribute is set.
Definition at line 259 of file theorem.h.
Referenced by CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), and CVC3::SearchEngineTheoremProducer::confIterIfThen().
bool CVC3::Theorem::matches | ( | const Expr & | e | ) | const [inline] |
void CVC3::Theorem::setCachedValue | ( | int | value | ) | const |
Check if the flag attribute is set.
Definition at line 435 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::setCachedValue(), d_expr, thm(), and CVC3::TheoremValue::setCachedValue().
Referenced by processNode(), CVC3::SearchEngineFast::traceConflict(), and recursivePrint().
int CVC3::Theorem::getCachedValue | ( | ) | const |
Check if the flag attribute is set.
Definition at line 441 of file theorem.cpp.
References DebugAssert, isNull(), isRefl(), exprValue(), CVC3::ExprValue::d_em, CVC3::ExprManager::getTM(), CVC3::TheoremManager::getCachedValue(), d_expr, thm(), and CVC3::TheoremValue::getCachedValue().
Referenced by processNode(), and recursivePrint().
ostream & CVC3::Theorem::print | ( | std::ostream & | os, |
const std::string & | name | ||
) | const |
Printing a theorem to a stream, calling it "name".
Definition at line 580 of file theorem.cpp.
References isNull(), getExpr(), CVC3::Expr::getEM(), isRefl(), withAssumptions(), CVC3::ExprManager::incIndent(), thm(), CVC3::TheoremValue::d_refcount, getScope(), isAssump(), CVC3::ExprManager::isActive(), getAssumptionsRef(), CVC3::ExprManager::indent(), withProof(), and getProof().
Definition at line 281 of file theorem.h.
References DebugAssert, and isNull().
friend class TheoremProducer [friend] |
friend class RegTheoremValue [friend] |
friend class RWTheoremValue [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.
Compare Theorems by TheoremValue pointers. Return -1, 0, or 1.
Definition at line 83 of file theorem.cpp.
std::ostream& operator<< | ( | std::ostream & | os, |
const Theorem & | t | ||
) | [friend] |
intptr_t CVC3::Theorem::d_thm |
Definition at line 91 of file theorem.h.
Referenced by CVC3::compare(), CVC3::compareByPtr(), operator=(), Theorem(), ~Theorem(), and hash().
Definition at line 92 of file theorem.h.
Referenced by Theorem(), getLHS(), getRHS(), isFlagged(), setFlag(), setCachedValue(), getCachedValue(), setExpandFlag(), getExpandFlag(), setLitFlag(), and getLitFlag().
union { ... } [private] |