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

#include <LiftingTree.h>

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

Public Types

using Tree = carl::tree< Sample >
 
using Iterator = Tree::iterator
 
using FSC = FullSampleComparator< Iterator, Settings::fullSampleComparator >
 
using SC = SampleComparator< Iterator, Settings::sampleComparator >
 
using Constraints = CADConstraints< Settings::backtracking >
 

Public Member Functions

 LiftingTree (const Constraints &c)
 
 LiftingTree (const LiftingTree &)=delete
 
 LiftingTree (LiftingTree &&)=delete
 
LiftingTree & operator= (const LiftingTree &)=delete
 
LiftingTree & operator= (LiftingTree &&)=delete
 
const auto & getTree () const
 
const auto & getLiftingQueue () const
 
void reset (std::vector< carl::Variable > &&vars)
 
bool hasFullSamples () const
 
Iterator getNextFullSample ()
 
void resetFullSamples ()
 
bool hasNextSample () const
 
Iterator getNextSample ()
 
void removeNextSample ()
 
void restoreRemovedSamples ()
 
bool liftSample (Iterator sample, const UPoly &p, std::size_t pid, bool ignore_nullifications)
 
bool addTrivialSample (Iterator sample)
 
Assignment extractSampleMap (Iterator it) const
 
void removedPolynomialsFromLevel (std::size_t level, const carl::Bitset &mask)
 
void removedConstraint (const carl::Bitset &mask)
 
bool is_consistent () const
 
std::string printSample (Iterator sample) const
 
std::string printFullSamples () const
 

Private Member Functions

std::size_t dim () const
 
void addToQueue (Iterator it)
 
void cleanQueuesFromExpired ()
 
bool insertRootSamples (Iterator parent, std::vector< Sample > &samples)
 
bool mergeRootSamples (Iterator parent, std::vector< Sample > &samples)
 

Private Attributes

const Constraints & mConstraints
 
std::vector< carl::Variable > mVariables
 
Tree mTree
 
SampleIteratorQueue< Iterator, FSC > mCheckingQueue
 
SampleIteratorQueue< Iterator, SC > mLiftingQueue
 
std::vector< Iterator > mRemovedFromLiftingQueue
 

Detailed Description

template<typename Settings>
class smtrat::cad::LiftingTree< Settings >

Definition at line 16 of file LiftingTree.h.

Member Typedef Documentation

◆ Constraints

template<typename Settings >
using smtrat::cad::LiftingTree< Settings >::Constraints = CADConstraints<Settings::backtracking>

Definition at line 22 of file LiftingTree.h.

◆ FSC

template<typename Settings >
using smtrat::cad::LiftingTree< Settings >::FSC = FullSampleComparator<Iterator,Settings::fullSampleComparator>

Definition at line 20 of file LiftingTree.h.

◆ Iterator

template<typename Settings >
using smtrat::cad::LiftingTree< Settings >::Iterator = Tree::iterator

Definition at line 19 of file LiftingTree.h.

◆ SC

template<typename Settings >
using smtrat::cad::LiftingTree< Settings >::SC = SampleComparator<Iterator,Settings::sampleComparator>

Definition at line 21 of file LiftingTree.h.

◆ Tree

template<typename Settings >
using smtrat::cad::LiftingTree< Settings >::Tree = carl::tree<Sample>

Definition at line 18 of file LiftingTree.h.

Constructor & Destructor Documentation

◆ LiftingTree() [1/3]

template<typename Settings >
smtrat::cad::LiftingTree< Settings >::LiftingTree ( const Constraints &  c)
inline

Definition at line 123 of file LiftingTree.h.

◆ LiftingTree() [2/3]

template<typename Settings >
smtrat::cad::LiftingTree< Settings >::LiftingTree ( const LiftingTree< Settings > &  )
delete

◆ LiftingTree() [3/3]

template<typename Settings >
smtrat::cad::LiftingTree< Settings >::LiftingTree ( LiftingTree< Settings > &&  )
delete

Member Function Documentation

◆ addToQueue()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::addToQueue ( Iterator  it)
inlineprivate

Definition at line 35 of file LiftingTree.h.

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

◆ addTrivialSample()

template<typename Settings >
bool smtrat::cad::LiftingTree< Settings >::addTrivialSample ( Iterator  sample)
inline

Definition at line 204 of file LiftingTree.h.

Here is the call graph for this function:

◆ cleanQueuesFromExpired()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::cleanQueuesFromExpired ( )
inlineprivate

Definition at line 44 of file LiftingTree.h.

Here is the caller graph for this function:

◆ dim()

template<typename Settings >
std::size_t smtrat::cad::LiftingTree< Settings >::dim ( ) const
inlineprivate

Definition at line 31 of file LiftingTree.h.

Here is the caller graph for this function:

◆ extractSampleMap()

template<typename Settings >
Assignment smtrat::cad::LiftingTree< Settings >::extractSampleMap ( Iterator  it) const
inline

Definition at line 222 of file LiftingTree.h.

Here is the caller graph for this function:

◆ getLiftingQueue()

template<typename Settings >
const auto& smtrat::cad::LiftingTree< Settings >::getLiftingQueue ( ) const
inline

Definition at line 132 of file LiftingTree.h.

