missing

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

src/ast/char_decl_plugin.cpp

@@ -20,7 +20,12 @@ Author:
 #include "util/zstring.h"
 #include "ast/char_decl_plugin.h"
 
-char_decl_plugin::char_decl_plugin() : m_charc_sym("Char") {
+char_decl_plugin::char_decl_plugin(): 
+    m_charc_sym("Char") {
+}
+
+char_decl_plugin::~char_decl_plugin() {
+    m_manager->dec_ref(m_char);
 }
 
 func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters,
@@ -52,7 +57,8 @@ void char_decl_plugin::set_manager(ast_manager * m, family_id id) {
 }
 
 void char_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const& logic) {
-    op_names.push_back(builtin_name("char.<=", OP_CHAR_LE));
+    // TODO: enable when character theory is turned on:
+    // op_names.push_back(builtin_name("char.<=", OP_CHAR_LE));
 }
 
 void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) {

src/ast/char_decl_plugin.h

@@ -44,7 +44,7 @@ class char_decl_plugin : public decl_plugin {
 public:
     char_decl_plugin();
 
-    ~char_decl_plugin() override {}
+    ~char_decl_plugin() override;
 
     void finalize() override {}
 

src/ast/reg_decl_plugins.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "ast/datatype_decl_plugin.h"
 #include "ast/recfun_decl_plugin.h"
 #include "ast/dl_decl_plugin.h"
+#include "ast/char_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/fpa_decl_plugin.h"
@@ -51,6 +52,9 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("seq")))) {
         m.register_plugin(symbol("seq"), alloc(seq_decl_plugin));
     }
+    if (!m.get_plugin(m.mk_family_id(symbol("char")))) {
+        m.register_plugin(symbol("char"), alloc(char_decl_plugin));
+    }
     if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) {
         m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin));
     }

src/cmd_context/cmd_context.cpp

@@ -27,6 +27,7 @@ Notes:
 #include "ast/bv_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/char_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/fpa_decl_plugin.h"
@@ -701,6 +702,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
         register_plugin(symbol("recfun"),   alloc(recfun::decl::plugin), logic_has_recfun());
         register_plugin(symbol("seq"),      alloc(seq_decl_plugin), logic_has_seq());
+        register_plugin(symbol("char"),     alloc(char_decl_plugin), logic_has_seq());
         register_plugin(symbol("pb"),       alloc(pb_decl_plugin), logic_has_pb());
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
         register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
@@ -717,6 +719,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("array"),    logic_has_array(), fids);
         load_plugin(symbol("datatype"), logic_has_datatype(), fids);
         load_plugin(symbol("recfun"),   logic_has_recfun(), fids);
+        load_plugin(symbol("char"),      logic_has_seq(), fids);
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);

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_char.h"
 #include "smt/theory_special_relations.h"
 #include "smt/theory_pb.h"
 #include "smt/theory_fpa.h"
@@ -227,7 +228,7 @@ namespace smt {
     void setup::setup_QF_BVRE() {
         setup_QF_BV();
         setup_QF_LIA();
-        m_context.register_plugin(alloc(theory_seq, m_context));
+        setup_seq();
     }
 
     void setup::setup_QF_UF(static_features const & st) {        
@@ -725,7 +726,7 @@ namespace smt {
         }
  
         else if (m_params.m_string_solver == "empty") {
-            m_context.register_plugin(alloc(smt::theory_seq_empty, m_context));
+            setup_seq();
         }
         else if (m_params.m_string_solver == "none") {
             // don't register any solver.
@@ -895,7 +896,7 @@ namespace smt {
             setup_seq();
         } 
         else if (m_params.m_string_solver == "empty") {
-            m_context.register_plugin(alloc(smt::theory_seq_empty, m_context));
+            setup_seq();
         }
         else if (m_params.m_string_solver == "none") {
             // don't register any solver.
@@ -929,6 +930,18 @@ namespace smt {
 
     void setup::setup_seq() {
         m_context.register_plugin(alloc(smt::theory_seq, m_context));
+        setup_char();
+    }
+
+    void setup::setup_char() {
+        // temporary: enable only char theory if it is used in seq
+        seq_util seq(m_manager);
+        sort* ch = seq.mk_char_sort();
+        sort* s  = seq.mk_string_sort();
+        family_id ch_fid = ch->get_family_id();
+        if (s->get_family_id() != ch_fid)
+            m_context.register_plugin(alloc(smt::theory_char, m_context, ch_fid));
+
     }
 
     void setup::setup_special_relations() {

src/smt/smt_setup.h

@@ -100,6 +100,7 @@ namespace smt {
         void setup_dl();
         void setup_seq_str(static_features const & st);
         void setup_seq();
+        void setup_char();
         void setup_card();
         void setup_i_arith();
         void setup_mi_arith();