Improvement. Add a warning when parsing problems that use array extensionality.

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

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
index 83e7f91cd0f80f08a9fb18800e3fbe10f449b2b4..9ee98a5b4bd9af2b7c2bc5bfdc75cc3b7d285e03 100644 (file)
--- a/src/parser/ParserInterface.h
+++ b/src/parser/ParserInterface.h
@@ -22,6 +22,7 @@ class ParserInterface
 {
        STPMgr& bm;
        //boost::object_pool<ASTNode> node_pool;
+       bool alreadyWarned;
 
 public:
        LETMgr letMgr;
@@ -33,6 +34,7 @@ public:
          letMgr(bm.ASTUndefined)
        {
                assert(nf != NULL);
+               alreadyWarned = false;
        }
 
        const ASTVec GetAsserts(void)
@@ -61,6 +63,17 @@ public:
         return nf->CreateNode(kind,children);
     }
 
+    ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTNode n0, const BEEV::ASTNode n1)
+    {
+        if (n0.GetIndexWidth() > 0 && !alreadyWarned)
+          {
+            cerr << "Warning: Parsing a term that uses array extensionality. STP doesn't handle array extensionality." << endl;
+            alreadyWarned = true;
+          }
+        return nf->CreateNode(kind,n0,n1);
+    }
+
+
     // These belong in the node factory..
 
     //TERMS//

diff --git a/src/parser/smt.y b/src/parser/smt.y
index ed37d5230b5caf6675af650b94b3cd21403477a6..c4dddbadf6031b2830c0ec134f6ff81bccf8d093 100644 (file)
--- a/src/parser/smt.y
+++ b/src/parser/smt.y
@@ -236,7 +236,7 @@ LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
 {
   if($4 != NULL){
     if($4->size() > 1) 
-      $$ = new ASTNode(parserInterface->nf->CreateNode(AND,*$4));
+      $$ = new ASTNode(parserInterface->CreateNode(AND,*$4));
     else if($4->size() ==1)
       $$ = new ASTNode((*$4)[0]);
      else
@@ -478,9 +478,8 @@ TRUE_TOK
   $$ = $1;
 }
 | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
-  //| LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK
 {
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(EQ,*$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(EQ,*$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -495,7 +494,7 @@ TRUE_TOK
   for(ASTVec::const_iterator it=terms.begin(),itend=terms.end();
       it!=itend; it++) {
     for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) {
-      ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->nf->CreateNode(EQ, *it, *it2)));
+      ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->CreateNode(EQ, *it, *it2)));
 
           
       forms.push_back(n); 
@@ -507,7 +506,7 @@ TRUE_TOK
  
   $$ = (forms.size() == 1) ?
     new ASTNode(forms[0]) :
-    new ASTNode(parserInterface->nf->CreateNode(AND, forms));
+    new ASTNode(parserInterface->CreateNode(AND, forms));
 
   delete $3;
 }
@@ -515,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->nf->CreateNode(BVSLT, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSLT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -523,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->nf->CreateNode(BVSLE, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSLE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -531,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->nf->CreateNode(BVSGT, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSGT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -539,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->nf->CreateNode(BVSGE, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVSGE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -547,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->nf->CreateNode(BVLT, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVLT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -555,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->nf->CreateNode(BVLE, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVLE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -563,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->nf->CreateNode(BVGT, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVGT, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -571,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->nf->CreateNode(BVGE, *$3, *$4));
+  ASTNode * n = new ASTNode(parserInterface->CreateNode(BVGE, *$3, *$4));
   $$ = n;
   delete $3;
   delete $4;      
@@ -587,7 +586,7 @@ TRUE_TOK
 }
 | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->nf->CreateNode(IMPLIES, *$3, *$4));
+  $$ = new ASTNode(parserInterface->CreateNode(IMPLIES, *$3, *$4));
   delete $3;
   delete $4;
 }
@@ -600,23 +599,23 @@ TRUE_TOK
 }
 | LPAREN_TOK AND_TOK an_formulas RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->nf->CreateNode(AND, *$3));
+  $$ = new ASTNode(parserInterface->CreateNode(AND, *$3));
   delete $3;
 }
 | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->nf->CreateNode(OR, *$3));
+  $$ = new ASTNode(parserInterface->CreateNode(OR, *$3));
   delete $3;
 }
 | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->nf->CreateNode(XOR, *$3, *$4));
