using namespace BEEV;
extern int smtparse(void*);
+extern int smt2parse(void*);
extern int cvcparse(void*);
extern int cvclex_destroy(void);
extern int smtlex_destroy(void);
+extern int smt2lex_destroy(void);
// callback for SIGALRM.
void handle_time_out(int parameter){
bool onePrintBack =false;
+static string tolower(const char * name)
+{
+ string s(name);
+ for (size_t i = 0; i < s.size(); ++i)
+ s[i] = ::tolower(s[i]);
+ return s;
+}
+
+
+
// Amount of memory to ask for at beginning of main.
static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
/********************************************************************
* step 5. Call SAT to determine if input is SAT or UNSAT
********************************************************************/
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT} OptionType;
int main(int argc, char ** argv) {
- char * infile;
+ char * infile = NULL;
extern FILE *cvcin;
extern FILE *smtin;
+ extern FILE *smt2in;
// Grab some memory from the OS upfront to reduce system time when
// individual hash tables are being allocated
helpstring +=
"-j <filename> : CNF Dumping. Creates a DIMACS equivalent file of the input STP file\n";
helpstring +=
- "-m : use the SMTLIB parser\n";
+ "-m : use the SMTLIB1 parser\n";
helpstring += "--output-CNF : save the CNF into output.cnf\n";
helpstring += "--output-bench : save in ABC's bench format to output.bench\n";
helpstring +=
"--print-back-CVC : print input in CVC format, then exit\n";
helpstring +=
- "--print-back-SMTLIB : print input in SMT-LIB2 format, then exit\n";
+ "--print-back-SMTLIB2 : print input in SMT-LIB2 format, then exit\n";
helpstring +=
"--print-back-SMTLIB1 : print input in SMT-LIB1 format, then exit\n";
helpstring +=
"-r : switch refinement off (optimizations are ON by default)\n";
helpstring +=
"-s : print function statistics\n";
-
- #if !defined CRYPTOMINISAT2
+#if !defined CRYPTOMINISAT2
+helpstring +=
+ "--simplifying-minisat : use simplifying-minisat rather than minisat\n";
+#endif
helpstring +=
- "--simplifying-minisat : use simplifying-minisat rather than minisat\n";
- #endif
-
+ "--SMTLIB1 : use the SMT-LIB1 format parser\n";
+ helpstring +=
+ "--SMTLIB2 : use the SMT-LIB2 format parser\n";
helpstring +=
"-t : print quick statistics\n";
helpstring +=
{
// long options.
map<string,OptionType> lookup;
- lookup.insert(make_pair("--print-back-C",PRINT_BACK_C));
- lookup.insert(make_pair("--print-back-CVC",PRINT_BACK_CVC));
- lookup.insert(make_pair("--print-back-SMTLIB",PRINT_BACK_SMTLIB));
- lookup.insert(make_pair("--print-back-SMTLIB1",PRINT_BACK_SMTLIB1));
- lookup.insert(make_pair("--print-back-GDL",PRINT_BACK_GDL));
- lookup.insert(make_pair("--print-back-dot",PRINT_BACK_DOT));
- lookup.insert(make_pair("--output-CNF",OUTPUT_CNF));
- lookup.insert(make_pair("--output-bench",OUTPUT_BENCH));
- lookup.insert(make_pair("--simplifying-minisat",USE_SIMPLIFYING_SOLVER));
-
-
- switch(lookup[argv[i]])
+ lookup.insert(make_pair(tolower("--print-back-C"),PRINT_BACK_C));
+ lookup.insert(make_pair(tolower("--print-back-CVC"),PRINT_BACK_CVC));
+ lookup.insert(make_pair(tolower("--print-back-SMTLIB2"),PRINT_BACK_SMTLIB2));
+ lookup.insert(make_pair(tolower("--print-back-SMTLIB1"),PRINT_BACK_SMTLIB1));
+ lookup.insert(make_pair(tolower("--print-back-GDL"),PRINT_BACK_GDL));
+ lookup.insert(make_pair(tolower("--print-back-dot"),PRINT_BACK_DOT));
+ lookup.insert(make_pair(tolower("--output-CNF"),OUTPUT_CNF));
+ lookup.insert(make_pair(tolower("--output-bench"),OUTPUT_BENCH));
+ lookup.insert(make_pair(tolower("--simplifying-minisat"),USE_SIMPLIFYING_SOLVER));
+ lookup.insert(make_pair(tolower("--SMTLIB2"),SMT_LIB2_FORMAT));
+ lookup.insert(make_pair(tolower("--SMTLIB1"),SMT_LIB1_FORMAT));
+
+ switch(lookup[tolower(argv[i])])
{
case PRINT_BACK_C:
bm->UserFlags.print_STPinput_back_C_flag = true;
bm->UserFlags.print_STPinput_back_CVC_flag = true;
onePrintBack = true;
break;
- case PRINT_BACK_SMTLIB:
- bm->UserFlags.print_STPinput_back_SMTLIB_flag = true;
+ case PRINT_BACK_SMTLIB2:
+ bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true;
onePrintBack = true;
break;
case PRINT_BACK_SMTLIB1:
case OUTPUT_BENCH:
bm->UserFlags.output_bench_flag = true;
break;
+ case SMT_LIB2_FORMAT:
+ bm->UserFlags.smtlib2_parser_flag = true;
+ bm->UserFlags.division_by_zero_returns_one_flag = true;
+ if (bm->UserFlags.smtlib1_parser_flag)
+ FatalError("Can't use both the smtlib and smtlib2 parsers");
+ break;
+ case SMT_LIB1_FORMAT:
+ bm->UserFlags.smtlib1_parser_flag = true;
+ bm->UserFlags.division_by_zero_returns_one_flag = true;
+ if (bm->UserFlags.smtlib2_parser_flag)
+ FatalError("Can't use both the smtlib and smtlib2 parsers");
+ break;
+
#if !defined CRYPTOMINISAT && !defined CRYPTOMINISAT2
case USE_SIMPLIFYING_SOLVER:
bm->UserFlags.print_cnf_flag = true;
bm->UserFlags.cnf_dump_filename = argv[++i];
break;
- case 'n':
- bm->UserFlags.print_output_flag = true;
- break;
case 'm':
- bm->UserFlags.smtlib_parser_flag=true;
+ bm->UserFlags.smtlib1_parser_flag=true;
bm->UserFlags.division_by_zero_returns_one_flag = true;
+ if (bm->UserFlags.smtlib2_parser_flag)
+ FatalError("Can't use both the smtlib and smtlib2 parsers");
+
+ break;
+ case 'n':
+ bm->UserFlags.print_output_flag = true;
break;
case 'p':
bm->UserFlags.print_counterexample_flag = true;
}
}
} else {
- infile = argv[i];
- if (bm->UserFlags.smtlib_parser_flag)
- {
- smtin = fopen(infile,"r");
- if(smtin == NULL)
- {
- fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
- FatalError("");
- }
- }
- else
+ if (NULL != infile)
+ FatalError("One input file only.");
+ infile = argv[i];
+ }
+ }
+
+ if (!bm->UserFlags.smtlib1_parser_flag && !bm->UserFlags.smtlib2_parser_flag)
+ {
+ // No parser is explicity requested.
+ if (NULL != infile && strlen(infile)>=5)
+ {
+ string f(infile);
+ if (!f.compare(f.length()-4, 4,".smt"))
+ {
+ bm->UserFlags.smtlib1_parser_flag = true;
+ }
+ if (!f.compare(f.length()-5, 5,".smt2"))
+ {
+ bm->UserFlags.smtlib2_parser_flag = true;
+ }
+ }
+ }
+
+ // If we're not reading the file from stdin.
+ if (infile != NULL)
+ {
+ if (bm->UserFlags.smtlib1_parser_flag)
+ {
+ smtin = fopen(infile,"r");
+ if(smtin == NULL)
+ {
+ fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
+ FatalError("");
+ }
+ } else
+ if (bm->UserFlags.smtlib2_parser_flag)
{
- cvcin = fopen(infile,"r");
- if(cvcin == NULL)
+ smt2in = fopen(infile,"r");
+ if(smt2in == NULL)
{
fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
FatalError("");
}
}
- }
+
+ else
+ {
+ cvcin = fopen(infile,"r");
+ if(cvcin == NULL)
+ {
+ fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
+ FatalError("");
+ }
}
+ }
+
//want to print the output always from the commandline.
bm->UserFlags.print_output_flag = true;
bm->GetRunTimes()->start(RunTimes::Parsing);
{
- // Wrap a typchecking node factory around the default node factory.
- // Every node created is typechecked.
- SimplifyingNodeFactory simpNF(*bm->defaultNodeFactory, *bm);
- TypeChecker nf(simpNF, *bm);
+ SimplifyingNodeFactory simpNF(*bm->defaultNodeFactory, *bm);
+ TypeChecker nfTypeCheckSimp(simpNF, *bm);
+ TypeChecker nfTypeCheckDefault(*bm->defaultNodeFactory, *bm);
+
+ ParserInterface piTypeCheckSimp(*bm, &nfTypeCheckSimp);
+ ParserInterface piTypeCheckDefault(*bm, &nfTypeCheckDefault);
+
+ // If you are converting formats, you probably don't want it simplifying (at least I dont).
+ if (false && onePrintBack)
+ {
+ parserInterface = &piTypeCheckDefault;
+ }
+ else
+ parserInterface = &piTypeCheckSimp;
- ParserInterface pi(*bm, &nf);
- parserInterface = π
- if (bm->UserFlags.smtlib_parser_flag) {
+ if (bm->UserFlags.smtlib1_parser_flag) {
smtparse((void*) AssertsQuery);
smtlex_destroy();
+ } else if (bm->UserFlags.smtlib2_parser_flag) {
+ smt2parse((void*) AssertsQuery);
+ smt2lex_destroy();
} else {
cvcparse((void*) AssertsQuery);
cvclex_destroy();
if(bm->UserFlags.print_STPinput_back_flag)
{
- if(bm->UserFlags.smtlib_parser_flag)
- bm->UserFlags.print_STPinput_back_SMTLIB_flag = true;
+ if(bm->UserFlags.smtlib1_parser_flag)
+ bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true;
else
bm->UserFlags.print_STPinput_back_CVC_flag = true;
}
printer::SMTLIB1_PrintBack(cout, original_input);
}
- if (bm->UserFlags.print_STPinput_back_SMTLIB_flag)
+ if (bm->UserFlags.print_STPinput_back_SMTLIB2_flag)
{
printer::SMTLIB2_PrintBack(cout, original_input);
}
--- /dev/null
+%{
+ /********************************************************************
+ * AUTHORS: Trevor Hansen, Vijay Ganesh, David L. Dill
+ *
+ * BEGIN DATE: July, 2006
+ *
+ * This file is modified version of the CVCL's smtlib.lex file. Please
+ * see CVCL license below
+ ********************************************************************/
+
+ /********************************************************************
+ * \file smtlib.lex
+ *
+ * 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++ -*-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);
+
+ // File-static (local to this file) variables and functions
+ static std::string _string_lit;
+ static char escapeChar(char c) {
+ switch(c) {
+ case 'n': return '\n';
+ case 't': return '\t';
+ default: return c;
+ }
+ }
+%}
+
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+
+%x COMMENT
+%x STRING_LITERAL
+%x USER_VALUE
+
+LETTER ([a-zA-Z])
+DIGIT ([0-9])
+OPCHAR (['\.\_])
+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;
+ };
+
+
+";" { BEGIN COMMENT; }
+<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */}
+<COMMENT>. { /* stay in comment mode */ }
+
+<INITIAL>"\"" { BEGIN STRING_LITERAL;
+ _string_lit.erase(_string_lit.begin(),
+ _string_lit.end()); }
+<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */
+ _string_lit.insert(_string_lit.end(),
+ escapeChar(smt2text[1])); }
+
+ <STRING_LITERAL>"\"" { BEGIN INITIAL;
+ smt2lval.str = new std::string(_string_lit);
+ return STRING_TOK; }
+
+<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*smt2text); }
+
+<INITIAL>"|" { BEGIN USER_VALUE;
+ _string_lit.erase(_string_lit.begin(),
+ _string_lit.end()); }
+<USER_VALUE>"|" { BEGIN INITIAL; /* return to normal mode */
+ smt2lval.str = new std::string(_string_lit);
+ return USER_VAL_TOK; }
+<USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n');}
+<USER_VALUE>. { _string_lit.insert(_string_lit.end(),*smt2text); }
+
+
+ /*
+ <INITIAL>"{" { BEGIN USER_VALUE;
+ _string_lit.erase(_string_lit.begin(),
+ _string_lit.end()); }
+ <USER_VALUE>"\\"[{}] {
+ _string_lit.insert(_string_lit.end(),smt2text[1]); }
+
+ <USER_VALUE>"}" { BEGIN INITIAL;
+ smt2lval.str = new std::string(_string_lit);
+ return USER_VAL_TOK; }
+ <USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n');}
+ <USER_VALUE>. { _string_lit.insert(_string_lit.end(),*smt2text); }
+*/
+
+"notes" { return NOTES_TOK; }
+"sorts" { return SORTS_TOK; }
+"funs" { return FUNS_TOK; }
+"preds" { return PREDS_TOK; }
+"extensions" { return EXTENSIONS_TOK; }
+"definition" { return DEFINITION_TOK; }
+"axioms" { return AXIOMS_TOK; }
+"sat" { return SAT_TOK; }
+"unsat" { return UNSAT_TOK; }
+"unknown" { return UNKNOWN_TOK; }
+"assumption" { return ASSUMPTION_TOK; }
+"status" { return STATUS_TOK; }
+
+"benchmark" { return BENCHMARK_TOK; }
+"extrasorts" { return EXTRASORTS_TOK; }
+"extrapreds" { return EXTRAPREDS_TOK; }
+"language" { return LANGUAGE_TOK; }
+":" { return COLON_TOK; }
+"\[" { return LBRACKET_TOK; }
+"\]" { return RBRACKET_TOK; }
+"(" { return LPAREN_TOK; }
+")" { return RPAREN_TOK; }
+"$" { return DOLLAR_TOK; }
+"?" { return QUESTION_TOK; }
+"_" { return UNDERSCORE_TOK; }
+"\|" { return PIPE_TOK; }
+"." { return DOT_TOK; }
+
+ /* Set info types */
+"source" { return SOURCE_TOK;}
+"category" { return CATEGORY_TOK;}
+"difficulty" { return DIFFICULTY_TOK; }
+"smt-lib-version" { return VERSION_TOK; }
+
+ /* COMMANDS */
+"set-logic" { return LOGIC_TOK; }
+"set-info" { return NOTES_TOK; }
+"declare-fun" { return DECLARE_FUNCTION_TOK; }
+ /*
+ "set-option"
+ "declare-sort"
+ "define-sort"
+ "push"
+ "pop"
+*/
+"assert" { return FORMULA_TOK; }
+"check-sat" { return CHECK_SAT_TOK; }
+ /*
+ "get-assertions"
+ "get-proof"
+ "get-unsat-core"
+ "get-value"
+ "get-assignment"
+ "get-option"
+ "get-info"
+*/
+"exit" {return EXIT_TOK;}
+
+ /* Types for QF_BV and QF_AUFBV. */
+"BitVec" { return BITVEC_TOK;}
+"Array" { return ARRAY_TOK;}
+"Bool" { return BOOL_TOK;}
+
+
+ /* CORE THEORY pg. 29 of the SMT-LIB2 standard 30-March-2010. */
+"true" { return TRUE_TOK; }
+"false" { return FALSE_TOK; }
+"not" { return NOT_TOK; }
+"and" { return AND_TOK; }
+"or" { return OR_TOK; }
+"xor" { return XOR_TOK;}
+"ite" { return ITE_TOK;} // PARAMETRIC
+"=" { return EQ_TOK;}
+"=>" { return IMPLIES_TOK; }
+
+ /* CORE THEORY. But not on pg 29. */
+"distinct" { return DISTINCT_TOK; } // variadic
+"let" { return LET_TOK; }
+
+ /* Functions for QF_BV and QF_AUFBV. */
+"bvshl" { return BVLEFTSHIFT_1_TOK;}
+"bvlshr" { return BVRIGHTSHIFT_1_TOK;}
+"bvashr" { return BVARITHRIGHTSHIFT_TOK;}
+"bvadd" { return BVPLUS_TOK;}
+"bvsub" { return BVSUB_TOK;}
+"bvnot" { return BVNOT_TOK;}
+"bvmul" { return BVMULT_TOK;}
+"bvudiv" { return BVDIV_TOK;}
+"bvsdiv" { return SBVDIV_TOK;}
+"bvurem" { return BVMOD_TOK;}
+"bvsrem" { return SBVREM_TOK;}
+"bvsmod" { return SBVMOD_TOK;}
+"bvneg" { return BVNEG_TOK;}
+"bvand" { return BVAND_TOK;}
+"bvor" { return BVOR_TOK;}
+"bvxor" { return BVXOR_TOK;}
+"bvnand" { return BVNAND_TOK;}
+"bvnor" { return BVNOR_TOK;}
+"bvxnor" { return BVXNOR_TOK;}
+"concat" { return BVCONCAT_TOK;}
+"extract" { return BVEXTRACT_TOK;}
+"bvult" { return BVLT_TOK;}
+"bvugt" { return BVGT_TOK;}
+"bvule" { return BVLE_TOK;}
+"bvuge" { return BVGE_TOK;}
+"bvslt" { return BVSLT_TOK;}
+"bvsgt" { return BVSGT_TOK;}
+"bvsle" { return BVSLE_TOK;}
+"bvsge" { return BVSGE_TOK;}
+"bvcomp" { return BVCOMP_TOK;}
+"zero_extend" { return BVZX_TOK;}
+"sign_extend" { return BVSX_TOK;}
+"repeat" { return BVREPEAT_TOK;}
+"rotate_left" { return BVROTATE_LEFT_TOK;}
+"rotate_right" { return BVROTATE_RIGHT_TOK;}
+
+ /* Functions for QF_AUFBV. */
+"select" { return SELECT_TOK; }
+"store" { return STORE_TOK; }
+
+
+(({LETTER})|(_)({ANYTHING}))({ANYTHING})* {
+ BEEV::ASTNode nptr = 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(nptr);
+ if ((smt2lval.node)->GetType() == BOOLEAN_TYPE)
+ return FORMID_TOK;
+ else
+ return TERMID_TOK;
+
+}
+. { smt2error("Illegal input character."); }
+%%
--- /dev/null
+%{
+ /********************************************************************
+ * AUTHORS: Trevor Hansen, Vijay Ganesh
+ *
+ * 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 "ParserInterface.h"
+
+ using namespace std;
+ using namespace BEEV;
+
+ // Suppress the bogus warning suppression in bison (it generates
+ // compile error)
+#undef __GNUC_MINOR__
+
+ extern char* smt2text;
+ extern int smt2lineno;
+ extern int smt2lex(void);
+
+ int yyerror(const char *s) {
+ cout << "syntax error: line " << smt2lineno << "\n" << s << endl;
+ cout << " token: " << smt2text << endl;
+ FatalError("");
+ return 1;
+ }
+
+ ASTNode querysmt2;
+ ASTVec assertionsSMT2;
+ vector<string> commands;
+#define YYLTYPE_IS_TRIVIAL 1
+#define YYMAXDEPTH 104857600
+#define YYERROR_VERBOSE 1
+#define YY_EXIT_FAILURE -1
+#define YYPARSE_PARAM AssertsQuery
+ %}
+
+%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 an_terms
+
+%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 <str> BVCONST_TOK
+%token <node> BITCONST_TOK
+%token <node> FORMID_TOK TERMID_TOK
+%token <str> STRING_TOK
+%token <str> USER_VAL_TOK
+
+ /* set-info tokens */
+%token SOURCE_TOK
+%token CATEGORY_TOK
+%token DIFFICULTY_TOK
+%token VERSION_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 ASSUMPTION_TOK
+%token FORMULA_TOK
+%token STATUS_TOK
+%token BENCHMARK_TOK
+%token EXTRASORTS_TOK
+%token DECLARE_FUNCTION_TOK
+%token EXTRAPREDS_TOK
+%token LANGUAGE_TOK
+
+ /* ASCII Symbols */
+%token DOLLAR_TOK
+%token QUESTION_TOK
+%token SEMICOLON_TOK
+%token UNDERSCORE_TOK
+%token PIPE_TOK
+%token DOT_TOK
+%token COLON_TOK
+%token LBRACKET_TOK
+%token RBRACKET_TOK
+%token LPAREN_TOK
+%token RPAREN_TOK
+
+ /* Status */
+%token SAT_TOK
+%token UNSAT_TOK
+%token UNKNOWN_TOK
+
+ /*BV SPECIFIC TOKENS*/
+%token BVLEFTSHIFT_1_TOK
+%token BVRIGHTSHIFT_1_TOK
+%token BVARITHRIGHTSHIFT_TOK
+%token BVPLUS_TOK
+%token BVSUB_TOK
+%token BVNOT_TOK //bvneg in CVCL
+%token BVMULT_TOK
+%token BVDIV_TOK
+%token SBVDIV_TOK
+%token BVMOD_TOK
+%token SBVREM_TOK
+%token SBVMOD_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 BVEXTRACT_TOK
+%token BVZX_TOK
+%token BVROTATE_RIGHT_TOK
+%token BVROTATE_LEFT_TOK
+%token BVREPEAT_TOK
+%token BVCOMP_TOK
+
+ /* Types for QF_BV and QF_AUFBV. */
+%token BITVEC_TOK
+%token ARRAY_TOK
+%token BOOL_TOK
+
+/* CORE THEORY pg. 29 of the SMT-LIB2 standard 30-March-2010. */
+%token TRUE_TOK;
+%token FALSE_TOK;
+%token NOT_TOK;
+%token AND_TOK;
+%token OR_TOK;
+%token XOR_TOK;
+%token ITE_TOK;
+%token EQ_TOK;
+%token IMPLIES_TOK;
+
+ /* CORE THEORY. But not on pg 29. */
+%token DISTINCT_TOK;
+%token LET_TOK;
+
+// COMMANDS
+%token EXIT_TOK
+%token CHECK_SAT_TOK
+
+%left LBRACKET_TOK RBRACKET_TOK
+
+ /* Functions for QF_AUFBV. */
+%token SELECT_TOK;
+%token STORE_TOK;
+
+
+%%
+cmd: commands
+{
+ if(querysmt2.IsNull())
+ {
+ querysmt2 = parserInterface->CreateNode(FALSE);
+ }
+
+ ((ASTVec*)AssertsQuery)->push_back(parserInterface->nf->CreateNode(AND,assertionsSMT2));
+ ((ASTVec*)AssertsQuery)->push_back(querysmt2);
+ parserInterface->letMgr.cleanupParserSymbolTable();
+ YYACCEPT;
+}
+;
+
+
+commands: cmdi commands
+| cmdi
+{}
+;
+
+cmdi:
+ LPAREN_TOK EXIT_TOK RPAREN_TOK
+ {
+ commands.push_back("exit");
+ }
+| LPAREN_TOK CHECK_SAT_TOK RPAREN_TOK
+ {
+ commands.push_back("check-sat");
+ }
+|
+ LPAREN_TOK LOGIC_TOK logic_name RPAREN_TOK
+ {
+ if (!(0 == strcmp($3->GetName(),"QF_BV") ||
+ 0 == strcmp($3->GetName(),"QF_AUFBV"))) {
+ yyerror("Wrong input logic:");
+ }
+ delete $3;
+ }
+| LPAREN_TOK NOTES_TOK attribute user_value RPAREN_TOK
+ {}
+| LPAREN_TOK NOTES_TOK attribute FORMID_TOK RPAREN_TOK
+ {}
+| LPAREN_TOK NOTES_TOK attribute NUMERAL_TOK DOT_TOK NUMERAL_TOK RPAREN_TOK
+ {}
+| LPAREN_TOK NOTES_TOK attribute STRING_TOK RPAREN_TOK
+ {}
+| LPAREN_TOK NOTES_TOK attribute RPAREN_TOK
+ {}
+| LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK
+ {}
+| LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK
+ {
+ assertionsSMT2.push_back(*$3);
+ }
+|
+benchmark
+{
+ ASTNode assumptions;
+ if($1 == NULL)
+ {
+ assumptions = parserInterface->CreateNode(TRUE);
+ }
+ else
+ {
+ assumptions = *$1;
+ }
+}
+;
+
+benchmark:
+LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
+{
+ if($4 != NULL){
+ if($4->size() > 1)
+ $$ = new ASTNode(parserInterface->nf->CreateNode(AND,*$4));
+ else
+ $$ = new ASTNode((*$4)[0]);
+ delete $4;
+ }
+ else {
+ $$ = NULL;
+ }
+ delete $3; //discard the benchmarkname.
+}
+;
+
+bench_name:
+FORMID_TOK
+{
+}
+;
+
+bench_attributes:
+bench_attribute
+{
+ $$ = new ASTVec;
+ if ($1 != NULL) {
+ $$->push_back(*$1);
+ parserInterface->AddAssert(*$1);
+ delete $1;
+ }
+}
+| bench_attributes bench_attribute
+{
+ if ($1 != NULL && $2 != NULL) {
+ $1->push_back(*$2);
+ parserInterface->AddAssert(*$2);
+ $$ = $1;
+ delete $2;
+ }
+}
+;
+
+bench_attribute:
+COLON_TOK ASSUMPTION_TOK an_formula
+{
+ //assumptions are like asserts
+ $$ = $3;
+}
+| COLON_TOK FORMULA_TOK an_formula
+{
+ // Previously this would call AddQuery() on the negation.
+ // But if multiple formula were (eroneously) present
+ // it discarded all but the last formula. Allowing multiple
+ // formula and taking the conjunction of them along with all
+ // the assumptions is what the other solvers do.
+
+ //assumptions are like asserts
+ $$ = $3;
+}
+
+| COLON_TOK EXTRAPREDS_TOK LPAREN_TOK var_decls RPAREN_TOK
+{
+ $$ = NULL;
+}
+| annotation
+{
+ $$ = NULL;
+}
+;
+
+logic_name:
+FORMID_TOK
+{
+ $$ = $1;
+}
+;
+
+status:
+SAT_TOK {
+ input_status = TO_BE_SATISFIABLE;
+ $$ = NULL;
+}
+| UNSAT_TOK {
+ input_status = TO_BE_UNSATISFIABLE;
+ $$ = NULL;
+ }
+| UNKNOWN_TOK
+{
+ input_status = TO_BE_UNKNOWN;
+ $$ = NULL;
+}
+;
+
+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
+{}
+| COLON_TOK VERSION_TOK
+{}
+| COLON_TOK STATUS_TOK status
+{}
+;
+
+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
+{
+}
+|
+var_decls var_decl
+{
+}
+;
+
+var_decl:
+FORMID_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK
+{
+ parserInterface->letMgr._parser_symbol_table.insert(*$1);
+ //Sort_symbs has the indexwidth/valuewidth. Set those fields in
+ //var
+ $1->SetIndexWidth(0);
+ $1->SetValueWidth($7);
+ delete $1;
+}
+| FORMID_TOK LPAREN_TOK RPAREN_TOK BOOL_TOK
+{
+ $1->SetIndexWidth(0);
+ $1->SetValueWidth(0);
+ parserInterface->letMgr._parser_symbol_table.insert(*$1);
+ //Sort_symbs has the indexwidth/valuewidth. Set those fields in
+ //var
+ //delete $2;
+}
+| LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK
+{
+ parserInterface->letMgr._parser_symbol_table.insert(*$2);
+ //Sort_symbs has the indexwidth/valuewidth. Set those fields in
+ //var
+ $2->SetIndexWidth($3.indexwidth);
+ $2->SetValueWidth($3.valuewidth);
+ delete $2;
+}
+| FORMID_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK ARRAY_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK RPAREN_TOK
+{
+ parserInterface->letMgr._parser_symbol_table.insert(*$1);
+ unsigned int index_len = $9;
+ unsigned int value_len = $14;
+ if(index_len > 0) {
+ $1->SetIndexWidth($9);
+ }
+ else {
+ FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n");
+ }
+
+ if(value_len > 0) {
+ $1->SetValueWidth($14);
+ }
+ else {
+ FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n");
+ }
+}
+
+;
+
+an_formulas:
+an_formula
+{
+ $$ = new 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 ASTNode(parserInterface->CreateNode(TRUE));
+ assert(0 == $$->GetIndexWidth());
+ assert(0 == $$->GetValueWidth());
+}
+| FALSE_TOK
+{
+ $$ = new ASTNode(parserInterface->CreateNode(FALSE));
+ assert(0 == $$->GetIndexWidth());
+ assert(0 == $$->GetValueWidth());
+}
+| fvar
+{
+ $$ = $1;
+}
+| LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(EQ,*$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK
+{
+ using namespace BEEV;
+
+ ASTVec terms = *$3;
+ ASTVec forms;
+
+ for(ASTVec::const_iterator it=terms.begin(),itend=terms.end();
+ it!=itend; it++) {
+ for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) {
+ ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->nf->CreateNode(EQ, *it, *it2)));
+
+
+ forms.push_back(n);
+ }
+ }
+
+ if(forms.size() == 0)
+ FatalError("empty distinct");
+
+ $$ = (forms.size() == 1) ?
+ new ASTNode(forms[0]) :
+ new ASTNode(parserInterface->nf->CreateNode(AND, forms));
+
+ delete $3;
+}
+
+| LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSLT, *$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSLE, *$3, *$4));
+ $$ = 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
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSGT, *$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSGE, *$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVLT, *$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVLE, *$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVGT, *$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK
+{
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVGE, *$3, *$4));
+ $$ = n;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK an_formula RPAREN_TOK
+{
+ $$ = $2;
+}
+| LPAREN_TOK NOT_TOK an_formula RPAREN_TOK
+{
+ $$ = new ASTNode(parserInterface->nf->CreateNode(NOT, *$3));
+ delete $3;
+}
+| LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
+{
+ $$ = new ASTNode(parserInterface->nf->CreateNode(IMPLIES, *$3, *$4));
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK ITE_TOK an_formula an_formula an_formula RPAREN_TOK
+{
+ $$ = new ASTNode(parserInterface->nf->CreateNode(ITE, *$3, *$4, *$5));
+ delete $3;
+ delete $4;
+ delete $5;
+}
+| LPAREN_TOK AND_TOK an_formulas RPAREN_TOK
+{
+ $$ = new ASTNode(parserInterface->nf->CreateNode(AND, *$3));
+ delete $3;
+}
+| LPAREN_TOK OR_TOK an_formulas RPAREN_TOK
+{
+ $$ = new ASTNode(parserInterface->nf->CreateNode(OR, *$3));
+ delete $3;
+}
+| LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
+{
+ $$ = new ASTNode(parserInterface->nf->CreateNode(XOR, *$3, *$4));
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK EQ_TOK an_formula an_formula RPAREN_TOK
+{
+ $$ = new ASTNode(parserInterface->nf->CreateNode(IFF, *$3, *$4));
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK LET_TOK LPAREN_TOK lets RPAREN_TOK an_formula RPAREN_TOK
+{
+ $$ = $6;
+ //Cleanup the LetIDToExprMap
+ parserInterface->letMgr.CleanupLetIDMap();
+}
+;
+
+lets: let lets
+| let
+{};
+
+let: LPAREN_TOK QUESTION_TOK FORMID_TOK an_formula RPAREN_TOK
+{
+ //set the valuewidth of the identifier
+ $3->SetValueWidth($4->GetValueWidth());
+ $3->SetIndexWidth($4->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
+ parserInterface->letMgr.LetExprMgr(*$3,*$4);
+
+ //delete $5;
+ //delete $6;
+}
+| LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK
+{
+ //set the valuewidth of the identifier
+ $3->SetValueWidth($4->GetValueWidth());
+ $3->SetIndexWidth($4->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
+ parserInterface->letMgr.LetExprMgr(*$3,*$4);
+
+ //delete $5;
+ //delete $6;
+}
+;
+
+
+
+an_terms:
+an_term
+{
+ $$ = new ASTVec;
+ if ($1 != NULL) {
+ $$->push_back(*$1);
+ delete $1;
+ }
+}
+|
+an_terms an_term
+{
+ if ($1 != NULL && $2 != NULL) {
+ $1->push_back(*$2);
+ $$ = $1;
+ delete $2;
+ }
+}
+;
+
+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
+{
+ $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
+ delete $1;
+}
+| LPAREN_TOK an_term RPAREN_TOK
+ //| LPAREN_TOK an_term annotations RPAREN_TOK
+{
+ $$ = $2;
+ //$$ = new ASTNode(parserInterface->SimplifyTerm(*$2));
+ //delete $2;
+}
+| SELECT_TOK an_term an_term
+{
+ //ARRAY READ
+ // valuewidth is same as array, indexwidth is 0.
+ ASTNode array = *$2;
+ ASTNode index = *$3;
+ unsigned int width = array.GetValueWidth();
+ ASTNode * n =
+ new ASTNode(parserInterface->nf->CreateTerm(READ, width, array, index));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| STORE_TOK an_term an_term an_term
+{
+ //ARRAY WRITE
+ unsigned int width = $4->GetValueWidth();
+ ASTNode array = *$2;
+ ASTNode index = *$3;
+ ASTNode writeval = *$4;
+ ASTNode write_term = parserInterface->nf->CreateArrayTerm(WRITE,$2->GetIndexWidth(),width,array,index,writeval);
+ ASTNode * n = new ASTNode(write_term);
+ $$ = n;
+ delete $2;
+ delete $3;
+ delete $4;
+}
+| LPAREN_TOK UNDERSCORE_TOK BVEXTRACT_TOK NUMERAL_TOK NUMERAL_TOK RPAREN_TOK an_term
+{
+ int width = $4 - $5 + 1;
+ if (width < 0)
+ yyerror("Negative width in extract");
+
+ if((unsigned)$4 >= $7->GetValueWidth())
+ yyerror("Parsing: Wrong width in BVEXTRACT\n");
+
+ ASTNode hi = parserInterface->CreateBVConst(32, $4);
+ ASTNode low = parserInterface->CreateBVConst(32, $5);
+ ASTNode output = parserInterface->nf->CreateTerm(BVEXTRACT, width, *$7,hi,low);
+ ASTNode * n = new ASTNode(output);
+ $$ = n;
+ //delete $7;
+}
+| LPAREN_TOK UNDERSCORE_TOK BVZX_TOK NUMERAL_TOK RPAREN_TOK an_term
+{
+ if (0 != $4)
+ {
+ unsigned w = $6->GetValueWidth() + $4;
+ ASTNode leading_zeroes = parserInterface->CreateZeroConst($4);
+ ASTNode *n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,w,leading_zeroes,*$6));
+ $$ = n;
+ //delete $5;
+ }
+ else
+ $$ = $6;
+}
+| LPAREN_TOK UNDERSCORE_TOK BVSX_TOK NUMERAL_TOK RPAREN_TOK an_term
+{
+ unsigned w = $6->GetValueWidth() + $4;
+ ASTNode width = parserInterface->CreateBVConst(32,w);
+ ASTNode *n = new ASTNode(parserInterface->nf->CreateTerm(BVSX,w,*$6,width));
+ $$ = n;
+ //delete $5;
+}
+
+| ITE_TOK an_formula an_term an_term
+{
+ const unsigned int width = $3->GetValueWidth();
+ $$ = new ASTNode(parserInterface->nf->CreateArrayTerm(ITE,$4->GetIndexWidth(), width,*$2, *$3, *$4));
+ delete $2;
+ delete $3;
+ delete $4;
+}
+| BVCONCAT_TOK an_term an_term
+{
+ const unsigned int width = $2->GetValueWidth() + $3->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVNOT_TOK an_term
+{
+ //this is the BVNEG (term) in the CVCL language
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, *$2));
+ $$ = n;
+ delete $2;
+}
+| BVNEG_TOK an_term
+{
+ //this is the BVUMINUS term in CVCL langauge
+ unsigned width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVUMINUS,width,*$2));
+ $$ = n;
+ delete $2;
+}
+| BVAND_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVOR_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVXOR_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVXOR, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+ | BVXNOR_TOK an_term an_term
+ {
+// (bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t)))
+
+
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(
+ parserInterface->nf->CreateTerm( BVOR, width,
+ parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3),
+ parserInterface->nf->CreateTerm(BVAND, width,
+ parserInterface->nf->CreateTerm(BVNEG, width, *$2),
+ parserInterface->nf->CreateTerm(BVNEG, width, *$3)
+ )));
+
+ $$ = n;
+ delete $2;
+ delete $3;
+
+ }
+ | BVCOMP_TOK an_term an_term
+ {
+
+
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(ITE, 1,
+ parserInterface->nf->CreateNode(EQ, *$2, *$3),
+ parserInterface->CreateOneConst(1),
+ parserInterface->CreateZeroConst(1)));
+
+ $$ = n;
+ delete $2;
+ delete $3;
+ }
+
+
+| BVSUB_TOK an_term an_term
+{
+ const unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSUB, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVPLUS_TOK an_term an_term
+{
+ const unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVPLUS, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+
+}
+| BVMULT_TOK an_term an_term
+{
+ const unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMULT, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+
+| BVDIV_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVDIV, width, *$2, *$3));
+ $$ = n;
+
+ delete $2;
+ delete $3;
+}
+| BVMOD_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMOD, width, *$2, *$3));
+ $$ = n;
+
+ delete $2;
+ delete $3;
+}
+| SBVDIV_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVDIV, width, *$2, *$3));
+ $$ = n;
+
+ delete $2;
+ delete $3;
+}
+| SBVREM_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVREM, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| SBVMOD_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVMOD, width, *$2, *$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVNAND_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3)));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVNOR_TOK an_term an_term
+{
+ unsigned int width = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3)));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVLEFTSHIFT_1_TOK an_term an_term
+{
+ // shifting left by who know how much?
+ unsigned int w = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVLEFTSHIFT,w,*$2,*$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVRIGHTSHIFT_1_TOK an_term an_term
+{
+ // shifting right by who know how much?
+ unsigned int w = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| BVARITHRIGHTSHIFT_TOK an_term an_term
+{
+ // shifting arithmetic right by who know how much?
+ unsigned int w = $2->GetValueWidth();
+ ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSRSHIFT,w,*$2,*$3));
+ $$ = n;
+ delete $2;
+ delete $3;
+}
+| LPAREN_TOK UNDERSCORE_TOK BVROTATE_LEFT_TOK NUMERAL_TOK RPAREN_TOK an_term
+{
+
+ ASTNode *n;
+ unsigned width = $6->GetValueWidth();
+ unsigned rotate = $4;
+ if (0 == rotate)
+ {
+ n = $6;
+ }
+ else if (rotate < width)
+ {
+ ASTNode high = parserInterface->CreateBVConst(32,width-1);
+ ASTNode zero = parserInterface->CreateBVConst(32,0);
+ ASTNode cut = parserInterface->CreateBVConst(32,width-rotate);
+ ASTNode cutMinusOne = parserInterface->CreateBVConst(32,width-rotate-1);
+
+ ASTNode top = parserInterface->nf->CreateTerm(BVEXTRACT,rotate,*$6,high, cut);
+ ASTNode bottom = parserInterface->nf->CreateTerm(BVEXTRACT,width-rotate,*$6,cutMinusOne,zero);
+ n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top));
+ delete $6;
+ }
+ else
+ {
+ n = NULL; // remove gcc warning.
+ yyerror("Rotate must be strictly less than the width.");
+ }
+
+ $$ = n;
+
+}
+| LPAREN_TOK UNDERSCORE_TOK BVROTATE_RIGHT_TOK NUMERAL_TOK RPAREN_TOK an_term
+{
+
+ ASTNode *n;
+ unsigned width = $6->GetValueWidth();
+ unsigned rotate = $4;
+ if (0 == rotate)
+ {
+ n = $6;
+ }
+ else if (rotate < width)
+ {
+ ASTNode high = parserInterface->CreateBVConst(32,width-1);
+ ASTNode zero = parserInterface->CreateBVConst(32,0);
+ ASTNode cut = parserInterface->CreateBVConst(32,rotate);
+ ASTNode cutMinusOne = parserInterface->CreateBVConst(32,rotate-1);
+
+ ASTNode bottom = parserInterface->nf->CreateTerm(BVEXTRACT,rotate,*$6,cutMinusOne, zero);
+ ASTNode top = parserInterface->nf->CreateTerm(BVEXTRACT,width-rotate,*$6,high,cut);
+ n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top));
+ delete $6;
+ }
+ else
+ {
+ n = NULL; // remove gcc warning.
+ yyerror("Rotate must be strictly less than the width.");
+ }
+
+ $$ = n;
+
+}
+ | BVREPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term
+ {
+ unsigned count = $3;
+ if (count < 1)
+ FatalError("One or more repeats please");
+
+ unsigned w = $5->GetValueWidth();
+ ASTNode n = *$5;
+
+ for (unsigned i =1; i < count; i++)
+ {
+ n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$5);
+ }
+ $$ = new ASTNode(n);
+ }
+| UNDERSCORE_TOK BVCONST_TOK NUMERAL_TOK
+{
+ $$ = new ASTNode(parserInterface->CreateBVConst($2, 10, $3));
+ $$->SetValueWidth($3);
+}
+;
+
+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 {
+ FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n");
+ }
+}
+;
+
+var:
+TERMID_TOK
+{
+ $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
+ delete $1;
+}
+| QUESTION_TOK TERMID_TOK
+{
+ $$ = $2;
+}
+;
+
+fvar:
+DOLLAR_TOK FORMID_TOK
+{
+ $$ = $2;
+}
+| FORMID_TOK
+{
+ $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
+ delete $1;
+}
+| QUESTION_TOK FORMID_TOK
+{
+ $$ = $2;
+}
+;
+%%
projects / francis / stp.git / commitdiff