cprover
Loading...
Searching...
No Matches
lispirep.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#include "lispirep.h"
11
12#include "irep.h"
13#include "lispexpr.h"
14
15void 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
43void irep2lisp(const irept &src, lispexprt &dest)
44{
45 dest.clear();
46 dest.value.clear();
48
49#if NAMED_SUB_IS_FORWARD_LIST
50 const std::size_t named_sub_size =
51 std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
52#else
53 const std::size_t named_sub_size = src.get_named_sub().size();
54#endif
55 dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size);
56
57 lispexprt id;
59 id.value=src.id_string();
60 dest.push_back(id);
61
62 // reserve objects for extra performance
63
64 for(const auto &irep : src.get_sub())
65 {
66 lispexprt name;
68 name.value.clear();
69 dest.push_back(name);
70
71 lispexprt sub;
72
73 irep2lisp(irep, sub);
74 dest.push_back(sub);
75 }
76
77 for(const auto &irep_entry : src.get_named_sub())
78 {
79 lispexprt name;
81 name.value = id2string(irep_entry.first);
82 dest.push_back(name);
83
84 lispexprt sub;
85
86 irep2lisp(irep_entry.second, sub);
87 dest.push_back(sub);
88 }
89
90 lispexprt nil;
92 nil.value="nil";
93
94 dest.push_back(nil);
95}
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
const std::string & id_string() const
Definition irep.h:399
subt & get_sub()
Definition irep.h:456
named_subt & get_named_sub()
Definition irep.h:458
lispsymbolt value
Definition lispexpr.h:77
enum lispexprt::@7 type
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void lisp2irep(const lispexprt &src, irept &dest)
Definition lispirep.cpp:15
void irep2lisp(const irept &src, lispexprt &dest)
Definition lispirep.cpp:43