Added support for logical formulas in the SMTLIB parser.

Started to work on parsing bitvector terms.


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

1 files changed, 346 insertions, 272 deletions

diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 65931db1..f464f7bc 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -96,8 +96,9 @@ int smtliberror(const char *s)
 %type <pat_ann> patterns_annotations
 */
 
-%type <node> an_formula an_atom prop_atom
-%type <str> logic_name status attribute annotation user_value
+%type <node> an_formula an_logical_formula an_atom prop_atom
+%type <node> an_term basic_term an_fun
+%type <str> logic_name status attribute user_value annotation annotations
 
 
 %token <str> NUMERAL_TOK
@@ -376,26 +377,146 @@ an_formulas:
 */
 
 
-an_formula:
-    an_atom
+an_logical_formula:
+
+    LPAREN_TOK NOT_TOK an_formula RPAREN_TOK
     {
-      $$ = $1;
+      $$ = Expr::createNot($3);
     }
-/*
-  | LPAREN_TOK connective an_formulas annotations RPAREN_TOK
+  | LPAREN_TOK NOT_TOK an_formula annotations RPAREN_TOK
     {
-      $$ = new CVC3::Expr(VC->listExpr(*$2, *$3));
-      delete $2;
-      delete $3;
-      delete $4;
+      $$ = Expr::createNot($3);
     }
-  | LPAREN_TOK connective an_formulas RPAREN_TOK
+
+  | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
     {
-      $$ = new CVC3::Expr(VC->listExpr(*$2, *$3));
-      delete $2;
-      delete $3;
+      $$ = Expr::createImplies($3, $4);
+    }
+  | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = Expr::createImplies($3, $4);
+    }
+
+  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula RPAREN_TOK
+    {
+      $$ = SelectExpr::create($3, $4, $5);
+    }
+  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = SelectExpr::create($3, $4, $5);
+    }
+
+  | LPAREN_TOK AND_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = AndExpr::create($3, $4);
+    }
+  | LPAREN_TOK AND_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = AndExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK OR_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = OrExpr::create($3, $4);
+    }
+  | LPAREN_TOK OR_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = OrExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = XorExpr::create($3, $4);
+    }
+  | LPAREN_TOK XOR_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = XorExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+  | LPAREN_TOK IFF_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+  | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK
+    {
+      $$ = Expr::createNot($3);
+    }
+  | LPAREN_TOK NOT_TOK an_formula annotations RPAREN_TOK
+    {
+      $$ = Expr::createNot($3);
+    }
+
+  | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = Expr::createImplies($3, $4);
+    }
+  | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = Expr::createImplies($3, $4);
+    }
+
+  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula RPAREN_TOK
+    {
+      $$ = SelectExpr::create($3, $4, $5);
+    }
+  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = SelectExpr::create($3, $4, $5);
+    }
+
+  | LPAREN_TOK AND_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = AndExpr::create($3, $4);
+    }
+  | LPAREN_TOK AND_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = AndExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK OR_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = OrExpr::create($3, $4);
+    }
+  | LPAREN_TOK OR_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = OrExpr::create($3, $4);
     }
 
+  | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = XorExpr::create($3, $4);
+    }
+  | LPAREN_TOK XOR_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = XorExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+  | LPAREN_TOK IFF_TOK an_formula an_formula annotations RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+;
+
+
+an_formula:
+    an_atom
+    {
+      $$ = $1;
+    }
+
+  | an_logical_formula
+    {
+      $$ = $1;
+    }
+/*
   | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK
     {
       CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
@@ -434,39 +555,6 @@ an_formula:
 ;
 
 
-/*
-connective:
-    NOT_TOK
-    {
-      $$ = new std::string("_NOT");
-    }
-  | IMPLIES_TOK
-    {
-      $$ = new std::string("_IMPLIES");
-    }
-  | IF_THEN_ELSE_TOK
-    {
-      $$ = new std::string("_IF");
-    }
-  | AND_TOK
-    {
-      $$ = new std::string("_AND");
-    }
-  | OR_TOK
-    {
-      $$ = new std::string("_OR");
-    }
-  | XOR_TOK
-    {
-      $$ = new std::string("_XOR");
-    }
-  | IFF_TOK
-    {
-      $$ = new std::string("_IFF");
-    }
-;
-*/
-
 an_atom:
     prop_atom 
     {
@@ -540,12 +628,10 @@ an_atom:
 prop_atom:
     TRUE_TOK
     {
-      //$$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR"));
       $$ = ConstantExpr::create(1, 1);
     }
   | FALSE_TOK
     { 
-      //$$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR"));
       $$ = ConstantExpr::create(0, 1);;
     }
 /*
@@ -561,20 +647,197 @@ prop_atom:
 ;  
 
 /*
-an_terms:
-    an_term
+an_comparison_fun:
+
+    LPAREN_TOK IMPLIES_TOK an_term an_term RPAREN_TOK
     {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
+      $$ = UltExpr::createImplies($3, $4);
     }
-  | an_terms an_term
+  | LPAREN_TOK IMPLIES_TOK an_term an_term annotations RPAREN_TOK
     {
-      $1->push_back(*$2);
-      $$ = $1; 
-      delete $2;
+      $$ = Expr::createImplies($3, $4);
     }
 ;
+*/
+
+
+an_fun:
+    an_logical_formula
+    {
+      $$ = $1;
+    }
+
+/*
+      $$ = new std::vector<CVC3::Expr>;
+      if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) {
+        $$->push_back(VC->idExpr("_BVLT"));
+      }
+      else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) {
+        $$->push_back(VC->idExpr("_BVLE"));
+      }
+      else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) {
+        $$->push_back(VC->idExpr("_BVGE"));
+      }
+      else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) {
+        $$->push_back(VC->idExpr("_BVGT"));
+      }
+      else if (BVENABLED && *$1 == "bvslt") {
+        $$->push_back(VC->idExpr("_BVSLT"));
+      }
+      else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) {
+        $$->push_back(VC->idExpr("_BVSLE"));
+      }
+      else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) {
+        $$->push_back(VC->idExpr("_BVSGE"));
+      }
+      else if (BVENABLED && *$1 == "bvsgt") {
+        $$->push_back(VC->idExpr("_BVSGT"));
+      }
+      else if (ARRAYSENABLED && *$1 == "select") {
+        $$->push_back(VC->idExpr("_READ"));
+      }
+      else if (ARRAYSENABLED && *$1 == "store") {
+        $$->push_back(VC->idExpr("_WRITE"));
+      }
+      else if (BVENABLED && *$1 == "bit0") {
+        $$->push_back(VC->idExpr("_BVCONST"));
+        $$->push_back(VC->ratExpr(0));
+        $$->push_back(VC->ratExpr(1));
+      }
+      else if (BVENABLED && *$1 == "bit1") {
+        $$->push_back(VC->idExpr("_BVCONST"));
+        $$->push_back(VC->ratExpr(1));
+        $$->push_back(VC->ratExpr(1));
+      }
+      else if (BVENABLED && *$1 == "concat") {
+        $$->push_back(VC->idExpr("_CONCAT"));
+      }
+      else if (BVENABLED && *$1 == "bvnot") {
+        $$->push_back(VC->idExpr("_BVNEG"));
+      }
+      else if (BVENABLED && *$1 == "bvand") {
+        $$->push_back(VC->idExpr("_BVAND"));
+      }
+      else if (BVENABLED && *$1 == "bvor") {
+        $$->push_back(VC->idExpr("_BVOR"));
+      }
+      else if (BVENABLED && *$1 == "bvneg") {
+        $$->push_back(VC->idExpr("_BVUMINUS"));
+      }
+      else if (BVENABLED && *$1 == "bvadd") {
+        $$->push_back(VC->idExpr("_BVPLUS"));
+      }
+      else if (BVENABLED && *$1 == "bvmul") {
+        $$->push_back(VC->idExpr("_BVMULT"));
+      }
+      else if (BVENABLED && *$1 == "bvudiv") {
+        $$->push_back(VC->idExpr("_BVUDIV"));
+      }
+      else if (BVENABLED && *$1 == "bvurem") {
+        $$->push_back(VC->idExpr("_BVUREM"));
+      }
+      else if (BVENABLED && *$1 == "bvshl") {
+        $$->push_back(VC->idExpr("_BVSHL"));
+      }
+      else if (BVENABLED && *$1 == "bvlshr") {
+        $$->push_back(VC->idExpr("_BVLSHR"));
+      }
+
+      else if (BVENABLED && *$1 == "bvxor") {
+        $$->push_back(VC->idExpr("_BVXOR"));
+      }
+      else if (BVENABLED && *$1 == "bvxnor") {
+        $$->push_back(VC->idExpr("_BVXNOR"));
+      }
+      else if (BVENABLED && *$1 == "bvcomp") {
+        $$->push_back(VC->idExpr("_BVCOMP"));
+      }
+
+      else if (BVENABLED && *$1 == "bvsub") {
+        $$->push_back(VC->idExpr("_BVSUB"));
+      }
+      else if (BVENABLED && *$1 == "bvsdiv") {
+        $$->push_back(VC->idExpr("_BVSDIV"));
+      }
+      else if (BVENABLED && *$1 == "bvsrem") {
+        $$->push_back(VC->idExpr("_BVSREM"));
+      }
+      else if (BVENABLED && *$1 == "bvsmod") {
+        $$->push_back(VC->idExpr("_BVSMOD"));
+      }
+      else if (BVENABLED && *$1 == "bvashr") {
+        $$->push_back(VC->idExpr("_BVASHR"));
+      }
+
+      // For backwards compatibility:
+      else if (BVENABLED && *$1 == "shift_left0") {
+        $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT"));
+      }
+      else if (BVENABLED && *$1 == "shift_right0") {
+        $$->push_back(VC->idExpr("_RIGHTSHIFT"));
+      }
+      else if (BVENABLED && *$1 == "sign_extend") {
+        $$->push_back(VC->idExpr("_SX"));
+        $$->push_back(VC->idExpr("_smtlib"));
+      }
+
+      // Bitvector constants
+      else if (BVENABLED &&
+               $1->size() > 2 &&
+               (*$1)[0] == 'b' &&
+               (*$1)[1] == 'v') {
+        bool done = false;
+        if ((*$1)[2] >= '0' && (*$1)[2] <= '9') {
+          int i = 3;
+          while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
+          if ((*$1)[i] == '\0') {
+            $$->push_back(VC->idExpr("_BVCONST"));
+            $$->push_back(VC->ratExpr($1->substr(2), 10));
+            $$->push_back(VC->ratExpr(32));
+            done = true;
+          }
+        }
+        else if ($1->size() > 5) {
+          std::string s = $1->substr(0,5);
+          if (s == "bvbin") {
+            int i = 5;
+            while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i;
+            if ((*$1)[i] == '\0') {
+              $$->push_back(VC->idExpr("_BVCONST"));
+              $$->push_back(VC->ratExpr($1->substr(5), 2));
+              $$->push_back(VC->ratExpr(i-5));
+              done = true;
+            }
+          }
+          else if (s == "bvhex") {
+            int i = 5;
+            char c = (*$1)[i];
+            while ((c >= '0' && c <= '9') ||
+                   (c >= 'a' && c <= 'f') ||
+                   (c >= 'A' && c <= 'F')) {
+              ++i;
+              c =(*$1)[i];
+            }
+            if ((*$1)[i] == '\0') {
+              $$->push_back(VC->idExpr("_BVCONST"));
+              $$->push_back(VC->ratExpr($1->substr(5), 16));
+              $$->push_back(VC->ratExpr(i-5));
+              done = true;
+            }
+          }
+        }
+        if (!done) $$->push_back(VC->idExpr(*$1));
+      }
+      else {
+        $$->push_back(VC->idExpr(*$1));
+      }
+      delete $1;
+*/
+
+
+
+;
+
 
 an_term:
     basic_term 
@@ -586,47 +849,33 @@ an_term:
       $$ = $2;
       delete $3;
     }
