mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

add multiline lisp style comments #1932

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-12 08:52:51 -08:00
parent 72400f1869
commit 8847898a7d
2 changed files with 30 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -64,6 +64,26 @@ namespace smt2 {
next();
}
}
void scanner::read_multiline_comment() {
SASSERT(curr() == '|');
next();
while (true) {
char c = curr();
if (m_at_eof)
return;
if (c == '\n') {
new_line();
next();
continue;
}
next();
if (c == '|' && curr() == '#') {
next();
return;
}
}
}
scanner::token scanner::read_quoted_symbol() {
SASSERT(curr() == '|');
@ -235,6 +255,10 @@ namespace smt2 {
throw scanner_exception("invalid empty bit-vector literal", m_line, m_spos);
return BV_TOKEN;
}
else if ('|') {
read_multiline_comment();
return NULL_TOKEN;
}
else {
throw scanner_exception("invalid bit-vector literal, expecting 'x' or 'b'", m_line, m_spos);
}
@ -295,6 +319,8 @@ namespace smt2 {
scanner::token scanner::scan() {
while (true) {
signed char c = curr();
token t;
m_pos = m_spos;
if (m_at_eof)
@ -329,7 +355,9 @@ namespace smt2 {
case '0':
return read_number();
case '#':
return read_bv_literal();
t = read_bv_literal();
if (t == NULL_TOKEN) break;
return t;
case '-':
if (m_smtlib2_compliant)
return read_symbol();

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

@ -92,6 +92,7 @@ namespace smt2 {
token read_symbol();
token read_quoted_symbol();
void read_comment();
void read_multiline_comment();
token read_number();
token read_signed_number();
token read_string();