CVC3: sat_api.cpp Source File

00001 ///////////////////////////////////////////////////////////////////////////////
00002 //                                                                           //
00003 // File: sat_api.cpp                                                         //
00004 // Author: Clark Barrett                                                     //
00005 // Created: 2002                               //
00006 // Description: Implementation of SatSolver class                            //
00007 //                                                                           //
00008 ///////////////////////////////////////////////////////////////////////////////
00009 
00010 #include "sat_api.h"
00011 
00012 using namespace std;
00013 
00014 #ifndef DPLL_BASIC
00015 SatSolver *SatSolver::Create()
00016 {
00017   return NULL;
00018 }
00019 #endif
00020 
00021 void SatSolver::PrintStatistics(ostream & os)
00022 {
00023   int val;
00024   float time;
00025 
00026     os << "Number of Variables\t\t\t" << NumVariables() << endl;
00027 
00028   val = GetNumLiterals();
00029   if (val != -1)
00030     os << "Number of Literals\t\t\t" << val << endl;
00031 
00032     os << "Number of Clauses\t\t\t" << NumClauses() << endl;
00033 
00034   val = GetBudgetUsed();
00035   if (val != -1)
00036     os << "Budget Used\t\t\t\t" << val << endl;
00037 
00038   val = GetMemUsed();
00039   if (val != -1)
00040     os << "Memory Used\t\t\t\t" << val << endl;
00041 
00042   val = GetMaxDLevel();
00043   if (val != -1)
00044     os << "Maximum Decision Level\t\t\t" << val << endl;
00045 
00046   val = GetNumDecisions();
00047   if (val != -1)
00048     os << "Number of Decisions\t\t\t" << val << endl;
00049 
00050   val = GetNumImplications();
00051   if (val != -1)
00052     os << "Number of Implications\t\t\t" << val << endl;
00053 
00054   val = GetNumConflicts();
00055   if (val != -1)
00056     os << "Number of Conflicts\t\t\t" << val << endl;
00057 
00058   val = GetNumExtConflicts();
00059   if (val != -1)
00060     os << "Number of External Conflicts\t\t" << val << endl;
00061 
00062   val = GetNumDeletedClauses();
00063   if (val != -1)
00064     os << "Number of Deleted Clauses\t\t" << val << endl;
00065 
00066   val = GetNumDeletedLiterals();
00067   if (val != -1)
00068     os << "Number of Deleted Literals\t\t" << val << endl;
00069 
00070   time = GetTotalTime();
00071   if (time != -1)
00072     os << endl << "Total Run Time\t\t\t\t" << time << endl;
00073 
00074   time = GetSATTime();
00075   if (time != -1)
00076     os << "Time spent in SAT\t\t\t" << time << endl;
00077 }