From 32058d9c68bf6b9413c2b3f1ba878b1fa0d470cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Jan 2021 16:43:03 -0800 Subject: [PATCH] add char_decl_plugin --- src/ast/char_decl_plugin.cpp | 89 ++++++++++++++++++++++++++++++++++++ src/ast/char_decl_plugin.h | 73 +++++++++++++++++++++++++++++ src/model/char_factory.h | 75 ++++++++++++++++++++++++++++++ src/model/seq_factory.h | 8 +--- src/smt/theory_char.cpp | 3 +- src/smt/theory_char.h | 4 +- 6 files changed, 241 insertions(+), 11 deletions(-) create mode 100644 src/ast/char_decl_plugin.cpp create mode 100644 src/ast/char_decl_plugin.h create mode 100644 src/model/char_factory.h diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp new file mode 100644 index 000000000..318b45d4f --- /dev/null +++ b/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(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& op_names, symbol const& logic) { + op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); +} + +void char_decl_plugin::get_sort_names(svector& 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, ¶m)); + return m_manager->mk_const(f); +} + +expr* char_decl_plugin::get_some_value(sort* s) { + return mk_char(0); +} diff --git a/src/ast/char_decl_plugin.h b/src/ast/char_decl_plugin.h new file mode 100644 index 000000000..ff26bc1e8 --- /dev/null +++ b/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 + +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& op_names, symbol const& logic) override; + + void get_sort_names(svector& 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; +}; diff --git a/src/model/char_factory.h b/src/model/char_factory.h new file mode 100644 index 000000000..997d3c4e0 --- /dev/null +++ b/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); + } + +}; + diff --git a/src/model/seq_factory.h b/src/model/seq_factory.h index 56df5f29d..8e952cc62 100644 --- a/src/model/seq_factory.h +++ b/src/model/seq_factory.h @@ -3,18 +3,12 @@ Copyright (c) 2011 Microsoft Corporation Module Name: - theory_seq_empty.h - -Abstract: - - + seq_factory.h Author: Nikolaj Bjorner (nbjorner) 2011-14-11 -Revision History: - --*/ #pragma once diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index 0a1c4c547..e8ec4a3fe 100644 --- a/src/smt/theory_char.cpp +++ b/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) { diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h index 9e1664c27..7f2f09343 100644 --- a/src/smt/theory_char.h +++ b/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;