cprover
smt2irep.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "smt2irep.h"
10 
11 #include <cassert>
12 #include <stack>
13 
14 #include "smt2_tokenizer.h"
15 
17 {
18 public:
19  explicit smt2irept(std::istream &_in):smt2_tokenizert(_in)
20  {
21  }
22 
23  inline irept operator()()
24  {
25  parse();
26  return result;
27  }
28 
29  bool parse() override;
30 
31 protected:
33 };
34 
36 {
37  std::stack<irept> stack;
38  result.clear();
39 
40  while(true)
41  {
42  switch(next_token())
43  {
44  case END_OF_FILE:
45  error() << "unexpected end of file" << eom;
46  return true;
47 
48  case STRING_LITERAL:
49  case NUMERAL:
50  case SYMBOL:
51  if(stack.empty())
52  {
54  return false; // all done!
55  }
56  else
57  stack.top().get_sub().push_back(irept(buffer));
58  break;
59 
60  case OPEN: // '('
61  // produce sub-irep
62  stack.push(irept());
63  break;
64 
65  case CLOSE: // ')'
66  // done with sub-irep
67  if(stack.empty())
68  {
69  error() << "unexpected ')'" << eom;
70  return true;
71  }
72  else
73  {
74  irept tmp=stack.top();
75  stack.pop();
76 
77  if(stack.empty())
78  {
79  result=tmp;
80  return false; // all done!
81  }
82 
83  stack.top().get_sub().push_back(tmp);
84  break;
85  }
86 
87  default:
88  return true;
89  }
90  }
91 }
92 
93 irept smt2irep(std::istream &in)
94 {
95  return smt2irept(in)();
96 }
irept smt2irep(std::istream &in)
Definition: smt2irep.cpp:93
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
smt2irept(std::istream &_in)
Definition: smt2irep.cpp:19
bool parse() override
Definition: smt2irep.cpp:35
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std::vector< exprt > stack
Definition: parser.h:30
#define STRING_LITERAL
mstreamt & result() const
Definition: message.h:312
std::string buffer
#define CLOSE
Definition: xml_y.tab.cpp:147
irept operator()()
Definition: smt2irep.cpp:23
mstreamt & error()
irept result
Definition: smt2irep.cpp:32