smtrat::mcsat::FullParallelExplanation< Backends > Struct Template Reference

This explanation executes all given explanation parallel in multiple threads and waits until every single one has finished, returning the result of the first listed explanation. More...

#include <FullParallelExplanation.h>

Private Types
using	B = std::tuple< Backends... >

Private Member Functions
template<std::size_t N = 0, carl::EnableIfBool< N==std::tuple_size< B >::value > = carl::dummy>
std::optional< Explanation >	explain (const mcsat::Bookkeeping &, carl::Variable, const FormulasT &, const std::size_t NUM_THREADS, std::mutex &mtx, std::vector< std::thread > &threads, std::vector< pthread_t > &nativeHandles, size_t &counter, std::vector< std::optional< Explanation >> &explanations) const

Private Attributes
B	mBackends

Detailed Description

template<typename... Backends>
struct smtrat::mcsat::FullParallelExplanation< Backends >

This explanation executes all given explanation parallel in multiple threads and waits until every single one has finished, returning the result of the first listed explanation.

Definition at line 19 of file FullParallelExplanation.h.

Member Typedef Documentation

B

template<typename... Backends>

using smtrat::mcsat::FullParallelExplanation< Backends >::B = std::tuple<Backends...>

private

Definition at line 21 of file FullParallelExplanation.h.

Member Function Documentation

explain()

template<typename... Backends>

template<std::size_t N = 0, carl::EnableIfBool< N==std::tuple_size< B >::value > = carl::dummy>

std::optional<Explanation> smtrat::mcsat::FullParallelExplanation< Backends >::explain ( const mcsat::Bookkeeping &  , carl::Variable  , const FormulasT &  , const std::size_t  NUM_THREADS, std::mutex &  mtx, std::vector< std::thread > &  threads, std::vector< pthread_t > &  nativeHandles, size_t &  counter, std::vector< std::optional< Explanation >> &  explanations  ) const

inlineprivate

Definition at line 25 of file FullParallelExplanation.h.

Field Documentation

mBackends

template<typename... Backends>

B smtrat::mcsat::FullParallelExplanation< Backends >::mBackends

private

Definition at line 22 of file FullParallelExplanation.h.

---

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

• smtrat-mcsat/explanations/FullParallelExplanation.h