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::clear
void clear()
Definition: irep.h:313
smt2irept::parse
bool parse() override
Definition: smt2irep.cpp:34
messaget::eom
static eomt eom
Definition: message.h:284
smt2_tokenizert
Definition: smt2_tokenizer.h:18
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:102
smt2irep
irept smt2irep(std::istream &in)
Definition: smt2irep.cpp:97
messaget::error
mstreamt & error() const
Definition: message.h:386
smt2_tokenizert::error
smt2_errort error()
generate an error exception
Definition: smt2_tokenizer.h:101
smt2irept::smt2irept
smt2irept(std::istream &_in)
Definition: smt2irep.cpp:18
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
smt2_tokenizer.h
CLOSE
#define CLOSE
Definition: xml_y.tab.cpp:163
smt2irept::result
irept result
Definition: smt2irep.cpp:31
parsert::stack
std::vector< exprt > stack
Definition: parser.h:30
STRING_LITERAL
#define STRING_LITERAL
Definition: ansi_c_lex.yy.cpp:4406
smt2_tokenizert::smt2_errort::get_line_no
unsigned get_line_no() const
Definition: smt2_tokenizer.h:45
smt2_tokenizert::buffer
std::string buffer
Definition: smt2_tokenizer.h:61
smt2_tokenizert::smt2_errort
Definition: smt2_tokenizer.h:27
smt2irept
Definition: smt2irep.cpp:15
smt2irept::operator()
irept operator()()
Definition: smt2irep.cpp:22
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
smt2_tokenizert::next_token
virtual tokent next_token()
Definition: smt2_tokenizer.cpp:203
smt2_tokenizert::smt2_errort::what
std::string what() const override
A human readable description of what went wrong.
Definition: smt2_tokenizer.h:40
smt2irep.h