mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
bv2char and char2bv with Clemens
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
34f878fb97
commit
f13ccf8969
|
@ -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<builtin_name>& 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<builtin_name>& sort_names, symbol const& logic) {
|
||||
|
|
|
@ -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(); }
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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(); }
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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 {
|
||||
|
|
Loading…
Reference in a new issue