Added support for bitvector variables to the SMTLIB parser (currently

widths have to be multiples of 8).



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

1 files changed, 17 insertions, 15 deletions

diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index febf76cd..3fef3e64 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -102,7 +102,7 @@ int smtliberror(const char *s)
 %type <node> an_fun an_arithmetic_fun an_bitwise_fun
 %type <node> an_pred
 %type <str> logic_name status attribute user_value annotation annotations 
-%type <str> var fvar
+%type <str> var fvar symb
 
 %token <str> NUMERAL_TOK
 %token <str> SYM_TOK
@@ -114,6 +114,8 @@ int smtliberror(const char *s)
 %token <str> BVBIN_TOK
 %token <str> BVHEX_TOK
 
+%token BITVEC_TOK
+
 %token TRUE_TOK
 %token FALSE_TOK
 %token ITE_TOK
@@ -264,12 +266,13 @@ bench_attribute:
     { 
       // XXX?
     }
+*/
 
-  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK
+  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK LPAREN_TOK SYM_TOK BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK RPAREN_TOK RPAREN_TOK
     {
-      //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
-      //delete $4;
+      PARSER->DeclareExpr(*$5, atoi($8->c_str()));
     }
+/*
   | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
     {
       //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
@@ -435,7 +438,8 @@ an_logical_formula:
 
     LPAREN_TOK NOT_TOK an_formula annotations
     {
-      $$ = Expr::createNot($3);
+      //$$ = Expr::createNot($3);
+      $$ = NULL;
     }
 
   | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations
@@ -843,18 +847,11 @@ basic_term:
     {
       $$ = PARSER->GetVar(*$1);
     }
-/*
-  | fun_symb 
+  | symb
     {
-      if ($1->size() == 1) {
-        $$ = new CVC3::Expr(((*$1)[0]));
-      }
-      else {
-        $$ = new CVC3::Expr(VC->listExpr(*$1));
-      }
-      delete $1;
+      std::cout << "SYMBOL " << *$1 << "\n";
+      $$ = PARSER->GetVar(*$1);
     }
-*/
 ;
 
 
@@ -966,5 +963,10 @@ fvar:
     }
 ;
 
+symb:
+    SYM_TOK
+    {
+      $$ = $1;
+    }
 
 %%