add char_decl_plugin

src/ast/char_decl_plugin.cpp

@@ -0,0 +1,89 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    char_decl_plugin.cpp
+
+Abstract:
+
+    char_plugin for unicode suppport
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-01-26
+
+
+--*/
+#pragma once
+
+#include "util/zstring.h"
+#include "ast/char_decl_plugin.h"
+
+char_decl_plugin::char_decl_plugin() : m_charc_sym("Char") {
+}
+
+func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters,
+                        unsigned arity, sort* const* domain, sort* range) {
+    ast_manager& m = *m_manager;
+    switch (k) {
+    case OP_CHAR_LE:
+        if (arity == 2 && domain[0] == m_char && domain[1] == m_char) 
+            return m.mk_func_decl(symbol("char.<="), arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr));
+        m.raise_exception("Incorrect parameters passed to character comparison");
+    case OP_CHAR_CONST:
+        if (num_parameters == 1 && 
+            arity == 0 && 
+            parameters[0].is_int() && 
+            0 <= parameters[0].get_int() && 
+            parameters[0].get_int() < static_cast<int>(zstring::unicode_max_char()))
+            return m.mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, num_parameters, parameters));
+        m.raise_exception("invalid character declaration");
+    default:
+        UNREACHABLE();
+    }    
+    return nullptr;
+}
+
+void char_decl_plugin::set_manager(ast_manager * m, family_id id) {
+    decl_plugin::set_manager(m, id);
+    m_char = m->mk_sort(symbol("Unicode"), sort_info(m_family_id, CHAR_SORT, 0, nullptr));
+    m->inc_ref(m_char);
+}
+
+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));
+}
+
+void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) {
+    sort_names.push_back(builtin_name("Unicode",  CHAR_SORT));
+}
+
+bool char_decl_plugin::is_value(app* e) const {
+    return is_app_of(e, m_family_id, OP_CHAR_CONST);
+}
+
+bool char_decl_plugin::is_unique_value(app* e) const {
+    return is_value(e);
+}
+
+bool char_decl_plugin::are_equal(app* a, app* b) const {
+    return a == b;
+}
+
+bool char_decl_plugin::are_distinct(app* a, app* b) const {
+    return 
+        a != b && 
+        is_app_of(a, m_family_id, OP_CHAR_CONST) && 
+        is_app_of(b, m_family_id, OP_CHAR_CONST); 
+}
+
+app* char_decl_plugin::mk_char(unsigned u) {
+    parameter param(u);
+    func_decl* f = m_manager->mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, 1, &param));
+    return m_manager->mk_const(f);
+}
+
+expr* char_decl_plugin::get_some_value(sort* s) {
+    return mk_char(0);
+}

src/ast/char_decl_plugin.h

@@ -0,0 +1,73 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    char_decl_plugin.h
+
+Abstract:
+
+    char_plugin for unicode suppport
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2011-11-14
+
+Revision History:
+
+    Updated to string sequences 2015-12-5
+
+    Add SMTLIB 2.6 support 2020-5-17
+
+--*/
+#pragma once
+
+#include "ast/ast.h"
+#include "ast/bv_decl_plugin.h"
+#include <string>
+
+enum char_sort_kind {
+    CHAR_SORT
+};
+
+enum char_op_kind {
+    OP_CHAR_CONST,
+    OP_CHAR_LE
+};
+
+class char_decl_plugin : public decl_plugin {
+    sort* m_char { nullptr };
+    symbol m_charc_sym;
+
+    void set_manager(ast_manager * m, family_id id) override;
+
+public:
+    char_decl_plugin();
+
+    ~char_decl_plugin() override {}
+
+    void finalize() override {}
+
+    decl_plugin* mk_fresh() override { return alloc(char_decl_plugin); }
+
+    sort* mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override { return m_char; }
+
+    func_decl* mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters,
+        unsigned arity, sort* const* domain, sort* range) override;
+
+    void get_op_names(svector<builtin_name>& op_names, symbol const& logic) override;
+
+    void get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) override;
+
+    bool is_value(app* e) const override;
+
+    bool is_unique_value(app* e) const override;
+
+    bool are_equal(app* a, app* b) const override;
+
+    bool are_distinct(app* a, app* b) const override;
+
+    app* mk_char(unsigned u);
+
+    expr* get_some_value(sort* s) override;
+};

src/model/char_factory.h

@@ -0,0 +1,75 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    char_factory.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2011-14-11
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "util/uint_set.h"
+#include "ast/char_decl_plugin.h"
+#include "ast/seq_decl_plugin.h"
+#include "model/model_core.h"
+#include "model/value_factory.h"
+
+class char_factory : public value_factory {
+    model_core&  m_model;
+    ast_manager& m;
+    seq_util     u;
+    uint_set     m_chars;
+    unsigned     m_next { 'A' };
+    expr_ref_vector m_trail;
+
+public:
+    
+    char_factory(ast_manager & m, family_id fid, model_core& md):
+        value_factory(m, fid),
+        m_model(md),
+        m(m),
+        u(m),
+        m_trail(m)
+    {
+    }
+        
+    expr* get_some_value(sort* s) override {
+        m_chars.insert('a');
+        return u.mk_char('a');
+    }
+
+    bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) override {
+        v1 = u.mk_char('a');
+        v2 = u.mk_char('b');
+        m_chars.insert('a');
+        m_chars.insert('b');
+        return true;
+    }
+
+    expr* get_fresh_value(sort* s) override {
+        while (m_chars.contains(m_next)) 
+            ++m_next;
+        if (m_next > u.max_char())
+            throw default_exception("Character range exhausted");
+        m_chars.insert(m_next);
+        return u.mk_char(m_next++);        
+    }
+
+    void register_value(expr* n) override {
+        unsigned ch;
+        if (u.is_const_char(n, ch)) 
+            m_chars.insert(ch);
+    }
+
+    void add_trail(expr* e) {
+        m_trail.push_back(e);
+    }    
+
+};
+

src/model/seq_factory.h

@@ -3,18 +3,12 @@ Copyright (c) 2011 Microsoft Corporation
 
 Module Name:
 
-    theory_seq_empty.h
-
-Abstract:
-
-    <abstract>
+    seq_factory.h
 
 Author:
 
     Nikolaj Bjorner (nbjorner) 2011-14-11
 
-Revision History:
-
 --*/
 #pragma once
 

src/smt/theory_char.cpp

@@ -341,10 +341,9 @@ namespace smt {
         return true;
     }
 
-    // TBD: seq_factory needs to be replaced by a "char_factory" in the case where theory_char is
     // a stand-alone theory.
     void theory_char::init_model(model_generator & mg) {
-        m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
+        m_factory = alloc(char_factory, get_manager(), get_family_id(), mg.get_model());
     }
 
     model_value_proc * theory_char::mk_value(enode * n, model_generator & mg) {

src/smt/theory_char.h

@@ -19,7 +19,7 @@ Author:
 #include "ast/seq_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
-#include "model/seq_factory.h"
+#include "model/char_factory.h"
 #include "smt/smt_theory.h"
 
 namespace smt {
@@ -43,7 +43,7 @@ namespace smt {
         bit_blaster             m_bb;
         stats                   m_stats;
         symbol                  m_bits2char;
-        seq_factory*            m_factory { nullptr };
+        char_factory*           m_factory { nullptr };
 
         struct reset_bits;