|
CVC3
|
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 }
1.7.3