CVC3  2.4.1
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
CVC3::TheoremProducer Class Reference

#include <theorem_producer.h>

Inheritance diagram for CVC3::TheoremProducer:
CVC3::ArithTheoremProducer CVC3::ArithTheoremProducer3 CVC3::ArithTheoremProducerOld CVC3::ArrayTheoremProducer CVC3::BitvectorTheoremProducer CVC3::CNF_TheoremProducer CVC3::CommonTheoremProducer CVC3::CoreTheoremProducer CVC3::DatatypeTheoremProducer CVC3::QuantTheoremProducer CVC3::RecordsTheoremProducer CVC3::SearchEngineTheoremProducer CVC3::SimulateTheoremProducer CVC3::UFTheoremProducer

Public Member Functions

 TheoremProducer (TheoremManager *tm)
 
virtual ~TheoremProducer ()
 
bool withProof ()
 Testing whether to generate proofs. More...
 
bool withAssumptions ()
 Testing whether to generate assumptions. More...
 
Proof newLabel (const Expr &e)
 Create a new proof label (bound variable) for an assumption (formula) More...
 
Proof newPf (const std::string &name)
 
Proof newPf (const std::string &name, const Expr &e)
 
Proof newPf (const std::string &name, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2)
 
Proof newPf (const std::string &name, const Expr &e, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)
 
Proof newPf (const Proof &label, const Expr &frm, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label formula proof) More...
 
Proof newPf (const Proof &label, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label proof). More...
 
Proof 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) More...
 
Proof newPf (const std::vector< Proof > &labels, const Proof &pf)
 

Protected Member Functions

Theorem newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
 Create a new theorem. See also newRWTheorem() and newReflTheorem() More...
 
Theorem newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 Create a rewrite theorem: lhs = rhs. More...
 
Theorem newReflTheorem (const Expr &e)
 Create a reflexivity theorem. More...
 
Theorem newAssumption (const Expr &thm, const Proof &pf, int scope=-1)
 
Theorem3 newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)
 
Theorem3 newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 
void soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)
 

Protected Attributes

TheoremManagerd_tm
 
ExprManagerd_em
 
const bool * d_checkProofs
 
Op d_pfOp
 
Expr d_hole
 

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 PF_HOLE.

virtual CVC3::TheoremProducer::~TheoremProducer ( )
inlinevirtual

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

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

Definition at line 107 of file theorem_producer.h.

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

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::andIntro(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::SearchEngineTheoremProducer::caseSplit(), 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::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CommonTheoremProducer::iffMP(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implMP(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::SearchEngineTheoremProducer::satProof(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::ArrayTheoremProducer::splitOnConstants(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::SearchEngineTheoremProducer::unitProp(), and CVC3::CommonTheoremProducer::varIntroRule().

Theorem CVC3::TheoremProducer::newRWTheorem ( const Expr lhs,
const Expr rhs,
const Assumptions assump,
const Proof pf 
)
inlineprotected

Create a rewrite theorem: lhs = rhs.

Definition at line 118 of file theorem_producer.h.

References d_tm.

Referenced by CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractAllToConstEq(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), 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::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivConst(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::BitvectorTheoremProducer::bvURemConst(), CVC3::BitvectorTheoremProducer::bvURemRewrite(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::canonBVPlus(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::constEq(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::BitvectorTheoremProducer::eqConst(), 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::BitvectorTheoremProducer::generalIneqn(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::BitvectorTheoremProducer::MarkNonSolvableEq(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negElim(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CommonTheoremProducer::notToIff(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

Theorem CVC3::TheoremProducer::newReflTheorem ( const Expr e)
inlineprotected

Create a reflexivity theorem.

Definition at line 125 of file theorem_producer.h.

Referenced by CVC3::BitvectorTheoremProducer::canonBVEQ(), and CVC3::CommonTheoremProducer::reflexivityRule().

Theorem CVC3::TheoremProducer::newAssumption ( const Expr thm,
const Proof pf,
int  scope = -1 
)
inlineprotected

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 
)
inlineprotected
Theorem3 CVC3::TheoremProducer::newRWTheorem3 ( const Expr lhs,
const Expr rhs,
const Assumptions assump,
const Proof pf 
)
inlineprotected

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::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::andIntro(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::CommonTheoremProducer::assumpRule(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractAllToConstEq(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), 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::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivConst(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::BitvectorTheoremProducer::bvURemConst(), CVC3::BitvectorTheoremProducer::bvURemRewrite(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::canonBVPlus(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::SearchEngineTheoremProducer::caseSplit(), 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::constEq(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::CommonTheoremProducer::excludedMiddle(), 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::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::BitvectorTheoremProducer::generalIneqn(), 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::ArrayTheoremProducer::interchangeIndices(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negElim(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::SearchEngineTheoremProducer::satProof(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::ArrayTheoremProducer::splitOnConstants(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

bool CVC3::TheoremProducer::withAssumptions ( )
inline
Proof TheoremProducer::newLabel ( const Expr e)
Proof TheoremProducer::newPf ( const std::string &  name)

Definition at line 75 of file theorem_producer.cpp.

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

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::andIntro(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractAllToConstEq(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), 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::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivConst(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::BitvectorTheoremProducer::bvURemConst(), CVC3::BitvectorTheoremProducer::bvURemRewrite(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::canonBVPlus(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::SearchEngineTheoremProducer::caseSplit(), 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::constEq(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::CommonTheoremProducer::excludedMiddle(), 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::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::BitvectorTheoremProducer::generalIneqn(), generateSatProof(), 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::ArrayTheoremProducer::interchangeIndices(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::BitvectorTheoremProducer::MarkNonSolvableEq(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negElim(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::BitvectorTheoremProducer::negNeg(), newLabel(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), CVC3::SearchEngineTheoremProducer::propAndrAF(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrLRT(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::CommonTheoremProducer::queryTCC(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::SearchEngineTheoremProducer::satProof(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::ArrayTheoremProducer::splitOnConstants(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

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

Definition at line 79 of file theorem_producer.cpp.

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

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

Definition at line 87 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 
)
Proof TheoremProducer::newPf ( const std::string &  name,
const Expr e1,
const Expr e2,
const Expr e3 
)

Definition at line 97 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 
)
Proof TheoremProducer::newPf ( const std::string &  name,
Expr::iterator  begin,
const Expr::iterator end 
)

Definition at line 119 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 129 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 139 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 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< Expr > &  args 
)

Definition at line 161 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 172 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 185 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 199 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 
)
Proof TheoremProducer::newPf ( const std::string &  name,
const std::vector< Expr > &  args,
const std::vector< Proof > &  pfs 
)

Definition at line 221 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 234 of file theorem_producer.cpp.

References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), IF_DEBUG, 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 247 of file theorem_producer.cpp.

References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), 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 258 of file theorem_producer.cpp.

References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), CVC3::Type::getExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::isVar(), LAMBDA, CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().

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

Member Data Documentation

TheoremManager* CVC3::TheoremProducer::d_tm
protected
ExprManager* CVC3::TheoremProducer::d_em
protected
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 TheoremProducer().


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