* Fixed Mac OS X compilation bug. (pull out sys/time.h from MINISAT namespace)

* Added Verilog style literals (16'd777)
* Added time out flag (-g 5, time out after 5s)

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@343 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 499bebada662b2c7a846345efcb20e02ff002f5d..b585b3e5c2accc1616a8c44263d106a36e8fdef2 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -20,6 +20,13 @@ using namespace BEEV;
 extern int smtparse(void*);
 extern int cvcparse(void*);
 
+// callback for SIGALRM.
+void handle_time_out(int parameter){
+   printf("Timed Out.\n");
+   exit(0);
+}
+
+
 // Amount of memory to ask for at beginning of main.
 static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
 /********************************************************************
@@ -52,6 +59,7 @@ int main(int argc, char ** argv) {
   ToSAT * tosat      = new ToSAT(bm, simp);
   AbsRefine_CounterExample * Ctr_Example = 
     new AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat);      
+  itimerval timeout; 
 
   ParserBM          = bm;
   GlobalSTP         = 
@@ -77,6 +85,8 @@ int main(int argc, char ** argv) {
     "-e  : expand finite-for construct\n";
   helpstring +=  
     "-f  : number of abstraction-refinement loops\n";
+  helpstring +=  
+    "-g  : timeout (seconds until STP gives up)\n";
   helpstring +=  
     "-h  : help\n";
   helpstring +=  
@@ -134,6 +144,14 @@ int main(int argc, char ** argv) {
               bm->UserFlags.num_absrefine_flag = true;
               bm->UserFlags.num_absrefine = atoi(argv[++i]);
               break;            
+            case 'g':
+              signal(SIGVTALRM, handle_time_out);
+              timeout.it_interval.tv_usec = 0;
+              timeout.it_interval.tv_sec  = 0;
+              timeout.it_value.tv_usec    = 0;
+              timeout.it_value.tv_sec     = atoi(argv[++i]);
+              setitimer(ITIMER_VIRTUAL, &timeout, NULL);
+              break;            
             case 'h':
               fprintf(stderr,usage,prog);
               cout << helpstring;

diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex
index ee6b990c6b4e2b4508a35c2513a712865c52dc67..fd0fc9dc18f8afaff2fc2fa1aa4c1c2350c001c3 100644 (file)
--- a/src/parser/CVC.lex
+++ b/src/parser/CVC.lex
@@ -42,6 +42,9 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 0h{HEX}+         { cvclval.node = new BEEV::ASTNode(BEEV::ParserBM->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;}
 0hex{HEX}+       { cvclval.node = new BEEV::ASTNode(BEEV::ParserBM->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;}
 {DIGIT}+        { cvclval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;}
+\'b[0-1]+ { cvclval.str = strdup(yytext+2); return BIN_BASED_NUMBER;}
+\'d[0-9]+ { cvclval.str = strdup(yytext+2); return DEC_BASED_NUMBER;}
+\'h[0-9a-fA-F]+ { cvclval.str = strdup(yytext+2); return HEX_BASED_NUMBER;}
 
 "%"             { BEGIN COMMENT;}
 <COMMENT>"\n"   { BEGIN INITIAL; /* return to normal mode */}

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 790a4f5263ffeb8d6161fb300ef8e925ccd3c099..6026f857c80db10d4e83aaa4a9326f659d290ce2 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -49,6 +49,7 @@
   //ASTNode,ASTVec
   BEEV::ASTNode *node;
   BEEV::ASTVec *vec;
+  char* str;
 
   //Hash_Map to hold Array Updates during parse A map from array index
   //to array values. To support the WITH construct
@@ -166,6 +167,9 @@
 %token <node> BVCONST_TOK
 %token <node> TERMID_TOK FORMID_TOK COUNTEREXAMPLE_TOK
 %token <uintval> NUMERAL_TOK
+%token <str> BIN_BASED_NUMBER
+%token <str> DEC_BASED_NUMBER
+%token <str> HEX_BASED_NUMBER
 
 %%
 
@@ -718,6 +722,24 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
   $$ = new ASTNode(ParserBM->CreateTerm(ITE,1,*$3,one,zero));
   delete $3;
 }
+| NUMERAL_TOK BIN_BASED_NUMBER 
+{ 
+  std::string* vals = new std::string($2);
+  $$ = new ASTNode(ParserBM->CreateBVConst(vals, 2, $1));
+  free($2); delete vals;
+}
+| NUMERAL_TOK DEC_BASED_NUMBER
+{ 
+  std::string* vals = new std::string($2);
+  $$ = new ASTNode(ParserBM->CreateBVConst(vals, 10, $1));
+  free($2); delete vals;
+}
+| NUMERAL_TOK HEX_BASED_NUMBER 
+{ 
+  std::string* vals = new std::string($2);
+  $$ = new ASTNode(ParserBM->CreateBVConst(vals, 16, $1));
+  free($2); delete vals;
+}
 |      Expr '[' Expr ']' 
 {                        
   // valuewidth is same as array, indexwidth is 0.

diff --git a/src/sat/core/Solver.h b/src/sat/core/Solver.h
index 25507117114e388abd53797a9ecd2e421da01219..db67797284296e7467cd54adf49bf4c5a1e1eb0b 100644 (file)
--- a/src/sat/core/Solver.h
+++ b/src/sat/core/Solver.h
@@ -29,19 +29,24 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "SolverTypes.h"
 
-namespace MINISAT {
-   
-/*************************************************************************************/
 #ifdef _MSC_VER
 #include <ctime>
 
-static inline double cpuTime(void) {
-    return (double)clock() / CLOCKS_PER_SEC; }
 #else
 
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
+#endif
+
+namespace MINISAT {
+   
+/*************************************************************************************/
+#ifdef _MSC_VER
+
+static inline double cpuTime(void) {
+    return (double)clock() / CLOCKS_PER_SEC; }
+#else
 
 static inline double cpuTime(void) {
     struct rusage ru;