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 <istream>
16 #include <ostream>
17 #include <string>
18 
19 #include <util/irep.h>
20 #include <util/graph.h>
21 #include <util/xml.h>
22 
23 struct xml_edget
24 {
26 };
27 
28 struct xml_graph_nodet:public graph_nodet<xml_edget>
29 {
32 
33  std::string node_name;
36  unsigned thread_nr;
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 bool read_graphml(
75  const std::string &filename,
76  graphmlt &dest,
77  graphmlt::node_indext &entry);
78 
79 bool write_graphml(const graphmlt &src, std::ostream &os);
80 
81 #endif // CPROVER_XMLLANG_GRAPHML_H
A generic directed graph with a parametric node type.
Definition: graph.h:132
bool has_invariant
Definition: graphml.h:38
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:212
std::string invariant_scope
Definition: graphml.h:40
bool has_node(const std::string &node_name) const
Definition: graphml.h:46
irep_idt line
Definition: graphml.h:35
unsigned thread_nr
Definition: graphml.h:36
irep_idt file
Definition: graphml.h:34
graph_nodet< xml_edget >::edgest edgest
Definition: graphml.h:31
graph_nodet< xml_edget >::edget edget
Definition: graphml.h:30
Definition: xml.h:18
nodet::node_indext node_indext
Definition: graph.h:139
std::map< std::string, std::string > key_valuest
Definition: graphml.h:66
A Template Class for Graphs.
node_indext add_node()
Definition: graph.h:145
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:55
key_valuest key_values
Definition: graphml.h:67
std::string invariant
Definition: graphml.h:39
xmlt xml_node
Definition: graphml.h:25
bool is_violation
Definition: graphml.h:37
std::string node_name
Definition: graphml.h:33
This class represents a node in a directed graph.
Definition: graph.h:33