- g -

• garbageCollect() : CVC3::ContextMemoryManager
• gc() : CVC3::ExprManager , CVC3::VariableManager
• geExpr() : CVC3::ValidityChecker , CVC3::VCL
• generalIneqn() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• generalTrig() : CVC3::TheoryQuant
• generate_CDB() : SAT::DPLLTBasic
• get() : 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::CDFlags , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CVC3::SmartCDO< T > , CVC3::CDO< T > , CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new
• get_antecedence() : CVariable
• get_clause_index() : CLitPoolElement
• getActiveSolver() : SAT::DPLLTMiniSat
• getAntecedent() : CVC3::Variable , CVC3::VariableValue
• getAntecedentIdx() : CVC3::Variable , CVC3::VariableValue
• getAssumpThm() : CVC3::Variable , CVC3::VariableValue
• getAssumptions() : CVC3::SearchEngine , CVC3::ValidityChecker , CVC3::SearchImplBase , CVC3::VCL , CVC3::SearchSat
• getAssumptionsRec() : CVC3::VCL , CVC3::Theorem
• getAssumptionsRef() : CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue , CVC3::RegTheoremValue , CVC3::RWTheoremValue
• getAssumptionsTCC() : CVC3::ValidityChecker , CVC3::VCL
• getAssumptionsUsed() : CVC3::ValidityChecker , CVC3::VCL , CVC3::SearchImplBase
• getBaseType() : CVC3::ValidityChecker , CVC3::VCL , CVC3::Theory
• getBeta() : CVC3::TheoryArithNew
• getBitvectorTypeParam() : CVC3::TheoryBitvector
• getBody() : CVC3::ExprClosure , CVC3::ExprValue , CVC3::Expr
• getBool() : CVC3::CLFlag
• getBoolExtractIndex() : CVC3::TheoryBitvector
• getBottomScope() : CVC3::SearchImplBase , CVC3::SearchSat
• getBoundIndex() : CVC3::ExprSkolem , CVC3::ExprValue , CVC3::Expr
• 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 , Xchaff
• getBVConstSize() : CVC3::TheoryBitvector
• getBVConstValue() : CVC3::TheoryBitvector
• getBVIndex() : CVC3::TheoryBitvector
• getBVMultParam() : CVC3::TheoryBitvector
• getBVPlusParam() : CVC3::TheoryBitvector
• getBVs() : CVC3::Trigger
• getCachedValue() : CVC3::Theorem , CVC3::TheoremValue , CVC3::TheoremManager
• GetClause() : SatSolver , Xchaff
• GetClauseLits() : SatSolver , Xchaff
• getClauses() : MiniSat::Solver
• getClosure() : CVC3::ValidityChecker , CVC3::VCL
• getCM() : CVC3::Context , CVC3::TheoryCore , CVC3::ExprManager , CVC3::VariableManager , CVC3::TheoremManager
• getCMM() : CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDMapOrdered< Key, Data > , CDOmapOrdered< Key, Data > , CVC3::ContextObj , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDO< T > , iterator , CDList< Theorem > , CDO< Theorem > , iterator , CDList< Expr > , CDMap< Expr, Theorem > , const_iterator , CDList< Ineq > , iterator , CDOmap< Expr, FreeConst > , CDMap< Expr, bool > , CDMap< Expr, CDList< dynTrig > , iterator , CDList< dynTrig > , vector< Expr > , CDList< size_t > , CDList< size_t > size_t , CVC3::Scope , CDList< T > , CDMap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new
• getCNFLit() : SAT::CNF_Manager
• getCommonRules() : CVC3::SearchEngine , CVC3::Theory
• getConcreteModel() : CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::VCL
• getConflictLevel() : MiniSat::Solver
• getConsForTester() : CVC3::TheoryDatatype
• getConsPos() : CVC3::TheoryDatatype
• getConst() : CVC3::TheoryArithNew::FreeConst , CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithNew::FreeConst , 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::SearchImplBase , CVC3::VCL , CVC3::SearchSat
• getCurrentClause() : SAT::CNF_Formula
• getCurrentContext() : CVC3::ContextManager , CVC3::ExprManager , CVC3::ValidityChecker , CVC3::VCL
• getDenominator() : CVC3::Rational
• getDerivation() : MiniSat::Solver
• getEM() : CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoremManager , CVC3::Expr , CVC3::Theory
• getEmptyVector() : CVC3::ExprManager
• getEx() : CVC3::Trigger
• getExistential() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprSkolem
• getExpandFlag() : CVC3::Theorem , CVC3::TheoremValue , CVC3::TheoremManager
• getExplanation() : SAT::DPLLT::TheoryAPI , CVC3::SearchSat , CVC3::SearchSatTheoryAPI
• getExpr() : CVC3::NotifyList , CVC3::Proof , CVC3::Type , CVC3::Variable , CVC3::Literal , CVC3::VariableValue , CVC3::Op , CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue , CVC3::RWTheoremValue
• getExprScore() : CVC3::TheoryQuant
• getExprTrans() : CVC3::TheoryCore
• getExprValue() : CVC3::ExprValue , CVC3::Expr , CVC3::BVConstExpr
• getExtractHi() : CVC3::TheoryBitvector
• getExtractLow() : CVC3::TheoryBitvector
• getFalse() : SAT::Lit
• getFanin() : SAT::CNF_Manager
• getFanout() : SAT::CNF_Manager
• getField() : CVC3::TheoryRecords , CVC3::ExprValue , CVC3::RecordsTheoremProducer
• getFieldIndex() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
• getFields() : CVC3::TheoryRecords , CVC3::ExprValue , CVC3::RecordsTheoremProducer
• getFind() : CVC3::Expr
• getFindLevel() : CVC3::Expr
• getFirst() : CVC3::Assumptions
• GetFirstClause() : SatSolver , Xchaff
• GetFirstVar() : SatSolver , Xchaff
• getFixedLeftShiftParam() : CVC3::TheoryBitvector
• getFixedRightShiftParam() : CVC3::TheoryBitvector
• getFlag() : CVC3::Expr , CVC3::ExprManager , CVC3::CLFlags , CVC3::TheoremManager
• getFlag0() : CVC3::CLFlags
• getFlags() : CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoremManager
• getFloor() : CVC3::TheoryArithNew::EpsRational
• getHead() : CVC3::Trigger
• getHelp() : CVC3::CLFlag
• getId() : SAT::Clause
• getID() : SAT::Lit
• getImplication() : SAT::DPLLT::TheoryAPI , CVC3::SearchSat , CVC3::SearchSatTheoryAPI
• getImplicationLevel() : MiniSat::Solver
• getImpliedLiteral() : CVC3::TheoryCore , CVC3::SearchEngine , CVC3::ValidityChecker , CVC3::SearchImplBase , CVC3::VCL , CVC3::SearchSat
• getImpliedLiteralByIndex() : CVC3::TheoryCore
• getIndex() : CVC3::TheoryRecords , SAT::Var , CVC3::RecordsTheoremProducer , CVC3::Expr
• getInputLang() : CVC3::ExprManager
• getInt() : CVC3::Rational , CVC3::CLFlag
• getInternalAssumptions() : CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::VCL , CVC3::SearchSat
• getIsAtomicFlag() : CVC3::Expr
• getKey() : CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDOmap< Expr, FreeConst > , CDOmap< Key, Data, HashFcn > new , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn >
• getKids() : CVC3::ExprValue , CVC3::ExprNode , CVC3::ExprNodeTmp , CVC3::Expr
• getKids1() : CVC3::ExprNode
• getKind() : CVC3::ExprManager , CVC3::Op , CVC3::ExprValue , CVC3::Expr
• getKindName() : CVC3::ExprManager
• getLeafAssumptions() : CVC3::Theorem
• getLemmas() : MiniSat::Solver
• getLevel() : MiniSat::Solver
• getLHS() : CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue , CVC3::RWTheoremValue
• getLit() : CVC3::SearchSat::LitPriorityPair
• getLiteral() : CVC3::Clause
• getLiterals() : CVC3::Clause
• getLitFlag() : CVC3::Theorem , CVC3::TheoremValue , CVC3::TheoremManager
• getLowerBound() : CVC3::TheoryArithNew
• getLowerBoundExplanation() : CVC3::TheoryArithNew
• getLowerBoundThm() : CVC3::TheoryArithNew
• GetMaxDLevel() : SatSolver , Xchaff
• getMaxSize() : CVC3::TheoryBitvector
• getMaxVar() : SAT::Clause
• getMemory() : CVC3::Context , CVC3::ContextMemoryManager , CVC3::ContextManager
• GetMemUsed() : SatSolver , Xchaff
• getMin() : MiniSat::Heap< C >
• getMM() : CVC3::RWTheoremValue , CVC3::ExprManager , CVC3::ExprValue , CVC3::TheoremManager , CVC3::TheoremValue , CVC3::RegTheoremValue
• getMMIndex() : CVC3::ExprRational , CVC3::ExprSymbol , CVC3::ExprVar , CVC3::ExprSkolem , CVC3::ExprTheorem , CVC3::ExprClosure , CVC3::BVConstExpr , CVC3::ExprApply , CVC3::ExprBoundVar , CVC3::ExprValue , CVC3::Expr , CVC3::ExprNode , CVC3::ExprNodeTmp , CVC3::ExprApplyTmp , CVC3::ExprString
• getModelTerm() : CVC3::Theory
• getModelValue() : CVC3::Theory , CVC3::TheoryCore
• getName() : CVC3::ExprBoundVar , CVC3::ExprVar , CVC3::ExprSymbol , CVC3::SearchEngine , CVC3::SearchEngineFast , CVC3::Expr , CVC3::ExprValue , CVC3::SearchSat , CVC3::SearchSimple , CVC3::Theory
• getNegExpr() : CVC3::Variable , CVC3::VariableValue
• getNewClauses() : SAT::DPLLT::TheoryAPI , CVC3::SearchSat , CVC3::SearchSatTheoryAPI
• GetNextClause() : Xchaff , SatSolver
• GetNextVar() : SatSolver , Xchaff
• getNotify() : CVC3::Expr
• getNullExpr() : CVC3::ExprManager
• GetNumConflicts() : SatSolver , Xchaff
• GetNumDecisions() : SatSolver , Xchaff
• GetNumDeletedClauses() : SatSolver , Xchaff
• GetNumDeletedLiterals() : SatSolver , Xchaff
• getNumerator() : CVC3::Rational
• GetNumExtConflicts() : SatSolver , Xchaff
• GetNumImplications() : SatSolver , Xchaff
• GetNumLiterals() : SatSolver , Xchaff
• getNumTheories() : CVC3::Theory
• getOp() : CVC3::Expr , CVC3::ExprApply , CVC3::ExprValue , CVC3::ExprApplyTmp
• getOpExpr() : CVC3::Expr
• getOpKind() : CVC3::Expr
• getOS() : CVC3::Debug
• getOSDumpTrace() : CVC3::Debug
• getOutputLang() : CVC3::ExprManager
• GetPhaseFromLit() : SatSolver , Xchaff
• getPredicates() : CVC3::TheoryCore
• getPrinter() : CVC3::ExprManager
• getPriority() : CVC3::SearchSat::LitPriorityPair
• getPrompt() : CVC3::ParserTemp
• getProof() : CVC3::Theorem , CVC3::TheoremValue , CVC3::VCL , CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::SearchSat , CVC3::SearchImplBase , CVC3::Theorem3
• getProofClosure() : CVC3::VCL , CVC3::ValidityChecker
• getProofTCC() : CVC3::VCL , CVC3::ValidityChecker
• getPushID() : MiniSat::Solver
• getQuantLevel() : CVC3::Theorem , CVC3::TheoremValue
• getQuantLevelForTerm() : CVC3::TheoryCore
• getRational() : CVC3::TheoryArithNew::EpsRational , CVC3::ExprRational , CVC3::TheoryArithNew::EpsRational , CVC3::Expr , CVC3::ExprValue
• getReachablePredicate() : CVC3::TheoryDatatype
• getReason() : MiniSat::Solver
• getRep() : CVC3::ExprNode , CVC3::ExprValue , CVC3::Expr
• getResource() : CVC3::TheoryCore
• getResourceLimit() : CVC3::TheoryCore
• getRestore() : CDList< Ineq > , iterator , CDList< dynTrig > , CDMap< Expr, CDList< dynTrig > , CDList< Expr > , CDO< T > , iterator , CDMap< Expr, Theorem > , CDMap< Expr, bool > , iterator , CDOmap< Expr, FreeConst > , CDMap< Key, Data, HashFcn > , iterator , CDOmap< Key, Data, HashFcn > new , CDOmapOrdered< Key, Data > , iterator , CDList< size_t > size_t , CDO< Theorem > , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > , iterator , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , iterator , CDList< T > , CDMapOrdered< Key, Data > , iterator , CDOmapOrdered< Key, Data > , CDList< size_t > , CDList< Theorem > , const_iterator , iterator , CVC3::ContextObj , iterator , vector< Expr >
• getRHS() : CVC3::TheoremValue , CVC3::Theorem3 , CVC3::RWTheoremValue , CVC3::Theorem
• getRules() : CVC3::TheoremManager , CVC3::VariableManager
• getRWMM() : CVC3::TheoremManager
• GetSATTime() : SatSolver , Xchaff
• getScope() : CVC3::Theorem3 , CVC3::TheoremValue , CVC3::Theorem , CVC3::Variable , CVC3::Literal , CVC3::VariableValue , CVC3::Clause
• getSelectorInfo() : CVC3::TheoryDatatype
• getSig() : CVC3::ExprNode , CVC3::ExprValue , CVC3::Expr
• getSimpCache() : CVC3::Expr
• getSimpCacheTag() : CVC3::ExprManager
• getSkolemAxioms() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• getStart() : MiniSat::Inference
• getStaticMemory() : CVC3::ContextMemoryManager
• getStatistics() : CVC3::TheoryCore , CVC3::VCL , CVC3::ValidityChecker
• getStats() : MiniSat::Solver
• getSteps() : MiniSat::Inference
• getString() : CVC3::ExprString , CVC3::ExprValue , CVC3::Expr , CVC3::CLFlag
• getStrVec() : CVC3::CLFlag
• getSubTerms() : CVC3::TheoryQuant
• getSXIndex() : CVC3::TheoryBitvector
• getTableauxEntry() : CVC3::TheoryArithNew
• getTCC() : CVC3::Theory , CVC3::ValidityChecker , CVC3::VCL
• getTerms() : CVC3::TheoryCore
• getTheorem() : CVC3::Clause , CVC3::ExprTheorem , CVC3::VariableValue , CVC3::Variable , CVC3::Literal , CVC3::Expr , CVC3::ExprValue
• getTheoremForTerm() : CVC3::TheoryCore
• getTheory() : CVC3::NotifyList
• getTM() : CVC3::ExprManager , CVC3::TheoryCore
• GetTotalTime() : SatSolver , Xchaff
• getTrail() : MiniSat::Solver
• getTranslator() : CVC3::TheoryCore
• getTrue() : SAT::Lit
• getTupleIndex() : CVC3::ExprValue
• getType() : CVC3::Expr , CVC3::ValidityChecker , CVC3::CLFlag , CVC3::VCL
• getTypePred() : CVC3::ValidityChecker , CVC3::Theory , CVC3::VCL
• getTypePredExpr() : CVC3::TheoryBitvector
• getTypePredType() : CVC3::TheoryBitvector
• getUid() : CVC3::ExprValue , CVC3::Expr , CVC3::ExprBoundVar
• getUnsigned() : CVC3::Rational
• getUpperBound() : CVC3::TheoryArithNew
• getUpperBoundExplanation() : CVC3::TheoryArithNew
• getUpperBoundThm() : CVC3::TheoryArithNew
• getUserAssumptions() : CVC3::SearchSat , CVC3::ValidityChecker , CVC3::SearchEngine , CVC3::VCL , CVC3::SearchImplBase
• getValue() : CVC3::BVConstExpr , MiniSat::Solver , SAT::DPLLTMiniSat , SAT::DPLLTBasic , CVC3::VariableValue , SAT::DPLLT , CVC3::SearchSat , CVC3::Variable , MiniSat::Solver , CVC3::Literal
• getVar() : CVC3::ExprValue , CVC3::Literal
• GetVar() : Xchaff , SatSolver
• getVar() : CVC3::Literal , SAT::Lit
• GetVarAssignment() : Xchaff , SatSolver
• GetVarFromLit() : SatSolver , Xchaff
• getVariableIntroThm() : CVC3::TheoryArithNew
• GetVarIndex() : SatSolver , Xchaff
• getVars() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprClosure
• getWatches() : MiniSat::Solver
• goalSatisfied() : CVC3::DecisionEngineDFS , CVC3::DecisionEngine , CVC3::DecisionEngineMBTF , CVC3::DecisionEngineCaching
• goodSynMatch() : CVC3::TheoryQuant
• goodSynMatchNewTrig() : CVC3::TheoryQuant
• grayShadow() : CVC3::TheoryArith , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• grayShadowConst() : CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules , CVC3::ArithTheoremProducer
• greaterthan() : CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer
• grow() : vec< T > , MiniSat::vec< T >
• growTo() : MiniSat::vec< T > , vec< T > , MiniSat::vec< T >
• gtExpr() : CVC3::VCL , CVC3::ValidityChecker

---