Refactor. Less verbose.

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

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
index 9ee98a5b4bd9af2b7c2bc5bfdc75cc3b7d285e03..d3c9405ed08ee53ead1ca65a3eae9c32f2a84572 100644 (file)
--- a/src/parser/ParserInterface.h
+++ b/src/parser/ParserInterface.h
@@ -128,6 +128,19 @@ public:
           return bm.LookupSymbol(name.c_str());
        }
 
+    // Create the node, then "new" it.
+    ASTNode * newNode(const Kind k, const ASTNode& n0, const ASTNode& n1)
+    {
+      return newNode(CreateNode(k,n0,n1));
+    }
+
+    // Create the node, then "new" it.
+    ASTNode * newNode(const Kind k, const int width, const ASTNode& n0, const ASTNode& n1)
+    {
+      return newNode(nf->CreateTerm(k,width,n0,n1));
+    }
+
+
     // On testcase20 it took about 4.2 seconds to parse using the standard allocator and the pool allocator.
        ASTNode * newNode(const ASTNode& copyIn)
        {

diff --git a/src/parser/smt.y b/src/parser/smt.y
index c4dddbadf6031b2830c0ec134f6ff81bccf8d093..1e056dbc97aef55901da2feaf2841c45e8b9bfdc 100644 (file)
--- a/src/parser/smt.y
+++ b/src/parser/smt.y
@@ -514,7 +514,7 @@ TRUE_TOK
 | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSLT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSLT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSLT, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -522,7 +522,7 @@ TRUE_TOK
 | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSLE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSLE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSLE, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -530,7 +530,7 @@ TRUE_TOK
 | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSGT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSGT, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -538,7 +538,7 @@ TRUE_TOK
 | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVSGE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSGE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSGE, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -546,7 +546,7 @@ TRUE_TOK
 | LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVLT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVLT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVLT, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -554,7 +554,7 @@ TRUE_TOK
 | LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVLE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVLE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVLE, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -562,7 +562,7 @@ TRUE_TOK
 | LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVGT_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVGT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVGT, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -570,7 +570,7 @@ TRUE_TOK
 | LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK
   //| LPAREN_TOK BVGE_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVGE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVGE, *$3, *$4);
   $$ = n;
   delete $3;
   delete $4;      
@@ -586,7 +586,7 @@ TRUE_TOK
 }
 | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->CreateNode(IMPLIES, *$3, *$4));
+  $$ = parserInterface->newNode(IMPLIES, *$3, *$4);
   delete $3;
   delete $4;
 }
@@ -609,13 +609,13 @@ TRUE_TOK
 }
 | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->CreateNode(XOR, *$3, *$4));
+  $$ = parserInterface->newNode(XOR, *$3, *$4);
   delete $3;
   delete $4;
 }
 | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->CreateNode(IFF, *$3, *$4));
+  $$ = parserInterface->newNode(IFF, *$3, *$4);
   delete $3;
   delete $4;
 }
@@ -697,11 +697,8 @@ BITCONST_TOK { $$ = $1; }
   delete $1;
 }
 | LPAREN_TOK an_term RPAREN_TOK
-  //| LPAREN_TOK an_term annotations RPAREN_TOK
 {
   $$ = $2;
-  //$$ = new ASTNode(parserInterface->SimplifyTerm(*$2));
-  //delete $2;
 }
 | SELECT_TOK an_term an_term
 {
@@ -781,7 +778,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVAND_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVAND, width, *$2, *$3);
   $$ = n;
   delete $2;
   delete $3;
@@ -789,7 +786,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVOR_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3)); 
+  ASTNode * n = parserInterface->newNode(BVOR, width, *$2, *$3); 
   $$ = n;
   delete $2;
   delete $3;
@@ -797,7 +794,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVXOR_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVXOR, width, *$2, *$3));
+  ASTNode * n =parserInterface->newNode(BVXOR, width, *$2, *$3);
   $$ = n;
   delete $2;
   delete $3;
@@ -839,7 +836,7 @@ BITCONST_TOK { $$ = $1; }
 |  BVSUB_TOK an_term an_term 
 {
   const unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSUB, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVSUB, width, *$2, *$3);
   $$ = n;
   delete $2;
   delete $3;
@@ -863,7 +860,7 @@ BITCONST_TOK { $$ = $1; }
 |      BVDIV_TOK an_term an_term  
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVDIV, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVDIV, width, *$2, *$3);
   $$ = n;
 
   delete $2;
@@ -872,7 +869,7 @@ BITCONST_TOK { $$ = $1; }
 |      BVMOD_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMOD, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVMOD, width, *$2, *$3);
   $$ = n;
 
   delete $2;
@@ -881,7 +878,7 @@ BITCONST_TOK { $$ = $1; }
 |      SBVDIV_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVDIV, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(SBVDIV, width, *$2, *$3);
   $$ = n;
 
   delete $2;
@@ -890,7 +887,7 @@ BITCONST_TOK { $$ = $1; }
 |      SBVREM_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVREM, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(SBVREM, width, *$2, *$3);
   $$ = n;
   delete $2;
   delete $3;
@@ -898,7 +895,7 @@ BITCONST_TOK { $$ = $1; }
 |      SBVMOD_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVMOD, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(SBVMOD, width, *$2, *$3);
   $$ = n;
   delete $2;
   delete $3;
