From eaab1611e5dc8209ae24fbeecfd361109be42bfd Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 10 Mar 2010 05:09:20 +0000 Subject: [PATCH] * Fix the SMT-LIB format printer so that it produces correct output. STP can now function as a CVC to SMT-LIB translator. * Cleanup the CVC format printer. * Bugfix in the CVC format printer. Add brackets to some unary operations to enforce the correct precedence. * Remove a un-unsed parameter from the CVC print-back. To isolate the bug in the CVC format printer I used Robert Brummayer's excellent delta-debugger. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@635 e59a4935-1847-0410-ae03-e826735625c1 --- src/main/main.cpp | 2 +- src/printer/AssortedPrinters.cpp | 2 +- src/printer/AssortedPrinters.h | 2 +- src/printer/PLPrinter.cpp | 196 ++++++++++++++------------- src/printer/SMTLIBPrinter.cpp | 218 ++++++++++++++++++++++--------- 5 files changed, 254 insertions(+), 166 deletions(-) diff --git a/src/main/main.cpp b/src/main/main.cpp index 1122d0c..cf7c484 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -289,7 +289,7 @@ int main(int argc, char ** argv) { } else { - print_STPInput_Back(asserts, query); + print_STPInput_Back(query); } return 0; } //end of PrintBack if diff --git a/src/printer/AssortedPrinters.cpp b/src/printer/AssortedPrinters.cpp index 4b0ece8..d332bbf 100644 --- a/src/printer/AssortedPrinters.cpp +++ b/src/printer/AssortedPrinters.cpp @@ -129,7 +129,7 @@ namespace BEEV } } - void print_STPInput_Back(const ASTNode& asserts, const ASTNode& query) { + void print_STPInput_Back(const ASTNode& query) { (BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout); (BEEV::GlobalSTP->bm)->printAssertsToStream(cout,0); cout << "QUERY("; diff --git a/src/printer/AssortedPrinters.h b/src/printer/AssortedPrinters.h index 3f8f872..90d0dc8 100644 --- a/src/printer/AssortedPrinters.h +++ b/src/printer/AssortedPrinters.h @@ -75,6 +75,6 @@ namespace BEEV void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision, int polarity=0); - void print_STPInput_Back(const ASTNode& asserts, const ASTNode& query); + void print_STPInput_Back(const ASTNode& query); };// end of namespace BEEV #endif diff --git a/src/printer/PLPrinter.cpp b/src/printer/PLPrinter.cpp index 3073c97..d6c791e 100644 --- a/src/printer/PLPrinter.cpp +++ b/src/printer/PLPrinter.cpp @@ -1,6 +1,6 @@ // -*- c++ -*- /******************************************************************** - * AUTHORS: Vijay Ganesh + * AUTHORS: Vijay Ganesh, Trevor Hansen * * BEGIN DATE: November, 2005 * @@ -12,8 +12,68 @@ namespace printer { - using std::string; - using namespace BEEV; +using std::string; +using namespace BEEV; + +string functionToCVCName(const Kind k) { + switch (k) { + + case BVUMINUS: + case NOT: + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + case BVMULT: + case AND: + case OR: + case NAND: + case NOR: + case XOR: + case BVSUB: + case BVPLUS: + case SBVDIV: + case SBVREM: + case BVDIV: + case BVMOD: + return _kind_names[k]; + break; + case BVSLT: + return "SBVLT"; + case BVSLE: + return "SBVLE"; + case BVSGT: + return "SBVGT"; + case BVSGE: + return "SBVGE"; + case IFF: + return "<=>"; + case IMPLIES: + return "=>"; + case BVNEG: + return "~"; + case EQ: + return "="; + case BVCONCAT: + return "@"; + case BVOR: + return "|"; + case BVAND: + return "&"; + case BVRIGHTSHIFT: + return ">>"; + default: { + cerr << "Unknown name when outputting:"; + FatalError(_kind_names[k]); + return ""; // to quieten compiler/ + } + } +} + void PL_Print1(ostream& os, const ASTNode& n,int indentation, bool letize) { @@ -45,7 +105,7 @@ namespace printer } //otherwise print it normally - Kind kind = n.GetKind(); + const Kind kind = n.GetKind(); const ASTVec &c = n.GetChildren(); switch (kind) { @@ -90,40 +150,14 @@ namespace printer os << endl; break; case BVUMINUS: - os << kind << "( "; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - break; case NOT: - os << "NOT("; - PL_Print1(os, c[0], indentation, letize); - os << ") " << endl; - break; case BVNEG: - os << " ~("; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - break; - case BVCONCAT: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " @ "; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; - case BVOR: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " | "; - PL_Print1(os, c[1], indentation, letize); - os << ")"; - break; - case BVAND: - os << "("; + assert(1 == c.size()); + os << "( "; + os << functionToCVCName(kind); + os << "( "; PL_Print1(os, c[0], indentation, letize); - os << " & "; - PL_Print1(os, c[1], indentation, letize); - os << ")"; + os << "))"; break; case BVEXTRACT: PL_Print1(os, c[0], indentation, letize); @@ -137,24 +171,26 @@ namespace printer os << "("; PL_Print1(os, c[0], indentation, letize); os << " << "; + if (!c[1].isConstant()) + { + FatalError("PL_Print1: The shift argument to a left shift must be a constant. Found:",c[1]); + } os << GetUnsignedConst(c[1]); os << ")"; + os << "["; + os << (c[0].GetValueWidth()-1); + os << " : " << "0]"; + break; - case BVRIGHTSHIFT: - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << " >> "; - os << GetUnsignedConst(c[1]); - os << ")"; - break; - case BVMULT: + + case BVMULT: // variable arity, function name at front, size next, comma separated. case BVSUB: case BVPLUS: case SBVDIV: case SBVREM: case BVDIV: case BVMOD: - os << kind << "("; + os << functionToCVCName(kind) << "("; os << n.GetValueWidth(); for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) @@ -204,7 +240,8 @@ namespace printer os << "} \n"; } break; - case BVLT: + + case BVLT: // two arity, prefixed function name. case BVLE: case BVGT: case BVGE: @@ -212,47 +249,28 @@ namespace printer case BVNAND: case BVNOR: case BVXNOR: - os << kind << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; case BVSLT: - os << "SBVLT" << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; case BVSLE: - os << "SBVLE" << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; case BVSGT: - os << "SBVGT" << "("; - PL_Print1(os, c[0], indentation, letize); - os << ","; - PL_Print1(os, c[1], indentation, letize); - os << ")" << endl; - break; case BVSGE: - os << "SBVGE" << "("; + assert(2 == c.size()); + os << functionToCVCName(kind) << "("; PL_Print1(os, c[0], indentation, letize); os << ","; PL_Print1(os, c[1], indentation, letize); os << ")" << endl; break; + + case BVCONCAT: // two arity, infix function name. + case BVOR: + case BVAND: + case BVRIGHTSHIFT: case EQ: - PL_Print1(os,c[0], indentation, letize); - os << " = "; - PL_Print1(os, c[1], indentation, letize); - os << endl; - break; - case AND: + case IFF: + case IMPLIES: + assert(2 == c.size()); + // run on. + case AND: // variable arity, infix function name. case OR: case NAND: case NOR: @@ -266,37 +284,13 @@ namespace printer it++; for (; it != itend; it++) { - os << " " << kind << " "; + os << " " << functionToCVCName(kind) << " "; PL_Print1(os, *it, indentation, letize); os << endl; } os << ")"; break; } - case IFF: - os << "("; - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - os << " <=> "; - os << "("; - PL_Print1(os,c[1], indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; - case IMPLIES: - os << "("; - os << "("; - PL_Print1(os, c[0], indentation, letize); - os << ")"; - os << " => "; - os << "("; - PL_Print1(os, c[1], indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; case BVSX: case BVZX: os << kind << "("; diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index 7d32058..9296111 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -1,7 +1,7 @@ /******************************************************************** - * AUTHORS: Vijay Ganesh + * AUTHORS: Trevor Hansen, Vijay Ganesh * - * BEGIN DATE: November, 2005 + * BEGIN DATE: July, 2009 * * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ @@ -9,11 +9,11 @@ #include "printers.h" #include +#include -// todo : fix lets. -// : Finish mapping function names from internal names to SMTLIB names. -// : build proper headers for PrintBack -// : Letize code for each printer should be merged. +// Outputs in the SMTLIB format. If you want something that can be parsed by other tools call +// SMTLIB_PrintBack(). SMTLIB_Print() prints just an expression. +// Wierdly is seems that only terms, not formulas can be LETized. namespace printer { @@ -21,6 +21,11 @@ namespace printer using std::string; using namespace BEEV; + string functionToSMTLIBName(const BEEV::Kind k); + void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); + void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os); + + static string tolower(const char * name) { string s(name); @@ -29,42 +34,67 @@ namespace printer return s; } - string functionToSMTLIBName(const BEEV::Kind k); - void SMTLIB_Print1(ostream& os, - const BEEV::ASTNode n, - int indentation, bool letize); - void printVarDeclsToStream( const STPMgr* mgr, ostream &os); +//Map from ASTNodes to LetVars +ASTNodeMap NodeLetVarMap; + +//This is a vector which stores the Node to LetVars pairs. It +//allows for sorted printing, as opposed to NodeLetVarMap +std::vector > NodeLetVarVec; + +//a partial Map from ASTNodes to LetVars. Needed in order to +//correctly print shared subterms inside the LET itself +ASTNodeMap NodeLetVarMap1; + +void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited, + ASTNodeSet& symbols) +{ + if (visited.find(n) != visited.end()) + return; // already visited. + + visited.insert(n); + + if (n.GetKind() == SYMBOL) + { + symbols.insert(n); + } + + for (unsigned i = 0; i < n.GetChildren().size(); i++) + buildListOfSymbols(n[i], visited, symbols); +} // Initial version intended to print the whole thing back. - void SMTLIB_PrintBack(ostream &os, const ASTNode& n) { - // need to add fake headers into here. +void SMTLIB_PrintBack(ostream &os, const ASTNode& n) +{ os << "(" << endl; os << "benchmark blah" << endl; - os << ":logic QF_BV" << endl; - printVarDeclsToStream(n.GetSTPMgr(),os); - os << ":formula" << endl; + os << ":logic QF_AUFBV" << endl; + ASTNodeSet visited, symbols; + buildListOfSymbols(n, visited, symbols); + printVarDeclsToStream(symbols, os); + os << ":formula "; SMTLIB_Print(os, n, 0); os << ")" << endl; } - void printVarDeclsToStream( const STPMgr* mgr, ostream &os) { - for(ASTVec::const_iterator i = mgr->ListOfDeclaredVars.begin(), - iend=mgr->ListOfDeclaredVars.end();i!=iend;i++) { +void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) +{ + for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i + != iend; i++) + { const BEEV::ASTNode& a = *i; // Should be a symbol. assert(a.GetKind()== SYMBOL); - switch(a.GetType()) { + switch (a.GetType()) + { case BEEV::BITVECTOR_TYPE: os << ":extrafuns (( "; a.nodeprint(os); - //os << " bv[" << a.GetValueWidth() << "]"; os << " BitVec[" << a.GetValueWidth() << "]"; os << " ))" << endl; break; - case BEEV::ARRAY_TYPE: os << ":extrafuns (( "; a.nodeprint(os); @@ -85,7 +115,7 @@ namespace printer void outputBitVec(const ASTNode n, ostream& os) { - Kind k = n.GetKind(); + const Kind k = n.GetKind(); const ASTVec &c = n.GetChildren(); ASTNode op; @@ -104,10 +134,8 @@ namespace printer // Prepend with zero to convert to unsigned. os << "bv"; - CBV unsign = - CONSTANTBV:: - BitVector_Concat((n.GetSTPMgr())->CreateZeroConst(1).GetBVConst(), - op.GetBVConst()); + CBV unsign = CONSTANTBV::BitVector_Concat( + n.GetSTPMgr()->CreateZeroConst(1).GetBVConst(), op.GetBVConst()); unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign); CONSTANTBV::BitVector_Destroy(unsign); os << str << "[" << op.GetValueWidth() << "]"; @@ -125,26 +153,24 @@ namespace printer } //if this node is present in the letvar Map, then print the letvar - STPMgr * bm = n.GetSTPMgr(); - //this is to print letvars for shared subterms inside the printing //of "(LET v0 = term1, v1=term1@term2,... - if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize) + if ((NodeLetVarMap1.find(n) != NodeLetVarMap1.end()) && !letize) { - SMTLIB_Print1(os, (bm->NodeLetVarMap1[n]), indentation, letize); + SMTLIB_Print1(os, (NodeLetVarMap1[n]), indentation, letize); return; } //this is to print letvars for shared subterms inside the actual //term to be printed - if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize) + if ((NodeLetVarMap.find(n) != NodeLetVarMap.end()) && letize) { - SMTLIB_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize); + SMTLIB_Print1(os, (NodeLetVarMap[n]), indentation, letize); return; } //otherwise print it normally - Kind kind = n.GetKind(); + const Kind kind = n.GetKind(); const ASTVec &c = n.GetChildren(); switch (kind) { @@ -152,7 +178,6 @@ namespace printer case BVCONST: outputBitVec(n, os); break; - case SYMBOL: n.nodeprint(os); break; @@ -162,7 +187,6 @@ namespace printer case TRUE: os << "true"; break; - case BVSX: case BVZX: { @@ -172,7 +196,7 @@ namespace printer else os << "(sign_extend["; - os << amount << "]"; + os << (amount - c[0].GetValueWidth()) << "]"; SMTLIB_Print1(os, c[0], indentation, letize); os << ")"; } @@ -203,18 +227,82 @@ namespace printer } } +void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet) +{ + const Kind kind = n.GetKind(); + + if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE) + return; + + const ASTVec &c = n.GetChildren(); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + { + const ASTNode& ccc = *it; + + const Kind k = ccc.GetKind(); + if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE) + continue; + + if (PLPrintNodeSet.find(ccc) == PLPrintNodeSet.end()) + { + //If branch: if *it is not in NodeSet then, + // + //1. add it to NodeSet + // + //2. Letize its childNodes + PLPrintNodeSet.insert(ccc); + LetizeNode(ccc, PLPrintNodeSet); + } + else + { + //0. Else branch: Node has been seen before + // + //1. Check if the node has a corresponding letvar in the + //1. NodeLetVarMap. + // + //2. if no, then create a new var and add it to the + //2. NodeLetVarMap + if (ccc.GetType() == BITVECTOR_TYPE && NodeLetVarMap.find(ccc) + == NodeLetVarMap.end()) + { + //Create a new symbol. Get some name. if it conflicts with a + //declared name, too bad. + int sz = NodeLetVarMap.size(); + ostringstream oss; + oss << "?let_k_" << sz; + + ASTNode CurrentSymbol = n.GetSTPMgr()->CreateSymbol( + oss.str().c_str()); + CurrentSymbol.SetValueWidth(n.GetValueWidth()); + CurrentSymbol.SetIndexWidth(n.GetIndexWidth()); + /* If for some reason the variable being created here is + * already declared by the user then the printed output will + * not be a legal input to the system. too bad. I refuse to + * check for this. [Vijay is the author of this comment.] + */ + + NodeLetVarMap[ccc] = CurrentSymbol; + std::pair + node_letvar_pair(CurrentSymbol, ccc); + NodeLetVarVec.push_back(node_letvar_pair); + } + } + } +} //end of LetizeNode() + // copied from Presentation Langauge printer. ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation) { - // Clear the PrintMap - STPMgr* bm = n.GetSTPMgr(); - bm->PLPrintNodeSet.clear(); - bm->NodeLetVarMap.clear(); - bm->NodeLetVarVec.clear(); - bm->NodeLetVarMap1.clear(); + // Clear the maps + NodeLetVarMap.clear(); + NodeLetVarVec.clear(); + NodeLetVarMap1.clear(); //pass 1: letize the node - n.LetizeNode(); + { + ASTNodeSet PLPrintNodeSet; + LetizeNode(n, PLPrintNodeSet); + } //pass 2: // @@ -224,41 +312,45 @@ namespace printer //3. Then print the Node itself, replacing every occurence of //3. expr1 with var1, expr2 with var2, ... //os << "("; - if (0 < bm->NodeLetVarMap.size()) + if (0 < NodeLetVarMap.size()) { - //ASTNodeMap::iterator it=bm->NodeLetVarMap.begin(); - //ASTNodeMap::iterator itend=bm->NodeLetVarMap.end(); - std::vector >::iterator - it = bm->NodeLetVarVec.begin(); - std::vector >::iterator - itend = bm->NodeLetVarVec.end(); - - os << "(LET "; + std::vector >::iterator it = + NodeLetVarVec.begin(); + const std::vector >::iterator itend = + NodeLetVarVec.end(); + + os << "(let ("; //print the let var first SMTLIB_Print1(os, it->first, indentation, false); - os << " = "; + os << " "; //print the expr SMTLIB_Print1(os, it->second, indentation, false); + os << " )"; //update the second map for proper printing of LET - bm->NodeLetVarMap1[it->second] = it->first; + NodeLetVarMap1[it->second] = it->first; + string closing = ""; for (it++; it != itend; it++) { - os << "," << endl; + os << " " << endl; + os << "(let ("; //print the let var first SMTLIB_Print1(os, it->first, indentation, false); - os << " = "; + os << " "; //print the expr SMTLIB_Print1(os, it->second, indentation, false); - + os << ")"; //update the second map for proper printing of LET - bm->NodeLetVarMap1[it->second] = it->first; + NodeLetVarMap1[it->second] = it->first; + closing += ")"; } - os << " IN " << endl; + os << " ( " << endl; SMTLIB_Print1(os, n, indentation, true); - os << ") "; + os << closing; + os << " ) ) "; + } else SMTLIB_Print1(os, n, indentation, false); @@ -289,8 +381,10 @@ namespace printer case OR: case XOR: case IFF: - //return _kind_names[k]; + case IMPLIES: + { return tolower(_kind_names[k]); + } case BVCONCAT: return "concat"; -- 2.47.3