From 26ab91a4480f60a0c8ecd7a6d5cac8bc502eecc9 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 17 Jan 2018 13:02:32 -0500
Subject: [PATCH] check duplicate bounds info for regex terms

---
 src/smt/theory_str.cpp | 32 ++++++++++++++++++++++++++++++--
 src/smt/theory_str.h   |  5 +++++
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 474dd9c39..3dccc5681 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -9755,7 +9755,32 @@ namespace smt {
                 CTRACE("str", lower_bound_exists, tout << "lower bound of " << mk_pp(str, m) << " is " << lower_bound_value << std::endl;);
                 CTRACE("str", upper_bound_exists, tout << "upper bound of " << mk_pp(str, m) << " is " << upper_bound_value << std::endl;);
 
-                if (upper_bound_exists) {
+                bool new_lower_bound_info = true;
+                bool new_upper_bound_info = true;
+                // check last seen lower/upper bound to avoid performing duplicate work
+                if (regex_last_lower_bound.contains(str)) {
+                    rational last_lb_value;
+                    regex_last_lower_bound.find(str, last_lb_value);
+                    if (last_lb_value == lower_bound_value) {
+                        new_lower_bound_info = false;
+                    }
+                }
+                if (regex_last_upper_bound.contains(str)) {
+                    rational last_ub_value;
+                    regex_last_upper_bound.find(str, last_ub_value);
+                    if (last_ub_value == upper_bound_value) {
+                        new_upper_bound_info = false;
+                    }
+                }
+
+                if (new_lower_bound_info) {
+                    regex_last_lower_bound.insert(str, lower_bound_value);
+                }
+                if (new_upper_bound_info) {
+                    regex_last_upper_bound.insert(str, upper_bound_value);
+                }
+
+                if (upper_bound_exists && new_upper_bound_info) {
                     // check current assumptions
                     if (regex_automaton_assumptions.contains(re) &&
                             !regex_automaton_assumptions[re].empty()){
@@ -9869,7 +9894,7 @@ namespace smt {
                     }
                 } else { // !upper_bound_exists
                     // no upper bound information
-                    if (lower_bound_exists && !lower_bound_value.is_zero()) {
+                    if (lower_bound_exists && !lower_bound_value.is_zero() && new_lower_bound_info) {
                         // nonzero lower bound, no upper bound
 
                         // check current assumptions
@@ -9930,10 +9955,13 @@ namespace smt {
                                         rhs.push_back(ctx.mk_eq_atom(str_len, m_autil.mk_numeral(lower_bound_value, true)));
                                     } else {
                                         // If there are solutions at and above the lower bound, add an additional bound.
+                                        // DISABLED as this is causing non-termination in the integer solver. --mtrberzi
+                                        /*
                                         rhs.push_back(m.mk_or(
                                                 ctx.mk_eq_atom(str_len, m_autil.mk_numeral(lower_bound_value, true)),
                                                 m_autil.mk_ge(str_len, m_autil.mk_numeral(refined_lower_bound, true))
                                         ));
+                                        */
                                     }
                                 } else {
                                     if (refined_lower_bound.is_minus_one()) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 7398f599b..cf3958ceb 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -413,6 +413,11 @@ protected:
     obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)
     obj_map<expr, ptr_vector<expr> > regex_term_to_extra_length_vars; // extra length vars used in regex_term_to_length_constraint entries
 
+    // keep track of the last lower/upper bound we saw for each string term
+    // so we don't perform duplicate work
+    obj_map<expr, rational> regex_last_lower_bound;
+    obj_map<expr, rational> regex_last_upper_bound;
+
     // each counter maps a (str.in.re) expression to an integer.
     // use helper functions regex_inc_counter() and regex_get_counter() to access
     obj_map<expr, unsigned> regex_length_attempt_count;