#include <theorem_producer.h>
Inherited by 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, and CVC3::UFTheoremProducer.
Public Member Functions
- TheoremProducer (TheoremManager *tm)
- virtual ~TheoremProducer ()
- bool withProof ()
- bool withAssumptions ()
- Proof newLabel (const Expr &e)
- 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)
- Proof newPf (const Proof &label, const Proof &pf)
- Proof newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
- 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()
- Create a new theorem. See also newRWTheorem() and newReflTheorem()
- Theorem newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
- Theorem newReflTheorem (const Expr &e)
- 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
- TheoremManager * d_tm
- ExprManager * d_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 | ( | ) | [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 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 | ||
| ) | [inline, protected] |
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().
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 |
||
| ) | [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 d_tm, IF_DEBUG, CVC3::Expr::isEq(), CVC3::Expr::isIff(), and 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::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] |
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::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), and CVC3::SearchEngineTheoremProducer::propIterThen().
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(), CVC3::TheoremManager::getFlags(), CVC3::ExprManager::newBoundVarExpr(), and newPf().
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 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().
Definition at line 79 of file theorem_producer.cpp.
References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().
Definition at line 83 of file theorem_producer.cpp.
References d_em, d_pfOp, CVC3::Proof::getExpr(), and CVC3::ExprManager::newVarExpr().
Definition at line 87 of file theorem_producer.cpp.
References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().
Definition at line 92 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 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 | ||
| ) |
Definition at line 108 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 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().
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().
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 | ||
| ) |
Definition at line 210 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 221 of file theorem_producer.cpp.
References d_em, d_pfOp, and CVC3::ExprManager::newVarExpr().
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().
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().
Definition at line 278 of file theorem_producer.cpp.
References d_tm, DebugAssert, CVC3::TheoremManager::getEM(), CVC3::Proof::getExpr(), CVC3::Expr::isVar(), LAMBDA, CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().
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::SearchEngineTheoremProducer::satProof(), 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::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::eliminateSkolemAxioms(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CommonTheoremProducer::iffTrue(), newPf(), CVC3::CommonTheoremProducer::notToIff(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::BitvectorTheoremProducer::rat(), CVC3::ArithTheoremProducerOld::rat(), CVC3::ArithTheoremProducer3::rat(), CVC3::ArithTheoremProducer::rat(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), 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 TheoremProducer().
The documentation for this class was generated from the following files:
