1 /********************************************************************
2 * AUTHORS: Vijay Ganesh
3 *
4 * BEGIN DATE: November, 2005
5 *
6 Permission is hereby granted, free of charge, to any person obtaining a copy
7 of this software and associated documentation files (the "Software"), to deal
8 in the Software without restriction, including without limitation the rights
9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10 copies of the Software, and to permit persons to whom the Software is
11 furnished to do so, subject to the following conditions:
12
13 The above copyright notice and this permission notice shall be included in
14 all copies or substantial portions of the Software.
15
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
22 THE SOFTWARE.
23 ********************************************************************/
24
25 #include "stp/Printer/AssortedPrinters.h"
26 #include "stp/Printer/printers.h"
27 #include <cstdint>
28
29 namespace stp
30 {
31 using std::cout;
32 using std::endl;
33
34 /******************************************************************
35 * Assorted print routines collected in one place. The code here is
36 * different from the one in printers directory. It is possible that
37 * there is some duplication.
38 *
39 * FIXME: Get rid of any redundant code
40 ******************************************************************/
41
LispPrint(ostream & os,int indentation) const42 ostream& ASTNode::LispPrint(ostream& os, int indentation) const
43 {
44 return printer::Lisp_Print(os, *this, indentation);
45 }
46
LispPrint_indent(ostream & os,int indentation) const47 ostream& ASTNode::LispPrint_indent(ostream& os, int indentation) const
48 {
49 return printer::Lisp_Print_indent(os, *this, indentation);
50 }
51
PL_Print(ostream & os,STPMgr * mgr,int indentation) const52 ostream& ASTNode::PL_Print(ostream& os, STPMgr* mgr, int indentation) const
53 {
54 return printer::PL_Print(os, *this, mgr, indentation);
55 }
56
57 // This is the IO manipulator. It builds an object of class
58 //"LispPrinter" that has a special overloaded "<<" operator.
lisp(const ASTNode & node,int indentation=0)59 inline LispPrinter lisp(const ASTNode& node, int indentation = 0)
60 {
61 LispPrinter lp(node, indentation);
62 return lp;
63 }
64
65 // FIXME: Made non-ref in the hope that it would work better.
lp(ASTNode node)66 void lp(ASTNode node)
67 {
68 cout << lisp(node) << endl;
69 }
70
lpvec(const ASTVec & vec)71 void lpvec(const ASTVec& vec)
72 {
73 LispPrintVec(cout, vec, 0);
74 cout << endl;
75 }
76
77 // //Variable Order Printer: A global function which converts a MINISAT
78 // //var into a ASTNODE var. It then prints this var along with
79 // //variable order dcisions taken by MINISAT.
80 // void Convert_MINISATVar_To_ASTNode_Print(int minisat_var,
81 // int decision_level, int polarity)
82 // {
83 // stp::ASTNode vv = stp::GlobalSTPMgr->_SATVar_to_AST[minisat_var];
84 // cout << spaces(decision_level);
85 // if (polarity)
86 // {
87 // cout << "!";
88 // }
89 // printer::PL_Print(cout,vv, 0);
90 // cout << endl;
91 // } //end of Convert_MINISATVar_To_ASTNode_Print()
92
printVarDeclsToStream(ostream & os,ASTNodeSet & ListOfDeclaredVars)93 void STPMgr::printVarDeclsToStream(ostream& os, ASTNodeSet& ListOfDeclaredVars)
94 {
95 for (ASTNodeSet::iterator i = ListOfDeclaredVars.begin(),
96 iend = ListOfDeclaredVars.end();
97 i != iend; i++)
98 {
99 stp::ASTNode a = *i;
100 switch (a.GetType())
101 {
102 case stp::BITVECTOR_TYPE:
103 a.PL_Print(os, this);
104 os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl;
105 break;
106 case stp::ARRAY_TYPE:
107 a.PL_Print(os, this);
108 os << " : ARRAY "
109 << "BITVECTOR(" << a.GetIndexWidth() << ") OF ";
110 os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl;
111 break;
112 case stp::BOOLEAN_TYPE:
113 a.PL_Print(os, this);
114 os << " : BOOLEAN;" << endl;
115 break;
116 default:
117 stp::FatalError("vc_printDeclsToStream: Unsupported type", a);
118 break;
119 }
120 }
121 } // printVarDeclsToStream
122
printAssertsToStream(ostream & os)123 void STPMgr::printAssertsToStream(ostream& os)
124 {
125 ASTVec v = GetAsserts();
126 for (ASTVec::iterator i = v.begin(), iend = v.end(); i != iend; i++)
127 {
128 ASTNode q = *i;
129 os << "ASSERT( ";
130 q.PL_Print(os, this);
131 os << ");" << endl;
132 }
133 }
134
print_STPInput_Back(const ASTNode & query,STPMgr * mgr)135 void print_STPInput_Back(const ASTNode& query, STPMgr* mgr)
136 {
137
138 // Determine the symbols in the query and asserts.
139 ASTNodeSet visited;
140 ASTNodeSet symbols;
141 buildListOfSymbols(query, visited, symbols);
142 ASTVec v = mgr->GetAsserts();
143 for (ASTVec::iterator i = v.begin(), iend = v.end(); i != iend; i++)
144 buildListOfSymbols(*i, visited, symbols);
145
146 mgr->printVarDeclsToStream(cout, symbols);
147 mgr->printAssertsToStream(cout);
148 cout << "QUERY(";
149 query.PL_Print(cout, mgr);
150 cout << ");\n";
151 }
152 } // end of namespace stp
153