bool print_STPinput_back_flag;
bool print_STPinput_back_C_flag;
bool print_STPinput_back_SMTLIB_flag;
+ bool print_STPinput_back_SMTLIB1_flag;
bool print_STPinput_back_CVC_flag;
bool print_STPinput_back_dot_flag;
bool print_STPinput_back_GDL_flag;
print_STPinput_back_flag = false;
print_STPinput_back_C_flag = false;
print_STPinput_back_SMTLIB_flag = false;
+ print_STPinput_back_SMTLIB1_flag = false;
print_STPinput_back_CVC_flag = false;
print_STPinput_back_GDL_flag = false;
print_STPinput_back_dot_flag = false;
char * vc_printSMTLIB(VC vc, Expr e)
{
stringstream ss;
- printer::SMTLIB_Print(ss,*((nodestar)e), 0);
+ printer::SMTLIB1_PrintBack(ss,*((nodestar)e));
string s = ss.str();
char *copy = strdup(s.c_str());
return copy;
* step 5. Call SAT to determine if input is SAT or UNSAT
********************************************************************/
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType;
int main(int argc, char ** argv) {
char * infile;
helpstring +=
"--print-back-CVC : print input in CVC format, then exit\n";
helpstring +=
- "--print-back-SMTLIB : print input in SMT-LIB format, then exit\n";
+ "--print-back-SMTLIB : print input in SMT-LIB2 format, then exit\n";
+ helpstring +=
+ "--print-back-SMTLIB1 : print input in SMT-LIB1 format, then exit\n";
helpstring +=
"--print-back-GDL : print AiSee's graph format, then exit\n";
helpstring +=
lookup.insert(make_pair("--print-back-C",PRINT_BACK_C));
lookup.insert(make_pair("--print-back-CVC",PRINT_BACK_CVC));
lookup.insert(make_pair("--print-back-SMTLIB",PRINT_BACK_SMTLIB));
+ lookup.insert(make_pair("--print-back-SMTLIB1",PRINT_BACK_SMTLIB1));
lookup.insert(make_pair("--print-back-GDL",PRINT_BACK_GDL));
lookup.insert(make_pair("--print-back-dot",PRINT_BACK_DOT));
lookup.insert(make_pair("--output-CNF",OUTPUT_CNF));
bm->UserFlags.print_STPinput_back_SMTLIB_flag = true;
onePrintBack = true;
break;
+ case PRINT_BACK_SMTLIB1:
+ bm->UserFlags.print_STPinput_back_SMTLIB1_flag = true;
+ onePrintBack = true;
+ break;
case PRINT_BACK_GDL:
bm->UserFlags.print_STPinput_back_GDL_flag = true;
onePrintBack = true;
print_STPInput_Back(query);
}
+ if (bm->UserFlags.print_STPinput_back_SMTLIB1_flag)
+ {
+ printer::SMTLIB1_PrintBack(cout, original_input);
+ }
+
if (bm->UserFlags.print_STPinput_back_SMTLIB_flag)
{
- printer::SMTLIB_PrintBack(cout, original_input);
+ printer::SMTLIB2_PrintBack(cout, original_input);
}
if (bm->UserFlags.print_STPinput_back_C_flag)
--- /dev/null
+/********************************************************************
+ * AUTHORS: Trevor Hansen, Vijay Ganesh
+ *
+ * BEGIN DATE: July, 2009
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
+#include "printers.h"
+#include <cassert>
+#include <cctype>
+#include "SMTLIBPrinter.h"
+
+// Outputs in the SMTLIB1 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.
+
+// NB: This code doesn't include the substitution map. So if you've already simplified
+// the graph, then solving what this prints out wont necessarily give you a model.
+
+
+namespace printer
+{
+ using std::string;
+ using namespace BEEV;
+
+ void SMTLIB1_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
+ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os);
+
+ void SMTLIB1_PrintBack(ostream &os, const ASTNode& n)
+{
+ os << "(" << endl;
+ os << "benchmark blah" << endl;
+ if (containsAnyArrayOps(n))
+ os << ":logic QF_AUFBV" << endl;
+ else
+ os << ":logic QF_BV" << endl;
+
+
+ ASTNodeSet visited, symbols;
+ buildListOfSymbols(n, visited, symbols);
+ printSMTLIB1VarDeclsToStream(symbols, os);
+ os << ":formula ";
+ SMTLIB_Print(os, n, 0, &SMTLIB1_Print1);
+ os << ")" << endl;
+ }
+
+void printSMTLIB1VarDeclsToStream(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())
+ {
+ case BEEV::BITVECTOR_TYPE:
+
+ os << ":extrafuns (( ";
+ a.nodeprint(os);
+ os << " BitVec[" << a.GetValueWidth() << "]";
+ os << " ))" << endl;
+ break;
+ case BEEV::ARRAY_TYPE:
+ os << ":extrafuns (( ";
+ a.nodeprint(os);
+ os << " Array[" << a.GetIndexWidth();
+ os << ":" << a.GetValueWidth() << "] ))" << endl;
+ break;
+ case BEEV::BOOLEAN_TYPE:
+ os << ":extrapreds (( ";
+ a.nodeprint(os);
+ os << "))" << endl;
+ break;
+ default:
+ BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);
+ break;
+ }
+ }
+ } //printVarDeclsToStream
+
+ void outputBitVec(const ASTNode n, ostream& os)
+ {
+ const Kind k = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ ASTNode op;
+
+ if (BITVECTOR == k)
+ {
+ op = c[0];
+ }
+ else if (BVCONST == k)
+ {
+ op = n;
+ }
+ else
+ FatalError("nsadfsdaf");
+
+ // CONSTANTBV::BitVector_to_Dec returns a signed representation by default.
+ // Prepend with zero to convert to unsigned.
+
+ os << "bv";
+ 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() << "]";
+ CONSTANTBV::BitVector_Dispose(str);
+ }
+
+ void SMTLIB1_Print1(ostream& os, const ASTNode n, int indentation, bool letize)
+ {
+ //os << spaces(indentation);
+ //os << endl << spaces(indentation);
+ if (!n.IsDefined())
+ {
+ FatalError("<undefined>");
+ return;
+ }
+
+ //if this node is present in the letvar Map, then print the letvar
+ //this is to print letvars for shared subterms inside the printing
+ //of "(LET v0 = term1, v1=term1@term2,...
+ if ((NodeLetVarMap1.find(n) != NodeLetVarMap1.end()) && !letize)
+ {
+ SMTLIB1_Print1(os, (NodeLetVarMap1[n]), indentation, letize);
+ return;
+ }
+
+ //this is to print letvars for shared subterms inside the actual
+ //term to be printed
+ if ((NodeLetVarMap.find(n) != NodeLetVarMap.end()) && letize)
+ {
+ SMTLIB1_Print1(os, (NodeLetVarMap[n]), indentation, letize);
+ return;
+ }
+
+ //otherwise print it normally
+ const Kind kind = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ switch (kind)
+ {
+ case BITVECTOR:
+ case BVCONST:
+ outputBitVec(n, os);
+ break;
+ case SYMBOL:
+ n.nodeprint(os);
+ break;
+ case FALSE:
+ os << "false";
+ break;
+ case NAND: // No NAND, NOR in smtlib format.
+ case NOR:
+ assert(c.size() ==2);
+ os << "(" << "not ";
+ if (NAND == kind )
+ os << "(" << "and ";
+ else
+ os << "(" << "or ";
+ SMTLIB1_Print1(os, c[0], 0, letize);
+ os << " " ;
+ SMTLIB1_Print1(os, c[1], 0, letize);
+ os << "))";
+ break;
+ case TRUE:
+ os << "true";
+ break;
+ case BVSX:
+ case BVZX:
+ {
+ unsigned int amount = GetUnsignedConst(c[1]);
+ if (BVZX == kind)
+ os << "(zero_extend[";
+ else
+ os << "(sign_extend[";
+
+ os << (amount - c[0].GetValueWidth()) << "]";
+ SMTLIB1_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ case BVEXTRACT:
+ {
+ unsigned int upper = GetUnsignedConst(c[1]);
+ unsigned int lower = GetUnsignedConst(c[2]);
+ assert(upper >= lower);
+ os << "(extract[" << upper << ":" << lower << "] ";
+ SMTLIB1_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ default:
+ {
+ // SMT-LIB only allows these functions to have two parameters.
+ if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2)
+ {
+ string close = "";
+
+ for (int i =0; i < c.size()-1; i++)
+ {
+ os << "(" << functionToSMTLIBName(kind);
+ os << " ";
+ SMTLIB1_Print1(os, c[i], 0, letize);
+ os << " ";
+ close += ")";
+ }
+ SMTLIB1_Print1(os, c[c.size()-1], 0, letize);
+ os << close;
+ }
+ else
+ {
+ os << "(" << functionToSMTLIBName(kind);
+
+ ASTVec::const_iterator iend = c.end();
+ for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
+ {
+ os << " ";
+ SMTLIB1_Print1(os, *i, 0, letize);
+ }
+
+ os << ")";
+ }
+ }
+ }
+ }
+}
--- /dev/null
+/********************************************************************
+ * AUTHORS: Trevor Hansen, Vijay Ganesh
+ *
+ * BEGIN DATE: July, 2009
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
+#include "printers.h"
+#include <cassert>
+#include <cctype>
+#include "SMTLIBPrinter.h"
+
+// 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
+{
+
+ using std::string;
+ using namespace BEEV;
+
+ void SMTLIB2_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
+ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os);
+
+void SMTLIB2_PrintBack(ostream &os, const ASTNode& n)
+{
+ if (containsAnyArrayOps(n))
+ os << "(set-logic QF_AUFBV)" << endl;
+ else
+ os << "(set-logic QF_BV)"<< endl;
+
+ os << "(set-info :smt-lib-version 2.0)"<< endl;
+ os << "(set-info :status unknown)"<< endl;
+
+ ASTNodeSet visited, symbols;
+ buildListOfSymbols(n, visited, symbols);
+ printVarDeclsToStream(symbols, os);
+ os << "(assert ";
+ SMTLIB_Print(os, n, 0, &SMTLIB2_Print1);
+ os << ")" << endl;
+ os << "(check-sat)" << endl;
+ os << "(exit)" << endl;
+ }
+
+void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
+{
+ for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i
+ != iend; i++)
+ {
+ const BEEV::ASTNode& a = *i;
+ os << "(declare-fun ";
+
+ // Should be a symbol.
+ assert(a.GetKind()== SYMBOL);
+ a.nodeprint(os);
+ os << " () (";
+
+ switch (a.GetType())
+ {
+ case BEEV::BITVECTOR_TYPE:
+ os << "_ BitVec " << a.GetValueWidth() << ")";
+ break;
+ case BEEV::ARRAY_TYPE:
+ os << "Array (_ BitVec " << a.GetIndexWidth() << ") (_BitVec " << a.GetValueWidth() << ") )";
+ break;
+ case BEEV::BOOLEAN_TYPE:
+ os << " Bool ";
+ break;
+ default:
+ BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);
+ break;
+ }
+ os << ")\n";
+ }
+ } //printVarDeclsToStream
+
+ void outputBitVecSMTLIB2(const ASTNode n, ostream& os)
+ {
+ const Kind k = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ ASTNode op;
+
+ if (BITVECTOR == k)
+ {
+ op = c[0];
+ }
+ else if (BVCONST == k)
+ {
+ op = n;
+ }
+ else
+ FatalError("nsadfsdaf");
+
+ // CONSTANTBV::BitVector_to_Dec returns a signed representation by default.
+ // Prepend with zero to convert to unsigned.
+
+ os << "(_ bv";
+ 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() << ")";
+ CONSTANTBV::BitVector_Dispose(str);
+ }
+
+ void SMTLIB2_Print1(ostream& os, const ASTNode n, int indentation, bool letize)
+ {
+ //os << spaces(indentation);
+ //os << endl << spaces(indentation);
+ if (!n.IsDefined())
+ {
+ FatalError("<undefined>");
+ return;
+ }
+
+ //if this node is present in the letvar Map, then print the letvar
+ //this is to print letvars for shared subterms inside the printing
+ //of "(LET v0 = term1, v1=term1@term2,...
+ if ((NodeLetVarMap1.find(n) != NodeLetVarMap1.end()) && !letize)
+ {
+ SMTLIB2_Print1(os, (NodeLetVarMap1[n]), indentation, letize);
+ return;
+ }
+
+ //this is to print letvars for shared subterms inside the actual
+ //term to be printed
+ if ((NodeLetVarMap.find(n) != NodeLetVarMap.end()) && letize)
+ {
+ SMTLIB2_Print1(os, (NodeLetVarMap[n]), indentation, letize);
+ return;
+ }
+
+ //otherwise print it normally
+ const Kind kind = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ switch (kind)
+ {
+ case BITVECTOR:
+ case BVCONST:
+ outputBitVecSMTLIB2(n, os);
+ break;
+ case SYMBOL:
+ n.nodeprint(os);
+ break;
+ case FALSE:
+ os << "false";
+ break;
+ case NAND: // No NAND, NOR in smtlib format.
+ case NOR:
+ assert(c.size() ==2);
+ os << "(" << "not ";
+ if (NAND == kind )
+ os << "(" << "and ";
+ else
+ os << "(" << "or ";
+ SMTLIB2_Print1(os, c[0], 0, letize);
+ os << " " ;
+ SMTLIB2_Print1(os, c[1], 0, letize);
+ os << "))";
+ break;
+ case TRUE:
+ os << "true";
+ break;
+ case BVSX:
+ case BVZX:
+ {
+ unsigned int amount = GetUnsignedConst(c[1]);
+ if (BVZX == kind)
+ os << "(_ zero_extend ";
+ else
+ os << "(_ sign_extend ";
+
+ os << (amount - c[0].GetValueWidth()) << ") ";
+ SMTLIB2_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ case BVEXTRACT:
+ {
+ unsigned int upper = GetUnsignedConst(c[1]);
+ unsigned int lower = GetUnsignedConst(c[2]);
+ assert(upper >= lower);
+ os << "((_ extract" << upper << " " << lower << ") ";
+ SMTLIB2_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ default:
+ {
+ // SMT-LIB only allows these functions to have two parameters.
+ if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2)
+ {
+ string close = "";
+
+ for (int i =0; i < c.size()-1; i++)
+ {
+ os << "(" << functionToSMTLIBName(kind);
+ os << " ";
+ SMTLIB2_Print1(os, c[i], 0, letize);
+ os << " ";
+ close += ")";
+ }
+ SMTLIB2_Print1(os, c[c.size()-1], 0, letize);
+ os << close;
+ }
+ else
+ {
+ os << "(" << functionToSMTLIBName(kind);
+
+ ASTVec::const_iterator iend = c.end();
+ for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
+ {
+ os << " ";
+ SMTLIB2_Print1(os, *i, 0, letize);
+ }
+
+ os << ")";
+ }
+ }
+ }
+ }
+}
-/********************************************************************
- * AUTHORS: Trevor Hansen, Vijay Ganesh
- *
- * BEGIN DATE: July, 2009
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
#include "printers.h"
-#include <cassert>
-#include <cctype>
+#include "SMTLIBPrinter.h"
-// 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.
+// Functions used by both the version1 and version2 STMLIB printers.
namespace printer
{
+using namespace BEEV;
- 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);
-
+ //Map from ASTNodes to LetVars
+ BEEV::ASTNodeMap NodeLetVarMap;
- static string tolower(const char * name)
- {
- string s(name);
- for (size_t i = 0; i < s.size(); ++i)
- s[i] = ::tolower(s[i]);
- return s;
- }
-
-//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<pair<ASTNode, ASTNode> > NodeLetVarVec;
-//This is a vector which stores the Node to LetVars pairs. It
-//allows for sorted printing, as opposed to NodeLetVarMap
-std::vector<pair<ASTNode, ASTNode> > NodeLetVarVec;
+ //a partial Map from ASTNodes to LetVars. Needed in order to
+ //correctly print shared subterms inside the LET itself
+ BEEV::ASTNodeMap NodeLetVarMap1;
-//a partial Map from ASTNodes to LetVars. Needed in order to
-//correctly print shared subterms inside the LET itself
-ASTNodeMap NodeLetVarMap1;
+ bool containsAnyArrayOps(const ASTNode& n)
+ {
+ return true;
+ }
- // Initial version intended to print the whole thing back.
-void SMTLIB_PrintBack(ostream &os, const ASTNode& n)
-{
- os << "(" << endl;
- os << "benchmark blah" << 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(ASTNodeSet& symbols, ostream& os)
-{
- for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i
- != iend; i++)
+ static string tolower(const char * name)
{
- const BEEV::ASTNode& a = *i;
+ string s(name);
+ for (size_t i = 0; i < s.size(); ++i)
+ s[i] = ::tolower(s[i]);
+ return s;
+ }
- // Should be a symbol.
- assert(a.GetKind()== SYMBOL);
+ // copied from Presentation Langauge printer.
+ ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB1_Print1)(ostream&, const ASTNode , int , bool ))
+ {
+ // Clear the maps
+ NodeLetVarMap.clear();
+ NodeLetVarVec.clear();
+ NodeLetVarMap1.clear();
- switch (a.GetType())
+ //pass 1: letize the node
{
- case BEEV::BITVECTOR_TYPE:
-
- os << ":extrafuns (( ";
- a.nodeprint(os);
- os << " BitVec[" << a.GetValueWidth() << "]";
- os << " ))" << endl;
- break;
- case BEEV::ARRAY_TYPE:
- os << ":extrafuns (( ";
- a.nodeprint(os);
- os << " Array[" << a.GetIndexWidth();
- os << ":" << a.GetValueWidth() << "] ))" << endl;
- break;
- case BEEV::BOOLEAN_TYPE:
- os << ":extrapreds (( ";
- a.nodeprint(os);
- os << "))" << endl;
- break;
- default:
- BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);
- break;
- }
- }
- } //printVarDeclsToStream
-
- void outputBitVec(const ASTNode n, ostream& os)
- {
- const Kind k = n.GetKind();
- const ASTVec &c = n.GetChildren();
- ASTNode op;
-
- if (BITVECTOR == k)
- {
- op = c[0];
- }
- else if (BVCONST == k)
- {
- op = n;
- }
- else
- FatalError("nsadfsdaf");
-
- // CONSTANTBV::BitVector_to_Dec returns a signed representation by default.
- // Prepend with zero to convert to unsigned.
-
- os << "bv";
- 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() << "]";
- CONSTANTBV::BitVector_Dispose(str);
- }
-
- void SMTLIB_Print1(ostream& os, const ASTNode n, int indentation, bool letize)
- {
- //os << spaces(indentation);
- //os << endl << spaces(indentation);
- if (!n.IsDefined())
- {
- os << "<undefined>";
- return;
- }
-
- //if this node is present in the letvar Map, then print the letvar
- //this is to print letvars for shared subterms inside the printing
- //of "(LET v0 = term1, v1=term1@term2,...
- if ((NodeLetVarMap1.find(n) != NodeLetVarMap1.end()) && !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 ((NodeLetVarMap.find(n) != NodeLetVarMap.end()) && letize)
- {
- SMTLIB_Print1(os, (NodeLetVarMap[n]), indentation, letize);
- return;
- }
-
- //otherwise print it normally
- const Kind kind = n.GetKind();
- const ASTVec &c = n.GetChildren();
- switch (kind)
- {
- case BITVECTOR:
- case BVCONST:
- outputBitVec(n, os);
- break;
- case SYMBOL:
- n.nodeprint(os);
- break;
- case FALSE:
- os << "false";
- break;
- case NAND: // No NAND, NOR in smtlib format.
- case NOR:
- assert(c.size() ==2);
- os << "(" << "not ";
- if (NAND == kind )
- os << "(" << "and ";
- else
- os << "(" << "or ";
- SMTLIB_Print1(os, c[0], 0, letize);
- os << " " ;
- SMTLIB_Print1(os, c[1], 0, letize);
- os << "))";
- break;
- case TRUE:
- os << "true";
- break;
- case BVSX:
- case BVZX:
- {
- unsigned int amount = GetUnsignedConst(c[1]);
- if (BVZX == kind)
- os << "(zero_extend[";
- else
- os << "(sign_extend[";
-
- os << (amount - c[0].GetValueWidth()) << "]";
- SMTLIB_Print1(os, c[0], indentation, letize);
- os << ")";
- }
- break;
- case BVEXTRACT:
- {
- unsigned int upper = GetUnsignedConst(c[1]);
- unsigned int lower = GetUnsignedConst(c[2]);
- assert(upper >= lower);
- os << "(extract[" << upper << ":" << lower << "] ";
- SMTLIB_Print1(os, c[0], indentation, letize);
- os << ")";
- }
- break;
- default:
- {
- // SMT-LIB only allows these functions to have two parameters.
- if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2)
- {
- string close = "";
-
- for (int i =0; i < c.size()-1; i++)
- {
- os << "(" << functionToSMTLIBName(kind);
- os << " ";
- SMTLIB_Print1(os, c[i], 0, letize);
- os << " ";
- close += ")";
- }
- SMTLIB_Print1(os, c[c.size()-1], 0, letize);
- os << close;
- }
- else
- {
- os << "(" << functionToSMTLIBName(kind);
-
- ASTVec::const_iterator iend = c.end();
- for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
- {
- os << " ";
- SMTLIB_Print1(os, *i, 0, letize);
- }
+ ASTNodeSet PLPrintNodeSet;
+ LetizeNode(n, PLPrintNodeSet);
+ }
- os << ")";
- }
- }
- }
- }
+ //pass 2:
+ //
+ //2. print all the let variables and their counterpart expressions
+ //2. as follows (LET var1 = expr1, var2 = expr2, ...
+ //
+ //3. Then print the Node itself, replacing every occurence of
+ //3. expr1 with var1, expr2 with var2, ...
+ //os << "(";
+ if (0 < NodeLetVarMap.size())
+ {
+ std::vector<pair<ASTNode, ASTNode> >::iterator it =
+ NodeLetVarVec.begin();
+ const std::vector<pair<ASTNode, ASTNode> >::iterator itend =
+ NodeLetVarVec.end();
-void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet)
-{
- const Kind kind = n.GetKind();
+ os << "(let (";
+ //print the let var first
+ SMTLIB1_Print1(os, it->first, indentation, false);
+ os << " ";
+ //print the expr
+ SMTLIB1_Print1(os, it->second, indentation, false);
+ os << " )";
- if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE)
- return;
+ //update the second map for proper printing of LET
+ NodeLetVarMap1[it->second] = it->first;
- const ASTVec &c = n.GetChildren();
- for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ string closing = "";
+ for (it++; it != itend; it++)
+ {
+ os << " " << endl;
+ os << "(let (";
+ //print the let var first
+ SMTLIB1_Print1(os, it->first, indentation, false);
+ os << " ";
+ //print the expr
+ SMTLIB1_Print1(os, it->second, indentation, false);
+ os << ")";
+ //update the second map for proper printing of LET
+ NodeLetVarMap1[it->second] = it->first;
+ closing += ")";
+ }
+
+ os << " ( " << endl;
+ SMTLIB1_Print1(os, n, indentation, true);
+ os << closing;
+ os << " ) ) ";
+
+ }
+ else
+ SMTLIB1_Print1(os, n, indentation, false);
+
+ os << endl;
+ return os;
+ }
+
+ void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet)
{
- const ASTNode& ccc = *it;
+ const Kind kind = n.GetKind();
- const Kind k = ccc.GetKind();
- if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE)
- continue;
+ if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE)
+ return;
- if (PLPrintNodeSet.find(ccc) == PLPrintNodeSet.end())
+ const ASTVec &c = n.GetChildren();
+ for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
{
- //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;
+ const ASTNode& ccc = *it;
- 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.]
- */
+ const Kind k = ccc.GetKind();
+ if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE)
+ continue;
- NodeLetVarMap[ccc] = CurrentSymbol;
- std::pair<ASTNode, ASTNode>
- node_letvar_pair(CurrentSymbol, ccc);
- NodeLetVarVec.push_back(node_letvar_pair);
+ 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<ASTNode, ASTNode>
+ 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 maps
- NodeLetVarMap.clear();
- NodeLetVarVec.clear();
- NodeLetVarMap1.clear();
-
- //pass 1: letize the node
- {
- ASTNodeSet PLPrintNodeSet;
- LetizeNode(n, PLPrintNodeSet);
- }
-
- //pass 2:
- //
- //2. print all the let variables and their counterpart expressions
- //2. as follows (LET var1 = expr1, var2 = expr2, ...
- //
- //3. Then print the Node itself, replacing every occurence of
- //3. expr1 with var1, expr2 with var2, ...
- //os << "(";
- if (0 < NodeLetVarMap.size())
- {
- std::vector<pair<ASTNode, ASTNode> >::iterator it =
- NodeLetVarVec.begin();
- const std::vector<pair<ASTNode, ASTNode> >::iterator itend =
- NodeLetVarVec.end();
-
- os << "(let (";
- //print the let var first
- SMTLIB_Print1(os, it->first, indentation, false);
- os << " ";
- //print the expr
- SMTLIB_Print1(os, it->second, indentation, false);
- os << " )";
-
- //update the second map for proper printing of LET
- NodeLetVarMap1[it->second] = it->first;
-
- string closing = "";
- for (it++; it != itend; it++)
- {
- os << " " << endl;
- os << "(let (";
- //print the let var first
- SMTLIB_Print1(os, it->first, indentation, false);
- os << " ";
- //print the expr
- SMTLIB_Print1(os, it->second, indentation, false);
- os << ")";
- //update the second map for proper printing of LET
- NodeLetVarMap1[it->second] = it->first;
- closing += ")";
- }
-
- os << " ( " << endl;
- SMTLIB_Print1(os, n, indentation, true);
- os << closing;
- os << " ) ) ";
-
- }
- else
- SMTLIB_Print1(os, n, indentation, false);
-
- os << endl;
- return os;
- }
+ } //end of LetizeNode()
string functionToSMTLIBName(const Kind k)
{
}
}
}
-
-}
+};
--- /dev/null
+#ifndef SMTLIBPRINTERS_H_
+#define SMTLIBPRINTERS_H_
+
+#include "printers.h"
+
+namespace printer
+{
+
+ //Map from ASTNodes to LetVars
+ extern BEEV::ASTNodeMap NodeLetVarMap;
+
+ //This is a vector which stores the Node to LetVars pairs. It
+ //allows for sorted printing, as opposed to NodeLetVarMap
+ extern std::vector<pair<ASTNode, ASTNode> > NodeLetVarVec;
+
+ //a partial Map from ASTNodes to LetVars. Needed in order to
+ //correctly print shared subterms inside the LET itself
+ extern BEEV::ASTNodeMap NodeLetVarMap1;
+
+ string functionToSMTLIBName(const Kind k);
+
+ void LetizeNode(const ASTNode& n, BEEV::ASTNodeSet& PLPrintNodeSet);
+
+ ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ));
+
+ bool containsAnyArrayOps(const ASTNode& n);
+};
+#endif
/********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
*
* BEGIN DATE: November, 2005
*
#include "../AST/ASTKind.h"
#include "../STPManager/STP.h"
-//using namespace std;
namespace printer
{
ostream& Dot_Print(ostream &os, const BEEV::ASTNode n);
- ostream& SMTLIB_Print(ostream &os,
- const BEEV::ASTNode n, const int indentation = 0);
- ostream& C_Print(ostream &os,
+ ostream& C_Print(ostream &os,
const BEEV::ASTNode n, const int indentation = 0);
ostream& PL_Print(ostream &os,
const BEEV::ASTNode& n, int indentation=0);
const BEEV::ASTNode& n, int indentation=0);
ostream& Lisp_Print_indent(ostream &os,
const BEEV::ASTNode& n,int indentation=0);
- void SMTLIB_PrintBack(ostream &os,
+
+ // The "PrintBack" functions also define all the variables that are used.
+ void SMTLIB1_PrintBack(ostream &os,
+ const BEEV::ASTNode& n );
+
+ void SMTLIB2_PrintBack(ostream &os,
const BEEV::ASTNode& n );
+
ostream& GDL_Print(ostream &os, const BEEV::ASTNode n);
ostream& GDL_Print(ostream &os, const ASTNode n, string (*annotate)(const ASTNode&));
projects / francis / stp.git / commitdiff