Here is a list of all class members with links to the classes they belong to:

- r -

• rafineInequalityToInteger() : CVC3::TheoryArithOld
• rafineIntegerConstraints() : CVC3::TheoryArithNew
• rafineStrictInteger() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• random_seed : MiniSat::VarOrder
• random_var_freq : MiniSat::SearchParams
• rat() : CVC3::ArithTheoremProducer , CVC3::TheoryArith , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::TheoryBitvector , CVC3::BitvectorTheoremProducer
• ratExpr() : CVC3::ValidityChecker , CVC3::VCL
• Rational() : CVC3::Rational
• RationalType : CVC3::TheoryArithNew::EpsRational , CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational
• readArrayLiteral() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
• readExpr() : CVC3::ValidityChecker , CVC3::VCL
• realShadow() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• realShadowEq() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• realType() : CVC3::TheoryArith , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ValidityChecker , CVC3::VCL
• rebuild() : CVC3::ExprValue , CVC3::Expr , CVC3::ExprManager
• 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::TheoryRecords , CVC3::RecordsTheoremProducer , CVC3::ValidityChecker , CVC3::VCL
• recordFact() : CVC3::SearchEngineFast
• recordNewRootLit() : CVC3::SearchSat
• recordSelect() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
• RecordsTheoremProducer() : CVC3::RecordsTheoremProducer
• recordType() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer , CVC3::ValidityChecker , CVC3::VCL
• 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 >::RefCDO< U >::RefNotifyObj , RefCDO< U > , CVC3::SmartCDO< T >::RefCDO< U > , RefCDO< U >
• refineCounterExample() : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryCore , CVC3::Theory , CVC3::TheoryArith
• reflexivityRule() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer , CVC3::Theory
• RefNotifyObj : RefCDO< U > , CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj , CVC3::SmartCDO< T >::RefCDO< U >
• refutes() : CVC3::Theorem
• RegisterAssignmentHook() : SatSolver
• registerAtom() : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryCore , CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker , CVC3::Theory , CVC3::VCL , CVC3::Theory , SAT::CNF_Manager::CNFCallback , SAT::CNF_Manager , CVC3::SearchSatCNFCallback
• 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_Impl , SAT::CNF_Formula , SAT::CD_CNF_Formula
• registerVar() : MiniSat::Solver
• RegTheoremValue() : CVC3::RegTheoremValue , CVC3::TheoremValue , CVC3::Theorem
• release() : vec< T > , 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 : CVC3::ExprStream , CVC3::Parser
• Reset() : SatSolver::Var , SatSolver::Lit , SatSolver::Clause , SatSolver
• reset() : SAT::Var , SAT::Lit , CVC3::ValidityChecker , SAT::CNF_Formula_Impl , CVC3::VCL
• 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() : SatSolver
• restart() : CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker , CVC3::VCL
• restartInternal() : CVC3::SearchImplBase , CVC3::SearchSimple , CVC3::SearchEngineFast
• restore() : CVC3::Scope , CVC3::SearchSat , CVC3::ContextObjChain
• restoreData() : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDMapData , iterator , CDOmap< Key, Data, HashFcn > , CDList< size_t > , CDMap< Expr, bool > , CDList< size_t > size_t , CDOmapOrdered< Key, Data > , iterator , CVC3::CDMap< Key, Data, HashFcn > , CDList< Theorem > , iterator , CDList< Ineq > , iterator , CDOmap< Expr, FreeConst > , CDO< Theorem > , iterator , CDMap< Expr, Theorem > , CVC3::CDMapOrderedData , CVC3::CDMapOrdered< Key, Data > , iterator , CVC3::CDO< T > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDList< T > , CDList< Expr > , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDMapOrdered< Key, Data > , CDO< T > , const_iterator , iterator , CDMap< Expr, CDList< dynTrig > , CDList< dynTrig > , CVC3::CDOmapOrdered< Key, Data > , CVC3::ContextObj , CDMap< Key, Data, HashFcn > , iterator , CVC3::CDFlags , CDOmap< Key, Data, HashFcn > new , CVC3::CDList< T >
• restoreIndent() : CVC3::ExprManager
• restorePre() : CVC3::SearchSat
• Restorer : CVC3::SearchSat , CVC3::SearchSat::Restorer
• resumeGC() : CVC3::VariableManager , CVC3::ExprManager
• returnFromCheck() : CVC3::ValidityChecker , CVC3::SearchSat , CVC3::SearchEngine , CVC3::VCL , CVC3::SearchImplBase
• rewrite() : CVC3::TheoryUF , CVC3::TheoryBitvector , CVC3::TheoryCore , CVC3::TheoryQuant , CVC3::Theory , CVC3::TheoryRecords , CVC3::TheoryArithOld , CVC3::TheoryArith3 , CVC3::TheorySimulate , CVC3::TheoryArithNew , CVC3::TheoryArray , CVC3::TheoryDatatype , CVC3::TheoryArith
• REWRITE_NORMAL : CVC3::Expr
• rewriteAnd() : CVC3::CommonTheoremProducer , 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::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• rewriteCC() : CVC3::Theory
• rewriteCore() : CVC3::TheoryCore
• rewriteDistinct() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIff() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• rewriteImplies() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
• rewriteIte() : CVC3::Theory
• rewriteIteBool() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteCond() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteElse() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteFalse() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• rewriteIteSame() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• rewriteIteThen() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteToAnd() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
• rewriteIteToIff() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteToImp() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteToNot() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteToOr() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteIteTrue() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• rewriteLeavesConst() : CVC3::ArithProofRules , CVC3::ArithTheoremProducerOld
• rewriteLetDecl() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteLitCore() : CVC3::TheoryCore
• rewriteLiteral() : CVC3::TheoryCore
• rewriteLitSelect() : CVC3::RecordsProofRules , CVC3::RecordsTheoremProducer
• rewriteLitUpdate() : CVC3::RecordsProofRules , CVC3::RecordsTheoremProducer
• rewriteNAND() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• rewriteNOR() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• rewriteNot() : CVC3::CompleteInstPreProcessor
• rewriteNotAnd() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteNotExists() : CVC3::CommonTheoremProducer , CVC3::QuantProofRules , CVC3::QuantTheoremProducer , CVC3::CommonProofRules
• rewriteNotFalse() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• rewriteNotForall() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules , CVC3::QuantTheoremProducer , CVC3::QuantProofRules
• rewriteNotIff() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteNotIte() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
• rewriteNotNot() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• rewriteNotOr() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
• rewriteNotTrue() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• rewriteOpDef() : CVC3::UFTheoremProducer , CVC3::UFProofRules
• rewriteOr() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer , CVC3::CommonProofRules , CVC3::CommonTheoremProducer , CVC3::Theory
• rewriteOrSubterms() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• rewriteReadWrite() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
• rewriteReadWrite2() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
• rewriteRedundantWrite1() : CVC3::ArrayTheoremProducer , CVC3::ArrayProofRules
• rewriteRedundantWrite2() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
• rewriteReflexivity() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• 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::ArrayProofRules , CVC3::ArrayTheoremProducer
• rewriteXNOR() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• rightMinusLeft() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer , CVC3::ArithProofRules
• rightShiftToConcat() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• rotlRule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• rotrRule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• rules : CVC3::TheoryArithOld::DifferenceLogicGraph
• RWTheoremValue() : CVC3::RWTheoremValue , CVC3::Theorem , CVC3::RWTheoremValue , CVC3::TheoremValue

---