From db60e10e8e7e575eb4e6d623fe1d61b48c3da52a Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Sun, 6 Sep 2009 23:41:17 +0000 Subject: [PATCH] changed regressall to regresscvc git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@198 e59a4935-1847-0410-ae03-e826735625c1 --- INSTALL | 2 +- README | 2 +- scripts/Makefile.in | 2 +- src/AST/AST.cpp | 2 +- src/AST/Transform.cpp | 3 ++- src/AST/printer/PLPrinter.cpp | 4 +--- src/parser/CVC.y | 18 +++++++++--------- src/parser/let-funcs.cpp | 11 +++++------ src/simplifier/simplifier.cpp | 6 +++++- 9 files changed, 26 insertions(+), 24 deletions(-) diff --git a/INSTALL b/INSTALL index c19d047..d869acb 100644 --- a/INSTALL +++ b/INSTALL @@ -22,7 +22,7 @@ 3. Run tests: - make regressall + make regresscvc NB: diff --git a/README b/README index ab02b5c..b3582e2 100644 --- a/README +++ b/README @@ -43,7 +43,7 @@ REGRESSIONS Assumes you have downloaded the testcases -make regressall +make regresscvc make regress_smt make regress_c_api make regressbigarray \ No newline at end of file diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 1f769ca..6c8beaa 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -77,7 +77,7 @@ REGRESS_LOG = `date +%Y-%m-%d`"-regress-cvc.log" PROGNAME=bin/stp ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) -.PHONY: regressall +.PHONY: regresscvc regressall: @echo "*********************************************************" \ | tee -a $(REGRESS_LOG) diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index c4d3ab6..72d7d03 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -802,7 +802,7 @@ namespace BEEV break; //case BVVARSHIFT: //case BVSRSHIFT: - break; + //break; default: break; } diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index 49cdf64..89646e1 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -253,14 +253,15 @@ namespace BEEV result = bm.CreateNode(k, vec); break; } + case FOR: default: if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType()) result = simpleForm; else { + FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k); cerr << "The input is: " << simpleForm << endl; cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl; - FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k); } break; } diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp index 2044c16..8bb7598 100644 --- a/src/AST/printer/PLPrinter.cpp +++ b/src/AST/printer/PLPrinter.cpp @@ -180,10 +180,8 @@ namespace printer PL_Print1(os, c[1], indentation, letize); os << ";"; PL_Print1(os, c[2], indentation, letize); - os << ";"; - PL_Print1(os, c[3], indentation, letize); os << "){ \n"; - PL_Print1(os, c[4], indentation, letize); + PL_Print1(os, c[3], indentation, letize); os << "} \n"; break; case BVLT: diff --git a/src/parser/CVC.y b/src/parser/CVC.y index af3439a..42ff10b 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -271,10 +271,6 @@ VarDecl : FORM_IDs ':' Type _parser_symbol_table.insert(*i); i->SetIndexWidth($3.indexwidth); i->SetValueWidth($3.valuewidth); - - //FIXME: HACK_ATTACK. this vector was hacked into the code to - //support a special request by Dawson' group. They want the - //counterexample to be printed in the order of variables declared. GlobalBeevMgr->ListOfDeclaredVars.push_back(*i); } delete $1; @@ -447,7 +443,7 @@ Formula : '(' Formula ')' { $$ = $2; } delete $1; delete $3; } - | FOR_TOK '(' TERMID_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}' + | FOR_TOK '(' FORMID_TOK ':' Type ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}' { //Allows a compact representation of //parameterized set of formulas (bounded @@ -462,20 +458,24 @@ Formula : '(' Formula ')' { $$ = $2; } //increment value (BVCONST) // //formula (it can be a nested forloop) + _parser_symbol_table.insert(*$3); + $3->SetIndexWidth($5.indexwidth); + $3->SetValueWidth($5.valuewidth); + ASTVec vec; vec.push_back(*$3); - vec.push_back(*$5); vec.push_back(*$7); vec.push_back(*$9); - vec.push_back(*$12); + vec.push_back(*$11); + vec.push_back(*$14); ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec)); GlobalBeevMgr->BVTypeCheck(*n); $$ = n; delete $3; - delete $5; delete $7; delete $9; - delete $12; + delete $11; + delete $14; } | NOT_TOK Formula { diff --git a/src/parser/let-funcs.cpp b/src/parser/let-funcs.cpp index 0f65e21..63f5a78 100644 --- a/src/parser/let-funcs.cpp +++ b/src/parser/let-funcs.cpp @@ -37,7 +37,7 @@ namespace BEEV { } (*_letid_expr_map)[var] = letExpr; - } + }//end of LetExprMgr() //this function looksup the "var to letexpr map" and returns the //corresponding letexpr. if there is no letexpr, then it simply @@ -57,10 +57,10 @@ namespace BEEV { ASTNodeMap::iterator it; if((it =_letid_expr_map->find(v)) != _letid_expr_map->end()) { if(it->second == ASTUndefined) - FatalError("Unresolved Identifier: ",v); + FatalError("ResolveID :: Unresolved Identifier: ",v); else return it->second; - } + }//end of ResolveID() //this is to mark the let-var as undefined. the let var is defined //only after the LetExprMgr has completed its work, and until then @@ -75,7 +75,6 @@ namespace BEEV { // This function simply cleans up the LetID -> LetExpr Map. void BeevMgr::CleanupLetIDMap(void) { - // ext/hash_map::clear() is very expensive on big empty lists. shortcut. if (_letid_expr_map->size() ==0) return; @@ -94,10 +93,10 @@ namespace BEEV { delete _letid_expr_map; _letid_expr_map = new ASTNodeMap(); - } + }//end of CleanupLetIDMap() void BeevMgr::InitializeLetIDMap(void) { _letid_expr_map = new ASTNodeMap(); - } + } //end of InitializeLetIDMap() }; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index c53a1ef..aeea77b 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -46,7 +46,11 @@ namespace BEEV if (pushNeg && (it = SimplifyMap->find(key)) != SimplifyMap->end()) { - output = (ASTFalse == it->second) ? ASTTrue : (ASTTrue == it->second) ? ASTFalse : CreateNode(NOT, it->second); + output = + (ASTFalse == it->second) ? + ASTTrue : + (ASTTrue == it->second) ? + ASTFalse : CreateNode(NOT, it->second); CountersAndStats("2nd_Successful_CheckSimplifyMap"); return true; } -- 2.47.3