cprover
smt2irep.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "smt2irep.h"
10
11#include <util/message.h>
12
13#include <stack>
14
15#include "smt2_tokenizer.h"
16
18{
19public:
20 smt2irept(std::istream &_in, message_handlert &message_handler)
21 : smt2_tokenizert(_in), log(message_handler)
22 {
23 }
24
26
27protected:
29};
30
32{
33 try
34 {
35 std::stack<irept> stack;
36
37 while(true)
38 {
39 switch(next_token())
40 {
41 case END_OF_FILE:
42 if(stack.empty())
43 return {};
44 else
45 throw error("unexpected end of file");
46
47 case STRING_LITERAL:
48 case NUMERAL:
49 case SYMBOL:
50 if(stack.empty())
51 return irept(buffer); // all done!
52 else
53 stack.top().get_sub().push_back(irept(buffer));
54 break;
55
56 case OPEN: // '('
57 // produce sub-irep
58 stack.push(irept());
59 break;
60
61 case CLOSE: // ')'
62 // done with sub-irep
63 if(stack.empty())
64 throw error("unexpected ')'");
65 else
66 {
67 irept tmp = stack.top();
68 stack.pop();
69
70 if(stack.empty())
71 return tmp; // all done!
72
73 stack.top().get_sub().push_back(tmp);
74 break;
75 }
76
77 case NONE:
78 case KEYWORD:
79 throw error("unexpected token");
80 }
81 }
82 }
83 catch(const smt2_errort &e)
84 {
86 log.error() << e.what() << messaget::eom;
87 return {};
88 }
89}
90
91optionalt<irept> smt2irep(std::istream &in, message_handlert &message_handler)
92{
93 return smt2irept(in, message_handler)();
94}
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
subt & get_sub()
Definition: irep.h:456
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
std::string what() const override
A human readable description of what went wrong.
unsigned get_line_no() const
smt2_errort error() const
generate an error exception
std::string buffer
messaget log
Definition: smt2irep.cpp:28
optionalt< irept > operator()()
Definition: smt2irep.cpp:31
smt2irept(std::istream &_in, message_handlert &message_handler)
Definition: smt2irep.cpp:20
void set_line(const irep_idt &line)
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< irept > smt2irep(std::istream &in, message_handlert &message_handler)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
Definition: smt2irep.cpp:91