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

- s -

• s : CVCL::CLFlag
• s_charHash : CVCL::ExprValue
• s_intHash : CVCL::ExprValue
• s_null : CVCL::Expr
• s_var() : CLitPoolElement
• sameKidCheck() : CVCL::BitvectorTheoremProducer
• sat() : CVCL::Clause
• SAT2cvcl() : SAT::DPLLTBasic
• SatAPI() : CVCL::SVC_API_impl
• Satisfiable() : Xchaff, SatSolver
• SATISFIABLE : SatSolver, SAT::DPLLT
• satSolver() : SAT::DPLLTBasic
• SatSolver() : SatSolver
• SATStatus : SatSolver
• Scope : CVCL::Scope, CVCL::ContextObj, CVCL::ContextObjChain
• scopeLevel() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchImplBase, CVCL::Debug, CVCL::ContextManager
• scopelevel() : CVCL::ExprManager
• ScopeWatcher() : CVCL::ScopeWatcher
• score() : CVariable, CVCL::VariableValue, CVCL::Literal, CVCL::Variable
• SearchEngine() : CVCL::SearchEngine
• SearchEngineFast() : CVCL::SearchEngineFast
• SearchEngineTheoremProducer() : CVCL::SearchEngineTheoremProducer
• SearchImplBase() : CVCL::SearchImplBase
• SearchSat() : CVCL::SearchSat
• SearchSatCoreSatAPI : CVCL::SearchSatCoreSatAPI, CVCL::SearchSat
• SearchSatDecider : CVCL::SearchSatDecider, CVCL::SearchSat
• SearchSatTheoryAPI : CVCL::SearchSatTheoryAPI, CVCL::SearchSat
• SearchSimple() : CVCL::SearchSimple
• selectLargest() : CVCL::TheoryArith::VarOrderGraph
• selectSmallest() : CVCL::TheoryArith::VarOrderGraph
• semCheckSat() : CVCL::TheoryQuant
• semInst() : CVCL::TheoryQuant
• separateMonomial() : CVCL::TheoryArith
• set() : CLitPoolElement, CVCL::SmartCDO< T >, CVCL::CDO< T >, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::CDFlags
• set_allow_multiple_conflict() : CSolver
• set_allow_multiple_conflict_clause() : CSolver
• set_antecedence() : CVariable
• set_clause_index() : CLitPoolElement
• set_cls_del_interval() : CSolver
• set_decision_strategy() : CSolver
• set_ht() : CLitPoolElement
• set_in_new_cl() : CVariable
• set_marked() : CVariable
• set_max_conflict_clause_length() : CSolver
• set_max_unrelevance() : CSolver
• set_mem_limit() : CSolver, CDatabase
• set_min_num_clause_lits_for_delete() : CSolver
• Set_Next_Hash_Entry() : CVCL::Hash_Ptr< _Key, _Data >
• set_preprocess_strategy() : CSolver
• set_random_seed() : CSolver
• set_randomness() : CSolver
• set_time_limit() : CSolver
• set_var_value() : CSolver
• set_var_value_not_current_dl() : CSolver
• set_var_value_with_current_dl() : CSolver
• set_variable_number() : CDatabase
• setAssumpThm() : CVCL::VariableValue, CVCL::Variable
• setBottomScope() : SAT::CNF_Manager
• SetBudget() : Xchaff, SatSolver
• setCachedValue() : CVCL::TheoremValue, CVCL::Theorem
• setComputeTransClosure() : CVCL::Expr
• setConst() : CVCL::Assumptions
• setCurrentTime() : CVCL::Debug
• setElapsed() : CVCL::Debug
• setExpandFlag() : CVCL::TheoremValue, CVCL::Theorem
• setFind() : CVCL::Expr
• setFinite() : CVCL::Expr
• setFlag() : CVCL::TheoremValue, CVCL::Theorem, CVCL::Expr, CVCL::CLFlags
• setId() : SAT::Clause
• setImpliedLiteral() : CVCL::Expr
• setIncomplete() : CVCL::TheoryCore, CVCL::Theory
• setInconsistent() : CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngineFast
• setIndex() : CVCL::ExprValue
• setIntAssumption() : CVCL::Expr
• setIsAtomicFlag() : CVCL::Expr
• setJustified() : CVCL::SearchSat, CVCL::Expr
• setLitFlag() : CVCL::TheoremValue, CVCL::Theorem
• SetMemLimit() : Xchaff, SatSolver
• setMessage() : CVCL::Exception
• setNull() : CVCL::ContextObj, CVCL::CDO< T >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMapOrderedData, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDMapData, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::CDList< T >, CVCL::CDFlags
• setNumVars() : SAT::CD_CNF_Formula, SAT::CNF_Formula_Impl, SAT::CNF_Formula
• setOS() : CVCL::Debug
• setPrompt1() : CVCL::ParserTemp
• setPrompt2() : CVCL::ParserTemp
• SetRandomness() : Xchaff, SatSolver
• SetRandSeed() : Xchaff, SatSolver
• setRep() : CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• setResourceLimit() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore
• setRestorePoint() : CVCL::SearchEngineFast::ConflictClauseManager
• setRewriteNormal() : CVCL::Expr
• setSatisfied() : SAT::Clause
• setSelected() : CVCL::Expr
• setSig() : CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• setSimpCache() : CVCL::Expr
• setSimpFrom() : CVCL::ExprValue, CVCL::Expr
• setSubtypePred() : CVCL::Expr
• setTCC() : CVCL::Expr
• setTranslated() : CVCL::Expr
• setType() : CVCL::Expr
• setUnit() : SAT::Clause
• setup() : CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatypeLazy, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• setupCC() : CVCL::Theory
• setupExpr() : CVCL::TheoryBitvector
• setupRec() : CVCL::TheoryArith
• setupSubFormulas() : CVCL::TheoryCore
• setupTerm() : CVCL::TheoryCore
• setupTriggers() : CVCL::TheoryQuant
• setUserAssumption() : CVCL::Expr
• setUserRegisteredAtom() : CVCL::Expr
• setValidType() : CVCL::Expr
• setValue() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::SearchSat
• SetVerbosity() : CVCL::SVC_API_impl
• setWellFounded() : CVCL::Expr
• signBVLTRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• signExtendBVLT() : CVCL::TheoryBitvector
• signExtendRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• simplifiedMultExpr() : CVCL::ArithTheoremProducer
• simplify() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory, CVCL::SearchImplBase, SAT::CNF_Formula_Impl
• simplifyExpr() : CVCL::Theory
• simplifyFullRec() : CVCL::TheoryCore
• simplifyInPlaceRec() : CVCL::TheoryCore
• simplifyOp() : CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::Theory
• simplifyRec() : CVCL::TheoryCore, CVCL::Theory
• simplifyThm() : CVCL::VCL, CVCL::ValidityChecker
• simplifyThm2() : CVCL::VCL, CVCL::ValidityChecker
• simulateExpr() : CVCL::VCL, CVCL::ValidityChecker
• SimulateTheoremProducer() : CVCL::SimulateTheoremProducer
• size() : CVCL::Hash_Table< _Key, _Data >, CVCL::BVConstExpr, CVCL::NotifyList, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, SAT::Clause, CVCL::Clause, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDList< T >, CVCL::Assumptions
• skolemExpr() : CVCL::Expr
• skolemize() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• skolemizeAx() : CVCL::VCCmd
• skolemizeRewrite() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• skolemizeRewriteVar() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• SmartCDO : CVCL::SmartCDO< T >, CVCL::SmartCDO< T >::RefCDO< U >
• SmtlibException() : CVCL::SmtlibException
• solve() : CSolver, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• solvedForm() : CVCL::TheoryArith
• soundError() : CVCL::TheoremProducer
• SoundException() : CVCL::SoundException
• space : CVCL::ExprStream
• split() : CVCL::SearchEngineFast
• splitGrayShadow() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• Splitter() : CVCL::SearchImplBase::Splitter
• stackLevel() : CVCL::VCL, CVCL::ValidityChecker
• start_cpu_time : CSolverStats
• start_world_time : CSolverStats
• StatCounter() : CVCL::StatCounter
• StatCounterMap : CVCL::Statistics
• StatFlag() : CVCL::StatFlag
• StatFlagMap : CVCL::Statistics
• StaticFlagsEnum : CVCL::Expr
• Statistics() : CVCL::Statistics
• stats() : CDatabase
• strict() : CVCL::TheoryArith::FreeConst
• stringExpr() : CVCL::VCL, CVCL::ValidityChecker
• subExprOf() : CVCL::Expr
• subrangeType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryArith
• subst() : CVCL::RefinedArithTheoremProducer
• substAndCanonize() : CVCL::TheoryArith
• substExpr() : CVCL::Expr
• substitute() : CVCL::ArithTheoremProducer, CVCL::ExprTransform
• substitutivityRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• subtypePredicate() : CVCL::TheoryCore, CVCL::Theory
• subtypeType() : CVCL::VCL, CVCL::ValidityChecker
• sumModM() : CVCL::ArithTheoremProducer
• sumMulF() : CVCL::ArithTheoremProducer
• sumNormalizedElements() : CVCL::BitvectorTheoremProducer
• sv : CVCL::CLFlag
• SVC_API_impl() : CVCL::SVC_API_impl
• SVCAssert() : CVCL::SVC_API_impl
• SVCDeny() : CVCL::SVC_API_impl
• switchContext() : CVCL::ContextManager
• symm() : CVCL::RefinedArithTheoremProducer
• symmetryRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• synCheckSat() : CVCL::TheoryQuant
• synInst() : CVCL::TheoryQuant

---