+  $$ = new ASTNode(parserInterface->CreateNode(XOR, *$3, *$4));
   delete $3;
   delete $4;
 }
 | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = new ASTNode(parserInterface->nf->CreateNode(IFF, *$3, *$4));
+  $$ = new ASTNode(parserInterface->CreateNode(IFF, *$3, *$4));
   delete $3;
   delete $4;
 }

diff --git a/src/parser/smt2.y b/src/parser/smt2.y
index 8371880cb4c8f9824c764a2f3fd40adc1c202bea..89114914231edfb9a440c116fd03bf2d65f515bd 100644 (file)
--- a/src/parser/smt2.y
+++ b/src/parser/smt2.y
@@ -197,7 +197,7 @@ cmd: commands END
     }  
         
        if (assertionsSMT2.size() > 1)
-       ((ASTVec*)AssertsQuery)->push_back(parserInterface->nf->CreateNode(AND,assertionsSMT2));
+       ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(AND,assertionsSMT2));
        else if (assertionsSMT2.size() > 0)
        ((ASTVec*)AssertsQuery)->push_back((assertionsSMT2[0]));
        else
@@ -365,7 +365,7 @@ TRUE_TOK
 }
 | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateNode(EQ,*$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(EQ,*$3, *$4));
   $$ = n;
   parserInterface->deleteNode($3);
   parserInterface->deleteNode($4);      
@@ -380,7 +380,7 @@ TRUE_TOK
   for(ASTVec::const_iterator it=terms.begin(),itend=terms.end();
       it!=itend; it++) {
     for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) {
-      ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->nf->CreateNode(EQ, *it, *it2)));
+      ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->CreateNode(EQ, *it, *it2)));
 
           
       forms.push_back(n); 
@@ -392,7 +392,7 @@ TRUE_TOK
  
   $$ = (forms.size() == 1) ?
     parserInterface->newNode(forms[0]) :
-    parserInterface->newNode(parserInterface->nf->CreateNode(AND, forms));
+    parserInterface->newNode(parserInterface->CreateNode(AND, forms));
 
   delete $3;
 }
@@ -406,7 +406,7 @@ TRUE_TOK
   for(ASTVec::const_iterator it=terms.begin(),itend=terms.end();
       it!=itend; it++) {
     for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) {
-      ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->nf->CreateNode(IFF, *it, *it2)));
+      ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->CreateNode(IFF, *it, *it2)));
       forms.push_back(n); 
     }
   }
@@ -416,62 +416,62 @@ TRUE_TOK
  
   $$ = (forms.size() == 1) ?
     parserInterface->newNode(forms[0]) :
-    parserInterface->newNode(parserInterface->nf->CreateNode(AND, forms));
+    parserInterface->newNode(parserInterface->CreateNode(AND, forms));
 
   delete $3;
 }
 | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
 {
-  ASTNode * n = parserInterface->newNode(parserInterface->nf->CreateNode(BVSLT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(BVSLE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(BVSGT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(BVSGE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(BVLT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(BVLE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(BVGT, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(BVGE, *$3, *$4));
+  ASTNode * n = parserInterface->newNode(parserInterface->CreateNode(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->nf->CreateNode(IMPLIES, *$3, *$4));
+  $$ = parserInterface->newNode(parserInterface->CreateNode(IMPLIES, *$3, *$4));
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);      
 }
@@ -500,23 +500,23 @@ TRUE_TOK
 }
 | LPAREN_TOK AND_TOK an_formulas RPAREN_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->nf->CreateNode(AND, *$3));
+  $$ = parserInterface->newNode(parserInterface->CreateNode(AND, *$3));
   delete $3;
 }
 | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->nf->CreateNode(OR, *$3));
+  $$ = parserInterface->newNode(parserInterface->CreateNode(OR, *$3));
   delete $3;
 }
 | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->nf->CreateNode(XOR, *$3, *$4));
+  $$ = parserInterface->newNode(parserInterface->CreateNode(XOR, *$3, *$4));
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);
 }
 | LPAREN_TOK EQ_TOK an_formula an_formula RPAREN_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->nf->CreateNode(IFF, *$3, *$4));
+  $$ = parserInterface->newNode(parserInterface->CreateNode(IFF, *$3, *$4));
   parserInterface->deleteNode( $3);
   parserInterface->deleteNode( $4);
 }