adding cmd_context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/python/z3/z3.py

@@ -10353,3 +10353,6 @@ def Range(lo, hi, ctx = None):
     lo = _coerce_seq(lo, ctx)
     hi = _coerce_seq(hi, ctx)
     return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
+
+# Special Relations
+

src/cmd_context/cmd_context.cpp

@@ -31,6 +31,7 @@ Notes:
 #include "ast/pb_decl_plugin.h"
 #include "ast/fpa_decl_plugin.h"
 #include "ast/csp_decl_plugin.h"
+#include "ast/special_relations_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/pp.h"
@@ -687,6 +688,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
         register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
         register_plugin(symbol("csp"),      alloc(csp_decl_plugin), smt_logics::logic_is_csp(m_logic));
+        register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin), !has_logic());
     }
     else {
         // the manager was created by an external module
@@ -703,6 +705,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);
         load_plugin(symbol("csp"),      smt_logics::logic_is_csp(m_logic), fids);
+
         for (family_id fid : fids) {
             decl_plugin * p = m_manager->get_plugin(fid);
             if (p) {

src/smt/smt_setup.cpp

@@ -33,6 +33,7 @@ Revision History:
 #include "smt/theory_dl.h"
 #include "smt/theory_seq_empty.h"
 #include "smt/theory_seq.h"
+#include "smt/theory_special_relations.h"
 #include "smt/theory_pb.h"
 #include "smt/theory_fpa.h"
 #include "smt/theory_str.h"
@@ -935,6 +936,10 @@ namespace smt {
         m_context.register_plugin(alloc(smt::theory_jobscheduler, m_manager));
     }
 
+    void setup::setup_special_relations() {
+        m_context.register_plugin(alloc(smt::theory_special_relations, m_manager));
+    }
+
     void setup::setup_unknown() {
         static_features st(m_manager);
         ptr_vector<expr> fmls;
@@ -950,6 +955,7 @@ namespace smt {
         setup_seq_str(st);
         setup_card();
         setup_fpa();
+        setup_special_relations();
     }
 
     void setup::setup_unknown(static_features & st) {

src/smt/smt_setup.h

@@ -82,6 +82,7 @@ namespace smt {
         void setup_QF_S();
         void setup_LRA();
         void setup_CSP();
+        void setup_special_relations();
         void setup_AUFLIA(bool simple_array = true);
         void setup_AUFLIA(static_features const & st);
         void setup_AUFLIRA(bool simple_array = true);