CVC3 2.2
|
#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::d_expr, CVC3::TheoremValue::d_refcount, DebugAssert, CVC3::TheoremManager::getMM(), CVC3::TheoremManager::getRWMM(), CVC3::ExprValue::incRefcount(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), 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::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 | ( | const Theorem & | th | ) |
Definition at line 170 of file theorem.cpp.
References CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, exprValue(), CVC3::ExprValue::incRefcount(), CVC3::int2string(), and thm().
CVC3::Theorem::~Theorem | ( | ) |
Definition at line 188 of file theorem.cpp.
References CVC3::TheoremValue::d_refcount, d_thm, CVC3::ExprValue::decRefcount(), CVC3::MemoryManager::deleteData(), exprValue(), FatalAssert, CVC3::TheoremValue::getMM(), IF_DEBUG, CVC3::int2string(), and thm().
void CVC3::Theorem::recursivePrint | ( | int & | i | ) | const [private] |
Definition at line 516 of file theorem.cpp.
References CVC3::Assumptions::begin(), CVC3::Assumptions::end(), std::endl(), getAssumptionsRef(), getCachedValue(), getExpr(), getScope(), isAssump(), isSubst(), and setCachedValue().
void CVC3::Theorem::getAssumptionsRec | ( | std::set< Expr > & | assumptions | ) | const [private] |
Definition at line 259 of file theorem.cpp.
References CVC3::Assumptions::begin(), CVC3::Assumptions::end(), getAssumptionsRef(), getExpr(), isAssump(), isFlagged(), isRefl(), and setFlag().
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 CVC3::Assumptions::begin(), CVC3::Assumptions::end(), getAssumptionsAndCongRec(), getAssumptionsRef(), getExpr(), getLHS(), getRHS(), isAssump(), CVC3::Expr::isAtomic(), CVC3::Expr::isAtomicFormula(), isFlagged(), isRefl(), isRewrite(), isSubst(), CVC3::Expr::isTerm(), CVC3::OR, setFlag(), CVC3::Assumptions::size(), and thm().
Referenced by getAssumptionsAndCong(), and getAssumptionsAndCongRec().
void CVC3::Theorem::GetSatAssumptionsRec | ( | std::vector< Theorem > & | assumptions | ) | const [private] |
Definition at line 288 of file theorem.cpp.
References CVC3::Assumptions::begin(), DebugAssert, CVC3::Assumptions::end(), getAssumptionsRef(), getExpr(), CVC3::Expr::isAbsLiteral(), isAssump(), isFlagged(), CVC3::Expr::isNot(), isRefl(), CVC3::Expr::isRegisteredAtom(), and setFlag().
ExprValue* CVC3::Theorem::exprValue | ( | ) | const [inline, private] |
Definition at line 132 of file theorem.h.
Referenced by clearAllFlags(), getCachedValue(), getExpandFlag(), getExpr(), getLitFlag(), getProof(), isFlagged(), operator=(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), Theorem(), withAssumptions(), withProof(), and ~Theorem().
TheoremValue* CVC3::Theorem::thm | ( | ) | const [inline, private] |
Definition at line 133 of file theorem.h.
Referenced by clearAllFlags(), getAssumptionsAndCongRec(), getAssumptionsRef(), getCachedValue(), getExpandFlag(), getExpr(), getLHS(), getLitFlag(), getProof(), getQuantLevel(), getQuantLevelDebug(), getRHS(), getScope(), isAssump(), isFlagged(), isRewrite(), isSubst(), print(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), setSubst(), Theorem(), withAssumptions(), withProof(), and ~Theorem().
void CVC3::Theorem::printDebug | ( | ) | const [inline] |
Definition at line 140 of file theorem.h.
Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theorem3::printDebug(), and CVC3::SearchEngineFast::traceConflict().
Definition at line 91 of file theorem.cpp.
References CVC3::TheoremValue::d_refcount, d_thm, DebugAssert, CVC3::MemoryManager::deleteData(), exprValue(), CVC3::TheoremValue::getMM(), and CVC3::ExprValue::incRefcount().
bool CVC3::Theorem::withProof | ( | ) | const |
Definition at line 214 of file theorem.cpp.
References CVC3::ExprValue::d_em, CVC3::TheoremValue::d_tm, exprValue(), CVC3::ExprManager::getTM(), isRefl(), thm(), and CVC3::TheoremManager::withProof().
Referenced by getProof(), print(), and CVC3::Theorem3::withProof().
bool CVC3::Theorem::withAssumptions | ( | ) | const |
Definition at line 219 of file theorem.cpp.
References CVC3::ExprValue::d_em, CVC3::TheoremValue::d_tm, exprValue(), CVC3::ExprManager::getTM(), isRefl(), thm(), and CVC3::TheoremManager::withAssumptions().
Referenced by print(), and CVC3::Theorem3::withAssumptions().
bool CVC3::Theorem::isNull | ( | ) | const [inline] |
Definition at line 164 of file theorem.h.
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryCore::buildModel(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::checkSat(), clearAllFlags(), CVC3::compare(), CVC3::TheoryArithOld::computeTermBounds(), MiniSat::Derivation::createProof(), CVC3::TheoryArith3::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), generateSatProof(), getAssumptionsAndCong(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRef(), CVC3::VCL::getAssumptionsUsed(), CVC3::SearchImplBase::getAssumptionsUsed(), getCachedValue(), CVC3::SearchSat::getCounterExample(), CVC3::SearchImplBase::getCounterExample(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), getExpandFlag(), getExpr(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), getLeafAssumptions(), getLHS(), getLitFlag(), getProof(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::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::TheoryArithOld::isInteger(), CVC3::TheoryArithNew::isInteger(), CVC3::TheoryArith3::isInteger(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArith3::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::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::operator<<(), print(), printSatProof(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::Circuit::propagate(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::SearchImplBase::replaceITE(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::Theory::rewriteCC(), SAT::SatProofNode::SatProofNode(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), setSubst(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::simplifyOp(), TheoremEq(), TheoremEq(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and CVC3::Theory::updateCC().
bool CVC3::Theorem::isRewrite | ( | ) | const |
Definition at line 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::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::compare(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchImplBase::findInCNFCache(), CVC3::BitvectorTheoremProducer::generalIneqn(), getAssumptionsAndCongRec(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::Theorem3::isRewrite(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryCore::processUpdates(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArray::renameExpr(), CVC3::SearchImplBase::replaceITE(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryDatatype::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), and CVC3::CommonTheoremProducer::transitivityRule().
bool CVC3::Theorem::isAssump | ( | ) | const |
Definition at line 395 of file theorem.cpp.
References DebugAssert, CVC3::TheoremValue::isAssump(), isNull(), isRefl(), and thm().
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryQuant::findInstAssumptions(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), GetSatAssumptionsRec(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::Theorem3::isAssump(), CVC3::SearchEngineFast::newIntAssumption(), print(), and recursivePrint().
bool CVC3::Theorem::isRefl | ( | ) | const [inline] |
Definition at line 171 of file theorem.h.
Referenced by CVC3::TheoryArray::checkSat(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), clearAllFlags(), CVC3::Theory::find(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Theory::findReduce(), getAssumptionsAndCong(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), getAssumptionsRef(), getCachedValue(), getExpandFlag(), getExpr(), getLeafAssumptions(), getLHS(), getLitFlag(), getProof(), getQuantLevel(), getQuantLevelDebug(), getRHS(), GetSatAssumptions(), GetSatAssumptionsRec(), getScope(), isAssump(), isFlagged(), isRewrite(), isSubst(), CVC3::ExprTransform::newPPrec(), CVC3::ExprTransform::preprocess(), print(), CVC3::TheoryBitvector::pushNegationRec(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), setQuantLevel(), setSubst(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::TheoryArray::update(), withAssumptions(), and withProof().
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::TheoryCore::addFact(), CVC3::SearchImplBase::addFact(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::SearchSat::addLemma(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::SearchImplBase::addToCNFCache(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::CommonTheoremProducer::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryCore::checkEquation(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryCore::checkSolved(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::Circuit::Circuit(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ClauseValue::ClauseValue(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::compare(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::SearchEngineFast::enqueueFact(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::SearchImplBase::findInCNFCache(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::SearchEngineFast::fixConflict(), CVC3::TheoryBitvector::generalBitBlast(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), CVC3::Theorem3::getExpr(), CVC3::SearchSat::getImplication(), CVC3::VCL::getImpliedLiteral(), CVC3::SearchSat::getImpliedLiteral(), CVC3::TheoryArithNew::getLowerBoundExplanation(), GetSatAssumptionsRec(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implMP(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), isAbsLiteral(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArith3::isStale(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::operator<<(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::pivotRule(), pprintx(), pprintxnodag(), CVC3::ExprTransform::preprocess(), print(), printx(), printxnodag(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArith3::processBuffer(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), processNode(), CVC3::TheoryArithOld::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::DecisionEngine::pushDecision(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryQuant::recInstantiate(), CVC3::SearchEngineFast::recordFact(), 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::TheoryCore::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArray::solve(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), TheoremEq(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::SearchEngineFast::traceConflict(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExpr(), CVC3::VCL::tryModelGeneration(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::SearchEngineFast::unitPropagation(), CVC3::QuantTheoremProducer::universalInst(), CVC3::TheoryQuant::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and CVC3::TheoryArith3::update().
const Expr & CVC3::Theorem::getLHS | ( | ) | const |
Definition at line 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::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::compare(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::Theory::find(), CVC3::SearchImplBase::findInCNFCache(), CVC3::Theory::findRef(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::BitvectorTheoremProducer::generalIneqn(), getAssumptionsAndCongRec(), CVC3::Theorem3::getLHS(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryCore::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryDatatype::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryQuant::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::Theory::updateHelper(), and CVC3::TheoryBitvector::updateSubterms().
const Expr & CVC3::Theorem::getRHS | ( | ) | const |
Definition at line 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::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArith::canonThm(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::compare(), CVC3::TheoryBitvector::comparebv(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::Theory::computeTCC(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::TheoryQuant::debug(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryQuant::enqueueInst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::Theory::find(), CVC3::Theory::findExpr(), CVC3::Theory::findReduced(), CVC3::Theory::findRef(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::BitvectorTheoremProducer::generalIneqn(), getAssumptionsAndCongRec(), CVC3::Theorem3::getRHS(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::Theory::leavesAreSimp(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::multMatchChild(), CVC3::ExprTransform::newPP(), CVC3::ExprTransform::newPPrec(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::ExprTransform::preprocess(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryArray::renameExpr(), CVC3::SearchImplBase::replaceITE(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryUF::rewrite(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryRecords::setup(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryCore::simplify(), CVC3::Theory::simplifyExpr(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::VCL::simplifyThm(), CVC3::TheoryDatatype::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::SearchEngineFast::split(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::TheoryQuant::synNewInst(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryQuant::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::Theory::updateCC(), CVC3::Theory::updateHelper(), and CVC3::TheoryBitvector::updateSubterms().
void CVC3::Theorem::GetSatAssumptions | ( | std::vector< Theorem > & | assumptions | ) | const |
Definition at line 309 of file theorem.cpp.
References CVC3::Assumptions::begin(), DebugAssert, CVC3::Assumptions::end(), getAssumptionsRef(), isFlagged(), isRefl(), and setFlag().
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 clearAllFlags(), getAssumptionsRec(), isNull(), and isRefl().
Referenced by CVC3::TheoryCore::buildModel(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::VCL::getAssumptionsUsed(), CVC3::SearchEngine::getConcreteModel(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryCore::refineCounterExample(), 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 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::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), CVC3::Theorem3::getAssumptionsRef(), CVC3::SearchImplBase::getAssumptionsUsed(), GetSatAssumptions(), GetSatAssumptionsRec(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::implIntro(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), print(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), recursivePrint(), CVC3::UFTheoremProducer::relToClosure(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::SearchEngineFast::traceConflict(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::SearchEngineTheoremProducer::verifyConflict().
Proof CVC3::Theorem::getProof | ( | ) | const |
Definition at line 402 of file theorem.cpp.
References DebugAssert, exprValue(), CVC3::TheoremValue::getProof(), isNull(), isRefl(), CVC3::PF_APPLY, thm(), and withProof().
Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CommonTheoremProducer::andElim(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::CNF_TheoremProducer::CNFAddUnit(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer3::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer3::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer3::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer3::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), generateSatProof(), CVC3::Theorem3::getProof(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::getProof(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), print(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::SearchEngineTheoremProducer::unitProp(), and CVC3::QuantTheoremProducer::universalInst().
int CVC3::Theorem::getScope | ( | ) | const |
Definition at line 486 of file theorem.cpp.
References DebugAssert, CVC3::TheoremValue::getScope(), isNull(), isRefl(), and thm().
Referenced by CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theorem3::getScope(), print(), CVC3::SearchEngineFast::recordFact(), recursivePrint(), CVC3::Literal::setValue(), CVC3::Variable::setValue(), and CVC3::SearchEngineFast::traceConflict().
unsigned CVC3::Theorem::getQuantLevel | ( | ) | const |
Return quantification level for this theorem.
Definition at line 491 of file theorem.cpp.
References DebugAssert, CVC3::TheoremValue::getQuantLevel(), isNull(), isRefl(), thm(), and CVC3::TRACE.
Referenced by CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryCore::setupTerm(), and CVC3::QuantTheoremProducer::universalInst().
unsigned CVC3::Theorem::getQuantLevelDebug | ( | ) | const |
Definition at line 497 of file theorem.cpp.
References DebugAssert, CVC3::TheoremValue::getQuantLevelDebug(), isNull(), isRefl(), thm(), and CVC3::TRACE.
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(), CVC3::TheoremValue::setQuantLevel(), and thm().
Referenced by CVC3::SearchSat::assertLit(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::SearchImplBase::newIntAssumption(), CVC3::QuantTheoremProducer::partialUniversalInst(), and CVC3::QuantTheoremProducer::universalInst().
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::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::ClauseValue::ClauseValue(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::Variable::deriveThmRec(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::VCL::getAssumptionsRec(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implMP(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), print(), processNode(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::TheoryArithNew::propagateTheory(), CVC3::ExprTransform::pushNegationRec(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryArray::renameExpr(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::setupTerm(), CVC3::VariableValue::setValue(), 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 |
Check if the flag attribute is set.
Definition at line 416 of file theorem.cpp.
References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), CVC3::TheoremValue::isFlagged(), CVC3::TheoremManager::isFlagged(), isNull(), isRefl(), and thm().
Referenced by CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryQuant::findInstAssumptions(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), GetSatAssumptions(), GetSatAssumptionsRec(), and processNode().
void CVC3::Theorem::clearAllFlags | ( | ) | const |
Clear the flag attribute in all the theorems.
Definition at line 422 of file theorem.cpp.
References CVC3::TheoremValue::clearAllFlags(), CVC3::TheoremManager::clearAllFlags(), CVC3::ExprValue::d_em, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().
Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), getAssumptionsAndCong(), getLeafAssumptions(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::Assumptions::operator[](), and CVC3::SearchEngineFast::traceConflict().
void CVC3::Theorem::setFlag | ( | ) | const |
Set the flag attribute.
Definition at line 429 of file theorem.cpp.
References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setFlag(), CVC3::TheoremManager::setFlag(), and thm().
Referenced by CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Assumptions::findTheorem(), getAssumptionsAndCongRec(), CVC3::VCL::getAssumptionsRec(), getAssumptionsRec(), GetSatAssumptions(), GetSatAssumptionsRec(), and processNode().
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 |
Set the "expand" attribute.
Definition at line 458 of file theorem.cpp.
References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setExpandFlag(), CVC3::TheoremManager::setExpandFlag(), and thm().
Referenced by CVC3::SearchEngineFast::traceConflict().
bool CVC3::Theorem::getExpandFlag | ( | ) | const |
Check the "expand" attribute.
Definition at line 464 of file theorem.cpp.
References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::TheoremValue::getExpandFlag(), CVC3::TheoremManager::getExpandFlag(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().
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 CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setLitFlag(), CVC3::TheoremManager::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::TheoremValue::getLitFlag(), CVC3::TheoremManager::getLitFlag(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().
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::SearchImplBase::addCNFFact(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::enqueueFact(), CVC3::Theorem3::isAbsLiteral(), processNode(), and CVC3::SearchEngineFast::unitPropagation().
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::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), and CVC3::SearchEngineTheoremProducer::propIterThen().
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::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), and CVC3::SearchEngineTheoremProducer::propIterThen().
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 CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), CVC3::TheoremValue::setCachedValue(), CVC3::TheoremManager::setCachedValue(), and thm().
Referenced by processNode(), recursivePrint(), and CVC3::SearchEngineFast::traceConflict().
int CVC3::Theorem::getCachedValue | ( | ) | const |
Check if the flag attribute is set.
Definition at line 441 of file theorem.cpp.
References CVC3::ExprValue::d_em, d_expr, DebugAssert, exprValue(), CVC3::TheoremValue::getCachedValue(), CVC3::TheoremManager::getCachedValue(), CVC3::ExprManager::getTM(), isNull(), isRefl(), and thm().
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 CVC3::TheoremValue::d_refcount, getAssumptionsRef(), CVC3::Expr::getEM(), getExpr(), getProof(), getScope(), CVC3::ExprManager::incIndent(), CVC3::ExprManager::indent(), CVC3::ExprManager::isActive(), isAssump(), isNull(), isRefl(), thm(), withAssumptions(), and withProof().
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(), hash(), operator=(), Theorem(), and ~Theorem().
Definition at line 92 of file theorem.h.
Referenced by getCachedValue(), getExpandFlag(), getLHS(), getLitFlag(), getRHS(), isFlagged(), setCachedValue(), setExpandFlag(), setFlag(), setLitFlag(), and Theorem().
union { ... } [private] |