From 1177be63913b2813f667d7202f09fe31f4a9688e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 May 2017 20:52:39 -0700
Subject: [PATCH] add common utility to set up seq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_setup.cpp | 30 +++++++++++++++++++-----------
 src/smt/smt_setup.h   |  3 ++-
 2 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 84e3dee32..820159d18 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -205,7 +205,7 @@ namespace smt {
     void setup::setup_QF_BVRE() {
         setup_QF_BV();
         setup_QF_LIA();
-        m_context.register_plugin(alloc(theory_seq, m_manager));
+        setup_seq();
     }
 
     void setup::setup_QF_UF(static_features const & st) {
@@ -705,7 +705,7 @@ namespace smt {
     }
 
     void setup::setup_QF_S() {
-        m_context.register_plugin(alloc(smt::theory_seq, m_manager));
+        setup_seq();
     }
 
     bool is_arith(static_features const & st) {
@@ -822,19 +822,23 @@ namespace smt {
         m_context.register_plugin(mk_theory_dl(m_manager));
     }
 
-    void setup::setup_seq(static_features const & st) {
+    void setup::setup_seq_str(static_features const & st) {
         // check params for what to do here when it's ambiguous
         if (m_params.m_string_solver == "z3str3") {
             setup_str();
-        } else if (m_params.m_string_solver == "seq") {
-            m_context.register_plugin(alloc(smt::theory_seq, m_manager));
-        } else if (m_params.m_string_solver == "auto") {
+        } 
+        else if (m_params.m_string_solver == "seq") {
+            setup_seq();
+        } 
+        else if (m_params.m_string_solver == "auto") {
             if (st.m_has_seq_non_str) {
-                m_context.register_plugin(alloc(smt::theory_seq, m_manager));
-            } else {
+                setup_seq();
+            } 
+            else {
                 setup_str();
             }
-        } else {
+        } 
+        else {
             throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
         }
     }
@@ -852,6 +856,10 @@ namespace smt {
         m_context.register_plugin(alloc(smt::theory_seq, m_manager));
     }
 
+    void setup::setup_seq() {
+        m_context.register_plugin(alloc(smt::theory_seq, m_manager));
+    }
+
     void setup::setup_unknown() {
         static_features st(m_manager);
         st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
@@ -861,7 +869,7 @@ namespace smt {
         setup_bv();
         setup_datatypes();
         setup_dl();
-        setup_seq(st);
+        setup_seq_str(st);
         setup_card();
         setup_fpa();
     }
@@ -876,7 +884,7 @@ namespace smt {
             setup_datatypes();
             setup_bv();
             setup_dl();
-            setup_seq(st);
+            setup_seq_str(st);
             setup_card();
             setup_fpa();
             return;
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index d30c896e5..80d5d7d1b 100644
--- a/src/smt/smt_setup.h
+++ b/src/smt/smt_setup.h
@@ -94,7 +94,8 @@ namespace smt {
         void setup_bv();
         void setup_arith();
         void setup_dl();
-        void setup_seq(static_features const & st);
+        void setup_seq_str(static_features const & st);
+        void setup_seq();
         void setup_card();
         void setup_i_arith();
         void setup_mi_arith();