mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

#5211

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-22 22:53:18 -07:00
parent 5d49cb5519
commit 67ec86fc66
4 changed files with 24 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/bv_decl_plugin.cpp
View file

@ -827,6 +827,15 @@ bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, ex
return true;
}
bool bv_recognizers::is_repeat(expr const * e, expr*& arg, unsigned& n) const {
if (!is_app_of(e, get_fid(), OP_REPEAT))
return false;
arg = to_app(e)->get_arg(0);
n = to_app(e)->get_parameter(0).get_int();
return true;
}
bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const {
if (!is_bv2int(e)) return false;
r = to_app(e)->get_arg(0);

1
src/ast/bv_decl_plugin.h
View file

@ -310,6 +310,7 @@ public:
unsigned get_extract_high(expr const * n) const { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
unsigned get_extract_low(expr const * n) const { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b) const;
bool is_repeat(expr const * e, expr*& arg, unsigned& n) const;
bool is_bv2int(expr const * e, expr * & r) const;
bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }

13
src/sat/smt/bv_internalize.cpp
View file

@ -213,6 +213,7 @@ namespace bv {
case OP_BSUB: internalize_sub(a); break;
case OP_CONCAT: internalize_concat(a); break;
case OP_EXTRACT: internalize_extract(a); break;
case OP_REPEAT: internalize_repeat(a); break;
case OP_MKBV: internalize_mkbv(a); break;
case OP_INT2BV: internalize_int2bv(a); break;
case OP_BV2INT: internalize_bv2int(a); break;
@ -641,6 +642,18 @@ namespace bv {
find_wpos(v);
}
void solver::internalize_repeat(app* e) {
unsigned n = 0;
expr* arg = nullptr;
VERIFY(bv.is_repeat(e, arg, n));
expr_ref_vector conc(m);
for (unsigned i = 0; i < n; ++i)
conc.push_back(arg);
expr_ref r(bv.mk_concat(conc), m);
mk_bits(get_th_var(e));
add_unit(eq_internalize(e, r));
}
void solver::internalize_bit2bool(app* n) {
unsigned idx = 0;
expr* arg = nullptr;

1
src/sat/smt/bv_solver.h
View file

@ -249,6 +249,7 @@ namespace bv {
void internalize_carry(app* n);
void internalize_sub(app* n);
void internalize_extract(app* n);
void internalize_repeat(app* n);
void internalize_bit2bool(app* n);
void internalize_udiv_i(app* n);
template<bool Signed, bool Reverse, bool Negated>