From 51a40859103e671dd7bea8d7568b64e79818c4fc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Nov 2016 15:19:11 +0000
Subject: [PATCH] check for logic in solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 contrib/cmake/src/solver/CMakeLists.txt |   1 +
 src/api/api_solver.cpp                  |  17 ++-
 src/cmd_context/cmd_context.cpp         | 127 ++------------------
 src/cmd_context/cmd_context.h           |   7 --
 src/solver/smt_logics.cpp               | 149 ++++++++++++++++++++++++
 src/solver/smt_logics.h                 |  40 +++++++
 6 files changed, 213 insertions(+), 128 deletions(-)
 create mode 100644 src/solver/smt_logics.cpp
 create mode 100644 src/solver/smt_logics.h

diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt
index 7f54e7745..56864a691 100644
--- a/contrib/cmake/src/solver/CMakeLists.txt
+++ b/contrib/cmake/src/solver/CMakeLists.txt
@@ -3,6 +3,7 @@ z3_add_component(solver
     check_sat_result.cpp
     combined_solver.cpp
     mus.cpp
+    smt_logics.cpp
     solver.cpp
     solver_na2as.cpp
     solver2tactic.cpp
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 786a7c4ba..6dc41efb2 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -32,6 +32,7 @@ Revision History:
 #include"smt_strategic_solver.h"
 #include"smt_solver.h"
 #include"smt_implied_equalities.h"
+#include"smt_logics.h"
 
 extern "C" {
 
@@ -80,10 +81,18 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_solver_for_logic(c, logic);
         RESET_ERROR_CODE();
-        Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory(to_symbol(logic)));
-        mk_c(c)->save_object(s);
-        Z3_solver r = of_solver(s);
-        RETURN_Z3(r);
+        if (!smt_logics::supported_logic(to_symbol(logic))) {
+            std::ostringstream strm;
+            strm << "logic '" << to_symbol(logic) << "' is not recognized";
+            throw default_exception(strm.str());
+            RETURN_Z3(0);
+        }
+        else {
+            Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory(to_symbol(logic)));
+            mk_c(c)->save_object(s);
+            Z3_solver r = of_solver(s);
+            RETURN_Z3(r);
+        }
         Z3_CATCH_RETURN(0);
     }
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 930a8fc71..3cf00c154 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -45,6 +45,7 @@ Notes:
 #include"model_params.hpp"
 #include"th_rewriter.h"
 #include"tactic_exception.h"
+#include"smt_logics.h"
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
@@ -503,128 +504,32 @@ void cmd_context::load_plugin(symbol const & name, bool install, svector<family_
     fids.erase(id);
 }
 
-bool cmd_context::logic_has_arith_core(symbol const & s) const {
-    return
-        s == "QF_LRA" ||
-        s == "QF_LIA" ||
-        s == "QF_RDL" ||
-        s == "QF_IDL" ||
-        s == "QF_AUFLIA" ||
-        s == "QF_ALIA" ||
-        s == "QF_AUFLIRA" ||
-        s == "QF_AUFNIA" ||
-        s == "QF_AUFNIRA" ||
-        s == "QF_ANIA" ||
-        s == "QF_LIRA" ||
-        s == "QF_UFLIA" ||
-        s == "QF_UFLRA" ||
-        s == "QF_UFIDL" ||
-        s == "QF_UFRDL" ||
-        s == "QF_NIA" ||
-        s == "QF_NRA" ||
-        s == "QF_NIRA" ||
-        s == "QF_UFNRA" ||
-        s == "QF_UFNIA" ||
-        s == "QF_UFNIRA" ||
-        s == "QF_BVRE" ||
-        s == "ALIA" ||
-        s == "AUFLIA" ||
-        s == "AUFLIRA" ||
-        s == "AUFNIA" ||
-        s == "AUFNIRA" ||
-        s == "UFLIA" ||
-        s == "UFLRA" ||
-        s == "UFNRA" ||
-        s == "UFNIRA" ||
-        s == "NIA" ||
-        s == "NRA" ||
-        s == "UFNIA" ||
-        s == "LIA" ||
-        s == "LRA" ||
-        s == "UFIDL" ||
-        s == "QF_FP" ||
-        s == "QF_FPBV" ||
-        s == "QF_BVFP" ||
-        s == "QF_S" ||
-        s == "ALL" ||
-        s == "QF_FD" || 
-        s == "HORN";
-}
 
 bool cmd_context::logic_has_arith() const {
-    return !has_logic() || logic_has_arith_core(m_logic);
+    return !has_logic() || smt_logics::logic_has_arith(m_logic);
 }
 
