00001 #include "sat_api.h"
00002
00003 using namespace std;
00004
00005 void SatSolver::PrintStatistics(ostream & os)
00006 {
00007 int val;
00008 float time;
00009
00010 os << "Number of Variables\t\t\t" << NumVariables() << endl;
00011
00012 val = GetNumLiterals();
00013 if (val != -1)
00014 os << "Number of Literals\t\t\t" << val << endl;
00015
00016 os << "Number of Clauses\t\t\t" << NumClauses() << endl;
00017
00018 val = GetBudgetUsed();
00019 if (val != -1)
00020 os << "Budget Used\t\t\t\t" << val << endl;
00021
00022 val = GetMemUsed();
00023 if (val != -1)
00024 os << "Memory Used\t\t\t\t" << val << endl;
00025
00026 val = GetMaxDLevel();
00027 if (val != -1)
00028 os << "Maximum Decision Level\t\t\t" << val << endl;
00029
00030 val = GetNumDecisions();
00031 if (val != -1)
00032 os << "Number of Decisions\t\t\t" << val << endl;
00033
00034 val = GetNumImplications();
00035 if (val != -1)
00036 os << "Number of Implications\t\t\t" << val << endl;
00037
00038 val = GetNumConflicts();
00039 if (val != -1)
00040 os << "Number of Conflicts\t\t\t" << val << endl;
00041
00042 val = GetNumExtConflicts();
00043 if (val != -1)
00044 os << "Number of External Conflicts\t\t" << val << endl;
00045
00046 val = GetNumDeletedClauses();
00047 if (val != -1)
00048 os << "Number of Deleted Clauses\t\t" << val << endl;
00049
00050 val = GetNumDeletedLiterals();
00051 if (val != -1)
00052 os << "Number of Deleted Literals\t\t" << val << endl;
00053
00054 time = GetTotalTime();
00055 if (time != -1)
00056 os << endl << "Total Run Time\t\t\t\t" << time << endl;
00057
00058 time = GetSATTime();
00059 if (time != -1)
00060 os << "Time spent in SAT\t\t\t" << time << endl;
00061 }
