CVC3::TheoremProducer

CVC3::TheoremProducer Class Reference

#include <theorem_producer.h>

Inheritance diagram for CVC3::TheoremProducer:

Inheritance graph
[legend]
Collaboration diagram for CVC3::TheoremProducer:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Definition at line 91 of file theorem_producer.h.

Constructor & Destructor Documentation

TheoremProducer::TheoremProducer ( TheoremManager *  tm  ) 

Definition at line 44 of file theorem_producer.cpp.

References d_em, d_hole, CVC3::ExprManager::newLeafExpr(), and CVC3::PF_HOLE.

virtual CVC3::TheoremProducer::~TheoremProducer (  )  [inline, virtual]

Definition at line 156 of file theorem_producer.h.

Member Function Documentation

Theorem CVC3::TheoremProducer::newTheorem ( const Expr &  thm,
const Assumptions &  assump,
const Proof &  pf 
) [inline, protected]

Create a new theorem. See also newRWTheorem() and newReflTheorem().

Definition at line 107 of file theorem_producer.h.

References CVC3::Debug::counter(), d_tm, CVC3::debugger, IF_DEBUG, CVC3::Expr::isEq(), CVC3::Expr::isIff(), and CVC3::TRACE.

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::QuantTheoremProducer::addNewConst(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::andIntro(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), 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::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::DatatypeTheoremProducer::dummyTheorem(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), 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::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::CoreTheoremProducer::typePred(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::CommonTheoremProducer::varIntroRule().

Theorem CVC3::TheoremProducer::newRWTheorem ( const Expr &  lhs,
const Expr &  rhs,
const Assumptions &  assump,
const Proof &  pf 
) [inline, protected]

Create a rewrite theorem: lhs = rhs.

Definition at line 118 of file theorem_producer.h.

References d_tm.

Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::BitvectorTheoremProducer::andZero(), CVC3::UFTheoremProducer::applyLambda(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractSXRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducerOld::canonInvertLeaf(), CVC3::ArithTheoremProducer::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultOne(), CVC3::ArithTheoremProducer::canonMultOne(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducer::canonMultTermConst(), CVC3::ArithTheoremProducerOld::canonMultZero(), CVC3::ArithTheoremProducer::canonMultZero(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::ArithTheoremProducerOld::canonUMinusToDivide(), CVC3::ArithTheoremProducer::canonUMinusToDivide(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::ArithTheoremProducerOld::dummyTheorem(), CVC3::ArithTheoremProducer::dummyTheorem(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandRecord(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::RecordsTheoremProducer::expandTuple(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::ArithTheoremProducerOld::flipInequality(), CVC3::ArithTheoremProducer::flipInequality(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::ArithTheoremProducerOld::minusToPlus(), CVC3::ArithTheoremProducer::minusToPlus(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::orOne(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteImplies(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::RecordsTheoremProducer::rewriteLitSelect(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CoreTheoremProducer::rewriteNotIte(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::RecordsTheoremProducer::rewriteUpdateSelect(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rewriteXOR(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::ArithTheoremProducerOld::trustedRewrite(), CVC3::ArithTheoremProducer::trustedRewrite(), CVC3::ArithTheoremProducerOld::uMinusToMult(), CVC3::ArithTheoremProducer::uMinusToMult(), CVC3::ArithTheoremProducerOld::varToMult(), CVC3::ArithTheoremProducer::varToMult(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

Theorem CVC3::TheoremProducer::newReflTheorem ( const Expr &  e  )  [inline, protected]

Create a reflexivity theorem.

Definition at line 125 of file theorem_producer.h.

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

Theorem CVC3::TheoremProducer::newAssumption ( const Expr &  thm,
const Proof &  pf,
int  scope = -1 
) [inline, protected]

Definition at line 129 of file theorem_producer.h.

References d_tm, and CVC3::Assumptions::emptyAssump().

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

Theorem3 CVC3::TheoremProducer::newTheorem3 ( const Expr &  thm,
const Assumptions &  assump,
const Proof &  pf 
) [inline, protected]

Definition at line 133 of file theorem_producer.h.

References CVC3::Debug::counter(), d_tm, CVC3::debugger, IF_DEBUG, CVC3::Expr::isEq(), CVC3::Expr::isIff(), and CVC3::TRACE.

Referenced by CVC3::CommonTheoremProducer::implIntro3(), and CVC3::CommonTheoremProducer::queryTCC().

Theorem3 CVC3::TheoremProducer::newRWTheorem3 ( const Expr &  lhs,
const Expr &  rhs,
const Assumptions &  assump,
const Proof &  pf 
) [inline, protected]

Definition at line 143 of file theorem_producer.h.

References d_tm.

void TheoremProducer::soundError ( const std::string &  file,
int  line,
const std::string &  cond,
const std::string &  msg 
) [protected]

Definition at line 33 of file theorem_producer.cpp.

bool CVC3::TheoremProducer::withProof (  )  [inline]

Testing whether to generate proofs.

Definition at line 159 of file theorem_producer.h.

References d_tm, and CVC3::TheoremManager::withProof().

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::QuantTheoremProducer::addNewConst(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::andIntro(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::BitvectorTheoremProducer::andZero(), CVC3::UFTheoremProducer::applyLambda(), CVC3::CommonTheoremProducer::assumpRule(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractSXRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducerOld::canonInvertLeaf(), CVC3::ArithTheoremProducer::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultOne(), CVC3::ArithTheoremProducer::canonMultOne(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducer::canonMultTermConst(), CVC3::ArithTheoremProducerOld::canonMultZero(), CVC3::ArithTheoremProducer::canonMultZero(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::ArithTheoremProducerOld::canonUMinusToDivide(), CVC3::ArithTheoremProducer::canonUMinusToDivide(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::RecordsTheoremProducer::expandRecord(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::RecordsTheoremProducer::expandTuple(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::ArithTheoremProducerOld::flipInequality(), CVC3::ArithTheoremProducer::flipInequality(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::ArithTheoremProducerOld::minusToPlus(), CVC3::ArithTheoremProducer::minusToPlus(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::orOne(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::QuantTheoremProducer::packVar(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), 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::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteImplies(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::RecordsTheoremProducer::rewriteLitSelect(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CoreTheoremProducer::rewriteNotIte(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::RecordsTheoremProducer::rewriteUpdateSelect(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rewriteXOR(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::ArithTheoremProducerOld::trustedRewrite(), CVC3::ArithTheoremProducer::trustedRewrite(), CVC3::CoreTheoremProducer::typePred(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::ArithTheoremProducerOld::uMinusToMult(), CVC3::ArithTheoremProducer::uMinusToMult(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::QuantTheoremProducer::universalInst(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::ArithTheoremProducerOld::varToMult(), CVC3::ArithTheoremProducer::varToMult(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

bool CVC3::TheoremProducer::withAssumptions (  )  [inline]

Testing whether to generate assumptions.

Definition at line 162 of file theorem_producer.h.

References d_tm, and CVC3::TheoremManager::withAssumptions().

Referenced by CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::CoreTheoremProducer::rewriteIteElse(), and CVC3::CoreTheoremProducer::rewriteIteThen().

Proof TheoremProducer::newLabel ( const Expr &  e  ) 

Create a new proof label (bound variable) for an assumption (formula).

Definition at line 52 of file theorem_producer.cpp.

References d_tm, CVC3::TheoremManager::getEM(), and CVC3::ExprManager::newBoundVarExpr().

Referenced by CVC3::CommonTheoremProducer::assumpRule(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::CommonTheoremProducer::skolemizeRewrite(), and CVC3::CommonTheoremProducer::skolemizeRewriteVar().

Proof TheoremProducer::newPf ( const std::string &  name  ) 

Definition at line 66 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::QuantTheoremProducer::addNewConst(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::andIntro(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::BitvectorTheoremProducer::andZero(), CVC3::UFTheoremProducer::applyLambda(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractSXRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducerOld::canonInvertLeaf(), CVC3::ArithTheoremProducer::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultOne(), CVC3::ArithTheoremProducer::canonMultOne(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducer::canonMultTermConst(), CVC3::ArithTheoremProducerOld::canonMultZero(), CVC3::ArithTheoremProducer::canonMultZero(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::ArithTheoremProducerOld::canonUMinusToDivide(), CVC3::ArithTheoremProducer::canonUMinusToDivide(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducerOld::equalLeaves1(), CVC3::ArithTheoremProducer::equalLeaves1(), CVC3::ArithTheoremProducerOld::equalLeaves2(), CVC3::ArithTheoremProducer::equalLeaves2(), CVC3::ArithTheoremProducerOld::equalLeaves3(), CVC3::ArithTheoremProducer::equalLeaves3(), CVC3::ArithTheoremProducerOld::equalLeaves4(), CVC3::ArithTheoremProducer::equalLeaves4(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::RecordsTheoremProducer::expandRecord(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::RecordsTheoremProducer::expandTuple(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::ArithTheoremProducerOld::flipInequality(), CVC3::ArithTheoremProducer::flipInequality(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::ArithTheoremProducerOld::minusToPlus(), CVC3::ArithTheoremProducer::minusToPlus(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::orOne(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::QuantTheoremProducer::packVar(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), 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::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteImplies(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::RecordsTheoremProducer::rewriteLitSelect(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CoreTheoremProducer::rewriteNotIte(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::RecordsTheoremProducer::rewriteUpdateSelect(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rewriteXOR(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::ArithTheoremProducerOld::trustedRewrite(), CVC3::ArithTheoremProducer::trustedRewrite(), CVC3::CoreTheoremProducer::typePred(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::ArithTheoremProducerOld::uMinusToMult(), CVC3::ArithTheoremProducer::uMinusToMult(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::QuantTheoremProducer::universalInst(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::ArithTheoremProducerOld::varToMult(), CVC3::ArithTheoremProducer::varToMult(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e 
)

Definition at line 70 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Proof &  pf 
)

Definition at line 74 of file theorem_producer.cpp.

References d_em, d_pfOp, CVC3::Proof::getExpr(), and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e1,
const Expr &  e2 
)

Definition at line 78 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e,
const Proof &  pf 
)

Definition at line 83 of file theorem_producer.cpp.

References d_em, d_pfOp, CVC3::Proof::getExpr(), and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e1,
const Expr &  e2,
const Expr &  e3 
)

Definition at line 88 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e1,
const Expr &  e2,
const Proof &  pf 
)

Definition at line 99 of file theorem_producer.cpp.

References d_em, d_pfOp, CVC3::Proof::getExpr(), and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
Expr::iterator  begin,
const Expr::iterator &  end 
)

Definition at line 110 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e,
Expr::iterator  begin,
const Expr::iterator &  end 
)

Definition at line 120 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
Expr::iterator  begin,
const Expr::iterator &  end,
const std::vector< Proof > &  pfs 
)

Definition at line 130 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const std::vector< Expr > &  args 
)

Definition at line 143 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e,
const std::vector< Expr > &  args 
)

Definition at line 152 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e,
const std::vector< Proof > &  pfs 
)

Definition at line 163 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const Expr &  e1,
const Expr &  e2,
const std::vector< Proof > &  pfs 
)

Definition at line 176 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const std::vector< Proof > &  pfs 
)

Definition at line 190 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const std::vector< Expr > &  args,
const Proof &  pf 
)

Definition at line 201 of file theorem_producer.cpp.

References d_em, d_pfOp, CVC3::Proof::getExpr(), and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const std::string &  name,
const std::vector< Expr > &  args,
const std::vector< Proof > &  pfs 
)

Definition at line 212 of file theorem_producer.cpp.

References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().

Proof TheoremProducer::newPf ( const Proof &  label,
const Expr &  frm,
const Proof &  pf 
)

Creating LAMBDA-abstraction (LAMBDA label formula proof).

The label must be a variable with a formula as a type, and matching the given "frm".

Definition at line 225 of file theorem_producer.cpp.

References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), IF_DEBUG, CVC3::LAMBDA, and CVC3::ExprManager::newClosureExpr().

Proof TheoremProducer::newPf ( const Proof &  label,
const Proof &  pf 
)

Creating LAMBDA-abstraction (LAMBDA label proof).

The label must be a variable with a formula as a type.

Definition at line 238 of file theorem_producer.cpp.

References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), CVC3::LAMBDA, and CVC3::ExprManager::newClosureExpr().

Proof TheoremProducer::newPf ( const std::vector< Proof > &  labels,
const std::vector< Expr > &  frms,
const Proof &  pf 
)

Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf).

Definition at line 249 of file theorem_producer.cpp.

References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), IF_DEBUG, CVC3::LAMBDA, and CVC3::ExprManager::newClosureExpr().

Proof TheoremProducer::newPf ( const std::vector< Proof > &  labels,
const Proof &  pf 
)

Definition at line 269 of file theorem_producer.cpp.

References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), CVC3::LAMBDA, and CVC3::ExprManager::newClosureExpr().

Member Data Documentation

TheoremManager* CVC3::TheoremProducer::d_tm [protected]

Definition at line 94 of file theorem_producer.h.

Referenced by newAssumption(), newLabel(), newPf(), newRWTheorem(), newRWTheorem3(), newTheorem(), newTheorem3(), CVC3::CommonTheoremProducer::substitutivityRule(), withAssumptions(), and withProof().

ExprManager* CVC3::TheoremProducer::d_em [protected]

Definition at line 95 of file theorem_producer.h.

Referenced by CVC3::CommonTheoremProducer::andElim(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::ArithTheoremProducerOld::dummyTheorem(), CVC3::ArithTheoremProducer::dummyTheorem(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), newPf(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::BitvectorTheoremProducer::rat(), CVC3::ArithTheoremProducerOld::rat(), CVC3::ArithTheoremProducer::rat(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::CommonTheoremProducer::rewriteReflexivity(), TheoremProducer(), CVC3::CommonTheoremProducer::trueTheorem(), and CVC3::CommonTheoremProducer::varIntroRule().

const bool* CVC3::TheoremProducer::d_checkProofs [protected]

Definition at line 98 of file theorem_producer.h.

Op CVC3::TheoremProducer::d_pfOp [protected]

Definition at line 100 of file theorem_producer.h.

Referenced by newPf().

Expr CVC3::TheoremProducer::d_hole [protected]

Definition at line 102 of file theorem_producer.h.

Referenced by CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), and TheoremProducer().

The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:37:48 2007 for CVC3 by  doxygen 1.5.1