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

This explanation executes all given explanation in parallel processes and waits for the fastest explanation, returning the fastest delivered explanation, terminating all other parallel processes. More...

#include <FastParallelExplanation.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>
void	explain (const mcsat::Bookkeeping &, carl::Variable, const FormulasT &, std::vector< pid_t > &pids) const
template<std::size_t N = 0>
	push_back (std::nullopt)
	explain (data, var, reason, pids)
	SMTRAT_LOG_DEBUG ("smtrat.mcsat.explanation", "Start looking for explanation")
	while (true)

Private Attributes
B	mBackends

Detailed Description

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

This explanation executes all given explanation in parallel processes and waits for the fastest explanation, returning the fastest delivered explanation, terminating all other parallel processes.

Definition at line 25 of file FastParallelExplanation.h.

Member Typedef Documentation

B

template<typename... Backends>

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

private

Definition at line 27 of file FastParallelExplanation.h.

Member Function Documentation

explain() [1/2]

template<typename... Backends>

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

void smtrat::mcsat::FastParallelExplanation< Backends >::explain ( const mcsat::Bookkeeping &  , carl::Variable  , const FormulasT &  , std::vector< pid_t > &  pids  ) const

inlineprivate

Definition at line 31 of file FastParallelExplanation.h.

explain() [2/2]

template<typename... Backends>

smtrat::mcsat::FastParallelExplanation< Backends >::explain ( data  , var  , reason  , pids    )

private

push_back()

template<typename... Backends>

template<std::size_t N = 0>

smtrat::mcsat::FastParallelExplanation< Backends >::push_back ( std::nullopt  )

private

SMTRAT_LOG_DEBUG()

template<typename... Backends>

smtrat::mcsat::FastParallelExplanation< Backends >::SMTRAT_LOG_DEBUG ( "smtrat.mcsat.explanation"  , "Start looking for explanation"    )

private

while()

template<typename... Backends>

smtrat::mcsat::FastParallelExplanation< Backends >::while ( true  )

inlineprivate

Definition at line 85 of file FastParallelExplanation.h.

Field Documentation

mBackends

template<typename... Backends>

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

private

Definition at line 28 of file FastParallelExplanation.h.

---

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

• smtrat-mcsat/explanations/FastParallelExplanation.h