@@ -923,7 +920,7 @@ BITCONST_TOK { $$ = $1; }
 {
   // shifting left by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVLEFTSHIFT,w,*$2,*$3));
+  ASTNode * n = parserInterface->newNode(BVLEFTSHIFT,w,*$2,*$3);
   $$ = n;
   delete $2;
   delete $3;
@@ -932,7 +929,7 @@ BITCONST_TOK { $$ = $1; }
 {
   // shifting right by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3));
+  ASTNode * n = parserInterface->newNode(BVRIGHTSHIFT,w,*$2,*$3);
   $$ = n;
   delete $2;
   delete $3;
@@ -941,7 +938,7 @@ BITCONST_TOK { $$ = $1; }
 {
   // shifting arithmetic right by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSRSHIFT,w,*$2,*$3));
+  ASTNode * n = parserInterface->newNode(BVSRSHIFT,w,*$2,*$3);
   $$ = n;
   delete $2;
   delete $3;

diff --git a/src/parser/smt2.y b/src/parser/smt2.y
index 89114914231edfb9a440c116fd03bf2d65f515bd..429b51a388a126adf588bd9559077eee3a17b4e1 100644 (file)
--- a/src/parser/smt2.y
+++ b/src/parser/smt2.y
@@ -365,7 +365,7 @@ TRUE_TOK
 }
 | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(EQ,*$3, *$4));
+  ASTNode * n = parserInterface->newNode(EQ,*$3, *$4);
   $$ = n;
   parserInterface->deleteNode($3);
   parserInterface->deleteNode($4);      
@@ -422,56 +422,56 @@ TRUE_TOK
 }
 | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVSLT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSLT, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode($3);
   parserInterface->deleteNode($4);      
 }
 | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVSLE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSLE, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
 | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVSGT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSGT, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
 | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVSGE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVSGE, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
 | LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVLT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVLT, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
 | LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVLE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVLE, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
 | LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVGT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVGT, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
 | LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(BVGE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(BVGE, *$3, *$4);
   $$ = n;
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
@@ -487,7 +487,7 @@ TRUE_TOK
 }
 | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->CreateNode(IMPLIES, *$3, *$4));
+  $$ = parserInterface->newNode(IMPLIES, *$3, *$4);
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
@@ -510,13 +510,13 @@ TRUE_TOK
 }
 | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->CreateNode(XOR, *$3, *$4));
+  $$ = parserInterface->newNode(XOR, *$3, *$4);
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);
 }
 | LPAREN_TOK EQ_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->CreateNode(IFF, *$3, *$4));
+  $$ = parserInterface->newNode(IFF, *$3, *$4);
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);
 }
@@ -694,7 +694,7 @@ TERMID_TOK
 |  BVAND_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVAND, width, *$2, *$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -702,7 +702,7 @@ TERMID_TOK
 |  BVOR_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3)); 
+  ASTNode * n = parserInterface->newNode(BVOR, width, *$2, *$3); 
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -710,7 +710,7 @@ TERMID_TOK
 |  BVXOR_TOK an_term an_term 
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVXOR, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVXOR, width, *$2, *$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -745,7 +745,7 @@ TERMID_TOK
 |  BVSUB_TOK an_term an_term 
 {
   const unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVSUB, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVSUB, width, *$2, *$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -753,7 +753,7 @@ TERMID_TOK
 |  BVPLUS_TOK an_term an_term 
 {
   const unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVPLUS, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVPLUS, width, *$2, *$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -770,7 +770,7 @@ TERMID_TOK
 |      BVDIV_TOK an_term an_term  
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVDIV, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVDIV, width, *$2, *$3);
   $$ = n;
 
     parserInterface->deleteNode( $2);
@@ -779,7 +779,7 @@ TERMID_TOK
 |      BVMOD_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVMOD, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(BVMOD, width, *$2, *$3);
   $$ = n;
 
     parserInterface->deleteNode( $2);
@@ -788,7 +788,7 @@ TERMID_TOK
 |      SBVDIV_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(SBVDIV, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(SBVDIV, width, *$2, *$3);
   $$ = n;
 
     parserInterface->deleteNode( $2);
@@ -797,7 +797,7 @@ TERMID_TOK
 |      SBVREM_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(SBVREM, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(SBVREM, width, *$2, *$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -805,7 +805,7 @@ TERMID_TOK
 |      SBVMOD_TOK an_term an_term
 {
   unsigned int width = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(SBVMOD, width, *$2, *$3));
+  ASTNode * n = parserInterface->newNode(SBVMOD, width, *$2, *$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -830,7 +830,7 @@ TERMID_TOK
 {
   // shifting left by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVLEFTSHIFT,w,*$2,*$3));
+  ASTNode * n = parserInterface->newNode(BVLEFTSHIFT,w,*$2,*$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -839,7 +839,7 @@ TERMID_TOK
 {
   // shifting right by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3));
+  ASTNode * n = parserInterface->newNode(BVRIGHTSHIFT,w,*$2,*$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);
@@ -848,7 +848,7 @@ TERMID_TOK
 {
   // shifting arithmetic right by who know how much?
   unsigned int w = $2->GetValueWidth();
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateTerm(BVSRSHIFT,w,*$2,*$3));
+  ASTNode * n = parserInterface->newNode(BVSRSHIFT,w,*$2,*$3);
   $$ = n;
     parserInterface->deleteNode( $2);
     parserInterface->deleteNode( $3);