CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
irep_serialization.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: binary irep conversions with hashing
4
5Author: CM Wintersteiger
6
7Date: 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
25void write_gb_word(std::ostream &, std::size_t);
26void write_gb_string(std::ostream &, const std::string &);
27
29{
30public:
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
55 };
56
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
71
72 static std::size_t read_gb_word(std::istream &);
73 irep_idt read_gb_string(std::istream &);
74
75private:
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
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.