From f13ccf8969ffa99b9913788d16bc2ed0a4497318 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Sep 2021 16:09:03 +0200 Subject: [PATCH] bv2char and char2bv with Clemens Signed-off-by: Nikolaj Bjorner --- src/ast/char_decl_plugin.cpp | 31 ++++++++++++++++++++++++++++++- src/ast/char_decl_plugin.h | 8 ++++++++ src/ast/seq_decl_plugin.cpp | 9 +++++++++ src/ast/seq_decl_plugin.h | 4 ++++ src/smt/theory_char.cpp | 34 ++++++++++++++++++++++++++++++++++ src/smt/theory_char.h | 2 ++ src/util/zstring.cpp | 15 ++++++--------- 7 files changed, 93 insertions(+), 10 deletions(-) diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 774309ed6..0f6f78486 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -48,7 +48,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, if (num_parameters != 1) msg << "incorrect number of parameters passed. Expected 1, received " << num_parameters; else if (arity != 0) - msg << "incorrect number of arguments passed. Expected 1, received " << arity; + msg << "incorrect number of arguments passed. Expected 0, received " << arity; else if (!parameters[0].is_int()) msg << "integer parameter expected"; else if (parameters[0].get_int() < 0) @@ -68,6 +68,32 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); + case OP_CHAR_TO_BV: + if (num_parameters != 0) + msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters; + else if (arity != 1) + msg << "incorrect number of arguments passed. Expected one character, received " << arity; + else if (m_char != domain[0]) + msg << "expected character sort argument"; + else { + bv_util b(m); + unsigned sz = num_bits(); + return m.mk_func_decl(symbol("char.to_bv"), arity, domain, b.mk_sort(sz), func_decl_info(m_family_id, k, 0, nullptr)); + } + m.raise_exception(msg.str()); + case OP_CHAR_FROM_BV: { + bv_util b(m); + if (num_parameters != 0) + msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters; + else if (arity != 1) + msg << "incorrect number of arguments passed. Expected one character, received " << arity; + else if (!b.is_bv_sort(domain[0]) || b.get_bv_size(domain[0]) != num_bits()) + msg << "expected bit-vector sort argument with " << num_bits(); + else { + m.mk_func_decl(symbol("char.to_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr)); + } + m.raise_exception(msg.str()); + } case OP_CHAR_IS_DIGIT: if (num_parameters != 0) msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters; @@ -77,6 +103,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_func_decl(symbol("char.is_digit"), arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); + default: UNREACHABLE(); } @@ -94,6 +121,8 @@ void char_decl_plugin::get_op_names(svector& op_names, symbol cons op_names.push_back(builtin_name("Char", OP_CHAR_CONST)); op_names.push_back(builtin_name("char.to_int", OP_CHAR_TO_INT)); op_names.push_back(builtin_name("char.is_digit", OP_CHAR_IS_DIGIT)); + op_names.push_back(builtin_name("char.to_bv", OP_CHAR_TO_BV)); + op_names.push_back(builtin_name("char.from_bv", OP_CHAR_FROM_BV)); } void char_decl_plugin::get_sort_names(svector& sort_names, symbol const& logic) { diff --git a/src/ast/char_decl_plugin.h b/src/ast/char_decl_plugin.h index 272c09844..3d934ffe4 100644 --- a/src/ast/char_decl_plugin.h +++ b/src/ast/char_decl_plugin.h @@ -34,6 +34,8 @@ enum char_op_kind { OP_CHAR_CONST, OP_CHAR_LE, OP_CHAR_TO_INT, + OP_CHAR_TO_BV, + OP_CHAR_FROM_BV, OP_CHAR_IS_DIGIT }; @@ -91,8 +93,14 @@ public: bool is_is_digit(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_IS_DIGIT); } + bool is_char2bv(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_TO_BV); } + + bool is_bv2char(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_FROM_BV); } + MATCH_UNARY(is_is_digit); MATCH_UNARY(is_to_int); + MATCH_UNARY(is_char2bv); + MATCH_UNARY(is_bv2char); MATCH_BINARY(is_le); static unsigned max_char() { return zstring::max_char(); } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 82ab83681..69ec244d5 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -798,6 +798,15 @@ bool seq_util::is_char2int(expr const* e) const { return ch.is_to_int(e); } +bool seq_util::is_bv2char(expr const* e) const { + return ch.is_bv2char(e); +} + +bool seq_util::is_char2bv(expr const* e) const { + return ch.is_char2bv(e); +} + + app* seq_util::mk_char(unsigned ch) const { return seq.mk_char(ch); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 6cd1398a9..f9589fee6 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -239,6 +239,8 @@ public: bool is_char_is_digit(expr const* e, expr*& d) const { return ch.is_is_digit(e, d); } bool is_char_is_digit(expr const* e) const { return ch.is_is_digit(e); } bool is_char2int(expr const* e) const; + bool is_bv2char(expr const* e) const; + bool is_char2bv(expr const* e) const; app* mk_char_bit(expr* e, unsigned i); app* mk_char(unsigned ch) const; app* mk_char_is_digit(expr* e) { return ch.mk_is_digit(e); } @@ -253,6 +255,8 @@ public: MATCH_BINARY(is_char_le); MATCH_UNARY(is_char2int); + MATCH_UNARY(is_char2bv); + MATCH_UNARY(is_bv2char); bool has_re() const { return seq.has_re(); } bool has_seq() const { return seq.has_seq(); } diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index a89693476..772438986 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -16,6 +16,7 @@ Author: --*/ #include "ast/ast_ll_pp.h" +#include "ast/bv_decl_plugin.h" #include "smt/theory_char.h" #include "smt/smt_context.h" #include "smt/smt_model_generator.h" @@ -84,6 +85,11 @@ namespace smt { expr* n = nullptr; if (seq.is_char2int(term, n)) new_char2int(v, n); + else if (seq.is_char2bv(term, n)) + new_char2bv(term, n); + else if (seq.is_bv2char(term, n)) + new_bv2char(v, n); + return true; } @@ -265,6 +271,34 @@ namespace smt { ctx.assign_eq(n1, n2, eq_justification(j)); } + void theory_char::new_char2bv(expr* b, expr* c) { + theory_var w = ctx.get_enode(c)->get_th_var(get_id()); + init_bits(w); + auto const& bits = get_bits(w); + bv_util bv(m); + SASSERT(bits.size() == bv.get_bv_size(b)); + unsigned i = 0; + for (auto bit1 : bits) { + auto bit2 = mk_literal(bv.mk_bit2bool(b, i++)); + ctx.mk_th_axiom(get_id(), ~bit1, bit2); + ctx.mk_th_axiom(get_id(), bit1, ~bit2); + } + } + + void theory_char::new_bv2char(theory_var v, expr* b) { + init_bits(v); + auto const& bits = get_bits(v); + bv_util bv(m); + SASSERT(bits.size() == bv.get_bv_size(b)); + unsigned i = 0; + for (auto bit1 : bits) { + auto bit2 = mk_literal(bv.mk_bit2bool(b, i++)); + ctx.mk_th_axiom(get_id(), ~bit1, bit2); + ctx.mk_th_axiom(get_id(), bit1, ~bit2); + } + } + + /** * 1. Check that values of classes are unique. diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h index 511bcbd10..8be817cda 100644 --- a/src/smt/theory_char.h +++ b/src/smt/theory_char.h @@ -57,6 +57,8 @@ namespace smt { bool final_check(); void new_const_char(theory_var v, unsigned c); void new_char2int(theory_var v, expr* c); + void new_bv2char(theory_var v, expr* b); + void new_char2bv(expr* n, expr* c); unsigned get_char_value(theory_var v); void internalize_le(literal lit, app* term); void internalize_is_digit(literal lit, app* term); diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp index 7352cea5c..9f61be171 100644 --- a/src/util/zstring.cpp +++ b/src/util/zstring.cpp @@ -86,16 +86,13 @@ zstring::zstring(char const* s) { } string_encoding zstring::get_encoding() { - if (gparams::get_value("encoding") == "unicode") { + if (gparams::get_value("encoding") == "unicode") + return unicode; + if (gparams::get_value("encoding") == "bmp") + return bmp; + if (gparams::get_value("encoding") == "ascii") + return ascii; return unicode; - } - if (gparams::get_value("encoding") == "bmp") { - return bmp; - } - if (gparams::get_value("encoding") == "ascii") { - return ascii; - } - return unicode; } bool zstring::well_formed() const {