From bdbd94fb1bd6a16a6cacc1246c8dd6d18aead213 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 4 Sep 2009 23:47:29 +0000 Subject: [PATCH] Major code refactoring. Moved main.cpp to main. Globals to Globals.cpp. Also made the parser return an actual object for the AST git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@187 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile | 8 +- scripts/Makefile.in | 8 +- src/AST/AST.cpp | 69 +----- src/AST/AST.h | 58 ++--- src/AST/ASTUtil.cpp | 1 + src/AST/ASTUtil.h | 54 ----- src/AST/AbstractionRefinement.cpp | 174 +++++++------- src/AST/ToCNF.cpp | 10 +- src/AST/ToSAT.cpp | 14 +- src/AST/Transform.cpp | 4 +- src/AST/printer/AssortedPrinters.cpp | 9 +- src/c_interface/c_interface.cpp | 4 +- src/main/Globals.cpp | 75 ++++++ src/main/Globals.h | 114 +++++++++ src/main/Makefile | 13 + src/main/main.cpp | 186 ++++++++++++++ src/parser/CVC.lex | 21 +- src/parser/CVC.y | 344 +++++++++++++------------- src/parser/Makefile | 13 +- src/parser/main.cpp | 212 ---------------- src/parser/smtlib.lex | 26 +- src/parser/smtlib.y | 347 ++++++++++++++------------- 22 files changed, 916 insertions(+), 848 deletions(-) create mode 100644 src/main/Globals.cpp create mode 100644 src/main/Globals.h create mode 100644 src/main/Makefile create mode 100644 src/main/main.cpp delete mode 100644 src/parser/main.cpp diff --git a/Makefile b/Makefile index 445fda2..1f769ca 100644 --- a/Makefile +++ b/Makefile @@ -26,8 +26,9 @@ all: $(MAKE) -C $(SRC)/c_interface $(MAKE) -C $(SRC)/constantbv $(MAKE) -C $(SRC)/parser + $(MAKE) -C $(SRC)/main $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \ - $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o + $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o $(RANLIB) libstp.a @mkdir -p lib @mv libstp.a lib/ @@ -52,16 +53,15 @@ clean: rm -rf bin/*~ rm -rf bin/stp rm -rf *.log - #rm -rf Makefile - #rm -rf config.info rm -f TAGS $(MAKE) clean -C $(SRC)/AST $(MAKE) clean -C $(SRC)/sat $(MAKE) clean -C $(SRC)/simplifier $(MAKE) clean -C $(SRC)/bitvec - $(MAKE) clean -C $(SRC)/parser $(MAKE) clean -C $(SRC)/c_interface $(MAKE) clean -C $(SRC)/constantbv + $(MAKE) clean -C $(SRC)/parser + $(MAKE) clean -C $(SRC)/main # this is make way too difficult because of the recursive Make junk, it # should be removed diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 445fda2..1f769ca 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -26,8 +26,9 @@ all: $(MAKE) -C $(SRC)/c_interface $(MAKE) -C $(SRC)/constantbv $(MAKE) -C $(SRC)/parser + $(MAKE) -C $(SRC)/main $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \ - $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o + $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o $(RANLIB) libstp.a @mkdir -p lib @mv libstp.a lib/ @@ -52,16 +53,15 @@ clean: rm -rf bin/*~ rm -rf bin/stp rm -rf *.log - #rm -rf Makefile - #rm -rf config.info rm -f TAGS $(MAKE) clean -C $(SRC)/AST $(MAKE) clean -C $(SRC)/sat $(MAKE) clean -C $(SRC)/simplifier $(MAKE) clean -C $(SRC)/bitvec - $(MAKE) clean -C $(SRC)/parser $(MAKE) clean -C $(SRC)/c_interface $(MAKE) clean -C $(SRC)/constantbv + $(MAKE) clean -C $(SRC)/parser + $(MAKE) clean -C $(SRC)/main # this is make way too difficult because of the recursive Make junk, it # should be removed diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 4f2e38f..c4d3ab6 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -8,69 +8,12 @@ // -*- c++ -*- #include "AST.h" - #include #include "printer/printers.h" #include "printer/AssortedPrinters.h" namespace BEEV { - //some global variables that are set through commandline options. it - //is best that these variables remain global. Default values set - //here - // - //collect statistics on certain functions - bool stats_flag = false; - //print DAG nodes - bool print_nodes_flag = false; - //run STP in optimized mode - bool optimize_flag = true; - //do sat refinement, i.e. underconstraint the problem, and feed to - //SAT. if this works, great. else, add a set of suitable constraints - //to re-constraint the problem correctly, and call SAT again, until - //all constraints have been added. - bool arrayread_refinement_flag = true; - //flag to control write refinement - bool arraywrite_refinement_flag = true; - //check the counterexample against the original input to STP - bool check_counterexample_flag = false; - //construct the counterexample in terms of original variable based - //on the counterexample returned by SAT solver - bool construct_counterexample_flag = true; - bool print_counterexample_flag = false; - bool print_binary_flag = false; - //if this option is true then print the way dawson wants using a - //different printer. do not use this printer. - bool print_arrayval_declaredorder_flag = false; - //flag to decide whether to print "valid/invalid" or not - bool print_output_flag = false; - //print the variable order chosen by the sat solver while it is - //solving. - bool print_sat_varorder_flag = false; - //turn on word level bitvector solver - bool wordlevel_solve_flag = true; - //turn off XOR flattening - bool xor_flatten_flag = false; - //Flag to switch on the smtlib parser - bool smtlib_parser_flag = false; - //print the input back - bool print_STPinput_back_flag = false; - - // If enabled. division, mod and remainder by zero will evaluate to 1. - bool division_by_zero_returns_one = false; - - enum inputStatus input_status = NOT_DECLARED; - - // Used only in smtlib lexer/parser - ASTNode SingleBitOne; - ASTNode SingleBitZero; - - //global BEEVMGR for the parser - BeevMgr * globalBeevMgr_for_parser; - - void (*vc_error_hdlr)(const char* err_msg) = NULL; - /** This is reusable empty vector, for representing empty children arrays */ - ASTVec _empty_ASTVec; //////////////////////////////////////////////////////////////// // ASTInternal members //////////////////////////////////////////////////////////////// @@ -1249,12 +1192,12 @@ namespace BEEV bool isAtomic(Kind kind) { if (TRUE == kind || FALSE == kind || - EQ == kind || - BVLT == kind || BVLE == kind || - BVGT == kind || BVGE == kind || - BVSLT == kind || BVSLE == kind || - BVSGT == kind || BVSGE == kind || - SYMBOL == kind || BVGETBIT == kind) + EQ == kind || + BVLT == kind || BVLE == kind || + BVGT == kind || BVGE == kind || + BVSLT == kind || BVSLE == kind || + BVSGT == kind || BVSGE == kind || + SYMBOL == kind || BVGETBIT == kind) return true; return false; } diff --git a/src/AST/AST.h b/src/AST/AST.h index 8cf5cbe..dd44d27 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -30,18 +30,13 @@ #include #include #include +#include "../main/Globals.h" #include "ASTUtil.h" #include "ASTKind.h" #include #include #include "../constantbv/constantbv.h" -namespace MINISAT -{ - class Solver; - typedef int Var; -} - /***************************************************************************** * LIST OF CLASSES DECLARED IN THIS FILE: * @@ -60,18 +55,6 @@ namespace BEEV using namespace __gnu_cxx; #endif - //return types for the GetType() function in ASTNode class - enum types - { - BOOLEAN_TYPE = 0, BITVECTOR_TYPE, ARRAY_TYPE, UNKNOWN_TYPE - }; - - enum SOLVER_RETURN_TYPE - { - SOLVER_INVALID=0, SOLVER_VALID=1, SOLVER_UNDECIDED=2, SOLVER_ERROR=-100 - }; - - class BeevMgr; class ASTNode; class ASTInternal; @@ -80,12 +63,11 @@ namespace BEEV class ASTBVConst; class BVSolver; - //Vector of ASTNodes, used for child nodes among other things. + //Useful typedefs: Vector of ASTNodes, used for child nodes among + //other things. typedef vector ASTVec; typedef unsigned int * CBV; extern ASTVec _empty_ASTVec; - extern BeevMgr * globalBeevMgr_for_parser; - /***************************************************************************/ /* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */ /***************************************************************************/ @@ -462,13 +444,15 @@ namespace BEEV // Constructor (bm only) ASTInternal(BeevMgr &bm, int nodenum = 0) : - _ref_count(0), _kind(UNDEFINED), _bm(bm), _node_num(nodenum), _index_width(0), _value_width(0) + _ref_count(0), _kind(UNDEFINED), _bm(bm), + _node_num(nodenum), _index_width(0), _value_width(0) { } // Constructor (kind only, empty children, int nodenum) ASTInternal(Kind kind, BeevMgr &bm, int nodenum = 0) : - _ref_count(0), _kind(kind), _bm(bm), _node_num(nodenum), _index_width(0), _value_width(0) + _ref_count(0), _kind(kind), _bm(bm), + _node_num(nodenum), _index_width(0), _value_width(0) { } @@ -476,7 +460,8 @@ namespace BEEV // the child nodes. // FIXME: is there a way to avoid repeating these? ASTInternal(Kind kind, const ASTVec &children, BeevMgr &bm, int nodenum = 0) : - _ref_count(0), _kind(kind), _children(children), _bm(bm), _node_num(nodenum), _index_width(0), _value_width(0) + _ref_count(0), _kind(kind), _children(children), + _bm(bm), _node_num(nodenum), _index_width(0), _value_width(0) { } @@ -486,8 +471,10 @@ namespace BEEV // temporary hash keys before uniquefication. // FIXME: I don't think children need to be copied. ASTInternal(const ASTInternal &int_node, int nodenum = 0) : - _ref_count(0), _kind(int_node._kind), _children(int_node._children), _bm(int_node._bm), _node_num(int_node._node_num), _index_width( - int_node._index_width), _value_width(int_node._value_width) + _ref_count(0), _kind(int_node._kind), + _children(int_node._children), _bm(int_node._bm), + _node_num(int_node._node_num), _index_width(int_node._index_width), + _value_width(int_node._value_width) { } @@ -1409,7 +1396,9 @@ namespace BEEV * BVGETBIT Node), and this maps allows us to assemble the bits * into bitvectors. */ - typedef hash_map *, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTtoBitvectorMap; + typedef hash_map *, + ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTtoBitvectorMap; ASTtoBitvectorMap _ASTNode_to_Bitvector; //Data structure that holds the counter-model @@ -1597,11 +1586,16 @@ namespace BEEV // Constructor BeevMgr() : - _interior_unique_table(INITIAL_INTERIOR_UNIQUE_TABLE_SIZE), _symbol_unique_table(INITIAL_SYMBOL_UNIQUE_TABLE_SIZE), _bvconst_unique_table( - INITIAL_BVCONST_UNIQUE_TABLE_SIZE), BBTermMemo(INITIAL_BBTERM_MEMO_TABLE_SIZE), BBFormMemo(INITIAL_BBFORM_MEMO_TABLE_SIZE), - _max_node_num(0), ASTFalse(CreateNode(FALSE)), ASTTrue(CreateNode(TRUE)), ASTUndefined(CreateNode(UNDEFINED)), SolverMap( - INITIAL_SOLVER_MAP_SIZE), _arrayread_symbol(INITIAL_ARRAYREAD_SYMBOL_SIZE), _introduced_symbols( - INITIAL_INTRODUCED_SYMBOLS_SIZE), _symbol_count(0) + _interior_unique_table(INITIAL_INTERIOR_UNIQUE_TABLE_SIZE), + _symbol_unique_table(INITIAL_SYMBOL_UNIQUE_TABLE_SIZE), + _bvconst_unique_table(INITIAL_BVCONST_UNIQUE_TABLE_SIZE), + BBTermMemo(INITIAL_BBTERM_MEMO_TABLE_SIZE), + BBFormMemo(INITIAL_BBFORM_MEMO_TABLE_SIZE), + _max_node_num(0), ASTFalse(CreateNode(FALSE)), + ASTTrue(CreateNode(TRUE)), ASTUndefined(CreateNode(UNDEFINED)), + SolverMap(INITIAL_SOLVER_MAP_SIZE), + _arrayread_symbol(INITIAL_ARRAYREAD_SYMBOL_SIZE), + _introduced_symbols(INITIAL_INTRODUCED_SYMBOLS_SIZE), _symbol_count(0) { _current_query = ASTUndefined; ValidFlag = false; diff --git a/src/AST/ASTUtil.cpp b/src/AST/ASTUtil.cpp index c860d5c..48e32f7 100644 --- a/src/AST/ASTUtil.cpp +++ b/src/AST/ASTUtil.cpp @@ -8,6 +8,7 @@ // -*- c++ -*- #include "ASTUtil.h" +#include "../main/Globals.h" namespace BEEV { ostream &operator<<(ostream &os, const Spacer &sp) diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h index 41f50d1..a705cc1 100644 --- a/src/AST/ASTUtil.h +++ b/src/AST/ASTUtil.h @@ -30,60 +30,6 @@ namespace BEEV { #ifdef EXT_HASH_MAP using namespace __gnu_cxx; #endif - //some global variables that are set through commandline options. it - //is best that these variables remain global. Default values set - //here - // - //collect statistics on certain functions - extern bool stats_flag; - //print DAG nodes - extern bool print_nodes_flag; - //run STP in optimized mode - extern bool optimize_flag; - //do sat refinement, i.e. underconstraint the problem, and feed to - //SAT. if this works, great. else, add a set of suitable constraints - //to re-constraint the problem correctly, and call SAT again, until - //all constraints have been added. - extern bool arrayread_refinement_flag; - //switch to control write refinements - extern bool arraywrite_refinement_flag; - //check the counterexample against the original input to STP - extern bool check_counterexample_flag; - //construct the counterexample in terms of original variable based - //on the counterexample returned by SAT solver - extern bool construct_counterexample_flag; - extern bool print_counterexample_flag; - extern bool print_binary_flag; - //if this option is true then print the way dawson wants using a - //different printer. do not use this printer. - extern bool print_arrayval_declaredorder_flag; - //flag to decide whether to print "valid/invalid" or not - extern bool print_output_flag; - //print the variable order chosen by the sat solver while it is - //solving. - extern bool print_sat_varorder_flag; - //turn on word level bitvector solver - extern bool wordlevel_solve_flag; - //XOR flattening optimizations. - extern bool xor_flatten_flag; - //this flag indicates that the BVSolver() succeeded - extern bool toplevel_solved_flag; - //print the input back - extern bool print_STPinput_back_flag; - //Flag to switch on the smtlib parser - extern bool smtlib_parser_flag; - - extern bool division_by_zero_returns_one; - - enum inputStatus - { - NOT_DECLARED =0, // Not included in the input file / stream - TO_BE_SATISFIABLE, - TO_BE_UNSATISFIABLE, - TO_BE_UNKNOWN // Specified in the input file as unknown. - }; - - extern enum inputStatus input_status; extern void (*vc_error_hdlr)(const char* err_msg); /*Spacer class is basically just an int, but the new class allows diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp index aae3646..df86ac4 100644 --- a/src/AST/AbstractionRefinement.cpp +++ b/src/AST/AbstractionRefinement.cpp @@ -19,8 +19,8 @@ namespace BEEV //FIXME: Write a detailed comment on how this actually works SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, - const ASTNode& inputAlreadyInSAT, - const ASTNode& original_input) { + const ASTNode& inputAlreadyInSAT, + const ASTNode& original_input) { //go over the list of indices for each array, and generate Leibnitz //axioms. Then assert these axioms into the SAT solver. Check if the //addition of the new constraints has made the bogus counterexample @@ -154,7 +154,7 @@ namespace BEEV //FIXME: Write a detailed comment on how this actually works SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + const ASTNode& original_input) { ASTNode writeAxiom; ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin(); @@ -214,7 +214,7 @@ namespace BEEV //Expands all finite-for-loops using counterexample-guided //abstraction-refinement. SOLVER_RETURN_TYPE BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + const ASTNode& original_input) { /* * For each 'finiteloop' in the global list 'List_Of_FiniteLoops' @@ -240,9 +240,9 @@ namespace BEEV //Expand the finite loop, check against model, and add false //formulas to the SAT solver SOLVER_RETURN_TYPE BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input, - const ASTNode& finiteloop, - ASTNodeMap* ParamToCurrentValMap) + const ASTNode& original_input, + const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap) { /* * 'finiteloop' is the finite loop to be expanded @@ -277,53 +277,53 @@ namespace BEEV //Go recursively thru' all the FOR-constructs. if(FOR == formulabody.GetKind()) { - while(paramCurrentValue < paramLimit) - { - SATBased_FiniteLoop_Refinement(SatSolver, original_input, - formulabody, ParamToCurrentValMap); - paramCurrentValue = paramCurrentValue + paramIncrement; + while(paramCurrentValue < paramLimit) + { + SATBased_FiniteLoop_Refinement(SatSolver, original_input, + formulabody, ParamToCurrentValMap); + paramCurrentValue = paramCurrentValue + paramIncrement; - //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); - } //end of While + //Update ParamToCurrentValMap with parameter and its current + //value + // + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + } //end of While } //end of recursion FORs ASTVec forloopFormulaVector; //Expand the leaf level FOR-construct completely for(; - paramCurrentValue < paramLimit; - paramCurrentValue = paramCurrentValue + paramIncrement) + paramCurrentValue < paramLimit; + paramCurrentValue = paramCurrentValue + paramIncrement) { - ASTNode currentFormula; - currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); - - //Check the currentformula against the model, and add it to the - //SAT solver if it is false against the model - if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) - { - forloopFormulaVector.push_back(currentFormula); - ASTNode forloopFormulas = - (forloopFormulaVector.size() != 1) ? - CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; - - SOLVER_RETURN_TYPE result = - CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input); - if(result != SOLVER_UNDECIDED) - { - return result; - } - } - - //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + ASTNode currentFormula; + currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); + + //Check the currentformula against the model, and add it to the + //SAT solver if it is false against the model + if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) + { + forloopFormulaVector.push_back(currentFormula); + ASTNode forloopFormulas = + (forloopFormulaVector.size() != 1) ? + CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; + + SOLVER_RETURN_TYPE result = + CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input); + if(result != SOLVER_UNDECIDED) + { + return result; + } + } + + //Update ParamToCurrentValMap with parameter and its current + //value + // + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); } //end of expanding the FOR loop return SOLVER_UNDECIDED; @@ -334,8 +334,8 @@ namespace BEEV //Expand the finite loop, check against model, and add false //formulas to the SAT solver ASTNode BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, - ASTNodeMap* ParamToCurrentValMap, - bool CheckUsingModel_Or_Expand = true) + ASTNodeMap* ParamToCurrentValMap, + bool CheckUsingModel_Or_Expand = true) { /* * 'finiteloop' is the finite loop to be expanded @@ -370,59 +370,59 @@ namespace BEEV //Go recursively thru' all the FOR-constructs. if(FOR == formulabody.GetKind()) { - while(paramCurrentValue < paramLimit) - { - Check_FiniteLoop_UsingModel(formulabody, - ParamToCurrentValMap, CheckUsingModel_Or_Expand); - paramCurrentValue = paramCurrentValue + paramIncrement; + while(paramCurrentValue < paramLimit) + { + Check_FiniteLoop_UsingModel(formulabody, + ParamToCurrentValMap, CheckUsingModel_Or_Expand); + paramCurrentValue = paramCurrentValue + paramIncrement; - //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); - } //end of While + //Update ParamToCurrentValMap with parameter and its current + //value + // + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + } //end of While } ASTVec forloopFormulaVector; //Expand the leaf level FOR-construct completely for(; - paramCurrentValue < paramLimit; - paramCurrentValue = paramCurrentValue + paramIncrement) + paramCurrentValue < paramLimit; + paramCurrentValue = paramCurrentValue + paramIncrement) { - ASTNode currentFormula; - currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); - - if(CheckUsingModel_Or_Expand) - { - //Check the currentformula against the model, and add it to the - //SAT solver if it is false against the model - if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) - return ASTFalse; - } - else - { - forloopFormulaVector.push_back(currentFormula); - } - - //Update ParamToCurrentValMap with parameter and its current - //value - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + ASTNode currentFormula; + currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); + + if(CheckUsingModel_Or_Expand) + { + //Check the currentformula against the model, and add it to the + //SAT solver if it is false against the model + if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) + return ASTFalse; + } + else + { + forloopFormulaVector.push_back(currentFormula); + } + + //Update ParamToCurrentValMap with parameter and its current + //value + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); } if(CheckUsingModel_Or_Expand) { - ASTNode retFormula = - (forloopFormulaVector.size() != 1) ? CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; - return retFormula; + ASTNode retFormula = + (forloopFormulaVector.size() != 1) ? CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; + return retFormula; } else { - return ASTTrue; + return ASTTrue; } } //end of the Check_FiniteLoop_UsingModel() diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp index 28d3440..bc1f99a 100644 --- a/src/AST/ToCNF.cpp +++ b/src/AST/ToCNF.cpp @@ -1776,15 +1776,15 @@ namespace BEEV //Call the SAT solver, and check the result before returning. This //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or SOLVER_UNDECIDED SOLVER_RETURN_TYPE BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input) + const ASTNode& modified_input, + const ASTNode& original_input) { ASTNode BBFormula = BBForm(modified_input); CNFMgr* cm = new CNFMgr(this); ClauseList* cl = cm->convertToCNF(BBFormula); if (stats_flag) { - cerr << "Number of clauses:" << cl->size() << endl; + cerr << "Number of clauses:" << cl->size() << endl; } //PrintClauseList(cout, *cl); bool sat = toSATandSolve(SatSolver, *cl); @@ -1811,7 +1811,7 @@ namespace BEEV ASTNode orig_result = ComputeFormulaUsingModel(original_input); if (!(ASTTrue == orig_result || ASTFalse == orig_result)) FatalError("TopLevelSat: Original input must compute to "\ - "true or false against model"); + "true or false against model"); // if the counterexample is indeed a good one, then return // invalid @@ -1840,7 +1840,7 @@ namespace BEEV } else { - //Control should never reach here + //Control should never reach here PrintOutput(true); return SOLVER_ERROR; } diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index 03fbeef..289d688 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -933,14 +933,14 @@ namespace BEEV { inputToSAT = simplified_solved_InputToSAT; simplified_solved_InputToSAT = - CreateSubstitutionMap(simplified_solved_InputToSAT); + CreateSubstitutionMap(simplified_solved_InputToSAT); //printf("##################################################\n"); ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = - SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); + SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = - bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); + bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); ASTNodeStats("after solving: ", simplified_solved_InputToSAT); } while (inputToSAT != simplified_solved_InputToSAT); @@ -953,13 +953,13 @@ namespace BEEV { inputToSAT = simplified_solved_InputToSAT; simplified_solved_InputToSAT = - CreateSubstitutionMap(simplified_solved_InputToSAT); + CreateSubstitutionMap(simplified_solved_InputToSAT); ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = - SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); + SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = - bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); + bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); ASTNodeStats("after solving: ", simplified_solved_InputToSAT); } while (inputToSAT != simplified_solved_InputToSAT); ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT); @@ -980,7 +980,7 @@ namespace BEEV //Begin_RemoveWrites = true; //ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = - SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); + SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); //ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); //simplified_solved_InputToSAT = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); //ASTNodeStats("after solving: ", simplified_solved_InputToSAT); diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index d5ab8b6..49cdf64 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -180,7 +180,7 @@ namespace BEEV { BeevMgr& bm = form.GetBeevMgr(); - assert(TransformMap != NULL); + assert(TransformMap != NULL); ASTNode result; @@ -273,7 +273,7 @@ namespace BEEV ASTNode TransformTerm(const ASTNode& inputterm) { - assert(TransformMap != NULL); + assert(TransformMap != NULL); BeevMgr& bm = inputterm.GetBeevMgr(); diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp index 7115ba3..b384a8a 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/AST/printer/AssortedPrinters.cpp @@ -294,12 +294,12 @@ namespace BEEV if (smtlib_parser_flag) { if (true_iff_valid && - (BEEV::input_status == TO_BE_SATISFIABLE)) + (input_status == TO_BE_SATISFIABLE)) { cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl; } else if (!true_iff_valid && - (BEEV::input_status == TO_BE_UNSATISFIABLE)) + (input_status == TO_BE_UNSATISFIABLE)) { cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; } @@ -349,7 +349,7 @@ namespace BEEV void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision_level, int polarity) { - BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var]; + BEEV::ASTNode vv = BEEV::GlobalBeevMgr->_SATVar_to_AST[minisat_var]; cout << spaces(decision_level); if (polarity) { @@ -357,6 +357,5 @@ namespace BEEV } printer::PL_Print(cout,vv, 0); cout << endl; - } - + } //end of Convert_MINISATVar_To_ASTNode_Print() };//end of namespace BEEV diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index b0e3b99..44b7f33 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -142,7 +142,7 @@ void vc_printExprCCode(VC vc, Expr e) { BEEV::ASTNode q = (*(nodestar)e); // print variable declarations - BEEV::ASTVec declsFromParser = (nodelist)BEEV::globalBeevMgr_for_parser->_special_print_set; + BEEV::ASTVec declsFromParser = (nodelist)BEEV::GlobalBeevMgr->_special_print_set; for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) { if(BEEV::BITVECTOR_TYPE == it->GetType()) { @@ -1459,7 +1459,7 @@ Expr vc_parseExpr(VC vc, char* infile) { BEEV::FatalError(""); } - BEEV::globalBeevMgr_for_parser = b; + BEEV::GlobalBeevMgr = b; CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); if(0 != c) { diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp new file mode 100644 index 0000000..88b219f --- /dev/null +++ b/src/main/Globals.cpp @@ -0,0 +1,75 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "../AST/AST.h" +namespace BEEV +{ + //some global variables that are set through commandline options. it + //is best that these variables remain global. Default values set + //here + // + //collect statistics on certain functions + bool stats_flag = false; + //print DAG nodes + bool print_nodes_flag = false; + //run STP in optimized mode + bool optimize_flag = true; + //do sat refinement, i.e. underconstraint the problem, and feed to + //SAT. if this works, great. else, add a set of suitable constraints + //to re-constraint the problem correctly, and call SAT again, until + //all constraints have been added. + bool arrayread_refinement_flag = true; + //flag to control write refinement + bool arraywrite_refinement_flag = true; + //check the counterexample against the original input to STP + bool check_counterexample_flag = false; + //construct the counterexample in terms of original variable based + //on the counterexample returned by SAT solver + bool construct_counterexample_flag = true; + bool print_counterexample_flag = false; + bool print_binary_flag = false; + //if this option is true then print the way dawson wants using a + //different printer. do not use this printer. + bool print_arrayval_declaredorder_flag = false; + //flag to decide whether to print "valid/invalid" or not + bool print_output_flag = false; + //print the variable order chosen by the sat solver while it is + //solving. + bool print_sat_varorder_flag = false; + //turn on word level bitvector solver + bool wordlevel_solve_flag = true; + //turn off XOR flattening + bool xor_flatten_flag = false; + //Flag to switch on the smtlib parser + bool smtlib_parser_flag = false; + //print the input back + bool print_STPinput_back_flag = false; + + // If enabled. division, mod and remainder by zero will evaluate to + // 1. + bool division_by_zero_returns_one = false; + + enum inputStatus input_status = NOT_DECLARED; + + + //global BEEVMGR for the parser + BeevMgr * GlobalBeevMgr; + + void (*vc_error_hdlr)(const char* err_msg) = NULL; + /** This is reusable empty vector, for representing empty children + arrays */ + ASTVec _empty_ASTVec; + + //Some global vars for the Main function. + const std::string version = "$Id: main.cpp 174 2009-09-03 19:22:47Z vijay_ganesh $"; + const char * prog = "stp"; + int linenum = 1; + const char * usage = "Usage: %s [-option] [infile]\n"; + std::string helpstring = "\n\n"; +}; //end of namespace BEEV diff --git a/src/main/Globals.h b/src/main/Globals.h new file mode 100644 index 0000000..212feed --- /dev/null +++ b/src/main/Globals.h @@ -0,0 +1,114 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +#ifndef GLOBALS_H +#define GLOBALS_H + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace MINISAT +{ + class Solver; + typedef int Var; +} + +namespace BEEV +{ + class BeevMgr; + class ASTNode; + class ASTInternal; + class ASTInterior; + class ASTSymbol; + class ASTBVConst; + class BVSolver; + + //some global variables that are set through commandline options. it + //is best that these variables remain global. Default values set + //here + // + //collect statistics on certain functions + extern bool stats_flag; + //print DAG nodes + extern bool print_nodes_flag; + //run STP in optimized mode + extern bool optimize_flag; + //do sat refinement, i.e. underconstraint the problem, and feed to + //SAT. if this works, great. else, add a set of suitable constraints + //to re-constraint the problem correctly, and call SAT again, until + //all constraints have been added. + extern bool arrayread_refinement_flag; + //switch to control write refinements + extern bool arraywrite_refinement_flag; + //check the counterexample against the original input to STP + extern bool check_counterexample_flag; + //construct the counterexample in terms of original variable based + //on the counterexample returned by SAT solver + extern bool construct_counterexample_flag; + extern bool print_counterexample_flag; + extern bool print_binary_flag; + //if this option is true then print the way dawson wants using a + //different printer. do not use this printer. + extern bool print_arrayval_declaredorder_flag; + //flag to decide whether to print "valid/invalid" or not + extern bool print_output_flag; + //print the variable order chosen by the sat solver while it is + //solving. + extern bool print_sat_varorder_flag; + //turn on word level bitvector solver + extern bool wordlevel_solve_flag; + //XOR flattening optimizations. + extern bool xor_flatten_flag; + //this flag indicates that the BVSolver() succeeded + extern bool toplevel_solved_flag; + //print the input back + extern bool print_STPinput_back_flag; + //Flag to switch on the smtlib parser + extern bool smtlib_parser_flag; + + extern bool division_by_zero_returns_one; + + enum inputStatus + { + NOT_DECLARED =0, // Not included in the input file / stream + TO_BE_SATISFIABLE, + TO_BE_UNSATISFIABLE, + TO_BE_UNKNOWN // Specified in the input file as unknown. + }; + extern enum inputStatus input_status; + + //return types for the GetType() function in ASTNode class + enum types + { + BOOLEAN_TYPE = 0, BITVECTOR_TYPE, ARRAY_TYPE, UNKNOWN_TYPE + }; + + enum SOLVER_RETURN_TYPE + { + SOLVER_INVALID=0, SOLVER_VALID=1, SOLVER_UNDECIDED=2, SOLVER_ERROR=-100 + }; + + //Useful global variables. There are very few them + extern BeevMgr * GlobalBeevMgr; + + //Some global vars for the Main function. + extern const char * prog; + extern int linenum; + extern const char * usage; + extern std::string helpstring; + extern const std::string version; +}; //end of namespace BEEV + +#endif diff --git a/src/main/Makefile b/src/main/Makefile new file mode 100644 index 0000000..03a0665 --- /dev/null +++ b/src/main/Makefile @@ -0,0 +1,13 @@ +include ../../scripts/Makefile.common + +SRCS = Globals.cpp main.cpp +OBJS = $(SRCS:.cpp=.o) +LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv -L../parser -lparser +CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp -I../sat/unsound + +parser: Globals.o main.o + $(CXX) $(CFLAGS) $(LDFLAGS) Globals.o main.o $(LIBS) -o stp + @mv stp ../../bin/stp + +clean: + rm -rf *.o *~ *.a .#* diff --git a/src/main/main.cpp b/src/main/main.cpp new file mode 100644 index 0000000..3331ab9 --- /dev/null +++ b/src/main/main.cpp @@ -0,0 +1,186 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- +#include "../AST/AST.h" +#include "../sat/core/Solver.h" +#include "../sat/core/SolverTypes.h" + +#ifdef EXT_HASH_MAP +using namespace __gnu_cxx; +#endif +using namespace BEEV; + +extern int smtparse(); +extern int cvcparse(void*); + +// Amount of memory to ask for at beginning of main. +static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; +/****************************************************************************** + * MAIN FUNCTION: + * + * step 0. Parse the input into an ASTVec. + * step 1. Do BV Rewrites + * step 2. Bitblasts the ASTNode. + * step 3. Convert to CNF + * step 4. Convert to SAT + * step 5. Call SAT to determine if input is SAT or UNSAT + ******************************************************************************/ +int main(int argc, char ** argv) { + char * infile; + extern FILE *cvcin; + extern FILE *smtin; + + // Grab some memory from the OS upfront to reduce system time when + // individual hash tables are being allocated + if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) + { + // FIXME: figure out how to get and print the real error + // message. + FatalError("Initial allocation of memory failed."); + } + + //populate the help string + helpstring += "version: " + version + "\n\n"; + helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; + helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; + helpstring += "-a : switch optimizations off (optimizations are ON by default)\n"; + helpstring += "-s : print function statistics\n"; + helpstring += "-v : print nodes \n"; + helpstring += "-c : construct counterexample\n"; + helpstring += "-d : check counterexample\n"; + helpstring += "-p : print counterexample\n"; + helpstring += "-y : print counterexample in binary\n"; + helpstring += "-b : STP input read back\n"; + helpstring += "-x : flatten nested XORs\n"; + helpstring += "-h : help\n"; + helpstring += "-m : use the SMTLIB parser\n"; + + + + for(int i=1; i < argc;i++) + { + if(argv[i][0] == '-') + { + switch(argv[i][1]) + { + case 'a' : + optimize_flag = false; + break; + case 'b': + print_STPinput_back_flag = true; + break; + case 'c': + construct_counterexample_flag = true; + break; + case 'd': + construct_counterexample_flag = true; + check_counterexample_flag = true; + break; + case 'h': + fprintf(stderr,usage,prog); + cout << helpstring; + //FatalError(""); + return -1; + break; + case 'n': + print_output_flag = true; + break; + case 'm': + smtlib_parser_flag=true; + division_by_zero_returns_one = true; + break; + case 'p': + print_counterexample_flag = true; + break; + case 'y': + print_binary_flag = true; + break; + case 'q': + print_arrayval_declaredorder_flag = true; + break; + case 'r': + arrayread_refinement_flag = false; + break; + case 's' : + stats_flag = true; + break; + case 'u': + arraywrite_refinement_flag = false; + break; + case 'v' : + print_nodes_flag = true; + break; + case 'w': + wordlevel_solve_flag = false; + break; + case 'x': + xor_flatten_flag = true; + break; + case 'z': + print_sat_varorder_flag = true; + break; + default: + fprintf(stderr,usage,prog); + cout << helpstring; + //FatalError(""); + return -1; + break; + } + if(argv[i][2]) { + fprintf(stderr, "Multiple character options are not allowed.\n"); + fprintf(stderr, "(for example: -ab is not an abbreviation for -a -b)\n"); + fprintf(stderr,usage,prog); + cout << helpstring; + return -1; + } + } else { + infile = argv[i]; + + if (smtlib_parser_flag) + { + smtin = fopen(infile,"r"); + if(smtin == 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(""); + } + } + } + } + + CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); + if(0 != c) { + cout << CONSTANTBV::BitVector_Error(c) << endl; + return 0; + } + + //want to print the output always from the commandline. + print_output_flag = true; + GlobalBeevMgr = new BeevMgr(); + ASTVec * AssertsQuery = new ASTVec; + + if (smtlib_parser_flag) { + smtparse(); + } + else { + cvcparse((void*)AssertsQuery); + ASTNode asserts = (*(ASTVec*)AssertsQuery)[0]; + ASTNode query = (*(ASTVec*)AssertsQuery)[1]; + GlobalBeevMgr->TopLevelSAT(asserts, query); + } + return 0; +}//end of Main diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex index daa28a3..bc9a176 100644 --- a/src/parser/CVC.lex +++ b/src/parser/CVC.lex @@ -11,8 +11,11 @@ #include "../AST/AST.h" #include "parseCVC_defs.h" -extern char *yytext; -extern int cvcerror (const char *msg); + using namespace std; + using namespace BEEV; + + extern char *yytext; + extern int cvcerror (const char *msg); %} %option noyywrap @@ -34,10 +37,10 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) [\n] { /*Skip new line */ } [ \t\r\f] { /* skip whitespace */ } -0b{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} -0bin{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} -0h{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} -0hex{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} +0b{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} +0bin{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} +0h{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} +0hex{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} {DIGIT}+ { cvclval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;} "%" { BEGIN COMMENT;} @@ -114,14 +117,14 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "POP" { return POP_TOK;} (({LETTER})|(_)({ANYTHING}))({ANYTHING})* { - BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); + BEEV::ASTNode nptr = BEEV::GlobalBeevMgr->CreateSymbol(yytext); // 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. - cvclval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); + cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->ResolveID(nptr)); //cvclval.node = new BEEV::ASTNode(nptr); - if ((cvclval.node)->GetType() == BEEV::BOOLEAN_TYPE) + if ((cvclval.node)->GetType() == BOOLEAN_TYPE) return FORMID_TOK; else return TERMID_TOK; diff --git a/src/parser/CVC.y b/src/parser/CVC.y index 293dc3c..54c2d2c 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -9,7 +9,8 @@ // -*- c++ -*- #include "../AST/AST.h" -using namespace std; + using namespace std; + using namespace BEEV; // Suppress the bogus warning suppression in bison (it generates // compile error) @@ -21,7 +22,7 @@ using namespace std; extern int cvclineno; int yyerror(const char *s) { cout << "syntax error: line " << cvclineno << "\n" << s << endl; - BEEV::FatalError(""); + FatalError(""); return 1; /* Dill: don't know what it should return */ }; @@ -29,6 +30,8 @@ using namespace std; #define YYMAXDEPTH 10485760 #define YYERROR_VERBOSE 1 #define YY_EXIT_FAILURE -1 + +#define YYPARSE_PARAM AssertsQuery %} %union { @@ -171,31 +174,42 @@ cmd : other_cmd counterexample : COUNTEREXAMPLE_TOK ';' { - BEEV::print_counterexample_flag = true; - BEEV::globalBeevMgr_for_parser->PrintCounterExample(true); + print_counterexample_flag = true; + GlobalBeevMgr->PrintCounterExample(true); } ; other_cmd : other_cmd1 | Query { - BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE),*$1); + //GlobalBeevMgr->TopLevelSAT(GlobalBeevMgr->CreateNode(TRUE),*$1); + ((ASTVec*)AssertsQuery)->push_back(GlobalBeevMgr->CreateNode(TRUE)); + ((ASTVec*)AssertsQuery)->push_back(*$1); delete $1; } | VarDecls Query { - BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE),*$2); + //GlobalBeevMgr->TopLevelSAT(GlobalBeevMgr->CreateNode(TRUE),*$2); + ((ASTVec*)AssertsQuery)->push_back(GlobalBeevMgr->CreateNode(TRUE)); + ((ASTVec*)AssertsQuery)->push_back(*$2); delete $2; } | other_cmd1 Query { - BEEV::ASTVec aaa = BEEV::globalBeevMgr_for_parser->GetAsserts(); + ASTVec aaa = GlobalBeevMgr->GetAsserts(); if(aaa.size() == 0) yyerror("Fatal Error: parsing: GetAsserts() call: no assertions: "); - if(aaa.size() == 1) - BEEV::globalBeevMgr_for_parser->TopLevelSAT(aaa[0],*$2); - else - BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND,aaa),*$2); + /* if(aaa.size() == 1) */ + /* { */ + /*GlobalBeevMgr->TopLevelSAT(aaa[0],*$2); */ + /* } */ + /* else */ + /* { */ + /*GlobalBeevMgr->TopLevelSAT(GlobalBeevMgr->CreateNode(AND,aaa),*$2); */ + /* } */ + ASTNode asserts = GlobalBeevMgr->CreateNode(AND,aaa); + ((ASTVec*)AssertsQuery)->push_back(asserts); + ((ASTVec*)AssertsQuery)->push_back(*$2); delete $2; } ; @@ -216,29 +230,29 @@ other_cmd1 : VarDecls Asserts /* push : PUSH_TOK */ /* { */ -/* BEEV::globalBeevMgr_for_parser->Push(); */ +/* GlobalBeevMgr->Push(); */ /* } */ /* | */ /* ; */ /* pop : POP_TOK */ /* { */ -/* BEEV::globalBeevMgr_for_parser->Pop(); */ +/* GlobalBeevMgr->Pop(); */ /* } */ /* | */ /* ; */ Asserts : Assert { - $$ = new BEEV::ASTVec; + $$ = new ASTVec; $$->push_back(*$1); - BEEV::globalBeevMgr_for_parser->AddAssert(*$1); + GlobalBeevMgr->AddAssert(*$1); delete $1; } | Asserts Assert { $1->push_back(*$2); - BEEV::globalBeevMgr_for_parser->AddAssert(*$2); + GlobalBeevMgr->AddAssert(*$2); $$ = $1; delete $2; } @@ -247,7 +261,7 @@ Asserts : Assert Assert : ASSERT_TOK Formula ';' { $$ = $2; } ; -Query : QUERY_TOK Formula ';' { BEEV::globalBeevMgr_for_parser->AddQuery(*$2); $$ = $2;} +Query : QUERY_TOK Formula ';' { GlobalBeevMgr->AddQuery(*$2); $$ = $2;} ; @@ -262,51 +276,51 @@ VarDecls : VarDecl ';' VarDecl : FORM_IDs ':' Type { - for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { - BEEV::_parser_symbol_table.insert(*i); + for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + _parser_symbol_table.insert(*i); i->SetIndexWidth($3.indexwidth); i->SetValueWidth($3.valuewidth); //FIXME: HACK_ATTACK. this vector was hacked into the code to //support a special request by Dawson' group. They want the //counterexample to be printed in the order of variables declared. - BEEV::globalBeevMgr_for_parser->_special_print_set.push_back(*i); + GlobalBeevMgr->_special_print_set.push_back(*i); } delete $1; } | FORM_IDs ':' Type '=' Expr { //do type checking. if doesn't pass then abort - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->BVTypeCheck(*$5); if($3.indexwidth != $5->GetIndexWidth()) yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); if($3.valuewidth != $5->GetValueWidth()) yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { //set the valuewidth of the identifier i->SetValueWidth($5->GetValueWidth()); i->SetIndexWidth($5->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->LetExprMgr(*i,*$5); + GlobalBeevMgr->LetExprMgr(*i,*$5); delete $5; } } | FORM_IDs ':' Type '=' Formula { //do type checking. if doesn't pass then abort - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->BVTypeCheck(*$5); if($3.indexwidth != $5->GetIndexWidth()) yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); if($3.valuewidth != $5->GetValueWidth()) yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { //set the valuewidth of the identifier i->SetValueWidth($5->GetValueWidth()); i->SetIndexWidth($5->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->LetExprMgr(*i,*$5); + GlobalBeevMgr->LetExprMgr(*i,*$5); delete $5; } } @@ -314,7 +328,7 @@ VarDecl : FORM_IDs ':' Type reverseFORM_IDs : FORMID_TOK { - $$ = new BEEV::ASTVec; + $$ = new ASTVec; $$->push_back(*$1); delete $1; } @@ -328,7 +342,7 @@ reverseFORM_IDs : FORMID_TOK FORM_IDs : reverseFORM_IDs { - $$ = new BEEV::ASTVec($1->rbegin(),$1->rend()); + $$ = new ASTVec($1->rbegin(),$1->rend()); delete $1; } ; @@ -348,7 +362,7 @@ BvType : BV_TOK '(' NUMERAL_TOK ')' $$.valuewidth = length; } else - BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); } ; BoolType : BOOLEAN_TOK @@ -373,12 +387,12 @@ IfExpr : IF_TOK Formula THEN_TOK Expr ElseRestExpr if($4->GetIndexWidth() != $5->GetIndexWidth()) yyerror("Width mismatch in IF-THEN-ELSE"); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE, width, *$2, *$4, *$5)); + GlobalBeevMgr->BVTypeCheck(*$2); + GlobalBeevMgr->BVTypeCheck(*$4); + GlobalBeevMgr->BVTypeCheck(*$5); + $$ = new ASTNode(GlobalBeevMgr->CreateTerm(ITE, width, *$2, *$4, *$5)); $$->SetIndexWidth($5->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$); + GlobalBeevMgr->BVTypeCheck(*$$); delete $2; delete $4; delete $5; @@ -394,12 +408,12 @@ ElseRestExpr : ELSE_TOK Expr ENDIF_TOK { $$ = $2; } if ($2->GetIndexWidth() != $4->GetValueWidth() || $2->GetIndexWidth() != $5->GetValueWidth()) yyerror("Width mismatch in IF-THEN-ELSE"); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE, width, *$2, *$4, *$5)); + GlobalBeevMgr->BVTypeCheck(*$2); + GlobalBeevMgr->BVTypeCheck(*$4); + GlobalBeevMgr->BVTypeCheck(*$5); + $$ = new ASTNode(GlobalBeevMgr->CreateTerm(ITE, width, *$2, *$4, *$5)); $$->SetIndexWidth($5->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$); + GlobalBeevMgr->BVTypeCheck(*$$); delete $2; delete $4; delete $5; @@ -408,36 +422,36 @@ ElseRestExpr : ELSE_TOK Expr ENDIF_TOK { $$ = $2; } /* Grammar for formulas */ Formula : '(' Formula ')' { $$ = $2; } - | FORMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); delete $1;} + | FORMID_TOK { $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); delete $1;} | BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')' { unsigned int width = $3->GetValueWidth(); if(width <= (unsigned)$5) yyerror("Fatal Error: BOOLEXTRACT: trying to boolextract a bit which beyond range"); - BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); - BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,1,*$3,hi,low)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); - BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,0); - BEEV::ASTNode * out = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ,*n,zero)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*out); + ASTNode hi = GlobalBeevMgr->CreateBVConst(32, $5); + ASTNode low = GlobalBeevMgr->CreateBVConst(32, $5); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVEXTRACT,1,*$3,hi,low)); + GlobalBeevMgr->BVTypeCheck(*n); + ASTNode zero = GlobalBeevMgr->CreateBVConst(1,0); + ASTNode * out = new ASTNode(GlobalBeevMgr->CreateNode(EQ,*n,zero)); + GlobalBeevMgr->BVTypeCheck(*out); $$ = out; delete $3; } | Expr '=' Expr { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ, *$1, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(EQ, *$1, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; delete $3; } | Expr NEQ_TOK Expr { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ, *$1, *$3))); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(NOT, GlobalBeevMgr->CreateNode(EQ, *$1, *$3))); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; delete $3; @@ -457,14 +471,14 @@ Formula : '(' Formula ')' { $$ = $2; } //increment value (BVCONST) // //formula (it can be a nested forloop) - BEEV::ASTVec vec; + ASTVec vec; vec.push_back(*$3); vec.push_back(*$5); vec.push_back(*$7); vec.push_back(*$9); vec.push_back(*$12); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FOR,vec)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; @@ -474,111 +488,111 @@ Formula : '(' Formula ')' { $$ = $2; } } | NOT_TOK Formula { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$2)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(NOT, *$2)); delete $2; } | Formula OR_TOK Formula %prec OR_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::OR, *$1, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(OR, *$1, *$3)); delete $1; delete $3; } | Formula NOR_TOK Formula { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOR, *$1, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(NOR, *$1, *$3)); delete $1; delete $3; } | Formula AND_TOK Formula %prec AND_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND, *$1, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(AND, *$1, *$3)); delete $1; delete $3; } | Formula NAND_TOK Formula { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NAND, *$1, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(NAND, *$1, *$3)); delete $1; delete $3; } | Formula IMPLIES_TOK Formula { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IMPLIES, *$1, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(IMPLIES, *$1, *$3)); delete $1; delete $3; } | Formula IFF_TOK Formula { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IFF, *$1, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(IFF, *$1, *$3)); delete $1; delete $3; } | Formula XOR_TOK Formula { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::XOR, *$1, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(XOR, *$1, *$3)); delete $1; delete $3; } | BVLT_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLT, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVLT, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; } | BVGT_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGT, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVGT, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; } | BVLE_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLE, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVLE, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; } | BVGE_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGE, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVGE, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; } | BVSLT_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLT, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSLT, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; } | BVSGT_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGT, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSGT, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; } | BVSLE_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLE, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSLE, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; } | BVSGE_TOK '(' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGE, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSGE, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; @@ -586,13 +600,13 @@ Formula : '(' Formula ')' { $$ = $2; } | IfForm | TRUELIT_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(TRUE)); $$->SetIndexWidth(0); $$->SetValueWidth(0); } | FALSELIT_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(FALSE)); $$->SetIndexWidth(0); $$->SetValueWidth(0); } @@ -601,14 +615,14 @@ Formula : '(' Formula ')' { $$ = $2; } { $$ = $4; //Cleanup the LetIDToExprMap - BEEV::globalBeevMgr_for_parser->CleanupLetIDMap(); + GlobalBeevMgr->CleanupLetIDMap(); } ; /*Grammar for ITEs which are Formulas */ IfForm : IF_TOK Formula THEN_TOK Formula ElseRestForm { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$2, *$4, *$5)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(ITE, *$2, *$4, *$5)); delete $2; delete $4; delete $5; @@ -618,7 +632,7 @@ IfForm : IF_TOK Formula THEN_TOK Formula ElseRestForm ElseRestForm : ELSE_TOK Formula ENDIF_TOK { $$ = $2; } | ELSIF_TOK Formula THEN_TOK Formula ElseRestForm { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$2, *$4, *$5)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(ITE, *$2, *$4, *$5)); delete $2; delete $4; delete $5; @@ -628,40 +642,40 @@ ElseRestForm : ELSE_TOK Formula ENDIF_TOK { $$ = $2; } /*Grammar for a list of expressions*/ Exprs : Expr { - $$ = new BEEV::ASTVec; - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$1); + $$ = new ASTVec; + GlobalBeevMgr->BVTypeCheck(*$1); $$->push_back(*$1); delete $1; } | Exprs ',' Expr { $1->push_back(*$3); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + GlobalBeevMgr->BVTypeCheck(*$3); $$ = $1; delete $3; } ; /* Grammar for Expr */ -Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); delete $1;} +Expr : TERMID_TOK { $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); delete $1;} | '(' Expr ')' { $$ = $2; } | BVCONST_TOK { $$ = $1; } | BOOL_TO_BV_TOK '(' Formula ')' { - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); - BEEV::ASTNode one = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,1); - BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,0); + GlobalBeevMgr->BVTypeCheck(*$3); + ASTNode one = GlobalBeevMgr->CreateBVConst(1,1); + ASTNode zero = GlobalBeevMgr->CreateBVConst(1,0); //return ITE(*$3, length(1), 0bin1, 0bin0) - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE,1,*$3,one,zero)); + $$ = new ASTNode(GlobalBeevMgr->CreateTerm(ITE,1,*$3,one,zero)); delete $3; } | Expr '[' Expr ']' { // valuewidth is same as array, indexwidth is 0. unsigned int width = $1->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, *$1, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(READ, width, *$1, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; @@ -671,8 +685,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- { // valuewidth is same as array, indexwidth is 0. unsigned int width = $1->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, *$1, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(READ, width, *$1, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; @@ -687,18 +701,18 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- if((unsigned)$3 >= $1->GetValueWidth()) 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 * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$1,hi,low)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode hi = GlobalBeevMgr->CreateBVConst(32, $3); + ASTNode low = GlobalBeevMgr->CreateBVConst(32, $5); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVEXTRACT, width, *$1,hi,low)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; } | BVNEG_TOK Expr { 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVNEG, width, *$2)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; } @@ -708,8 +722,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- if (width != $3->GetValueWidth()) { yyerror("Width mismatch in AND"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVAND, width, *$1, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVAND, width, *$1, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; delete $3; @@ -720,8 +734,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- if (width != $3->GetValueWidth()) { yyerror("Width mismatch in OR"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVOR, width, *$1, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVOR, width, *$1, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; delete $3; @@ -732,8 +746,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- if (width != $5->GetValueWidth()) { yyerror("Width mismatch in XOR"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXOR, width, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVXOR, width, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $5; @@ -744,8 +758,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- if (width != $5->GetValueWidth()) { yyerror("Width mismatch in NAND"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNAND, width, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVNAND, width, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; @@ -757,8 +771,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- if (width != $5->GetValueWidth()) { yyerror("Width mismatch in NOR"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNOR, width, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVNOR, width, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; @@ -770,8 +784,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- if (width != $5->GetValueWidth()) { yyerror("Width mismatch in NOR"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXNOR, width, *$3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVXNOR, width, *$3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; @@ -782,15 +796,15 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- //width of the expr which is being sign //extended. $5 is the resulting length of the //signextended expr - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + GlobalBeevMgr->BVTypeCheck(*$3); if($3->GetValueWidth() == $5) { $$ = $3; } else { - BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$5); - BEEV::ASTNode *n = - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSX, $5,*$3,width)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode width = GlobalBeevMgr->CreateBVConst(32,$5); + ASTNode *n = + new ASTNode(GlobalBeevMgr->CreateTerm(BVSX, $5,*$3,width)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; } @@ -798,8 +812,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- | Expr BVCONCAT_TOK Expr { unsigned int width = $1->GetValueWidth() + $3->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, width, *$1, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT, width, *$1, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; @@ -807,47 +821,47 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- } | Expr BVLEFTSHIFT_TOK NUMERAL_TOK { - BEEV::ASTNode zero_bits = BEEV::globalBeevMgr_for_parser->CreateZeroConst($3); - BEEV::ASTNode * n = - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, + ASTNode zero_bits = GlobalBeevMgr->CreateZeroConst($3); + ASTNode * n = + new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT, $1->GetValueWidth() + $3, *$1, zero_bits)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $1; } | Expr BVRIGHTSHIFT_TOK NUMERAL_TOK { - BEEV::ASTNode len = BEEV::globalBeevMgr_for_parser->CreateZeroConst($3); + ASTNode len = GlobalBeevMgr->CreateZeroConst($3); unsigned int w = $1->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,*$1,hi,low); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,len, extract)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode hi = GlobalBeevMgr->CreateBVConst(32,w-1); + ASTNode low = GlobalBeevMgr->CreateBVConst(32,$3); + ASTNode extract = GlobalBeevMgr->CreateTerm(BVEXTRACT,w-$3,*$1,hi,low); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT, w,len, extract)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; } else - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateZeroConst(w)); + $$ = new ASTNode(GlobalBeevMgr->CreateZeroConst(w)); delete $1; } | BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVPLUS, $3, *$5)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVPLUS, $3, *$5)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; } | BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSUB, $3, *$5, *$7)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVSUB, $3, *$5, *$7)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; @@ -856,15 +870,15 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- | BVUMINUS_TOK '(' Expr ')' { unsigned width = $3->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVUMINUS,width,*$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVUMINUS,width,*$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; } | BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMULT, $3, *$5, *$7)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVMULT, $3, *$5, *$7)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; @@ -872,8 +886,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- } | BVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVDIV, $3, *$5, *$7)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVDIV, $3, *$5, *$7)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; @@ -881,8 +895,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- } | BVMOD_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMOD, $3, *$5, *$7)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVMOD, $3, *$5, *$7)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; @@ -890,8 +904,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- } | SBVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVDIV, $3, *$5, *$7)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(SBVDIV, $3, *$5, *$7)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; @@ -899,8 +913,8 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- } | SBVREM_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVREM, $3, *$5, *$7)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(SBVREM, $3, *$5, *$7)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; delete $7; @@ -911,35 +925,35 @@ Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser- { $$ = $4; //Cleanup the LetIDToExprMap - //BEEV::globalBeevMgr_for_parser->CleanupLetIDMap(); + //GlobalBeevMgr->CleanupLetIDMap(); } ; /*Grammar for Array Update Expr*/ ArrayUpdateExpr : Expr WITH_TOK Updates { - BEEV::ASTNode * result; + ASTNode * result; unsigned int width = $1->GetValueWidth(); - BEEV::ASTNodeMap::iterator it = $3->begin(); - BEEV::ASTNodeMap::iterator itend = $3->end(); - result = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE, + ASTNodeMap::iterator it = $3->begin(); + ASTNodeMap::iterator itend = $3->end(); + result = new ASTNode(GlobalBeevMgr->CreateTerm(WRITE, width, *$1, (*it).first, (*it).second)); result->SetIndexWidth($1->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result); + GlobalBeevMgr->BVTypeCheck(*result); for(it++;it!=itend;it++) { - result = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE, + result = new ASTNode(GlobalBeevMgr->CreateTerm(WRITE, width, *result, (*it).first, (*it).second)); result->SetIndexWidth($1->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result); + GlobalBeevMgr->BVTypeCheck(*result); } - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result); + GlobalBeevMgr->BVTypeCheck(*result); $$ = result; delete $3; } @@ -947,7 +961,7 @@ ArrayUpdateExpr : Expr WITH_TOK Updates Updates : '[' Expr ']' ASSIGN_TOK Expr { - $$ = new BEEV::ASTNodeMap(); + $$ = new ASTNodeMap(); (*$$)[*$2] = *$5; } | Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr @@ -964,7 +978,7 @@ LetDecls : LetDecl LetDecl : FORMID_TOK '=' Expr { //Expr must typecheck - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + GlobalBeevMgr->BVTypeCheck(*$3); //set the valuewidth of the identifier $1->SetValueWidth($3->GetValueWidth()); @@ -978,14 +992,14 @@ LetDecl : FORMID_TOK '=' Expr // //2. Ensure that LET variables are not //2. defined more than once - BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$3); + GlobalBeevMgr->LetExprMgr(*$1,*$3); delete $1; delete $3; } | FORMID_TOK ':' Type '=' Expr { //do type checking. if doesn't pass then abort - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->BVTypeCheck(*$5); if($3.indexwidth != $5->GetIndexWidth()) yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); @@ -996,28 +1010,28 @@ LetDecl : FORMID_TOK '=' Expr $1->SetValueWidth($5->GetValueWidth()); $1->SetIndexWidth($5->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$5); + GlobalBeevMgr->LetExprMgr(*$1,*$5); delete $1; delete $5; } | FORMID_TOK '=' Formula { //Expr must typecheck - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + GlobalBeevMgr->BVTypeCheck(*$3); //set the valuewidth of the identifier $1->SetValueWidth($3->GetValueWidth()); $1->SetIndexWidth($3->GetIndexWidth()); //Do LET-expr management - BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$3); + GlobalBeevMgr->LetExprMgr(*$1,*$3); delete $1; delete $3; } | FORMID_TOK ':' Type '=' Formula { //do type checking. if doesn't pass then abort - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->BVTypeCheck(*$5); if($3.indexwidth != $5->GetIndexWidth()) yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); @@ -1029,7 +1043,7 @@ LetDecl : FORMID_TOK '=' Expr $1->SetIndexWidth($5->GetIndexWidth()); //Do LET-expr management - BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$5); + GlobalBeevMgr->LetExprMgr(*$1,*$5); delete $1; delete $5; } diff --git a/src/parser/Makefile b/src/parser/Makefile index e3e086a..2769085 100644 --- a/src/parser/Makefile +++ b/src/parser/Makefile @@ -3,17 +3,16 @@ include ../../scripts/Makefile.common LEX=flex YACC=bison -d -y --debug -v -SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp let-funcs.cpp main.cpp +SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp let-funcs.cpp OBJS = $(SRCS:.cpp=.o) LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv -#CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp -CFLAGS += -I../sat/mtl -I../sat/core -I../sat/unsound +CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp -I../sat/unsound -all: parseSMT.cpp lexSMT.cpp parseCVC.cpp lexCVC.cpp let-funcs.cpp parser parseCVC.o lexCVC.o let-funcs.o +#all: parseSMT.cpp lexSMT.cpp parseCVC.cpp lexCVC.cpp let-funcs.cpp parser parseCVC.o lexCVC.o let-funcs.o -parser: lexCVC.o parseCVC.o lexSMT.o parseSMT.o let-funcs.o main.o - $(CXX) $(CFLAGS) $(LDFLAGS) lexCVC.o lexSMT.o parseCVC.o parseSMT.o main.o let-funcs.o $(LIBS) -o parser - @mv parser ../../bin/stp +libparser.a: $(OBJS) + $(AR) rc $@ $^ + $(RANLIB) $@ lexCVC.cpp: CVC.lex parseCVC_defs.h ../AST/AST.h $(LEX) -o lexCVC.cpp --prefix cvc CVC.lex diff --git a/src/parser/main.cpp b/src/parser/main.cpp deleted file mode 100644 index 0cb181e..0000000 --- a/src/parser/main.cpp +++ /dev/null @@ -1,212 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -#include -#include -#include -#include -#include -#include -#include -//#include -#include -#include "../AST/AST.h" -#include "../sat/core/Solver.h" -#include "../sat/core/SolverTypes.h" -//#include "../sat/VarOrder.h" - -#include - -#ifdef EXT_HASH_MAP -using namespace __gnu_cxx; -#endif - -/* GLOBAL FUNCTION: parser - */ -extern int smtparse(); -extern int cvcparse(); - - -namespace BEEV -{ - extern BEEV::ASTNode SingleBitOne; - extern BEEV::ASTNode SingleBitZero; -} - -const string version = "$Id$"; - -/* GLOBAL VARS: Some global vars for the Main function. - * - */ -const char * prog = "stp"; -int linenum = 1; -const char * usage = "Usage: %s [-option] [infile]\n"; -std::string helpstring = "\n\n"; - -// Amount of memory to ask for at beginning of main. -static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; - -/****************************************************************************** - * MAIN FUNCTION: - * - * step 0. Parse the input into an ASTVec. - * step 1. Do BV Rewrites - * step 2. Bitblasts the ASTNode. - * step 3. Convert to CNF - * step 4. Convert to SAT - * step 5. Call SAT to determine if input is SAT or UNSAT - ******************************************************************************/ -int main(int argc, char ** argv) { - char * infile; - extern FILE *cvcin; - extern FILE *smtin; - - - - // Grab some memory from the OS upfront to reduce system time when individual - // hash tables are being allocated - - if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) { - // FIXME: figure out how to get and print the real error message. - BEEV::FatalError("Initial allocation of memory failed."); - } - - //populate the help string - helpstring += "version: " + version + "\n\n"; - helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; - helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; - helpstring += "-a : switch optimizations off (optimizations are ON by default)\n"; - helpstring += "-s : print function statistics\n"; - helpstring += "-v : print nodes \n"; - helpstring += "-c : construct counterexample\n"; - helpstring += "-d : check counterexample\n"; - helpstring += "-p : print counterexample\n"; - helpstring += "-y : print counterexample in binary\n"; - helpstring += "-b : STP input read back\n"; - helpstring += "-x : flatten nested XORs\n"; - helpstring += "-h : help\n"; - helpstring += "-m : use the SMTLIB parser\n"; - - - - for(int i=1; i < argc;i++) { - if(argv[i][0] == '-') { - switch(argv[i][1]) { - case 'a' : - BEEV::optimize_flag = false; - break; - case 'b': - BEEV::print_STPinput_back_flag = true; - break; - case 'c': - BEEV::construct_counterexample_flag = true; - break; - case 'd': - BEEV::construct_counterexample_flag = true; - BEEV::check_counterexample_flag = true; - break; - case 'h': - fprintf(stderr,usage,prog); - cout << helpstring; - //BEEV::FatalError(""); - return -1; - break; - case 'n': - BEEV::print_output_flag = true; - break; - case 'm': - BEEV::smtlib_parser_flag=true; - BEEV::division_by_zero_returns_one = true; - break; - case 'p': - BEEV::print_counterexample_flag = true; - break; - case 'y': - BEEV::print_binary_flag = true; - break; - case 'q': - BEEV::print_arrayval_declaredorder_flag = true; - break; - case 'r': - BEEV::arrayread_refinement_flag = false; - break; - case 's' : - BEEV::stats_flag = true; - break; - case 'u': - BEEV::arraywrite_refinement_flag = false; - break; - case 'v' : - BEEV::print_nodes_flag = true; - break; - case 'w': - BEEV::wordlevel_solve_flag = false; - break; - case 'x': - BEEV::xor_flatten_flag = true; - break; - case 'z': - BEEV::print_sat_varorder_flag = true; - break; - default: - fprintf(stderr,usage,prog); - cout << helpstring; - //BEEV::FatalError(""); - return -1; - break; - } - if(argv[i][2]) { - fprintf(stderr, "Multiple character options are not allowed.\n"); - fprintf(stderr, "(for example: -ab is not an abbreviation for -a -b)\n"); - fprintf(stderr,usage,prog); - cout << helpstring; - return -1; - } - } else { - infile = argv[i]; - - if (BEEV::smtlib_parser_flag) - { - smtin = fopen(infile,"r"); - if(smtin == NULL) - { - fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); - BEEV::FatalError(""); - } - } - else - { - cvcin = fopen(infile,"r"); - if(cvcin == NULL) - { - fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); - BEEV::FatalError(""); - } - } - } - } - - CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); - if(0 != c) { - cout << CONSTANTBV::BitVector_Error(c) << endl; - return 0; - } - - //want to print the output always from the commandline. - BEEV::print_output_flag = true; - BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr(); - - BEEV::SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); - BEEV::SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); - - if (BEEV::smtlib_parser_flag) - smtparse(); - else - cvcparse(); -}//end of Main diff --git a/src/parser/smtlib.lex b/src/parser/smtlib.lex index 80af712..4544673 100644 --- a/src/parser/smtlib.lex +++ b/src/parser/smtlib.lex @@ -36,13 +36,15 @@ #include #include "../AST/AST.h" #include "parseSMT_defs.h" + + using namespace std; + using namespace BEEV; extern char *smttext; extern int smterror (const char *msg); // File-static (local to this file) variables and functions - static std::string _string_lit; - + static std::string _string_lit; static char escapeChar(char c) { switch(c) { case 'n': return '\n'; @@ -50,16 +52,6 @@ default: return c; } } - -namespace BEEV -{ - extern BEEV::ASTNode SingleBitOne; - extern BEEV::ASTNode SingleBitZero; - } - -/* Changed for smtlib speedup */ -/* bv{DIGIT}+ { smtlval.node = new BEEV::ASTNode(BEEV::_bm->CreateBVConst(smttext+2, 10)); return BVCONST_TOK;} */ - %} %option noyywrap @@ -87,10 +79,10 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) bit{DIGIT}+ { char c = smttext[3]; if (c == '1') { - smtlval.node = new BEEV::ASTNode(BEEV::SingleBitOne); + smtlval.node = new BEEV::ASTNode(GlobalBeevMgr->CreateOneConst(1)); } else { - smtlval.node = new BEEV::ASTNode(BEEV::SingleBitZero); + smtlval.node = new BEEV::ASTNode(GlobalBeevMgr->CreateZeroConst(1)); } return BITCONST_TOK; }; @@ -223,14 +215,14 @@ bit{DIGIT}+ { "boolbv" { return BOOL_TO_BV_TOK;} (({LETTER})|(_)({ANYTHING}))({ANYTHING})* { - BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(smttext); + BEEV::ASTNode nptr = BEEV::GlobalBeevMgr->CreateSymbol(smttext); // 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. - smtlval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); + smtlval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->ResolveID(nptr)); //smtlval.node = new BEEV::ASTNode(nptr); - if ((smtlval.node)->GetType() == BEEV::BOOLEAN_TYPE) + if ((smtlval.node)->GetType() == BOOLEAN_TYPE) return FORMID_TOK; else return TERMID_TOK; diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y index 756ff3e..ccec390 100644 --- a/src/parser/smtlib.y +++ b/src/parser/smtlib.y @@ -37,7 +37,8 @@ #include "../AST/AST.h" using namespace std; - + using namespace BEEV; + // Suppress the bogus warning suppression in bison (it generates // compile error) #undef __GNUC_MINOR__ @@ -50,11 +51,11 @@ int yyerror(const char *s) { cout << "syntax error: line " << smtlineno << "\n" << s << endl; cout << " token: " << smttext << endl; - BEEV::FatalError(""); + FatalError(""); return 1; } - BEEV::ASTNode query; + ASTNode query; #define YYLTYPE_IS_TRIVIAL 1 #define YYMAXDEPTH 104857600 #define YYERROR_VERBOSE 1 @@ -204,18 +205,18 @@ cmd: benchmark { - BEEV::ASTNode assumptions; + ASTNode assumptions; if($1 == NULL) { - assumptions = BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE); + assumptions = GlobalBeevMgr->CreateNode(TRUE); } else { assumptions = *$1; } if(query.IsNull()) { - query = BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE); + query = GlobalBeevMgr->CreateNode(FALSE); } - BEEV::globalBeevMgr_for_parser->TopLevelSAT(assumptions, query); + GlobalBeevMgr->TopLevelSAT(assumptions, query); delete $1; YYACCEPT; @@ -227,9 +228,9 @@ benchmark: { if($4 != NULL){ if($4->size() > 1) - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND,*$4)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(AND,*$4)); else - $$ = new BEEV::ASTNode((*$4)[0]); + $$ = new ASTNode((*$4)[0]); delete $4; } else { @@ -250,10 +251,10 @@ bench_name: bench_attributes: bench_attribute { - $$ = new BEEV::ASTVec; + $$ = new ASTVec; if ($1 != NULL) { $$->push_back(*$1); - BEEV::globalBeevMgr_for_parser->AddAssert(*$1); + GlobalBeevMgr->AddAssert(*$1); delete $1; } } @@ -261,7 +262,7 @@ bench_attributes: { if ($1 != NULL && $2 != NULL) { $1->push_back(*$2); - BEEV::globalBeevMgr_for_parser->AddAssert(*$2); + GlobalBeevMgr->AddAssert(*$2); $$ = $1; delete $2; } @@ -326,16 +327,16 @@ logic_name: status: SAT_TOK { - BEEV::input_status = BEEV::TO_BE_SATISFIABLE; + input_status = TO_BE_SATISFIABLE; $$ = NULL; } | UNSAT_TOK { - BEEV::input_status = BEEV::TO_BE_UNSATISFIABLE; + input_status = TO_BE_UNSATISFIABLE; $$ = NULL; } | UNKNOWN_TOK { - BEEV::input_status = BEEV::TO_BE_UNKNOWN; + input_status = TO_BE_UNKNOWN; $$ = NULL; } ; @@ -405,7 +406,7 @@ var_decls: var_decl: LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK { - BEEV::_parser_symbol_table.insert(*$2); + _parser_symbol_table.insert(*$2); //Sort_symbs has the indexwidth/valuewidth. Set those fields in //var $2->SetIndexWidth($3.indexwidth); @@ -413,7 +414,7 @@ var_decl: } | LPAREN_TOK FORMID_TOK RPAREN_TOK { - BEEV::_parser_symbol_table.insert(*$2); + _parser_symbol_table.insert(*$2); //Sort_symbs has the indexwidth/valuewidth. Set those fields in //var $2->SetIndexWidth(0); @@ -424,7 +425,7 @@ var_decl: an_formulas: an_formula { - $$ = new BEEV::ASTVec; + $$ = new ASTVec; if ($1 != NULL) { $$->push_back(*$1); delete $1; @@ -444,13 +445,13 @@ an_formulas: an_formula: TRUE_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(TRUE)); $$->SetIndexWidth(0); $$->SetValueWidth(0); } | FALSE_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(FALSE)); $$->SetIndexWidth(0); $$->SetValueWidth(0); } @@ -461,8 +462,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateSimplifiedEQ(*$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -474,12 +475,12 @@ an_formula: ASTVec terms = *$3; ASTVec forms; - for(BEEV::ASTVec::const_iterator it=terms.begin(),itend=terms.end(); + for(ASTVec::const_iterator it=terms.begin(),itend=terms.end(); it!=itend; it++) { for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) { - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ, *it, *it2))); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(NOT, GlobalBeevMgr->CreateNode(EQ, *it, *it2))); - globalBeevMgr_for_parser->BVTypeCheck(*n); + GlobalBeevMgr->BVTypeCheck(*n); forms.push_back(*n); } @@ -489,8 +490,8 @@ an_formula: FatalError("empty distinct"); $$ = (forms.size() == 1) ? - new BEEV::ASTNode(forms[0]) : - new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND, forms)); + new ASTNode(forms[0]) : + new ASTNode(GlobalBeevMgr->CreateNode(AND, forms)); delete $3; } @@ -498,8 +499,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSLT, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -507,8 +508,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSLE, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -516,8 +517,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSGT, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -525,8 +526,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVSGE, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -534,8 +535,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVLT, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -543,8 +544,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVLE, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -552,8 +553,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVGT, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -561,8 +562,8 @@ an_formula: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(BVGE, *$3, *$4)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; delete $4; @@ -573,41 +574,41 @@ an_formula: } | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(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)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(IMPLIES, *$3, *$4)); delete $3; delete $4; } | LPAREN_TOK ITE_TOK an_formula an_formula an_formula RPAREN_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedFormulaITE(*$3, *$4, *$5)); + $$ = new ASTNode(GlobalBeevMgr->CreateSimplifiedFormulaITE(*$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)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(AND, *$3)); delete $3; } | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::OR, *$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(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)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(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)); + $$ = new ASTNode(GlobalBeevMgr->CreateNode(IFF, *$3, *$4)); delete $3; delete $4; } @@ -616,7 +617,7 @@ an_formula: { $$ = $2; //Cleanup the LetIDToExprMap - BEEV::globalBeevMgr_for_parser->CleanupLetIDMap(); + GlobalBeevMgr->CleanupLetIDMap(); } ; @@ -624,7 +625,7 @@ 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); + GlobalBeevMgr->BVTypeCheck(*$6); //set the valuewidth of the identifier $5->SetValueWidth($6->GetValueWidth()); @@ -638,21 +639,21 @@ letexpr_mgmt: // //2. Ensure that LET variables are not //2. defined more than once - BEEV::globalBeevMgr_for_parser->LetExprMgr(*$5,*$6); + GlobalBeevMgr->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); + GlobalBeevMgr->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); + GlobalBeevMgr->LetExprMgr(*$5,*$6); delete $5; delete $6; } @@ -660,7 +661,7 @@ letexpr_mgmt: an_terms: an_term { - $$ = new BEEV::ASTVec; + $$ = new ASTVec; if ($1 != NULL) { $$->push_back(*$1); delete $1; @@ -680,11 +681,11 @@ an_terms: an_term: BVCONST_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($1, 10, 32)); + $$ = new ASTNode(GlobalBeevMgr->CreateBVConst($1, 10, 32)); } | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($1,10,$3)); + $$ = new ASTNode(GlobalBeevMgr->CreateBVConst($1,10,$3)); delete $1; } | an_nonbvconst_term @@ -694,26 +695,26 @@ an_nonbvconst_term: BITCONST_TOK { $$ = $1; } | var { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + $$ = new ASTNode(GlobalBeevMgr->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)); + //$$ = new ASTNode(GlobalBeevMgr->SimplifyTerm(*$2)); //delete $2; } | SELECT_TOK an_term an_term { //ARRAY READ // valuewidth is same as array, indexwidth is 0. - BEEV::ASTNode array = *$2; - BEEV::ASTNode index = *$3; + ASTNode array = *$2; + 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); + ASTNode * n = + new ASTNode(GlobalBeevMgr->CreateTerm(READ, width, array, index)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -722,13 +723,13 @@ an_nonbvconst_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); + ASTNode array = *$2; + ASTNode index = *$3; + ASTNode writeval = *$4; + ASTNode write_term = GlobalBeevMgr->CreateTerm(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); + GlobalBeevMgr->BVTypeCheck(write_term); + ASTNode * n = new ASTNode(write_term); $$ = n; delete $2; delete $3; @@ -761,7 +762,7 @@ an_nonbvconst_term: /* val >>= low; */ /* // val is the desired BV32. */ -/* BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(width, val)); */ +/* ASTNode * n = new ASTNode(GlobalBeevMgr->CreateBVConst(width, val)); */ /* $$ = n; */ /* } */ | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term @@ -773,11 +774,11 @@ an_nonbvconst_term: if((unsigned)$3 >= $7->GetValueWidth()) 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(output); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode hi = GlobalBeevMgr->CreateBVConst(32, $3); + ASTNode low = GlobalBeevMgr->CreateBVConst(32, $5); + ASTNode output = GlobalBeevMgr->CreateTerm(BVEXTRACT, width, *$7,hi,low); + ASTNode * n = new ASTNode(output); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $7; } @@ -792,13 +793,13 @@ an_nonbvconst_term: 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)); + GlobalBeevMgr->BVTypeCheck(*$2); + GlobalBeevMgr->BVTypeCheck(*$3); + GlobalBeevMgr->BVTypeCheck(*$4); + $$ = new ASTNode(GlobalBeevMgr->CreateSimplifiedTermITE(*$2, *$3, *$4)); + //$$ = new ASTNode(GlobalBeevMgr->CreateTerm(ITE,width,*$2, *$3, *$4)); $$->SetIndexWidth($4->GetIndexWidth()); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$); + GlobalBeevMgr->BVTypeCheck(*$$); delete $2; delete $3; delete $4; @@ -806,8 +807,8 @@ an_nonbvconst_term: | 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; @@ -817,8 +818,8 @@ an_nonbvconst_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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVNEG, width, *$2)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; } @@ -826,8 +827,8 @@ an_nonbvconst_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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVUMINUS,width,*$2)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; } @@ -837,8 +838,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVAND, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -849,8 +850,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVOR, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -861,8 +862,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVXOR, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -873,8 +874,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVSUB, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -885,8 +886,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVPLUS, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -898,8 +899,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVMULT, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -911,8 +912,8 @@ an_nonbvconst_term: if (width != $3->GetValueWidth()) { yyerror("Width mismatch in BVDIV"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVDIV, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVDIV, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; @@ -924,8 +925,8 @@ an_nonbvconst_term: if (width != $3->GetValueWidth()) { yyerror("Width mismatch in BVMOD"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMOD, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVMOD, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; @@ -937,8 +938,8 @@ an_nonbvconst_term: if (width != $3->GetValueWidth()) { yyerror("Width mismatch in SBVDIV"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVDIV, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(SBVDIV, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; @@ -950,8 +951,8 @@ an_nonbvconst_term: if (width != $3->GetValueWidth()) { yyerror("Width mismatch in SBVREM"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVREM, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(SBVREM, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -962,8 +963,8 @@ an_nonbvconst_term: if (width != $3->GetValueWidth()) { yyerror("Width mismatch in SBVMOD"); } - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVMOD, width, *$2, *$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(SBVMOD, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -979,8 +980,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVNAND, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -991,8 +992,8 @@ an_nonbvconst_term: 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); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVNOR, width, *$2, *$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; delete $3; @@ -1001,25 +1002,25 @@ an_nonbvconst_term: { 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); + ASTNode trailing_zeros = GlobalBeevMgr->CreateBVConst($3, 0); + ASTNode hi = GlobalBeevMgr->CreateBVConst(32, w-$3-1); + ASTNode low = GlobalBeevMgr->CreateBVConst(32,0); + ASTNode m = GlobalBeevMgr->CreateTerm(BVEXTRACT,w-$3,*$2,hi,low); + ASTNode * n = + new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT,w,m,trailing_zeros)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; } else - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); + $$ = new ASTNode(GlobalBeevMgr->CreateBVConst(w,0)); delete $2; } | BVLEFTSHIFT_1_TOK an_term an_term { // shifting left by who know how much? unsigned int w = $2->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVLEFTSHIFT,w,*$2,*$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVLEFTSHIFT,w,*$2,*$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; } @@ -1027,30 +1028,30 @@ an_nonbvconst_term: { // shifting right by who know how much? unsigned int w = $2->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVRIGHTSHIFT,w,*$2,*$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; } | BVRIGHTSHIFT_TOK an_term NUMERAL_TOK { - BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst($3, 0); + ASTNode leading_zeros = GlobalBeevMgr->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); + ASTNode hi = GlobalBeevMgr->CreateBVConst(32,w-1); + ASTNode low = GlobalBeevMgr->CreateBVConst(32,$3); + ASTNode extract = GlobalBeevMgr->CreateTerm(BVEXTRACT,w-$3,*$2,hi,low); + ASTNode * n = + new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT, w,leading_zeros, extract)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; } else { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); + $$ = new ASTNode(GlobalBeevMgr->CreateBVConst(w,0)); } delete $2; } @@ -1058,16 +1059,16 @@ an_nonbvconst_term: { // shifting arithmetic right by who know how much? unsigned int w = $2->GetValueWidth(); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSRSHIFT,w,*$2,*$3)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateTerm(BVSRSHIFT,w,*$2,*$3)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $2; } | BVROTATE_LEFT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term { - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->BVTypeCheck(*$5); - BEEV::ASTNode *n; + ASTNode *n; unsigned width = $5->GetValueWidth(); unsigned rotate = $3; if (0 == rotate) @@ -1076,14 +1077,14 @@ an_nonbvconst_term: } else if (rotate < width) { - BEEV::ASTNode high = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-1); - BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0); - BEEV::ASTNode cut = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-rotate); - BEEV::ASTNode cutMinusOne = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-rotate-1); - - BEEV::ASTNode top = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,rotate,*$5,high, cut); - BEEV::ASTNode bottom = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,width-rotate,*$5,cutMinusOne,zero); - n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,width,bottom,top)); + ASTNode high = GlobalBeevMgr->CreateBVConst(32,width-1); + ASTNode zero = GlobalBeevMgr->CreateBVConst(32,0); + ASTNode cut = GlobalBeevMgr->CreateBVConst(32,width-rotate); + ASTNode cutMinusOne = GlobalBeevMgr->CreateBVConst(32,width-rotate-1); + + ASTNode top = GlobalBeevMgr->CreateTerm(BVEXTRACT,rotate,*$5,high, cut); + ASTNode bottom = GlobalBeevMgr->CreateTerm(BVEXTRACT,width-rotate,*$5,cutMinusOne,zero); + n = new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT,width,bottom,top)); delete $5; } else @@ -1092,15 +1093,15 @@ an_nonbvconst_term: yyerror("Rotate must be strictly less than the width."); } - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; } | BVROTATE_RIGHT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term { - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->BVTypeCheck(*$5); - BEEV::ASTNode *n; + ASTNode *n; unsigned width = $5->GetValueWidth(); unsigned rotate = $3; if (0 == rotate) @@ -1109,14 +1110,14 @@ an_nonbvconst_term: } else if (rotate < width) { - BEEV::ASTNode high = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,width-1); - BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0); - BEEV::ASTNode cut = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,rotate); - BEEV::ASTNode cutMinusOne = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,rotate-1); - - BEEV::ASTNode bottom = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,rotate,*$5,cutMinusOne, zero); - BEEV::ASTNode top = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,width-rotate,*$5,high,cut); - n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,width,bottom,top)); + ASTNode high = GlobalBeevMgr->CreateBVConst(32,width-1); + ASTNode zero = GlobalBeevMgr->CreateBVConst(32,0); + ASTNode cut = GlobalBeevMgr->CreateBVConst(32,rotate); + ASTNode cutMinusOne = GlobalBeevMgr->CreateBVConst(32,rotate-1); + + ASTNode bottom = GlobalBeevMgr->CreateTerm(BVEXTRACT,rotate,*$5,cutMinusOne, zero); + ASTNode top = GlobalBeevMgr->CreateTerm(BVEXTRACT,width-rotate,*$5,high,cut); + n = new ASTNode(GlobalBeevMgr->CreateTerm(BVCONCAT,width,bottom,top)); delete $5; } else @@ -1125,27 +1126,27 @@ an_nonbvconst_term: yyerror("Rotate must be strictly less than the width."); } - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; } | BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term { - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->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); + ASTNode width = GlobalBeevMgr->CreateBVConst(32,w); + ASTNode *n = new ASTNode(GlobalBeevMgr->CreateTerm(BVSX,w,*$5,width)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; } | BVZX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term { - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + GlobalBeevMgr->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::BVZX,w,*$5,width)); - BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + ASTNode width = GlobalBeevMgr->CreateBVConst(32,w); + ASTNode *n = new ASTNode(GlobalBeevMgr->CreateTerm(BVZX,w,*$5,width)); + GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $5; } @@ -1165,7 +1166,7 @@ sort_symb: $$.valuewidth = length; } else { - BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); } } | ARRAY_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK @@ -1176,14 +1177,14 @@ sort_symb: $$.indexwidth = $3; } else { - BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + 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"); + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); } } ; @@ -1191,12 +1192,12 @@ sort_symb: var: FORMID_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); delete $1; } | TERMID_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); delete $1; } | QUESTION_TOK TERMID_TOK @@ -1212,7 +1213,7 @@ fvar: } | FORMID_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); delete $1; } ; -- 2.47.3