mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix #3994 remove bogus option

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-16 18:51:52 -07:00
parent 767dff4a5a
commit 040d4b8d24
4 changed files with 9 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/bv_rewriter.cpp
View file

@ -33,7 +33,6 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
m_urem_simpl = p.bv_urem_simpl();
m_blast_eq_value = p.blast_eq_value();
m_split_concat_eq = p.split_concat_eq();
m_udiv2mul = p.udiv2mul();
m_bvnot2arith = p.bvnot2arith();
m_bvnot_simpl = p.bv_not_simpl();
m_bv_sort_ac = p.bv_sort_ac();
@ -1046,8 +1045,6 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
TRACE("bv_udiv", tout << "hi_div0: " << hi_div0 << "\n";);
TRACE("udiv2mul", tout << mk_ismt2_pp(arg2, m()) << " udiv2mul: " << m_udiv2mul << "\n";);
if (is_numeral(arg2, r2, bv_size)) {
r2 = m_util.norm(r2, bv_size);
if (r2.is_zero()) {
@ -1080,14 +1077,6 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
return BR_REWRITE1;
}
if (m_udiv2mul) {
TRACE("udiv2mul", tout << "using udiv2mul\n";);
numeral inv_r2;
if (m_util.mult_inverse(r2, bv_size, inv_r2)) {
result = m().mk_app(get_fid(), OP_BMUL, mk_numeral(inv_r2, bv_size), arg1);
return BR_REWRITE1;
}
}
result = m().mk_app(get_fid(), OP_BUDIV_I, arg1, arg2);
return BR_DONE;

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

@ -59,7 +59,6 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool m_mkbv2num;
bool m_ite2id;
bool m_split_concat_eq;
bool m_udiv2mul;
bool m_bvnot2arith;
bool m_bv_sort_ac;
bool m_trailing;

3
src/ast/rewriter/bv_rewriter_params.pyg
View file

@ -1,8 +1,7 @@
def_module_params(module_name='rewriter',
class_name='bv_rewriter_params',
export=True,
params=(("udiv2mul", BOOL, False, "convert constant udiv to mul"),
("split_concat_eq", BOOL, False, "split equalities of the form (= (concat t1 t2) t3)"),
params=(("split_concat_eq", BOOL, False, "split equalities of the form (= (concat t1 t2) t3)"),
("bit2bool", BOOL, True, "try to convert bit-vector terms of size 1 into Boolean terms"),
("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"),
("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),

15
src/smt/smt_context.cpp
View file

@ -913,12 +913,12 @@ namespace smt {
enode * parent = *it;
if (parent->is_cgc_enabled()) {
CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent),
tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" <<
parent->get_owner_id() << ", parents: \n";
for (unsigned i = 0; i < r2->m_parents.size(); i++) {
tout << "#" << r2->m_parents[i]->get_owner_id() << " ";
}
display(tout););
tout << "old num_parents: " << r2_num_parents
<< "\nnum_parents: " << r2->m_parents.size()
<< "\nparent: #" << parent->get_owner_id()
<< "\nparents: ";
for (enode* p : r2->m_parents) tout << "#" << p->get_owner_id() << " ";
display(tout << "\n"););
SASSERT(parent->is_cgr());
SASSERT(m_cg_table.contains_ptr(parent));
m_cg_table.erase(parent);
@ -930,7 +930,7 @@ namespace smt {
curr->m_root = r1;
curr = curr->m_next;
}
while(curr != r1);
while (curr != r1);
// restore parents of r2
r2->m_parents.shrink(r2_num_parents);
@ -939,6 +939,7 @@ namespace smt {
for (enode * parent : enode::parents(r1)) {
TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";);
if (parent->is_cgc_enabled()) {
enode * cg = parent->m_cg;
if (!parent->is_true_eq() &&
(parent == cg || // parent was root of the congruence class before and after the merge