- g -

• garbageCollect() : CVC3::ContextMemoryManager
• gc() : CVC3::ExprManager , CVC3::VariableManager
• geExpr() : CVC3::ValidityChecker , CVC3::VCL
• generalBitBlast() : CVC3::TheoryBitvector
• generalIneqn() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• generalTrig() : CVC3::TheoryQuant
• generate_CDB() : SAT::DPLLTBasic
• get() : CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDO< T > , CDO< Theorem > , SmartCDO< T > , CDOmap< Expr, FreeConst > , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDFlags , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDO< T > , CVC3::SmartCDO< T >
• Get_ITEs() : CVC3::ExprTransform
• GetAckSwap() : CVC3::ExprTransform
• getActiveSolver() : SAT::DPLLTMiniSat
• getAntecedent() : CVC3::Variable , CVC3::VariableValue
• getAntecedentIdx() : CVC3::Variable , CVC3::VariableValue
• getAssumpThm() : CVC3::Variable , CVC3::VariableValue
• getAssumptions() : CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::VCL , CVC3::SearchImplBase , CVC3::SearchSat
• getAssumptionsAndCong() : CVC3::Theorem
• getAssumptionsAndCongRec() : CVC3::Theorem
• getAssumptionsRec() : CVC3::VCL , CVC3::Theorem
• getAssumptionsRef() : CVC3::Theorem , CVC3::RWTheoremValue , CVC3::Theorem3 , CVC3::TheoremValue , CVC3::RegTheoremValue
• getAssumptionsTCC() : CVC3::ValidityChecker , CVC3::VCL
• getAssumptionsUsed() : CVC3::ValidityChecker , CVC3::VCL , CVC3::SearchImplBase
• getBaseType() : CVC3::Theory , CVC3::ValidityChecker , CVC3::VCL
• getBeta() : CVC3::TheoryArithNew
• getBitvectorTypeParam() : CVC3::TheoryBitvector
• getBody() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprClosure
• getBool() : CVC3::CLFlag
• getBoolExtractIndex() : CVC3::TheoryBitvector
• getBottomScope() : CVC3::SearchImplBase , CVC3::SearchSat
• getBoundIndex() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprSkolem
• getBucketByIndex() : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• getBucketByKey() : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• getBucketIndex() : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• GetBudgetUsed() : SatSolver
• getBVConstSize() : CVC3::TheoryBitvector
• getBVConstValue() : CVC3::TheoryBitvector
• getBVIndex() : CVC3::TheoryBitvector
• getBVMultParam() : CVC3::TheoryBitvector
• getBVPlusParam() : CVC3::TheoryBitvector
• getBVs() : CVC3::Trigger
• getCachedValue() : CVC3::Theorem , CVC3::TheoremManager , CVC3::TheoremValue
• GetClause() : SatSolver
• GetClauseLits() : SatSolver
• getClauses() : MiniSat::Solver
• getClauseTheorem() : SAT::Clause
• getClosure() : CVC3::ValidityChecker , CVC3::VCL
• getCM() : CVC3::TheoremManager , CVC3::Context , CVC3::TheoryCore , CVC3::ExprManager , CVC3::VariableManager
• getCMM() : CVC3::Scope , CDList< T > , CDOmap< Key, Data, HashFcn > , CDMap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDMapOrdered< Key, Data > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDO< T > , iterator , CDList< Theorem > , CDO< Theorem > , CDMap< Expr, Theorem > , iterator , CDList< Expr > , const_iterator , CVC3::ContextObj , iterator , CDOmap< Expr, FreeConst > , iterator , CDList< Ineq > , iterator , CDMap< Expr, bool > , CDMap< Expr, CDList< dynTrig > , iterator , CDList< dynTrig > , CDList< size_t > , CDList< size_t > size_t
• getCNFLit() : SAT::CNF_Manager
• getCommonRules() : CVC3::Theory , CVC3::SearchEngine
• getConcreteModel() : CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::VCL
• getConflictLevel() : MiniSat::Solver
• getConsForTester() : CVC3::TheoryDatatype
• getConsPos() : CVC3::TheoryDatatype
• getConst() : CVC3::TheoryArithNew::FreeConst , CVC3::TheoryArith3::FreeConst , CVC3::TheoryArith3::Ineq , CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::FreeConst , CVC3::TheoryArithOld::Ineq
• getConstant() : CVC3::TheoryDatatype
• getContext() : CVC3::Scope
• getCoreRules() : CVC3::TheoryCore
• getCounterExample() : CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::SearchEngineFast , CVC3::VCL , CVC3::SearchImplBase , CVC3::SearchSat
• getCurAssignments() : SAT::DPLLT , SAT::DPLLTBasic , SAT::DPLLTMiniSat
• getCurClauses() : SAT::DPLLT , SAT::DPLLTBasic , SAT::DPLLTMiniSat
• getCurQuantLevel() : CVC3::TheoryCore
• getCurrentClause() : SAT::CNF_Formula
• getCurrentContext() : CVC3::ContextManager , CVC3::ExprManager , CVC3::ValidityChecker , CVC3::VCL
• getDenominator() : CVC3::Rational
• getDerivation() : MiniSat::Solver
• getEdge() : CVC3::TheoryArithOld::DifferenceLogicGraph
• getEdgeTheorems() : CVC3::TheoryArithOld::DifferenceLogicGraph
• getEdgeWeight() : CVC3::TheoryArithOld::DifferenceLogicGraph
• getEM() : CVC3::Expr , CVC3::Theory , CVC3::TheoremManager , CVC3::ValidityChecker , CVC3::VCL
• getEmptyVector() : CVC3::ExprManager
• getEpsilon() : CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational
• getEqNext() : CVC3::Expr
• getEx() : CVC3::Trigger
• getExistential() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprSkolem
• getExpandFlag() : CVC3::Theorem , CVC3::TheoremManager , CVC3::TheoremValue
• getExplanation() : SAT::DPLLT::TheoryAPI , CVC3::SearchSat , CVC3::SearchSatTheoryAPI
• getExpr() : CVC3::Theorem3 , CVC3::NotifyList , CVC3::Proof , CVC3::Type , CVC3::Variable , CVC3::Literal , CVC3::VariableValue , CVC3::Op , CVC3::Theorem , CVC3::TheoremValue , CVC3::RWTheoremValue
• getExprScore() : CVC3::TheoryQuant
• getExprTrans() : CVC3::TheoryCore
• getExprValue() : CVC3::BVConstExpr , CVC3::Expr , CVC3::ExprValue
• getExtractHi() : CVC3::TheoryBitvector
• getExtractLow() : CVC3::TheoryBitvector
• getFactors() : CVC3::TheoryArith3 , CVC3::TheoryArithOld
• getFalse() : SAT::Lit
• getFanin() : SAT::CNF_Manager
• getFanout() : SAT::CNF_Manager
• getField() : CVC3::RecordsTheoremProducer , CVC3::ExprValue , CVC3::TheoryRecords
• getFieldIndex() : CVC3::RecordsTheoremProducer , CVC3::TheoryRecords
• getFields() : CVC3::RecordsTheoremProducer , CVC3::ExprValue , CVC3::TheoryRecords
• getFind() : CVC3::Expr
• getFindLevel() : CVC3::Expr
• getFirst() : CVC3::Assumptions
• GetFirstClause() : SatSolver
• GetFirstVar() : SatSolver
• getFixedLeftShiftParam() : CVC3::TheoryBitvector
• getFixedRightShiftParam() : CVC3::TheoryBitvector
• getFlag() : CVC3::TheoremManager , CVC3::Expr , CVC3::ExprManager , CVC3::CLFlags
• getFlag0() : CVC3::CLFlags
• getFlags() : CVC3::TheoremManager , CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::VCL
• getFloor() : CVC3::TheoryArithNew::EpsRational , CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational
• GetFormulaMap() : CVC3::ExprTransform
• GetGTerms2() : CVC3::ExprTransform
• getHead() : CVC3::Trigger , CVC3::TheoryQuant
• getHeadExpr() : CVC3::TheoryQuant
• getHelp() : CVC3::CLFlag
• getID() : SAT::Lit
• getImplication() : SAT::DPLLT::TheoryAPI , CVC3::SearchSat , CVC3::SearchSatTheoryAPI
• getImplicationLevel() : MiniSat::Solver
• getImpliedLiteral() : CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::VCL , CVC3::SearchImplBase , CVC3::SearchSat
• getImpliedLiteralByIndex() : CVC3::TheoryCore
• getIndex() : CVC3::Expr , CVC3::RecordsTheoremProducer , CVC3::TheoryRecords , SAT::Var
• getInputLang() : CVC3::ExprManager
• getInt() : CVC3::Rational , CVC3::CLFlag
• getInternalAssumptions() : CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::VCL , CVC3::SearchImplBase , CVC3::SearchSat
• getIsAtomicFlag() : CVC3::Expr
• getKey() : CDOmap< Key, Data, HashFcn > new , CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDOmap< Key, Data, HashFcn > , CDOmap< Expr, FreeConst >
• getKids() : CVC3::ExprNode , CVC3::Expr , CVC3::ExprNodeTmp , CVC3::ExprValue
• getKids1() : CVC3::ExprNode
• getKind() : CVC3::Expr , CVC3::ExprManager , CVC3::Op , CVC3::ExprValue
• getKindName() : CVC3::ExprManager
• getLeaf() : SAT::SatProofNode
• getLeafAssumptions() : CVC3::Theorem
• getLeaves() : CVC3::ArithTheoremProducerOld
• getLeftParent() : SAT::SatProofNode
• getLemmas() : MiniSat::Solver
• getLevel() : MiniSat::Solver
• getLHS() : CVC3::Theorem3 , CVC3::Theorem , CVC3::TheoremValue , CVC3::RWTheoremValue
• getLit() : CVC3::SearchSat::LitPriorityPair , SAT::SatProofNode
• getLiteral() : CVC3::Clause
• getLiterals() : CVC3::Clause
• getLitFlag() : CVC3::Theorem , CVC3::TheoremManager , CVC3::TheoremValue
• getLowerBound() : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• getLowerBoundExplanation() : CVC3::TheoryArithNew
• getLowerBoundThm() : CVC3::TheoryArithNew
• GetMaxDLevel() : SatSolver
• getMaxSize() : CVC3::TheoryBitvector
• getMaxVar() : SAT::Clause
• getMemory() : CVC3::Scope , CVC3::Context , CVC3::ContextManager , CVC3::ContextNotifyObj , CVC3::ContextMemoryManager , CVC3::ExprManager , CVC3::ExprManagerNotifyObj , CVC3::VCL
• GetMemUsed() : SatSolver
• getMin() : MiniSat::Heap< C >
• getMM() : CVC3::RWTheoremValue , CVC3::TheoremManager , CVC3::ExprManager , CVC3::ExprValue , CVC3::TheoremValue , CVC3::RegTheoremValue
• getMMIndex() : CVC3::BVConstExpr , CVC3::ExprNode , CVC3::ExprApply , CVC3::ExprString , CVC3::Expr , CVC3::ExprSkolem , CVC3::ExprRational , CVC3::ExprVar , CVC3::ExprSymbol , CVC3::ExprBoundVar , CVC3::ExprClosure , CVC3::ExprValue , CVC3::ExprNodeTmp , CVC3::ExprApplyTmp
• getModelTerm() : CVC3::Theory
• getModelValue() : CVC3::Theory , CVC3::TheoryCore
• getName() : CVC3::ExprValue , CVC3::Theory , CVC3::SearchSimple , CVC3::ExprVar , CVC3::ExprSymbol , CVC3::ExprBoundVar , CVC3::SearchEngine , CVC3::SearchEngineFast , CVC3::SearchSat , CVC3::Expr
• getNegExpr() : CVC3::VariableValue , CVC3::Variable
• getNewClauses() : SAT::DPLLT::TheoryAPI , CVC3::SearchSat , CVC3::SearchSatTheoryAPI
• GetNextClause() : SatSolver
• GetNextVar() : SatSolver
• getNodeProof() : SAT::SatProofNode
• getNotify() : CVC3::Expr
• getNullExpr() : CVC3::ExprManager
• GetNumConflicts() : SatSolver
• GetNumDecisions() : SatSolver
• GetNumDeletedClauses() : SatSolver
• GetNumDeletedLiterals() : SatSolver
• getNumerator() : CVC3::Rational
• GetNumExtConflicts() : SatSolver
• GetNumImplications() : SatSolver
• GetNumLiterals() : SatSolver
• getNumTheories() : CVC3::Theory
• getOp() : CVC3::ExprValue , CVC3::Expr , CVC3::ExprApplyTmp , CVC3::ExprApply
• getOpExpr() : CVC3::Expr
• getOpKind() : CVC3::Expr
• GetOrderedTerms() : CVC3::ExprTransform
• GetOrdering() : CVC3::ExprTransform
• getOutputLang() : CVC3::ExprManager
• GetPEqs() : CVC3::ExprTransform
• GetPhaseFromLit() : SatSolver
• getPlusTerms() : CVC3::BitvectorTheoremProducer
• getPredicates() : CVC3::TheoryCore
• getPrinter() : CVC3::ExprManager
• getPriority() : CVC3::SearchSat::LitPriorityPair
• getPrompt() : CVC3::ParserTemp
• getProof() : CVC3::Theorem , CVC3::Theorem3 , CVC3::SearchImplBase , MiniSat::Solver , CVC3::VCL , SAT::DPLLTMiniSat , CVC3::SearchSat , CVC3::SearchEngine , CVC3::TheoremValue , CVC3::ValidityChecker
• getProofClosure() : CVC3::ValidityChecker , CVC3::VCL
• getProofQuery() : CVC3::ValidityChecker , CVC3::VCL
• getProofTCC() : CVC3::ValidityChecker , CVC3::VCL
• getPushID() : MiniSat::Solver
• getQuantLevel() : CVC3::Theorem , CVC3::TheoremValue
• getQuantLevelDebug() : CVC3::Theorem , CVC3::TheoremValue
• getQuantLevelForTerm() : CVC3::TheoryCore
• getRational() : CVC3::ExprValue , CVC3::Expr , CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational , CVC3::ExprRational , CVC3::TheoryArithNew::EpsRational
• getReachablePredicate() : CVC3::TheoryDatatype
• getReason() : MiniSat::Solver
• getRep() : CVC3::ExprNode , CVC3::Expr , CVC3::ExprValue
• getResource() : CVC3::TheoryCore
• getResourceLimit() : CVC3::TheoryCore
• getRestore() : CDOmap< Key, Data, HashFcn > new , iterator , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , iterator , CDOmap< Expr, FreeConst > , CDMap< Expr, Theorem > , CDList< Theorem > , iterator , CDMap< Expr, bool > , CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > , CDList< size_t > , CDMap< Key, Data, HashFcn > , iterator , CDList< dynTrig > , CDMapOrdered< Key, Data > , iterator , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , iterator , CDMap< Expr, CDList< dynTrig > , iterator , const_iterator , iterator , CDList< Expr > , CVC3::ContextObj , CDList< T > , CDList< size_t > size_t , CDO< T > , CDO< Theorem > , CDList< Ineq >
• getRHS() : CVC3::Theorem3 , CVC3::Theorem , CVC3::TheoremValue , CVC3::RWTheoremValue
• getRightParent() : SAT::SatProofNode
• getRoot() : SAT::SatProof
• getRules() : CVC3::VariableManager , CVC3::TheoremManager
• getRWMM() : CVC3::TheoremManager
• GetSatAssumptions() : CVC3::Theorem
• GetSatAssumptionsRec() : CVC3::Theorem
• getSatProof() : SAT::DPLLTMiniSat , SAT::DPLLT , SAT::DPLLTBasic
• GetSATTime() : SatSolver
• getScope() : CVC3::Theorem3 , CVC3::Variable , CVC3::Theorem , CVC3::Literal , CVC3::VariableValue , CVC3::Clause , CVC3::TheoremValue
• getSelectorInfo() : CVC3::TheoryDatatype
• getSig() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprNode
• getSimpCache() : CVC3::Expr
• getSimpCacheTag() : CVC3::ExprManager
• getSize() : CVC3::Expr , CVC3::ExprValue
• getSkolemAxioms() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• getSmartClauses() : CVC3::CNF_TheoremProducer
• GetSortedOpVec() : CVC3::ExprTransform
• getStart() : MiniSat::Inference
• getStaticMemory() : CVC3::ContextMemoryManager
• getStatistics() : CVC3::TheoryCore , CVC3::VCL , CVC3::ValidityChecker
• getStats() : MiniSat::Solver
• getSteps() : MiniSat::Inference
• getString() : CVC3::ExprValue , CVC3::Expr , CVC3::ExprString , CVC3::CLFlag
• getStrVec() : CVC3::CLFlag
• GetSub_vec() : CVC3::ExprTransform
• getSubTerms() : CVC3::TheoryQuant
• getSXIndex() : CVC3::TheoryBitvector
• getTableauxEntry() : CVC3::TheoryArithNew
• getTCC() : CVC3::VCL , CVC3::Theory , CVC3::ValidityChecker
• getTerminalsConstFlag() : CVC3::Expr
• getTerms() : CVC3::TheoryCore
• getTheorem() : MiniSat::Clause , CVC3::VariableValue , CVC3::Expr , CVC3::Literal , CVC3::ExprValue , CVC3::Variable , CVC3::Clause
• getTheoremForTerm() : CVC3::TheoryCore
• getTheory() : CVC3::NotifyList
• getTM() : CVC3::TheoryCore , CVC3::ExprManager
• GetTotalTime() : SatSolver
• getTrail() : MiniSat::Solver
• getTranslator() : CVC3::TheoryCore
• getTriggers() : CVC3::ExprClosure , CVC3::ExprValue , CVC3::Expr
• getTrue() : SAT::Lit
• getTupleIndex() : CVC3::ExprValue
• getType() : CVC3::Expr , CVC3::CLFlag , CVC3::ValidityChecker , CVC3::VCL
• getTypePred() : CVC3::Theory , CVC3::ValidityChecker , CVC3::VCL
• getTypePredExpr() : CVC3::TheoryBitvector
• getTypePredType() : CVC3::TheoryBitvector
• getUid() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprBoundVar
• getUnsatTheorem() : CVC3::TheoryArithOld::DifferenceLogicGraph
• getUnsigned() : CVC3::Rational
• getUpperBound() : CVC3::TheoryArithOld , CVC3::TheoryArithNew
• getUpperBoundExplanation() : CVC3::TheoryArithNew
• getUpperBoundThm() : CVC3::TheoryArithNew
• getUserAssumptions() : CVC3::SearchEngine , CVC3::ValidityChecker , CVC3::SearchSat , CVC3::VCL , CVC3::SearchImplBase
• getValuation() : CVC3::TheoryArithOld::DifferenceLogicGraph
• getValue() : CVC3::SearchEngine , CVC3::SearchSat , SAT::DPLLTBasic , CVC3::SearchSat , CVC3::Literal , CVC3::BVConstExpr , SAT::DPLLT , CVC3::Variable , CVC3::SearchImplBase , CVC3::VariableValue , MiniSat::Solver , SAT::DPLLTMiniSat , MiniSat::Solver , CVC3::SearchSat
• getVar() : SAT::Lit
• GetVar() : SatSolver
• getVar() : CVC3::ExprValue , CVC3::Literal
• GetVarAssignment() : SatSolver
• GetVarFromLit() : SatSolver
• getVariableIntroThm() : CVC3::TheoryArithNew
• getVariables() : CVC3::TheoryArithOld::DifferenceLogicGraph
• GetVarIndex() : SatSolver
• getVars() : CVC3::Expr , CVC3::ExprClosure , CVC3::ExprValue
• getVerticesTopological() : CVC3::TheoryArithOld::VarOrderGraph
• getWatches() : MiniSat::Solver
• goalSatisfied() : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF , CVC3::DecisionEngineDFS , CVC3::DecisionEngine
• goodSynMatch() : CVC3::TheoryQuant
• goodSynMatchNewTrig() : CVC3::TheoryQuant
• grayShadow() : CVC3::TheoryArith , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3
• grayShadowConst() : CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer
• greaterthan() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• grow() : vec< T > , MiniSat::vec< T >
• growTo() : MiniSat::vec< T > , vec< T > , MiniSat::vec< T > , vec< T >
• gtExpr() : CVC3::ValidityChecker , CVC3::VCL

---