cprover
graphml.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Read/write graphs as GraphML
4 
5 Author: Michael Tautschnig, mt@eecs.qmul.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_XMLLANG_GRAPHML_H
13 #define CPROVER_XMLLANG_GRAPHML_H
14 
15 #include <iosfwd>
16 #include <string>
17 
18 #include <util/irep.h>
19 #include <util/graph.h>
20 #include <util/xml.h>
21 
22 struct xml_edget
23 {
25 };
26 
27 struct xml_graph_nodet:public graph_nodet<xml_edget>
28 {
31 
32  std::string node_name;
35  unsigned thread_nr;
38  std::string invariant;
39  std::string invariant_scope;
40 };
41 
42 class graphmlt:public grapht<xml_graph_nodet>
43 {
44 public:
45  bool has_node(const std::string &node_name) const
46  {
47  for(const auto &n : nodes)
48  if(n.node_name==node_name)
49  return true;
50 
51  return false;
52  }
53 
54  node_indext add_node_if_not_exists(std::string node_name)
55  {
56  for(node_indext i=0; i<nodes.size(); ++i)
57  {
58  if(nodes[i].node_name==node_name)
59  return i;
60  }
61 
63  }
64 
65  typedef std::map<std::string, std::string> key_valuest;
67 };
68 
69 bool read_graphml(
70  std::istream &is,
71  graphmlt &dest,
72  graphmlt::node_indext &entry);
73 bool read_graphml(
74  const std::string &filename,
75  graphmlt &dest,
76  graphmlt::node_indext &entry);
77 
78 bool write_graphml(const graphmlt &src, std::ostream &os);
79 
80 #endif // CPROVER_XMLLANG_GRAPHML_H
A generic directed graph with a parametric node type.
Definition: graph.h:133
bool has_invariant
Definition: graphml.h:37
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:212
std::string invariant_scope
Definition: graphml.h:39
bool has_node(const std::string &node_name) const
Definition: graphml.h:45
irep_idt line
Definition: graphml.h:34
unsigned thread_nr
Definition: graphml.h:35
irep_idt file
Definition: graphml.h:33
graph_nodet< xml_edget >::edgest edgest
Definition: graphml.h:30
graph_nodet< xml_edget >::edget edget
Definition: graphml.h:29
Definition: xml.h:18
nodet::node_indext node_indext
Definition: graph.h:140
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::map< std::string, std::string > key_valuest
Definition: graphml.h:65
A Template Class for Graphs.
node_indext add_node()
Definition: graph.h:146
bool read_graphml(std::istream &is, graphmlt &dest, graphmlt::node_indext &entry)
Definition: graphml.cpp:184
node_indext add_node_if_not_exists(std::string node_name)
Definition: graphml.h:54
key_valuest key_values
Definition: graphml.h:66
std::string invariant
Definition: graphml.h:38
xmlt xml_node
Definition: graphml.h:24
bool is_violation
Definition: graphml.h:36
std::string node_name
Definition: graphml.h:32
This class represents a node in a directed graph.
Definition: graph.h:34