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