CVC3  2.4.1
sat_api.cpp
Go to the documentation of this file.
1 ///////////////////////////////////////////////////////////////////////////////
2 // //
3 // File: sat_api.cpp //
4 // Author: Clark Barrett //
5 // Created: 2002 //
6 // Description: Implementation of SatSolver class //
7 // //
8 ///////////////////////////////////////////////////////////////////////////////
9 
10 #include "sat_api.h"
11 
12 using namespace std;
13 
14 #ifndef DPLL_BASIC
16 {
17  return NULL;
18 }
19 #endif
20 
21 void SatSolver::PrintStatistics(ostream & os)
22 {
23  int val;
24  float time;
25 
26  os << "Number of Variables\t\t\t" << NumVariables() << endl;
27 
28  val = GetNumLiterals();
29  if (val != -1)
30  os << "Number of Literals\t\t\t" << val << endl;
31 
32  os << "Number of Clauses\t\t\t" << NumClauses() << endl;
33 
34  val = GetBudgetUsed();
35  if (val != -1)
36  os << "Budget Used\t\t\t\t" << val << endl;
37 
38  val = GetMemUsed();
39  if (val != -1)
40  os << "Memory Used\t\t\t\t" << val << endl;
41 
42  val = GetMaxDLevel();
43  if (val != -1)
44  os << "Maximum Decision Level\t\t\t" << val << endl;
45 
46  val = GetNumDecisions();
47  if (val != -1)
48  os << "Number of Decisions\t\t\t" << val << endl;
49 
50  val = GetNumImplications();
51  if (val != -1)
52  os << "Number of Implications\t\t\t" << val << endl;
53 
54  val = GetNumConflicts();
55  if (val != -1)
56  os << "Number of Conflicts\t\t\t" << val << endl;
57 
58  val = GetNumExtConflicts();
59  if (val != -1)
60  os << "Number of External Conflicts\t\t" << val << endl;
61 
62  val = GetNumDeletedClauses();
63  if (val != -1)
64  os << "Number of Deleted Clauses\t\t" << val << endl;
65 
66  val = GetNumDeletedLiterals();
67  if (val != -1)
68  os << "Number of Deleted Literals\t\t" << val << endl;
69 
70  time = GetTotalTime();
71  if (time != -1)
72  os << endl << "Total Run Time\t\t\t\t" << time << endl;
73 
74  time = GetSATTime();
75  if (time != -1)
76  os << "Time spent in SAT\t\t\t" << time << endl;
77 }
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
static SatSolver * Create()
Definition: sat_api.cpp:15
void PrintStatistics(std::ostream &os=std::cout)
Definition: sat_api.cpp:21