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_parser.h"
15 
16 class smt2irept:public smt2_parsert
17 {
18 public:
19  explicit smt2irept(std::istream &_in):smt2_parsert(_in)
20  {
21  }
22 
23  inline irept operator()()
24  {
26  return result;
27  }
28 
29 protected:
31  std::stack<irept> stack;
32 
33  // overload from smt2_parsert
34 
35  virtual void symbol()
36  {
37  if(stack.empty())
38  result=irept(buffer);
39  else
40  stack.top().get_sub().push_back(irept(buffer));
41  }
42 
43  virtual void string_literal()
44  {
45  symbol(); // we don't distinguish
46  }
47 
48  virtual void numeral()
49  {
50  symbol(); // we don't distinguish
51  }
52 
53  // '('
54  virtual void open_expression()
55  {
56  // produce sub-irep
57  stack.push(irept());
58  }
59 
60  // ')'
61  virtual void close_expression()
62  {
63  // done with sub-irep
64  assert(!stack.empty()); // unexpected )
65 
66  irept tmp=stack.top();
67  stack.pop();
68 
69  if(stack.empty())
70  result=tmp;
71  else
72  stack.top().get_sub().push_back(tmp);
73  }
74 
75  virtual void keyword()
76  {
77  // ignore
78  }
79 
80  virtual void error(const std::string &message)
81  {
82  }
83 };
84 
85 irept smt2irep(std::istream &in)
86 {
87  return smt2irept(in)();
88 }
irept smt2irep(std::istream &in)
Definition: smt2irep.cpp:85
virtual void error(const std::string &message)
Definition: smt2irep.cpp:80
virtual void close_expression()
Definition: smt2irep.cpp:61
std::stack< irept > stack
Definition: smt2irep.cpp:31
std::istream & in
Definition: smt2_parser.h:26
std::string buffer
Definition: smt2_parser.h:27
virtual void open_expression()
Definition: smt2irep.cpp:54
virtual void keyword()
Definition: smt2irep.cpp:75
smt2irept(std::istream &_in)
Definition: smt2irep.cpp:19
virtual void string_literal()
Definition: smt2irep.cpp:43
Base class for tree-like data structures with sharing.
Definition: irep.h:87
void operator()()
irept operator()()
Definition: smt2irep.cpp:23
irept result
Definition: smt2irep.cpp:30
virtual void symbol()
Definition: smt2irep.cpp:35
virtual void numeral()
Definition: smt2irep.cpp:48