From 27a821a2aba8c61024ff579fa664829dec9d2a29 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 4 Sep 2009 19:08:11 +0000 Subject: [PATCH] cleaned up FOR-construct parsing, and printing git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@186 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 2 +- src/AST/AbstractionRefinement.cpp | 32 +++++++++++++++------------- src/AST/Makefile | 2 +- src/AST/printer/AssortedPrinters.cpp | 12 +++++++++-- src/AST/printer/AssortedPrinters.h | 2 +- src/AST/printer/CPrinter.cpp | 9 ++++++++ src/AST/printer/LispPrinter.cpp | 9 ++++++++ src/AST/printer/PLPrinter.cpp | 22 +++++++++++++++++++ src/AST/printer/SMTLIBPrinter.cpp | 9 ++++++++ src/AST/printer/dotPrinter.cpp | 9 ++++++++ src/AST/printer/printers.h | 9 ++++++++ src/parser/CVC.y | 32 ++++++++++++++++++++-------- 12 files changed, 120 insertions(+), 29 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index 8c51e89..8cf5cbe 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1,6 +1,6 @@ // -*- c++ -*- /******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill + * AUTHORS: Vijay Ganesh * * BEGIN DATE: November, 2005 * diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp index 6622c76..aae3646 100644 --- a/src/AST/AbstractionRefinement.cpp +++ b/src/AST/AbstractionRefinement.cpp @@ -290,7 +290,7 @@ namespace BEEV //'value' for the same 'key' (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); } //end of While - } + } //end of recursion FORs ASTVec forloopFormulaVector; //Expand the leaf level FOR-construct completely @@ -303,19 +303,20 @@ namespace BEEV //Check the currentformula against the model, and add it to the //SAT solver if it is false against the model - if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) { - forloopFormulaVector.push_back(currentFormula); - ASTNode forloopFormulas = - (forloopFormulaVector.size() != 1) ? - CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; - - SOLVER_RETURN_TYPE result = - CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input); - if(result != SOLVER_UNDECIDED) - { - return result; - } - } + if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) + { + forloopFormulaVector.push_back(currentFormula); + ASTNode forloopFormulas = + (forloopFormulaVector.size() != 1) ? + CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; + + SOLVER_RETURN_TYPE result = + CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input); + if(result != SOLVER_UNDECIDED) + { + return result; + } + } //Update ParamToCurrentValMap with parameter and its current //value @@ -323,7 +324,8 @@ namespace BEEV //FIXME: Possible leak since I am not freeing the previous //'value' for the same 'key' (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); - } + } //end of expanding the FOR loop + return SOLVER_UNDECIDED; } //end of the SATBased_FiniteLoop_Refinement() diff --git a/src/AST/Makefile b/src/AST/Makefile index fb3ebd1..b9bedad 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -29,7 +29,7 @@ ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl clean: rm -rf *.o *~ bbtest asttest cnftest *.a ASTKind.h ASTKind.cpp .#* - rm -rf printer/*.o + rm -rf printer/*.o printer/*~ depend: makedepend -Y -- $(CFLAGS) -- $(SRCS) diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp index 73b22cb..7115ba3 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/AST/printer/AssortedPrinters.cpp @@ -6,6 +6,7 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ // -*- c++ -*- + #include "../AST.h" #include "AssortedPrinters.h" #include "printers.h" @@ -14,7 +15,7 @@ // to get the PRIu64 macro from inttypes, this needs to be defined. #define __STDC_FORMAT_MACROS #include -#undef __STDC_FORMAT_MACROS +//#undef __STDC_FORMAT_MACROS namespace BEEV { @@ -172,7 +173,14 @@ namespace BEEV { os << "ASSERT( "; f.PL_Print(os,0); - os << " = "; + if(BOOLEAN_TYPE == f.GetType()) + { + os << "<=>"; + } + else + { + os << " = "; + } if (BITVECTOR_TYPE == se.GetType()) { TermToConstTermUsingModel(se, false).PL_Print(os, 0); diff --git a/src/AST/printer/AssortedPrinters.h b/src/AST/printer/AssortedPrinters.h index bfaaef1..c887128 100644 --- a/src/AST/printer/AssortedPrinters.h +++ b/src/AST/printer/AssortedPrinters.h @@ -1,6 +1,6 @@ // -*- c++ -*- /******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill + * AUTHORS: Vijay Ganesh * * BEGIN DATE: November, 2005 * diff --git a/src/AST/printer/CPrinter.cpp b/src/AST/printer/CPrinter.cpp index f272b69..dfef1d8 100644 --- a/src/AST/printer/CPrinter.cpp +++ b/src/AST/printer/CPrinter.cpp @@ -1,3 +1,12 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + #include "printers.h" #include diff --git a/src/AST/printer/LispPrinter.cpp b/src/AST/printer/LispPrinter.cpp index 51bada5..ca49afe 100644 --- a/src/AST/printer/LispPrinter.cpp +++ b/src/AST/printer/LispPrinter.cpp @@ -1,3 +1,12 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + #include "printers.h" namespace printer diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp index b76515b..2044c16 100644 --- a/src/AST/printer/PLPrinter.cpp +++ b/src/AST/printer/PLPrinter.cpp @@ -1,3 +1,12 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + #include "printers.h" namespace printer @@ -164,6 +173,19 @@ namespace printer PL_Print1(os, c[2], indentation, letize); os << endl << "ENDIF"; break; + case FOR: + os << "FOR("; + PL_Print1(os, c[0], indentation, letize); + os << ";"; + 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); + os << "} \n"; + break; case BVLT: case BVLE: case BVGT: diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp index 15ca41e..1839e58 100644 --- a/src/AST/printer/SMTLIBPrinter.cpp +++ b/src/AST/printer/SMTLIBPrinter.cpp @@ -1,3 +1,12 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + #include "printers.h" #include diff --git a/src/AST/printer/dotPrinter.cpp b/src/AST/printer/dotPrinter.cpp index b2b24a0..1fdb0b7 100644 --- a/src/AST/printer/dotPrinter.cpp +++ b/src/AST/printer/dotPrinter.cpp @@ -1,3 +1,12 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + #include "printers.h" /* diff --git a/src/AST/printer/printers.h b/src/AST/printer/printers.h index 46c1e4f..06815f2 100644 --- a/src/AST/printer/printers.h +++ b/src/AST/printer/printers.h @@ -1,3 +1,12 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + #ifndef PRINTERS_H_ #define PRINTERS_H_ diff --git a/src/parser/CVC.y b/src/parser/CVC.y index 15b068d..293dc3c 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -442,21 +442,35 @@ Formula : '(' Formula ')' { $$ = $2; } delete $1; delete $3; } - | FOR_TOK '(' Formula ';' Formula ';' Formula ')' '{' Formula '}' + | FOR_TOK '(' TERMID_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}' { //Allows a compact representation of - //parameterized set of formulas + //parameterized set of formulas (bounded + //universal quantification) // - //$1 is the initialization (this is an AND of - //formulas of the form var = constant) + //parameter name (a variable) // - //$2 is the constant bounding (this is an AND - //of formulas of the form var < constant). + //initial value (BVCONST) // - //$3 is the increment (this is an AND of - //formulas of the form var = var + constant). + //limit value (BVCONST) // - //$4 is the parameterized formula + //increment value (BVCONST) + // + //formula (it can be a nested forloop) + BEEV::ASTVec vec; + vec.push_back(*$3); + vec.push_back(*$5); + vec.push_back(*$7); + vec.push_back(*$9); + vec.push_back(*$12); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FOR,vec)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + delete $7; + delete $9; + delete $12; } | NOT_TOK Formula { -- 2.47.3