From 696b3c79b99b855a777e8e44a7679de9f4dab78d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jan 2021 06:13:37 -0800 Subject: [PATCH] fixes to self-contained character unicode --- src/ast/char_decl_plugin.cpp | 36 +++++++++++++++++++++++++----------- src/ast/seq_decl_plugin.cpp | 7 +++++-- src/smt/theory_char.cpp | 19 +++++++++++++++---- src/smt/theory_char.h | 2 ++ 4 files changed, 47 insertions(+), 17 deletions(-) diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 19914b17b..ca25d04d5 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -19,6 +19,7 @@ Author: #include "util/zstring.h" #include "ast/char_decl_plugin.h" +#include "ast/ast_pp.h" char_decl_plugin::char_decl_plugin(): m_charc_sym("Char") { @@ -31,19 +32,33 @@ char_decl_plugin::~char_decl_plugin() { 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; + std::stringstream msg; switch (k) { case OP_CHAR_LE: - if (arity == 2 && domain[0] == m_char && domain[1] == m_char) + if (arity != 2) + msg << "incorrect number of arguments passed. Expected 2, received " << arity; + else if(domain[0] != m_char) + msg << "incorrect first argument type " << mk_pp(domain[0], *m_manager); + else if (domain[1] != m_char) + msg << "incorrect second argument type " << mk_pp(domain[1], *m_manager); + else 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"); + m.raise_exception(msg.str()); + 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())) + if (num_parameters != 1) + msg << "incorrect number of parameters passed. Expected 1, recieved " << num_parameters; + else if (arity != 0) + msg << "incorrect number of arguments passed. Expected 1, received " << arity; + else if (!parameters[0].is_int()) + msg << "integer parameter expected"; + else if (parameters[0].get_int() < 0) + msg << "non-negative parameter expected"; + else if (parameters[0].get_int() > static_cast(zstring::unicode_max_char())) + msg << "parameter expected within character range"; + else 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"); + m.raise_exception(msg.str()); default: UNREACHABLE(); } @@ -57,8 +72,7 @@ void char_decl_plugin::set_manager(ast_manager * m, family_id id) { } void char_decl_plugin::get_op_names(svector& op_names, symbol const& logic) { - // TODO: enable when character theory is turned on: - // op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); + op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); } void char_decl_plugin::get_sort_names(svector& sort_names, symbol const& logic) { @@ -91,7 +105,7 @@ app* char_decl_plugin::mk_char(unsigned u) { } expr* char_decl_plugin::get_some_value(sort* s) { - return mk_char(0); + return mk_char('A'); } app* char_decl_plugin::mk_le(expr* a, expr* b) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 7fb3623ad..dc472942b 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -257,8 +257,11 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_REPLACE_ALL] = alloc(psig, m, "str.replace_all", 1, 3, seqAseqAseqA, seqA); m_sigs[OP_STRING_CONST] = nullptr; m_sigs[_OP_CHAR_CONST] = nullptr; - sort* charTcharT[2] = { m_char, m_char }; - m_sigs[_OP_CHAR_LE] = unicode() ? alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT) : nullptr; + m_sigs[_OP_CHAR_LE] = nullptr; + if (unicode() && !_USE_CHAR_PLUGIN) { + sort* charTcharT[2] = { m_char, m_char }; + m_sigs[_OP_CHAR_LE] = alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT); + } m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[_OP_STRING_FROM_CHAR] = alloc(psig, m, "char", 1, 0, nullptr, strT); diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index 238d037ba..82432fe00 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -55,6 +55,15 @@ namespace smt { return (m_bits.size() > (unsigned)v) && !m_bits[v].empty(); } + theory_var theory_char::mk_var(enode* n) { + if (is_attached_to_var(n)) + return n->get_th_var(get_id()); + theory_var v = theory::mk_var(n); + ctx.attach_th_var(n, this, v); + ctx.mark_as_relevant(n); + return v; + } + bool theory_char::internalize_atom(app * term, bool gate_ctx) { for (auto arg : *term) mk_var(ensure_enode(arg)); @@ -70,7 +79,9 @@ namespace smt { for (auto arg : *term) mk_var(ensure_enode(arg)); - theory_var v = mk_var(ensure_enode(term)); + enode* e = ctx.e_internalized(term) ? ctx.get_enode(term) : ctx.mk_enode(term, false, m.is_bool(term), true); + + theory_var v = mk_var(e); unsigned c = 0; if (seq.is_const_char(term, c)) new_const_char(v, c); @@ -91,7 +102,7 @@ namespace smt { if (has_bits(v)) return; - expr* e = get_expr(v); + expr* e = m_th->get_expr(v); m_bits.reserve(v + 1); auto& bits = m_bits[v]; while ((unsigned) v >= m_ebits.size()) @@ -131,8 +142,8 @@ namespace smt { void theory_char::internalize_le(literal lit, app* term) { expr* x = nullptr, *y = nullptr; VERIFY(seq.is_char_le(term, x, y)); - theory_var v1 = ctx.get_enode(x)->get_th_var(get_id()); - theory_var v2 = ctx.get_enode(y)->get_th_var(get_id()); + theory_var v1 = ctx.get_enode(x)->get_th_var(m_th->get_id()); + theory_var v2 = ctx.get_enode(y)->get_th_var(m_th->get_id()); init_bits(v1); init_bits(v2); auto const& b1 = get_ebits(v1); diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h index ae4b22b29..d236f7320 100644 --- a/src/smt/theory_char.h +++ b/src/smt/theory_char.h @@ -57,6 +57,8 @@ namespace smt { void enforce_value_bound(theory_var v); void enforce_bits(); + theory_var mk_var(enode* n) override; + public: theory_char(context& ctx, family_id fid, theory * th);