diff options
| -rw-r--r-- | lib/SMT/smtlib.lex | 47 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 44 |
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: |