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

- r -

• randomness : CSolverParameters
• rat() : CVCL::BitvectorTheoremProducer, CVCL::RefinedArithTheoremProducer, CVCL::ArithTheoremProducer, CVCL::TheoryBitvector, CVCL::TheoryArith
• ratExpr() : CVCL::VCL, CVCL::ValidityChecker
• Rational() : CVCL::Rational
• readArrayLiteral() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• readExpr() : CVCL::VCL, CVCL::ValidityChecker
• Ready() : CVCL::SVC_API_impl
• real_solve() : CSolver
• realShadow() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• realShadowEq() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• realType() : CVCL::ArithTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryArith
• realUsed() : CVCL::TheoryArith
• rebuild() : CVCL::ExprValue, CVCL::ExprManager, CVCL::Expr
• rebuildRec() : CVCL::ExprManager
• recFindBoundVars() : CVCL::QuantTheoremProducer
• recGoodSemMatch() : CVCL::TheoryQuant
• recInstantiate() : CVCL::TheoryQuant
• recordExpr() : CVCL::RecordsTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryRecords
• recordFact() : CVCL::SearchEngineFast
• recordSelect() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• RecordsTheoremProducer() : CVCL::RecordsTheoremProducer
• recordType() : CVCL::RecordsTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryRecords
• recordUpdate() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• recSelectExpr() : CVCL::VCL, CVCL::ValidityChecker
• recSynMatch() : CVCL::TheoryQuant
• recUpdateExpr() : CVCL::VCL, CVCL::ValidityChecker
• recursiveMap() : CVCL::TheoryQuant
• recursivePrint() : CVCL::Theorem
• recursiveSubst() : CVCL::Expr
• RefCDO() : CVCL::SmartCDO< T >::RefCDO< U >
• RefCDO< U > : CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj
• reference : CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• refineCounterExample() : CVCL::TheoryCore, CVCL::TheoryArith, CVCL::Theory
• RefinedArithTheoremProducer() : CVCL::RefinedArithTheoremProducer
• reflexivityRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• ReflexivityTheoremValue : CVCL::ReflexivityTheoremValue, CVCL::TheoremValue
• RefNotifyObj : CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj, CVCL::SmartCDO< T >::RefCDO< U >
• refutes() : CVCL::Theorem
• RegisterAssignmentHook() : CSolver, Xchaff, SatSolver
• registerAtom() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• registerCoreSatAPI() : CVCL::TheoryCore
• RegisterDecisionHook() : CSolver, Xchaff, SatSolver
• RegisterDeductionHook() : CSolver, Xchaff, SatSolver
• RegisterDLevelHook() : CSolver, Xchaff, SatSolver
• registerKinds() : CVCL::Theory
• registerPrettyPrinter() : CVCL::ExprManager
• registerSubclass() : CVCL::ExprManager
• registerTheory() : CVCL::Theory
• registerTypeComputer() : CVCL::ExprManager
• registerUnit() : SAT::CD_CNF_Formula, SAT::CNF_Formula_Impl, SAT::CNF_Formula
• relToClosure() : CVCL::UFTheoremProducer, CVCL::UFProofRules
• relTrans() : CVCL::UFTheoremProducer, CVCL::UFProofRules
• renameExpr() : CVCL::TheoryArray
• replaceITE() : CVCL::SearchImplBase
• replaceITErec() : SAT::CNF_Manager
• reportResult() : CVCL::VCCmd
• reprocessFlags() : CVCL::VCL, CVCL::ValidityChecker
• Reset() : CVCL::Hash_Ptr< _Key, _Data >, CVCL::Dict_Ptr< _Key, _Data >, CVCL::SVC_API_impl, Xchaff, SatSolver, SatSolver::Clause, SatSolver::Lit, SatSolver::Var
• reset() : CVCL::DebugTime, CVCL::ExprStream, SAT::DPLLTBasic, CVCL::DebugTimer, SAT::CNF_Formula_Impl, SAT::Lit, SAT::Var
• resetDag() : CVCL::ExprStream
• resetIndent() : CVCL::ExprStream
• ResetVariable() : CVCL::SVC_API_impl
• Resize() : CVCL::Hash_Table< _Key, _Data >
• resolveID() : CVCL::Theory
• Restart() : Xchaff, SatSolver
• restart() : CSolver, CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• restart_backtrack_incr : CSolverParameters
• restart_backtrack_incr_incr : CSolverParameters
• restart_randomness : CSolverParameters
• restart_time_incr_incr : CSolverParameters
• restart_time_increment : CSolverParameters
• restartInternal() : CVCL::SearchSimple, CVCL::SearchImplBase, CVCL::SearchEngineFast
• restore() : CVCL::ContextObjChain, CVCL::Scope
• restoreData() : CVCL::ContextObj, CVCL::CDO< T >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMapOrderedData, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDMapData, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::CDList< T >, CVCL::CDFlags
• restoreDPLLT() : CVCL::SearchSat
• restoreIndent() : CVCL::ExprManager
• Restorer : CVCL::SearchSat::Restorer, CVCL::SearchSat
• Result : SAT::DPLLT
• resumeGC() : CVCL::VariableManager, CVCL::ExprManager
• returnFromCheck() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• returnFromSat() : SAT::DPLLTBasic, SAT::DPLLT
• rewrite() : CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• REWRITE_NORMAL : CVCL::Expr
• rewriteAnd() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteAndSubterms() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteAtomic() : CVCL::TheoryBitvector, CVCL::Theory
• rewriteAux() : CVCL::TheoryRecords, CVCL::TheoryBitvector
• rewriteBoolean() : CVCL::TheoryBitvector
• rewriteBV() : CVCL::TheoryBitvector
• rewriteCC() : CVCL::Theory
• rewriteConst() : CVCL::TheoryBitvector
• rewriteConstDef() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteCore() : CVCL::TheoryCore
• rewriteIff() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteImplies() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIte() : CVCL::TheoryCore
• rewriteIteBool() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteCond() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteElse() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteFalse() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteSame() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteThen() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteToAnd() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteToIff() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteToImp() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteToNot() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteToOr() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteIteTrue() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteLetDecl() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteLitCore() : CVCL::TheoryCore
• rewriteLiteral() : CVCL::TheoryCore
• rewriteLitSelect() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• rewriteLitUpdate() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• rewriteN() : CVCL::TheoryCore
• rewriteNotAnd() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteNotExists() : CVCL::QuantTheoremProducer, CVCL::QuantProofRules, CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotFalse() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotForall() : CVCL::QuantTheoremProducer, CVCL::QuantProofRules, CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotIff() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteNotIte() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteNotNot() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotOr() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteNotTrue() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteOpDef() : CVCL::UFTheoremProducer, CVCL::UFProofRules
• rewriteOr() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteOrSubterms() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• rewriteReadWrite() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteRedundantWrite1() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteRedundantWrite2() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteReflexivity() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteSameStore() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteSelCons() : CVCL::DatatypeTheoremProducer, CVCL::DatatypeProofRules
• rewriteTestCons() : CVCL::DatatypeTheoremProducer, CVCL::DatatypeProofRules
• rewriteToDiff() : CVCL::TheoryArith
• rewriteUpdateSelect() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• rewriteUsingSymmetry() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteWriteWrite() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rightMinusLeft() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• rightShiftToConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• run_periodic_functions() : CSolver
• RWTheoremValue : CVCL::RWTheoremValue, CVCL::TheoremValue

---