SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Member Functions | Private Attributes
smtrat::mcsat::icp::Dependencies Class Reference

#include <Dependencies.h>

Collaboration diagram for smtrat::mcsat::icp::Dependencies:
Collaboration graph
[legend]

Public Member Functions

template<typename Contractor >
void add (const Contractor &c)
 
void add (carl::Variable v, const FormulaT &c, const std::vector< carl::Variable > &used)
 
std::vector< FormulaT > get (carl::Variable v, bool negate=true) const
 

Private Member Functions

std::size_t get_constraint_id (const FormulaT &c)
 

Private Attributes

std::vector< FormulaT > mConstraints
 
std::map< FormulaT, std::size_t > mConstraintIDs
 
std::map< carl::Variable, carl::Bitset > mData
 

Detailed Description

Definition at line 10 of file Dependencies.h.

Member Function Documentation

◆ add() [1/2]

void smtrat::mcsat::icp::Dependencies::add ( carl::Variable  v,
const FormulaT &  c,
const std::vector< carl::Variable > &  used 
)
inline

Definition at line 30 of file Dependencies.h.

Here is the call graph for this function:

◆ add() [2/2]

template<typename Contractor >
void smtrat::mcsat::icp::Dependencies::add ( const Contractor &  c)
inline

Definition at line 26 of file Dependencies.h.

Here is the caller graph for this function:

◆ get()

std::vector<FormulaT> smtrat::mcsat::icp::Dependencies::get ( carl::Variable  v,
bool  negate = true 
) const
inline

Definition at line 40 of file Dependencies.h.

Here is the caller graph for this function:

◆ get_constraint_id()

std::size_t smtrat::mcsat::icp::Dependencies::get_constraint_id ( const FormulaT &  c)
inlineprivate

Definition at line 16 of file Dependencies.h.

Here is the caller graph for this function:

Field Documentation

◆ mConstraintIDs

std::map<FormulaT,std::size_t> smtrat::mcsat::icp::Dependencies::mConstraintIDs
private

Definition at line 13 of file Dependencies.h.

◆ mConstraints

std::vector<FormulaT> smtrat::mcsat::icp::Dependencies::mConstraints
private

Definition at line 12 of file Dependencies.h.

◆ mData

std::map<carl::Variable,carl::Bitset> smtrat::mcsat::icp::Dependencies::mData
private

Definition at line 14 of file Dependencies.h.

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