diff options
Diffstat (limited to 'stp/parser/smtlib.y')
-rw-r--r-- | stp/parser/smtlib.y | 1036 |
1 files changed, 0 insertions, 1036 deletions
diff --git a/stp/parser/smtlib.y b/stp/parser/smtlib.y deleted file mode 100644 index 0aa22dee..00000000 --- a/stp/parser/smtlib.y +++ /dev/null @@ -1,1036 +0,0 @@ -%{ - /******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: July, 2006 - * - * This file is modified version of the CVCL's smtlib.y file. Please - * see CVCL license below - ********************************************************************/ - - /******************************************************************** - * - * \file smtlib.y - * - * Author: Sergey Berezin, Clark Barrett - * - * Created: Apr 30 2005 - * - * <hr> - * Copyright (C) 2004 by the Board of Trustees of Leland Stanford - * Junior University and by New York University. - * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. In particular: - * - * - The above copyright notice and this permission notice must appear - * in all copies of the software and related documentation. - * - * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, - * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. - * - * <hr> - ********************************************************************/ - // -*- c++ -*- - -#include "../AST/AST.h" - using namespace std; - - // Suppress the bogus warning suppression in bison (it generates - // compile error) -#undef __GNUC_MINOR__ - - extern char* yytext; - extern int yylineno; - - //int yylineno; - - extern int yylex(void); - - int yyerror(char *s) { - //yylineno = 0; - cout << "syntax error: line " << yylineno << "\n" << s << endl; - cout << " token: " << yytext << endl; - BEEV::FatalError(""); - return 1; - } - - BEEV::ASTNode query; -#define YYLTYPE_IS_TRIVIAL 1 -#define YYMAXDEPTH 104857600 -#define YYERROR_VERBOSE 1 -#define YY_EXIT_FAILURE -1 -%} - -%union { - // FIXME: Why is this not an UNSIGNED int? - int uintval; /* for numerals in types. */ - - // for BV32 BVCONST - unsigned long long ullval; - - struct { - //stores the indexwidth and valuewidth - //indexwidth is 0 iff type is bitvector. positive iff type is - //array, and stores the width of the indexing bitvector - unsigned int indexwidth; - //width of the bitvector type - unsigned int valuewidth; - } indexvaluewidth; - - //ASTNode,ASTVec - BEEV::ASTNode *node; - BEEV::ASTVec *vec; - std::string *str; -}; - -%start cmd - -%type <indexvaluewidth> sort_symb sort_symbs -%type <node> status -%type <vec> bench_attributes an_formulas - -%type <node> benchmark bench_name bench_attribute -%type <node> an_term an_nonbvconst_term an_formula - -%type <node> var fvar logic_name -%type <str> user_value - -%token <uintval> NUMERAL_TOK -%token <ullval> BVCONST_TOK -%token <node> BITCONST_TOK -%token <node> FORMID_TOK TERMID_TOK -%token <str> STRING_TOK -%token <str> USER_VAL_TOK -%token SOURCE_TOK -%token CATEGORY_TOK -%token DIFFICULTY_TOK -%token BITVEC_TOK -%token ARRAY_TOK -%token SELECT_TOK -%token STORE_TOK -%token TRUE_TOK -%token FALSE_TOK -%token NOT_TOK -%token IMPLIES_TOK -%token ITE_TOK -%token IF_THEN_ELSE_TOK -%token AND_TOK -%token OR_TOK -%token XOR_TOK -%token IFF_TOK -%token EXISTS_TOK -%token FORALL_TOK -%token LET_TOK -%token FLET_TOK -%token NOTES_TOK -%token CVC_COMMAND_TOK -%token SORTS_TOK -%token FUNS_TOK -%token PREDS_TOK -%token EXTENSIONS_TOK -%token DEFINITION_TOK -%token AXIOMS_TOK -%token LOGIC_TOK -%token COLON_TOK -%token LBRACKET_TOK -%token RBRACKET_TOK -%token LPAREN_TOK -%token RPAREN_TOK -%token SAT_TOK -%token UNSAT_TOK -%token UNKNOWN_TOK -%token ASSUMPTION_TOK -%token FORMULA_TOK -%token STATUS_TOK -%token BENCHMARK_TOK -%token EXTRASORTS_TOK -%token EXTRAFUNS_TOK -%token EXTRAPREDS_TOK -%token LANGUAGE_TOK -%token DOLLAR_TOK -%token QUESTION_TOK -%token DISTINCT_TOK -%token SEMICOLON_TOK -%token EOF_TOK -%token EQ_TOK -/*BV SPECIFIC TOKENS*/ -%token NAND_TOK -%token NOR_TOK -%token NEQ_TOK -%token ASSIGN_TOK -%token BV_TOK -%token BOOLEAN_TOK -%token BVLEFTSHIFT_TOK -%token BVLEFTSHIFT_1_TOK -%token BVRIGHTSHIFT_TOK -%token BVRIGHTSHIFT_1_TOK -%token BVPLUS_TOK -%token BVSUB_TOK -%token BVNOT_TOK //bvneg in CVCL -%token BVMULT_TOK -%token BVDIV_TOK -%token BVMOD_TOK -%token BVNEG_TOK //bvuminus in CVCL -%token BVAND_TOK -%token BVOR_TOK -%token BVXOR_TOK -%token BVNAND_TOK -%token BVNOR_TOK -%token BVXNOR_TOK -%token BVCONCAT_TOK -%token BVLT_TOK -%token BVGT_TOK -%token BVLE_TOK -%token BVGE_TOK -%token BVSLT_TOK -%token BVSGT_TOK -%token BVSLE_TOK -%token BVSGE_TOK -%token BVSX_TOK -%token BOOLEXTRACT_TOK -%token BOOL_TO_BV_TOK -%token BVEXTRACT_TOK - -%left LBRACKET_TOK RBRACKET_TOK - -%% - -cmd: - benchmark - { - if($1 != NULL) { - BEEV::globalBeevMgr_for_parser->TopLevelSAT(*$1,query); - delete $1; - } - YYACCEPT; - } -; - -benchmark: - LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK - { - if($4 != NULL){ - if($4->size() > 1) - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND,*$4)); - else - $$ = new BEEV::ASTNode((*$4)[0]); - delete $4; - } - else { - $$ = NULL; - } - } -/* | EOF_TOK */ -/* { */ -/* } */ -; - -bench_name: - FORMID_TOK - { - } -; - -bench_attributes: - bench_attribute - { - $$ = new BEEV::ASTVec; - if ($1 != NULL) { - $$->push_back(*$1); - BEEV::globalBeevMgr_for_parser->AddAssert(*$1); - delete $1; - } - } - | bench_attributes bench_attribute - { - if ($1 != NULL && $2 != NULL) { - $1->push_back(*$2); - BEEV::globalBeevMgr_for_parser->AddAssert(*$2); - $$ = $1; - delete $2; - } - } -; - -bench_attribute: - COLON_TOK ASSUMPTION_TOK an_formula - { - //assumptions are like asserts - $$ = $3; - } - | COLON_TOK FORMULA_TOK an_formula - { - //the query - query = BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT,*$3); - BEEV::globalBeevMgr_for_parser->AddQuery(query); - //dummy true - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); - - - } - | COLON_TOK STATUS_TOK status - { - $$ = NULL; - } - | COLON_TOK LOGIC_TOK logic_name - { - if (!(0 == strcmp($3->GetName(),"QF_UFBV") || - 0 == strcmp($3->GetName(),"QF_AUFBV"))) { - yyerror("Wrong input logic:"); - } - $$ = NULL; - } - | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK var_decls RPAREN_TOK - { - $$ = NULL; - } - | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK var_decls RPAREN_TOK - { - $$ = NULL; - } - | annotation - { - $$ = NULL; - } -; - -logic_name: - FORMID_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = $1; - } - | FORMID_TOK - { - $$ = $1; - } -; - -status: - SAT_TOK { $$ = NULL; } - | UNSAT_TOK { $$ = NULL; } - | UNKNOWN_TOK { $$ = NULL; } -; - - -/* annotations: */ -/* annotation */ -/* { */ -/* } */ -/* | annotations annotation */ -/* { */ -/* } */ -/* ; */ - -annotation: - attribute - { - } - | attribute user_value - { - } -; - -user_value: - USER_VAL_TOK - { - //cerr << "Printing user_value: " << *$1 << endl; - } -; - -attribute: - COLON_TOK SOURCE_TOK - { - } - | COLON_TOK CATEGORY_TOK - { - } - | COLON_TOK DIFFICULTY_TOK -; - -sort_symbs: - sort_symb - { - //a single sort symbol here means either a BitVec or a Boolean - $$.indexwidth = $1.indexwidth; - $$.valuewidth = $1.valuewidth; - } - | sort_symb sort_symb - { - //two sort symbols mean f: type --> type - $$.indexwidth = $1.valuewidth; - $$.valuewidth = $2.valuewidth; - } -; - -var_decls: - var_decl - { - } -// | LPAREN_TOK var_decl RPAREN_TOK - | - var_decls var_decl - { - } -; - -var_decl: - LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK - { - BEEV::_parser_symbol_table.insert(*$2); - //Sort_symbs has the indexwidth/valuewidth. Set those fields in - //var - $2->SetIndexWidth($3.indexwidth); - $2->SetValueWidth($3.valuewidth); - } - | LPAREN_TOK FORMID_TOK RPAREN_TOK - { - BEEV::_parser_symbol_table.insert(*$2); - //Sort_symbs has the indexwidth/valuewidth. Set those fields in - //var - $2->SetIndexWidth(0); - $2->SetValueWidth(0); - } -; - -an_formulas: - an_formula - { - $$ = new BEEV::ASTVec; - if ($1 != NULL) { - $$->push_back(*$1); - delete $1; - } - } - | - an_formulas an_formula - { - if ($1 != NULL && $2 != NULL) { - $1->push_back(*$2); - $$ = $1; - delete $2; - } - } -; - -an_formula: - TRUE_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); - } - | FALSE_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); - } - | fvar - { - $$ = $1; - } - | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedEQ(*$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVSLT_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLT, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVSLE_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLE, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGT, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVSGE_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGE, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVLT_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLT, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVLE_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLE, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVGT_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGT, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK - //| LPAREN_TOK BVGE_TOK an_term an_term annotations RPAREN_TOK - { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGE, *$3, *$4)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK an_formula RPAREN_TOK - { - $$ = $2; - } - | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$3)); - delete $3; - } - | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IMPLIES, *$3, *$4)); - delete $3; - delete $4; - } - | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula RPAREN_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$3, *$4, *$5)); - delete $3; - delete $4; - delete $5; - } - | LPAREN_TOK AND_TOK an_formulas RPAREN_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND, *$3)); - delete $3; - } - | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::OR, *$3)); - delete $3; - } - | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::XOR, *$3, *$4)); - delete $3; - delete $4; - } - | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IFF, *$3, *$4)); - delete $3; - delete $4; - } - | letexpr_mgmt an_formula RPAREN_TOK - //| letexpr_mgmt an_formula annotations RPAREN_TOK - { - $$ = $2; - //Cleanup the LetIDToExprMap - BEEV::globalBeevMgr_for_parser->CleanupLetIDMap(); - } -; - -letexpr_mgmt: - LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK - { - //Expr must typecheck - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$6); - - //set the valuewidth of the identifier - $5->SetValueWidth($6->GetValueWidth()); - $5->SetIndexWidth($6->GetIndexWidth()); - - //populate the hashtable from LET-var --> - //LET-exprs and then process them: - // - //1. ensure that LET variables do not clash - //1. with declared variables. - // - //2. Ensure that LET variables are not - //2. defined more than once - BEEV::globalBeevMgr_for_parser->LetExprMgr(*$5,*$6); - delete $5; - delete $6; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK - { - //Expr must typecheck - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$6); - - //set the valuewidth of the identifier - $5->SetValueWidth($6->GetValueWidth()); - $5->SetIndexWidth($6->GetIndexWidth()); - - //Do LET-expr management - BEEV::globalBeevMgr_for_parser->LetExprMgr(*$5,*$6); - delete $5; - delete $6; - } - -/* an_terms: */ -/* an_term */ -/* { */ -/* } */ -/* | an_terms an_term */ -/* { */ -/* } */ -/* ; */ - -an_term: - BVCONST_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(64, $1)); - } - | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($3, $1)); - } - | an_nonbvconst_term - ; - -an_nonbvconst_term: - BITCONST_TOK { $$ = $1; } - | var - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); - delete $1; - } - | LPAREN_TOK an_term RPAREN_TOK - //| LPAREN_TOK an_term annotations RPAREN_TOK - { - $$ = $2; - //$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(*$2)); - //delete $2; - } - | LPAREN_TOK TERMID_TOK an_term RPAREN_TOK - { - //ARRAY READ - // valuewidth is same as array, indexwidth is 0. - BEEV::ASTNode in = *$2; - BEEV::ASTNode m = *$3; - unsigned int width = in.GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, in, m)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | SELECT_TOK an_term an_term - { - //ARRAY READ - // valuewidth is same as array, indexwidth is 0. - BEEV::ASTNode array = *$2; - BEEV::ASTNode index = *$3; - unsigned int width = array.GetValueWidth(); - BEEV::ASTNode * n = - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, array, index)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | STORE_TOK an_term an_term an_term - { - //ARRAY WRITE - unsigned int width = $4->GetValueWidth(); - BEEV::ASTNode array = *$2; - BEEV::ASTNode index = *$3; - BEEV::ASTNode writeval = *$4; - BEEV::ASTNode write_term = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE,width,array,index,writeval); - write_term.SetIndexWidth($2->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(write_term); - BEEV::ASTNode * n = new BEEV::ASTNode(write_term); - $$ = n; - delete $2; - delete $3; - delete $4; - } -/* | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK BVCONST_TOK */ -/* { */ -/* // This special case is when we have an extract on top of a constant bv, which happens */ -/* // almost all the time in the smt syntax. */ - -/* // $3 is high, $5 is low. They are ints (why not unsigned? See uintval) */ -/* int hi = $3; */ -/* int low = $5; */ -/* int width = hi - low + 1; */ - -/* if (width < 0) */ -/* yyerror("Negative width in extract"); */ - -/* unsigned long long int val = $7; */ - -/* // cut and past from BV32 const evaluator */ - -/* unsigned long long int mask1 = 0xffffffffffffffffLL; */ - -/* mask1 >>= 64-(hi+1); */ - -/* //extract val[hi:0] */ -/* val &= mask1; */ -/* //extract val[hi:low] */ -/* val >>= low; */ - -/* // val is the desired BV32. */ -/* BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(width, val)); */ -/* $$ = n; */ -/* } */ - | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term - { - int width = $3 - $5 + 1; - if (width < 0) - yyerror("Negative width in extract"); - - if((unsigned)$3 >= $7->GetValueWidth() || (unsigned)$5 < 0) - yyerror("Parsing: Wrong width in BVEXTRACT\n"); - - BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3); - BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); - BEEV::ASTNode output = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$7,hi,low); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(output)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $7; - } - | ITE_TOK an_formula an_term an_term - { - unsigned int width = $3->GetValueWidth(); - if (width != $4->GetValueWidth()) { - cerr << *$3; - cerr << *$4; - yyerror("Width mismatch in IF-THEN-ELSE"); - } - if($3->GetIndexWidth() != $4->GetIndexWidth()) - yyerror("Width mismatch in IF-THEN-ELSE"); - - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4); - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedTermITE(*$2, *$3, *$4)); - //$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE,width,*$2, *$3, *$4)); - $$->SetIndexWidth($4->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$); - delete $2; - delete $3; - delete $4; - } - | BVCONCAT_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth() + $3->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - - delete $2; - delete $3; - } - | BVNOT_TOK an_term - { - //this is the BVNEG (term) in the CVCL language - unsigned int width = $2->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNEG, width, *$2)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - } - | BVNEG_TOK an_term - { - //this is the BVUMINUS term in CVCL langauge - unsigned width = $2->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVUMINUS,width,*$2)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - } - | BVAND_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in AND"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVAND, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVOR_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in OR"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVOR, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVXOR_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in XOR"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXOR, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVSUB_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVSUB"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSUB, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVPLUS_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVPLUS"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVPLUS, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - - } - | BVMULT_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVMULT"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMULT, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVNAND_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVNAND"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNAND, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVNOR_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVNOR"); - } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNOR, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVLEFTSHIFT_TOK an_term NUMERAL_TOK - { - unsigned int w = $2->GetValueWidth(); - if((unsigned)$3 < w) { - BEEV::ASTNode trailing_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst($3, 0); - BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, w-$3-1); - BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0); - BEEV::ASTNode m = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$2,hi,low); - BEEV::ASTNode * n = - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,w,m,trailing_zeros)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - } - else - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); - delete $2; - } - | BVLEFTSHIFT_1_TOK an_term an_term - { - unsigned int w = $2->GetValueWidth(); - unsigned int shift_amt = GetUnsignedConst(*$3); - if((unsigned)shift_amt < w) { - BEEV::ASTNode trailing_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0); - BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, w-shift_amt-1); - BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0); - BEEV::ASTNode m = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low); - BEEV::ASTNode * n = - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,w,m,trailing_zeros)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - } - else { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); - } - delete $2; - //delete $3; - } - | BVRIGHTSHIFT_TOK an_term NUMERAL_TOK - { - BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst($3, 0); - unsigned int w = $2->GetValueWidth(); - - //the amount by which you are rightshifting - //is less-than/equal-to the length of input - //bitvector - if((unsigned)$3 < w) { - BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1); - BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$3); - BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$2,hi,low); - BEEV::ASTNode * n = - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,leading_zeros, extract)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - } - else { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); - } - delete $2; - } - | BVRIGHTSHIFT_1_TOK an_term an_term - { - unsigned int shift_amt = GetUnsignedConst(*$3); - BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0); - unsigned int w = $2->GetValueWidth(); - - //the amount by which you are rightshifting - //is less-than/equal-to the length of input - //bitvector - if((unsigned)shift_amt < w) { - BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1); - BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,shift_amt); - BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low); - BEEV::ASTNode * n = - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,leading_zeros, extract)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - } - else { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); - } - delete $2; - } - | BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term - { - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); - unsigned w = $5->GetValueWidth() + $3; - BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w); - BEEV::ASTNode *n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSX,w,*$5,width)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - $$ = n; - delete $5; - } -; - -sort_symb: - BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - // Just return BV width. If sort is BOOL, width is 0. - // Otherwise, BITVEC[w] returns w. - // - //((indexwidth is 0) && (valuewidth>0)) iff type is BV - $$.indexwidth = 0; - unsigned int length = $3; - if(length > 0) { - $$.valuewidth = length; - } - else { - BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); - } - } - | ARRAY_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK - { - unsigned int index_len = $3; - unsigned int value_len = $5; - if(index_len > 0) { - $$.indexwidth = $3; - } - else { - BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); - } - - if(value_len > 0) { - $$.valuewidth = $5; - } - else { - BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); - } - } -; - -var: - FORMID_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); - delete $1; - } - | TERMID_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); - delete $1; - } - | QUESTION_TOK TERMID_TOK - { - $$ = $2; - } -; - -fvar: - DOLLAR_TOK FORMID_TOK - { - $$ = $2; - } - | FORMID_TOK - { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); - delete $1; - } -; -%% |