CVC3: Class Members

- 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() : CVC3::CDFlags , CVC3::CDOmap< Key, Data, HashFcn > , 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::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat , CVC3::ValidityChecker , CVC3::VCL
getAssumptionsAndCong() : CVC3::Theorem
getAssumptionsAndCongRec() : CVC3::Theorem
getAssumptionsRec() : CVC3::Theorem , CVC3::VCL
getAssumptionsRef() : CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue , CVC3::RegTheoremValue , CVC3::RWTheoremValue
getAssumptionsTCC() : CVC3::ValidityChecker , CVC3::VCL
getAssumptionsUsed() : CVC3::SearchImplBase , CVC3::ValidityChecker , CVC3::VCL
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::Context , CVC3::ExprManager , CVC3::TheoremManager , CVC3::TheoryCore , CVC3::VariableManager
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::TheoryArith3::FreeConst , CVC3::TheoryArith3::TheoryArith3::Ineq , CVC3::TheoryArithNew::TheoryArithNew::FreeConst , CVC3::TheoryArithNew::TheoryArithNew::Ineq , CVC3::TheoryArithOld::TheoryArithOld::FreeConst , CVC3::TheoryArithOld::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::TheoryArithOld::DifferenceLogicGraph
getEdgeTheorems() : CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph
getEdgeWeight() : CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph
getEM() : CVC3::Expr , CVC3::TheoremManager , CVC3::Theory , CVC3::ValidityChecker , CVC3::VCL
getEmptyVector() : CVC3::ExprManager
getEpsilon() : CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::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::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
GetFirstVar() : SatSolver
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::TheoryArithNew::EpsRational , CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::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::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
getLeaf() : SAT::SatProofNode
getLeafAssumptions() : CVC3::Theorem
getLeaves() : CVC3::ArithTheoremProducerOld
getLeftParent() : SAT::SatProofNode
getLemmas() : MiniSat::Solver
getLevel() : MiniSat::Solver
getLHS() : CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue , CVC3::RWTheoremValue
getLit() : CVC3::SearchSat::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::ExprManager , CVC3::ExprManagerNotifyObj , CVC3::ContextMemoryManager , CVC3::VCL
GetMemUsed() : SatSolver
getMin() : MiniSat::Heap< C >
getMM() : CVC3::TheoremValue , CVC3::ExprManager , CVC3::ExprValue , CVC3::TheoremManager , CVC3::RegTheoremValue , CVC3::RWTheoremValue
getMMIndex() : CVC3::Expr , CVC3::ExprNode , CVC3::ExprNodeTmp , CVC3::ExprApplyTmp , CVC3::ExprApply , CVC3::ExprString , CVC3::ExprSkolem , CVC3::ExprRational , CVC3::ExprSymbol , CVC3::ExprBoundVar , CVC3::ExprClosure , CVC3::ExprValue , CVC3::BVConstExpr , CVC3::ExprVar
getModelTerm() : CVC3::Theory
getModelValue() : CVC3::Theory , CVC3::TheoryCore
getName() : CVC3::ExprValue , CVC3::ExprVar , CVC3::ExprSymbol , CVC3::ExprBoundVar , CVC3::SearchEngine , CVC3::SearchEngineFast , CVC3::SearchSat , CVC3::Theory , CVC3::SearchSimple , CVC3::Expr
getNegExpr() : CVC3::Variable , CVC3::VariableValue
getNewClauses() : CVC3::SearchSat , CVC3::SearchSatTheoryAPI , SAT::DPLLT::DPLLT::TheoryAPI
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::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
getPlusTerms() : CVC3::BitvectorTheoremProducer
getPredicates() : CVC3::TheoryCore
getPrinter() : CVC3::ExprManager
getPriority() : CVC3::SearchSat::SearchSat::LitPriorityPair
getPrompt() : CVC3::ParserTemp
getProof() : CVC3::SearchSat , SAT::DPLLTMiniSat , CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::Theorem , CVC3::Theorem3 , CVC3::ValidityChecker , CVC3::VCL , MiniSat::Solver , CVC3::TheoremValue
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::TheoryArithNew::TheoryArithNew::EpsRational , CVC3::ExprRational , CVC3::ExprValue , CVC3::Expr , CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EpsRational
getReachablePredicate() : CVC3::TheoryDatatype
getReason() : MiniSat::Solver
getRep() : CVC3::ExprNode , CVC3::ExprValue , CVC3::Expr
getResource() : CVC3::TheoryCore
getResourceLimit() : CVC3::TheoryCore
getRestore() : CVC3::ContextObj
getRHS() : CVC3::Theorem , CVC3::Theorem3 , CVC3::RWTheoremValue , CVC3::TheoremValue
getRightParent() : SAT::SatProofNode
getRoot() : SAT::SatProof
getRules() : CVC3::VariableManager , CVC3::TheoremManager
getRWMM() : CVC3::TheoremManager
GetSatAssumptions() : CVC3::Theorem
GetSatAssumptionsRec() : CVC3::Theorem
getSatProof() : SAT::DPLLTMiniSat , SAT::DPLLTBasic , SAT::DPLLT
GetSATTime() : SatSolver
getScope() : CVC3::Variable , CVC3::TheoremValue , CVC3::VariableValue , CVC3::Theorem3 , CVC3::Clause , CVC3::Theorem , CVC3::Literal
getSelectorInfo() : CVC3::TheoryDatatype
getSig() : CVC3::ExprValue , CVC3::Expr , CVC3::ExprNode
getSimpCache() : CVC3::Expr
getSimpCacheTag() : CVC3::ExprManager
getSize() : CVC3::Expr , CVC3::ExprValue
getSkolemAxioms() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
getSmartClauses() : CVC3::CNF_TheoremProducer
GetSortedOpVec() : CVC3::ExprTransform
getStart() : MiniSat::Inference
getStaticMemory() : CVC3::ContextMemoryManager
getStatistics() : CVC3::ValidityChecker , CVC3::TheoryCore , CVC3::VCL
getStats() : MiniSat::Solver
getSteps() : MiniSat::Inference
getString() : CVC3::CLFlag , CVC3::Expr , CVC3::ExprValue , CVC3::ExprString , CVC3::MemoryTracker
getStrVec() : CVC3::CLFlag
GetSub_vec() : CVC3::ExprTransform
getSubTerms() : CVC3::TheoryQuant
getSXIndex() : CVC3::TheoryBitvector
getTableauxEntry() : CVC3::TheoryArithNew
getTCC() : CVC3::Theory , CVC3::VCL , CVC3::ValidityChecker
getTerminalsConstFlag() : CVC3::Expr
getTerms() : CVC3::TheoryCore
getTheorem() : CVC3::VariableValue , CVC3::Expr , CVC3::Variable , CVC3::Clause , CVC3::ExprValue , MiniSat::Clause , CVC3::Literal
getTheoremForTerm() : CVC3::TheoryCore
getTheory() : CVC3::NotifyList
getTM() : CVC3::TheoryCore , CVC3::ExprManager
GetTotalTime() : SatSolver
getTrail() : MiniSat::Solver
getTranslator() : CVC3::TheoryCore
getTrigs() : CVC3::ExprClosure , CVC3::Expr , CVC3::ExprValue
getTrue() : SAT::Lit
getTupleIndex() : CVC3::ExprValue
getType() : CVC3::VCL , CVC3::Expr , CVC3::ValidityChecker , CVC3::CLFlag
getTypePred() : CVC3::ValidityChecker , CVC3::Theory , CVC3::VCL
getTypePredExpr() : CVC3::TheoryBitvector
getTypePredType() : CVC3::TheoryBitvector
getUid() : CVC3::ExprValue , CVC3::ExprBoundVar , CVC3::Expr
getUnsatTheorem() : CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph
getUnsigned() : CVC3::Rational
getUpperBound() : CVC3::TheoryArithOld , CVC3::TheoryArithNew
getUpperBoundExplanation() : CVC3::TheoryArithNew
getUpperBoundThm() : CVC3::TheoryArithNew
getUserAssumptions() : CVC3::SearchImplBase , CVC3::ValidityChecker , CVC3::SearchSat , CVC3::SearchEngine , CVC3::VCL
getValuation() : CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph
getValue() : CVC3::SearchEngine , SAT::DPLLTMiniSat , CVC3::VariableValue , MiniSat::Solver , SAT::DPLLTBasic , CVC3::BVConstExpr , CVC3::SearchSat , SAT::DPLLT , CVC3::SearchSat , CVC3::Literal , MiniSat::Solver , CVC3::SearchSat , CVC3::Variable , CVC3::SearchImplBase
getVar() : CVC3::Literal , CVC3::ExprValue
GetVar() : SatSolver
getVar() : CVC3::Literal , SAT::Lit
GetVarAssignment() : SatSolver
GetVarFromLit() : SatSolver
getVariableIntroThm() : CVC3::TheoryArithNew
getVariables() : CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph
GetVarIndex() : SatSolver
getVars() : CVC3::ExprValue , CVC3::Expr , CVC3::ExprClosure
getVec() : CVC3::MemoryTracker
getVecAndData() : CVC3::MemoryTracker
getVecAndDataP() : CVC3::MemoryTracker
getVerticesTopological() : CVC3::TheoryArithOld::TheoryArithOld::VarOrderGraph
getWatches() : MiniSat::Solver
goalSatisfied() : CVC3::DecisionEngineCaching , CVC3::DecisionEngine , CVC3::DecisionEngineMBTF , CVC3::DecisionEngineDFS
goodSynMatch() : CVC3::TheoryQuant
goodSynMatchNewTrig() : CVC3::TheoryQuant
grayShadow() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::TheoryArith , CVC3::ArithTheoremProducer3
grayShadowConst() : CVC3::ArithTheoremProducer3 , CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
greaterthan() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer
grow() : MiniSat::vec< T >
growTo() : MiniSat::vec< T >
gtExpr() : CVC3::ValidityChecker , CVC3::VCL