cprover
|
#include <graph_visitor.h>
Public Member Functions | |
void | PT (const edget &e, std::set< unsigned > &edges) |
void | CT (const edget &e, std::set< unsigned > &edges) |
void | CT_not_powr (const edget &e, std::set< unsigned > &edges) |
void | IT (const edget &e, std::set< unsigned > &edges) |
void | const_graph_explore (event_grapht &graph, event_idt next, event_idt end, std::list< event_idt > &old_path) |
void | graph_explore (event_grapht &graph, event_idt next, event_idt end, std::list< event_idt > &old_path, std::set< unsigned > &edges) |
void | graph_explore_BC (event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges, bool porw) |
void | graph_explore_AC (event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges, bool porw) |
void | graph_explore_BC (event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges) |
void | graph_explore_AC (event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges) |
void | const_graph_explore_BC (event_grapht &egraph, event_idt next, std::list< event_idt > &old_path) |
void | const_graph_explore_AC (event_grapht &egraph, event_idt next, std::list< event_idt > &old_path) |
const_graph_visitort (fence_insertert &_fence_inserter) | |
Protected Types | |
typedef event_grapht::critical_cyclet::delayt | edget |
Protected Attributes | |
fence_insertert & | fence_inserter |
std::set< event_idt > | visited_nodes |
Definition at line 22 of file graph_visitor.h.
|
protected |
Definition at line 25 of file graph_visitor.h.
|
inlineexplicit |
Definition at line 70 of file graph_visitor.h.
void const_graph_visitort::const_graph_explore | ( | event_grapht & | graph, |
event_idt | next, | ||
event_idt | end, | ||
std::list< event_idt > & | old_path | ||
) |
Definition at line 61 of file graph_visitor.cpp.
References fence_insertert::add_edge(), fence_inserter, event_grapht::has_po_edge(), event_grapht::po_out(), and visited_nodes.
Referenced by cycles_visitort::po_edges().
void const_graph_visitort::const_graph_explore_AC | ( | event_grapht & | egraph, |
event_idt | next, | ||
std::list< event_idt > & | old_path | ||
) |
Definition at line 279 of file graph_visitor.cpp.
References fence_insertert::add_edge(), fence_inserter, abstract_eventt::operation, event_grapht::po_in(), abstract_eventt::Read, visited_nodes, and abstract_eventt::Write.
Referenced by cycles_visitort::po_edges().
void const_graph_visitort::const_graph_explore_BC | ( | event_grapht & | egraph, |
event_idt | next, | ||
std::list< event_idt > & | old_path | ||
) |
Definition at line 164 of file graph_visitor.cpp.
References fence_insertert::add_edge(), fence_inserter, abstract_eventt::operation, event_grapht::po_out(), abstract_eventt::Read, visited_nodes, and abstract_eventt::Write.
Referenced by cycles_visitort::po_edges().
void const_graph_visitort::CT | ( | const edget & | edge, |
std::set< unsigned > & | edges | ||
) |
Definition at line 379 of file graph_visitor.cpp.
References instrumentert::egraph, fence_inserter, event_grapht::critical_cyclet::delayt::first, graph_explore_AC(), graph_explore_BC(), fence_insertert::instrumenter, abstract_eventt::operation, event_grapht::po_in(), event_grapht::po_out(), abstract_eventt::Read, event_grapht::critical_cyclet::delayt::second, visited_nodes, and abstract_eventt::Write.
Referenced by fence_insertert::mip_fill_matrix(), and fence_insertert::preprocess().
void const_graph_visitort::CT_not_powr | ( | const edget & | edge, |
std::set< unsigned > & | edges | ||
) |
Definition at line 434 of file graph_visitor.cpp.
References instrumentert::egraph, fence_inserter, event_grapht::critical_cyclet::delayt::first, graph_explore_AC(), graph_explore_BC(), fence_insertert::instrumenter, abstract_eventt::operation, event_grapht::po_in(), event_grapht::po_out(), abstract_eventt::Read, event_grapht::critical_cyclet::delayt::second, visited_nodes, and abstract_eventt::Write.
Referenced by fence_insertert::mip_fill_matrix(), and fence_insertert::preprocess().
void const_graph_visitort::graph_explore | ( | event_grapht & | graph, |
event_idt | next, | ||
event_idt | end, | ||
std::list< event_idt > & | old_path, | ||
std::set< unsigned > & | edges | ||
) |
Definition at line 19 of file graph_visitor.cpp.
References fence_insertert::add_edge(), fence_inserter, event_grapht::has_po_edge(), event_grapht::po_out(), and visited_nodes.
Referenced by PT().
void const_graph_visitort::graph_explore_AC | ( | event_grapht & | egraph, |
event_idt | next, | ||
std::list< event_idt > & | old_path, | ||
std::set< unsigned > & | edges, | ||
bool | porw | ||
) |
Definition at line 219 of file graph_visitor.cpp.
References fence_insertert::add_edge(), messaget::debug(), messaget::eom(), fence_inserter, fence_insertert::instrumenter, instrumentert::message, abstract_eventt::operation, event_grapht::po_in(), abstract_eventt::Read, visited_nodes, and abstract_eventt::Write.
Referenced by CT(), CT_not_powr(), and graph_explore_AC().
|
inline |
Definition at line 56 of file graph_visitor.h.
References graph_explore_AC().
void const_graph_visitort::graph_explore_BC | ( | event_grapht & | egraph, |
event_idt | next, | ||
std::list< event_idt > & | old_path, | ||
std::set< unsigned > & | edges, | ||
bool | porw | ||
) |
Definition at line 102 of file graph_visitor.cpp.
References fence_insertert::add_edge(), messaget::debug(), messaget::eom(), fence_inserter, fence_insertert::instrumenter, instrumentert::message, abstract_eventt::operation, event_grapht::po_out(), abstract_eventt::Read, visited_nodes, and abstract_eventt::Write.
Referenced by CT(), CT_not_powr(), and graph_explore_BC().
|
inline |
Definition at line 48 of file graph_visitor.h.
References graph_explore_BC().
void const_graph_visitort::IT | ( | const edget & | e, |
std::set< unsigned > & | edges | ||
) |
void const_graph_visitort::PT | ( | const edget & | e, |
std::set< unsigned > & | edges | ||
) |
all the pos in between
Definition at line 335 of file graph_visitor.cpp.
References instrumentert::egraph, fence_inserter, event_grapht::critical_cyclet::delayt::first, graph_explore(), fence_insertert::instrumenter, fence_insertert::map_from_e, event_grapht::po_out(), event_grapht::critical_cyclet::delayt::second, and visited_nodes.
Referenced by fence_insertert::mip_fill_matrix(), and fence_insertert::preprocess().
|
protected |
Definition at line 27 of file graph_visitor.h.
Referenced by const_graph_explore(), const_graph_explore_AC(), const_graph_explore_BC(), CT(), CT_not_powr(), graph_explore(), graph_explore_AC(), graph_explore_BC(), and PT().
|
protected |
Definition at line 28 of file graph_visitor.h.
Referenced by const_graph_explore(), const_graph_explore_AC(), const_graph_explore_BC(), CT(), CT_not_powr(), graph_explore(), graph_explore_AC(), graph_explore_BC(), and PT().