◆ getNextFullSample()

template<typename Settings >
Iterator smtrat::cad::LiftingTree< Settings >::getNextFullSample ( )
inline

Definition at line 149 of file LiftingTree.h.

◆ getNextSample()

template<typename Settings >
Iterator smtrat::cad::LiftingTree< Settings >::getNextSample ( )
inline

Definition at line 164 of file LiftingTree.h.

◆ getTree()

template<typename Settings >
const auto& smtrat::cad::LiftingTree< Settings >::getTree ( ) const
inline

Definition at line 129 of file LiftingTree.h.

◆ hasFullSamples()

template<typename Settings >
bool smtrat::cad::LiftingTree< Settings >::hasFullSamples ( ) const
inline

Definition at line 146 of file LiftingTree.h.

◆ hasNextSample()

template<typename Settings >
bool smtrat::cad::LiftingTree< Settings >::hasNextSample ( ) const
inline

Definition at line 161 of file LiftingTree.h.

Here is the caller graph for this function:

◆ insertRootSamples()

template<typename Settings >
bool smtrat::cad::LiftingTree< Settings >::insertRootSamples ( Iterator  parent,
std::vector< Sample > &  samples 
)
inlineprivate

Definition at line 52 of file LiftingTree.h.

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

◆ is_consistent()

template<typename Settings >
bool smtrat::cad::LiftingTree< Settings >::is_consistent ( ) const
inline

Definition at line 265 of file LiftingTree.h.

Here is the caller graph for this function:

◆ liftSample()

template<typename Settings >
bool smtrat::cad::LiftingTree< Settings >::liftSample ( Iterator  sample,
const UPoly &  p,
std::size_t  pid,
bool  ignore_nullifications 
)
inline

Definition at line 177 of file LiftingTree.h.

Here is the call graph for this function:

◆ mergeRootSamples()

template<typename Settings >
bool smtrat::cad::LiftingTree< Settings >::mergeRootSamples ( Iterator  parent,
std::vector< Sample > &  samples 
)
inlineprivate

Definition at line 82 of file LiftingTree.h.

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

◆ operator=() [1/2]

template<typename Settings >
LiftingTree& smtrat::cad::LiftingTree< Settings >::operator= ( const LiftingTree< Settings > &  )
delete

◆ operator=() [2/2]

template<typename Settings >
LiftingTree& smtrat::cad::LiftingTree< Settings >::operator= ( LiftingTree< Settings > &&  )
delete

◆ printFullSamples()

template<typename Settings >
std::string smtrat::cad::LiftingTree< Settings >::printFullSamples ( ) const
inline

Definition at line 280 of file LiftingTree.h.

Here is the call graph for this function:

◆ printSample()

template<typename Settings >
std::string smtrat::cad::LiftingTree< Settings >::printSample ( Iterator  sample) const
inline

Definition at line 271 of file LiftingTree.h.

Here is the caller graph for this function:

◆ removedConstraint()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::removedConstraint ( const carl::Bitset &  mask)
inline

Definition at line 256 of file LiftingTree.h.

◆ removedPolynomialsFromLevel()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::removedPolynomialsFromLevel ( std::size_t  level,
const carl::Bitset &  mask 
)
inline

Definition at line 235 of file LiftingTree.h.

Here is the call graph for this function:

◆ removeNextSample()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::removeNextSample ( )
inline

Definition at line 168 of file LiftingTree.h.

Here is the call graph for this function:

◆ reset()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::reset ( std::vector< carl::Variable > &&  vars)
inline

Definition at line 135 of file LiftingTree.h.

Here is the call graph for this function:

◆ resetFullSamples()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::resetFullSamples ( )
inline

Definition at line 152 of file LiftingTree.h.

Here is the call graph for this function:

◆ restoreRemovedSamples()

template<typename Settings >
void smtrat::cad::LiftingTree< Settings >::restoreRemovedSamples ( )
inline

Definition at line 172 of file LiftingTree.h.

Field Documentation

◆ mCheckingQueue

template<typename Settings >
SampleIteratorQueue<Iterator, FSC> smtrat::cad::LiftingTree< Settings >::mCheckingQueue
private

Definition at line 27 of file LiftingTree.h.

◆ mConstraints

template<typename Settings >
const Constraints& smtrat::cad::LiftingTree< Settings >::mConstraints
private

Definition at line 24 of file LiftingTree.h.

◆ mLiftingQueue

template<typename Settings >
SampleIteratorQueue<Iterator, SC> smtrat::cad::LiftingTree< Settings >::mLiftingQueue
private

Definition at line 28 of file LiftingTree.h.

◆ mRemovedFromLiftingQueue

template<typename Settings >
std::vector<Iterator> smtrat::cad::LiftingTree< Settings >::mRemovedFromLiftingQueue
private

Definition at line 29 of file LiftingTree.h.

◆ mTree

template<typename Settings >
Tree smtrat::cad::LiftingTree< Settings >::mTree
private

Definition at line 26 of file LiftingTree.h.

◆ mVariables

template<typename Settings >
std::vector<carl::Variable> smtrat::cad::LiftingTree< Settings >::mVariables
private

Definition at line 25 of file LiftingTree.h.

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