Adding timers for the sake of profiling

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index 18d7c6a647bafc95b29e4da60688ec782982a1ac..56fa2f6e45b2f299ba104f4458c8402eaaa873c2 100644 (file)
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -10,6 +10,7 @@
 #include "csolver.h"
 #include "common.h"
 #include <algorithm>
+#include <ctime>
 
 using namespace std;
 
@@ -192,7 +193,10 @@ void originalNqueensEncoding(int N){
                addArrayClauseLiteral(solver, cnf[i].size(), cnf[i].data());
        }
        finishedClauses(solver);
+       int start_s=clock();
        int result = solve(solver);
+       int stop_s=clock();
+       cout << "SAT Solving time: " << (stop_s-start_s)/double(CLOCKS_PER_SEC)*1000 << " ms" << endl;
        switch(result){
                case IS_UNSAT:
                        printf("Problem is unsat\n");