From 2c48ffe7a72ed88cb4a76e24242acba67f3b3635 Mon Sep 17 00:00:00 2001
From: Thai Trinh <trinhmt@comp.nus.edu.sg>
Date: Fri, 8 Dec 2017 13:41:18 +0800
Subject: [PATCH] Fixed setup_QF_S(): using configuration to choose the
 corresponding string solver

---
 src/smt/smt_setup.cpp | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 80543bb6f..fc7442008 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -123,8 +123,8 @@ namespace smt {
             setup_QF_FP();
         else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
             setup_QF_FPBV();
-//        else if (m_logic == "QF_S")
-//            setup_QF_S();
+        else if (m_logic == "QF_S")
+            setup_QF_S();
         else if (m_logic == "QF_DT")
             setup_QF_DT();
         else
@@ -170,8 +170,8 @@ namespace smt {
                  setup_QF_BVRE();
             else if (m_logic == "QF_AUFLIA")
                 setup_QF_AUFLIA(st);
-//            else if (m_logic == "QF_S")
-//                setup_QF_S();
+            else if (m_logic == "QF_S")
+                setup_QF_S();
             else if (m_logic == "AUFLIA")
                 setup_AUFLIA(st);
             else if (m_logic == "AUFLIRA")
@@ -723,8 +723,18 @@ namespace smt {
     }
 
     void setup::setup_QF_S() {
-        m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
-        m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
+        if (m_params.m_string_solver == "z3str3") {
+            setup_str();
+        }
+        else if (m_params.m_string_solver == "seq") {
+            setup_seq();
+        }
+        else if (m_params.m_string_solver == "auto") {
+            setup_seq();
+        }
+        else {
+            throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
+        }
     }
 
     bool is_arith(static_features const & st) {