SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Data Fields
smtrat::covering_ng::CoveringResult< PropertiesSet > Struct Template Reference

#include <types.h>

Public Member Functions

 CoveringResult ()
 
 CoveringResult (Status s)
 
 CoveringResult (Status s, std::vector< Interval< PropertiesSet >> &inter)
 
 CoveringResult (Status s, std::vector< Interval< PropertiesSet >> &&inter)
 
 CoveringResult (Status s, const cadcells::Assignment &ass)
 
 CoveringResult (Status s, const std::optional< cadcells::Assignment > &ass)
 
 CoveringResult (Status s, const cadcells::Assignment &ass, const std::vector< Interval< PropertiesSet >> &inter)
 
 CoveringResult (Status s, const std::optional< cadcells::Assignment > &ass, const std::vector< Interval< PropertiesSet >> &inter)
 
bool is_failed () const
 
bool is_failed_projection () const
 
bool is_sat () const
 
bool is_unsat () const
 
bool is_parameter () const
 
const auto & sample () const
 
const auto & intervals () const
 

Data Fields

Status status
 
std::optional< std::vector< Interval< PropertiesSet > > > m_intervals
 
std::optional< cadcells::Assignment > m_sample
 

Detailed Description

template<typename PropertiesSet>
struct smtrat::covering_ng::CoveringResult< PropertiesSet >

Definition at line 37 of file types.h.

Constructor & Destructor Documentation

◆ CoveringResult() [1/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( )
inline

Definition at line 42 of file types.h.

◆ CoveringResult() [2/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( Status  s)
inlineexplicit

Definition at line 43 of file types.h.

◆ CoveringResult() [3/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( Status  s,
std::vector< Interval< PropertiesSet >> &  inter 
)
inline

Definition at line 46 of file types.h.

◆ CoveringResult() [4/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( Status  s,
std::vector< Interval< PropertiesSet >> &&  inter 
)
inline

Definition at line 47 of file types.h.

◆ CoveringResult() [5/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( Status  s,
const cadcells::Assignment &  ass 
)
inline

Definition at line 48 of file types.h.

◆ CoveringResult() [6/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( Status  s,
const std::optional< cadcells::Assignment > &  ass 
)
inline

Definition at line 49 of file types.h.

◆ CoveringResult() [7/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( Status  s,
const cadcells::Assignment &  ass,
const std::vector< Interval< PropertiesSet >> &  inter 
)
inline

Definition at line 50 of file types.h.

◆ CoveringResult() [8/8]

template<typename PropertiesSet >
smtrat::covering_ng::CoveringResult< PropertiesSet >::CoveringResult ( Status  s,
const std::optional< cadcells::Assignment > &  ass,
const std::vector< Interval< PropertiesSet >> &  inter 
)
inline

Definition at line 51 of file types.h.

Member Function Documentation

◆ intervals()

template<typename PropertiesSet >
const auto& smtrat::covering_ng::CoveringResult< PropertiesSet >::intervals ( ) const
inline

Definition at line 71 of file types.h.

Here is the caller graph for this function:

◆ is_failed()

template<typename PropertiesSet >
bool smtrat::covering_ng::CoveringResult< PropertiesSet >::is_failed ( ) const
inline

Definition at line 53 of file types.h.

Here is the caller graph for this function:

◆ is_failed_projection()

template<typename PropertiesSet >
bool smtrat::covering_ng::CoveringResult< PropertiesSet >::is_failed_projection ( ) const
inline

Definition at line 56 of file types.h.

◆ is_parameter()

template<typename PropertiesSet >
bool smtrat::covering_ng::CoveringResult< PropertiesSet >::is_parameter ( ) const
inline

Definition at line 65 of file types.h.

◆ is_sat()

template<typename PropertiesSet >
bool smtrat::covering_ng::CoveringResult< PropertiesSet >::is_sat ( ) const
inline

Definition at line 59 of file types.h.

Here is the caller graph for this function:

◆ is_unsat()

template<typename PropertiesSet >
bool smtrat::covering_ng::CoveringResult< PropertiesSet >::is_unsat ( ) const
inline

Definition at line 62 of file types.h.

Here is the caller graph for this function:

◆ sample()

template<typename PropertiesSet >
const auto& smtrat::covering_ng::CoveringResult< PropertiesSet >::sample ( ) const
inline

Definition at line 68 of file types.h.

Here is the caller graph for this function:

Field Documentation

◆ m_intervals

template<typename PropertiesSet >
std::optional<std::vector<Interval<PropertiesSet> > > smtrat::covering_ng::CoveringResult< PropertiesSet >::m_intervals

Definition at line 39 of file types.h.

◆ m_sample

template<typename PropertiesSet >
std::optional<cadcells::Assignment> smtrat::covering_ng::CoveringResult< PropertiesSet >::m_sample

Definition at line 40 of file types.h.

◆ status

template<typename PropertiesSet >
Status smtrat::covering_ng::CoveringResult< PropertiesSet >::status

Definition at line 38 of file types.h.

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