add profiling option

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,19 +753,23 @@ 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
       for(unsigned i = 0; i < leaves.size(); i++)
 	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;
     }
 

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();

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'),
                           ))