CVC3: Class Members

- r -

rafineInequalityToInteger() : CVC3::TheoryArithOld
rafineIntegerConstraints() : CVC3::TheoryArithNew
rafineStrictInteger() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithProofRules , CVC3::ArithTheoremProducerOld
rat() : CVC3::TheoryBitvector , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::BitvectorTheoremProducer , CVC3::TheoryArith
ratExpr() : CVC3::VCL , CVC3::ValidityChecker
Rational() : CVC3::Rational
readArrayLiteral() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
readExpr() : CVC3::ValidityChecker , CVC3::VCL
realShadow() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
realShadowEq() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
realType() : CVC3::TheoryArith , CVC3::ValidityChecker , CVC3::VCL , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
rebuild() : CVC3::Expr , CVC3::ExprManager , CVC3::ExprValue
rebuildRec() : CVC3::ExprManager
recCompleteInster() : recCompleteInster
recFindBoundVars() : CVC3::QuantTheoremProducer
recGeneralTrig() : CVC3::TheoryQuant
recGoodSemMatch() : CVC3::TheoryQuant
recInstantiate() : CVC3::TheoryQuant
recInstMacros() : CVC3::CompleteInstPreProcessor
recMultMatch() : CVC3::TheoryQuant
recMultMatchDebug() : CVC3::TheoryQuant
recMultMatchNewWay() : CVC3::TheoryQuant
recMultMatchOldWay() : CVC3::TheoryQuant
recordExpr() : CVC3::ValidityChecker , CVC3::VCL , CVC3::RecordsTheoremProducer , CVC3::TheoryRecords , CVC3::ValidityChecker
recordFact() : CVC3::SearchEngineFast
recordNewRootLit() : CVC3::SearchSat
recordSelect() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
RecordsTheoremProducer() : CVC3::RecordsTheoremProducer
recordType() : CVC3::TheoryRecords , CVC3::ValidityChecker , CVC3::VCL , CVC3::RecordsTheoremProducer
recordUpdate() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
recQuantLevel() : CVC3::TheoremValue
recRewriteNot() : CVC3::CompleteInstPreProcessor
recSearchCover() : CVC3::TheoryQuant
recSelectExpr() : CVC3::ValidityChecker , CVC3::VCL
recSkolemize() : CVC3::CompleteInstPreProcessor
recSynMatch() : CVC3::TheoryQuant
recSynMatchBackupOnly() : CVC3::TheoryQuant
recUpdateExpr() : CVC3::ValidityChecker , CVC3::VCL
recursiveCanonSimpCheck() : CVC3::TheoryArith
recursiveMap() : CVC3::TheoryQuant
recursivePrint() : CVC3::Theorem
recursiveQuantSubst() : CVC3::Expr
recursiveSubst() : CVC3::Expr
reduceDB() : MiniSat::Solver
RefCDO() : CVC3::SmartCDO< T >::SmartCDO::RefCDO< U >
refineCounterExample() : CVC3::Theory , CVC3::TheoryArith , CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryCore
reflexivityRule() : CVC3::CommonProofRules , CVC3::Theory , CVC3::CommonTheoremProducer
RefNotifyObj() : CVC3::SmartCDO< T >::SmartCDO::RefCDO< U >::SmartCDO::RefCDO::RefNotifyObj
refutes() : CVC3::Theorem
RegisterAssignmentHook() : SatSolver
registerAtom() : CVC3::Theory , CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::VCL , CVC3::SearchSatCNFCallback , SAT::CNF_Manager::CNF_Manager::CNFCallback , SAT::CNF_Manager , CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat
registerClause() : MiniSat::Derivation
registerCNFCallback() : SAT::CNF_Manager
registerCoreSatAPI() : CVC3::TheoryCore
RegisterDecisionHook() : SatSolver
RegisterDeductionHook() : SatSolver
RegisterDLevelHook() : SatSolver
registerInference() : MiniSat::Derivation
registerInputClause() : MiniSat::Derivation
registerKinds() : CVC3::Theory
registerLeaf() : SAT::SatProof
registerNode() : SAT::SatProof
registerPrettyPrinter() : CVC3::ExprManager
registerSubclass() : CVC3::ExprManager
registerTheory() : CVC3::Theory
registerTrig() : CVC3::TheoryQuant
registerTrigReal() : CVC3::TheoryQuant
registerTypeComputer() : CVC3::ExprManager
registerUnit() : SAT::CNF_Formula , SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
registerVar() : MiniSat::Solver
RegTheoremValue() : CVC3::RegTheoremValue
release() : MiniSat::vec< T >
relToClosure() : CVC3::UFProofRules , CVC3::UFTheoremProducer
relTrans() : CVC3::UFProofRules , CVC3::UFTheoremProducer
remove() : MiniSat::Solver
removedClause() : MiniSat::Derivation
RemoveFunctionApps() : CVC3::ExprTransform
removeWatch() : MiniSat::Solver
renameExpr() : CVC3::TheoryArray
repeatRule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
replaceITE() : CVC3::SearchImplBase
replaceITErec() : SAT::CNF_Manager
reportResult() : CVC3::VCCmd
reprocessFlags() : CVC3::ValidityChecker , CVC3::VCL
requestPop() : MiniSat::Solver
reset() : SAT::Var , SAT::Lit , SAT::CNF_Formula_Impl , CVC3::Parser , CVC3::ValidityChecker , CVC3::VCL
Reset() : SatSolver::SatSolver::Var , SatSolver::SatSolver::Lit , SatSolver::SatSolver::Clause , SatSolver
resetDag() : CVC3::ExprStream
ResetException() : CVC3::ResetException
resetIndent() : CVC3::ExprStream
resize() : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
resolveID() : CVC3::Theory
resolveTheoryImplication() : MiniSat::Solver
restart() : CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker , CVC3::VCL
Restart() : SatSolver
restartInternal() : CVC3::SearchImplBase , CVC3::SearchEngineFast , CVC3::SearchSimple
restore() : CVC3::SearchSat , CVC3::Scope , CVC3::ContextObjChain
restoreData() : CVC3::CDMapData , CVC3::CDFlags , CVC3::CDList< T > , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDMap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDMapOrderedData , CVC3::CDMapOrdered< Key, Data > , CVC3::CDO< T > , CVC3::ContextObj
restoreIndent() : CVC3::ExprManager
restorePre() : CVC3::SearchSat
Restorer() : CVC3::SearchSat::SearchSat::Restorer
resumeGC() : CVC3::ExprManager , CVC3::VariableManager
returnFromCheck() : CVC3::SearchEngine , CVC3::VCL , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker
rewrite() : CVC3::TheorySimulate , CVC3::TheoryCore , CVC3::Theory , CVC3::TheoryArith , CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArray , CVC3::TheoryBitvector , CVC3::TheoryDatatype , CVC3::TheoryQuant , CVC3::TheoryRecords , CVC3::TheoryUF
rewriteAnd() : CVC3::Theory , CVC3::CommonProofRules , CVC3::CommonTheoremProducer
rewriteAndSubterms() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteAtomic() : CVC3::Theory , CVC3::TheoryBitvector
rewriteAux() : CVC3::TheoryRecords
rewriteBoolean() : CVC3::TheoryBitvector
rewriteBV() : CVC3::TheoryBitvector
rewriteBVCOMP() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
rewriteBVSub() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
rewriteCC() : CVC3::Theory
rewriteCore() : CVC3::TheoryCore
rewriteDistinct() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteIff() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
rewriteImplies() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteIte() : CVC3::Theory
rewriteIteBool() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteCond() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteElse() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteFalse() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
rewriteIteSame() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
rewriteIteThen() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteIteToAnd() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteToIff() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteToImp() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteToNot() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteToOr() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteIteTrue() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
rewriteLeavesConst() : CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
rewriteLetDecl() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteLitCore() : CVC3::TheoryCore
rewriteLiteral() : CVC3::TheoryCore
rewriteLitSelect() : CVC3::RecordsTheoremProducer , CVC3::RecordsProofRules
rewriteLitUpdate() : CVC3::RecordsTheoremProducer , CVC3::RecordsProofRules
rewriteNAND() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
rewriteNOR() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
rewriteNot() : CVC3::CompleteInstPreProcessor
rewriteNotAnd() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteNotExists() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer , CVC3::QuantTheoremProducer , CVC3::QuantProofRules
rewriteNotFalse() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
rewriteNotForall() : CVC3::CommonTheoremProducer , CVC3::QuantProofRules , CVC3::CommonProofRules , CVC3::QuantTheoremProducer
rewriteNotIff() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteNotIte() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
rewriteNotNot() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
rewriteNotOr() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteNotTrue() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
rewriteOpDef() : CVC3::UFTheoremProducer , CVC3::UFProofRules
rewriteOr() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules , CVC3::Theory
rewriteOrSubterms() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
rewriteReadWrite() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
rewriteReadWrite2() : CVC3::ArrayTheoremProducer , CVC3::ArrayProofRules
rewriteRedundantWrite1() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
rewriteRedundantWrite2() : CVC3::ArrayTheoremProducer , CVC3::ArrayProofRules
rewriteReflexivity() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
rewriteSameStore() : CVC3::ArrayTheoremProducer , CVC3::ArrayProofRules
rewriteSelCons() : CVC3::DatatypeProofRules , CVC3::DatatypeTheoremProducer
rewriteTestCons() : CVC3::DatatypeTheoremProducer , CVC3::DatatypeProofRules
rewriteToDiff() : CVC3::TheoryArith
rewriteUpdateSelect() : CVC3::RecordsTheoremProducer , CVC3::RecordsProofRules
rewriteUsingSymmetry() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
rewriteWriteWrite() : CVC3::ArrayTheoremProducer , CVC3::ArrayProofRules
rewriteXNOR() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
rightMinusLeft() : CVC3::ArithTheoremProducer , CVC3::ArithProofRules , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
rightShiftToConcat() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
rotlRule() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
rotrRule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
RWTheoremValue() : CVC3::RWTheoremValue