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

- g -

• gc() : CVCL::VariableManager, CVCL::ExprManager
• gcd : CVCL::Rational::Impl, CVCL::Rational
• geExpr() : CVCL::VCL, CVCL::ValidityChecker
• generalIneqn() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• generate_CDB() : SAT::DPLLTBasic
• get() : CVCL::SmartCDO< T >, CVCL::CDO< T >, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::CDFlags
• get_antecedence() : CVariable
• get_clause_index() : CLitPoolElement
• getAntecedent() : CVCL::VariableValue, CVCL::Variable
• getAntecedentIdx() : CVCL::VariableValue, CVCL::Variable
• getAssumpThm() : CVCL::VariableValue, CVCL::Variable
• getAssumptions() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theorem3, CVCL::Theorem, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• getAssumptionsCopy() : CVCL::Theorem3, CVCL::Theorem
• getAssumptionsRec() : CVCL::VCL, CVCL::Theorem
• getAssumptionsRef() : CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• getAssumptionsTCC() : CVCL::VCL, CVCL::ValidityChecker
• getAssumptionsUsed() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchImplBase
• getBaseType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory
• getBitvectorTypeParam() : CVCL::TheoryBitvector
• getBody() : CVCL::ExprClosure, CVCL::ExprValue, CVCL::Expr
• getBool() : CVCL::CLFlag
• getBoolExtractIndex() : CVCL::TheoryBitvector
• getBottomScope() : CVCL::SearchSatCoreSatAPI, CVCL::CoreSatAPI_implBase, CVCL::TheoryCore::CoreSatAPI, CVCL::SearchSat, CVCL::SearchImplBase
• getBoundIndex() : CVCL::ExprSkolem, CVCL::ExprValue, CVCL::Expr
• GetBudgetUsed() : Xchaff, SatSolver
• getBVConstSize() : CVCL::TheoryBitvector
• getBVConstValue() : CVCL::TheoryBitvector
• getBVMultParam() : CVCL::TheoryBitvector
• getBVPlusParam() : CVCL::TheoryBitvector
• getCachedValue() : CVCL::TheoremValue, CVCL::Theorem
• GetClause() : Xchaff, SatSolver
• GetClauseLits() : Xchaff, SatSolver
• getClosure() : CVCL::VCL, CVCL::ValidityChecker
• getCM() : CVCL::VariableManager, CVCL::TheoryCore, CVCL::TheoremManager, CVCL::ExprManager, CVCL::Context
• getCNFLit() : SAT::CNF_Manager
• getCommonRules() : CVCL::Theory
• getConcreteModel() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchEngine
• GetConfClause() : CVCL::SVC_API_impl
• getConsForTester() : CVCL::TheoryDatatype
• getConsPos() : CVCL::TheoryDatatype
• getConst() : CVCL::TheoryArith::Ineq, CVCL::TheoryArith::FreeConst
• getConstant() : CVCL::TheoryDatatype
• getCoreRules() : CVCL::TheoryCore
• getCounterExample() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngineFast, CVCL::SearchEngine
• getCreated() : CVCL::Rational
• getCurrentClause() : SAT::CNF_Formula
• getCurrentContext() : CVCL::VCL, CVCL::ValidityChecker, CVCL::ExprManager, CVCL::ContextManager
• getDeleted() : CVCL::Rational
• getDen() : CVCL::Rational::Impl
• getDenominator() : CVCL::Rational
• getE0() : CVCL::TheoryCore
• getE1() : CVCL::TheoryCore
• getEM() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory, CVCL::TheoremManager, CVCL::Expr
• getEmptyVector() : CVCL::ExprManager
• getExistential() : CVCL::ExprSkolem, CVCL::ExprValue, CVCL::Expr
• getExpandFlag() : CVCL::TheoremValue, CVCL::Theorem
• getExplanation() : CVCL::SearchSatTheoryAPI, CVCL::SearchSat, SAT::DPLLT::TheoryAPI
• getExpr() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::Type, CVCL::Theorem3, CVCL::Theorem, CVCL::Proof, CVCL::NotifyList, CVCL::Op
• getExprTrans() : CVCL::TheoryCore
• getExprValue() : CVCL::BVConstExpr, CVCL::ExprValue, CVCL::Expr
• getExtractHi() : CVCL::TheoryBitvector
• getExtractLow() : CVCL::TheoryBitvector
• getFalse() : SAT::Lit
• getFanin() : SAT::CNF_Manager
• getFanout() : SAT::CNF_Manager
• getField() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords, CVCL::ExprValue
• getFieldIndex() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• getFields() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords, CVCL::ExprValue
• getFind() : CVCL::Expr
• GetFirstClause() : Xchaff, SatSolver
• GetFirstVar() : Xchaff, SatSolver
• getFixedLeftShiftParam() : CVCL::TheoryBitvector
• getFixedRightShiftParam() : CVCL::TheoryBitvector
• getFlag() : CVCL::TheoremManager, CVCL::ExprManager, CVCL::Expr, CVCL::CLFlags
• getFlag0() : CVCL::CLFlags
• getFlags() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::TheoremManager
• getHead() : CVCL::TheoryQuant
• getHeight() : CVCL::ExprValue, CVCL::Expr
• getHelp() : CVCL::CLFlag
• getHighestKid() : CVCL::ExprValue, CVCL::Expr
• getID() : SAT::Lit
• getId() : SAT::Clause
• getImplication() : CVCL::SearchSatTheoryAPI, CVCL::SearchSat, SAT::DPLLT::TheoryAPI
• GetImplications() : CVCL::SVC_API_impl
• GetImplicationsRec() : CVCL::SVC_API_impl
• getImpliedLiteral() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• getImpliedLiteralByIndex() : CVCL::TheoryCore
• getIndex() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords, CVCL::Expr, SAT::Var
• getInputLang() : CVCL::ExprManager
• getInt() : CVCL::Rational::Impl, CVCL::Rational, CVCL::CLFlag
• getInternalAssumptions() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• getIsAtomicFlag() : CVCL::Expr
• getKey() : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• getKids() : CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• getKind() : CVCL::ExprValue, CVCL::Op, CVCL::ExprManager, CVCL::Expr
• getKindName() : CVCL::ExprManager
• getLangUsed() : CVCL::TheoryArith
• getLeafAssumptions() : CVCL::Theorem
• getLHS() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• getLiteral() : CVCL::Clause
• getLiterals() : CVCL::Clause
• getLitFlag() : CVCL::TheoremValue, CVCL::Theorem
• GetMaxDLevel() : Xchaff, SatSolver
• getMaxVar() : SAT::Clause
• GetMemUsed() : Xchaff, SatSolver
• getMM() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::TheoremManager, CVCL::ExprValue, CVCL::ExprManager
• getMMIndex() : CVCL::BVConstExpr, CVCL::ExprClosure, CVCL::ExprBoundVar, CVCL::ExprSymbol, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprApply, CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• getModelTerm() : CVCL::Theory
• getModelValue() : CVCL::TheoryCore, CVCL::Theory
• getName() : CVCL::Theory, CVCL::SearchSimple, CVCL::SearchSat, CVCL::SearchEngineFast, CVCL::SearchEngine, CVCL::ExprBoundVar, CVCL::ExprSymbol, CVCL::ExprVar, CVCL::Expr
• getNeg() : CVCL::ExprTransform
• getNegExpr() : CVCL::VariableValue, CVCL::Variable
• getNewClauses() : CVCL::SearchSatTheoryAPI, CVCL::SearchSat, SAT::DPLLT::TheoryAPI
• GetNextClause() : Xchaff, SatSolver
• GetNextVar() : Xchaff, SatSolver
• getNotify() : CVCL::Expr
• getNullExpr() : CVCL::ExprManager
• getNum() : CVCL::Rational::Impl
• GetNumConflicts() : Xchaff, SatSolver
• GetNumDecisions() : Xchaff, SatSolver
• GetNumDeletedClauses() : Xchaff, SatSolver
• GetNumDeletedLiterals() : Xchaff, SatSolver
• getNumerator() : CVCL::Rational
• GetNumExtConflicts() : Xchaff, SatSolver
• GetNumImplications() : Xchaff, SatSolver
• GetNumLiterals() : Xchaff, SatSolver
• getNumTheories() : CVCL::Theory
• getOp() : CVCL::ExprApply, CVCL::ExprValue, CVCL::Expr
• getOpExpr() : CVCL::Expr
• getOpKind() : CVCL::Expr
• getOS() : CVCL::Debug
• getOSDumpTrace() : CVCL::Debug
• getOutputLang() : CVCL::ExprManager
• getParent() : CVCL::ExprStream
• GetPhaseFromLit() : Xchaff, SatSolver
• getPrinter() : CVCL::ExprManager
• getPrompt() : CVCL::ParserTemp
• getProof() : CVCL::TheoremValue, CVCL::VCL, CVCL::ValidityChecker, CVCL::Theorem3, CVCL::Theorem, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• getProofClosure() : CVCL::VCL, CVCL::ValidityChecker
• getProofTCC() : CVCL::VCL, CVCL::ValidityChecker
• getRational() : CVCL::ExprRational, CVCL::ExprValue, CVCL::Expr
• getReachablePredicate() : CVCL::TheoryDatatype
• getReflMM() : CVCL::TheoremManager
• getRep() : CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• getResource() : CVCL::TheoryCore
• getRHS() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• getRules() : CVCL::VariableManager, CVCL::TheoremManager
• getRWMM() : CVCL::TheoremManager
• GetSATTime() : Xchaff, SatSolver
• getScope() : CVCL::TheoremValue, CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::Theorem3, CVCL::Theorem, CVCL::Clause
• getSelectorInfo() : CVCL::TheoryDatatype
• getSig() : CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• getSimpCache() : CVCL::Expr
• getSimpCacheTag() : CVCL::ExprManager
• getSimpFrom() : CVCL::ExprValue, CVCL::Expr
• getSkolemAxioms() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• getStatistics() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore
• getString() : CVCL::ExprString, CVCL::ExprValue, CVCL::Expr, CVCL::CLFlag
• getStrVec() : CVCL::CLFlag
• getSXIndex() : CVCL::TheoryBitvector
• getTCC() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory
• getTerms() : CVCL::TheoryCore
• getTheorem() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::Clause
• getTheory() : CVCL::NotifyList
• getTM() : CVCL::TheoryCore
• GetTotalTime() : Xchaff, SatSolver
• getTrue() : SAT::Lit
• getTupleIndex() : CVCL::ExprValue
• getType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr, CVCL::CLFlag
• getTypePred() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory
• getTypePredExpr() : CVCL::TheoryBitvector
• getTypePredType() : CVCL::TheoryBitvector
• getUid() : CVCL::ExprBoundVar, CVCL::ExprValue, CVCL::Expr
• getUnsigned() : CVCL::Rational::Impl, CVCL::Rational
• getUserAssumptions() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• getValue() : CVCL::BVConstExpr, CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::SearchSat, SAT::DPLLTBasic, SAT::DPLLT
• GetVar() : Xchaff, SatSolver
• getVar() : CVCL::Literal, CVCL::ExprValue, SAT::Lit
• GetVarAssignment() : Xchaff, SatSolver
• GetVarFromLit() : Xchaff, SatSolver
• GetVarIndex() : Xchaff, SatSolver
• getVars() : CVCL::ExprClosure, CVCL::ExprValue, CVCL::Expr
• goalSatisfied() : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineDFS, CVCL::DecisionEngineCaching, CVCL::DecisionEngine
• goodSynMatch() : CVCL::TheoryQuant
• grayShadow() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• grayShadowConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• greaterthan() : CVCL::ArithTheoremProducer
• gtExpr() : CVCL::VCL, CVCL::ValidityChecker

---