From e9b31f29954ccc2252a5d122bcbe25b9f1601bc1 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Fri, 6 Nov 2015 14:13:38 -0500
Subject: [PATCH] temporarily patched in a get_eqc_allUnroll() implementation

---
 src/smt/theory_str.cpp | 26 +++++++++++++++++++++++++-
 src/smt/theory_str.h   |  4 ++++
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index cb31aedde..0965e7873 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -3263,7 +3263,7 @@ final_check_status theory_str::final_check_eh() {
     }
 
     // -----------------------------------------------------------
-    // variables in freeVar are those not bouned by Concats
+    // variables in freeVar are those not bounded by Concats
     // classify variables in freeVarMap:
     // (1) freeVar = unroll(r1, t1)
     // (2) vars are not bounded by either concat or unroll
@@ -3424,6 +3424,30 @@ void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
 	NOT_IMPLEMENTED_YET();
 }
 
+/*
+ * Collect all unroll functions
+ * and constant string in eqc of node n
+ */
+void theory_str::get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet) {
+  constStr = NULL;
+  unrollFuncSet.clear();
+  context & ctx = get_context();
+
+  expr * curr = n;
+  do {
+    if (is_string(to_app(curr))) {
+      constStr = curr;
+    } else if (false) /*(td->Unroll == Z3_get_app_decl(ctx, Z3_to_app(ctx, curr)))*/ { // TODO
+      if (unrollFuncSet.find(curr) == unrollFuncSet.end()) {
+        unrollFuncSet.insert(curr);
+      }
+    }
+    enode * e_curr = ctx.get_enode(curr);
+    curr = e_curr->get_next()->get_owner();
+    // curr = get_eqc_next(t, curr);
+  } while (curr != n);
+}
+
 void theory_str::init_model(model_generator & mg) {
     TRACE("t_str", tout << "initializing model" << std::endl; display(tout););
     m_factory = alloc(str_value_factory, get_manager(), get_family_id());
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 60c2c3a8e..86f45aea0 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -160,6 +160,10 @@ namespace smt {
         expr * getMostLeftNodeInConcat(expr * node);
         expr * getMostRightNodeInConcat(expr * node);
 
+        // strRegex
+
+        void get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);
+
         void dump_assignments();
     public:
         theory_str(ast_manager & m);