mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #4114

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-26 16:12:56 -07:00
parent 51c3778354
commit 029edcfabd
5 changed files with 26 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_setup.cpp
View file

@ -566,7 +566,7 @@ namespace smt {
m_params.m_bv_cc = false; m_params.m_bv_cc = false;
m_params.m_bb_ext_gates = true; m_params.m_bb_ext_gates = true;
m_params.m_nnf_cnf = false; m_params.m_nnf_cnf = false;
m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params)); m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params));
} }
void setup::setup_QF_AUFBV() { void setup::setup_QF_AUFBV() {
@ -575,7 +575,7 @@ namespace smt {
m_params.m_bv_cc = false; m_params.m_bv_cc = false;
m_params.m_bb_ext_gates = true; m_params.m_bb_ext_gates = true;
m_params.m_nnf_cnf = false; m_params.m_nnf_cnf = false;
m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params)); m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params));
setup_arrays(); setup_arrays();
} }
@ -853,7 +853,7 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("bv"), "no bit-vector")); m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("bv"), "no bit-vector"));
break; break;
case BS_BLASTER: case BS_BLASTER:
m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params)); m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params));
break; break;
} }
} }

39
src/smt/theory_bv.cpp
View file

@ -127,7 +127,6 @@ namespace smt {
#if 0 #if 0
// possible fix for #2182, but effect of fix needs to be checked. // possible fix for #2182, but effect of fix needs to be checked.
if (idx < m_bits[v_arg].size()) { if (idx < m_bits[v_arg].size()) {
//std::cout << mk_pp(n, get_manager()) << "\n";
ctx.mk_th_axiom(get_id(), m_bits[v_arg][idx], literal(bv, true)); ctx.mk_th_axiom(get_id(), m_bits[v_arg][idx], literal(bv, true));
ctx.mk_th_axiom(get_id(), ~m_bits[v_arg][idx], literal(bv, false)); ctx.mk_th_axiom(get_id(), ~m_bits[v_arg][idx], literal(bv, false));
} }
@ -162,7 +161,7 @@ namespace smt {
e = ctx.get_enode(n); e = ctx.get_enode(n);
} }
else { else {
e = ctx.mk_enode(n, !m_params.m_bv_reflect, false, m_params.m_bv_cc); e = ctx.mk_enode(n, !params().m_bv_reflect, false, params().m_bv_cc);
mk_var(e); mk_var(e);
} }
// SASSERT(e->get_th_var(get_id()) != null_theory_var); // SASSERT(e->get_th_var(get_id()) != null_theory_var);
@ -179,7 +178,7 @@ namespace smt {
} }
enode * theory_bv::get_arg(enode * n, unsigned idx) { enode * theory_bv::get_arg(enode * n, unsigned idx) {
if (m_params.m_bv_reflect) { if (params().m_bv_reflect) {
return n->get_arg(idx); return n->get_arg(idx);
} }
else { else {
@ -933,15 +932,15 @@ namespace smt {
case OP_BSMOD0: return false; case OP_BSMOD0: return false;
case OP_MKBV: internalize_mkbv(term); return true; case OP_MKBV: internalize_mkbv(term); return true;
case OP_INT2BV: case OP_INT2BV:
if (m_params.m_bv_enable_int2bv2int) { if (params().m_bv_enable_int2bv2int) {
internalize_int2bv(term); internalize_int2bv(term);
} }
return m_params.m_bv_enable_int2bv2int; return params().m_bv_enable_int2bv2int;
case OP_BV2INT: case OP_BV2INT:
if (m_params.m_bv_enable_int2bv2int) { if (params().m_bv_enable_int2bv2int) {
internalize_bv2int(term); internalize_bv2int(term);
} }
return m_params.m_bv_enable_int2bv2int; return params().m_bv_enable_int2bv2int;
default: default:
TRACE("bv_op", tout << "unsupported operator: " << mk_ll_pp(term, get_manager()) << "\n";); TRACE("bv_op", tout << "unsupported operator: " << mk_ll_pp(term, get_manager()) << "\n";);
UNREACHABLE(); UNREACHABLE();
@ -985,7 +984,7 @@ namespace smt {
/* relevancy() is true and m_bv_lazy_le is false (the default configuration). */ \ /* relevancy() is true and m_bv_lazy_le is false (the default configuration). */ \
/* So, we need to check also the m_bv_lazy_le flag here. */ \ /* So, we need to check also the m_bv_lazy_le flag here. */ \
/* Maybe, we should rename the le_atom to bridge_atom, and m_bv_lazy_le option to m_bv_lazy_bridge. */ \ /* Maybe, we should rename the le_atom to bridge_atom, and m_bv_lazy_le option to m_bv_lazy_bridge. */ \
if (!ctx.relevancy() || !m_params.m_bv_lazy_le) { \ if (!ctx.relevancy() || !params().m_bv_lazy_le) { \
ctx.mk_th_axiom(get_id(), l, ~def); \ ctx.mk_th_axiom(get_id(), l, ~def); \
ctx.mk_th_axiom(get_id(), ~l, def); \ ctx.mk_th_axiom(get_id(), ~l, def); \
} \ } \
@ -1018,7 +1017,7 @@ namespace smt {
le_atom * a = new (get_region()) le_atom(l, def); le_atom * a = new (get_region()) le_atom(l, def);
insert_bv2a(l.var(), a); insert_bv2a(l.var(), a);
m_trail_stack.push(mk_atom_trail(l.var())); m_trail_stack.push(mk_atom_trail(l.var()));
if (!ctx.relevancy() || !m_params.m_bv_lazy_le) { if (!ctx.relevancy() || !params().m_bv_lazy_le) {
ctx.mk_th_axiom(get_id(), l, ~def); ctx.mk_th_axiom(get_id(), l, ~def);
ctx.mk_th_axiom(get_id(), ~l, def); ctx.mk_th_axiom(get_id(), ~l, def);
} }
@ -1120,14 +1119,14 @@ namespace smt {
// based on the number of bits used by the arguments. // based on the number of bits used by the arguments.
// //
bool theory_bv::approximate_term(app* n) { bool theory_bv::approximate_term(app* n) {
if (m_params.m_bv_blast_max_size == INT_MAX) { if (params().m_bv_blast_max_size == INT_MAX) {
return false; return false;
} }
unsigned num_args = n->get_num_args(); unsigned num_args = n->get_num_args();
for (unsigned i = 0; i <= num_args; i++) { for (unsigned i = 0; i <= num_args; i++) {
expr* arg = (i == num_args)?n:n->get_arg(i); expr* arg = (i == num_args)?n:n->get_arg(i);
sort* s = get_manager().get_sort(arg); sort* s = get_manager().get_sort(arg);
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) { if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) {
if (!m_approximates_large_bvs) { if (!m_approximates_large_bvs) {
TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";); TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";);
get_context().push_trail(value_trail<context, bool>(m_approximates_large_bvs)); get_context().push_trail(value_trail<context, bool>(m_approximates_large_bvs));
@ -1253,9 +1252,6 @@ namespace smt {
// TRACE("bv", tout << "has th_justification\n";); // TRACE("bv", tout << "has th_justification\n";);
// return; // return;
// } // }
//for (auto kv : m_prop_queue) {
// std::cout << "v" << kv.first << "[" << kv.second << "]\n";
//}
m_prop_queue.reset(); m_prop_queue.reset();
bit_atom * b = static_cast<bit_atom*>(a); bit_atom * b = static_cast<bit_atom*>(a);
var_pos_occ * curr = b->m_occs; var_pos_occ * curr = b->m_occs;
@ -1405,17 +1401,17 @@ namespace smt {
if (a && !a->is_bit()) { if (a && !a->is_bit()) {
le_atom * le = static_cast<le_atom*>(a); le_atom * le = static_cast<le_atom*>(a);
ctx.mark_as_relevant(le->m_def); ctx.mark_as_relevant(le->m_def);
if (m_params.m_bv_lazy_le) { if (params().m_bv_lazy_le) {
ctx.mk_th_axiom(get_id(), le->m_var, ~le->m_def); ctx.mk_th_axiom(get_id(), le->m_var, ~le->m_def);
ctx.mk_th_axiom(get_id(), ~le->m_var, le->m_def); ctx.mk_th_axiom(get_id(), ~le->m_var, le->m_def);
} }
} }
} }
else if (m_params.m_bv_enable_int2bv2int && m_util.is_bv2int(n)) { else if (params().m_bv_enable_int2bv2int && m_util.is_bv2int(n)) {
ctx.mark_as_relevant(n->get_arg(0)); ctx.mark_as_relevant(n->get_arg(0));
assert_bv2int_axiom(n); assert_bv2int_axiom(n);
} }
else if (m_params.m_bv_enable_int2bv2int && m_util.is_int2bv(n)) { else if (params().m_bv_enable_int2bv2int && m_util.is_int2bv(n)) {
ctx.mark_as_relevant(n->get_arg(0)); ctx.mark_as_relevant(n->get_arg(0));
assert_int2bv_axiom(n); assert_int2bv_axiom(n);
} }
@ -1492,9 +1488,12 @@ namespace smt {
return false; return false;
} }
theory_bv::theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params): smt_params const& theory_bv::params() const {
return get_context().get_fparams();
}
theory_bv::theory_bv(ast_manager & m, bit_blaster_params const & bb_params):
theory(m.mk_family_id("bv")), theory(m.mk_family_id("bv")),
m_params(params),
m_util(m), m_util(m),
m_autil(m), m_autil(m),
m_bb(m, bb_params), m_bb(m, bb_params),
@ -1509,7 +1508,7 @@ namespace smt {
} }
theory* theory_bv::mk_fresh(context* new_ctx) { theory* theory_bv::mk_fresh(context* new_ctx) {
return alloc(theory_bv, new_ctx->get_manager(), m_params, m_bb.get_params()); return alloc(theory_bv, new_ctx->get_manager(), new_ctx->get_fparams());
} }

4
src/smt/theory_bv.h
View file

@ -106,7 +106,6 @@ namespace smt {
atom * get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, 0); } atom * get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, 0); }
#endif #endif
theory_bv_stats m_stats; theory_bv_stats m_stats;
theory_bv_params const & m_params;
bv_util m_util; bv_util m_util;
arith_util m_autil; arith_util m_autil;
bit_blaster m_bb; bit_blaster m_bb;
@ -253,8 +252,9 @@ namespace smt {
void init_model(model_generator & m) override; void init_model(model_generator & m) override;
model_value_proc * mk_value(enode * n, model_generator & mg) override; model_value_proc * mk_value(enode * n, model_generator & mg) override;
smt_params const& params() const;
public: public:
theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params); theory_bv(ast_manager & m, bit_blaster_params const & bb_params);
~theory_bv() override; ~theory_bv() override;
theory * mk_fresh(context * new_ctx) override; theory * mk_fresh(context * new_ctx) override;

2
src/smt/theory_pb.cpp
View file

@ -451,7 +451,7 @@ namespace smt {
} }
theory * theory_pb::mk_fresh(context * new_ctx) { theory * theory_pb::mk_fresh(context * new_ctx) {
return alloc(theory_pb, new_ctx->get_manager(), m_params); return alloc(theory_pb, new_ctx->get_manager(), new_ctx->get_fparams());
} }
bool theory_pb::internalize_atom(app * atom, bool gate_ctx) { bool theory_pb::internalize_atom(app * atom, bool gate_ctx) {

2
src/smt/theory_seq.h
View file

@ -443,7 +443,7 @@ namespace smt {
void relevant_eh(app* n) override; void relevant_eh(app* n) override;
bool should_research(expr_ref_vector &) override; bool should_research(expr_ref_vector &) override;
void add_theory_assumptions(expr_ref_vector & assumptions) override; void add_theory_assumptions(expr_ref_vector & assumptions) override;
theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); } theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), new_ctx->get_fparams()); }
char const * get_name() const override { return "seq"; } char const * get_name() const override { return "seq"; }
bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); } bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); }
bool is_safe_to_copy(bool_var v) const; bool is_safe_to_copy(bool_var v) const;