-  | LPAREN_TOK fun_symb an_terms annotations RPAREN_TOK
+
+  | an_fun
     {
-      $2->insert($2->end(), $3->begin(), $3->end());
-      $$ = new CVC3::Expr(VC->listExpr(*$2));
-      delete $2;
-      delete $3;
-      delete $4;
+      $$ = $1;
     }
-  | LPAREN_TOK fun_symb an_terms RPAREN_TOK
+
+  | LPAREN_TOK ITE_TOK an_formula an_term an_term RPAREN_TOK
     {
-      $2->insert($2->end(), $3->begin(), $3->end());
-      $$ = new CVC3::Expr(VC->listExpr(*$2));
-      delete $2;
-      delete $3;
+      $$ = SelectExpr::create($3, $4, $5);
     }
   | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK
     {
-      $$ = new CVC3::Expr(VC->listExpr("_IF", *$3, *$4, *$5));
-      delete $3;
-      delete $4;
-      delete $5;
-      delete $6;
-    }
-  | LPAREN_TOK ITE_TOK an_formula an_term an_term RPAREN_TOK
-    {
-      $$ = new CVC3::Expr(VC->listExpr("_IF", *$3, *$4, *$5));
-      delete $3;
-      delete $4;
-      delete $5;
+      $$ = SelectExpr::create($3, $4, $5);
     }
 ;
 
+
 basic_term:
-  | TRUE_TOK
+    TRUE_TOK
     {
-      $$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR"));
+      $$ = ConstantExpr::create(1, 1);
     }
   | FALSE_TOK
     { 
-      $$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR"));
+      $$ = ConstantExpr::create(0, 1);;
     }
+/*
   | fvar
     {
       $$ = $1;
@@ -645,39 +894,25 @@ basic_term:
       }
       delete $1;
     }
-;
 */
+;
+
+
 
-/*
 annotations:
-    annotation
-    {
-      $$->push_back(*$1);
-      delete $1;
-    }
-  | annotations annotation
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-  ;
-*/
+    annotation { }
+  | annotations annotation { }
+;
 
 annotation:
-    attribute
-    { $$ = $1; }
-
-  | attribute user_value
-    { $$ = $1; }
+    attribute { }
 
+  | attribute user_value {  }
 ;
 
-
 user_value:
-    USER_VAL_TOK
+    USER_VAL_TOK  
     {
-      $$ = NULL;
       delete $1;
     }
 ;
@@ -775,7 +1010,9 @@ pred_symb:
       delete $1;
     }
 ;
+*/
 
+/*
 fun_symb:
     SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
     {
@@ -828,171 +1065,9 @@ fun_symb:
     }
   | SYM_TOK
     {
-      $$ = new std::vector<CVC3::Expr>;
-      if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) {
-        $$->push_back(VC->idExpr("_BVLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) {
-        $$->push_back(VC->idExpr("_BVLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) {
-        $$->push_back(VC->idExpr("_BVGE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) {
-        $$->push_back(VC->idExpr("_BVGT"));
-      }
-      else if (BVENABLED && *$1 == "bvslt") {
-        $$->push_back(VC->idExpr("_BVSLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) {
-        $$->push_back(VC->idExpr("_BVSLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) {
-        $$->push_back(VC->idExpr("_BVSGE"));
-      }
-      else if (BVENABLED && *$1 == "bvsgt") {
-        $$->push_back(VC->idExpr("_BVSGT"));
-      }
-      else if (ARRAYSENABLED && *$1 == "select") {
-        $$->push_back(VC->idExpr("_READ"));
-      }
-      else if (ARRAYSENABLED && *$1 == "store") {
-        $$->push_back(VC->idExpr("_WRITE"));
-      }
-      else if (BVENABLED && *$1 == "bit0") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(0));
-        $$->push_back(VC->ratExpr(1));
-      }
-      else if (BVENABLED && *$1 == "bit1") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(1));
-        $$->push_back(VC->ratExpr(1));
-      }
-      else if (BVENABLED && *$1 == "concat") {
-        $$->push_back(VC->idExpr("_CONCAT"));
-      }
-      else if (BVENABLED && *$1 == "bvnot") {
-        $$->push_back(VC->idExpr("_BVNEG"));
-      }
-      else if (BVENABLED && *$1 == "bvand") {
-        $$->push_back(VC->idExpr("_BVAND"));
-      }
-      else if (BVENABLED && *$1 == "bvor") {
-        $$->push_back(VC->idExpr("_BVOR"));
-      }
-      else if (BVENABLED && *$1 == "bvneg") {
-        $$->push_back(VC->idExpr("_BVUMINUS"));
-      }
-      else if (BVENABLED && *$1 == "bvadd") {
-        $$->push_back(VC->idExpr("_BVPLUS"));
-      }
-      else if (BVENABLED && *$1 == "bvmul") {
-        $$->push_back(VC->idExpr("_BVMULT"));
-      }
-      else if (BVENABLED && *$1 == "bvudiv") {
-        $$->push_back(VC->idExpr("_BVUDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvurem") {
-        $$->push_back(VC->idExpr("_BVUREM"));
-      }
-      else if (BVENABLED && *$1 == "bvshl") {
-        $$->push_back(VC->idExpr("_BVSHL"));
-      }
-      else if (BVENABLED && *$1 == "bvlshr") {
-        $$->push_back(VC->idExpr("_BVLSHR"));
-      }
-
-      else if (BVENABLED && *$1 == "bvxor") {
-        $$->push_back(VC->idExpr("_BVXOR"));
-      }
-      else if (BVENABLED && *$1 == "bvxnor") {
-        $$->push_back(VC->idExpr("_BVXNOR"));
-      }
-      else if (BVENABLED && *$1 == "bvcomp") {
-        $$->push_back(VC->idExpr("_BVCOMP"));
-      }
 
-      else if (BVENABLED && *$1 == "bvsub") {
-        $$->push_back(VC->idExpr("_BVSUB"));
-      }
-      else if (BVENABLED && *$1 == "bvsdiv") {
-        $$->push_back(VC->idExpr("_BVSDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvsrem") {
-        $$->push_back(VC->idExpr("_BVSREM"));
-      }
-      else if (BVENABLED && *$1 == "bvsmod") {
-        $$->push_back(VC->idExpr("_BVSMOD"));
-      }
-      else if (BVENABLED && *$1 == "bvashr") {
-        $$->push_back(VC->idExpr("_BVASHR"));
-      }
-
-      // For backwards compatibility:
-      else if (BVENABLED && *$1 == "shift_left0") {
-        $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "shift_right0") {
-        $$->push_back(VC->idExpr("_RIGHTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "sign_extend") {
-        $$->push_back(VC->idExpr("_SX"));
-        $$->push_back(VC->idExpr("_smtlib"));
-      }
-
-      // Bitvector constants
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        bool done = false;
-        if ((*$1)[2] >= '0' && (*$1)[2] <= '9') {
-          int i = 3;
-          while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-          if ((*$1)[i] == '\0') {
-            $$->push_back(VC->idExpr("_BVCONST"));
-            $$->push_back(VC->ratExpr($1->substr(2), 10));
-            $$->push_back(VC->ratExpr(32));
-            done = true;
-          }
-        }
-        else if ($1->size() > 5) {
-          std::string s = $1->substr(0,5);
-          if (s == "bvbin") {
-            int i = 5;
-            while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i;
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 2));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-          else if (s == "bvhex") {
-            int i = 5;
-            char c = (*$1)[i];
-            while ((c >= '0' && c <= '9') ||
-                   (c >= 'a' && c <= 'f') ||
-                   (c >= 'A' && c <= 'F')) {
-              ++i;
-              c =(*$1)[i];
-            }
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 16));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-        }
-        if (!done) $$->push_back(VC->idExpr(*$1));
-      }
-      else {
-        $$->push_back(VC->idExpr(*$1));
-      }
-      delete $1;
     }
+
   | AR_SYMB 
     { 
       $$ = new std::vector<CVC3::Expr>;
@@ -1028,7 +1103,6 @@ fun_symb:
 ;
 */
 
-
 attribute:
     COLON_TOK SYM_TOK
     {