* Add binary & hexidecimal for smtlib2 format.

* Fix the syntax of the smtlib2 repeat function.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@775 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/parser/LetMgr.cpp b/src/parser/LetMgr.cpp
index 614fd19f01df64c553475aa69301eada75e20b0d..a64692d312e12aacd45626ef568186526fc1f564 100644 (file)
--- a/src/parser/LetMgr.cpp
+++ b/src/parser/LetMgr.cpp
@@ -77,10 +77,9 @@ namespace BEEV {
     if (_letid_expr_map->size()  ==0)
       return;
 
-
-    // I don't know what this does. Commenting it out and all the regression
-    // tests still pass.
-//#if 0
+    // If ?v0 is encountered and is set with a bitwidth of 6 (say),
+    // when it's next encountered in another let, then we want it to
+    // have a formula type.
     ASTNodeMap::iterator it = _letid_expr_map->begin();
     ASTNodeMap::iterator itend = _letid_expr_map->end();
     for(;it!=itend;it++) {
@@ -89,7 +88,7 @@ namespace BEEV {
         it->first.SetIndexWidth(0);
       }
     }
-//#endif
+
 
     // May contain lots of buckets, so reset.
     delete _letid_expr_map;

diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex
index 0021155d1a9e800177c02b14edd60abe2a6293f7..c9a4cef012594bff4e946a0e8448f8d916263daf 100644 (file)
--- a/src/parser/smtlib2.lex
+++ b/src/parser/smtlib2.lex
@@ -33,14 +33,10 @@
    * <hr>
    ********************************************************************/
   // -*- c++ -*-L
-#include <iostream>
 #include "parser.h"
 #include "parse2SMT_defs.h"
 #include "ParserInterface.h"
 
-  using namespace std;
-  using namespace BEEV;
-  
   extern char *smt2text;
   extern int smt2error (const char *msg);
 
@@ -63,7 +59,7 @@
 
 %x     COMMENT
 %x     STRING_LITERAL
-%x      USER_VALUE
+%x  USER_VALUE
 
 LETTER ([a-zA-Z])
 DIGIT  ([0-9])
@@ -72,22 +68,12 @@ ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})
 
 %%
 [ \n\t\r\f]    { /* sk'ip whitespace */ }
-{DIGIT}+       { smt2lval.uintval = strtoul(smt2text, NULL, 10); return NUMERAL_TOK; }
-
-
-        bv{DIGIT}+     { smt2lval.str = new std::string(smt2text+2); return BVCONST_TOK; }
 
-bit{DIGIT}+     {
-                  char c = smt2text[3];
-                  if (c == '1') {
-                    smt2lval.node = new BEEV::ASTNode(parserInterface->CreateOneConst(1));
-                  }
-                  else {
-                    smt2lval.node = new BEEV::ASTNode(parserInterface->CreateZeroConst(1));
-                  }
-                  return BITCONST_TOK;
-               };
+{DIGIT}+       { smt2lval.uintval = strtoul(smt2text, NULL, 10); return NUMERAL_TOK; }
 
+bv{DIGIT}+     { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_TOK; }
+#b{DIGIT}+  { smt2lval.str = new std::string(smt2text+2); return BVCONST_BINARY_TOK; }
+#x(DIGIT|[a-fA-F])+  { smt2lval.str = new std::string(smt2text+2); return BVCONST_HEXIDECIMAL_TOK; }
 
 ";"            { BEGIN COMMENT; }
 <COMMENT>"\n"  { BEGIN INITIAL; /* return to normal mode */}
