CBMC
irep_serialization.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: binary irep conversions with hashing
4 
5 Author: CM Wintersteiger
6 
7 Date: May 2007
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_UTIL_IREP_SERIALIZATION_H
15 #define CPROVER_UTIL_IREP_SERIALIZATION_H
16 
17 #include <map>
18 #include <iosfwd>
19 #include <string>
20 #include <vector>
21 
22 #include "irep_hash_container.h"
23 #include "irep.h"
24 
25 void write_gb_word(std::ostream &, std::size_t);
26 void write_gb_string(std::ostream &, const std::string &);
27 
29 {
30 public:
32  {
33  public:
34  typedef std::vector<std::pair<bool, irept> > ireps_on_readt;
36 
38  typedef std::map<std::size_t, std::size_t> ireps_on_writet;
40 
41  typedef std::vector<bool> string_mapt;
43 
44  typedef std::vector<std::pair<bool, irep_idt> > string_rev_mapt;
46 
47  void clear()
48  {
50  ireps_on_write.clear();
51  ireps_on_read.clear();
52  string_map.clear();
53  string_rev_map.clear();
54  }
55  };
56 
58  ireps_container(ic)
59  {
60  read_buffer.resize(1, 0);
61  clear();
62  };
63 
64  const irept &reference_convert(std::istream &);
65  void reference_convert(const irept &irep, std::ostream &);
66 
67  irep_idt read_string_ref(std::istream &);
68  void write_string_ref(std::ostream &, const irep_idt &);
69 
70  void clear() { ireps_container.clear(); }
71 
72  static std::size_t read_gb_word(std::istream &);
73  irep_idt read_gb_string(std::istream &);
74 
75 private:
77  std::vector<char> read_buffer;
78 
79  void write_irep(std::ostream &, const irept &irep);
80  irept read_irep(std::istream &);
81 };
82 
83 #endif // CPROVER_UTIL_IREP_SERIALIZATION_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
irep_full_hash_containert irep_full_hash_container
std::map< std::size_t, std::size_t > ireps_on_writet
std::vector< std::pair< bool, irept > > ireps_on_readt
std::vector< std::pair< bool, irep_idt > > string_rev_mapt
ireps_containert & ireps_container
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.
irept read_irep(std::istream &)
static std::size_t read_gb_word(std::istream &)
Interpret a stream of byte as a 7-bit encoded unsigned number.
void write_irep(std::ostream &, const irept &irep)
irep_serializationt(ireps_containert &ic)
std::vector< char > read_buffer
const irept & reference_convert(std::istream &)
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
irep_idt read_gb_string(std::istream &)
reads a string from the stream
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
IREP Hash Container.
void write_gb_word(std::ostream &, std::size_t)
Write 7 bits of u each time, least-significant byte first, until we have zero.
void write_gb_string(std::ostream &, const std::string &)
outputs the string and then a zero byte.