Skip to content
Snippets Groups Projects
Commit cb707b87 authored by Petr Rockai's avatar Petr Rockai
Browse files

MC: Extract the task queue type from the final machine stack.

parent dea2fa3a
No related branches found
No related tags found
No related merge requests found
...@@ -491,9 +491,19 @@ namespace divine::mc ...@@ -491,9 +491,19 @@ namespace divine::mc
struct TMachine : machine::tree< smt::NoSolver > {}; struct TMachine : machine::tree< smt::NoSolver > {};
struct GMachine : machine::graph< smt::NoSolver > {}; struct GMachine : machine::graph< smt::NoSolver > {};
template< typename M >
struct TQ : M::tq {};
template< typename M >
struct MW
{
struct TQ : M::tq {};
struct W : Weaver< TQ > {};
};
template< typename M > template< typename M >
auto weave( M &machine ) auto weave( M &machine )
{ {
return mc::Weaver< typename M::tq >().extend_ref( machine ); return typename MW< M >::W().extend_ref( machine );
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment