mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
perf improvements, mus
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
6438c477b3
commit
b928734348
7 changed files with 242 additions and 21 deletions
|
|
@ -43,7 +43,6 @@ class inc_sat_solver : public solver {
|
|||
model_ref m_model;
|
||||
model_converter_ref m_mc;
|
||||
tactic_ref m_preprocess;
|
||||
statistics m_stats;
|
||||
unsigned m_num_scopes;
|
||||
sat::literal_vector m_asms;
|
||||
goal_ref_buffer m_subgoals;
|
||||
|
|
@ -89,7 +88,8 @@ public:
|
|||
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
|
||||
m_solver.pop_to_base_level();
|
||||
dep2asm_t dep2asm;
|
||||
|
||||
|
||||
m_model.reset();
|
||||
lbool r = internalize_formulas();
|
||||
if (r != l_true) return r;
|
||||
r = internalize_assumptions(num_assumptions, assumptions, dep2asm);
|
||||
|
|
@ -98,7 +98,6 @@ public:
|
|||
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
|
||||
switch (r) {
|
||||
case l_true:
|
||||
extract_model();
|
||||
break;
|
||||
case l_false:
|
||||
// TBD: expr_dependency core is not accounted for.
|
||||
|
|
@ -109,7 +108,6 @@ public:
|
|||
default:
|
||||
break;
|
||||
}
|
||||
m_solver.collect_statistics(m_stats);
|
||||
return r;
|
||||
}
|
||||
virtual void set_cancel(bool f) {
|
||||
|
|
@ -155,13 +153,17 @@ public:
|
|||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
st.copy(m_stats);
|
||||
m_preprocess->collect_statistics(st);
|
||||
m_solver.collect_statistics(st);
|
||||
}
|
||||
virtual void get_unsat_core(ptr_vector<expr> & r) {
|
||||
r.reset();
|
||||
r.append(m_core.size(), m_core.c_ptr());
|
||||
}
|
||||
virtual void get_model(model_ref & m) {
|
||||
if (!m_model) {
|
||||
extract_model();
|
||||
}
|
||||
m = m_model;
|
||||
}
|
||||
virtual proof * get_proof() {
|
||||
|
|
@ -190,7 +192,6 @@ private:
|
|||
}
|
||||
catch (tactic_exception & ex) {
|
||||
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
|
||||
m_preprocess->collect_statistics(m_stats);
|
||||
return l_undef;
|
||||
}
|
||||
m_mc = concat(m_mc.get(), m_mc2.get());
|
||||
|
|
@ -270,6 +271,9 @@ private:
|
|||
|
||||
}
|
||||
|
||||
// TBD: this is super-expensive because of the
|
||||
// bit-blasting model converter.
|
||||
|
||||
void extract_model() {
|
||||
model_ref md = alloc(model, m);
|
||||
sat::model const & ll_m = m_solver.get_model();
|
||||
|
|
|
|||
|
|
@ -123,7 +123,7 @@ struct mus::imp {
|
|||
TRACE("opt",
|
||||
display_vec(tout << "core: ", core);
|
||||
display_vec(tout << "mus: ", mus);
|
||||
display_vec(tout << "model: ", model);
|
||||
// display_vec(tout << "model: ", model);
|
||||
);
|
||||
core.pop_back();
|
||||
expr* cls = m_cls2expr[cls_id].get();
|
||||
|
|
@ -140,8 +140,8 @@ struct mus::imp {
|
|||
case l_true:
|
||||
assumptions.push_back(cls);
|
||||
mus.push_back(cls_id);
|
||||
extract_model(model);
|
||||
if (m_rmr_enabled) {
|
||||
extract_model(model);
|
||||
sz = core.size();
|
||||
core.append(mus);
|
||||
rmr(core, mus, model);
|
||||
|
|
|
|||
163
src/sat/sat_mus.cpp
Normal file
163
src/sat/sat_mus.cpp
Normal file
|
|
@ -0,0 +1,163 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_mus.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4)
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2014-20-7
|
||||
|
||||
Notes:
|
||||
|
||||
Model rotation needs fixes to ensure that hard constraints are satisfied
|
||||
under pertubed model. Model rotation also has o be consistent with theories.
|
||||
|
||||
--*/
|
||||
|
||||
#include "sat_solver.h"
|
||||
#include "sat_mus.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
mus::mus(solver& s):s(s) {}
|
||||
|
||||
mus::~mus() {}
|
||||
|
||||
void mus::reset() {
|
||||
m_core.reset();
|
||||
m_mus.reset();
|
||||
m_assumptions.reset();
|
||||
}
|
||||
|
||||
void mus::set_core() {
|
||||
m_core.append(m_mus);
|
||||
s.m_core.reset();
|
||||
s.m_core.append(m_core);
|
||||
}
|
||||
|
||||
lbool mus::operator()() {
|
||||
reset();
|
||||
literal_vector& core = m_core;
|
||||
literal_vector& mus = m_mus;
|
||||
literal_vector& assumptions = m_assumptions;
|
||||
core.append(s.get_core());
|
||||
SASSERT(!core.empty());
|
||||
|
||||
if (core.size() == 1) {
|
||||
return l_true;
|
||||
}
|
||||
while (!core.empty()) {
|
||||
TRACE("sat",
|
||||
tout << "core: " << core << "\n";
|
||||
tout << "mus: " << mus << "\n";);
|
||||
|
||||
if (s.m_cancel) {
|
||||
set_core();
|
||||
return l_undef;
|
||||
}
|
||||
literal lit = core.back();
|
||||
core.pop_back();
|
||||
unsigned sz = assumptions.size();
|
||||
assumptions.push_back(~lit);
|
||||
assumptions.append(core);
|
||||
lbool is_sat = s.check(assumptions.size(), assumptions.c_ptr());
|
||||
assumptions.resize(sz);
|
||||
switch (is_sat) {
|
||||
case l_undef:
|
||||
core.push_back(lit);
|
||||
set_core();
|
||||
return l_undef;
|
||||
case l_true: {
|
||||
assumptions.push_back(lit);
|
||||
mus.push_back(lit);
|
||||
unsigned sz = core.size();
|
||||
core.append(mus);
|
||||
rmr();
|
||||
core.resize(sz);
|
||||
break;
|
||||
}
|
||||
case l_false:
|
||||
core.reset();
|
||||
for (unsigned i = 0; i < s.get_core().size(); ++i) {
|
||||
literal lit = s.get_core()[i];
|
||||
if (!mus.contains(lit)) {
|
||||
core.push_back(lit);
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
return l_true;
|
||||
}
|
||||
|
||||
lbool mus::eval(literal l) const {
|
||||
return value_at(l, s.get_model());
|
||||
}
|
||||
|
||||
void mus::rmr() {
|
||||
model& model = s.m_model;
|
||||
literal lit = m_mus.back();
|
||||
literal assumption_lit;
|
||||
SASSERT(eval(lit) == l_false); // literal is false in current model.
|
||||
find_swappable(lit);
|
||||
for (unsigned i = 0; i < m_toswap.size(); ++i) {
|
||||
lit = m_toswap[i];
|
||||
SASSERT(eval(lit) == l_false);
|
||||
model[lit.var()] = ~model[lit.var()]; // swap assignment
|
||||
if (has_single_unsat(assumption_lit) && !m_mus.contains(assumption_lit)) {
|
||||
m_mus.push_back(assumption_lit);
|
||||
rmr();
|
||||
}
|
||||
model[lit.var()] = ~model[lit.var()]; // swap assignment back
|
||||
}
|
||||
}
|
||||
|
||||
bool mus::has_single_unsat(literal& assumption_lit) {
|
||||
model const& model = s.get_model();
|
||||
return false;
|
||||
}
|
||||
|
||||
void mus::find_swappable(literal lit) {
|
||||
m_toswap.reset();
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
||||
|
||||
bool has_single_unsat(svector<bool> const& model, unsigned& cls_id) const {
|
||||
cls_id = UINT_MAX;
|
||||
for (unsigned i = 0; i < m_cls2lits.size(); ++i) {
|
||||
if (!eval(model, m_cls2lits[i])) {
|
||||
if (cls_id == UINT_MAX) {
|
||||
cls_id = i;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "clause: " << cls_id << " model: ", model););
|
||||
return cls_id != UINT_MAX;
|
||||
}
|
||||
|
||||
bool eval(svector<bool> const& model, smt::literal_vector const& cls) const {
|
||||
bool result = false;
|
||||
for (unsigned i = 0; !result && i < cls.size(); ++i) {
|
||||
result = (model[cls[i].var()] != cls[i].sign());
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "model: ", model);
|
||||
display_vec(tout << "clause: ", cls);
|
||||
tout << "result: " << result << "\n";);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
#endif
|
||||
44
src/sat/sat_mus.h
Normal file
44
src/sat/sat_mus.h
Normal file
|
|
@ -0,0 +1,44 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
mus.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4)
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2014-20-7
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _SAT_MUS_H_
|
||||
#define _SAT_MUS_H_
|
||||
|
||||
namespace sat {
|
||||
class mus {
|
||||
literal_vector m_core;
|
||||
literal_vector m_assumptions;
|
||||
literal_vector m_mus;
|
||||
literal_vector m_toswap;
|
||||
solver& s;
|
||||
public:
|
||||
mus(solver& s);
|
||||
~mus();
|
||||
lbool operator()();
|
||||
private:
|
||||
void rmr();
|
||||
bool has_single_unsat(literal& assumption_lit);
|
||||
void find_swappable(literal lit);
|
||||
void reset();
|
||||
void set_core();
|
||||
lbool eval(literal l) const;
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
@ -18,4 +18,5 @@ def_module_params('sat',
|
|||
('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
|
||||
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
|
||||
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
|
||||
('minimize_core', BOOL, False, 'minimize computed core'),
|
||||
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))
|
||||
|
|
|
|||
|
|
@ -39,13 +39,15 @@ namespace sat {
|
|||
m_scc(*this, p),
|
||||
m_asymm_branch(*this, p),
|
||||
m_probing(*this, p),
|
||||
m_mus(*this),
|
||||
m_inconsistent(false),
|
||||
m_num_frozen(0),
|
||||
m_activity_inc(128),
|
||||
m_case_split_queue(m_activity),
|
||||
m_qhead(0),
|
||||
m_scope_lvl(0),
|
||||
m_params(p) {
|
||||
m_params(p),
|
||||
m_minimize_core(p.get_bool("minimize_core", false)) {
|
||||
m_config.updt_params(p);
|
||||
}
|
||||
|
||||
|
|
@ -710,7 +712,6 @@ namespace sat {
|
|||
init_assumptions(num_lits, lits);
|
||||
propagate(false);
|
||||
if (inconsistent()) {
|
||||
TRACE("sat", tout << "initialized -> inconsistent\n";);
|
||||
if (tracking_assumptions())
|
||||
resolve_conflict();
|
||||
return l_false;
|
||||
|
|
@ -721,8 +722,7 @@ namespace sat {
|
|||
lbool r = bounded_search();
|
||||
if (r != l_undef)
|
||||
return r;
|
||||
pop(scope_lvl());
|
||||
SASSERT(scope_lvl() == 1);
|
||||
pop_reinit(scope_lvl());
|
||||
m_conflicts_since_restart = 0;
|
||||
m_restart_threshold = m_config.m_restart_initial;
|
||||
}
|
||||
|
|
@ -900,10 +900,10 @@ namespace sat {
|
|||
|
||||
void solver::reinit_assumptions() {
|
||||
if (tracking_assumptions() && scope_lvl() == 0) {
|
||||
TRACE("sat", tout << m_assumptions.size() << "\n";);
|
||||
push();
|
||||
for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) {
|
||||
literal l = m_assumptions[i];
|
||||
assign(l, justification());
|
||||
assign(m_assumptions[i], justification());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -937,7 +937,8 @@ namespace sat {
|
|||
\brief Apply all simplifications.
|
||||
*/
|
||||
void solver::simplify_problem() {
|
||||
pop_core(scope_lvl());
|
||||
pop(scope_lvl());
|
||||
m_trail.reset();
|
||||
|
||||
SASSERT(scope_lvl() == 0);
|
||||
|
||||
|
|
@ -1055,7 +1056,7 @@ namespace sat {
|
|||
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
|
||||
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
|
||||
IF_VERBOSE(30, display_status(verbose_stream()););
|
||||
pop(scope_lvl());
|
||||
pop_reinit(scope_lvl());
|
||||
m_conflicts_since_restart = 0;
|
||||
switch (m_config.m_restart) {
|
||||
case RS_GEOMETRIC:
|
||||
|
|
@ -1508,7 +1509,7 @@ namespace sat {
|
|||
|
||||
unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr());
|
||||
|
||||
pop(m_scope_lvl - new_scope_lvl);
|
||||
pop_reinit(m_scope_lvl - new_scope_lvl);
|
||||
TRACE("sat_conflict_detail", display(tout); tout << "assignment:\n"; display_assignment(tout););
|
||||
clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
|
||||
if (lemma) {
|
||||
|
|
@ -1620,6 +1621,9 @@ namespace sat {
|
|||
}
|
||||
while (idx > 0);
|
||||
reset_unmark(old_size);
|
||||
if (m_minimize_core) {
|
||||
m_mus(); //ignore return value on cancelation.
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -2082,12 +2086,12 @@ namespace sat {
|
|||
m_ext->push();
|
||||
}
|
||||
|
||||
void solver::pop(unsigned num_scopes) {
|
||||
pop_core(num_scopes);
|
||||
void solver::pop_reinit(unsigned num_scopes) {
|
||||
pop(num_scopes);
|
||||
reinit_assumptions();
|
||||
}
|
||||
|
||||
void solver::pop_core(unsigned num_scopes) {
|
||||
void solver::pop(unsigned num_scopes) {
|
||||
if (num_scopes == 0)
|
||||
return;
|
||||
if (m_ext)
|
||||
|
|
@ -2232,6 +2236,7 @@ namespace sat {
|
|||
m_probing.updt_params(p);
|
||||
m_scc.updt_params(p);
|
||||
m_rand.set_seed(p.get_uint("random_seed", 0));
|
||||
m_minimize_core = p.get_bool("minimize_core", false);
|
||||
}
|
||||
|
||||
void solver::collect_param_descrs(param_descrs & d) {
|
||||
|
|
|
|||
|
|
@ -32,6 +32,7 @@ Revision History:
|
|||
#include"sat_asymm_branch.h"
|
||||
#include"sat_iff3_finder.h"
|
||||
#include"sat_probing.h"
|
||||
#include"sat_mus.h"
|
||||
#include"params.h"
|
||||
#include"statistics.h"
|
||||
#include"stopwatch.h"
|
||||
|
|
@ -79,6 +80,7 @@ namespace sat {
|
|||
scc m_scc;
|
||||
asymm_branch m_asymm_branch;
|
||||
probing m_probing;
|
||||
mus m_mus;
|
||||
bool m_inconsistent;
|
||||
// A conflict is usually a single justification. That is, a justification
|
||||
// for false. If m_not_l is not null_literal, then m_conflict is a
|
||||
|
|
@ -121,6 +123,7 @@ namespace sat {
|
|||
literal_vector m_assumptions;
|
||||
literal_set m_assumption_set;
|
||||
literal_vector m_core;
|
||||
bool m_minimize_core;
|
||||
|
||||
void del_clauses(clause * const * begin, clause * const * end);
|
||||
|
||||
|
|
@ -132,6 +135,7 @@ namespace sat {
|
|||
friend class asymm_branch;
|
||||
friend class probing;
|
||||
friend class iff3_finder;
|
||||
friend class mus;
|
||||
friend struct mk_stat;
|
||||
public:
|
||||
solver(params_ref const & p, extension * ext);
|
||||
|
|
@ -352,7 +356,7 @@ namespace sat {
|
|||
// -----------------------
|
||||
void push();
|
||||
void pop(unsigned num_scopes);
|
||||
void pop_core(unsigned num_scopes);
|
||||
void pop_reinit(unsigned num_scopes);
|
||||
|
||||
void unassign_vars(unsigned old_sz);
|
||||
void reinit_clauses(unsigned old_sz);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue