From: trevor_hansen Date: Fri, 21 May 2010 18:21:41 +0000 (+0000) Subject: * Add binary & hexidecimal for smtlib2 format. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=04329a5dff69bb4a5e83334e7714ac380eb4a75b;p=francis%2Fstp.git * 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 614fd19..a64692d 100644 --- 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 0021155..c9a4cef 100644 --- a/src/parser/smtlib2.lex +++ b/src/parser/smtlib2.lex @@ -33,14 +33,10 @@ *
********************************************************************/ // -*- c++ -*-L -#include #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; } "\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 b38b755..ba801ee 100644 --- a/src/parser/smtlib2.y +++ b/src/parser/smtlib2.y @@ -94,14 +94,18 @@ %type bench_attributes an_formulas an_terms %type benchmark bench_name bench_attribute -%type an_term an_nonbvconst_term an_formula +%type an_term an_formula %type var fvar logic_name %type user_value %token NUMERAL_TOK -%token BVCONST_TOK -%token BITCONST_TOK + +%token BVCONST_DECIMAL_TOK +%token BVCONST_BINARY_TOK +%token BVCONST_HEXIDECIMAL_TOK + + /*%token BITCONST_TOK*/ %token FORMID_TOK TERMID_TOK %token STRING_TOK %token 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.