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

- n -

• naiveCheckSat() : CVC3::TheoryQuant
• name : LFSCPfVar , CVC3::Context
• nAssigns() : MiniSat::Solver
• nClauses() : MiniSat::Solver
• negate() : CVC3::Expr
• negatedInequality() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• negBVand() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• negBVor() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• negBVxnor() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• negBVxor() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• negConcat() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• negConst() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• negElim() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• negIntro() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• negNeg() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• NEW_formula_map : CVC3::ExprTransform
• newAssumption() : CVC3::TheoremProducer
• newBitvectorType() : CVC3::TheoryBitvector
• newBitvectorTypeExpr() : CVC3::TheoryBitvector
• newBitvectorTypePred() : CVC3::TheoryBitvector
• newBoolExtractExpr() : CVC3::TheoryBitvector
• newBoundVarExpr() : CVC3::ExprManager
• NewBryantVar() : CVC3::ExprTransform
• newBVAndExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVASHR() : CVC3::ValidityChecker , CVC3::VCL
• newBVCompExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVConstExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVExtractExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVIndexExpr() : CVC3::TheoryBitvector
• newBVLEExpr() : CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoryBitvector
• newBVLSHR() : CVC3::ValidityChecker , CVC3::VCL
• newBVLTExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVMultExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVMultPadExpr() : CVC3::TheoryBitvector
• newBVNandExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVNegExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVNorExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVOneString() : CVC3::TheoryBitvector
• newBVOrExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVPlusExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVPlusPadExpr() : CVC3::TheoryBitvector
• newBVSDivExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVSHL() : CVC3::ValidityChecker , CVC3::VCL
• newBVSLEExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVSLTExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVSModExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVSRemExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVSubExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVUDivExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVUminusExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVURemExpr() : CVC3::VCL , CVC3::TheoryBitvector , CVC3::ValidityChecker
• newBVXnorExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVXorExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newBVZeroString() : CVC3::TheoryBitvector
• newChunk() : CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager
• newClause() : SAT::CNF_Formula , SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
• newClosureExpr() : CVC3::ExprManager
• newConcatExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newData() : CVC3::MemoryManager , CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager , CVC3::MemoryManagerMalloc
• newExpr() : CVC3::ExprManager
• newExprValue() : CVC3::ExprManager
• newFixedConstWidthLeftShiftExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newFixedLeftShiftExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newFixedRightShiftExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newFunction() : CVC3::Theory
• newIntAssumption() : CVC3::SearchEngineFast , CVC3::SearchImplBase
• newKind() : CVC3::ExprManager
• newLabel() : CVC3::TheoremProducer
• newLeafExpr() : CVC3::ExprManager
• newLiteral() : CVC3::SearchImplBase
• newName() : CVC3::ExprStream
• newPf() : CVC3::TheoremProducer
• newPP() : CVC3::ExprTransform
• newPPrec() : CVC3::ExprTransform
• newRatExpr() : CVC3::ExprManager
• newReflTheorem() : CVC3::TheoremProducer
• newRWTheorem() : CVC3::TheoremProducer
• newRWTheorem3() : CVC3::TheoremProducer
• newRWThm() : CVC3::QuantProofRules , CVC3::QuantTheoremProducer
• newSkolemExpr() : CVC3::ExprManager
• newStringExpr() : CVC3::ExprManager
• newSubtypeExpr() : CVC3::Theory
• newSXExpr() : CVC3::TheoryBitvector , CVC3::ValidityChecker , CVC3::VCL
• newSymbolExpr() : CVC3::ExprManager
• newTheorem() : CVC3::TheoremProducer
• newTheorem3() : CVC3::TheoremProducer
• newTopMatch() : CVC3::TheoryQuant
• newTopMatchBackupOnly() : CVC3::TheoryQuant
• newTopMatchNoSig() : CVC3::TheoryQuant
• newTopMatchSig() : CVC3::TheoryQuant
• newTypeExpr() : CVC3::Theory
• newUserAssumption() : CVC3::SearchEngine , CVC3::SearchImplBase , CVC3::SearchSat
• newUserAssumptionInt() : CVC3::SearchSat
• newUserAssumptionIntHelper() : CVC3::SearchSat
• newVar() : MiniSat::VarOrder
• NewVar() : CVC3::ExprTransform
• newVar() : CVC3::Theory , MiniSat::VarOrder
• newVarExpr() : CVC3::ExprManager
• newVariableValue() : CVC3::VariableManager
• next() : CVC3::Parser , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data >
• next_restart_backtrack : CSolverParameters
• next_restart_time : CSolverParameters
• nextClauseID() : MiniSat::Solver
• nextFlag() : CVC3::ExprManager
• nextIndex() : CVC3::ExprManager
• nLearnts() : MiniSat::Solver
• nnode_map : LFSCObj
• noCycle() : CVC3::DatatypeTheoremProducer , CVC3::DatatypeProofRules
• nodag : CVC3::ExprStream
• nodeCount : LFSCConvert
• nodeCountTh : LFSCConvert
• nonLinearIneqSignSplit() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• nonlinearSignSplit() : CVC3::TheoryArithOld
• NORMAL : CVC3::TheoryCore
• NormalizationType : CVC3::TheoryArithNew
• normalize() : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArith3
• NORMALIZE_GCD : CVC3::TheoryArithNew
• normalize_to_tf() : TReturn
• normalize_tr() : TReturn
• normalize_tret() : TReturn
• NORMALIZE_UNIT : CVC3::TheoryArithNew
• normalizeProjectIneqs() : CVC3::TheoryArith3 , CVC3::TheoryArithOld , CVC3::TheoryArithNew
• normalizeQuant() : CVC3::QuantProofRules , CVC3::QuantTheoremProducer
• NOT_ARRAY_NORMALIZED : CVC3::Expr
• notArrayNormalized() : CVC3::Expr
• notBVEQ1Rule() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• notBVLTRule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• notExpr() : CVC3::VCL , CVC3::ValidityChecker , CVC3::Expr
• notify() : CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj , CVC3::VariableManagerNotifyObj , CVC3::ExprManagerNotifyObj , CVC3::TheoryCore::CoreNotifyObj , CVC3::SearchSat::Restorer , CVC3::ContextNotifyObj , CVC3::SearchEngineFast::ConflictClauseManager
• notifyInconsistent() : CVC3::TheoryQuant , CVC3::Theory
• NotifyList() : CVC3::NotifyList
• notifyPre() : CVC3::SearchSat::Restorer , CVC3::VariableManagerNotifyObj , CVC3::ExprManagerNotifyObj , CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj , CVC3::ContextNotifyObj
• notNotElim() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• notToIff() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• NotToIte() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• null_cdlist : CVC3::TheoryQuant
• nullRat : LFSCObj
• num_added_clauses : CDatabaseStats , CDatabase
• num_added_literals : CDatabaseStats , CDatabase
• num_backtracks : CSolverStats
• num_clauses() : CDatabase
• num_decisions : CSolverStats , CSolver
• num_deleted_clauses() : CDatabase , CDatabaseStats
• num_deleted_literals : CDatabaseStats , CDatabase
• num_free_variables() : CSolver , CSolverStats
• num_implications() : CSolver , CSolverStats
• num_literals() : CDatabase
• num_lits() : CClause
• num_variables() : CDatabase
• numClauses() : SAT::CNF_Formula
• NumClauses() : Xchaff
• numClauses() : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
• NumClauses() : SatSolver
• numFanins() : SAT::CNF_Manager
• numFanouts() : SAT::CNF_Manager
• numImpliedLiterals() : CVC3::TheoryCore
• NumVariables() : SatSolver , Xchaff
• numVars() : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula , SAT::CNF_Manager , SAT::CNF_Formula
• nVars() : MiniSat::Solver