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 <stack>
12 
13 #include "smt2_tokenizer.h"
14 
16 {
17 public:
18  explicit smt2irept(std::istream &_in):smt2_tokenizert(_in)
19  {
20  }
21 
22  inline irept operator()()
23  {
24  parse();
25  return result;
26  }
27 
28  bool parse() override;
29 
30 protected:
32 };
33 
35 {
36  try
37  {
38  std::stack<irept> stack;
39  result.clear();
40 
41  while(true)
42  {
43  switch(next_token())
44  {
45  case END_OF_FILE:
46  throw error("unexpected end of file");
47 
48  case STRING_LITERAL:
49  case NUMERAL:
50  case SYMBOL:
51  if(stack.empty())
52  {
53  result = irept(buffer);
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  throw error("unexpected ')'");
69  else
70  {
71  irept tmp = stack.top();
72  stack.pop();
73 
74  if(stack.empty())
75  {
76  result = tmp;
77  return false; // all done!
78  }
79 
80  stack.top().get_sub().push_back(tmp);
81  break;
82  }
83 
84  default:
85  throw error("unexpected token");
86  }
87  }
88  }
89  catch(const smt2_errort &e)
90  {
92  messaget::error() << e.what() << eom;
93  return true;
94  }
95 }
96 
97 irept smt2irep(std::istream &in)
98 {
99  return smt2irept(in)();
100 }
irept smt2irep(std::istream &in)
Definition: smt2irep.cpp:97
unsigned get_line_no() const
std::string what() const override
A human readable description of what went wrong.
smt2irept(std::istream &_in)
Definition: smt2irep.cpp:18
source_locationt source_location
Definition: message.h:236
mstreamt & error() const
Definition: message.h:386
void set_line(const irep_idt &line)
bool parse() override
Definition: smt2irep.cpp:34
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std::vector< exprt > stack
Definition: parser.h:30
#define STRING_LITERAL
static eomt eom
Definition: message.h:284
mstreamt & result() const
Definition: message.h:396
std::string buffer
#define CLOSE
Definition: xml_y.tab.cpp:147
smt2_errort error()
generate an error exception
irept operator()()
Definition: smt2irep.cpp:22
irept result
Definition: smt2irep.cpp:31
virtual tokent next_token()