SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Attributes
smtrat::SATModule< Settings >::LiteralClauses Struct Reference
Collaboration diagram for smtrat::SATModule< Settings >::LiteralClauses:
Collaboration graph
[legend]

Public Member Functions

 LiteralClauses ()
 
 LiteralClauses (const LiteralClauses &)=delete
 
 LiteralClauses (LiteralClauses &&_toMove)
 
 ~LiteralClauses ()
 
const std::vector< Minisat::CRef > & positives () const
 
const std::vector< Minisat::CRef > & negatives () const
 
void addPositive (Minisat::CRef _cref)
 
void addNegative (Minisat::CRef _cref)
 
void removePositive (Minisat::CRef _cref)
 
void removeNegative (Minisat::CRef _cref)
 
void reloc (Minisat::ClauseAllocator &_ca, Minisat::ClauseAllocator &_to)
 
size_t numOfNegatives () const
 
size_t numOfPositives () const
 

Private Attributes

std::vector< Minisat::CRef > mPositives
 
std::vector< Minisat::CRef > mNegatives
 

Detailed Description

template<class Settings>
struct smtrat::SATModule< Settings >::LiteralClauses

Definition at line 338 of file SATModule.h.

Constructor & Destructor Documentation

◆ LiteralClauses() [1/3]

template<class Settings >
smtrat::SATModule< Settings >::LiteralClauses::LiteralClauses ( )
inline

Definition at line 346 of file SATModule.h.

◆ LiteralClauses() [2/3]

template<class Settings >
smtrat::SATModule< Settings >::LiteralClauses::LiteralClauses ( const LiteralClauses &  )
delete

◆ LiteralClauses() [3/3]

template<class Settings >
smtrat::SATModule< Settings >::LiteralClauses::LiteralClauses ( LiteralClauses &&  _toMove)
inline

Definition at line 348 of file SATModule.h.

◆ ~LiteralClauses()

template<class Settings >
smtrat::SATModule< Settings >::LiteralClauses::~LiteralClauses ( )
inline

Definition at line 352 of file SATModule.h.

Member Function Documentation

◆ addNegative()

template<class Settings >
void smtrat::SATModule< Settings >::LiteralClauses::addNegative ( Minisat::CRef  _cref)
inline

Definition at line 369 of file SATModule.h.

◆ addPositive()

template<class Settings >
void smtrat::SATModule< Settings >::LiteralClauses::addPositive ( Minisat::CRef  _cref)
inline

Definition at line 364 of file SATModule.h.

◆ negatives()

template<class Settings >
const std::vector<Minisat::CRef>& smtrat::SATModule< Settings >::LiteralClauses::negatives ( ) const
inline

Definition at line 359 of file SATModule.h.

◆ numOfNegatives()

template<class Settings >
size_t smtrat::SATModule< Settings >::LiteralClauses::numOfNegatives ( ) const
inline

Definition at line 402 of file SATModule.h.

◆ numOfPositives()

template<class Settings >
size_t smtrat::SATModule< Settings >::LiteralClauses::numOfPositives ( ) const
inline

Definition at line 407 of file SATModule.h.

◆ positives()

template<class Settings >
const std::vector<Minisat::CRef>& smtrat::SATModule< Settings >::LiteralClauses::positives ( ) const
inline

Definition at line 354 of file SATModule.h.

◆ reloc()

template<class Settings >
void smtrat::SATModule< Settings >::LiteralClauses::reloc ( Minisat::ClauseAllocator &  _ca,
Minisat::ClauseAllocator &  _to 
)
inline

Definition at line 394 of file SATModule.h.

Here is the call graph for this function:

◆ removeNegative()

template<class Settings >
void smtrat::SATModule< Settings >::LiteralClauses::removeNegative ( Minisat::CRef  _cref)
inline

Definition at line 384 of file SATModule.h.

Here is the call graph for this function:

◆ removePositive()

template<class Settings >
void smtrat::SATModule< Settings >::LiteralClauses::removePositive ( Minisat::CRef  _cref)
inline

Definition at line 374 of file SATModule.h.

Here is the call graph for this function:

Field Documentation

◆ mNegatives

template<class Settings >
std::vector<Minisat::CRef> smtrat::SATModule< Settings >::LiteralClauses::mNegatives
private

Definition at line 342 of file SATModule.h.

◆ mPositives

template<class Settings >
std::vector<Minisat::CRef> smtrat::SATModule< Settings >::LiteralClauses::mPositives
private

Definition at line 341 of file SATModule.h.

The documentation for this struct was generated from the following file: