$(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/
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
$(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/
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
// -*- c++ -*-
#include "AST.h"
-
#include <assert.h>
#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
////////////////////////////////////////////////////////////////
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;
}
#include <map>
#include <set>
#include <algorithm>
+#include "../main/Globals.h"
#include "ASTUtil.h"
#include "ASTKind.h"
#include <stdint.h>
#include <stdlib.h>
#include "../constantbv/constantbv.h"
-namespace MINISAT
-{
- class Solver;
- typedef int Var;
-}
-
/*****************************************************************************
* LIST OF CLASSES DECLARED IN THIS FILE:
*
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;
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<ASTNode> ASTVec;
typedef unsigned int * CBV;
extern ASTVec _empty_ASTVec;
- extern BeevMgr * globalBeevMgr_for_parser;
-
/***************************************************************************/
/* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */
/***************************************************************************/
// 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)
{
}
// 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)
{
}
// 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)
{
}
* BVGETBIT Node), and this maps allows us to assemble the bits
* into bitvectors.
*/
- typedef hash_map<ASTNode, hash_map<unsigned int, bool> *, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTtoBitvectorMap;
+ typedef hash_map<ASTNode,
+ hash_map<unsigned int, bool> *,
+ ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTtoBitvectorMap;
ASTtoBitvectorMap _ASTNode_to_Bitvector;
//Data structure that holds the counter-model
// 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;
// -*- c++ -*-
#include "ASTUtil.h"
+#include "../main/Globals.h"
namespace BEEV
{
ostream &operator<<(ostream &os, const Spacer &sp)
#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
//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
//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();
//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'
//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
//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;
//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
//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()
//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);
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
}
else
{
- //Control should never reach here
+ //Control should never reach here
PrintOutput(true);
return SOLVER_ERROR;
}
{
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);
{
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);
//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);
{
BeevMgr& bm = form.GetBeevMgr();
- assert(TransformMap != NULL);
+ assert(TransformMap != NULL);
ASTNode result;
ASTNode TransformTerm(const ASTNode& inputterm)
{
- assert(TransformMap != NULL);
+ assert(TransformMap != NULL);
BeevMgr& bm = inputterm.GetBeevMgr();
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;
}
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)
{
}
printer::PL_Print(cout,vv, 0);
cout << endl;
- }
-
+ } //end of Convert_MINISATVar_To_ASTNode_Print()
};//end of namespace BEEV
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()) {
BEEV::FatalError("");
}
- BEEV::globalBeevMgr_for_parser = b;
+ BEEV::GlobalBeevMgr = b;
CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
if(0 != c) {
--- /dev/null
+/********************************************************************
+ * 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
--- /dev/null
+// -*- 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 <iostream>
+#include <sstream>
+#include <string>
+#include <algorithm>
+#include <ctime>
+#include <unistd.h>
+#include <signal.h>
+#include <stdio.h>
+#include <unistd.h>
+
+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
--- /dev/null
+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 .#*
--- /dev/null
+/********************************************************************
+ * 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
#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
[\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;}
"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;
// -*- 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)
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 */
};
#define YYMAXDEPTH 10485760
#define YYERROR_VERBOSE 1
#define YY_EXIT_FAILURE -1
+
+#define YYPARSE_PARAM AssertsQuery
%}
%union {
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;
}
;
/* 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;
}
Assert : ASSERT_TOK Formula ';' { $$ = $2; }
;
-Query : QUERY_TOK Formula ';' { BEEV::globalBeevMgr_for_parser->AddQuery(*$2); $$ = $2;}
+Query : QUERY_TOK Formula ';' { GlobalBeevMgr->AddQuery(*$2); $$ = $2;}
;
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;
}
}
reverseFORM_IDs : FORMID_TOK
{
- $$ = new BEEV::ASTVec;
+ $$ = new ASTVec;
$$->push_back(*$1);
delete $1;
}
FORM_IDs : reverseFORM_IDs
{
- $$ = new BEEV::ASTVec($1->rbegin(),$1->rend());
+ $$ = new ASTVec($1->rbegin(),$1->rend());
delete $1;
}
;
$$.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
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;
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;
/* 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;
//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;
}
| 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;
| 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);
}
{
$$ = $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;
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;
/*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;
{
// 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;
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;
}
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;
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;
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;
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;
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;
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;
//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;
}
| 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;
}
| 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;
| 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;
}
| 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;
}
| 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;
}
| 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;
}
| 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;
{
$$ = $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;
}
Updates : '[' Expr ']' ASSIGN_TOK Expr
{
- $$ = new BEEV::ASTNodeMap();
+ $$ = new ASTNodeMap();
(*$$)[*$2] = *$5;
}
| Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr
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());
//
//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: ");
$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: ");
$1->SetIndexWidth($5->GetIndexWidth());
//Do LET-expr management
- BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$5);
+ GlobalBeevMgr->LetExprMgr(*$1,*$5);
delete $1;
delete $5;
}
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
+++ /dev/null
-/********************************************************************
- * AUTHORS: Vijay Ganesh
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#include <iostream>
-#include <sstream>
-#include <string>
-#include <algorithm>
-#include <ctime>
-#include <unistd.h>
-#include <signal.h>
-//#include <zlib.h>
-#include <stdio.h>
-#include "../AST/AST.h"
-#include "../sat/core/Solver.h"
-#include "../sat/core/SolverTypes.h"
-//#include "../sat/VarOrder.h"
-
-#include <unistd.h>
-
-#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
#include <iostream>
#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';
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
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;
};
"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;
#include "../AST/AST.h"
using namespace std;
-
+ using namespace BEEV;
+
// Suppress the bogus warning suppression in bison (it generates
// compile error)
#undef __GNUC_MINOR__
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
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;
{
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 {
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;
}
}
{
if ($1 != NULL && $2 != NULL) {
$1->push_back(*$2);
- BEEV::globalBeevMgr_for_parser->AddAssert(*$2);
+ GlobalBeevMgr->AddAssert(*$2);
$$ = $1;
delete $2;
}
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;
}
;
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);
}
| 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);
an_formulas:
an_formula
{
- $$ = new BEEV::ASTVec;
+ $$ = new ASTVec;
if ($1 != NULL) {
$$->push_back(*$1);
delete $1;
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);
}
| 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;
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);
}
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;
}
| 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;
| 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;
| 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;
| 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;
| 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;
| 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;
| 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;
| 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;
}
| 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;
}
{
$$ = $2;
//Cleanup the LetIDToExprMap
- BEEV::globalBeevMgr_for_parser->CleanupLetIDMap();
+ GlobalBeevMgr->CleanupLetIDMap();
}
;
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());
//
//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;
}
an_terms:
an_term
{
- $$ = new BEEV::ASTVec;
+ $$ = new ASTVec;
if ($1 != NULL) {
$$->push_back(*$1);
delete $1;
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
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;
{
//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;
/* 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
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;
}
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;
| 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;
{
//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;
}
{
//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;
}
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
{
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;
}
{
// 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;
}
{
// 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)
}
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
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)
}
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
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;
}
$$.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
$$.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");
}
}
;
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
}
| FORMID_TOK
{
- $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1));
+ $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1));
delete $1;
}
;
projects / francis / stp.git / commitdiff