-bool cmd_context::logic_has_bv_core(symbol const & s) const {
-    return
-        s == "UFBV" ||
-        s == "AUFBV" ||
-        s == "ABV" ||
-        s == "BV" ||
-        s == "QF_BV" ||
-        s == "QF_UFBV" ||
-        s == "QF_ABV" ||
-        s == "QF_AUFBV" ||
-        s == "QF_BVRE" ||
-        s == "QF_FPBV" ||
-        s == "QF_BVFP" ||
-        s == "ALL" ||
-        s == "QF_FD" ||
-        s == "HORN";
-}
 
-bool cmd_context::logic_has_horn(symbol const& s) const {
-    return s == "HORN";
-}
 
 bool cmd_context::logic_has_bv() const {
-    return !has_logic() || logic_has_bv_core(m_logic);
-}
-
-bool cmd_context::logic_has_seq_core(symbol const& s) const {
-    return s == "QF_BVRE" || s == "QF_S" || s == "ALL";
+    return !has_logic() || smt_logics::logic_has_bv(m_logic);
 }
 
 bool cmd_context::logic_has_seq() const {
-    return !has_logic() || logic_has_seq_core(m_logic);
-}
-
-bool cmd_context::logic_has_fpa_core(symbol const& s) const {
-    return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL";
+    return !has_logic() || smt_logics::logic_has_seq(m_logic);
 }
 
 bool cmd_context::logic_has_fpa() const {
-    return !has_logic() || logic_has_fpa_core(m_logic);
+    return !has_logic() || smt_logics::logic_has_fpa(m_logic);
 }
 
