mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-06-14 08:10:21 -07:00
parent 9253ca9d86 c8c262fb93
commit 8da0146318
2 changed files with 16 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/parsers/smt2/smt2scanner.cpp
View file

@ -23,10 +23,12 @@ namespace smt2 {
void scanner::next() { void scanner::next() {
if (m_cache_input) if (m_cache_input)
m_cache.push_back(m_curr); m_cache.push_back(m_curr);
SASSERT(m_curr != EOF); SASSERT(!m_at_eof);
if (m_interactive) { if (m_interactive) {
m_curr = m_stream.get(); m_curr = m_stream.get();
if (m_stream.eof())
m_at_eof = true;
} }
else if (m_bpos < m_bend) { else if (m_bpos < m_bend) {
m_curr = m_buffer[m_bpos]; m_curr = m_buffer[m_bpos];
@ -37,7 +39,7 @@ namespace smt2 {
m_bend = static_cast<unsigned>(m_stream.gcount()); m_bend = static_cast<unsigned>(m_stream.gcount());
m_bpos = 0; m_bpos = 0;
if (m_bpos == m_bend) { if (m_bpos == m_bend) {
m_curr = EOF; m_at_eof = true;
} }
else { else {
m_curr = m_buffer[m_bpos]; m_curr = m_buffer[m_bpos];
@ -52,7 +54,7 @@ namespace smt2 {
next(); next();
while (true) { while (true) {
char c = curr(); char c = curr();
if (c == EOF) if (m_at_eof)
return; return;
if (c == '\n') { if (c == '\n') {
new_line(); new_line();
@ -70,7 +72,7 @@ namespace smt2 {
next(); next();
while (true) { while (true) {
char c = curr(); char c = curr();
if (c == EOF) { if (m_at_eof) {
throw scanner_exception("unexpected end of quoted symbol", m_line, m_spos); throw scanner_exception("unexpected end of quoted symbol", m_line, m_spos);
} }
else if (c == '\n') { else if (c == '\n') {
@ -167,7 +169,7 @@ namespace smt2 {
m_string.reset(); m_string.reset();
while (true) { while (true) {
char c = curr(); char c = curr();
if (c == EOF) if (m_at_eof)
throw scanner_exception("unexpected end of string", m_line, m_spos); throw scanner_exception("unexpected end of string", m_line, m_spos);
if (c == '\n') { if (c == '\n') {
new_line(); new_line();
@ -237,10 +239,11 @@ namespace smt2 {
} }
} }
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive): scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive) :
m_interactive(interactive), m_interactive(interactive),
m_spos(0), m_spos(0),
m_curr(0), // avoid Valgrind warning m_curr(0), // avoid Valgrind warning
m_at_eof(false),
m_line(1), m_line(1),
m_pos(0), m_pos(0),
m_bv_size(UINT_MAX), m_bv_size(UINT_MAX),
@ -289,9 +292,13 @@ namespace smt2 {
} }
scanner::token scanner::scan() { scanner::token scanner::scan() {
while (true) { while (true) {
signed char c = curr(); signed char c = curr();
m_pos = m_spos; m_pos = m_spos;
if (m_at_eof)
return EOF_TOKEN;
switch (m_normalized[(unsigned char) c]) { switch (m_normalized[(unsigned char) c]) {
case ' ': case ' ':
next(); next();
@ -327,8 +334,6 @@ namespace smt2 {
return read_symbol(); return read_symbol();
else else
return read_signed_number(); return read_signed_number();
case -1:
return EOF_TOKEN;
default: { default: {
scanner_exception ex("unexpected character", m_line, m_spos); scanner_exception ex("unexpected character", m_line, m_spos);
next(); next();

1
src/parsers/smt2/smt2scanner.h
View file

@ -34,6 +34,7 @@ namespace smt2 {
bool m_interactive; bool m_interactive;
int m_spos; // position in the current line of the stream int m_spos; // position in the current line of the stream
char m_curr; // current char; char m_curr; // current char;
bool m_at_eof;
int m_line; // line int m_line; // line
int m_pos; // start position of the token int m_pos; // start position of the token