SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Attributes | Friends
smtrat::mcsat::ClauseChain::Link Struct Reference

#include <ClauseChain.h>

Public Member Functions

 Link (const FormulaT &&clause, const FormulaT &&impliedTseitinLiteral)
 
 Link (const FormulaT &&clause)
 
bool isPropagating () const
 
bool isConflicting () const
 
bool isOptional () const
 
const FormulaT & clause () const
 
const FormulaT & impliedTseitinLiteral () const
 

Private Attributes

FormulaT mClause
 
std::optional< FormulaT > mImpliedTseitinLiteral
 

Friends

std::ostream & operator<< (std::ostream &stream, const Link &link)
 

Detailed Description

Definition at line 18 of file ClauseChain.h.

Constructor & Destructor Documentation

◆ Link() [1/2]

smtrat::mcsat::ClauseChain::Link::Link ( const FormulaT &&  clause,
const FormulaT &&  impliedTseitinLiteral 
)
inline

Definition at line 24 of file ClauseChain.h.

◆ Link() [2/2]

smtrat::mcsat::ClauseChain::Link::Link ( const FormulaT &&  clause)
inline

Definition at line 27 of file ClauseChain.h.

Member Function Documentation

◆ clause()

const FormulaT& smtrat::mcsat::ClauseChain::Link::clause ( ) const
inline

Definition at line 42 of file ClauseChain.h.

◆ impliedTseitinLiteral()

const FormulaT& smtrat::mcsat::ClauseChain::Link::impliedTseitinLiteral ( ) const
inline

Definition at line 46 of file ClauseChain.h.

Here is the call graph for this function:

◆ isConflicting()

bool smtrat::mcsat::ClauseChain::Link::isConflicting ( ) const
inline

Definition at line 34 of file ClauseChain.h.

◆ isOptional()

bool smtrat::mcsat::ClauseChain::Link::isOptional ( ) const
inline

Definition at line 38 of file ClauseChain.h.

◆ isPropagating()

bool smtrat::mcsat::ClauseChain::Link::isPropagating ( ) const
inline

Definition at line 30 of file ClauseChain.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  stream,
const Link &  link 
)
friend

Definition at line 142 of file ClauseChain.h.

Field Documentation

◆ mClause

FormulaT smtrat::mcsat::ClauseChain::Link::mClause
private

Definition at line 20 of file ClauseChain.h.

◆ mImpliedTseitinLiteral

std::optional<FormulaT> smtrat::mcsat::ClauseChain::Link::mImpliedTseitinLiteral
private

Definition at line 21 of file ClauseChain.h.

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