From f555074e27c6b570546cd27bd5410cf88af3faf1 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sat, 23 Jul 2016 23:29:56 -0400
Subject: [PATCH] add option to disable integer theory integration in
 theory_str; this is currently ENABLED

---
 src/smt/theory_str.cpp | 21 +++++++++++++++++++++
 src/smt/theory_str.h   | 16 ++++++++++++++++
 2 files changed, 37 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index d77290b46..35bc7ab20 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -34,6 +34,7 @@ theory_str::theory_str(ast_manager & m):
         opt_VerifyFinalCheckProgress(true),
 		opt_LCMUnrollStep(2),
 		opt_NoQuickReturn_Concat_IntegerTheory(true),
+		opt_DisableIntegerTheoryIntegration(true),
         /* Internal setup */
         search_started(false),
         m_autil(m),
@@ -3747,6 +3748,11 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
 }
 
 bool theory_str::get_value(expr* e, rational& val) const {
+    if (opt_DisableIntegerTheoryIntegration) {
+        TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
+        return false;
+    }
+
     context& ctx = get_context();
     ast_manager & m = get_manager();
     theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
@@ -3773,6 +3779,11 @@ bool theory_str::get_value(expr* e, rational& val) const {
 }
 
 bool theory_str::lower_bound(expr* _e, rational& lo) {
+    if (opt_DisableIntegerTheoryIntegration) {
+        TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
+        return false;
+    }
+
     context& ctx = get_context();
     ast_manager & m = get_manager();
     theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), _e);
@@ -3782,6 +3793,11 @@ bool theory_str::lower_bound(expr* _e, rational& lo) {
 }
 
 bool theory_str::upper_bound(expr* _e, rational& hi) {
+    if (opt_DisableIntegerTheoryIntegration) {
+        TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
+        return false;
+    }
+
     context& ctx = get_context();
     ast_manager & m = get_manager();
     theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), _e);
@@ -3791,6 +3807,11 @@ bool theory_str::upper_bound(expr* _e, rational& hi) {
 }
 
 bool theory_str::get_len_value(expr* e, rational& val) {
+    if (opt_DisableIntegerTheoryIntegration) {
+        TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
+        return false;
+    }
+
     context& ctx = get_context();
     ast_manager & m = get_manager();
     theory* th = ctx.get_theory(m_autil.get_family_id());
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index d2b51a712..0ba4a1a4d 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -100,9 +100,25 @@ namespace smt {
          * will not return from the function after asserting their axioms.
          * This means that control will fall through to the type 1-6 axioms,
          * causing those to be added as well.
+         * The default behaviour of Z3str2 is to set this to 'false'.
          */
         bool opt_NoQuickReturn_Concat_IntegerTheory;
 
+        /*
+         * If DisableIntegerTheoryIntegration is set to true,
+         * ALL calls to the integer theory integration methods
+         * (get_value, get_len_value, lower_bound, upper_bound)
+         * will ignore what the arithmetic solver believes about length terms,
+         * and will return no information.
+         *
+         * This reduces performance significantly, but can be useful to enable
+         * if it is suspected that string-integer integration, or the arithmetic solver itself,
+         * might have a bug.
+         *
+         * The default behaviour of Z3str2 is to set this to 'false'.
+         */
+        bool opt_DisableIntegerTheoryIntegration;
+
         bool search_started;
         arith_util m_autil;
         str_util m_strutil;