mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

opt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-16 22:31:54 -07:00
parent 33f74b9c9f
commit f748a03ac7
10 changed files with 60 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/opt/maxres.cpp
View file

@ -224,35 +224,26 @@ public:
enable_sls(m_asms);
set_mus(false);
ptr_vector<expr> mcs;
while (m_lower < m_upper) {
lbool is_sat = l_true;
while (m_lower < m_upper && is_sat == l_true) {
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
vector<ptr_vector<expr> > cores;
ptr_vector<expr> mss;
model_ref mdl;
expr_ref tmp(m);
mcs.reset();
s().get_model(mdl);
update_assignment(mdl.get());
mss.append(m_asms.size(), m_asms.c_ptr());
is_sat = m_mss(cores, mss, mcs);
lbool is_sat = s().check_sat(0, 0);
if (is_sat == l_true) {
vector<ptr_vector<expr> > cores;
ptr_vector<expr> mss;
model_ref mdl;
expr_ref tmp(m);
mcs.reset();
s().get_model(mdl);
update_assignment(mdl.get());
for (unsigned i = 0; i < m_asms.size(); ++i) {
VERIFY(mdl->eval(m_asms[i].get(), tmp));
if (m.is_true(tmp)) {
mss.push_back(m_asms[i].get());
}
}
is_sat = m_mss(cores, mss, mcs);
std::cout << mcs.size() << " " << is_sat << "\n";
}
switch (is_sat) {
case l_undef:
return l_undef;
case l_false:
m_lower = m_upper;
break;
case l_true: {
return l_true;
case l_true: {
is_sat = process_sat(mcs);
if (is_sat != l_true) {
return is_sat;
@ -263,6 +254,12 @@ public:
break;
}
}
if (m_cancel) {
return l_undef;
}
if (m_lower < m_upper) {
is_sat = s().check_sat(0, 0);
}
}
m_lower = m_upper;
return l_true;

3
src/opt/maxsmt.cpp
View file

@ -179,6 +179,9 @@ namespace opt {
}
void maxsmt::verify_assignment() {
// TBD: have to use a different solver
// because we don't push local scope any longer.
return;
solver::scoped_push _sp(m_s);
commit_assignment();
if (l_true != m_s.check_sat(0,0)) {

1
src/opt/maxsmt.h
View file

@ -75,7 +75,6 @@ namespace opt {
void set_model() { s().get_model(m_model); }
virtual void updt_params(params_ref& p);
virtual void init_soft(vector<rational> const& weights, expr_ref_vector const& soft);
void add_hard(expr* e){ s().assert_expr(e); }
solver& s() { return m_s; }
void init();
expr* mk_not(expr* e);

35
src/opt/mss.cpp
View file

@ -49,7 +49,7 @@ namespace opt {
return true;
}
void mss::initialize(vector<exprs>& cores, exprs& literals) {
void mss::initialize(exprs& literals) {
expr* n;
expr_set lits, core_lits;
for (unsigned i = 0; i < literals.size(); ++i) {
@ -67,8 +67,8 @@ namespace opt {
// did not occur in previous cores and did not evaluate to true
// in the current model.
//
for (unsigned i = 0; i < cores.size(); ++i) {
exprs const& core = cores[i];
for (unsigned i = 0; i < m_cores.size(); ++i) {
exprs const& core = m_cores[i];
for (unsigned j = 0; j < core.size(); ++j) {
expr* n = core[j];
if (!core_lits.contains(n)) {
@ -97,7 +97,7 @@ namespace opt {
}
}
}
cores.push_back(rest_core);
m_cores.push_back(rest_core);
}
void mss::add_mss(expr* n) {
@ -148,23 +148,20 @@ namespace opt {
m_mss.reset();
m_todo.reset();
m_s.get_model(m_model);
m_cores.reset();
SASSERT(m_model);
vector<exprs> cores(_cores);
m_cores.append(_cores);
initialize(literals);
TRACE("opt",
for (unsigned i = 0; i < cores.size(); ++i) {
display_vec(tout << "core: ", cores[i].size(), cores[i].c_ptr());
}
display_vec(tout << "lits: ", literals.size(), literals.c_ptr());
);
initialize(cores, literals);
TRACE("opt", display(tout););
display(tout););
lbool is_sat = l_true;
for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
bool has_mcs = false;
bool is_last = i + 1 < cores.size();
bool is_last = i + 1 < m_cores.size();
SASSERT(check_invariant());
update_core(cores[i]); // remove members of mss
is_sat = process_core(1, cores[i], has_mcs, is_last);
update_core(m_cores[i]); // remove members of mss
is_sat = process_core(1, m_cores[i], has_mcs, is_last);
}
if (is_sat == l_true) {
SASSERT(check_invariant());
@ -180,6 +177,7 @@ namespace opt {
}
m_mcs.reset();
m_mss_set.reset();
IF_VERBOSE(2, display_vec(verbose_stream() << "mcs: ", mcs.size(), mcs.c_ptr()););
return is_sat;
}
@ -208,7 +206,7 @@ namespace opt {
unsigned sz_save = m_mss.size();
m_mss.append(sz, core.c_ptr());
lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
IF_VERBOSE(2, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr()););
IF_VERBOSE(3, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr()););
m_mss.resize(sz_save);
switch (is_sat) {
case l_true:
@ -253,6 +251,9 @@ namespace opt {
}
void mss::display(std::ostream& out) const {
for (unsigned i = 0; i < m_cores.size(); ++i) {
display_vec(out << "core: ", m_cores[i].size(), m_cores[i].c_ptr());
}
expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
out << "mcs:\n";
for (; it != end; ++it) {
@ -261,7 +262,7 @@ namespace opt {
out << "\n";
out << "mss:\n";
for (unsigned i = 0; i < m_mss.size(); ++i) {
out << mk_pp(m_mss[i], m) << "\n";
out << mk_pp(m_mss[i], m) << "\n";
}
out << "\n";
if (m_model) {

3
src/opt/mss.h
View file

@ -29,6 +29,7 @@ namespace opt {
exprs m_mss;
expr_set m_mcs;
expr_set m_mss_set;
vector<exprs> m_cores;
exprs m_todo;
model_ref m_model;
public:
@ -42,7 +43,7 @@ namespace opt {
void get_model(model_ref& mdl) { mdl = m_model; }
private:
void initialize(vector<exprs>& cores, exprs& literals);
void initialize(exprs& literals);
bool check_result();
void add_mss(expr* n);
void update_mss();

1
src/opt/opt_context.cpp
View file

@ -436,6 +436,7 @@ namespace opt {
}
if (m_maxsat_engine != symbol("maxres") &&
m_maxsat_engine != symbol("mus-mss-maxres") &&
m_maxsat_engine != symbol("mss-maxres") &&
m_maxsat_engine != symbol("bcd2") &&
m_maxsat_engine != symbol("sls")) {
return;

4
src/opt/wmax.cpp
View file

@ -84,15 +84,12 @@ namespace opt {
lbool operator()() {
TRACE("opt", tout << "weighted maxsat\n";);
scoped_ensure_theory wth(*this);
solver::scoped_push _s(s());
lbool is_sat = l_true;
bool was_sat = false;
for (unsigned i = 0; i < m_soft.size(); ++i) {
wth().assert_weighted(m_soft[i].get(), m_weights[i]);
}
solver::scoped_push __s(s());
while (l_true == is_sat) {
IF_VERBOSE(1, verbose_stream() << "(opt.wmax [" << m_lower << ":" << m_upper << "])\n";);
is_sat = s().check_sat(0,0);
if (m_cancel) {
is_sat = l_undef;
@ -106,6 +103,7 @@ namespace opt {
s().assert_expr(fml);
was_sat = true;
}
IF_VERBOSE(1, verbose_stream() << "(opt.wmax [" << m_lower << ":" << m_upper << "])\n";);
}
if (was_sat) {
wth().get_assignment(m_assignment);

1
src/sat/sat_solver.cpp
View file

@ -51,6 +51,7 @@ namespace sat {
m_config.updt_params(p);
m_conflicts_since_gc = 0;
m_next_simplify = 0;
m_num_checkpoints = 0;
}
solver::~solver() {

14
src/sat/sat_solver.h
View file

@ -82,8 +82,8 @@ namespace sat {
scc m_scc;
asymm_branch m_asymm_branch;
probing m_probing;
mus m_mus;
wsls m_wsls;
mus m_mus; // MUS for minimal core extraction
wsls m_wsls; // SLS facility for MaxSAT use
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
@ -123,9 +123,9 @@ namespace sat {
stopwatch m_stopwatch;
params_ref m_params;
scoped_ptr<solver> m_clone; // for debugging purposes
literal_vector m_assumptions;
literal_set m_assumption_set;
literal_vector m_core;
literal_vector m_assumptions; // additional assumptions during check
literal_set m_assumption_set; // set of enabled assumptions
literal_vector m_core; // unsat core
void del_clauses(clause * const * begin, clause * const * end);
@ -230,6 +230,9 @@ namespace sat {
clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
void checkpoint() {
if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
++m_num_checkpoints;
if (m_num_checkpoints < 10) return;
m_num_checkpoints = 0;
if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
}
typedef std::pair<literal, literal> bin_clause;
@ -275,6 +278,7 @@ namespace sat {
unsigned m_luby_idx;
unsigned m_conflicts_since_gc;
unsigned m_gc_threshold;
unsigned m_num_checkpoints;
double m_min_d_tk;
unsigned m_next_simplify;
bool decide();

8
src/tactic/bv/bit_blaster_tactic.cpp
View file

@ -69,6 +69,7 @@ class bit_blaster_tactic : public tactic {
expr_ref new_curr(m());
proof_ref new_pr(m());
unsigned size = g->size();
bool change = false;
for (unsigned idx = 0; idx < size; idx++) {
if (g->inconsistent())
break;
@ -79,10 +80,13 @@ class bit_blaster_tactic : public tactic {
proof * pr = g->pr(idx);
new_pr = m().mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
if (curr != new_curr) {
change = true;
g->update(idx, new_curr, new_pr, g->dep(idx));
}
}
if (g->models_enabled())
if (change && g->models_enabled())
mc = mk_bit_blaster_model_converter(m(), m_rewriter.const2bits());
else
mc = 0;