@@ -147,9 +133,9 @@ bit{DIGIT}+     {
 "extrasorts"    { return EXTRASORTS_TOK; }
 "extrapreds"    { return EXTRAPREDS_TOK; }
 "language"      { return LANGUAGE_TOK; }
+
+ /* Valid character are: ~ ! @ # $ % ^ & * _ - + = | \ : ; " < > . ? / ( )     */
 ":"             { return COLON_TOK; }
-"\["            { return LBRACKET_TOK; }
-"\]"            { return RBRACKET_TOK; }
 "("             { return LPAREN_TOK; }
 ")"             { return RPAREN_TOK; }
 "$"             { return DOLLAR_TOK; }
@@ -252,14 +238,14 @@ bit{DIGIT}+     {
 
 
 (({LETTER})|(_)({ANYTHING}))({ANYTHING})*      {
-  BEEV::ASTNode nptr = parserInterface->CreateSymbol(smt2text); 
+  BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(smt2text); 
 
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting
   // the whole grammar to eliminate the term/formula distinction.  
-  smt2lval.node = new BEEV::ASTNode(parserInterface->letMgr.ResolveID(nptr));
+  smt2lval.node = new BEEV::ASTNode(BEEV::parserInterface->letMgr.ResolveID(nptr));
   //smt2lval.node = new BEEV::ASTNode(nptr);
-  if ((smt2lval.node)->GetType() == BOOLEAN_TYPE)
+  if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE)
     return FORMID_TOK;
   else 
     return TERMID_TOK;

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index b38b7558eb561321bf59ca3a547814d4cd769310..ba801ee1d91e6c054676c541a345e38c6d602a70 100644 (file)
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -94,14 +94,18 @@
 %type <vec> bench_attributes an_formulas an_terms
 
 %type <node> benchmark bench_name bench_attribute
-%type <node> an_term an_nonbvconst_term an_formula 
+%type <node> an_term  an_formula 
 
 %type <node> var fvar logic_name
 %type <str> user_value
 
 %token <uintval> NUMERAL_TOK
-%token <str> BVCONST_TOK
-%token <node> BITCONST_TOK
+
+%token <str> BVCONST_DECIMAL_TOK
+%token <str> BVCONST_BINARY_TOK
+%token <str> BVCONST_HEXIDECIMAL_TOK
+
+ /*%token <node> BITCONST_TOK*/
 %token <node> FORMID_TOK TERMID_TOK 
 %token <str> STRING_TOK
 %token <str> USER_VAL_TOK
@@ -139,8 +143,6 @@
 %token PIPE_TOK
 %token DOT_TOK
 %token COLON_TOK
-%token LBRACKET_TOK
-%token RBRACKET_TOK
 %token LPAREN_TOK
 %token RPAREN_TOK
 
@@ -211,8 +213,6 @@
 %token EXIT_TOK
 %token CHECK_SAT_TOK
 
-%left LBRACKET_TOK RBRACKET_TOK
-
  /* Functions for QF_AUFBV. */
 %token SELECT_TOK;
 %token STORE_TOK; 
@@ -734,22 +734,9 @@ an_terms an_term
 }
 ;
 
-an_term:
-BVCONST_TOK
-{
-  $$ = new ASTNode(parserInterface->CreateBVConst($1, 10, 32));
-}
-| BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-{
-  $$ = new ASTNode(parserInterface->CreateBVConst($1,10,$3));
-  delete $1;
-}
-| an_nonbvconst_term
-;
 
-an_nonbvconst_term: 
-BITCONST_TOK { $$ = $1; }
-| var
+an_term: 
+var
 {
   $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
   delete $1;
@@ -1090,30 +1077,44 @@ BITCONST_TOK { $$ = $1; }
   $$ = n;
       
 }
-   |  BVREPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 
-    {
-         unsigned count = $3;
+| LPAREN_TOK UNDERSCORE_TOK BVREPEAT_TOK  NUMERAL_TOK  NUMERAL_TOK RPAREN_TOK an_term
+{
+         unsigned count = $4;
          if (count < 1)
                FatalError("One or more repeats please");
 
-         unsigned w = $5->GetValueWidth();  
-      ASTNode n =  *$5;
+         unsigned w = $7->GetValueWidth();  
+      ASTNode n =  *$7;
       
       for (unsigned i =1; i < count; i++)
       {
-         n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$5);
+         n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$7);
       }
       $$ = new ASTNode(n);
-    }
-| UNDERSCORE_TOK BVCONST_TOK NUMERAL_TOK
+}
+| UNDERSCORE_TOK BVCONST_DECIMAL_TOK NUMERAL_TOK
 {
        $$ = new ASTNode(parserInterface->CreateBVConst($2, 10, $3));
     $$->SetValueWidth($3);
 }
+| BVCONST_HEXIDECIMAL_TOK
+{
+       unsigned width = $1->length()*4;
+       $$ = new ASTNode(parserInterface->CreateBVConst($1, 16, width));
+    $$->SetValueWidth(width);
+}
+| BVCONST_BINARY_TOK
+{
+       unsigned width = $1->length();
+       $$ = new ASTNode(parserInterface->CreateBVConst($1, 2, width));
+    $$->SetValueWidth(width);
+}
+
 ;
-  
+
+ 
 sort_symb:
-BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
+BITVEC_TOK LPAREN_TOK NUMERAL_TOK RPAREN_TOK
 {
   // Just return BV width.  If sort is BOOL, width is 0.
   // Otherwise, BITVEC[w] returns w.