From 4535228fe2759bf2f3aac21aa699021848510749 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 4 Feb 2020 13:11:48 -0500
Subject: [PATCH] z3str3: mk_value searches equivalence class of terms for
 candidate model variables

---
 src/smt/theory_str.cpp    | 15 +++++++++++++++
 src/smt/theory_str_mc.cpp | 29 +++++++++++++++++++++++++++--
 2 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index edb34bba7..05f9b38eb 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -9621,6 +9621,21 @@ namespace smt {
         if (hasEqc) {
             return to_app(n_eqc);
         } else {
+            theory_var curr = get_var(n);
+            if (curr != null_theory_var) {
+                curr = m_find.find(curr);
+                theory_var first = curr;
+                do {
+                    expr* a = get_ast(curr);
+                    zstring val;
+                    if (candidate_model.find(a, val)) {
+                        return to_app(mk_string(val));
+                    }
+                    curr = m_find.next(curr);
+                }
+                while (curr != first && curr != null_theory_var);
+            }
+            // fail to find
             return nullptr;
         }
     }
diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index 9b692a91a..2a5f4ab7f 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -28,6 +28,7 @@
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "smt_kernel.h"
+#include "model/model_smt2_pp.h"
 
 namespace smt {
 
@@ -641,7 +642,7 @@ namespace smt {
             bool len_exists = v.get_value(arg2, len);
             ENSURE(pos_exists);
             ENSURE(len_exists);
-            TRACE("str_fl", tout << "reduce substring term: base=" << mk_pp(term, m) << ", pos=" << pos.to_string() << ", len=" << len.to_string() << std::endl;);
+            TRACE("str_fl", tout << "reduce substring term: base=" << mk_pp(term, m) << " (length="<<base_chars.size()<<"), pos=" << pos.to_string() << ", len=" << len.to_string() << std::endl;);
             // Case 1: pos < 0 or pos >= strlen(base) or len < 0
             // ==> (Substr ...) = ""
             if (pos.is_neg() || pos >= rational(base_chars.size()) || len.is_neg()) {
@@ -954,6 +955,23 @@ namespace smt {
             precondition.push_back(m.mk_eq(u.str.mk_length(var), mk_int(e.get_value())));
         }
 
+        TRACE_CODE(
+            if(is_trace_enabled("str_fl")) {
+                tout << "formulas asserted to bitvector subsolver:" << std::endl;
+                for (auto e : fixed_length_assumptions) {
+                    tout << mk_pp(e, subsolver.m()) << std::endl;
+                }
+                tout << "variable to character mappings:" << std::endl;
+                for (auto &entry : var_to_char_subterm_map) {
+                    tout << mk_pp(entry.m_key, get_manager()) << ":";
+                    for (auto e : entry.m_value) {
+                        tout << " " << mk_pp(e, subsolver.m());
+                    }
+                    tout << std::endl;
+                }
+            }
+        );
+
         TRACE("str_fl", tout << "calling subsolver" << std::endl;);
 
         lbool subproblem_status = subsolver.check(fixed_length_assumptions);
@@ -966,7 +984,7 @@ namespace smt {
 
             expr_substitution subst(m);
 
-            // model_smt2_pp(std::cout, m, *subModel, 2);
+            //model_smt2_pp(std::cout, m, *subModel, 2);
             for (auto entry : var_to_char_subterm_map) {
                 svector<unsigned> assignment;
                 expr * var = entry.m_key;
@@ -984,6 +1002,13 @@ namespace smt {
                 model.insert(var, strValue);
                 subst.insert(var, mk_string(strValue));
             }
+            TRACE_CODE(
+                if (is_trace_enabled("str_fl")) {
+                    for (auto entry : model) {
+                        tout << mk_pp(entry.m_key, m) << " = " << entry.m_value << std::endl;
+                    }
+                }
+            );
             for (auto entry : uninterpreted_to_char_subterm_map) {
                 svector<unsigned> assignment;
                 expr * var = entry.m_key;