SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Types | Public Member Functions | Static Public Member Functions | Data Fields
smtrat::fmplex::Node Struct Reference

#include <Node.h>

Collaboration diagram for smtrat::fmplex::Node:
Collaboration graph
[legend]

Public Types

enum class  Type {
  UNDETERMINED , CONFLICT , LEAF , LBS ,
  UBS , NBS , FM
}
 
using RowIndex = Matrix::RowIndex
 
using ColIndex = Matrix::ColIndex
 

Public Member Functions

 Node (bool is_sat)
 
 Node ()
 
 Node (const Matrix &m, const std::vector< ColIndex > &cols)
 
 Node (const Matrix &m, const std::vector< ColIndex > &cols, const std::set< RowIndex > &ign)
 
 Node (Matrix &&m, const std::vector< ColIndex > &cols)
 
bool is_conflict () const
 
bool is_finished () const
 
void choose_elimination ()
 

Static Public Member Functions

static Node conflict ()
 
static Node leaf ()
 

Data Fields

Matrix matrix
 
Type type = Type::UNDETERMINED
 
ColIndex chosen_col
 
std::vector< ColIndex > cols_to_elim
 
std::vector< RowIndex > eliminators
 
std::set< RowIndex > ignored
 

Detailed Description

Definition at line 10 of file Node.h.

Member Typedef Documentation

◆ ColIndex

using smtrat::fmplex::Node::ColIndex = Matrix::ColIndex

Definition at line 12 of file Node.h.

◆ RowIndex

using smtrat::fmplex::Node::RowIndex = Matrix::RowIndex

Definition at line 11 of file Node.h.

Member Enumeration Documentation

◆ Type

enum smtrat::fmplex::Node::Type
strong
Enumerator
UNDETERMINED 
CONFLICT 
LEAF 
LBS 
UBS 
NBS 
FM 

Definition at line 14 of file Node.h.

Constructor & Destructor Documentation

◆ Node() [1/5]

smtrat::fmplex::Node::Node ( bool  is_sat)
inline

Definition at line 23 of file Node.h.

Here is the call graph for this function:

◆ Node() [2/5]

smtrat::fmplex::Node::Node ( )
inline

Definition at line 28 of file Node.h.

Here is the caller graph for this function:

◆ Node() [3/5]

smtrat::fmplex::Node::Node ( const Matrix &  m,
const std::vector< ColIndex > &  cols 
)
inline

Definition at line 30 of file Node.h.

◆ Node() [4/5]

smtrat::fmplex::Node::Node ( const Matrix &  m,
const std::vector< ColIndex > &  cols,
const std::set< RowIndex > &  ign 
)
inline

Definition at line 34 of file Node.h.

◆ Node() [5/5]

smtrat::fmplex::Node::Node ( Matrix &&  m,
const std::vector< ColIndex > &  cols 
)
inline

Definition at line 39 of file Node.h.

Member Function Documentation

◆ choose_elimination()

void smtrat::fmplex::Node::choose_elimination ( )
inline

Definition at line 50 of file Node.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ conflict()

static Node smtrat::fmplex::Node::conflict ( )
inlinestatic

Definition at line 47 of file Node.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ is_conflict()

bool smtrat::fmplex::Node::is_conflict ( ) const
inline

Definition at line 44 of file Node.h.

◆ is_finished()

bool smtrat::fmplex::Node::is_finished ( ) const
inline

Definition at line 45 of file Node.h.

◆ leaf()

static Node smtrat::fmplex::Node::leaf ( )
inlinestatic

Definition at line 48 of file Node.h.

Here is the call graph for this function:
Here is the caller graph for this function:

Field Documentation

◆ chosen_col

ColIndex smtrat::fmplex::Node::chosen_col

Definition at line 18 of file Node.h.

◆ cols_to_elim

std::vector<ColIndex> smtrat::fmplex::Node::cols_to_elim

Definition at line 19 of file Node.h.

◆ eliminators

std::vector<RowIndex> smtrat::fmplex::Node::eliminators

Definition at line 20 of file Node.h.

◆ ignored

std::set<RowIndex> smtrat::fmplex::Node::ignored

Definition at line 21 of file Node.h.

◆ matrix

Matrix smtrat::fmplex::Node::matrix

Definition at line 16 of file Node.h.

◆ type

Type smtrat::fmplex::Node::type = Type::UNDETERMINED

Definition at line 17 of file Node.h.

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