SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Types | Private Attributes
smtrat::Backend< Settings > Class Template Reference

#include <Backend.h>

Collaboration diagram for smtrat::Backend< Settings >:
Collaboration graph
[legend]

Public Member Functions

 Backend ()
 
void init (std::vector< carl::Variable > &varOrdering)
 
std::size_t dimension ()
 
std::shared_ptr< cadcells::Polynomial::ContextType > getContext ()
 
const carl::Assignment< cadcells::RAN > & getCurrentAssignment ()
 
auto & getCoveringInformation ()
 
FormulaSetT getInfeasibleSubset ()
 
void addConstraint (const ConstraintT &constraint)
 
void addConstraint (const size_t level, const std::vector< ConstraintT > &&constraints)
 
auto & getUnknownConstraints ()
 
auto & getUnknownConstraints (std::size_t &level)
 
auto & getKnownConstraints ()
 
auto & getKnownConstraints (std::size_t &level)
 
void updateAssignment (std::size_t level)
 
void resetStoredData (std::size_t level)
 
void resetDerivationToConstraintMap ()
 
void removeConstraint (const ConstraintT &constraint)
 
void setConstraintsKnown (const std::size_t &level)
 
void setConstraintsUnknown (const std::size_t &level)
 
void processUnknownConstraints (const std::size_t &level, const bool prune_assignment)
 
Answer getUnsatCover (const std::size_t level)
 

Private Types

using op = typename Settings::op
 
using PropSet = typename op::PropertiesSet
 

Private Attributes

std::shared_ptr< cadcells::Polynomial::ContextType > mContext
 
std::vector< boost::container::flat_set< cadcells::Constraint > > mUnknownConstraints
 
std::vector< boost::container::flat_set< cadcells::Constraint > > mKnownConstraints
 
std::shared_ptr< datastructures::PolyPool > mPool
 
std::shared_ptr< datastructures::Projections > mProjections
 
carl::Assignment< cadcells::RAN > mCurrentAssignment
 
std::vector< LevelWiseInformation< Settings > > mCoveringInformation
 
std::map< datastructures::SampledDerivationRef< PropSet >, std::vector< cadcells::Constraint > > mDerivationToConstraint
 

Detailed Description

template<typename Settings>
class smtrat::Backend< Settings >

Definition at line 41 of file Backend.h.

Member Typedef Documentation

◆ op

template<typename Settings >
using smtrat::Backend< Settings >::op = typename Settings::op
private

Definition at line 43 of file Backend.h.

◆ PropSet

template<typename Settings >
using smtrat::Backend< Settings >::PropSet = typename op::PropertiesSet
private

Definition at line 44 of file Backend.h.

Constructor & Destructor Documentation

◆ Backend()

template<typename Settings >
smtrat::Backend< Settings >::Backend ( )
inline

Definition at line 73 of file Backend.h.

Member Function Documentation

◆ addConstraint() [1/2]

template<typename Settings >
void smtrat::Backend< Settings >::addConstraint ( const ConstraintT &  constraint)
inline

Definition at line 124 of file Backend.h.

Here is the call graph for this function:

◆ addConstraint() [2/2]

template<typename Settings >
void smtrat::Backend< Settings >::addConstraint ( const size_t  level,
const std::vector< ConstraintT > &&  constraints 
)
inline

Definition at line 133 of file Backend.h.

Here is the call graph for this function:

◆ dimension()

template<typename Settings >
std::size_t smtrat::Backend< Settings >::dimension ( )
inline

Definition at line 91 of file Backend.h.

Here is the caller graph for this function:

◆ getContext()

template<typename Settings >
std::shared_ptr<cadcells::Polynomial::ContextType> smtrat::Backend< Settings >::getContext ( )
inline

Definition at line 95 of file Backend.h.

◆ getCoveringInformation()

template<typename Settings >
auto& smtrat::Backend< Settings >::getCoveringInformation ( )
inline

Definition at line 103 of file Backend.h.

◆ getCurrentAssignment()

template<typename Settings >
const carl::Assignment<cadcells::RAN>& smtrat::Backend< Settings >::getCurrentAssignment ( )
inline

Definition at line 99 of file Backend.h.

◆ getInfeasibleSubset()

template<typename Settings >
FormulaSetT smtrat::Backend< Settings >::getInfeasibleSubset ( )
inline

Definition at line 108 of file Backend.h.

◆ getKnownConstraints() [1/2]

