still adding labels to duality

src/duality/duality.h

@@ -733,8 +733,10 @@ namespace Duality {
 
      Term ProjectFormula(std::vector<Term> &keep_vec, const Term &f);
 
+    public:
       int SubtermTruth(hash_map<ast,int> &memo, const Term &);
 
+    private:
       void ImplicantRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
 			hash_set<ast> *done, bool truth, hash_set<ast> &dont_cares);
 

src/duality/duality_profiling.cpp

@@ -25,82 +25,7 @@ Revision History:
 #include <string.h>
 #include <stdlib.h>
 
-#ifdef WIN32
+#include "duality_wrapper.h"
-
-// 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
-
-
 
 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 {
 
@@ -554,6 +555,15 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return res;
   }
 
+  double current_time()
+  {
+    static stopwatch sw;
+    static bool started = false;
+    if(!started)
+      sw.start();
+    return sw.get_seconds();
+  }
+
 }
 
 

src/duality/duality_wrapper.h

@@ -1283,7 +1283,9 @@ namespace Duality {
       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

src/muz_qe/duality_dl_interface.cpp

@@ -36,9 +36,12 @@ Revision History:
 #include "expr_abstract.h"
 #include "model_smt2_pp.h"
 
+// template class symbol_table<family_id>;
+
+
 #include "duality.h"
 
-using namespace Duality;
+// using namespace Duality;
 
 namespace Duality {
 
@@ -231,7 +234,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
 
   // print the label and the proved fact
 
-  out << "(" << node.number;
+  out << "(step s!" << node.number;
   out << " (" << node.Name.name();
   for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
     out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]);
@@ -239,7 +242,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
 
   // print the substitution
 
-  out << "  (\n";
+  out << "  (subst\n";
   RPFP::Edge *orig_edge = edge.map;
   int orig_clause = d->dd()->map[orig_edge];
   expr &t = d->dd()->clauses[orig_clause];
@@ -257,14 +260,26 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
   }
   out << "  )\n";
   
+  out << "  (labels";
+  std::vector<RPFP::label_struct> &labels = d->dd()->clause_labels[orig_clause];
+  {
+    hash_map<ast,int> memo;
+    for(unsigned j = 0; j < labels.size(); j++){
+      RPFP::label_struct &lab = labels[j];
+      int truth = cex.tree->SubtermTruth(memo,lab.value);
+      if(truth == 1 && lab.pos || truth == 0 && !lab.pos)
+	out << " " << lab.name;
+    }
+  }
+  out << "  )\n";
 
   // reference the proofs of all the children, in syntactic order
   // "true" means the child is not needed
   
-  out << "  (";
+  out << "  (ref ";
   for(unsigned i = 0; i < edge.Children.size(); i++){
     if(!cex.tree->Empty(edge.Children[i]))
-      out << " " << edge.Children[i]->number;
+      out << " s!" << edge.Children[i]->number;
     else
       out << " true";
   }
@@ -280,7 +295,7 @@ void dl_interface::display_certificate(std::ostream& out) {
     model_smt2_pp(out, m, *md.get(), 0); 
   }
   else if(_d->status == StatusRefutation){
-    out << "(\n";
+    out << "(derivation\n";
     // negation of the query is the last clause -- prove it
     print_proof(this,out,_d->cex);
     out << ")\n";