From b15010e9749516a526eb2f7a85d14695b48225cd Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Thu, 3 Sep 2009 20:15:06 +0000 Subject: [PATCH] moved many BeevMgr and related classes print functions into a separate file printers/AssortedPrinters.cpp git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@176 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/printer/AssortedPrinters.cpp | 316 +++++++++++++++++++++++++++ src/AST/printer/AssortedPrinters.h | 74 +++++++ 2 files changed, 390 insertions(+) create mode 100644 src/AST/printer/AssortedPrinters.cpp create mode 100644 src/AST/printer/AssortedPrinters.h diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp new file mode 100644 index 0000000..cdca005 --- /dev/null +++ b/src/AST/printer/AssortedPrinters.cpp @@ -0,0 +1,316 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- +#include "../AST.h" +#include "AssortedPrinters.h" +#include "printers.h" + +namespace BEEV +{ + /****************************************************************** + * Assorted print routines collected in one place. The code here is + * different from the one in printers directory. It is possible that + * there is some duplication. + * + * FIXME: Get rid of any redundant code + ******************************************************************/ + + ostream &ASTNode::LispPrint(ostream &os, int indentation) const + { + printer::Lisp_Print(os, *this, indentation); + } + + ostream &ASTNode::LispPrint_indent(ostream &os, int indentation) const + { + printer::Lisp_Print_indent(os, *this, indentation); + } + + ostream& ASTNode::PL_Print(ostream &os, int indentation) const + { + printer::PL_Print(os, *this, indentation); + } + + //This is the IO manipulator. It builds an object of class + //"LispPrinter" that has a special overloaded "<<" operator. + inline LispPrinter lisp(const ASTNode &node, int indentation = 0) + { + LispPrinter lp(node, indentation); + return lp; + } //end of LispPrinter_lisp + + //iomanipulator. builds an object of class "LisPrinter" that has a + //special overloaded "<<" operator. + inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0) + { + LispVecPrinter lvp(vec, indentation); + return lvp; + } //end of LispVecPrinter_lisp() + + // FIXME: Made non-ref in the hope that it would work better. + void lp(ASTNode node) + { + cout << lisp(node) << endl; + } + + void lpvec(const ASTVec &vec) + { + vec[0].GetBeevMgr().AlreadyPrintedSet.clear(); + LispPrintVec(cout, vec, 0); + cout << endl; + } + + // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver + void BeevMgr::PrintStats(MINISAT::Solver& s) + { + if (!stats_flag) + return; + double cpu_time = MINISAT::cpuTime(); + uint64_t mem_used = MINISAT::memUsed(); + reportf("restarts : %llu\n", s.starts); + reportf("conflicts : %llu (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); + reportf("decisions : %llu (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); + reportf("propagations : %llu (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); + reportf("conflict literals : %llu (%4.2f %% deleted)\n", s.tot_literals, + (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); + if (mem_used != 0) + reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); + reportf("CPU time : %g s\n", cpu_time); + } //end of PrintStats() + + // Prints Satisfying assignment directly, for debugging. + void BeevMgr::PrintSATModel(MINISAT::Solver& newS) + { + if (!newS.okay()) + FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT", ASTUndefined); + // FIXME: Don't put tests like this in the print functions. The print functions + // should print unconditionally. Put a conditional around the call if you don't + // want them to print + if (!(stats_flag && print_nodes_flag)) + return; + + int num_vars = newS.nVars(); + cout << "Satisfying assignment: " << endl; + for (int i = 0; i < num_vars; i++) + { + if (newS.model[i] == MINISAT::l_True) + { + ASTNode s = _SATVar_to_AST[i]; + cout << s << endl; + } + else if (newS.model[i] == MINISAT::l_False) + { + ASTNode s = _SATVar_to_AST[i]; + cout << CreateNode(NOT, s) << endl; + } + } + } //end of PrintSATModel() + + + /* FUNCTION: prints a counterexample for INVALID inputs. iterate + * through the CounterExampleMap data structure and print it to + * stdout + */ + void BeevMgr::PrintCounterExample(bool t, std::ostream& os) + { + //global command-line option + // FIXME: This should always print the counterexample. If you want + // to turn it off, check the switch at the point of call. + if (!print_counterexample_flag) + { + return; + } + + //input is valid, no counterexample to print + if (ValidFlag) + { + return; + } + + //if this option is true then print the way dawson wants using a + //different printer. do not use this printer. + if (print_arrayval_declaredorder_flag) + { + return; + } + + //t is true if SAT solver generated a counterexample, else it is + //false + if (!t) + { + cerr << "PrintCounterExample: No CounterExample to print: " << endl; + return; + } + + //os << "\nCOUNTEREXAMPLE: \n" << endl; + ASTNodeMap::iterator it = CounterExampleMap.begin(); + ASTNodeMap::iterator itend = CounterExampleMap.end(); + for (; it != itend; it++) + { + ASTNode f = it->first; + ASTNode se = it->second; + + if (ARRAY_TYPE == se.GetType()) + { + FatalError("TermToConstTermUsingModel: entry in counterexample is an arraytype. bogus:", se); + } + + //skip over introduced variables + if (f.GetKind() == SYMBOL && (_introduced_symbols.find(f) != _introduced_symbols.end())) + continue; + if (f.GetKind() == SYMBOL || (f.GetKind() == READ && f[0].GetKind() == SYMBOL && f[1].GetKind() == BVCONST)) + { + os << "ASSERT( "; + f.PL_Print(os,0); + os << " = "; + if (BITVECTOR_TYPE == se.GetType()) + { + TermToConstTermUsingModel(se, false).PL_Print(os, 0); + } + else + { + se.PL_Print(os, 0); + } + os << " );" << endl; + } + } + //os << "\nEND OF COUNTEREXAMPLE" << endl; + } //End of PrintCounterExample + + +/* iterate through the CounterExampleMap data structure and print it + * to stdout. this function prints only the declared array variables + * IN the ORDER in which they were declared. It also assumes that + * the variables are of the form 'varname_number'. otherwise it will + * not print anything. This function was specifically written for + * Dawson Engler's group (bug finding research group at Stanford) + */ + void BeevMgr::PrintCounterExample_InOrder(bool t) + { + //global command-line option to print counterexample. we do not + //want both counterexample printers to print at the sametime. + // FIXME: This should always print the counterexample. If you want + // to turn it off, check the switch at the point of call. + if (print_counterexample_flag) + return; + + //input is valid, no counterexample to print + if (ValidFlag) + return; + + //print if the commandline option is '-q'. allows printing the + //counterexample in order. + if (!print_arrayval_declaredorder_flag) + return; + + //t is true if SAT solver generated a counterexample, else it is + //false + if (!t) + { + cerr << "PrintCounterExample: No CounterExample to print: " << endl; + return; + } + + //vector to store the integer values + std::vector out_int; + cout << "% "; + for (ASTVec::iterator it = _special_print_set.begin(), itend = _special_print_set.end(); it != itend; it++) + { + if (ARRAY_TYPE == it->GetType()) + { + //get the name of the variable + const char * c = it->GetName(); + std::string ss(c); + if (!(0 == strncmp(ss.c_str(), "ini_", 4))) + continue; + reverse(ss.begin(), ss.end()); + + //cout << "debugging: " << ss; + size_t pos = ss.find('_', 0); + if (!((0 < pos) && (pos < ss.size()))) + continue; + + //get the associated length + std::string sss = ss.substr(0, pos); + reverse(sss.begin(), sss.end()); + int n = atoi(sss.c_str()); + + it->PL_Print(cout, 2); + for (int j = 0; j < n; j++) + { + ASTNode index = CreateBVConst(it->GetIndexWidth(), j); + ASTNode readexpr = CreateTerm(READ, it->GetValueWidth(), *it, index); + ASTNode val = GetCounterExample(t, readexpr); + //cout << "ASSERT( "; + //cout << " = "; + out_int.push_back(GetUnsignedConst(val)); + //cout << "\n"; + } + } + } + cout << endl; + for (unsigned int jj = 0; jj < out_int.size(); jj++) + cout << out_int[jj] << endl; + cout << endl; + } //End of PrintCounterExample_InOrder + + + void BeevMgr::printCacheStatus() + { + cerr << SimplifyMap->size() << endl; + cerr << SimplifyNegMap->size() << endl; + cerr << ReferenceCount->size() << endl; + cerr << TermsAlreadySeenMap.size() << endl; + + cerr << SimplifyMap->bucket_count() << endl; + cerr << SimplifyNegMap->bucket_count() << endl; + cerr << ReferenceCount->bucket_count() << endl; + cerr << TermsAlreadySeenMap.bucket_count() << endl; + } //printCacheStatus() + + //This function prints the output of the STP solver + void BeevMgr::PrintOutput(bool true_iff_valid) + { + if (print_output_flag) + { + if (smtlib_parser_flag) + { + if (true_iff_valid && (BEEV::input_status == TO_BE_SATISFIABLE)) + { + cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl; + } + else if (!true_iff_valid && (BEEV::input_status == TO_BE_UNSATISFIABLE)) + { + cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; + } + } + } + + if (true_iff_valid) + { + ValidFlag = true; + if (print_output_flag) + { + if (smtlib_parser_flag) + cout << "unsat\n"; + else + cout << "Valid.\n"; + } + } + else + { + ValidFlag = false; + if (print_output_flag) + { + if (smtlib_parser_flag) + cout << "sat\n"; + else + cout << "Invalid.\n"; + } + } + } //end of PrintOutput() +};//end of namespace BEEV diff --git a/src/AST/printer/AssortedPrinters.h b/src/AST/printer/AssortedPrinters.h new file mode 100644 index 0000000..bfaaef1 --- /dev/null +++ b/src/AST/printer/AssortedPrinters.h @@ -0,0 +1,74 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef PRINTER_H +#define PRINTER_H + +#include "../AST.h" + +namespace BEEV +{ + using namespace std; + + /*************************************************************************** + Class LispPrinter: iomanipulator for printing ASTNode or ASTVec + ***************************************************************************/ + class LispPrinter + { + + public: + ASTNode _node; + + // number of spaces to print before first real character of + // object. + int _indentation; + + // FIXME: pass ASTNode by reference + // Constructor to build the LispPrinter object + LispPrinter(ASTNode node, int indentation) : + _node(node), _indentation(indentation) + { + } + + friend ostream &operator<<(ostream &os, const LispPrinter &lp) + { + return lp._node.LispPrint(os, lp._indentation); + } + ; + + }; //End of ListPrinter + + /***************************************************************************/ + /* Class LispVecPrinter:iomanipulator for printing vector of ASTNodes */ + /***************************************************************************/ + class LispVecPrinter + { + + public: + const ASTVec * _vec; + // number of spaces to print before first real + // character of object. + int _indentation; + + // Constructor to build the LispPrinter object + LispVecPrinter(const ASTVec &vec, int indentation) + { + _vec = &vec; + _indentation = indentation; + } + + friend ostream &operator<<(ostream &os, const LispVecPrinter &lvp) + { + LispPrintVec(os, *lvp._vec, lvp._indentation); + return os; + } + ; + }; //End of Class ListVecPrinter +};// end of namespace BEEV +#endif -- 2.47.3