From c9783f7525a03c4d24eb910204f0287ebd709bfb Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 20 Apr 2011 13:35:50 +0000 Subject: [PATCH] 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 --- src/parser/ParserInterface.h | 13 ++++++++++++ src/parser/smt.y | 35 ++++++++++++++++----------------- src/parser/smt2.y | 38 ++++++++++++++++++------------------ 3 files changed, 49 insertions(+), 37 deletions(-) diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h index 83e7f91..9ee98a5 100644 --- a/src/parser/ParserInterface.h +++ b/src/parser/ParserInterface.h @@ -22,6 +22,7 @@ class ParserInterface { STPMgr& bm; //boost::object_pool 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 ed37d52..c4dddba 100644 --- 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 8371880..8911491 100644 --- 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); } -- 2.47.3