From 612cc5cfbae49e09cddf57bea9541186197981f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Feb 2021 16:01:33 -0800 Subject: [PATCH] fix #5014 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 1 + src/ast/char_decl_plugin.cpp | 14 +++++++++++++- src/ast/char_decl_plugin.h | 7 ++++++- src/ast/seq_decl_plugin.cpp | 4 ++++ src/ast/seq_decl_plugin.h | 3 +++ src/sat/smt/ba_solver.cpp | 4 ---- src/smt/seq_axioms.cpp | 1 + src/smt/theory_char.cpp | 24 ++++++++++++++++++++++++ src/smt/theory_char.h | 1 + 9 files changed, 53 insertions(+), 6 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 72e843227..a27314f56 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -432,6 +432,7 @@ public: app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(m_afid, OP_ADD, num_args, args); } app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); } app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); } + app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.c_ptr()); } app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); } app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); } diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 848c78ead..e348dc4bc 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -17,6 +17,7 @@ Author: --*/ #include "util/gparams.h" #include "ast/char_decl_plugin.h" +#include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" char_decl_plugin::char_decl_plugin(): @@ -46,7 +47,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_CHAR_CONST: if (num_parameters != 1) - msg << "incorrect number of parameters passed. Expected 1, recieved " << num_parameters; + 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; else if (!parameters[0].is_int()) @@ -58,6 +59,16 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, 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(msg.str()); + case OP_CHAR_TO_INT: + 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 { + arith_util a(m); + 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()); default: UNREACHABLE(); } @@ -73,6 +84,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) { op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); op_names.push_back(builtin_name("Char", OP_CHAR_CONST)); + op_names.push_back(builtin_name("char.to_int", OP_CHAR_TO_INT)); } 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 48cd59aff..2bbf80261 100644 --- a/src/ast/char_decl_plugin.h +++ b/src/ast/char_decl_plugin.h @@ -32,7 +32,8 @@ enum char_sort_kind { enum char_op_kind { OP_CHAR_CONST, - OP_CHAR_LE + OP_CHAR_LE, + OP_CHAR_TO_INT }; class char_decl_plugin : public decl_plugin { @@ -76,12 +77,16 @@ public: app* mk_le(expr* a, expr* b); + app* mk_to_int(expr* a) { return m_manager->mk_app(m_family_id, OP_CHAR_TO_INT, 1, &a); } + bool is_le(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_LE); } bool is_const_char(expr const* e, unsigned& c) const { return is_app_of(e, m_family_id, OP_CHAR_CONST) && (c = to_app(e)->get_parameter(0).get_int(), true); } + bool is_to_int(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_TO_INT); } + bool unicode() const { return m_unicode; } unsigned max_char() const { return m_unicode ? zstring::unicode_max_char() : zstring::ascii_max_char(); } unsigned num_bits() const { return m_unicode ? zstring::unicode_num_bits() : zstring::ascii_num_bits(); } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 020896593..57ae9b564 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -767,6 +767,10 @@ bool seq_util::is_char_le(expr const* e) const { return ch.is_le(e); } +bool seq_util::is_char2int(expr const* e) const { + return ch.is_to_int(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 da8758dce..be5a64adc 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -234,10 +234,12 @@ public: bool is_const_char(expr* e, unsigned& c) const; bool is_const_char(expr* e) const { unsigned c; return is_const_char(e, c); } bool is_char_le(expr const* e) const; + bool is_char2int(expr const* e) const; app* mk_char_bit(expr* e, unsigned i); app* mk_char(unsigned ch) const; app* mk_le(expr* ch1, expr* ch2) const; app* mk_lt(expr* ch1, expr* ch2) const; + app* mk_char2int(expr* e) { return ch.mk_to_int(e); } unsigned max_char() const { return seq.max_char(); } unsigned num_bits() const { return seq.num_bits(); } @@ -245,6 +247,7 @@ public: bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); } MATCH_BINARY(is_char_le); + MATCH_UNARY(is_char2int); bool has_re() const { return seq.has_re(); } bool has_seq() const { return seq.has_seq(); } diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp index 67ff49c98..1e93090ca 100644 --- a/src/sat/smt/ba_solver.cpp +++ b/src/sat/smt/ba_solver.cpp @@ -1437,10 +1437,6 @@ namespace sat { bool ba_solver::init_watch(constraint& c) { - if (c.is_xr()) { - std::cout << c.is_xr() << "\n"; - } - return !inconsistent() && c.init_watch(*this); } diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index 42010ef5f..c1a8c35cc 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -813,6 +813,7 @@ void seq_axioms::add_str_to_code_axiom(expr* n) { literal len_is1 = mk_eq(mk_len(e), a.mk_int(1)); add_axiom(~len_is1, mk_ge(n, 0)); add_axiom(~len_is1, mk_le(n, seq.max_char())); + add_axiom(~len_is1, mk_eq(n, seq.mk_char2int(mk_nth(e, 0)))); if (!seq.str.is_from_code(e)) add_axiom(~len_is1, mk_eq(e, seq.str.mk_from_code(n))); add_axiom(len_is1, mk_eq(n, a.mk_int(-1))); diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index 9d2fa598f..5b17e7ed2 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -79,6 +79,9 @@ namespace smt { unsigned c = 0; if (seq.is_const_char(term, c)) new_const_char(v, c); + expr* n = nullptr; + if (seq.is_char2int(term, n)) + new_char2int(v, n); return true; } @@ -216,6 +219,27 @@ namespace smt { } } + void theory_char::new_char2int(theory_var v, expr* c) { + theory_var w = ctx.get_enode(c)->get_th_var(get_id()); + init_bits(w); + auto const& bits = get_ebits(w); + expr_ref_vector sum(m); + unsigned p = 0; + arith_util a(m); + for (auto b : bits) { + sum.push_back(m.mk_ite(b, a.mk_int(1 << p), a.mk_int(0))); + p++; + } + expr_ref sum_bits(a.mk_add(sum), m); + enode* n1 = get_enode(v); + enode* n2 = ensure_enode(sum_bits); + justification* j = + ctx.mk_justification( + ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), n1, n2)); + ctx.assign_eq(n1, n2, eq_justification(j)); + } + + /** * 1. Check that values of classes are unique. * Check that values within each class is the same. diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h index c1092f20d..146d522e4 100644 --- a/src/smt/theory_char.h +++ b/src/smt/theory_char.h @@ -57,6 +57,7 @@ namespace smt { bool final_check(); void new_const_char(theory_var v, unsigned c); + void new_char2int(theory_var v, expr* c); unsigned get_char_value(theory_var v); void internalize_le(literal lit, app* term);