Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:

[detail level 12345]

CBitset	A class representing a bitset with dynamic size
CBloomFilter
CClauseBuffer	Wrapper for boost::lockfree::queue to manage ClauseExchange objects
▼CClauseDatabase	Abstract base class defining the interface for clause storage and management
CClauseDatabaseBufferPerEntity	A clause database that maintain separate buffers for each entity, mimicing old painless default behavior
CClauseDatabaseMallob	A clause database implementation attempting to naively mimic the Simplified Adaptive Database from Mallob (ref:https://doi.org/10.1613/jair.1.15827)
CClauseDatabasePerSize	A clause database that organizes clauses based on their size
CClauseDatabaseSingleBuffer	This is just a ClauseDatabase wrapper around a ClauseBuufer
CClauseExchange	Represents an exchangeable clause with flexible array member
CClauseUtils::ClauseExchangeEqual	Equality functor for ClauseExchange objects
CClauseUtils::ClauseExchangeHash	Hash functor for ClauseExchange objects
CClauseUtils::ClauseExchangePtrEqual	Equality functor for ClauseExchangePtr objects
CClauseUtils::ClauseExchangePtrHash	Hash functor for ClauseExchangePtr objects
CClauseUtils::ClauseHash	Hash functor for simple clauses
CClauseMeta
▼CParsers::ClauseProcessor	Abstract base class for clause processors
CParsers::RedundancyFilter	Filter for removing redundant clauses
CParsers::SBVAInit	A filter for Structured BVA (Binary Variable Addition)
CParsers::TautologyFilter	Filter for removing tautological clauses. A tautological clause or simple a tautology is a clause that contains a literal and its complement, thus always satisfied
CDataType
▼Cstd::enable_shared_from_this
▼CSharingEntity	A base class representing entities that can exchange clauses between themselves
▼CSharingStrategy	SharingStrategy class, inheriting from SharingEntity
▼CGlobalSharingStrategy	Base class for global clause sharing strategies across MPI processes
CAllGatherSharing	Implements a global sharing strategy using MPI_Allgather for clause exchange
CGenericGlobalSharing	Implements a generic global sharing strategy for clause exchange
CMallobSharing	Implements a global sharing strategy based on the Mallob algorithm
CHordeSatSharing	This strategy is a HordeSat-like sharing strategy
CSimpleSharing	This strategy is a simple sharing strategy
▼CSolverCdclInterface	Interface for CDCL (Conflict-Driven Clause Learning) solvers This class provides a common interface for all CDCL solvers. It inherits from SolverInterface for solving primitives and SharingEntity for sharing primitives
CCadical	Implements the different interfaces to interact with the Cadical CDCL solver
CGlucoseSyrup	Instance of a Glucose solver
CKissat	Instance of a Kissat solver
CKissatINCSolver	Instance of a KissatINCSolver solver
CKissatMABSolver	Instance of a KissatMABSolver solver
CLingeling	Instance of a Lingeling solver
CMapleCOMSPSSolver	Instance of a MapleCOMSPS solver
CMiniSat	Instance of a Minisat solver
Cfnv< T, Enable >	Struct for Fowler-Noll-Vo parameters
Cfnv< T, typename std::enable_if< sizeof(T)==4 >::type >	Fowler-Noll-Vo hash parameters for 32 bits
Cfnv< T, typename std::enable_if< sizeof(T)==8 >::type >	Fowler-Noll-Vo hash parameters for 64 bits
CFormula	Represents a SAT formula with unit and non-unit clauses
CHashMap
CHashNode
Cpainless::skipzero_span< T >::Iterator
▼CCaDiCaL::Learner
CCadical	Implements the different interfaces to interact with the Cadical CDCL solver
CLocalSearchStats	Local search statistics
CMutex	Mutex class
CPairCompare	Functor for the priority queue used in solve()
Cparameter
CParameters
CPreprocessorStats	Preperocessing technique statistics
CProofClause
CqueuePair	QueuePair struct used for the priorityQueue in solve
CSharer	A sharer is a thread responsible for executing a list of SharingStrategies
▼CSharingStatistics	Local Sharing statistics.Sharing statistics
CGlobalSharingStatistics	Statistics of a global sharing strategy
CSharingStrategyFactory	Factory class for creating and managing sharing strategies
Cpainless::skipzero_span< T >	A span-like container that skips zero elements when iterating
CSolverFactory	Factory class for creating and managing SAT solvers
▼CSolverInterface	Interface for a SAT solver with standard features
▼CLocalSearchInterface	Interface for Local Search solvers
CYalSat	Implements LocalSearchInterface to interact with the YalSAT local search solver
▼CPreprocessorInterface	Interface for preprocessor algorithms in SAT solving
CStructuredBVA	Structured Binary Variable Addition (SBVA) preprocessing algorithm
Cpreprocess	The different simplification techniques implemented in PRS framework
CSolverCdclInterface	Interface for CDCL (Conflict-Driven Clause Learning) solvers This class provides a common interface for all CDCL solvers. It inherits from SolverInterface for solving primitives and SharingEntity for sharing primitives
CSolvingCdclStatistics	Structure for solver statistics
▼CCaDiCaL::Terminator
CCadical	Implements the different interfaces to interact with the Cadical CDCL solver
CThread	Thread class
Ctype_gate
CGlucose::vec< T >
CMapleCOMSPS::vec< T >
CMinisat::vec< T, _Size >
Cpainless::vector2D< T >	A 2D vector implementation optimized for sparse data
Cpainless::vector2D< int >
▼CWorkingStrategy	Base Interface for Working Strategies
CPortfolioPRS	An Implementation of WorkingStrategy that mimics the strategy used in the PRS-Distributed solver from ISC24
CPortfolioSimple	A Simple Implementation of WorkingStrategy for the portfolio parallel strategy This strategy uses the different factories SolverFactory and SharingStrategyFactory in order to instantiate the different needed components specified by the parameters
CSequentialWorker	Basic Implementation of WorkingStrategy for a sequential execution
Cxorgate