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

- n -

• naiveCheckSat() : CVCL::TheoryQuant
• name() : CVCL::Context
• neg() : CVCL::RefinedArithTheoremProducer
• negate() : CVCL::Expr
• negatedInequality() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• negBVand() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• negBVor() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• negConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• negConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• negIntro() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• negNeg() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• newAssumption() : CVCL::TheoremProducer
• newBitvectorType() : CVCL::TheoryBitvector
• newBitvectorTypeExpr() : CVCL::TheoryBitvector
• newBitvectorTypePred() : CVCL::TheoryBitvector
• newBoolExtractExpr() : CVCL::TheoryBitvector
• newBoundVarExpr() : CVCL::ExprManager
• newBVAndExpr() : CVCL::TheoryBitvector
• newBVConstExpr() : CVCL::TheoryBitvector
• newBVExtractExpr() : CVCL::TheoryBitvector
• newBVLEExpr() : CVCL::TheoryBitvector
• newBVLTExpr() : CVCL::TheoryBitvector
• newBVMultExpr() : CVCL::TheoryBitvector
• newBVNandExpr() : CVCL::TheoryBitvector
• newBVNegExpr() : CVCL::TheoryBitvector
• newBVNorExpr() : CVCL::TheoryBitvector
• newBVOneString() : CVCL::TheoryBitvector
• newBVOrExpr() : CVCL::TheoryBitvector
• newBVPlusExpr() : CVCL::TheoryBitvector
• newBVUminusExpr() : CVCL::TheoryBitvector
• newBVXnorExpr() : CVCL::TheoryBitvector
• newBVXorExpr() : CVCL::TheoryBitvector
• newBVZeroString() : CVCL::TheoryBitvector
• newChunk() : CVCL::MemoryManagerChunks
• newClause() : SAT::CD_CNF_Formula, SAT::CNF_Formula_Impl, SAT::CNF_Formula
• newClosureExpr() : CVCL::ExprManager
• newConcatExpr() : CVCL::TheoryBitvector
• newData() : CVCL::MemoryManagerMalloc, CVCL::MemoryManagerChunks, CVCL::MemoryManager
• newEquivCkExpr() : CVCL::TheoryCore
• newExpr() : CVCL::ExprManager
• newExprValue() : CVCL::ExprManager
• newFixedLeftShiftExpr() : CVCL::TheoryBitvector
• newFixedRightShiftExpr() : CVCL::TheoryBitvector
• newFunction() : CVCL::Theory
• newIntAssumption() : CVCL::SearchImplBase, CVCL::SearchEngineFast
• newKind() : CVCL::ExprManager
• newLabel() : CVCL::TheoremProducer
• newLeafExpr() : CVCL::ExprManager
• newLiteral() : CVCL::SearchImplBase
• newName() : CVCL::ExprStream
• newPf() : CVCL::TheoremProducer
• newRatExpr() : CVCL::ExprManager
• newReflTheorem() : CVCL::TheoremProducer
• newRWTheorem() : CVCL::TheoremProducer
• newRWTheorem3() : CVCL::TheoremProducer
• newSBVLEExpr() : CVCL::TheoryBitvector
• newSBVLTExpr() : CVCL::TheoryBitvector
• newSkolemExpr() : CVCL::ExprManager
• newStringExpr() : CVCL::ExprManager
• newSXExpr() : CVCL::TheoryBitvector
• newSymbolExpr() : CVCL::ExprManager
• newTheorem() : CVCL::TheoremProducer
• newTheorem3() : CVCL::TheoremProducer
• newTimer() : CVCL::Debug
• newTypeExpr() : CVCL::Theory
• newUserAssumption() : CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngine
• newVar() : CVCL::Theory
• newVarExpr() : CVCL::ExprManager
• newVariableValue() : CVCL::VariableManager
• Next() : CVCL::Hash_Entry< _Key, _Data >
• next : CVCL::Parser, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::SVC_API_impl::varinfo
• next_restart_backtrack : CSolverParameters
• next_restart_time : CSolverParameters
• nextFlag() : CVCL::ExprManager
• nextIndex() : CVCL::ExprManager
• noCycle() : CVCL::DatatypeTheoremProducer, CVCL::DatatypeProofRules
• nodag : CVCL::ExprStream
• normalize() : CVCL::TheoryArith
• normalizeBVArith() : CVCL::TheoryBitvector
• normalizeConcat() : CVCL::TheoryBitvector
• normalizeProjectIneqs() : CVCL::TheoryArith
• notBVLTRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• notExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• notify() : CVCL::VariableManagerNotifyObj, CVCL::TheoryCore::CoreNotifyObj, CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj, CVCL::SearchEngineFast::ConflictClauseManager, CVCL::ExprManagerNotifyObj, CVCL::ContextNotifyObj
• notifyInconsistent() : CVCL::TheoryQuant, CVCL::Theory
• NotifyList() : CVCL::NotifyList
• notifyPre() : CVCL::VariableManagerNotifyObj, CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj, CVCL::SearchSat::Restorer, CVCL::ExprManagerNotifyObj, CVCL::ContextNotifyObj
• notifySAT : CVCL::TheoryCore
• notNotElim() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• notToIff() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• NotToIte() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• Null() : CVCL::Hash_Ptr< _Key, _Data >
• num_added_clauses : CDatabase, CDatabaseStats
• num_added_literals : CDatabase, CDatabaseStats
• num_backtracks : CSolverStats
• num_clauses() : CDatabase
• num_decisions : CSolver, CSolverStats
• num_deleted_clauses : CDatabase, CDatabaseStats
• num_deleted_literals : CDatabase, CDatabaseStats
• num_free_variables : CSolver, CSolverStats
• num_implications : CSolver, CSolverStats
• num_literals() : CDatabase
• num_lits() : CClause
• num_variables() : CDatabase
• NumClauses() : Xchaff, SatSolver
• numClauses() : SAT::CD_CNF_Formula, SAT::CNF_Formula_Impl, SAT::CNF_Formula
• NumEntries() : CVCL::Dict< _Key, _Data >
• numFanins() : SAT::CNF_Manager
• numFanouts() : SAT::CNF_Manager
• numImpliedLiterals() : CVCL::TheoryCore
• NumVariables() : Xchaff, SatSolver
• numVars() : SAT::CNF_Manager, SAT::CD_CNF_Formula, SAT::CNF_Formula_Impl, SAT::CNF_Formula

---