-bool cmd_context::logic_has_array_core(symbol const & s) const {
-    return
-        s == "QF_AX" ||
-        s == "QF_AUFLIA" ||
-        s == "QF_ANIA" ||
-        s == "QF_ALIA" ||
-        s == "QF_AUFLIRA" ||
-        s == "QF_AUFNIA" ||
-        s == "QF_AUFNIRA" ||
-        s == "ALIA" ||
-        s == "AUFLIA" ||
-        s == "AUFLIRA" ||
-        s == "AUFNIA" ||
-        s == "AUFNIRA" ||
-        s == "AUFBV" ||
-        s == "ABV" ||
-        s == "ALL" ||
-        s == "QF_ABV" ||
-        s == "QF_AUFBV" ||
-        s == "HORN";
-}
 
 bool cmd_context::logic_has_array() const {
-    return !has_logic() || logic_has_array_core(m_logic);
+    return !has_logic() || smt_logics::logic_has_array(m_logic);
 }
 
 bool cmd_context::logic_has_datatype() const {
-    return !has_logic() || m_logic == "QF_FD";
+    return !has_logic() || smt_logics::logic_has_datatype(m_logic);
 }
 
 void cmd_context::init_manager_core(bool new_manager) {
@@ -706,31 +611,19 @@ void cmd_context::init_external_manager() {
     init_manager_core(false);
 }
 
-bool cmd_context::supported_logic(symbol const & s) const {
-    return s == "QF_UF" || s == "UF" || s == "ALL" || s == "QF_FD" ||
-        logic_has_arith_core(s) || logic_has_bv_core(s) ||
-        logic_has_array_core(s) || logic_has_seq_core(s) ||
-        logic_has_horn(s) || logic_has_fpa_core(s);
-}
 
 bool cmd_context::set_logic(symbol const & s) {
     if (has_logic())
         throw cmd_exception("the logic has already been set");
     if (has_manager() && m_main_ctx)
         throw cmd_exception("logic must be set before initialization");
-    if (!supported_logic(s)) {
+    if (!smt_logics::supported_logic(s)) {
         return false;
     }
     m_logic = s;
-    if (is_logic("QF_RDL") ||
-        is_logic("QF_LRA") ||
-        is_logic("UFLRA") ||
-        is_logic("LRA") ||
-        is_logic("RDL") ||
-        is_logic("QF_NRA") ||
-        is_logic("QF_UFNRA") ||
-        is_logic("QF_UFLRA"))
+    if (smt_logics::logic_has_reals_only(s)) {
         m_numeral_as_real = true;
+    }
     return true;
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 097a9aff2..34d93c97b 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -249,19 +249,12 @@ protected:
     void erase_psort_decl_core(symbol const & s);
     void erase_macro_core(symbol const & s);
 
-    bool logic_has_arith_core(symbol const & s) const;
-    bool logic_has_bv_core(symbol const & s) const;
-    bool logic_has_array_core(symbol const & s) const;
-    bool logic_has_seq_core(symbol const & s) const;
-    bool logic_has_fpa_core(symbol const & s) const;
-    bool logic_has_horn(symbol const& s) const;
     bool logic_has_arith() const;
     bool logic_has_bv() const;
     bool logic_has_seq() const;
     bool logic_has_array() const;
     bool logic_has_datatype() const;
     bool logic_has_fpa() const;
-    bool supported_logic(symbol const & s) const;
 
     void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
     void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
new file mode 100644
index 000000000..9ee047839
--- /dev/null
+++ b/src/solver/smt_logics.cpp
@@ -0,0 +1,149 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    smt_logics.cpp
+
+Abstract:
+
+    Module for recognizing SMT logics.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-11-4
+
+Revision History:
+
+--*/
+#include "symbol.h"
+#include "smt_logics.h"
+
+
+
+bool smt_logics::supported_logic(symbol const & s) {
+    return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || 
+        logic_has_arith(s) || logic_has_bv(s) ||
+        logic_has_array(s) || logic_has_seq(s) ||
+        logic_has_horn(s) || logic_has_fpa(s);
+}
+
+bool smt_logics::logic_has_reals_only(symbol const& s) {
+    return 
+        s == "QF_RDL" ||
+        s == "QF_LRA" ||
+        s == "UFLRA" ||
+        s == "LRA" ||
+        s == "RDL" ||
+        s == "QF_NRA" ||
+        s == "QF_UFNRA" ||
+        s == "QF_UFLRA";
+}
+
+bool smt_logics::logic_has_arith(symbol const & s) {
+    return
+        s == "QF_LRA" ||
+        s == "QF_LIA" ||
+        s == "QF_RDL" ||
+        s == "QF_IDL" ||
+        s == "QF_AUFLIA" ||
+        s == "QF_ALIA" ||
+        s == "QF_AUFLIRA" ||
+        s == "QF_AUFNIA" ||
+        s == "QF_AUFNIRA" ||
+        s == "QF_ANIA" ||
+        s == "QF_LIRA" ||
+        s == "QF_UFLIA" ||
+        s == "QF_UFLRA" ||
+        s == "QF_UFIDL" ||
+        s == "QF_UFRDL" ||
+        s == "QF_NIA" ||
+        s == "QF_NRA" ||
+        s == "QF_NIRA" ||
+        s == "QF_UFNRA" ||
+        s == "QF_UFNIA" ||
+        s == "QF_UFNIRA" ||
+        s == "QF_BVRE" ||
+        s == "ALIA" ||
+        s == "AUFLIA" ||
+        s == "AUFLIRA" ||
+        s == "AUFNIA" ||
+        s == "AUFNIRA" ||
+        s == "UFLIA" ||
+        s == "UFLRA" ||
+        s == "UFNRA" ||
+        s == "UFNIRA" ||
+        s == "NIA" ||
+        s == "NRA" ||
+        s == "UFNIA" ||
+        s == "LIA" ||
+        s == "LRA" ||
+        s == "UFIDL" ||
+        s == "QF_FP" ||
+        s == "QF_FPBV" ||
+        s == "QF_BVFP" ||
+        s == "QF_S" ||
+        s == "ALL" ||
+        s == "QF_FD" || 
+        s == "HORN";
+}
+
+bool smt_logics::logic_has_bv(symbol const & s) {
+    return
+        s == "UFBV" ||
+        s == "AUFBV" ||
+        s == "ABV" ||
+        s == "BV" ||
+        s == "QF_BV" ||
+        s == "QF_UFBV" ||
+        s == "QF_ABV" ||
+        s == "QF_AUFBV" ||
+        s == "QF_BVRE" ||
+        s == "QF_FPBV" ||
+        s == "QF_BVFP" ||
+        s == "ALL" ||
+        s == "QF_FD" ||
+        s == "HORN";
+}
+
+bool smt_logics::logic_has_array(symbol const & s) {
+    return
+        s == "QF_AX" ||
+        s == "QF_AUFLIA" ||
+        s == "QF_ANIA" ||
+        s == "QF_ALIA" ||
+        s == "QF_AUFLIRA" ||
+        s == "QF_AUFNIA" ||
+        s == "QF_AUFNIRA" ||
+        s == "ALIA" ||
+        s == "AUFLIA" ||
+        s == "AUFLIRA" ||
+        s == "AUFNIA" ||
+        s == "AUFNIRA" ||
+        s == "AUFBV" ||
+        s == "ABV" ||
+        s == "ALL" ||
+        s == "QF_ABV" ||
+        s == "QF_AUFBV" ||
+        s == "HORN";
+}
+
+bool smt_logics::logic_has_seq(symbol const & s) {
+    return s == "QF_BVRE" || s == "QF_S" || s == "ALL";
+}
+
+bool smt_logics::logic_has_fpa(symbol const & s) {
+    return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL";
+}
+
+bool smt_logics::logic_has_uf(symbol const & s) {
+    return s == "QF_UF" || s == "UF";
+}
+
+bool smt_logics::logic_has_horn(symbol const& s) {
+    return s == "HORN";
+}
+
+bool smt_logics::logic_has_datatype(symbol const& s) {
+    return s == "QF_FD";
+}
diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h
new file mode 100644
index 000000000..f283040d9
--- /dev/null
+++ b/src/solver/smt_logics.h
@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    smt_logics.h
+
+Abstract:
+
+    Module for recognizing SMT logics.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-11-4
+
+Revision History:
+
+--*/
+#ifndef SMT_LOGICS_H_
+#define SMT_LOGICS_H_
+
+class smt_logics {
+public:
+    smt_logics() {}        
+    static bool supported_logic(symbol const & s);
+    static bool logic_has_reals_only(symbol const& l);       
+    static bool logic_is_all(symbol const& s) { return s == "ALL"; }
+    static bool logic_has_uf(symbol const& s);
+    static bool logic_has_arith(symbol const & s);
+    static bool logic_has_bv(symbol const & s);
+    static bool logic_has_array(symbol const & s);
+    static bool logic_has_seq(symbol const & s);
+    static bool logic_has_fpa(symbol const & s);
+    static bool logic_has_horn(symbol const& s);
+    static bool logic_has_fd(symbol const& s) { return s == "QF_FD"; }
+    static bool logic_has_datatype(symbol const& s);
+};
+
+#endif /* SMT_LOGICS_H_ */
+