mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fixes to self-contained character unicode
This commit is contained in:
parent
d0f1d8f59e
commit
696b3c79b9
|
@ -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<int>(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<int>(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<builtin_name>& 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<builtin_name>& 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) {
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue