From c3eae9bf2ad9b67c6794def031b0293a10e06132 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 5 Jun 2013 17:02:13 -0700
Subject: [PATCH] working on incremental stratified inlining in duality

---
 src/duality/duality_solver.cpp      | 31 +++++++++++++++++++++++++----
 src/muz_qe/dl_cmds.cpp              |  4 ++--
 src/muz_qe/duality_dl_interface.cpp |  3 ++-
 3 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index e53ead302..40c82eac8 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -200,6 +200,9 @@ namespace Duality {
 	    best.insert(*it);
       }
 #endif
+
+      /** Called when done expanding a tree */
+      virtual void Done() {}
     };
     
 
@@ -749,7 +752,8 @@ namespace Duality {
       DoTopoSort();
       for(unsigned i = 0; i < leaves.size(); i++){
 	Node *node = leaves[i];
-	if(!SatisfyUpperBound(node))
+	bool res = SatisfyUpperBound(node);
+	if(!res)
 	  return false;
       }
       // don't leave any dangling nodes!
@@ -1429,6 +1433,7 @@ namespace Duality {
 	tree->AssertNode(top); // assert the negation of the top-level spec
 	timer_start("Build");
 	bool res = Build();
+	heuristic->Done();
 	timer_stop("Build");
 	timer_start("Pop");
 	tree->Pop(1);
@@ -2019,12 +2024,20 @@ namespace Duality {
       }
 
       ~ReplayHeuristic(){
-	delete old_cex.tree;
+	if(old_cex.tree)
+	  delete old_cex.tree;
       }
 
       // Maps nodes of derivation tree into old cex
       hash_map<Node *, Node*> cex_map;
       
+      void Done() {
+	cex_map.clear();
+	if(old_cex.tree)
+	  delete old_cex.tree;
+	old_cex.tree = 0; // only replay once!
+      }
+
       void ShowNodeAndChildren(Node *n){
 	std::cout << n->Name.name() << ": ";
 	std::vector<Node *> &chs = n->Outgoing->Children;
@@ -2033,8 +2046,18 @@ namespace Duality {
 	std::cout << std::endl;
       }
 
+      // HACK: When matching relation names, we drop suffixes used to
+      // make the names unique between runs. For compatibility
+      // with boggie, we drop suffixes beginning with @@
+      std::string BaseName(const std::string &name){
+	int pos = name.find("@@");
+	if(pos >= 1)
+	  return name.substr(0,pos);
+	return name;
+      }
+
       virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority){
-	if(!high_priority){
+	if(!high_priority || !old_cex.tree){
 	  Heuristic::ChooseExpand(choices,best,false);
 	  return;
 	}
@@ -2053,7 +2076,7 @@ namespace Duality {
 	    if(old_parent && old_parent->Outgoing){
 	      std::vector<Node *> &old_chs = old_parent->Outgoing->Children;
 	      for(unsigned i = 0, j=0; i < chs.size(); i++){
-		if(j < old_chs.size() && chs[i]->Name.name() == old_chs[j]->Name.name())
+		if(j < old_chs.size() && BaseName(chs[i]->Name.name().str()) == BaseName(old_chs[j]->Name.name().str()))
 		  cex_map[chs[i]] = old_chs[j++];
 		else {
 		  std::cout << "unmatched child: " << chs[i]->Name.name() << std::endl;
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp
index c88e7346e..ade4b633d 100644
--- a/src/muz_qe/dl_cmds.cpp
+++ b/src/muz_qe/dl_cmds.cpp
@@ -476,10 +476,10 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c
     ctx.insert(alloc(dl_query_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
-#ifndef _EXTERNAL_RELEASE
+    // #ifndef _EXTERNAL_RELEASE
     ctx.insert(alloc(dl_push_cmd, dl_ctx)); // not exposed to keep command-extensions simple.
     ctx.insert(alloc(dl_pop_cmd, dl_ctx));
-#endif
+    // #endif
 }
 
 void install_dl_cmds(cmd_context & ctx) {
diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index e53d79409..fd26a2a2b 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -340,7 +340,8 @@ void dl_interface::display_certificate(std::ostream& out) {
       func_decl cnst = orig_model.get_func_decl(i);
       if(locals.find(cnst) == locals.end()){
 	func_interp thing = orig_model.get_func_interp(cnst);
-	mod.register_decl(to_func_decl(cnst.raw()),thing);
+	::func_interp *thing_raw = thing;
+	mod.register_decl(to_func_decl(cnst.raw()),thing_raw->copy());
       }
     }
     model_v2_pp(out,mod);