CBMC
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 class message_handlert;
23 
24 struct xml_edget
25 {
27 };
28 
29 struct xml_graph_nodet:public graph_nodet<xml_edget>
30 {
33 
34  std::string node_name;
39  std::string invariant;
40  std::string invariant_scope;
41 };
42 
43 class graphmlt:public grapht<xml_graph_nodet>
44 {
45 public:
46  bool has_node(const std::string &node_name) const
47  {
48  for(const auto &n : nodes)
49  if(n.node_name==node_name)
50  return true;
51 
52  return false;
53  }
54 
55  node_indext add_node_if_not_exists(std::string node_name)
56  {
57  for(node_indext i=0; i<nodes.size(); ++i)
58  {
59  if(nodes[i].node_name==node_name)
60  return i;
61  }
62 
64  }
65 
66  typedef std::map<std::string, std::string> key_valuest;
68 };
69 
70 bool read_graphml(
71  std::istream &is,
72  graphmlt &dest,
73  graphmlt::node_indext &entry,
74  message_handlert &message_handler);
75 bool read_graphml(
76  const std::string &filename,
77  graphmlt &dest,
78  graphmlt::node_indext &entry,
79  message_handlert &message_handler);
80 
81 bool write_graphml(const graphmlt &src, std::ostream &os);
82 
83 #endif // CPROVER_XMLLANG_GRAPHML_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
This class represents a node in a directed graph.
Definition: graph.h:35
bool has_node(const std::string &node_name) const
Definition: graphml.h:46
node_indext add_node_if_not_exists(std::string node_name)
Definition: graphml.h:55
std::map< std::string, std::string > key_valuest
Definition: graphml.h:66
key_valuest key_values
Definition: graphml.h:67
A generic directed graph with a parametric node type.
Definition: graph.h:167
nodet::node_indext node_indext
Definition: graph.h:173
node_indext add_node(arguments &&... values)
Definition: graph.h:180
Definition: xml.h:21
A Template Class for Graphs.
bool read_graphml(std::istream &is, graphmlt &dest, graphmlt::node_indext &entry, message_handlert &message_handler)
Definition: graphml.cpp:175
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:203
xmlt xml_node
Definition: graphml.h:26
std::string invariant
Definition: graphml.h:39
irep_idt file
Definition: graphml.h:35
irep_idt line
Definition: graphml.h:36
bool has_invariant
Definition: graphml.h:38
std::string invariant_scope
Definition: graphml.h:40
bool is_violation
Definition: graphml.h:37
graph_nodet< xml_edget >::edgest edgest
Definition: graphml.h:32
graph_nodet< xml_edget >::edget edget
Definition: graphml.h:31
std::string node_name
Definition: graphml.h:34