mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

hide bit-vector dependencies under seq_util

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-12-03 08:45:17 -08:00
parent dbfeeb8b1c
commit 2aa7ccc4a9
16 changed files with 89 additions and 97 deletions

34
src/ast/rewriter/seq_rewriter.cpp
View file

@ -45,14 +45,13 @@ expr_ref sym_expr::accept(expr* e) {
result = m.mk_eq(e, m_t);
break;
case t_range: {
bv_util bv(m);
rational r1, r2, r3;
unsigned sz;
if (bv.is_numeral(m_t, r1, sz) && bv.is_numeral(e, r2, sz) && bv.is_numeral(m_s, r3, sz)) {
seq_util u(m);
unsigned r1, r2, r3;
if (u.is_const_char(m_t, r1) && u.is_const_char(e, r2) && u.is_const_char(m_s, r3)) {
result = m.mk_bool_val((r1 <= r2) && (r2 <= r3));
}
else {
result = m.mk_and(bv.mk_ule(m_t, e), bv.mk_ule(e, m_s));
result = m.mk_and(u.mk_le(m_t, e), u.mk_le(e, m_s));
}
break;
}
@ -190,7 +189,7 @@ public:
}*/
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(nullptr), m_sa(nullptr) {}
re2automaton::re2automaton(ast_manager& m): m(m), u(m), m_ba(nullptr), m_sa(nullptr) {}
re2automaton::~re2automaton() {}
@ -248,9 +247,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
s1.length() == 1 && s2.length() == 1) {
unsigned start = s1[0];
unsigned stop = s2[0];
unsigned nb = s1.num_bits();
expr_ref _start(bv.mk_numeral(start, nb), m);
expr_ref _stop(bv.mk_numeral(stop, nb), m);
expr_ref _start(u.mk_char(start), m);
expr_ref _stop(u.mk_char(stop), m);
TRACE("seq", tout << "Range: " << start << " " << stop << "\n";);
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
return a.detach();
@ -463,14 +461,12 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
* (seq.unit (_ BitVector 8)) ==> String constant
*/
br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
bv_util bvu(m());
rational n_val;
unsigned int n_size;
unsigned ch;
// specifically we want (_ BitVector 8)
if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
if (m_util.is_const_char(e, ch)) {
// convert to string constant
zstring str(n_val.get_unsigned());
TRACE("seq_verbose", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
zstring str(ch);
TRACE("seq_verbose", tout << "rewrite seq.unit of 8-bit value " << ch << " to string constant \"" << str<< "\"" << std::endl;);
result = m_util.str.mk_string(str);
return BR_DONE;
}
@ -1977,15 +1973,13 @@ bool seq_rewriter::min_length(unsigned n, expr* const* es, unsigned& len) {
bool seq_rewriter::is_string(unsigned n, expr* const* es, zstring& s) const {
zstring s1;
expr* e;
bv_util bv(m());
rational val;
unsigned sz;
unsigned ch;
for (unsigned i = 0; i < n; ++i) {
if (m_util.str.is_string(es[i], s1)) {
s = s + s1;
}
else if (m_util.str.is_unit(es[i], e) && bv.is_numeral(e, val, sz)) {
s = s + zstring(val.get_unsigned());
else if (m_util.str.is_unit(es[i], e) && m_util.is_const_char(e, ch)) {
s = s + zstring(ch);
}
else {
return false;

1
src/ast/rewriter/seq_rewriter.h
View file

@ -77,7 +77,6 @@ class re2automaton {
ast_manager& m;
sym_expr_manager sm;
seq_util u;
bv_util bv;
scoped_ptr<expr_solver> m_solver;
scoped_ptr<boolean_algebra_t> m_ba;
scoped_ptr<symbolic_automata_t> m_sa;

19
src/ast/seq_decl_plugin.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "ast/arith_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/bv_decl_plugin.h"
#include <sstream>
static bool is_hex_digit(char ch, unsigned& d) {
@ -967,6 +968,24 @@ app* seq_util::str::mk_char(char ch) const {
return mk_char(s, 0);
}
bool seq_util::is_const_char(expr* e, unsigned& c) const {
bv_util bv(m);
rational r;
unsigned sz;
return bv.is_numeral(e, r, sz) && r.is_unsigned(), c = r.get_unsigned(), true;
}
app* seq_util::mk_char(unsigned ch) const {
bv_util bv(m);
return bv.mk_numeral(rational(ch), 8);
}
app* seq_util::mk_le(expr* ch1, expr* ch2) const {
bv_util bv(m);
return bv.mk_ule(ch1, ch2);
}
bool seq_util::str::is_string(expr const* n, zstring& s) const {
if (is_string(n)) {
s = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());

4
src/ast/seq_decl_plugin.h
View file

@ -22,7 +22,6 @@ Revision History:
#define SEQ_DECL_PLUGIN_H_
#include "ast/ast.h"
#include "ast/bv_decl_plugin.h"
enum seq_sort_kind {
@ -221,6 +220,9 @@ public:
bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
bool is_char(expr* e) const { return is_char(m.get_sort(e)); }
bool is_const_char(expr* e, unsigned& c) const;
app* mk_char(unsigned ch) const;
app* mk_le(expr* ch1, expr* ch2) const;
app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }

1
src/opt/opt_context.cpp
View file

@ -1573,7 +1573,6 @@ namespace opt {
m_model_converter->display(verbose_stream() << "mc\n");
model_smt2_pp(verbose_stream(), m, *mdl, 0);
verbose_stream() << to_string_internal() << "\n");
exit(0);
}
}
}

6
src/opt/pb_sls.cpp
View file

@ -403,10 +403,8 @@ namespace smt {
}
int new_break_count = flip(~lit);
if (-break_count != new_break_count) {
verbose_stream() << lit << "\n";
IF_VERBOSE(0, display(verbose_stream(), cls););
display(verbose_stream());
exit(0);
IF_VERBOSE(0, display(verbose_stream() << lit << "\n", cls);
display(verbose_stream()));
}
// VERIFY(-break_count == flip(~lit));
}

2
src/sat/ba_solver.cpp
View file

@ -676,7 +676,6 @@ namespace sat {
verbose_stream() << "alit: " << alit << "\n";
verbose_stream() << "num watch " << num_watch << "\n");
UNREACHABLE();
exit(0);
return l_undef;
}
@ -2606,7 +2605,6 @@ namespace sat {
IF_VERBOSE(0, s().display_watches(verbose_stream()));
UNREACHABLE();
exit(1);
return false;
}
}

1
src/sat/sat_drat.cpp
View file

@ -288,7 +288,6 @@ namespace sat {
display(tout);
s.display(tout););
UNREACHABLE();
exit(0);
}
}

2
src/sat/sat_model_converter.cpp
View file

@ -95,7 +95,7 @@ namespace sat {
IF_VERBOSE(0, display(verbose_stream() << "violated ate\n", *it) << "\n");
IF_VERBOSE(0, for (unsigned v = 0; v < m.size(); ++v) verbose_stream() << v << " := " << m[v] << "\n";);
IF_VERBOSE(0, display(verbose_stream()));
exit(0);
UNREACHABLE();
first = false;
}
if (!sat && it->get_kind() != ATE && v0 != null_bool_var) {

12
src/smt/smt_arith_value.cpp
View file

@ -92,8 +92,18 @@ namespace smt {
return false;
}
bool arith_value::get_value(expr* e, rational& val) const {
if (!m_ctx->e_internalized(e)) return false;
expr_ref _val(m);
enode* n = m_ctx->get_enode(e);
if (m_tha && m_tha->get_value(n, _val) && a.is_numeral(_val, val)) return true;
if (m_thi && m_thi->get_value(n, _val) && a.is_numeral(_val, val)) return true;
if (m_thr && m_thr->get_value(n, val)) return true;
return false;
}
bool arith_value::get_value(expr* e, rational& val) {
bool arith_value::get_value_equiv(expr* e, rational& val) const {
if (!m_ctx->e_internalized(e)) return false;
expr_ref _val(m);
enode* next = m_ctx->get_enode(e), *n = next;

3
src/smt/smt_arith_value.h
View file

@ -38,9 +38,10 @@ namespace smt {
void init(context* ctx);
bool get_lo_equiv(expr* e, rational& lo, bool& strict);
bool get_up_equiv(expr* e, rational& up, bool& strict);
bool get_value(expr* e, rational& value);
bool get_value_equiv(expr* e, rational& value) const;
bool get_lo(expr* e, rational& lo, bool& strict) const;
bool get_up(expr* e, rational& up, bool& strict) const;
bool get_value(expr* e, rational& value) const;
bool get_fixed(expr* e, rational& value) const;
final_check_status final_check();
};

1
src/smt/theory_bv.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "smt/theory_bv.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/bv_decl_plugin.h"
#include "smt/smt_model_generator.h"
#include "util/stats.h"

2
src/smt/theory_jobscheduler.cpp
View file

@ -576,7 +576,7 @@ namespace smt {
arith_value av(get_manager());
av.init(&get_context());
rational val;
if (av.get_value(e, val) && val.is_uint64()) {
if (av.get_value_equiv(e, val) && val.is_uint64()) {
return val.get_uint64();
}
return 0;

95
src/smt/theory_seq.cpp
View file

@ -3457,9 +3457,8 @@ void theory_seq::add_itos_axiom(expr* e) {
void theory_seq::ensure_digit_axiom() {
if (m_si_axioms.empty()) {
bv_util bv(m);
for (unsigned i = 0; i < 10; ++i) {
expr_ref cnst(bv.mk_numeral(rational('0'+i), bv.mk_sort(8)), m);
expr_ref cnst(m_util.mk_char('0'+i), m);
add_axiom(mk_eq(digit2int(cnst), m_autil.mk_int(i), false));
}
}
@ -3512,11 +3511,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
}
literal theory_seq::is_digit(expr* ch) {
bv_util bv(m);
literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, nullptr, nullptr, nullptr, m.mk_bool_sort()));
expr_ref d2i = digit2int(ch);
expr_ref _lo(bv.mk_ule(bv.mk_numeral(rational('0'), bv.mk_sort(8)), ch), m);
expr_ref _hi(bv.mk_ule(ch, bv.mk_numeral(rational('9'), bv.mk_sort(8))), m);
expr_ref _lo(m_util.mk_le(m_util.mk_char('0'), ch), m);
expr_ref _hi(m_util.mk_le(ch, m_util.mk_char('9')), m);
literal lo = mk_literal(_lo);
literal hi = mk_literal(_hi);
add_axiom(~lo, ~hi, isd);
@ -3817,18 +3815,17 @@ public:
SASSERT(values.size() == m_dependencies.size());
expr_ref_vector args(th.m);
unsigned j = 0, k = 0;
rational val;
bool is_string = th.m_util.is_string(m_sort);
expr_ref result(th.m);
if (is_string) {
unsigned_vector sbuffer;
bv_util bv(th.m);
rational val;
unsigned sz;
unsigned ch;
for (source_t src : m_source) {
switch (src) {
case unit_source: {
VERIFY(bv.is_numeral(values[j++], val, sz));
sbuffer.push_back(val.get_unsigned());
VERIFY(th.m_util.is_const_char(values[j++], ch));
sbuffer.push_back(ch);
break;
}
case string_source: {
@ -4634,32 +4631,9 @@ static T* get_th_arith(context& ctx, theory_id afid, expr* e) {
}
}
static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v) {
theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, afid, e);
if (tha) return tha->get_value(ctx.get_enode(e), v);
theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, afid, e);
if (thi) return thi->get_value(ctx.get_enode(e), v);
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr) return thr->get_value(ctx.get_enode(e), v);
TRACE("seq", tout << "no arithmetic theory\n";);
return false;
}
bool theory_seq::get_num_value(expr* e, rational& val) const {
context& ctx = get_context();
expr_ref _val(m);
if (!ctx.e_internalized(e))
return false;
enode* next = ctx.get_enode(e), *n = next;
do {
if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
return true;
}
next = next->get_next();
}
while (next != n);
TRACE("seq", tout << "no value for " << mk_pp(e, m) << "\n";);
return false;
return m_arith_value.get_value_equiv(e, val) && val.is_int();
}
bool theory_seq::lower_bound(expr* e, rational& lo) const {
@ -4748,9 +4722,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
}
else {
len = mk_len(c);
if (ctx.e_internalized(len) &&
get_arith_value(ctx, m_autil.get_family_id(), len, len_val) &&
m_autil.is_numeral(len_val, val1)) {
if (m_arith_value.get_value(len, val1)) {
val += val1;
}
else {
@ -5050,13 +5022,14 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
expr* theory_seq::coalesce_chars(expr* const& e) {
expr_ref theory_seq::coalesce_chars(expr* const& e) {
context& ctx = get_context();
expr* s;
unsigned ch;
expr_ref result(m);
if (m_util.str.is_concat(e)) {
expr_ref_vector concats(m);
expr_ref_vector rs(m), concats(m);
m_util.str.get_concat(e, concats);
expr_ref_vector result(m);
for (unsigned i = 0; i < concats.size(); ++i) {
expr_ref tmp(coalesce_chars(concats[i].get()), m);
if (m_util.str.is_empty(tmp)) continue;
@ -5076,32 +5049,30 @@ expr* theory_seq::coalesce_chars(expr* const& e) {
}
}
if (flag) {
result.push_back(m_util.str.mk_string(zs));
rs.push_back(m_util.str.mk_string(zs));
if (i < concats.size())
result.push_back(tmp);
rs.push_back(tmp);
}
else
result.push_back(tmp);
rs.push_back(tmp);
}
SASSERT(result.size() > 0);
if (result.size() > 1)
return m_util.str.mk_concat(result.size(), result.c_ptr());
else
return e;
}
else if (m_util.str.is_unit(e, s)) {
bv_util bvu(m);
if (bvu.is_bv(s)) {
expr_ref result(m);
expr * args[1] = {s};
if (BR_FAILED != m_seq_rewrite.mk_app_core(to_app(e)->get_decl(), 1, args, result)) {
if (!ctx.e_internalized(result))
ctx.internalize(result, false);
return result;
}
SASSERT(rs.size() > 0);
if (rs.size() > 1) {
return expr_ref(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
}
else {
result = e;
return result;
}
}
return e;
else if (m_util.str.is_unit(e, s) && m_util.is_const_char(s, ch) &&
BR_FAILED != m_seq_rewrite.mk_app_core(to_app(e)->get_decl(), 1, &s, result)) {
if (!ctx.e_internalized(result))
ctx.internalize(result, false);
return result;
}
result = e;
return result;
}
expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, expr*e4, sort* range) {
@ -5111,9 +5082,11 @@ expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3,
if (!range) {
range = m.get_sort(e1);
}
expr_ref_vector pinned(m);
if (name == m_seq_align) {
for (unsigned i = 0; i < len; ++i) {
es[i] = coalesce_chars(es[i]);
pinned.push_back(coalesce_chars(es[i]));
es[i] = pinned.back();
TRACE("seq", tout << mk_pp(es[i], m) << "\n";);
}
}

2
src/smt/theory_seq.h
View file

@ -606,7 +606,7 @@ namespace smt {
bool get_length(expr* s, rational& val) const;
void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
expr* coalesce_chars(expr* const& str);
expr_ref coalesce_chars(expr* const& str);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr);
bool is_skolem(symbol const& s, expr* e) const;

1
src/solver/solver.cpp
View file

@ -209,7 +209,6 @@ void solver::assert_expr(expr* f, expr* t) {
expr_ref a(t, m);
if (m_enforce_model_conversion) {
IF_VERBOSE(0, verbose_stream() << "enforce model conversion\n";);
exit(0);
model_converter_ref mc = get_model_converter();
if (mc) {
(*mc)(fml);