Main Page | Modules | Namespace List | Class Hierarchy | Alphabetical List | Class List | Directories | File List | Namespace Members | Class Members | File Members | Related Pages | Search for 
CVCL::TheoremProducer

CVCL::TheoremProducer Class Reference

#include <theorem_producer.h>

Inheritance diagram for CVCL::TheoremProducer:

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

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Definition at line 99 of file theorem_producer.h.

Constructor & Destructor Documentation

TheoremProducer::TheoremProducer (  TheoremManager *  tm  ) 
 

Definition at line 52 of file theorem_producer.cpp.

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

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

Definition at line 165 of file theorem_producer.h.

Member Function Documentation

Theorem CVCL::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 115 of file theorem_producer.h.

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

Referenced by CVCL::CommonTheoremProducer::andElim(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::DatatypeTheoremProducer::dummyTheorem(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implMP(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::RefinedArithTheoremProducer::ltAddR(), CVCL::RefinedArithTheoremProducer::ltScale(), CVCL::RefinedArithTheoremProducer::ltTrans(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::DatatypeTheoremProducer::noCycle(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), CVCL::ArithTheoremProducer::realShadow(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::CoreTheoremProducer::typePred(), CVCL::BitvectorTheoremProducer::typePredBit(), CVCL::SearchEngineTheoremProducer::unitProp(), and CVCL::CommonTheoremProducer::varIntroRule().

Theorem CVCL::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 126 of file theorem_producer.h.

References d_tm.

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

Theorem CVCL::TheoremProducer::newReflTheorem (  const Expr &  e,
const Proof &  pf
)  [inline, protected]
 

Create a reflexivity theorem.

Definition at line 133 of file theorem_producer.h.

References d_tm.

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

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

Definition at line 137 of file theorem_producer.h.

References d_tm.

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

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

Definition at line 141 of file theorem_producer.h.

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

Referenced by CVCL::CoreTheoremProducer::queryTCC().

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

Definition at line 151 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
)  throw (Exception) [protected]
 

Definition at line 41 of file theorem_producer.cpp.

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

Testing whether to generate proofs.

Definition at line 168 of file theorem_producer.h.

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

Referenced by CVCL::RefinedArithTheoremProducer::addAssoc(), CVCL::RefinedArithTheoremProducer::addInvR(), CVCL::RefinedArithTheoremProducer::addLID(), CVCL::RefinedArithTheoremProducer::addSymm(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::CommonTheoremProducer::andElim(), CVCL::CoreTheoremProducer::AndToIte(), CVCL::BitvectorTheoremProducer::andZero(), CVCL::UFTheoremProducer::applyLambda(), CVCL::RefinedArithTheoremProducer::arithmetic(), CVCL::CommonTheoremProducer::assumpRule(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitExtractSXRule(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::bvuminusBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusBVUminus(), CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusVar(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDivide(), CVCL::ArithTheoremProducer::canonDivideConst(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonDivideVar(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonInvertConst(), CVCL::ArithTheoremProducer::canonInvertLeaf(), CVCL::ArithTheoremProducer::canonInvertMult(), CVCL::ArithTheoremProducer::canonInvertPow(), CVCL::ArithTheoremProducer::canonMult(), CVCL::ArithTheoremProducer::canonMultConstConst(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultConstTerm(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonMultOne(), CVCL::ArithTheoremProducer::canonMultTermConst(), CVCL::ArithTheoremProducer::canonMultZero(), CVCL::ArithTheoremProducer::canonPlus(), CVCL::ArithTheoremProducer::canonPowConst(), CVCL::ArithTheoremProducer::canonUMinusToDivide(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::RefinedArithTheoremProducer::distribL(), CVCL::RefinedArithTheoremProducer::divideDef(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::BitvectorTheoremProducer::eqConst(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::equalLeaves1(), CVCL::ArithTheoremProducer::equalLeaves2(), CVCL::ArithTheoremProducer::equalLeaves3(), CVCL::ArithTheoremProducer::equalLeaves4(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::RecordsTheoremProducer::expandRecord(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::RecordsTheoremProducer::expandTuple(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::BitvectorTheoremProducer::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flipBVMult(), CVCL::ArithTheoremProducer::flipInequality(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CoreTheoremProducer::iffAndDistrib(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::CoreTheoremProducer::iffOrDistrib(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implMP(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::ArrayTheoremProducer::interchangeIndices(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::BitvectorTheoremProducer::iteBVnegRule(), CVCL::BitvectorTheoremProducer::iteExtractRule(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::RefinedArithTheoremProducer::ltAddR(), CVCL::RefinedArithTheoremProducer::ltScale(), CVCL::RefinedArithTheoremProducer::ltTrans(), CVCL::RefinedArithTheoremProducer::minusDef(), CVCL::ArithTheoremProducer::minusToPlus(), CVCL::RefinedArithTheoremProducer::multAssoc(), CVCL::ArithTheoremProducer::multEqn(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::RefinedArithTheoremProducer::multInvR(), CVCL::RefinedArithTheoremProducer::multLID(), CVCL::RefinedArithTheoremProducer::multSymm(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), CVCL::BitvectorTheoremProducer::negConst(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::BitvectorTheoremProducer::negNeg(), CVCL::DatatypeTheoremProducer::noCycle(), CVCL::BitvectorTheoremProducer::notBVLTRule(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::CommonTheoremProducer::notToIff(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::BitvectorTheoremProducer::orOne(), CVCL::CoreTheoremProducer::OrToIte(), CVCL::BitvectorTheoremProducer::padBVLTRule(), CVCL::BitvectorTheoremProducer::padBVMult(), CVCL::BitvectorTheoremProducer::padBVPlus(), CVCL::BitvectorTheoremProducer::padSBVLTRule(), CVCL::ArithTheoremProducer::plusPredicate(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), CVCL::CoreTheoremProducer::queryTCC(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::CommonTheoremProducer::reflexivityRule(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), CVCL::CoreTheoremProducer::rewriteConstDef(), CVCL::CommonTheoremProducer::rewriteIff(), CVCL::CoreTheoremProducer::rewriteImplies(), CVCL::CoreTheoremProducer::rewriteIteBool(), CVCL::CoreTheoremProducer::rewriteIteCond(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CoreTheoremProducer::rewriteIteToAnd(), CVCL::CoreTheoremProducer::rewriteIteToIff(), CVCL::CoreTheoremProducer::rewriteIteToImp(), CVCL::CoreTheoremProducer::rewriteIteToNot(), CVCL::CoreTheoremProducer::rewriteIteToOr(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::CoreTheoremProducer::rewriteLetDecl(), CVCL::RecordsTheoremProducer::rewriteLitSelect(), CVCL::RecordsTheoremProducer::rewriteLitUpdate(), CVCL::CoreTheoremProducer::rewriteNotAnd(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotFalse(), CVCL::QuantTheoremProducer::rewriteNotForall(), CVCL::CommonTheoremProducer::rewriteNotForall(), CVCL::CoreTheoremProducer::rewriteNotIff(), CVCL::CoreTheoremProducer::rewriteNotIte(), CVCL::CommonTheoremProducer::rewriteNotNot(), CVCL::CoreTheoremProducer::rewriteNotOr(), CVCL::CommonTheoremProducer::rewriteNotTrue(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::CoreTheoremProducer::rewriteOrSubterms(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite2(), CVCL::CommonTheoremProducer::rewriteReflexivity(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::DatatypeTheoremProducer::rewriteTestCons(), CVCL::RecordsTheoremProducer::rewriteUpdateSelect(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::ArithTheoremProducer::rightMinusLeft(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::BitvectorTheoremProducer::signExtendRule(), CVCL::CommonTheoremProducer::skolemizeRewrite(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), CVCL::CoreTheoremProducer::typePred(), CVCL::BitvectorTheoremProducer::typePredBit(), CVCL::ArithTheoremProducer::uMinusToMult(), CVCL::SearchEngineTheoremProducer::unitProp(), CVCL::CommonTheoremProducer::varIntroRule(), CVCL::BitvectorTheoremProducer::zeroCoeffBVMult(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

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

Testing whether to generate assumptions.

Definition at line 171 of file theorem_producer.h.

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

Referenced by CVCL::CommonTheoremProducer::andElim(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::equalLeaves1(), CVCL::ArithTheoremProducer::equalLeaves2(), CVCL::ArithTheoremProducer::equalLeaves3(), CVCL::ArithTheoremProducer::equalLeaves4(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implMP(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::CommonTheoremProducer::notToIff(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), CVCL::CoreTheoremProducer::queryTCC(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), and CVCL::SearchEngineTheoremProducer::unitProp().

Proof TheoremProducer::newLabel (  const Expr &  e  ) 
 

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

Definition at line 60 of file theorem_producer.cpp.

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

Referenced by CVCL::CommonTheoremProducer::assumpRule(), CVCL::CommonTheoremProducer::skolemizeRewrite(), and CVCL::CommonTheoremProducer::skolemizeRewriteVar().

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

Referenced by CVCL::RefinedArithTheoremProducer::addAssoc(), CVCL::RefinedArithTheoremProducer::addInvR(), CVCL::RefinedArithTheoremProducer::addLID(), CVCL::RefinedArithTheoremProducer::addSymm(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::CommonTheoremProducer::andElim(), CVCL::CoreTheoremProducer::AndToIte(), CVCL::BitvectorTheoremProducer::andZero(), CVCL::UFTheoremProducer::applyLambda(), CVCL::RefinedArithTheoremProducer::arithmetic(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitExtractSXRule(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::bvuminusBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusBVUminus(), CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusVar(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDivide(), CVCL::ArithTheoremProducer::canonDivideConst(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonDivideVar(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonInvertConst(), CVCL::ArithTheoremProducer::canonInvertLeaf(), CVCL::ArithTheoremProducer::canonInvertMult(), CVCL::ArithTheoremProducer::canonInvertPow(), CVCL::ArithTheoremProducer::canonMult(), CVCL::ArithTheoremProducer::canonMultConstConst(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultConstTerm(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonMultOne(), CVCL::ArithTheoremProducer::canonMultTermConst(), CVCL::ArithTheoremProducer::canonMultZero(), CVCL::ArithTheoremProducer::canonPlus(), CVCL::ArithTheoremProducer::canonPowConst(), CVCL::ArithTheoremProducer::canonUMinusToDivide(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::RefinedArithTheoremProducer::distribL(), CVCL::RefinedArithTheoremProducer::divideDef(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::BitvectorTheoremProducer::eqConst(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::ArithTheoremProducer::equalLeaves1(), CVCL::ArithTheoremProducer::equalLeaves2(), CVCL::ArithTheoremProducer::equalLeaves3(), CVCL::ArithTheoremProducer::equalLeaves4(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::RecordsTheoremProducer::expandRecord(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::RecordsTheoremProducer::expandTuple(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::BitvectorTheoremProducer::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flipBVMult(), CVCL::ArithTheoremProducer::flipInequality(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CoreTheoremProducer::iffAndDistrib(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffMP(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::CoreTheoremProducer::iffOrDistrib(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implMP(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::ArrayTheoremProducer::interchangeIndices(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::BitvectorTheoremProducer::iteBVnegRule(), CVCL::BitvectorTheoremProducer::iteExtractRule(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::RefinedArithTheoremProducer::ltAddR(), CVCL::RefinedArithTheoremProducer::ltScale(), CVCL::RefinedArithTheoremProducer::ltTrans(), CVCL::RefinedArithTheoremProducer::minusDef(), CVCL::ArithTheoremProducer::minusToPlus(), CVCL::RefinedArithTheoremProducer::multAssoc(), CVCL::ArithTheoremProducer::multEqn(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::RefinedArithTheoremProducer::multInvR(), CVCL::RefinedArithTheoremProducer::multLID(), CVCL::RefinedArithTheoremProducer::multSymm(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), CVCL::BitvectorTheoremProducer::negConst(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::BitvectorTheoremProducer::negNeg(), CVCL::DatatypeTheoremProducer::noCycle(), CVCL::BitvectorTheoremProducer::notBVLTRule(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::CommonTheoremProducer::notToIff(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::BitvectorTheoremProducer::orOne(), CVCL::CoreTheoremProducer::OrToIte(), CVCL::BitvectorTheoremProducer::padBVLTRule(), CVCL::BitvectorTheoremProducer::padBVMult(), CVCL::BitvectorTheoremProducer::padBVPlus(), CVCL::BitvectorTheoremProducer::padSBVLTRule(), CVCL::ArithTheoremProducer::plusPredicate(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), CVCL::CoreTheoremProducer::queryTCC(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::CommonTheoremProducer::reflexivityRule(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), CVCL::CoreTheoremProducer::rewriteConstDef(), CVCL::CommonTheoremProducer::rewriteIff(), CVCL::CoreTheoremProducer::rewriteImplies(), CVCL::CoreTheoremProducer::rewriteIteBool(), CVCL::CoreTheoremProducer::rewriteIteCond(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CoreTheoremProducer::rewriteIteToAnd(), CVCL::CoreTheoremProducer::rewriteIteToIff(), CVCL::CoreTheoremProducer::rewriteIteToImp(), CVCL::CoreTheoremProducer::rewriteIteToNot(), CVCL::CoreTheoremProducer::rewriteIteToOr(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::CoreTheoremProducer::rewriteLetDecl(), CVCL::RecordsTheoremProducer::rewriteLitSelect(), CVCL::RecordsTheoremProducer::rewriteLitUpdate(), CVCL::CoreTheoremProducer::rewriteNotAnd(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotFalse(), CVCL::QuantTheoremProducer::rewriteNotForall(), CVCL::CommonTheoremProducer::rewriteNotForall(), CVCL::CoreTheoremProducer::rewriteNotIff(), CVCL::CoreTheoremProducer::rewriteNotIte(), CVCL::CommonTheoremProducer::rewriteNotNot(), CVCL::CoreTheoremProducer::rewriteNotOr(), CVCL::CommonTheoremProducer::rewriteNotTrue(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::CoreTheoremProducer::rewriteOrSubterms(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite2(), CVCL::CommonTheoremProducer::rewriteReflexivity(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::DatatypeTheoremProducer::rewriteTestCons(), CVCL::RecordsTheoremProducer::rewriteUpdateSelect(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::ArithTheoremProducer::rightMinusLeft(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::BitvectorTheoremProducer::signExtendRule(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), CVCL::CoreTheoremProducer::typePred(), CVCL::BitvectorTheoremProducer::typePredBit(), CVCL::ArithTheoremProducer::uMinusToMult(), CVCL::SearchEngineTheoremProducer::unitProp(), CVCL::CommonTheoremProducer::varIntroRule(), CVCL::BitvectorTheoremProducer::zeroCoeffBVMult(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 233 of file theorem_producer.cpp.

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

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 246 of file theorem_producer.cpp.

References d_tm, CVCL::TheoremManager::getEM(), CVCL::Proof::getExpr(), CVCL::Expr::isVar(), CVCL::LAMBDA, CVCL::ExprManager::newClosureExpr(), and CVCL::Expr::toString().

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 257 of file theorem_producer.cpp.

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

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

Definition at line 277 of file theorem_producer.cpp.

References d_tm, CVCL::TheoremManager::getEM(), CVCL::Proof::getExpr(), CVCL::Expr::isVar(), CVCL::LAMBDA, CVCL::ExprManager::newClosureExpr(), and CVCL::Expr::toString().

Member Data Documentation

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

Definition at line 102 of file theorem_producer.h.

Referenced by CVCL::RefinedArithTheoremProducer::addAssoc(), CVCL::RefinedArithTheoremProducer::addInvR(), CVCL::RefinedArithTheoremProducer::addLID(), CVCL::RefinedArithTheoremProducer::addSymm(), CVCL::RefinedArithTheoremProducer::distribL(), CVCL::RefinedArithTheoremProducer::divideDef(), CVCL::RefinedArithTheoremProducer::ltAddR(), CVCL::RefinedArithTheoremProducer::ltScale(), CVCL::RefinedArithTheoremProducer::ltTrans(), CVCL::RefinedArithTheoremProducer::minusDef(), CVCL::RefinedArithTheoremProducer::multAssoc(), CVCL::RefinedArithTheoremProducer::multInvR(), CVCL::RefinedArithTheoremProducer::multLID(), CVCL::RefinedArithTheoremProducer::multSymm(), CVCL::RefinedArithTheoremProducer::multZeroL(), newAssumption(), newLabel(), newPf(), newReflTheorem(), newRWTheorem(), newRWTheorem3(), newTheorem(), newTheorem3(), withAssumptions(), and withProof().

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

Reimplemented in CVCL::RefinedArithTheoremProducer.

Definition at line 103 of file theorem_producer.h.

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

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

Definition at line 106 of file theorem_producer.h.

Op CVCL::TheoremProducer::d_pfOp [protected]
 

Definition at line 108 of file theorem_producer.h.

Expr CVCL::TheoremProducer::d_hole [protected]
 

Definition at line 110 of file theorem_producer.h.

Referenced by CVCL::ArithTheoremProducer::canonDivideConst(), and TheoremProducer().

The documentation for this class was generated from the following files:
Generated on Thu Apr 13 16:57:44 2006 for CVC Lite by  doxygen 1.4.4