Added bitvector function/predicate names to the lexer.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73455 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 90 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; }
 
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index f464f7bc..6b7a1978 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -153,6 +153,50 @@ int smtliberror(const char *s)
 %token SEMICOLON_TOK
 %token EOF_TOK
 %token PAT_TOK
+
+%token FALSE_TOK
+%token TRUE_TOK
+
+%token BVCONCAT_TOK
+%token BVEXTRACT_TOK
+
+%token BVNOT_TOK
+%token BVAND_TOK
+%token BVOR_TOK
+%token BVNEG_TOK
+%token BVNAND_TOK
+%token BVNOR_TOK
+%token BVXOR_TOK
+%token BVXNOR_TOK
+
+%token BVCOMP_TOK
+%token BVULT_TOK
+%token BVULE_TOK
+%token BVUGT_TOK
+%token BVUGE_TOK
+%token BVSLT_TOK
+%token BVSLE_TOK
+%token BVSGT_TOK
+%token BVSGE_TOK
+
+%token BVADD_TOK
+%token BVSUB_TOK
+%token BVMUL_TOK
+%token BVUDIV_TOK
+%token BVUREM_TOK
+%token BVSDIV_TOK
+%token BVSREM_TOK
+%token BVSMOD_TOK
+%token BVSHL_TOK
+%token BVLSHR_TOK
+%token BVASHR_TOK
+
+%token REPEAT_TOK
+%token ZEXT_TOK
+%token SEXT_TOK
+%token ROL_TOK
+%token ROR_TOK
+
 %%
 
 cmd: