From 67e73077773b6fa136c8a4896f5f2e55cfd77e9b Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 14 Dec 2016 15:00:17 -0500
Subject: [PATCH] add cut var debug info, wip

---
 src/smt/theory_str.cpp | 39 ++++++++++++++++++++++++++++++++++++++-
 src/smt/theory_str.h   |  2 ++
 2 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index b18d51a98..503485293 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -2481,6 +2481,43 @@ expr_ref theory_str::generate_mutual_exclusion(expr_ref_vector & terms) {
     return final_result;
 }
 
+void theory_str::print_cut_var(expr * node, std::ofstream & xout) {
+    ast_manager & m = get_manager();
+    /*
+#ifdef DEBUGLOG
+  __debugPrint(logFile, "\n>> CUT info of [");
+  printZ3Node(t, node);
+  __debugPrint(logFile, "]\n");
+
+  if (cut_VARMap.find(node) != cut_VARMap.end()) {
+    if (!cut_VARMap[node].empty()) {
+      __debugPrint(logFile, "[%2d] {", cut_VARMap[node].top()->level);
+      std::map<Z3_ast, int>::iterator itor = cut_VARMap[node].top()->vars.begin();
+      for (; itor != cut_VARMap[node].top()->vars.end(); itor++) {
+        printZ3Node(t, itor->first);
+        __debugPrint(logFile, ", ");
+      }
+      __debugPrint(logFile, "}\n");
+    } else {
+
+    }
+  }
+  __debugPrint(logFile, "------------------------\n\n");
+#endif
+*/
+    xout << "Cut info of " << mk_pp(node, m) << std::endl;
+    if (cut_var_map.contains(node)) {
+        if (!cut_var_map[node].empty()) {
+            xout << "[" << cut_var_map[node].top()->level << "] ";
+            std::map<expr*, int>::iterator itor = cut_var_map[node].top()->vars.begin();
+            for (; itor != cut_var_map[node].top()->vars.end(); ++itor) {
+                xout << mk_pp(itor->first, m) << ", ";
+            }
+            xout << std::endl;
+        }
+    }
+}
+
 /*
  * Handle two equivalent Concats.
  */
@@ -3013,7 +3050,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
         } else {
             loopDetected = true;
             TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
-            // TODO printCutVar(m, y);
+            TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);});
         }
 
         // break option 2:
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 2a9997517..73f8d9dcc 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -439,6 +439,8 @@ namespace smt {
         void process_concat_eq_type5(expr * concatAst1, expr * concatAst2);
         void process_concat_eq_type6(expr * concatAst1, expr * concatAst2);
 
+        void print_cut_var(expr * node, std::ofstream & xout);
+
         expr_ref generate_mutual_exclusion(expr_ref_vector & exprs);
 
         bool new_eq_check(expr * lhs, expr * rhs);