From ee4b9d46f114a4b7ccdd2881f8b4b186b8fcc26e Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Mon, 27 May 2013 19:22:47 -0700
Subject: [PATCH] fix labels bug in duality

---
 src/duality/duality.h               |  4 +-
 src/duality/duality_rpfp.cpp        | 71 ++++++++++++++++++++++++++++-
 src/duality/duality_wrapper.cpp     |  3 --
 src/muz_qe/duality_dl_interface.cpp |  3 +-
 4 files changed, 74 insertions(+), 7 deletions(-)

diff --git a/src/duality/duality.h b/src/duality/duality.h
index 0a580a463..ef16696ec 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -676,7 +676,7 @@ namespace Duality {
 
       void GetLabels(Edge *e, std::vector<symbol> &labels);
 
-      int GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos);
+      //      int GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos);
 
     private:
       
@@ -767,6 +767,8 @@ namespace Duality {
 
       Term ModelValueAsConstraint(const Term &t);
 
+      void GetLabelsRec(hash_map<ast,int> &memo, const Term &f, std::vector<symbol> &labels,
+			hash_set<ast> *done, bool truth);
     };
     
     /** RPFP solver base class. */
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index e46a52908..77a007c82 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -809,6 +809,13 @@ namespace Duality {
 	goto done;
       }
     }
+    {
+      bool pos; std::vector<symbol> names;
+      if(f.is_label(pos,names)){
+	res = SubtermTruth(memo,f.arg(0));
+	goto done;
+      }
+    }
     {
       expr bv = dualModel.eval(f);
       if(bv.is_app() && bv.decl().get_decl_kind() == Equal && 
@@ -843,6 +850,7 @@ namespace Duality {
       ands and, or, not. Returns result in memo. 
   */
 
+#if 0
   int RPFP::GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos){
     if(memo[labpos].find(f) != memo[labpos].end()){
       return memo[labpos][f];
@@ -918,13 +926,72 @@ namespace Duality {
     memo[labpos][f] = res;
     return res;
   }
+#endif
+
+  void RPFP::GetLabelsRec(hash_map<ast,int> &memo, const Term &f, std::vector<symbol> &labels,
+			  hash_set<ast> *done, bool truth){
+    if(done[truth].find(f) != done[truth].end())
+      return; /* already processed */
+    if(f.is_app()){
+      int nargs = f.num_args();
+      decl_kind k = f.decl().get_decl_kind();
+      if(k == Implies){
+	GetLabelsRec(memo,f.arg(1) || !f.arg(0) ,labels,done,truth);
+	goto done;
+      }
+      if(k == Iff){
+	int b = SubtermTruth(memo,f.arg(0));
+	if(b == 2)
+	  throw "disaster in GetLabelsRec";
+	GetLabelsRec(memo,f.arg(1),labels,done,truth ? b : !b);
+	goto done;
+      }
+      if(truth ? k == And : k == Or) {
+	for(int i = 0; i < nargs; i++)
+	  GetLabelsRec(memo,f.arg(i),labels,done,truth);
+	goto done;
+      }
+      if(truth ? k == Or : k == And) {
+	for(int i = 0; i < nargs; i++){
+	  Term a = f.arg(i);
+	  timer_start("SubtermTruth");
+	  int b = SubtermTruth(memo,a);
+	  timer_stop("SubtermTruth");
+	  if(truth ? (b == 1) : (b == 0)){
+	    GetLabelsRec(memo,a,labels,done,truth);
+	    goto done;
+	  }
+	}
+	/* Unreachable! */
+	throw "error in RPFP::GetLabelsRec";
+	goto done;
+      }
+      else if(k == Not) {
+	GetLabelsRec(memo,f.arg(0),labels,done,!truth);
+	goto done;
+      }
+      else {
+	bool pos; std::vector<symbol> names;
+	if(f.is_label(pos,names)){
+	  GetLabelsRec(memo,f.arg(0), labels, done, truth);
+	  if(pos == truth)
+	    for(unsigned i = 0; i < names.size(); i++)
+	      labels.push_back(names[i]);
+	  goto done;
+	}
+      }
+    }
+  done:
+    done[truth].insert(f);
+  }
 
   void RPFP::GetLabels(Edge *e, std::vector<symbol> &labels){
     if(!e->map || e->map->labeled.null())
       return;
     Term tl = Localize(e, e->map->labeled);
-    hash_map<ast,int> memo[2];
-    GetLabelsRec(memo,tl,labels,true);
+    hash_map<ast,int> memo;
+    hash_set<ast> done[2];
+    GetLabelsRec(memo,tl,labels,done,true);
   }
 
 #ifdef Z3OPS
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index 9ac3ec53e..bfdc382bf 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -30,9 +30,6 @@ Revision History:
 namespace Duality {
 
   solver::solver(Duality::context& c) : object(c), the_model(c) {
-    // TODO: the following is a HACK to enable proofs in the old smt solver
-    // When we stop using that solver, this hack can be removed
-    m().toggle_proof_mode(PGM_FINE);  
     params_ref p;
     p.set_bool("proof", true); // this is currently useless
     p.set_bool("model", true); 
diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index e57ba5826..e49b89775 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -117,7 +117,8 @@ void dl_interface::check_reset() {
 #endif
 
 
-  lbool dl_interface::query(::expr * query) {
+lbool dl_interface::query(::expr * query) {
+
   // TODO: you can only call this once!
   // we restore the initial state in the datalog context
   m_ctx.ensure_opened();