mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

b-and, stats, reinsert variable to heap, debugging

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-11 20:22:23 -08:00
parent c03a05eb75
commit f388f58a4b
10 changed files with 55 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/arith_solver.cpp
View file

@ -1212,8 +1212,6 @@ namespace arith {
default:
UNREACHABLE();
}
if (lia_check == l_true && !check_band_terms())
lia_check = l_false;
return lia_check;
}

3
src/sat/smt/intblast_solver.cpp
View file

@ -257,6 +257,8 @@ namespace intblast {
lbool r = m_solver->check_sat(es);
m_solver->collect_statistics(m_stats);
IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
if (r == l_false) {
@ -975,5 +977,4 @@ namespace intblast {
st.copy(m_stats);
}
}

2
src/sat/smt/intblast_solver.h
View file

@ -137,7 +137,7 @@ namespace intblast {
sat::literal_vector const& unsat_core();
rational get_value(expr* e) const;
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values);
};

18
src/sat/smt/polysat/core.cpp
View file

@ -119,7 +119,7 @@ namespace polysat {
m_activity.pop_back();
m_justification.pop_back();
m_watch.pop_back();
m_values.pop_back();
m_values.pop_back();
m_var_queue.del_var_eh(v);
}
@ -160,6 +160,7 @@ namespace polysat {
s.add_eq_literal(m_var, m_value);
return sat::check_result::CR_CONTINUE;
case find_t::resource_out:
m_var_queue.unassign_var_eh(m_var);
return sat::check_result::CR_GIVEUP;
}
UNREACHABLE();
@ -342,8 +343,21 @@ namespace polysat {
for (auto const& [sc, d, value] : m_constraint_index)
out << sc << " " << d << " := " << value << "\n";
for (unsigned i = 0; i < m_vars.size(); ++i)
out << "p" << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n";
out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n";
m_var_queue.display(out << "vars ") << "\n";
return out;
}
bool core::try_eval(pdd const& p, rational& r) {
auto q = subst(p);
if (!q.is_val())
return false;
r = q.val();
return true;
}
void core::collect_statistics(statistics& st) const {
}
}

3
src/sat/smt/polysat/core.h
View file

@ -104,6 +104,9 @@ namespace polysat {
pdd value(rational const& v, unsigned sz);
pdd subst(pdd const&);
bool try_eval(pdd const& p, rational& r);
void collect_statistics(statistics& st) const;
signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
signed_constraint eq(pdd const& p, pdd const& q) { return m_constraints.eq(p - q); }

9
src/sat/smt/polysat_internalize.cpp
View file

@ -86,6 +86,7 @@ namespace polysat {
case OP_BSUB: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
case OP_BLSHR: internalize_lshr(a); break;
case OP_BSHL: internalize_shl(a); break;
case OP_BASHR: internalize_ashr(a); break;
case OP_BAND: internalize_band(a); break;
case OP_BOR: internalize_bor(a); break;
case OP_BXOR: internalize_bxor(a); break;
@ -148,7 +149,7 @@ namespace polysat {
case OP_BSDIV_I:
case OP_BSREM_I:
case OP_BSMOD_I:
case OP_BASHR:
IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
NOT_IMPLEMENTED_YET();
return;
@ -254,6 +255,12 @@ namespace polysat {
auto sc = m_core.lshr(expr2pdd(x), expr2pdd(y), expr2pdd(n));
}
void solver::internalize_ashr(app* n) {
expr* x, * y;
VERIFY(bv.is_bv_ashr(n, x, y));
auto sc = m_core.ashr(expr2pdd(x), expr2pdd(y), expr2pdd(n));
}
void solver::internalize_shl(app* n) {
expr* x, * y;
VERIFY(bv.is_bv_shl(n, x, y));

35
src/sat/smt/polysat_model.cpp
View file

@ -26,32 +26,18 @@ namespace polysat {
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
if (m_use_intblast_model) {
expr_ref value(m);
if (n->interpreted())
value = n->get_expr();
else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) {
bv_rewriter rw(m);
expr_ref_vector args(m);
for (auto arg : euf::enode_args(n))
args.push_back(values.get(arg->get_root_id()));
rw.mk_app(n->get_decl(), args.size(), args.data(), value);
VERIFY(value);
}
else {
rational r = m_intblast.get_value(n->get_expr());
verbose_stream() << ctx.bpp(n) << " := " << r << "\n";
value = bv.mk_numeral(r, get_bv_size(n));
}
values.set(n->get_root_id(), value);
TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
m_intblast.add_value(n, mdl, values);
return;
}
#if 0
auto p = expr2pdd(n->get_expr());
rational val;
VERIFY(m_polysat.try_eval(p, val));
values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n));
#endif
if (!m_core.try_eval(p, val)) {
ctx.s().display(verbose_stream());
verbose_stream() << ctx.bpp(n) << " := " << p << "\n";
UNREACHABLE();
}
VERIFY(m_core.try_eval(p, val));
values.set(n->get_root_id(), bv.mk_numeral(val, get_bv_size(n)));
}
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
@ -78,6 +64,11 @@ namespace polysat {
}
void solver::collect_statistics(statistics& st) const {
m_intblast.collect_statistics(st);
m_core.collect_statistics(st);
}
std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const {
return out;
}

6
src/sat/smt/polysat_solver.cpp
View file

@ -184,6 +184,9 @@ namespace polysat {
void solver::new_eq_eh(euf::th_eq const& eq) {
auto v1 = eq.v1(), v2 = eq.v2();
euf::enode* n = var2enode(v1);
if (!bv.is_bv(n->get_expr()))
return;
pdd p = var2pdd(v1);
pdd q = var2pdd(v2);
auto sc = m_core.eq(p, q);
@ -197,6 +200,9 @@ namespace polysat {
void solver::new_diseq_eh(euf::th_eq const& ne) {
euf::theory_var v1 = ne.v1(), v2 = ne.v2();
euf::enode* n = var2enode(v1);
if (!bv.is_bv(n->get_expr()))
return;
pdd p = var2pdd(v1);
pdd q = var2pdd(v2);
auto sc = ~m_core.eq(p, q);

3
src/sat/smt/polysat_solver.h
View file

@ -121,6 +121,7 @@ namespace polysat {
void internalize_bxnor(app* n);
void internalize_band(app* n);
void internalize_lshr(app* n);
void internalize_ashr(app* n);
void internalize_shl(app* n);
template<bool Signed, bool Reverse, bool Negated>
void internalize_le(app* n);
@ -174,7 +175,7 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override {}
void collect_statistics(statistics& st) const override;
euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx, get_id()); }
extension* copy(sat::solver* s) override { throw default_exception("nyi"); }
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}