mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
delay evaluation of model, throttle propagation, introduce LUT results into cutset
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
7b2f6791bc
commit
2d59b81353
14 changed files with 112 additions and 84 deletions
|
|
@ -404,6 +404,8 @@ public:
|
|||
void update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j);
|
||||
|
||||
|
||||
unsigned num_changed_bounds() const { return m_rows_with_changed_bounds.size(); }
|
||||
|
||||
void detect_rows_with_changed_bounds_for_column(unsigned j);
|
||||
|
||||
void detect_rows_with_changed_bounds();
|
||||
|
|
|
|||
|
|
@ -275,6 +275,18 @@ namespace sat {
|
|||
SASSERT(!m_aig[v].empty());
|
||||
}
|
||||
|
||||
void aig_cuts::add_cut(bool_var v, uint64_t lut, bool_var_vector const& args) {
|
||||
reserve(v);
|
||||
for (bool_var w : args) reserve(w);
|
||||
// optional: reshuffle lut and sort variables.
|
||||
cut c;
|
||||
for (bool_var w : args) VERIFY(c.add(w));
|
||||
c.set_table(lut);
|
||||
// add-don't care?
|
||||
insert_cut(v, c, m_cuts[v]);
|
||||
}
|
||||
|
||||
|
||||
void aig_cuts::set_root(bool_var v, literal r) {
|
||||
IF_VERBOSE(10, verbose_stream() << "set-root " << v << " -> " << r << "\n");
|
||||
m_roots.push_back(std::make_pair(v, r));
|
||||
|
|
|
|||
|
|
@ -158,6 +158,7 @@ namespace sat {
|
|||
aig_cuts();
|
||||
void add_var(unsigned v);
|
||||
void add_node(literal head, bool_op op, unsigned sz, literal const* args);
|
||||
void add_cut(bool_var v, uint64_t lut, bool_var_vector const& args);
|
||||
void set_root(bool_var v, literal r);
|
||||
|
||||
void set_on_clause_add(on_clause_t& on_clause_add);
|
||||
|
|
|
|||
|
|
@ -230,8 +230,9 @@ namespace sat {
|
|||
|
||||
#if 0
|
||||
std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut =
|
||||
[&,this](uint64_t l, bool_var_vector const& vars, bool_var v) {
|
||||
[&,this](uint64_t lut, bool_var_vector const& vars, bool_var v) {
|
||||
m_stats.m_xluts++;
|
||||
m_aig_cuts.add_cut(v, lut, vars);
|
||||
};
|
||||
lut_finder lf(s);
|
||||
lf.set(on_lut);
|
||||
|
|
|
|||
|
|
@ -513,7 +513,7 @@ namespace smt {
|
|||
if (m_asserted_formulas.inconsistent() || inconsistent()) {
|
||||
return l_false;
|
||||
}
|
||||
scoped_mk_model smk(*this);
|
||||
reset_model();
|
||||
init_search();
|
||||
flet<bool> l(m_searching, true);
|
||||
unsigned level = m_scope_lvl;
|
||||
|
|
|
|||
|
|
@ -3343,8 +3343,10 @@ namespace smt {
|
|||
r = l_undef;
|
||||
}
|
||||
if (r == l_true && gparams::get_value("model_validate") == "true") {
|
||||
model_ref mdl;
|
||||
get_model(mdl);
|
||||
for (theory* t : m_theory_set) {
|
||||
t->validate_model(*m_model);
|
||||
t->validate_model(*mdl);
|
||||
}
|
||||
#if 0
|
||||
for (literal lit : m_assigned_literals) {
|
||||
|
|
@ -3560,7 +3562,7 @@ namespace smt {
|
|||
return l_false;
|
||||
}
|
||||
timeit tt(get_verbosity_level() >= 100, "smt.stats");
|
||||
scoped_mk_model smk(*this);
|
||||
reset_model();
|
||||
SASSERT(at_search_level());
|
||||
TRACE("search", display(tout); display_enodes_lbls(tout););
|
||||
TRACE("search_detail", m_asserted_formulas.display(tout););
|
||||
|
|
@ -3594,35 +3596,34 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool context::restart(lbool& status, unsigned curr_lvl) {
|
||||
SASSERT(status != l_true || !inconsistent());
|
||||
|
||||
reset_model();
|
||||
|
||||
if (m_last_search_failure != OK) {
|
||||
if (status != l_false) {
|
||||
// build candidate model before returning
|
||||
mk_proto_model(status);
|
||||
// status = l_undef;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
if (status == l_false) {
|
||||
return false;
|
||||
}
|
||||
if (status == l_true) {
|
||||
SASSERT(!inconsistent());
|
||||
mk_proto_model(l_true);
|
||||
if (status == l_true && !m_qmanager->has_quantifiers()) {
|
||||
return false;
|
||||
}
|
||||
if (status == l_true && m_qmanager->has_quantifiers()) {
|
||||
// possible outcomes DONE l_true, DONE l_undef, CONTINUE
|
||||
mk_proto_model();
|
||||
quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
|
||||
if (cmr == quantifier_manager::SAT) {
|
||||
// done
|
||||
status = l_true;
|
||||
switch (cmr) {
|
||||
case quantifier_manager::SAT:
|
||||
return false;
|
||||
}
|
||||
if (cmr == quantifier_manager::UNKNOWN) {
|
||||
case quantifier_manager::UNKNOWN:
|
||||
IF_VERBOSE(2, verbose_stream() << "(smt.giveup quantifiers)\n";);
|
||||
// giving up
|
||||
m_last_search_failure = QUANTIFIERS;
|
||||
status = l_undef;
|
||||
return false;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
inc_limits();
|
||||
|
|
@ -3807,7 +3808,7 @@ namespace smt {
|
|||
|
||||
|
||||
if (m_fparams.m_model_on_final_check) {
|
||||
mk_proto_model(l_undef);
|
||||
mk_proto_model();
|
||||
model_pp(std::cout, *m_proto_model);
|
||||
std::cout << "END_OF_MODEL\n";
|
||||
std::cout.flush();
|
||||
|
|
@ -4395,15 +4396,16 @@ namespace smt {
|
|||
}
|
||||
TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";);
|
||||
if (fcs == FC_DONE) {
|
||||
mk_proto_model(l_true);
|
||||
m_model = m_proto_model->mk_model();
|
||||
add_rec_funs_to_model();
|
||||
reset_model();
|
||||
model_ref mdl;
|
||||
get_model(mdl);
|
||||
}
|
||||
|
||||
return fcs == FC_DONE;
|
||||
}
|
||||
|
||||
void context::mk_proto_model(lbool r) {
|
||||
void context::mk_proto_model() {
|
||||
if (m_model || m_proto_model) return;
|
||||
TRACE("get_model",
|
||||
display(tout);
|
||||
display_normalized_enodes(tout);
|
||||
|
|
@ -4412,9 +4414,10 @@ namespace smt {
|
|||
);
|
||||
failure fl = get_last_search_failure();
|
||||
if (fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) {
|
||||
TRACE("get_model", tout << "last search failure: " << fl << "\n";);
|
||||
}
|
||||
else if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) {
|
||||
TRACE("get_model", tout << "last search failure: " << fl << "\n";);
|
||||
}
|
||||
else if (m_fparams.m_model || m_fparams.m_model_on_final_check ||
|
||||
(m_qmanager->has_quantifiers() && m_qmanager->model_based())) {
|
||||
m_model_generator->reset();
|
||||
m_proto_model = m_model_generator->mk_model();
|
||||
m_qmanager->adjust_model(m_proto_model.get());
|
||||
|
|
@ -4427,8 +4430,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
proof * context::get_proof() {
|
||||
|
||||
proof * context::get_proof() {
|
||||
if (!m_unsat_proof) {
|
||||
m_unsat_proof = m_clause_proof.get_proof();
|
||||
}
|
||||
|
|
@ -4436,11 +4438,22 @@ namespace smt {
|
|||
return m_unsat_proof;
|
||||
}
|
||||
|
||||
void context::get_model(model_ref & m) const {
|
||||
void context::get_model(model_ref & m) {
|
||||
if (inconsistent())
|
||||
m = nullptr;
|
||||
else
|
||||
m = const_cast<model*>(m_model.get());
|
||||
else {
|
||||
mk_proto_model();
|
||||
if (!m_model && m_proto_model) {
|
||||
m_model = m_proto_model->mk_model();
|
||||
try {
|
||||
add_rec_funs_to_model();
|
||||
}
|
||||
catch (...) {
|
||||
// no op
|
||||
}
|
||||
}
|
||||
m = m_model.get();
|
||||
}
|
||||
}
|
||||
|
||||
void context::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
|
||||
|
|
@ -4459,10 +4472,6 @@ namespace smt {
|
|||
return result;
|
||||
}
|
||||
|
||||
void context::get_proto_model(proto_model_ref & m) const {
|
||||
m = const_cast<proto_model*>(m_proto_model.get());
|
||||
}
|
||||
|
||||
failure context::get_last_search_failure() const {
|
||||
return m_last_search_failure;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -215,27 +215,8 @@ namespace smt {
|
|||
proto_model_ref m_proto_model;
|
||||
model_ref m_model;
|
||||
std::string m_unknown;
|
||||
void mk_proto_model(lbool r);
|
||||
struct scoped_mk_model {
|
||||
context & m_ctx;
|
||||
scoped_mk_model(context & ctx):m_ctx(ctx) {
|
||||
m_ctx.m_proto_model = nullptr;
|
||||
m_ctx.m_model = nullptr;
|
||||
}
|
||||
~scoped_mk_model() {
|
||||
if (m_ctx.m_proto_model.get() != nullptr) {
|
||||
m_ctx.m_model = m_ctx.m_proto_model->mk_model();
|
||||
try {
|
||||
m_ctx.add_rec_funs_to_model();
|
||||
}
|
||||
catch (...) {
|
||||
// no op
|
||||
}
|
||||
m_ctx.m_proto_model = nullptr; // proto_model is not needed anymore.
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void mk_proto_model();
|
||||
void reset_model() { m_model = nullptr; m_proto_model = nullptr; }
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
|
@ -1614,12 +1595,12 @@ namespace smt {
|
|||
|
||||
expr_ref_vector get_trail();
|
||||
|
||||
void get_model(model_ref & m) const;
|
||||
void get_model(model_ref & m);
|
||||
|
||||
void set_model(model* m) { m_model = m; }
|
||||
|
||||
bool update_model(bool refinalize);
|
||||
|
||||
void get_proto_model(proto_model_ref & m) const;
|
||||
|
||||
bool validate_model();
|
||||
|
||||
unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); }
|
||||
|
|
|
|||
|
|
@ -132,7 +132,7 @@ namespace smt {
|
|||
return m_kernel.find_mutexes(vars, mutexes);
|
||||
}
|
||||
|
||||
void get_model(model_ref & m) const {
|
||||
void get_model(model_ref & m) {
|
||||
m_kernel.get_model(m);
|
||||
}
|
||||
|
||||
|
|
@ -315,7 +315,7 @@ namespace smt {
|
|||
return m_imp->find_mutexes(vars, mutexes);
|
||||
}
|
||||
|
||||
void kernel::get_model(model_ref & m) const {
|
||||
void kernel::get_model(model_ref & m) {
|
||||
m_imp->get_model(m);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -153,7 +153,7 @@ namespace smt {
|
|||
/**
|
||||
\brief Return the model associated with the last check command.
|
||||
*/
|
||||
void get_model(model_ref & m) const;
|
||||
void get_model(model_ref & m);
|
||||
|
||||
/**
|
||||
\brief Return the proof of unsatisfiability associated with the last check command.
|
||||
|
|
|
|||
|
|
@ -206,7 +206,7 @@ namespace smt {
|
|||
case l_true:
|
||||
pctx.get_model(mdl);
|
||||
if (mdl) {
|
||||
ctx.m_model = mdl->translate(tr);
|
||||
ctx.set_model(mdl->translate(tr));
|
||||
}
|
||||
break;
|
||||
case l_false:
|
||||
|
|
|
|||
|
|
@ -165,6 +165,8 @@ namespace smt {
|
|||
m_plugin->add(q);
|
||||
}
|
||||
|
||||
bool has_quantifiers() const { return !m_quantifiers.empty(); }
|
||||
|
||||
void display_stats(std::ostream & out, quantifier * q) {
|
||||
quantifier_stat * s = get_stat(q);
|
||||
unsigned num_instances = s->get_num_instances();
|
||||
|
|
@ -478,6 +480,10 @@ namespace smt {
|
|||
return m_imp->m_plugin->model_based();
|
||||
}
|
||||
|
||||
bool quantifier_manager::has_quantifiers() const {
|
||||
return m_imp->has_quantifiers();
|
||||
}
|
||||
|
||||
bool quantifier_manager::mbqi_enabled(quantifier *q) const {
|
||||
return m_imp->m_plugin->mbqi_enabled(q);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -79,6 +79,7 @@ namespace smt {
|
|||
};
|
||||
|
||||
bool model_based() const;
|
||||
bool has_quantifiers() const;
|
||||
bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
|
||||
void adjust_model(proto_model * m);
|
||||
check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
|
||||
|
|
|
|||
|
|
@ -1623,7 +1623,7 @@ public:
|
|||
svector<lpvar> vars;
|
||||
theory_var sz = static_cast<theory_var>(th.get_num_vars());
|
||||
for (theory_var v = 0; v < sz; ++v) {
|
||||
if (can_be_used_in_random_update(v))
|
||||
if (th.is_relevant_and_shared(get_enode(v)))
|
||||
vars.push_back(get_lpvar(v));
|
||||
}
|
||||
if (vars.empty()) {
|
||||
|
|
@ -2368,20 +2368,36 @@ public:
|
|||
|
||||
}
|
||||
|
||||
void propagate_bounds_with_lp_solver() {
|
||||
if (BP_NONE == propagation_mode()) {
|
||||
return;
|
||||
unsigned m_propagation_delay{1};
|
||||
unsigned m_propagation_count{0};
|
||||
|
||||
bool should_propagate() {
|
||||
++m_propagation_count;
|
||||
return BP_NONE != propagation_mode() && (m_propagation_count >= m_propagation_delay);
|
||||
}
|
||||
|
||||
void update_propagation_threshold(bool made_progress) {
|
||||
m_propagation_count = 0;
|
||||
if (made_progress) {
|
||||
m_propagation_delay = std::max(1u, m_propagation_delay-1u);
|
||||
}
|
||||
int num_of_p = lp().settings().stats().m_num_of_implied_bounds;
|
||||
(void)num_of_p;
|
||||
else {
|
||||
m_propagation_delay += 2;
|
||||
}
|
||||
}
|
||||
|
||||
void propagate_bounds_with_lp_solver() {
|
||||
if (!should_propagate())
|
||||
return;
|
||||
local_bound_propagator bp(*this);
|
||||
unsigned num_changed = lp().num_changed_bounds();
|
||||
|
||||
lp().propagate_bounds_for_touched_rows(bp);
|
||||
if (m.canceled()) {
|
||||
return;
|
||||
}
|
||||
int new_num_of_p = lp().settings().stats().m_num_of_implied_bounds;
|
||||
(void)new_num_of_p;
|
||||
CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
|
||||
unsigned props = m_stats.m_bound_propagations1;
|
||||
|
||||
if (is_infeasible()) {
|
||||
get_infeasibility_explanation_and_set_conflict();
|
||||
}
|
||||
|
|
@ -2390,28 +2406,26 @@ public:
|
|||
propagate_lp_solver_bound(bp.m_ibounds[i]);
|
||||
}
|
||||
}
|
||||
update_propagation_threshold(props < m_stats.m_bound_propagations1);
|
||||
}
|
||||
|
||||
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {
|
||||
theory_var v = lp().local_to_external(vi);
|
||||
if (v == null_theory_var)
|
||||
if (v == null_theory_var) {
|
||||
return false;
|
||||
|
||||
}
|
||||
if (m_unassigned_bounds[v] == 0 || m_bounds.size() <= static_cast<unsigned>(v)) {
|
||||
return false;
|
||||
}
|
||||
for (lp_api::bound* b : m_bounds[v]) {
|
||||
if (ctx().get_assignment(b->get_bv()) == l_undef &&
|
||||
null_literal != is_bound_implied(kind, bval, *b))
|
||||
null_literal != is_bound_implied(kind, bval, *b)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
nla::solver* get_nla_solver() {
|
||||
return m_switcher.m_nla ? m_switcher.m_nla->get() : nullptr;
|
||||
}
|
||||
|
||||
struct local_bound_propagator: public lp::lp_bound_propagator {
|
||||
imp & m_imp;
|
||||
local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {}
|
||||
|
|
@ -2476,7 +2490,7 @@ public:
|
|||
);
|
||||
DEBUG_CODE(
|
||||
for (auto& lit : m_core) {
|
||||
SASSERT(ctx().get_assignment(lit) == l_true);
|
||||
VERIFY(ctx().get_assignment(lit) == l_true);
|
||||
});
|
||||
++m_stats.m_bound_propagations1;
|
||||
assign(lit);
|
||||
|
|
|
|||
|
|
@ -1525,12 +1525,12 @@ void mpz_manager<SYNCH>::big_set(mpz & target, mpz const & source) {
|
|||
template<bool SYNCH>
|
||||
int mpz_manager<SYNCH>::big_compare(mpz const & a, mpz const & b) {
|
||||
#ifndef _MP_GMP
|
||||
sign_cell ca(*this, a), cb(*this, b);
|
||||
|
||||
if (ca.sign() > 0) {
|
||||
if (sign(a) > 0) {
|
||||
// a is positive
|
||||
if (cb.sign() > 0) {
|
||||
if (sign(b) > 0) {
|
||||
// a & b are positive
|
||||
sign_cell ca(*this, a), cb(*this, b);
|
||||
return m_mpn_manager.compare(ca.cell()->m_digits, ca.cell()->m_size,
|
||||
cb.cell()->m_digits, cb.cell()->m_size);
|
||||
}
|
||||
|
|
@ -1541,12 +1541,13 @@ int mpz_manager<SYNCH>::big_compare(mpz const & a, mpz const & b) {
|
|||
}
|
||||
else {
|
||||
// a is negative
|
||||
if (cb.sign() > 0) {
|
||||
if (sign(b) > 0) {
|
||||
// b is positive
|
||||
return -1; // a < b
|
||||
}
|
||||
else {
|
||||
// a & b are negative
|
||||
sign_cell ca(*this, a), cb(*this, b);
|
||||
return m_mpn_manager.compare(cb.cell()->m_digits, cb.cell()->m_size,
|
||||
ca.cell()->m_digits, ca.cell()->m_size);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue