diff options
Diffstat (limited to 'stp/parser/main.cpp')
| -rw-r--r-- | stp/parser/main.cpp | 181 |
1 files changed, 181 insertions, 0 deletions
diff --git a/stp/parser/main.cpp b/stp/parser/main.cpp new file mode 100644 index 00000000..ed251ed3 --- /dev/null +++ b/stp/parser/main.cpp @@ -0,0 +1,181 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * 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 "parsePL_defs.h" +#include "../sat/Solver.h" +#include "../sat/SolverTypes.h" +#include "../sat/VarOrder.h" + +#include <unistd.h> + +#ifdef EXT_HASH_MAP + using namespace __gnu_cxx; +#endif + +/* GLOBAL FUNCTION: parser + */ +extern int yyparse(); +//extern int smtlibparse(); + +/* 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; + +// Used only in smtlib lexer/parser +BEEV::ASTNode SingleBitOne; +BEEV::ASTNode SingleBitZero; + +/****************************************************************************** + * 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 *yyin; + + // 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 += "-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 += "-x : flatten nested XORs\n"; + helpstring += "-h : help\n"; + + for(int i=1; i < argc;i++) { + if(argv[i][0] == '-') + switch(argv[i][1]) { + case 'a' : + BEEV::optimize = false; + BEEV::wordlevel_solve = false; + break; + case 'b': + BEEV::print_STPinput_back = true; + break; + case 'c': + BEEV::construct_counterexample = true; + break; + case 'd': + BEEV::construct_counterexample = true; + BEEV::check_counterexample = true; + break; + case 'e': + BEEV::variable_activity_optimize = true; + break; + case 'f': + BEEV::smtlib_parser_enable = true; + break; + case 'h': + fprintf(stderr,usage,prog); + cout << helpstring; + //BEEV::FatalError(""); + return -1; + break; + case 'l' : + BEEV::linear_search = true; + break; + case 'n': + BEEV::print_output = true; + break; + case 'p': + BEEV::print_counterexample = true; + break; + case 'q': + BEEV::print_arrayval_declaredorder = true; + break; + case 'r': + BEEV::arrayread_refinement = false; + break; + case 's' : + BEEV::stats = true; + break; + case 'u': + BEEV::arraywrite_refinement = false; + break; + case 'v' : + BEEV::print_nodes = true; + break; + case 'w': + BEEV::wordlevel_solve = false; + break; + case 'x': + BEEV::xor_flatten = true; + break; + case 'z': + BEEV::print_sat_varorder = true; + break; + default: + fprintf(stderr,usage,prog); + cout << helpstring; + //BEEV::FatalError(""); + return -1; + break; + } + else { + infile = argv[i]; + yyin = fopen(infile,"r"); + if(yyin == NULL) { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + BEEV::FatalError(""); + } + } + } + +#ifdef NATIVE_C_ARITH +#else + CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); + if(0 != c) { + cout << CONSTANTBV::BitVector_Error(c) << endl; + return 0; + } +#endif + + //want to print the output always from the commandline. + BEEV::print_output = true; + BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr(); + + SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); + SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); + //BEEV::smtlib_parser_enable = true; + yyparse(); +}//end of Main |