- g -

• garbageCollect() : CVC3::ContextMemoryManager
• gc() : CVC3::ExprManager , CVC3::VariableManager
• geExpr() : CVC3::ValidityChecker , CVC3::VCL
• generalBitBlast() : CVC3::TheoryBitvector
• generalIneqn() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• generalTrig() : CVC3::TheoryQuant
• generate_CDB() : SAT::DPLLTBasic
• get() : RefPtr< T > , CVC3::CDFlags , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDO< T > , CVC3::SmartCDO< T >
• get_antecedence() : CVariable
• get_clause_index() : CLitPoolElement
• Get_ITEs() : CVC3::ExprTransform
• get_length() : LFSCProofExpr , LFSCPfVar , LFSCPfLambda , LFSCProofGeneric , LFSCPfLet , LFSCBoolRes , LFSCLem , LFSCClausify , LFSCAssume , LFSCLraAdd , LFSCLraAxiom , LFSCLraMulC , LFSCLraSub , LFSCLraPoly , LFSCLraContra , LFSCProof
• get_proof_counter() : LFSCProof
• get_proof_pattern() : LFSCConvert
• get_string_length() : LFSCProof
• GetAckSwap() : CVC3::ExprTransform
• getActiveSolver() : SAT::DPLLTMiniSat
• getAntecedent() : CVC3::Variable , CVC3::VariableValue
• getAntecedentIdx() : CVC3::Variable , CVC3::VariableValue
• getAssignment() : CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::VCL
• getAssumpThm() : CVC3::Variable , CVC3::VariableValue
• getAssumptions() : CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker , CVC3::VCL
• getAssumptionsAndCong() : CVC3::Theorem
• getAssumptionsAndCongRec() : CVC3::Theorem
• getAssumptionsRec() : CVC3::Theorem , CVC3::VCL
• getAssumptionsRef() : CVC3::RegTheoremValue , CVC3::RWTheoremValue , CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue
• getAssumptionsTCC() : CVC3::ValidityChecker , CVC3::VCL
• getAssumptionsUsed() : CVC3::SearchImplBase , CVC3::ValidityChecker , CVC3::VCL
• getBaseArray() : CVC3::TheoryArray
• 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 , Xchaff
• 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
• getChild() : LFSCBoolRes , LFSCClausify , LFSCAssume , LFSCLraAdd , LFSCLraMulC , LFSCLraSub , LFSCLraPoly , LFSCLraContra , LFSCProof , LFSCPfLambda , LFSCProofGeneric
• getChOp() : LFSCProof
• GetClause() : SatSolver , Xchaff
• GetClauseLits() : SatSolver , Xchaff
• getClauses() : MiniSat::Solver
• getClauseTheorem() : SAT::Clause
• getClosure() : CVC3::ValidityChecker , CVC3::VCL
• getCM() : CVC3::ExprManager , CVC3::TheoremManager , CVC3::TheoryCore , CVC3::VariableManager , CVC3::Context
• getCMM() : CVC3::Scope , CVC3::ContextObj
• getCNFLit() : SAT::CNF_Manager
• getCommonRules() : CVC3::SearchEngine , CVC3::Theory
• getConcreteModel() : CVC3::SearchEngine , CVC3::ValidityChecker , CVC3::VCL
• getConflictLevel() : MiniSat::Solver
• getConsForTester() : CVC3::TheoryDatatype
• getConsPos() : CVC3::TheoryDatatype
• getConst() : CVC3::TheoryArith3::FreeConst , CVC3::TheoryArith3::Ineq , CVC3::TheoryArithNew::FreeConst , CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::FreeConst , CVC3::TheoryArithOld::Ineq
• getConstant() : CVC3::TheoryDatatype
• getContext() : CVC3::Scope
• getCoreRules() : CVC3::TheoryCore
• getCounterExample() : CVC3::SearchEngine , CVC3::SearchEngineFast , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker , CVC3::VCL
• 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::TheoremManager , CVC3::Theory , 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::Op , CVC3::NotifyList , CVC3::Proof , CVC3::Theorem , CVC3::Theorem3 , CVC3::Type , CVC3::Variable , CVC3::Literal , CVC3::VariableValue , CVC3::TheoremValue , CVC3::RWTheoremValue
• getExprScore() : CVC3::TheoryQuant
• getExprTrans() : CVC3::TheoryCore
• getExprValue() : CVC3::Expr , CVC3::ExprValue , CVC3::BVConstExpr
• getExtractHi() : CVC3::TheoryBitvector
• getExtractLow() : CVC3::TheoryBitvector
• getFactors() : CVC3::TheoryArith3 , CVC3::TheoryArithOld
• getFalse() : SAT::Lit
• getFanin() : SAT::CNF_Manager
• getFanout() : SAT::CNF_Manager
• getField() : CVC3::ExprValue , CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
• getFieldIndex() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
• getFields() : CVC3::ExprValue , CVC3::TheoryRecords , 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::CLFlags , CVC3::Expr , CVC3::ExprManager , CVC3::TheoremManager
• 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::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::VCL
• getImpliedLiteralByIndex() : CVC3::TheoryCore
• getIndex() : SAT::Var , CVC3::Expr , CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
• getInputLang() : CVC3::ExprManager
• getInt() : CVC3::CLFlag , CVC3::Rational
• getInternalAssumptions() : CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker , CVC3::VCL
• getIsAtomicFlag() : CVC3::Expr
• getKey() : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data >
• getKids() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprNode , CVC3::ExprNodeTmp
• getKids1() : CVC3::ExprNode
• getKind() : CVC3::Expr , CVC3::ExprManager , CVC3::Op , CVC3::ExprValue
• getKindName() : CVC3::ExprManager
• getL() : TReturn
• getLeaf() : SAT::SatProofNode
• getLeafAssumptions() : CVC3::Theorem
• getLeaves() : CVC3::ArithTheoremProducerOld
• getLeftParent() : SAT::SatProofNode
• getLemmas() : MiniSat::Solver
• getLevel() : MiniSat::Solver
• getLFSCProof() : LFSCConvert , TReturn
• getLHS() : CVC3::Theorem , CVC3::Theorem3 , 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 , Xchaff
• getMaxSize() : CVC3::TheoryBitvector
• getMaxVar() : SAT::Clause
• getMemory() : CVC3::Context , CVC3::Scope , CVC3::ContextManager , CVC3::ContextNotifyObj , CVC3::ExprManager , CVC3::ExprManagerNotifyObj , CVC3::ContextMemoryManager , CVC3::VCL
• GetMemUsed() : Xchaff , SatSolver
• getMin() : MiniSat::Heap< C >
• getMM() : CVC3::TheoremManager , CVC3::ExprManager , CVC3::ExprValue , CVC3::TheoremValue , CVC3::RegTheoremValue , CVC3::RWTheoremValue
• getMMIndex() : CVC3::ExprRational , CVC3::ExprClosure , CVC3::Expr , CVC3::ExprValue , CVC3::ExprNode , CVC3::ExprNodeTmp , CVC3::ExprApplyTmp , CVC3::ExprApply , CVC3::ExprString , CVC3::ExprSkolem , CVC3::ExprVar , CVC3::ExprSymbol , CVC3::ExprBoundVar , CVC3::BVConstExpr
• getModelTerm() : CVC3::Theory
• getModelValue() : CVC3::TheoryCore , CVC3::Theory
• getName() : CVC3::SearchSat , CVC3::Expr , CVC3::ExprValue , CVC3::ExprVar , CVC3::ExprSymbol , CVC3::ExprBoundVar , CVC3::SearchEngine , CVC3::SearchEngineFast , CVC3::SearchSimple , CVC3::Theory
• getNegExpr() : CVC3::VariableValue , CVC3::Variable
• getNewClauses() : SAT::DPLLT::TheoryAPI , CVC3::SearchSat , CVC3::SearchSatTheoryAPI
• GetNextClause() : SatSolver , Xchaff
• GetNextVar() : SatSolver , Xchaff
• getNodeProof() : SAT::SatProofNode
• getNotify() : CVC3::Expr
• getNullExpr() : CVC3::ExprManager
• getNumChildren() : LFSCBoolRes , LFSCAssume , LFSCLraAdd , LFSCLraMulC , LFSCLraPoly , LFSCLraContra , LFSCProof , LFSCProofGeneric , LFSCPfLambda , LFSCClausify , LFSCLraSub
• GetNumConflicts() : SatSolver , Xchaff
• GetNumDecisions() : SatSolver , Xchaff
• GetNumDeletedClauses() : SatSolver , Xchaff
• GetNumDeletedLiterals() : Xchaff , SatSolver
• getNumerator() : CVC3::Rational
• GetNumExtConflicts() : SatSolver , Xchaff
• GetNumImplications() : SatSolver , Xchaff
• GetNumLiterals() : SatSolver , Xchaff
• getNumNodes() : LFSCObj
• getNumTheories() : CVC3::Theory
• getOp() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprApplyTmp , CVC3::ExprApply
• getOpExpr() : CVC3::Expr
• getOpKind() : CVC3::Expr
• GetOrderedTerms() : CVC3::ExprTransform
• GetOrdering() : CVC3::ExprTransform
• getOutputLang() : CVC3::ExprManager
• GetPEqs() : CVC3::ExprTransform
• GetPhaseFromLit() : SatSolver , Xchaff
• getPlusTerms() : CVC3::BitvectorTheoremProducer
• getPredicates() : CVC3::TheoryCore
• getPrinter() : CVC3::ExprManager
• getPriority() : CVC3::SearchSat::LitPriorityPair
• getPrompt() : CVC3::ParserTemp
• getProof() : MiniSat::Solver , CVC3::SearchSat , CVC3::VCL , CVC3::SearchImplBase , CVC3::SearchEngine , SAT::DPLLTMiniSat , CVC3::Theorem3 , CVC3::TheoremValue , CVC3::ValidityChecker , CVC3::Theorem
• getProofClosure() : CVC3::ValidityChecker , CVC3::VCL
• getProofQuery() : CVC3::ValidityChecker , CVC3::VCL
• getProofTCC() : CVC3::VCL , CVC3::ValidityChecker
• getProvesY() : TReturn
• getPushID() : MiniSat::Solver
• getQuantLevel() : CVC3::TheoremValue , CVC3::Theorem
• getQuantLevelDebug() : CVC3::Theorem , CVC3::TheoremValue
• getQuantLevelForTerm() : CVC3::TheoryCore
• getRational() : CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational , CVC3::Expr , CVC3::ExprValue , TReturn , CVC3::TheoryArithNew::EpsRational , CVC3::ExprRational
• getReachablePredicate() : CVC3::TheoryDatatype
• getReason() : MiniSat::Solver
• GetRefCount() : Obj
• getRep() : CVC3::ExprNode , CVC3::Expr , CVC3::ExprValue
• getResource() : CVC3::TheoryCore
• getResourceLimit() : CVC3::TheoryCore
• getRestore() : CVC3::ContextObj
• getRHS() : CVC3::RWTheoremValue , CVC3::TheoremValue , CVC3::Theorem , CVC3::Theorem3
• getRightParent() : SAT::SatProofNode
• getRoot() : SAT::SatProof
• getRules() : CVC3::TheoremManager , CVC3::VariableManager
• getRWMM() : CVC3::TheoremManager
• GetSatAssumptions() : CVC3::Theorem
• GetSatAssumptionsRec() : CVC3::Theorem
• getSatProof() : SAT::DPLLT , SAT::DPLLTBasic , SAT::DPLLTMiniSat
• GetSATTime() : SatSolver , Xchaff
• getScope() : CVC3::Literal , CVC3::Theorem3 , CVC3::Variable , CVC3::Clause , CVC3::Theorem , CVC3::VariableValue , CVC3::TheoremValue
• getSelectorInfo() : CVC3::TheoryDatatype
• getSig() : CVC3::ExprNode , CVC3::Expr , CVC3::ExprValue
• getSimpCache() : CVC3::Expr
• getSimpCacheTag() : CVC3::ExprManager
• getSize() : CVC3::ExprValue , CVC3::Expr
• getSkolemAxioms() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• getSmartClauses() : CVC3::CNF_TheoremProducer
• GetSortedOpVec() : CVC3::ExprTransform
• getStart() : MiniSat::Inference
• getStaticMemory() : CVC3::ContextMemoryManager
• getStatistics() : CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoryCore
• getStats() : MiniSat::Solver
• getSteps() : MiniSat::Inference
• getString() : CVC3::MemoryTracker , CVC3::Expr , CVC3::CLFlag , CVC3::ExprValue , CVC3::ExprString
• getStrVec() : CVC3::CLFlag
• GetSub_vec() : CVC3::ExprTransform
• getSubTerms() : CVC3::TheoryQuant
• getSXIndex() : CVC3::TheoryBitvector
• getTableauxEntry() : CVC3::TheoryArithNew
• getTCC() : CVC3::ValidityChecker , CVC3::Theory , CVC3::VCL
• getTerminalsConstFlag() : CVC3::Expr
• getTerms() : CVC3::TheoryCore
• getTheorem() : CVC3::Clause , CVC3::Literal , MiniSat::Clause , CVC3::VariableValue , CVC3::Expr , CVC3::Variable , CVC3::ExprValue
• getTheoremForTerm() : CVC3::TheoryCore
• getTheory() : CVC3::NotifyList
• getTM() : CVC3::TheoryCore , CVC3::ExprManager
• GetTotalTime() : Xchaff , SatSolver
• getTrail() : MiniSat::Solver
• getTranslator() : CVC3::TheoryCore
• getTriggers() : CVC3::ExprClosure , CVC3::ExprValue , CVC3::Expr
• getTrue() : SAT::Lit
• getTupleIndex() : CVC3::ExprValue
• getType() : CVC3::VCL , CVC3::Expr , CVC3::ValidityChecker , CVC3::CLFlag
• getTypePred() : CVC3::ValidityChecker , CVC3::VCL , CVC3::Theory
• getTypePredExpr() : CVC3::TheoryBitvector
• getTypePredType() : CVC3::TheoryBitvector
• getUid() : CVC3::Expr , CVC3::ExprBoundVar , CVC3::ExprValue
• getUnsatTheorem() : CVC3::TheoryArithOld::DifferenceLogicGraph
• getUnsigned() : CVC3::Unsigned , CVC3::Rational
• getUnsignedMP() : CVC3::Rational
• getUpperBound() : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• getUpperBoundExplanation() : CVC3::TheoryArithNew
• getUpperBoundThm() : CVC3::TheoryArithNew
• getUserAssumptions() : CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::ValidityChecker , CVC3::VCL , CVC3::SearchSat
• getValuation() : CVC3::TheoryArithOld::DifferenceLogicGraph
• getValue() : CVC3::SearchSat , SAT::DPLLT , SAT::DPLLTBasic , SAT::DPLLTMiniSat , CVC3::Variable , CVC3::SearchEngine , MiniSat::Solver , CVC3::TheoryCore , CVC3::SearchSat , CVC3::BVConstExpr , CVC3::VCL , MiniSat::Solver , CVC3::ValidityChecker , CVC3::VariableValue , CVC3::Literal , CVC3::SearchSat , CVC3::SearchImplBase
• GetVar() : Xchaff
• getVar() : CVC3::Literal
• GetVar() : SatSolver
• getVar() : SAT::Lit , CVC3::ExprValue
• GetVarAssignment() : SatSolver , Xchaff
• GetVarFromLit() : SatSolver , Xchaff
• getVariableIntroThm() : CVC3::TheoryArithNew
• getVariables() : CVC3::TheoryArithOld::DifferenceLogicGraph
• GetVarIndex() : Xchaff , SatSolver
• getVars() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprClosure
• getVec() : CVC3::MemoryTracker
• getVecAndData() : CVC3::MemoryTracker
• getVecAndDataP() : CVC3::MemoryTracker
• getVerticesTopological() : CVC3::TheoryArithOld::VarOrderGraph
• getWatches() : MiniSat::Solver
• getY() : LFSCObj
• goalSatisfied() : CVC3::DecisionEngineCaching , CVC3::DecisionEngine , CVC3::DecisionEngineMBTF , CVC3::DecisionEngineDFS
• goodSynMatch() : CVC3::TheoryQuant
• goodSynMatchNewTrig() : CVC3::TheoryQuant
• grayShadow() : CVC3::TheoryArith , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• grayShadowConst() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• greaterthan() : CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3
• grow() : MiniSat::vec< T >
• growTo() : MiniSat::vec< T >
• gtExpr() : CVC3::ValidityChecker , CVC3::VCL