mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixes for unicode

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-31 14:55:52 -08:00
parent 60cc9d8182
commit 6d99a8f0cc
3 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/char_decl_plugin.cpp
View file

@ -74,6 +74,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) { void char_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const& logic) {
op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); op_names.push_back(builtin_name("char.<=", OP_CHAR_LE));
op_names.push_back(builtin_name("Char", OP_CHAR_CONST));
} }
void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) { void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) {
@ -113,8 +114,14 @@ expr* char_decl_plugin::get_some_value(sort* s) {
app* char_decl_plugin::mk_le(expr* a, expr* b) { app* char_decl_plugin::mk_le(expr* a, expr* b) {
expr_ref _ch1(a, *m_manager), _ch2(b, *m_manager); expr_ref _ch1(a, *m_manager), _ch2(b, *m_manager);
unsigned v1 = 0, v2 = 0; unsigned v1 = 0, v2 = 0;
if (is_const_char(a, v1) && is_const_char(b, v2)) bool c1 = is_const_char(a, v1);
bool c2 = is_const_char(b, v2);
if (c1 && c2)
return m_manager->mk_bool_val(v1 <= v2); return m_manager->mk_bool_val(v1 <= v2);
if (c1 && v1 == 0)
return m_manager->mk_true();
if (c2 && v2 == max_char())
return m_manager->mk_true();
expr* es[2] = { a, b }; expr* es[2] = { a, b };
return m_manager->mk_app(m_family_id, OP_CHAR_LE, 2, es); return m_manager->mk_app(m_family_id, OP_CHAR_LE, 2, es);
} }

3
src/smt/theory_char.cpp
View file

@ -15,6 +15,7 @@ Author:
--*/ --*/
#include "ast/ast_ll_pp.h"
#include "smt/theory_char.h" #include "smt/theory_char.h"
#include "smt/smt_context.h" #include "smt/smt_context.h"
#include "smt/smt_model_generator.h" #include "smt/smt_model_generator.h"
@ -241,7 +242,7 @@ namespace smt {
enforce_ackerman(u, v); enforce_ackerman(u, v);
return false; return false;
} }
if (c >= seq.max_char()) { if (c > seq.max_char()) {
enforce_value_bound(v); enforce_value_bound(v);
return false; return false;
} }

2
src/util/zstring.cpp
View file

@ -45,7 +45,7 @@ bool zstring::is_escape_char(char const *& s, unsigned& result) {
unsigned d; unsigned d;
if (*s == '\\' && *(s+1) == 'u' && *(s+2) == '{') { if (*s == '\\' && *(s+1) == 'u' && *(s+2) == '{') {
result = 0; result = 0;
for (unsigned i = 0; i < 5; ++i) { for (unsigned i = 0; i < 6; ++i) {
if (is_hex_digit(*(s+3+i), d)) { if (is_hex_digit(*(s+3+i), d)) {
result = 16*result + d; result = 16*result + d;
} }