From 97a7ae1589c0ec2c2f50004a927b26455c74de06 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 5 Jun 2013 18:01:05 -0700
Subject: [PATCH] add profiling option

---
 src/api/dotnet/Properties/AssemblyInfo.cs |  4 ++--
 src/duality/duality_solver.cpp            | 15 +++++++++++++--
 src/muz_qe/duality_dl_interface.cpp       |  6 ++++++
 src/muz_qe/fixedpoint_params.pyg          |  1 +
 4 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs b/src/api/dotnet/Properties/AssemblyInfo.cs
index 517349177..1cd0fe7b8 100644
--- a/src/api/dotnet/Properties/AssemblyInfo.cs
+++ b/src/api/dotnet/Properties/AssemblyInfo.cs
@@ -34,6 +34,6 @@ using System.Security.Permissions;
 // You can specify all the values or you can default the Build and Revision Numbers 
 // by using the '*' as shown below:
 // [assembly: AssemblyVersion("4.2.0.0")]
-[assembly: AssemblyVersion("4.3.2.0")]
-[assembly: AssemblyFileVersion("4.3.2.0")]
+[assembly: AssemblyVersion("4.3.2.0")]
+[assembly: AssemblyFileVersion("4.3.2.0")]
 
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 40c82eac8..142d8e457 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -684,6 +684,7 @@ namespace Duality {
 
     bool CandidateFeasible(const Candidate &cand){
       if(!FeasibleEdges) return true;
+      timer_start("CandidateFeasible");
       RPFP *checker = new RPFP(rpfp->ls);
       // std::cout << "Checking feasibility of extension " << cand.edge->Parent->number << std::endl;
       checker->Push();
@@ -691,8 +692,10 @@ namespace Duality {
       Node *root = checker->CloneNode(cand.edge->Parent);
 #ifdef BOUNDED
       for(unsigned i = 0; i < cand.Children.size(); i++)
-	if(NodePastRecursionBound(cand.Children[i]))
+	if(NodePastRecursionBound(cand.Children[i])){
+	  timer_stop("CandidateFeasible");
 	  return false;
+	}
 #endif      
 #ifdef NEW_CAND_SEL
       GenNodeSolutionFromIndSet(cand.edge->Parent,root->Bound);
@@ -710,6 +713,7 @@ namespace Duality {
       if(!res)reporter->Reject(cand.edge,cand.Children);
       checker->Pop(1);
       delete checker;
+      timer_stop("CandidateFeasible");
       return res;
     }
 
@@ -749,12 +753,15 @@ namespace Duality {
     int StratifiedLeafCount;
 
     bool DoStratifiedInlining(){
+      timer_start("StratifiedInlining");
       DoTopoSort();
       for(unsigned i = 0; i < leaves.size(); i++){
 	Node *node = leaves[i];
 	bool res = SatisfyUpperBound(node);
-	if(!res)
+	if(!res){
+	  timer_stop("StratifiedInlining");
 	  return false;
+	}
       }
       // don't leave any dangling nodes!
 #ifndef EFFORT_BOUNDED_STRAT
@@ -762,6 +769,7 @@ namespace Duality {
 	if(!leaves[i]->Outgoing)
 	  MakeLeaf(leaves[i],true);    
 #endif
+      timer_stop("StratifiedInlining");
       return true;
     }
     
@@ -1333,6 +1341,7 @@ namespace Duality {
 
     /** Extend the unwinding, keeping it solved. */
     bool Extend(Candidate &cand){
+      timer_start("Extend");
       Node *node = CreateNodeInstance(cand.edge->Parent);
       CreateEdgeInstance(cand.edge,node,cand.Children);
       UpdateBackEdges(node);
@@ -1344,11 +1353,13 @@ namespace Duality {
 	ExpandUnderapproxNodes(cex.tree, cex.root);
 #endif
 	if(UseUnderapprox) BuildFullCex(node);
+	timer_stop("Extend");
 	return res;
       }
 #ifdef EARLY_EXPAND
       TryExpandNode(node);
 #endif
+      timer_stop("Extend");
       return res;
     }
 
diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index fd26a2a2b..e59baa4c5 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -41,6 +41,7 @@ Revision History:
 
 
 #include "duality.h"
+#include "duality_profiling.h"
 
 // using namespace Duality;
 
@@ -202,6 +203,11 @@ lbool dl_interface::query(::expr * query) {
   // Solve!
   bool ans = rs->Solve();
   
+  // profile!
+
+  if(m_ctx.get_params().profile())
+    print_profile(std::cout);
+
   // save the result and counterexample if there is one
   _d->status = ans ? StatusModel : StatusRefutation;
   _d->cex = rs->GetCounterexample();
diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg
index 567a35216..fcd280f25 100644
--- a/src/muz_qe/fixedpoint_params.pyg
+++ b/src/muz_qe/fixedpoint_params.pyg
@@ -64,6 +64,7 @@ def_module_params('fixedpoint',
 	                  ('use_underapprox', BOOL, False, 'DUALITY: Use underapproximations'),
 			  ('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'),
 			  ('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'),
+			  ('profile', BOOL, False, 'DUALITY: profile run time'),
                           ))