26 os <<
"Number of Variables\t\t\t" << NumVariables() <<
endl;
28 val = GetNumLiterals();
30 os <<
"Number of Literals\t\t\t" << val <<
endl;
32 os <<
"Number of Clauses\t\t\t" << NumClauses() <<
endl;
34 val = GetBudgetUsed();
36 os <<
"Budget Used\t\t\t\t" << val <<
endl;
40 os <<
"Memory Used\t\t\t\t" << val <<
endl;
44 os <<
"Maximum Decision Level\t\t\t" << val <<
endl;
46 val = GetNumDecisions();
48 os <<
"Number of Decisions\t\t\t" << val <<
endl;
50 val = GetNumImplications();
52 os <<
"Number of Implications\t\t\t" << val <<
endl;
54 val = GetNumConflicts();
56 os <<
"Number of Conflicts\t\t\t" << val <<
endl;
58 val = GetNumExtConflicts();
60 os <<
"Number of External Conflicts\t\t" << val <<
endl;
62 val = GetNumDeletedClauses();
64 os <<
"Number of Deleted Clauses\t\t" << val <<
endl;
66 val = GetNumDeletedLiterals();
68 os <<
"Number of Deleted Literals\t\t" << val <<
endl;
70 time = GetTotalTime();
72 os << endl <<
"Total Run Time\t\t\t\t" << time <<
endl;
76 os <<
"Time spent in SAT\t\t\t" << time <<
endl;
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
static SatSolver * Create()
void PrintStatistics(std::ostream &os=std::cout)