Skip to content

Commit 8e3e625

Browse files
author
Daniel Kroening
committed
smt2 tokenizer: keywords
Keywords are simple symbols preceded by a colon, and used for a range of purposes in the SMT-LIB2 syntax. The tokenizer now recognizes keywords.
1 parent 549d138 commit 8e3e625

File tree

2 files changed

+8
-1
lines changed

2 files changed

+8
-1
lines changed

src/solvers/smt2/smt2_tokenizer.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -254,7 +254,13 @@ void smt2_tokenizert::get_token_from_stream()
254254

255255
case ':': // keyword
256256
token = get_simple_symbol();
257-
return;
257+
if(token == SYMBOL)
258+
{
259+
token = KEYWORD;
260+
return;
261+
}
262+
else
263+
throw error("expecting symbol after colon");
258264

259265
case '#':
260266
if(in->get(ch))

src/solvers/smt2/smt2_tokenizer.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ class smt2_tokenizert:public parsert
6060
STRING_LITERAL,
6161
NUMERAL,
6262
SYMBOL,
63+
KEYWORD,
6364
OPEN,
6465
CLOSE
6566
};

0 commit comments

Comments
 (0)