template<typename Settings >
auto& smtrat::Backend< Settings >::getKnownConstraints ( )
inline

Definition at line 150 of file Backend.h.

◆ getKnownConstraints() [2/2]

template<typename Settings >
auto& smtrat::Backend< Settings >::getKnownConstraints ( std::size_t &  level)
inline

Definition at line 154 of file Backend.h.

◆ getUnknownConstraints() [1/2]

template<typename Settings >
auto& smtrat::Backend< Settings >::getUnknownConstraints ( )
inline

Definition at line 142 of file Backend.h.

◆ getUnknownConstraints() [2/2]

template<typename Settings >
auto& smtrat::Backend< Settings >::getUnknownConstraints ( std::size_t &  level)
inline

Definition at line 146 of file Backend.h.

◆ getUnsatCover()

template<typename Settings >
Answer smtrat::Backend< Settings >::getUnsatCover ( const std::size_t  level)
inline

Definition at line 271 of file Backend.h.

Here is the call graph for this function:

◆ init()

template<typename Settings >
void smtrat::Backend< Settings >::init ( std::vector< carl::Variable > &  varOrdering)
inline

Definition at line 78 of file Backend.h.

◆ processUnknownConstraints()

template<typename Settings >
void smtrat::Backend< Settings >::processUnknownConstraints ( const std::size_t &  level,
const bool  prune_assignment 
)
inline

Definition at line 243 of file Backend.h.

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

◆ removeConstraint()

template<typename Settings >
void smtrat::Backend< Settings >::removeConstraint ( const ConstraintT &  constraint)
inline

Definition at line 185 of file Backend.h.

Here is the call graph for this function:

◆ resetDerivationToConstraintMap()

template<typename Settings >
void smtrat::Backend< Settings >::resetDerivationToConstraintMap ( )
inline

Definition at line 180 of file Backend.h.

Here is the caller graph for this function:

◆ resetStoredData()

template<typename Settings >
void smtrat::Backend< Settings >::resetStoredData ( std::size_t  level)
inline

Definition at line 163 of file Backend.h.

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

◆ setConstraintsKnown()

template<typename Settings >
void smtrat::Backend< Settings >::setConstraintsKnown ( const std::size_t &  level)
inline

Definition at line 226 of file Backend.h.

Here is the caller graph for this function:

◆ setConstraintsUnknown()

template<typename Settings >
void smtrat::Backend< Settings >::setConstraintsUnknown ( const std::size_t &  level)
inline

Definition at line 233 of file Backend.h.

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

◆ updateAssignment()

template<typename Settings >
void smtrat::Backend< Settings >::updateAssignment ( std::size_t  level)
inline

Definition at line 158 of file Backend.h.

Here is the caller graph for this function:

Field Documentation

◆ mContext

template<typename Settings >
std::shared_ptr<cadcells::Polynomial::ContextType> smtrat::Backend< Settings >::mContext
private

Definition at line 48 of file Backend.h.

◆ mCoveringInformation

template<typename Settings >
std::vector<LevelWiseInformation<Settings> > smtrat::Backend< Settings >::mCoveringInformation
private

Definition at line 66 of file Backend.h.

◆ mCurrentAssignment

template<typename Settings >
carl::Assignment<cadcells::RAN> smtrat::Backend< Settings >::mCurrentAssignment
private

Definition at line 63 of file Backend.h.

◆ mDerivationToConstraint

template<typename Settings >
std::map<datastructures::SampledDerivationRef<PropSet>, std::vector<cadcells::Constraint> > smtrat::Backend< Settings >::mDerivationToConstraint
private

Definition at line 69 of file Backend.h.

◆ mKnownConstraints

template<typename Settings >
std::vector<boost::container::flat_set<cadcells::Constraint> > smtrat::Backend< Settings >::mKnownConstraints
private

Definition at line 54 of file Backend.h.

◆ mPool

template<typename Settings >
std::shared_ptr<datastructures::PolyPool> smtrat::Backend< Settings >::mPool
private

Definition at line 57 of file Backend.h.

◆ mProjections

template<typename Settings >
std::shared_ptr<datastructures::Projections> smtrat::Backend< Settings >::mProjections
private

Definition at line 60 of file Backend.h.

◆ mUnknownConstraints

template<typename Settings >
std::vector<boost::container::flat_set<cadcells::Constraint> > smtrat::Backend< Settings >::mUnknownConstraints
private

Definition at line 51 of file Backend.h.

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