mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

fix #3076 - need to apply relevancy propagation in mk_bits. Assume bv v is already relevant but did not have bits associated with it, the bits need to then be marked as relevant

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-10 10:35:53 -07:00
parent df1b308dd0
commit bed2097fc4
5 changed files with 31 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/qe/qsat.cpp
View file

@ -548,11 +548,10 @@ namespace qe {
m_solver(mk_smt_solver(m, m_params, symbol::null))
{
m_params.set_bool("model", true);
m_params.set_uint("relevancy_lvl", 0);
m_params.set_uint("relevancy", 0);
m_params.set_uint("case_split_strategy", CS_ACTIVITY_WITH_CACHE);
m_solver->updt_params(m_params);
}
}
solver& s() { return *m_solver; }
solver const& s() const { return *m_solver; }

5
src/smt/smt_context.cpp
View file

@ -149,6 +149,9 @@ namespace smt {
void context::updt_params(params_ref const& p) {
m_params.append(p);
m_asserted_formulas.updt_params(p);
if (!m_setup.already_configured()) {
m_fparams.updt_params(p);
}
}
unsigned context::relevancy_lvl() const {
@ -308,7 +311,7 @@ namespace smt {
}
void context::assign_core(literal l, b_justification j, bool decision) {
CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << (decision?"decision: ":"propagating: ") << l << " ";
CTRACE("assign_core", l.var() == 2816, tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_smt2(tout, l); tout << " level: " << m_scope_lvl << "\n";
display(tout, j););
m_assigned_literals.push_back(l);

3
src/smt/smt_setup.cpp
View file

@ -152,6 +152,7 @@ namespace smt {
ptr_vector<expr> fmls;
m_context.get_asserted_formulas(fmls);
st.collect(fmls.size(), fmls.c_ptr());
TRACE("setup", st.display_primitive(tout););
IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
if (m_logic == "QF_UF")
setup_QF_UF(st);
@ -947,7 +948,7 @@ namespace smt {
ptr_vector<expr> fmls;
m_context.get_asserted_formulas(fmls);
st.collect(fmls.size(), fmls.c_ptr());
TRACE("setup", tout << "setup_unknown\n";);
TRACE("setup", tout << "setup_unknown\n";);
setup_arith();
setup_arrays();
setup_bv();

33
src/smt/theory_bv.cpp
View file

@ -53,6 +53,7 @@ namespace smt {
app * owner = n->get_owner();
unsigned bv_size = get_bv_size(n);
context & ctx = get_context();
bool is_relevant = ctx.is_relevant(n);
literal_vector & bits = m_bits[v];
TRACE("bv", tout << "v" << v << "\n";);
bits.reset();
@ -61,6 +62,9 @@ namespace smt {
ctx.internalize(bit, true);
bool_var b = ctx.get_bool_var(bit);
bits.push_back(literal(b));
if (is_relevant && !ctx.is_relevant(b)) {
ctx.mark_as_relevant(b);
}
}
}
@ -885,9 +889,7 @@ namespace smt {
find_wpos(v);
}
bool theory_bv::internalize_term(app * term) {
scoped_suspend_rlimit _suspend_cancel(get_manager().limit());
try {
bool theory_bv::internalize_term_core(app * term) {
SASSERT(term->get_family_id() == get_family_id());
TRACE("bv", tout << "internalizing term: " << mk_bounded_pp(term, get_manager()) << "\n";);
if (approximate_term(term)) {
@ -945,6 +947,12 @@ namespace smt {
UNREACHABLE();
return false;
}
}
bool theory_bv::internalize_term(app * term) {
scoped_suspend_rlimit _suspend_cancel(get_manager().limit());
try {
return internalize_term_core(term);
}
catch (z3_exception& ex) {
IF_VERBOSE(1, verbose_stream() << "internalize_term: " << ex.msg() << "\n";);
@ -1129,7 +1137,6 @@ namespace smt {
}
}
return false;
}
void theory_bv::apply_sort_cnstr(enode * n, sort * s) {
@ -1236,7 +1243,7 @@ namespace smt {
void theory_bv::assign_eh(bool_var v, bool is_true) {
atom * a = get_bv2a(v);
TRACE("bv", tout << "assert: b" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
TRACE("bv", tout << "assert: p" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
if (a->is_bit()) {
// The following optimization is not correct.
// Boolean variables created for performing bit-blasting are reused.
@ -1246,6 +1253,9 @@ namespace smt {
// TRACE("bv", tout << "has th_justification\n";);
// return;
// }
//for (auto kv : m_prop_queue) {
// std::cout << "v" << kv.first << "[" << kv.second << "]\n";
//}
m_prop_queue.reset();
bit_atom * b = static_cast<bit_atom*>(a);
var_pos_occ * curr = b->m_occs;
@ -1253,7 +1263,6 @@ namespace smt {
m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx));
curr = curr->m_next;
}
TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";);
propagate_bits();
#if WATCH_DISEQ
@ -1286,7 +1295,7 @@ namespace smt {
continue;
}
theory_var v2 = next(v);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << " " << ctx.get_scope_level() << "\n";);
TRACE("bv", tout << "propagating v" << v << " #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << " " << ctx.get_scope_level() << "\n";);
literal antecedent = bit;
if (val == l_false) {
@ -1307,7 +1316,7 @@ namespace smt {
}
assign_bit(consequent, v, v2, idx, antecedent, false);
if (ctx.inconsistent()) {
TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";);
TRACE("bv", tout << "inconsistent " << bit << " " << bit2 << "\n";);
m_prop_queue.reset();
return;
}
@ -1389,7 +1398,7 @@ namespace smt {
void theory_bv::relevant_eh(app * n) {
ast_manager & m = get_manager();
context & ctx = get_context();
TRACE("bv", tout << "relevant: " << mk_pp(n, m) << "\n";);
TRACE("bv", tout << "relevant: " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
if (m.is_bool(n)) {
bool_var v = ctx.get_bool_var(n);
atom * a = get_bv2a(v);
@ -1425,6 +1434,7 @@ namespace smt {
void theory_bv::push_scope_eh() {
theory::push_scope_eh();
m_trail_stack.push_scope();
// check_invariant();
#if WATCH_DISEQ
m_diseq_watch_lim.push_back(m_diseq_watch_trail.size());
#endif
@ -1504,7 +1514,7 @@ namespace smt {
void theory_bv::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
TRACE("bv", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";);
TRACE("bv", tout << "merging: v" << v1 << " #" << get_enode(v1)->get_owner_id() << " v" << v2 << " #" << get_enode(v2)->get_owner_id() << "\n";);
TRACE("bv_bit_prop", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";);
if (!merge_zero_one_bits(r1, r2)) {
TRACE("bv", tout << "conflict detected\n";);
@ -1540,6 +1550,7 @@ namespace smt {
SASSERT(bit1 != ~bit2);
lbool val1 = ctx.get_assignment(bit1);
lbool val2 = ctx.get_assignment(bit2);
TRACE("bv", tout << "merge v" << v1 << " " << bit1 << ":= " << val1 << " " << bit2 << ":= " << val2 << "\n";);
if (val1 == val2)
continue;
changed = true;
@ -1741,7 +1752,7 @@ namespace smt {
context & ctx = get_context();
literal_vector const & bits = m_bits[v];
for (literal lit : bits) {
out << " ";
out << " " << lit << ":";
ctx.display_literal(out, lit);
}
numeral val;

1
src/smt/theory_bv.h
View file

@ -173,6 +173,7 @@ namespace smt {
void fixed_var_eh(theory_var v);
void add_fixed_eq(theory_var v1, theory_var v2);
bool get_fixed_value(theory_var v, numeral & result) const;
bool internalize_term_core(app * term);
void internalize_num(app * n);
void internalize_add(app * n);
void internalize_sub(app * n);