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

fix bug in blocked clause elimination that was enabled for external variables, fix other bugs in maxres

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-10 21:23:05 -07:00
parent 317e76a11b
commit e832bdd257
9 changed files with 233 additions and 107 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/opt/inc_sat_solver.cpp
View file

@ -93,11 +93,12 @@ public:
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(num_assumptions, assumptions, dep2asm);
extract_assumptions(dep2asm, m_asms);
if (r != l_true) return r;
extract_assumptions(dep2asm, m_asms);
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
switch (r) {
case l_true:
check_assumptions(dep2asm);
break;
case l_false:
// TBD: expr_dependency core is not accounted for.
@ -271,6 +272,23 @@ private:
}
void check_assumptions(dep2asm_t& dep2asm) {
sat::model const & ll_m = m_solver.get_model();
dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
sat::literal lit = it->m_value;
lbool polarity = lit.sign()?l_false:l_true;
lbool value = sat::value_at(lit.var(), ll_m);
if (value != polarity) {
std::cout << mk_pp(it->m_key, m) << " evaluates to " << value << "\n";
std::cout << m_asms << "\n";
m_solver.display_assignment(std::cout);
// m_solver.display(std::cout);
throw default_exception("bad state");
}
}
}
// TBD: this is super-expensive because of the
// bit-blasting model converter.
@ -286,6 +304,7 @@ private:
continue;
}
sat::bool_var v = it->m_value;
// std::cout << mk_pp(n, m) << " -> " << sat::value_at(v, ll_m) << "\n";
switch (sat::value_at(v, ll_m)) {
case l_true:
md->register_decl(to_app(n)->get_decl(), m.mk_true());

103
src/opt/maxres.cpp
View file

@ -59,6 +59,8 @@ Notes:
#include "ast_pp.h"
#include "mus.h"
#include "mss.h"
#include "inc_sat_solver.h"
using namespace opt;
@ -117,7 +119,7 @@ public:
else {
asum = mk_fresh_bool("soft");
fml = m.mk_iff(asum, e);
m_s->assert_expr(fml);
s().assert_expr(fml);
}
new_assumption(asum, w);
m_upper += w;
@ -138,17 +140,17 @@ public:
while (true) {
TRACE("opt",
display_vec(tout, m_asms.size(), m_asms.c_ptr());
m_s->display(tout);
s().display(tout);
tout << "\n";
display(tout);
);
lbool is_sat = m_s->check_sat(m_asms.size(), m_asms.c_ptr());
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
if (m_cancel) {
return l_undef;
}
switch (is_sat) {
case l_true: {
m_s->get_model(m_model);
s().get_model(m_model);
expr_ref tmp(m);
DEBUG_CODE(
for (unsigned i = 0; i < m_asms.size(); ++i) {
@ -157,6 +159,7 @@ public:
});
for (unsigned i = 0; i < m_soft.size(); ++i) {
VERIFY(m_model->eval(m_soft[i].get(), tmp));
std::cout << mk_pp(m_soft[i].get(), m) << " -> " << tmp << "\n";
m_assignment[i] = m.is_true(tmp);
}
m_upper = m_lower;
@ -186,7 +189,7 @@ public:
while (m_lower < m_upper) {
TRACE("opt",
display_vec(tout, m_asms.size(), m_asms.c_ptr());
m_s->display(tout);
s().display(tout);
tout << "\n";
display(tout);
);
@ -203,11 +206,10 @@ public:
return l_true;
case l_true:
SASSERT(cores.empty() || mcs.empty());
SASSERT(!cores.empty() || !mcs.empty());
for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
is_sat = process_unsat(cores[i]);
}
if (is_sat == l_true && !mcs.empty()) {
if (is_sat == l_true && cores.empty()) {
is_sat = process_sat(mcs);
}
if (is_sat != l_true) {
@ -216,7 +218,7 @@ public:
break;
}
}
m_lower = m_lower;
m_lower = m_upper;
return l_true;
}
@ -247,7 +249,7 @@ public:
ptr_vector<expr> core;
while (is_sat == l_false) {
core.reset();
m_s->get_unsat_core(core);
s().get_unsat_core(core);
is_sat = minimize_core(core);
if (is_sat != l_true) {
break;
@ -261,7 +263,7 @@ public:
TRACE("opt",
display_vec(tout << "core: ", core.size(), core.c_ptr());
display_vec(tout << "assumptions: ", asms.size(), asms.c_ptr()););
is_sat = m_s->check_sat(asms.size(), asms.c_ptr());
is_sat = s().check_sat(asms.size(), asms.c_ptr());
}
TRACE("opt",
tout << "num cores: " << cores.size() << "\n";
@ -280,9 +282,8 @@ public:
lbool process_sat(ptr_vector<expr>& corr_set) {
expr_ref fml(m), tmp(m);
TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
SASSERT(!corr_set.empty()); // we should somehow stop if all soft are satisfied.
if (corr_set.empty()) {
return l_false;
return l_true;
}
remove_core(corr_set);
@ -314,7 +315,7 @@ public:
TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
max_resolve(core, w);
fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
m_s->assert_expr(fml);
s().assert_expr(fml);
m_lower += w;
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
return l_true;
@ -407,9 +408,9 @@ public:
if (i > 2) {
dd = mk_fresh_bool("d");
fml = m.mk_implies(dd, d);
m_s->assert_expr(fml);
s().assert_expr(fml);
fml = m.mk_implies(dd, b_i);
m_s->assert_expr(fml);
s().assert_expr(fml);
d = dd;
}
else {
@ -419,7 +420,7 @@ public:
cls = m.mk_or(b_i1, d);
fml = m.mk_implies(asum, cls);
new_assumption(asum, w);
m_s->assert_expr(fml);
s().assert_expr(fml);
}
}
@ -449,20 +450,20 @@ public:
if (i > 2) {
d = mk_fresh_bool("d");
fml = m.mk_implies(d, cls);
m_s->assert_expr(fml);
s().assert_expr(fml);
}
else {
d = cls;
}
asum = mk_fresh_bool("a");
fml = m.mk_implies(asum, b_i1);
m_s->assert_expr(fml);
s().assert_expr(fml);
fml = m.mk_implies(asum, cls);
m_s->assert_expr(fml);
s().assert_expr(fml);
new_assumption(asum, w);
}
fml = m.mk_or(m_B.size(), m_B.c_ptr());
m_s->assert_expr(fml);
s().assert_expr(fml);
}
lbool try_improve_bound(vector<ptr_vector<expr> >& cores, ptr_vector<expr>& mcs) {
@ -473,25 +474,29 @@ public:
while (true) {
rational upper = m_max_upper;
unsigned sz = 0;
for (unsigned i = 0; m_upper <= upper && i < asms.size(); ++i, ++sz) {
for (unsigned i = 0; m_upper <= rational(2)*upper && i < asms.size(); ++i, ++sz) {
upper -= get_weight(asms[i].get());
}
lbool is_sat = m_s->check_sat(sz, asms.c_ptr());
lbool is_sat = s().check_sat(sz, asms.c_ptr());
switch (is_sat) {
case l_true: {
ptr_vector<expr> lits;
lits.append(asms.size(), asms.c_ptr());
s().get_model(m_model); // last model is best way to reduce search space.
update_assignment();
ptr_vector<expr> mss;
mss.append(asms.size(), asms.c_ptr());
set_mus(false);
is_sat = m_mss(cores, lits);
is_sat = m_mss(cores, mss, mcs);
set_mus(true);
if (is_sat != l_true) {
return is_sat;
}
m_mss.get_model(m_model); // last model is best way to reduce search space.
update_assignment();
if (cores.empty() || asms.size() < cores.back().size()) {
if (!cores.empty() && mcs.size() > cores.back().size()) {
mcs.reset();
}
else {
cores.reset();
mcs.append(asms.size(), asms.c_ptr());
}
return l_true;
}
@ -499,7 +504,7 @@ public:
return l_undef;
case l_false:
core.reset();
m_s->get_unsat_core(core);
s().get_unsat_core(core);
is_sat = minimize_core(core);
if (is_sat != l_true) {
break;
@ -531,23 +536,29 @@ public:
void update_assignment() {
rational upper(0);
expr_ref tmp(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref tmp(m);
expr* n = m_soft[i].get();
VERIFY(m_model->eval(n, tmp));
CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp),
tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
m_assignment[i] = m.is_true(tmp);
if (!m_assignment[i]) {
if (!m.is_true(tmp)) {
upper += m_weights[i];
}
CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp),
tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
}
if (upper >= m_upper) {
return;
}
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr* n = m_soft[i].get();
VERIFY(m_model->eval(n, tmp));
m_assignment[i] = m.is_true(tmp);
}
SASSERT(upper <= m_upper);
m_upper = upper;
// verify_assignment();
IF_VERBOSE(1, verbose_stream() <<
"(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
}
void remove_soft(ptr_vector<expr> const& core, expr_ref_vector& asms) {
@ -579,6 +590,26 @@ public:
m_max_upper = m_upper;
}
void verify_assignment() {
IF_VERBOSE(0, verbose_stream() << "verify assignment\n";);
ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);
for (unsigned i = 0; i < m_assertions.size(); ++i) {
sat_solver->assert_expr(m_assertions[i].get());
}
expr_ref n(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
n = m_soft[i].get();
if (!m_assignment[i]) {
n = m.mk_not(n);
}
sat_solver->assert_expr(n);
}
lbool is_sat = sat_solver->check_sat(0, 0);
if (is_sat == l_false) {
IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";);
}
}
};
opt::maxsmt_solver_base* opt::mk_maxres(ast_manager& m, opt_solver* s, params_ref& p,

21
src/opt/maxsmt.cpp
View file

@ -134,6 +134,7 @@ namespace opt {
unsigned sz = s().get_num_assertions();
for (unsigned i = 0; i < sz; ++i) {
sat_solver->assert_expr(s().get_assertion(i));
m_assertions.push_back(s().get_assertion(i));
}
m_s = sat_solver;
}
@ -232,16 +233,24 @@ namespace opt {
});
DEBUG_CODE(if (is_sat == l_true) {
m_s->push();
commit_assignment();
VERIFY(l_true == m_s->check_sat(0,0));
m_s->pop(1);
// TBD: check that all extensions are unsat too
verify_assignment();
});
});
// TBD: check that all extensions are unsat too
return is_sat;
}
void maxsmt::verify_assignment() {
m_s->push();
commit_assignment();
if (l_true != m_s->check_sat(0,0)) {
IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";);
UNREACHABLE();
}
m_s->pop(1);
}
bool maxsmt::get_assignment(unsigned idx) const {
if (m_msolver) {
return m_msolver->get_assignment(idx);

4
src/opt/maxsmt.h
View file

@ -48,6 +48,7 @@ namespace opt {
ast_manager& m;
volatile bool m_cancel;
expr_ref_vector m_soft;
expr_ref_vector m_assertions;
vector<rational> m_weights;
rational m_lower;
rational m_upper;
@ -65,6 +66,7 @@ namespace opt {
maxsmt_solver_base(opt_solver* s, ast_manager& m, params_ref& p,
vector<rational> const& ws, expr_ref_vector const& soft):
m_s(s), m(m), m_cancel(false), m_soft(m),
m_assertions(m),
m_enable_sls(false), m_enable_sat(false),
m_sls_enabled(false), m_sat_enabled(false) {
m_s->get_model(m_model);
@ -148,6 +150,8 @@ namespace opt {
private:
bool is_maxsat_problem(vector<rational> const& ws) const;
void verify_assignment();
};

11
src/opt/mss.cpp
View file

@ -144,7 +144,7 @@ namespace opt {
m_todo.resize(j);
}
lbool mss::operator()(vector<exprs> const& _cores, exprs& literals) {
lbool mss::operator()(vector<exprs> const& _cores, exprs& literals, exprs& mcs) {
m_mss.reset();
m_todo.reset();
m_s->get_model(m_model);
@ -171,6 +171,11 @@ namespace opt {
TRACE("opt", display(tout););
literals.reset();
literals.append(m_mss);
mcs.reset();
expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
for (; it != end; ++it) {
mcs.push_back(*it);
}
SASSERT(check_result());
}
m_mcs.reset();
@ -203,12 +208,12 @@ 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(1, display_vec(verbose_stream(), sz, core.c_ptr()););
m_mss.resize(sz_save);
switch (is_sat) {
case l_true:
m_s->get_model(m_model);
update_mss();
// sz entries from core should now be in mss.
update_mss();
DEBUG_CODE(
for (unsigned i = 0; i < sz; ++i) {
SASSERT(m_mss_set.contains(core[i]));

2
src/opt/mss.h
View file

@ -35,7 +35,7 @@ namespace opt {
mss(ref<solver>& s, ast_manager& m);
~mss();
lbool operator()(vector<exprs> const& cores, exprs& literals);
lbool operator()(vector<exprs> const& cores, exprs& literals, exprs& mcs);
void set_cancel(bool f) { m_cancel = f; }

3
src/sat/sat_simplifier.cpp
View file

@ -917,6 +917,9 @@ namespace sat {
void process(literal l) {
TRACE("blocked_clause", tout << "processing: " << l << "\n";);
if (s.is_external(l.var()) || s.was_eliminated(l.var())) {
return;
}
model_converter::entry * new_entry = 0;
{
m_to_remove.reset();

171
src/sat/sat_solver.cpp
View file

@ -880,7 +880,9 @@ namespace sat {
TRACE("sat",
for (unsigned i = 0; i < num_lits; ++i)
tout << lits[i] << " ";
tout << "\n";);
tout << "\n";
m_mc.display(tout);
);
#define _INSERT_LIT(_l_) \
SASSERT(is_external((_l_).var())); \
m_assumption_set.insert(_l_); \
@ -950,7 +952,7 @@ namespace sat {
m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
if (!m_learned.empty()) {
m_simplifier(true);
CASSERT("sat_missed_prop", check_missed_propagation());
@ -1000,6 +1002,7 @@ namespace sat {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model\"\n";);
if (!check_model(m_model))
throw solver_exception("check model failed");
if (m_clone) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
if (!m_clone->check_model(m_model))
@ -1018,7 +1021,12 @@ namespace sat {
for (; it != end; ++it) {
clause const & c = *(*it);
if (!c.satisfied_by(m)) {
TRACE("sat_model_bug", tout << "failed: " << c << "\n";);
TRACE("sat", tout << "failed: " << c << "\n";
tout << "assumptions: " << m_assumptions << "\n";
tout << "trail: " << m_trail << "\n";
tout << "model: " << m << "\n";
m_mc.display(tout);
);
ok = false;
}
}
@ -1036,15 +1044,28 @@ namespace sat {
continue;
literal l2 = it2->get_literal();
if (value_at(l2, m) != l_true) {
TRACE("sat_model_bug", tout << "failed binary: " << l << " " << l2 << " learned: " << it2->is_learned() << "\n";);
TRACE("sat", tout << "failed binary: " << l << " " << l2 << " learned: " << it2->is_learned() << "\n";
m_mc.display(tout););
ok = false;
}
}
}
}
if (!m_mc.check_model(m))
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
if (value_at(m_assumptions[i], m) != l_true) {
TRACE("sat",
tout << m_assumptions[i] << " does not model check\n";
tout << "trail: " << m_trail << "\n";
tout << "model: " << m << "\n";
m_mc.display(tout);
);
ok = false;
}
}
if (ok && !m_mc.check_model(m)) {
ok = false;
TRACE("sat", tout << "check: " << ok << "\n" << m << "\n";);
TRACE("sat", tout << "model: " << m << "\n"; m_mc.display(tout););
}
return ok;
}
@ -1532,73 +1553,99 @@ namespace sat {
}
}
void solver::resolve_conflict_for_unsat_core() {
TRACE("sat", display(tout););
void solver::process_consequent_for_unsat_core(literal consequent, justification const& js) {
TRACE("sat", tout << "processing consequent: " << consequent << "\n";
display_justification(tout << "js kind: ", js);
tout << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
process_antecedent_for_unsat_core(~(js.get_literal()));
break;
case justification::TERNARY:
process_antecedent_for_unsat_core(~(js.get_literal1()));
process_antecedent_for_unsat_core(~(js.get_literal2()));
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
unsigned i = 0;
if (consequent != null_literal) {
SASSERT(c[0] == consequent || c[1] == consequent);
if (c[0] == consequent) {
i = 1;
}
else {
process_antecedent_for_unsat_core(~c[0]);
i = 2;
}
}
unsigned sz = c.size();
for (; i < sz; i++)
process_antecedent_for_unsat_core(~c[i]);
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(consequent, js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it)
process_antecedent_for_unsat_core(*it);
break;
}
default:
UNREACHABLE();
break;
}
}
void solver::resolve_conflict_for_unsat_core() {
TRACE("sat", display(tout);
unsigned level = 0;
for (unsigned i = 0; i < m_trail.size(); ++i) {
literal l = m_trail[i];
if (level != m_level[l.var()]) {
level = m_level[l.var()];
tout << level << ": ";
}
tout << l;
if (m_mark[l.var()]) {
tout << "*";
}
tout << " ";
}
tout << "\n";
);
m_core.reset();
if (m_conflict_lvl == 0) {
return;
}
unsigned old_size = m_unmark.size();
m_core.reset();
int idx = skip_literals_above_conflict_level();
if (m_not_l != null_literal) {
TRACE("sat", tout << "not_l: " << m_not_l << "\n";);
justification js = m_justification[m_not_l.var()];
TRACE("sat", tout << "not_l: " << m_not_l << "\n";
display_justification(tout, js);
tout << "\n";);
process_antecedent_for_unsat_core(m_not_l);
if (is_assumption(~m_not_l)) {
m_core.push_back(~m_not_l);
}
else {
process_consequent_for_unsat_core(m_not_l, js);
}
}
literal consequent = m_not_l;
justification js = m_conflict;
do {
TRACE("sat", tout << "processing consequent: " << consequent << "\n";
tout << "js kind: " << js << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
process_antecedent_for_unsat_core(~(js.get_literal()));
break;
case justification::TERNARY:
process_antecedent_for_unsat_core(~(js.get_literal1()));
process_antecedent_for_unsat_core(~(js.get_literal2()));
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
unsigned i = 0;
if (consequent != null_literal) {
SASSERT(c[0] == consequent || c[1] == consequent);
if (c[0] == consequent) {
i = 1;
}
else {
process_antecedent_for_unsat_core(~c[0]);
i = 2;
}
}
unsigned sz = c.size();
for (; i < sz; i++)
process_antecedent_for_unsat_core(~c[i]);
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(consequent, js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it)
process_antecedent_for_unsat_core(*it);
break;
}
default:
UNREACHABLE();
break;
}
while (true) {
process_consequent_for_unsat_core(consequent, js);
idx--;
while (idx >= 0) {
literal l = m_trail[idx];
if (is_marked(l.var()))
@ -1611,17 +1658,16 @@ namespace sat {
}
consequent = m_trail[idx];
if (lvl(consequent) < m_conflict_lvl) {
TRACE("sat", tout << consequent << " at level " << lvl(consequent) << "\n";);
break;
}
bool_var c_var = consequent.var();
SASSERT(lvl(consequent) == m_conflict_lvl);
js = m_justification[c_var];
idx--;
}
while (idx > 0);
reset_unmark(old_size);
if (m_config.m_minimize_core) {
m_mus(); //ignore return value on cancelation.
m_mus(); // ignore return value on cancelation.
}
}
@ -2362,6 +2408,13 @@ namespace sat {
out << ")\n";
}
void solver::display_justification(std::ostream & out, justification const& js) const {
out << js;
if (js.is_clause()) {
out << *(m_cls_allocator.get_clause(js.get_clause_offset()));
}
}
unsigned solver::num_clauses() const {
unsigned num_cls = 0;
num_cls += m_trail.size(); // units;

4
src/sat/sat_solver.h
View file

@ -328,6 +328,7 @@ namespace sat {
unsigned get_max_lvl(literal consequent, justification js);
void process_antecedent(literal antecedent, unsigned & num_marks);
void process_antecedent_for_unsat_core(literal antecedent);
void process_consequent_for_unsat_core(literal consequent, justification const& js);
void fill_ext_antecedents(literal consequent, justification js);
unsigned skip_literals_above_conflict_level();
void forget_phase_of_vars(unsigned from_lvl);
@ -425,11 +426,12 @@ namespace sat {
void display(std::ostream & out) const;
void display_watches(std::ostream & out) const;
void display_dimacs(std::ostream & out) const;
void display_assignment(std::ostream & out) const;
void display_justification(std::ostream & out, justification const& j) const;
protected:
void display_binary(std::ostream & out) const;
void display_units(std::ostream & out) const;
void display_assignment(std::ostream & out) const;
unsigned num_clauses() const;
bool is_unit(clause const & c) const;
bool is_empty(clause const & c) const;