From 8d5507008e2c52b15104eebe1062a6f8591fa6c1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Mar 2019 17:51:15 -0700
Subject: [PATCH] adding cmd_context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3/z3.py         | 3 +++
 src/cmd_context/cmd_context.cpp | 3 +++
 src/smt/smt_setup.cpp           | 6 ++++++
 src/smt/smt_setup.h             | 1 +
 4 files changed, 13 insertions(+)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index e3995ddb5..267a24a20 100644
--- a/src/api/python/z3/z3.py
+++ b/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
+
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 9de183ca8..9fbeced71 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/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) {
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 731034921..89213c86d 100644
--- a/src/smt/smt_setup.cpp
+++ b/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) {
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index 01a143301..53186f91c 100644
--- a/src/smt/smt_setup.h
+++ b/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);