about summary refs log tree commit diff homepage
path: root/lib/SMT/smtlib.lex
diff options
context:
space:
mode:
Diffstat (limited to 'lib/SMT/smtlib.lex')
-rw-r--r--lib/SMT/smtlib.lex47
1 files changed, 46 insertions, 1 deletions
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index 24acf56c..da61a8f5 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -191,7 +191,7 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 "extrapreds"    { return EXTRAPREDS_TOK; }
 "language"      { return LANGUAGE_TOK; }
 "distinct"      { return DISTINCT_TOK; }
-":pattern"          { return PAT_TOK; } 
+":pattern"      { return PAT_TOK; } 
 ":"             { return COLON_TOK; }
 "\["            { return LBRACKET_TOK; }
 "\]"            { return RBRACKET_TOK; }
@@ -202,6 +202,51 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 "$"             { return DOLLAR_TOK; }
 "?"             { return QUESTION_TOK; }
 
+
+"bit0"          { return FALSE_TOK; }
+"bit1"          { return TRUE_TOK; }
+
+"concat"        { return BVCONCAT_TOK; }
+"extract"       { return BVEXTRACT_TOK; }
+
+"bvnot"         { return BVNOT_TOK; }
+"bvand"         { return BVAND_TOK; }
+"bvor"          { return BVOR_TOK; }
+"bvneg"         { return BVNEG_TOK; }
+"bvnand"        { return BVNAND_TOK; }
+"bvnor"         { return BVNOR_TOK; }
+"bvxor"         { return BVXOR_TOK; }
+"bvxnor"        { return BVXNOR_TOK; }
+
+"bvcomp"        { return BVCOMP_TOK; }
+"bvult"         { return BVULT_TOK; }
+"bvule"         { return BVULE_TOK; }
+"bvugt"         { return BVUGT_TOK; }
+"bvuge"         { return BVUGE_TOK; }
+"bvslt"         { return BVSLT_TOK; }
+"bvsle"         { return BVSLE_TOK; }
+"bvsgt"         { return BVSGT_TOK; }
+"bvsge"         { return BVSGE_TOK; }
+
+"bvadd"         { return BVADD_TOK; }
+"bvsub"         { return BVSUB_TOK; }
+"bvmul"         { return BVMUL_TOK; }
+"bvudiv"        { return BVUDIV_TOK; }
+"bvurem"        { return BVUREM_TOK; }
+"bvsdiv"        { return BVSDIV_TOK; }
+"bvsrem"        { return BVSREM_TOK; }
+"bvsmod"        { return BVSMOD_TOK; }
+"bvshl"         { return BVSHL_TOK; }
+"bvlshr"        { return BVLSHR_TOK; }
+"bvashr"        { return BVASHR_TOK; }
+
+"repeat"        { return REPEAT_TOK; }
+"zero_extend"   { return ZEXT_TOK; }
+"sign_extend"   { return SEXT_TOK; }
+"rotate_left"   { return ROL_TOK; }
+"rotate_right"  { return ROR_TOK; }
+
+
 [=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
 ({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }