CBMC
lispirep.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "lispirep.h"
11 
12 #include "irep.h"
13 #include "lispexpr.h"
14 
15 void lisp2irep(const lispexprt &src, irept &dest)
16 {
17  dest.make_nil();
18 
19  if(src.type!=lispexprt::List || src.empty())
20  return;
21 
22  dest.id(src[0].value);
23 
24  for(std::size_t i=1; i<src.size(); i++)
25  if(!src[i].is_nil())
26  {
27  const std::string &name=src[i].value;
28  i++;
29 
30  if(i<src.size())
31  {
32  irept sub;
33  lisp2irep(src[i], sub);
34 
35  if(name.empty())
36  dest.move_to_sub(sub);
37  else
38  dest.move_to_named_sub(name, sub);
39  }
40  }
41 }
42 
43 void irep2lisp(const irept &src, lispexprt &dest)
44 {
45  dest.clear();
46  dest.value.clear();
47  dest.type=lispexprt::List;
48 
49  const std::size_t named_sub_size = src.get_named_sub().size();
50  dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size);
51 
52  lispexprt id;
54  id.value=src.id_string();
55  dest.push_back(id);
56 
57  // reserve objects for extra performance
58 
59  for(const auto &irep : src.get_sub())
60  {
61  lispexprt name;
63  name.value.clear();
64  dest.push_back(name);
65 
66  lispexprt sub;
67 
68  irep2lisp(irep, sub);
69  dest.push_back(sub);
70  }
71 
72  for(const auto &irep_entry : src.get_named_sub())
73  {
74  lispexprt name;
76  name.value = id2string(irep_entry.first);
77  dest.push_back(name);
78 
79  lispexprt sub;
80 
81  irep2lisp(irep_entry.second, sub);
82  dest.push_back(sub);
83  }
84 
85  lispexprt nil;
87  nil.value="nil";
88 
89  dest.push_back(nil);
90 }
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
subt & get_sub()
Definition: irep.h:448
void move_to_named_sub(const irep_idt &name, irept &irep)
Definition: irep.cpp:26
named_subt & get_named_sub()
Definition: irep.h:450
const std::string & id_string() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:388
void make_nil()
Definition: irep.h:446
void move_to_sub(irept &irep)
Definition: irep.cpp:35
@ String
Definition: lispexpr.h:76
@ Symbol
Definition: lispexpr.h:76
lispsymbolt value
Definition: lispexpr.h:77
enum lispexprt::@7 type
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void lisp2irep(const lispexprt &src, irept &dest)
Definition: lispirep.cpp:15
void irep2lisp(const irept &src, lispexprt &dest)
Definition: lispirep.cpp:43