working on duality

src/duality/duality_profiling.cpp

@@ -25,82 +25,7 @@ Revision History:
 #include <string.h>
 #include <stdlib.h>
 
-#ifdef WIN32
-
-// include "Windows.h"
-
-
-#if 0
-typedef __int64 clock_t;
-
-static clock_t current_time(){
-  LARGE_INTEGER lpPerformanceCount;
-  lpPerformanceCount.QuadPart = 0;
-  QueryPerformanceCounter(&lpPerformanceCount);
-  return lpPerformanceCount.QuadPart;
-}
-
-static void output_time(std::ostream &os, clock_t time){
-	LARGE_INTEGER lpFrequency;
-	lpFrequency.QuadPart = 1;
-	QueryPerformanceFrequency(&lpFrequency);
-    os << ((double)time)/lpFrequency.QuadPart;
-}
-#else
-
-typedef double clock_t;
-
-static clock_t current_time(){
-  FILETIME lpCreationTime;
-  FILETIME lpExitTime;
-  FILETIME lpKernelTime;
-  FILETIME lpUserTime;
-
-  GetProcessTimes( GetCurrentProcess(),
-		   &lpCreationTime, &lpExitTime, &lpKernelTime, &lpUserTime );
-
-
-  double usr_time = ((double) lpUserTime.dwLowDateTime)/10000000. +
-				((double) lpUserTime.dwHighDateTime)/(10000000. * pow(2.0,32.0));
-  return usr_time;
-}
-
-static void output_time(std::ostream &os, clock_t time){
-  os << time;
-}
-
-#endif
-
-#else
-
-#include <sys/times.h>
-#include <unistd.h>
-#include <sys/time.h>
-#include <sys/resource.h>
-
-static clock_t current_time(){
-#if 0
-  struct tms buf;
-  times(&buf);
-  return buf.tms_utime;
-#else
-  struct rusage r;
-  getrusage(RUSAGE_SELF, &r);
-  return 1000 * r.ru_utime.tv_sec + r.ru_utime.tv_usec / 1000;
-#endif
-}
-
-static void output_time(std::ostream &os, clock_t time){
-#if 0
-  os << ((double)time)/sysconf(_SC_CLK_TCK);
-#else
-  os << ((double)time)/1000;
-#endif
-}
-
-#endif
-
-
+#include "duality_wrapper.h"
 
 namespace Duality {
   

src/duality/duality_solver.cpp

@@ -1266,7 +1266,7 @@ namespace Duality {
       DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand);
       bool res = dt.Derive(unwinding,node,UseUnderapprox);
       int end_decs = rpfp->CumulativeDecisions();
-      std::cout << "decisions: " << (end_decs - start_decs)  << std::endl;
+      // std::cout << "decisions: " << (end_decs - start_decs)  << std::endl;
       last_decisions = end_decs - start_decs;
       if(res){
 	cex.tree = dt.tree;

src/duality/duality_wrapper.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "iz3interp.h"
 #include "statistics.h"
 #include "expr_abstract.h"
+#include "stopwatch.h"
 
 namespace Duality {
 
@@ -545,6 +546,15 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     a.show();
   }
 
+  double current_time()
+  {
+    static stopwatch sw;
+    static bool started = false;
+    if(!started)
+      sw.start();
+    return sw.get_seconds();
+  }
+
 }
 
 

src/duality/duality_wrapper.h

@@ -1281,8 +1281,10 @@ namespace Duality {
       m().inc_ref(a.raw());
       return to_expr(a.raw());
     }
-    
-    
+
+    typedef double clock_t;
+    clock_t current_time();
+    inline void output_time(std::ostream &os, clock_t time){os << time;}
 };
 
 // to make Duality::ast hashable