mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-26 09:27:57 -08:00
parent 127bae85bd
commit 49d7fd4f9c
4 changed files with 174 additions and 85 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_context.cpp
View file

@ -1985,6 +1985,15 @@ namespace smt {
m_watches[(~cls->get_literal(idx)).index()].remove_clause(cls); m_watches[(~cls->get_literal(idx)).index()].remove_clause(cls);
} }
/**
\brief Remove boolean variable from watch lists.
*/
void context::remove_watch(bool_var v) {
literal lit(v);
m_watches[lit.index()].reset();
m_watches[(~lit).index()].reset();
}
/** /**
\brief Update the index used for backward subsumption. \brief Update the index used for backward subsumption.
*/ */

11
src/smt/smt_context.h
View file

@ -302,6 +302,7 @@ namespace smt {
} }
#endif #endif
clause_vector const& get_lemmas() const { return m_lemmas; }
literal get_literal(expr * n) const; literal get_literal(expr * n) const;
@ -604,8 +605,6 @@ namespace smt {
void remove_cls_occs(clause * cls); void remove_cls_occs(clause * cls);
void mark_as_deleted(clause * cls);
void del_clause(clause * cls); void del_clause(clause * cls);
void del_clauses(clause_vector & v, unsigned old_size); void del_clauses(clause_vector & v, unsigned old_size);
@ -630,6 +629,14 @@ namespace smt {
void reassert_units(unsigned units_to_reassert_lim); void reassert_units(unsigned units_to_reassert_lim);
public:
// \brief exposed for PB solver to participate in GC
void remove_watch(bool_var v);
void mark_as_deleted(clause * cls);
// ----------------------------------- // -----------------------------------
// //
// Internalization // Internalization

213
src/smt/theory_pb.cpp
View file

@ -289,31 +289,12 @@ namespace smt {
std::swap(m_args[index], m_args[bound]); std::swap(m_args[index], m_args[bound]);
} }
SASSERT(th.validate_unit_propagation(*this)); SASSERT(th.validate_unit_propagation(*this));
literal_vector& lits = th.get_literals();
lits.push_back(m_lit);
for (unsigned i = bound; i < sz; ++i) {
SASSERT(ctx.get_assignment(lit(i)) == l_false);
lits.push_back(~lit(i));
}
for (unsigned i = 0; i < bound; ++i) { for (unsigned i = 0; i < bound && !ctx.inconsistent(); ++i) {
literal lit2 = lit(i); th.add_assign(*this, lit(i));
lbool value = ctx.get_assignment(lit2);
switch (value) {
case l_true:
break;
case l_false:
TRACE("pb", tout << "conflict: " << alit << " " << lit2 << "\n";);
set_conflict(th, lit2);
return l_false;
case l_undef:
SASSERT(validate_assign(th, lits, lit2));
th.add_assign(*this, lits, lit2);
break;
}
} }
return l_true; return ctx.inconsistent() ? l_false : l_true;
} }
/** /**
@ -369,10 +350,8 @@ namespace smt {
SASSERT(ctx.get_assignment(lit()) == l_true); SASSERT(ctx.get_assignment(lit()) == l_true);
unsigned j = 0, sz = size(), bound = k(); unsigned j = 0, sz = size(), bound = k();
if (bound == sz) { if (bound == sz) {
literal_vector& lits = th.get_literals();
lits.push_back(lit());
for (unsigned i = 0; i < sz && !ctx.inconsistent(); ++i) { for (unsigned i = 0; i < sz && !ctx.inconsistent(); ++i) {
th.add_assign(*this, lits, lit(i)); th.add_assign(*this, lit(i));
} }
return; return;
} }
@ -412,11 +391,8 @@ namespace smt {
set_conflict(th, alit); set_conflict(th, alit);
} }
else if (j == bound) { else if (j == bound) {
literal_vector lits(sz - bound, m_args.c_ptr() + bound);
th.negate(lits);
lits.push_back(lit());
for (unsigned i = 0; i < bound && !ctx.inconsistent(); ++i) { for (unsigned i = 0; i < bound && !ctx.inconsistent(); ++i) {
th.add_assign(*this, lits, lit(i)); th.add_assign(*this, lit(i));
} }
} }
else { else {
@ -457,9 +433,11 @@ namespace smt {
theory(m.mk_family_id("pb")), theory(m.mk_family_id("pb")),
m_params(p), m_params(p),
m_simplex(m.limit()), m_simplex(m.limit()),
m_util(m), pb(m),
m_max_compiled_coeff(rational(8)), m_max_compiled_coeff(rational(8)),
m_cardinality_lemma(false), m_cardinality_lemma(false),
m_restart_lim(3),
m_restart_inc(0),
m_antecedent_exprs(m), m_antecedent_exprs(m),
m_cardinality_exprs(m) m_cardinality_exprs(m)
{ {
@ -485,7 +463,7 @@ namespace smt {
SASSERT(!ctx.b_internalized(atom)); SASSERT(!ctx.b_internalized(atom));
m_stats.m_num_predicates++; m_stats.m_num_predicates++;
if (m_util.is_aux_bool(atom)) { if (pb.is_aux_bool(atom)) {
bool_var abv = ctx.mk_bool_var(atom); bool_var abv = ctx.mk_bool_var(atom);
ctx.set_var_theory(abv, get_id()); ctx.set_var_theory(abv, get_id());
std::cout << "aux bool " << ctx.get_scope_level() << " " << mk_pp(atom, get_manager()) << " " << literal(abv) << "\n"; std::cout << "aux bool " << ctx.get_scope_level() << " " << mk_pp(atom, get_manager()) << " " << literal(abv) << "\n";
@ -496,17 +474,17 @@ namespace smt {
return true; return true;
} }
SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || SASSERT(pb.is_at_most_k(atom) || pb.is_le(atom) ||
m_util.is_ge(atom) || m_util.is_at_least_k(atom) || pb.is_ge(atom) || pb.is_at_least_k(atom) ||
m_util.is_eq(atom)); pb.is_eq(atom));
unsigned num_args = atom->get_num_args(); unsigned num_args = atom->get_num_args();
bool_var abv = ctx.mk_bool_var(atom); bool_var abv = ctx.mk_bool_var(atom);
ctx.set_var_theory(abv, get_id()); ctx.set_var_theory(abv, get_id());
ineq* c = alloc(ineq, m_mpz_mgr, literal(abv), m_util.is_eq(atom)); ineq* c = alloc(ineq, m_mpz_mgr, literal(abv), pb.is_eq(atom));
c->m_args[0].m_k = m_util.get_k(atom); c->m_args[0].m_k = pb.get_k(atom);
numeral& k = c->m_args[0].m_k; numeral& k = c->m_args[0].m_k;
arg_t& args = c->m_args[0]; arg_t& args = c->m_args[0];
@ -514,10 +492,10 @@ namespace smt {
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
expr* arg = atom->get_arg(i); expr* arg = atom->get_arg(i);
literal l = compile_arg(arg); literal l = compile_arg(arg);
numeral c = m_util.get_coeff(atom, i); numeral c = pb.get_coeff(atom, i);
args.push_back(std::make_pair(l, c)); args.push_back(std::make_pair(l, c));
} }
if (m_util.is_at_most_k(atom) || m_util.is_le(atom)) { if (pb.is_at_most_k(atom) || pb.is_le(atom)) {
// turn W <= k into -W >= -k // turn W <= k into -W >= -k
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = -args[i].second; args[i].second = -args[i].second;
@ -525,7 +503,7 @@ namespace smt {
k = -k; k = -k;
} }
else { else {
SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom) || m_util.is_eq(atom)); SASSERT(pb.is_at_least_k(atom) || pb.is_ge(atom) || pb.is_eq(atom));
} }
TRACE("pb", display(tout, *c);); TRACE("pb", display(tout, *c););
//app_ref fml1(m), fml2(m); //app_ref fml1(m), fml2(m);
@ -640,7 +618,6 @@ namespace smt {
// is available. // is available.
if (!has_bv) { if (!has_bv) {
app_ref tmp(m), fml(m); app_ref tmp(m), fml(m);
pb_util pb(m);
tmp = pb.mk_fresh_bool(); tmp = pb.mk_fresh_bool();
fml = m.mk_iff(tmp, arg); fml = m.mk_iff(tmp, arg);
TRACE("pb", tout << "create proxy " << fml << "\n";); TRACE("pb", tout << "create proxy " << fml << "\n";);
@ -754,23 +731,38 @@ namespace smt {
// ---------------------------- // ----------------------------
// cardinality constraints // cardinality constraints
class theory_pb::card_justification : public theory_propagation_justification {
class theory_pb::card_justification : public justification {
card& m_card; card& m_card;
family_id m_fid;
public: public:
card_justification(card& c, family_id fid, region & r, card_justification(card& c, family_id fid)
unsigned num_lits, literal const * lits, literal consequent): : justification(true), m_card(c), m_fid(fid) {}
theory_propagation_justification(fid, r, num_lits, lits, consequent),
m_card(c)
{}
card& get_card() { return m_card; } card& get_card() { return m_card; }
virtual void get_antecedents(conflict_resolution& cr) {
cr.mark_literal(m_card.lit());
for (unsigned i = m_card.k(); i < m_card.size(); ++i) {
cr.mark_literal(~m_card.lit(i));
}
}
virtual theory_id get_from_theory() const {
return m_fid;
}
virtual proof* mk_proof(smt::conflict_resolution& cr) { return 0; }
}; };
bool theory_pb::is_cardinality_constraint(app * atom) { bool theory_pb::is_cardinality_constraint(app * atom) {
if (m_util.is_ge(atom) && m_util.has_unit_coefficients(atom)) { if (pb.is_ge(atom) && pb.has_unit_coefficients(atom)) {
return true; return true;
} }
if (m_util.is_at_least_k(atom)) { if (pb.is_at_least_k(atom)) {
return true; return true;
} }
// TBD: other conditions // TBD: other conditions
@ -789,7 +781,7 @@ namespace smt {
unsigned num_args = atom->get_num_args(); unsigned num_args = atom->get_num_args();
bool_var abv = ctx.mk_bool_var(atom); bool_var abv = ctx.mk_bool_var(atom);
ctx.set_var_theory(abv, get_id()); ctx.set_var_theory(abv, get_id());
unsigned bound = m_util.get_k(atom).get_unsigned(); unsigned bound = pb.get_k(atom).get_unsigned();
literal lit(abv); literal lit(abv);
if (bound == 0) { if (bound == 0) {
@ -801,8 +793,11 @@ namespace smt {
ctx.mk_th_axiom(get_id(), 1, &lit); ctx.mk_th_axiom(get_id(), 1, &lit);
return true; return true;
} }
// hack to differentiate constraints that come from input vs. lemmas.
bool aux = pb.is_at_least_k(atom);
card* c = alloc(card, lit, bound); card* c = alloc(card, lit, bound, aux);
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
expr* arg = atom->get_arg(i); expr* arg = atom->get_arg(i);
@ -923,7 +918,7 @@ namespace smt {
} }
} }
out << " >= " << c.k() << "\n"; out << " >= " << c.k() << "\n";
if (c.num_propagations()) out << "propagations: " << c.num_propagations() << "\n"; if (c.all_propagations()) out << "propagations: " << c.all_propagations() << "\n";
return out; return out;
} }
@ -942,19 +937,16 @@ namespace smt {
SASSERT(ctx.inconsistent()); SASSERT(ctx.inconsistent());
} }
void theory_pb::add_assign(card& c, literal_vector const& lits, literal l) { void theory_pb::add_assign(card& c, literal l) {
context& ctx = get_context(); context& ctx = get_context();
if (ctx.get_assignment(l) == l_true) { if (ctx.get_assignment(l) == l_true) {
return; return;
} }
c.inc_propagations(*this); c.inc_propagations(*this);
m_stats.m_num_propagations++; m_stats.m_num_propagations++;
TRACE("pb", tout << "#prop: " << c.num_propagations() << " - " << lits << " " << c.lit() << " => " << l << "\n";); TRACE("pb", tout << "#prop: " << c.num_propagations() << " - " << c.lit() << " => " << l << "\n";);
SASSERT(validate_antecedents(lits));
SASSERT(validate_unit_propagation(c)); SASSERT(validate_unit_propagation(c));
ctx.assign(l, ctx.mk_justification( ctx.assign(l, ctx.mk_justification(card_justification(c, get_id())));
card_justification(
c, get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), l)));
} }
void theory_pb::clear_watch(card& c) { void theory_pb::clear_watch(card& c) {
@ -1459,6 +1451,83 @@ namespace smt {
compile_ineq(*m_to_compile[i]); compile_ineq(*m_to_compile[i]);
} }
m_to_compile.reset(); m_to_compile.reset();
return;
if (m_restart_lim <= m_restart_inc) {
m_restart_inc = 0;
if (gc()) {
m_restart_lim = 3;
}
else {
m_restart_lim *= 4;
m_restart_lim /= 3;
}
}
++m_restart_inc;
}
bool theory_pb::gc() {
context& ctx = get_context();
unsigned z = 0, nz = 0;
m_occs.reset();
for (unsigned i = 0; i < m_card_trail.size(); ++i) {
bool_var v = m_card_trail[i];
if (v == null_bool_var) continue;
card* c = m_var_infos[v].m_card;
if (c) {
unsigned np = c->num_propagations();
c->reset_propagations();
literal lit = c->lit();
if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) {
double activity = ctx.get_activity(v);
// std::cout << "activity: " << ctx.get_activity(v) << " " << np << "\n";
if (activity <= 0) {
nz++;
}
else {
z++;
clear_watch(*c);
m_var_infos[v].m_card = 0;
dealloc(c);
m_card_trail[i] = null_bool_var;
ctx.remove_watch(v);
// TBD: maybe v was used in a clause for propagation.
m_occs.insert(v);
}
}
}
}
clause_vector const& lemmas = ctx.get_lemmas();
for (unsigned i = 0; i < lemmas.size(); ++i) {
clause* cl = lemmas[i];
if (!cl->deleted()) {
unsigned sz = cl->get_num_literals();
for (unsigned j = 0; j < sz; ++j) {
literal lit = cl->get_literal(j);
if (m_occs.contains(lit.var())) {
//std::cout << "deleting clause " << lit << " " << sz << "\n";
//ctx.mark_as_deleted(cl);
break;
}
}
}
}
std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
return z*10 >= nz;
m_occs.reset();
for (unsigned i = 0; i < lemmas.size(); ++i) {
clause* cl = lemmas[i];
unsigned sz = cl->get_num_literals();
for (unsigned j = 0; j < sz; ++j) {
unsigned idx = cl->get_literal(j).index();
m_occs.insert(idx);
}
}
} }
@ -1562,10 +1631,12 @@ namespace smt {
while (m_card_trail.size() > sz) { while (m_card_trail.size() > sz) {
bool_var v = m_card_trail.back(); bool_var v = m_card_trail.back();
m_card_trail.pop_back(); m_card_trail.pop_back();
card* c = m_var_infos[v].m_card; if (v != null_bool_var) {
clear_watch(*c); card* c = m_var_infos[v].m_card;
m_var_infos[v].m_card = 0; clear_watch(*c);
dealloc(c); m_var_infos[v].m_card = 0;
dealloc(c);
}
} }
m_card_lim.resize(new_lim); m_card_lim.resize(new_lim);
@ -1803,22 +1874,18 @@ namespace smt {
m_coeff2args[coeff].push_back(v); m_coeff2args[coeff].push_back(v);
} }
std::sort(m_active_coeffs.begin(), m_active_coeffs.end()); std::sort(m_active_coeffs.begin(), m_active_coeffs.end());
for (unsigned i = 0; i < m_active_coeffs.size(); ++i) {
std::cout << m_active_coeffs[i] << " ";
}
std::cout << "\n";
return true; return true;
} }
void theory_pb::add_cardinality_lemma() { void theory_pb::add_cardinality_lemma() {
context& ctx = get_context(); context& ctx = get_context();
normalize_active_coeffs(); normalize_active_coeffs();
SASSERT(m_seen.empty());
int s = 0; int s = 0;
int new_bound = 0; int new_bound = 0;
if (!init_arg_max()) { if (!init_arg_max()) {
return; return;
} }
// TBD: can be optimized
while (s < m_bound) { while (s < m_bound) {
int coeff; int coeff;
int arg = arg_max(coeff); int arg = arg_max(coeff);
@ -1826,12 +1893,8 @@ namespace smt {
s += coeff; s += coeff;
++new_bound; ++new_bound;
} }
int slack = m_active_coeffs.empty() ? m_bound : (std::min(m_bound, static_cast<int>(m_active_coeffs[0]) - 1));
reset_arg_max(); reset_arg_max();
int slack = m_bound;
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
int coeff = get_abs_coeff(m_active_vars[i]);
slack = std::min(slack, coeff - 1);
}
while (slack > 0) { while (slack > 0) {
bool found = false; bool found = false;
@ -2007,7 +2070,6 @@ namespace smt {
m_cardinality_exprs[i] = m.mk_not(a); m_cardinality_exprs[i] = m.mk_not(a);
} }
} }
pb_util pb(m);
app_ref atl(pb.mk_at_least_k(m_cardinality_exprs.size(), m_cardinality_exprs.c_ptr(), m_bound), m); app_ref atl(pb.mk_at_least_k(m_cardinality_exprs.size(), m_cardinality_exprs.c_ptr(), m_bound), m);
VERIFY(internalize_card(atl, false)); VERIFY(internalize_card(atl, false));
bool_var abv = ctx.get_bool_var(atl); bool_var abv = ctx.get_bool_var(atl);
@ -2138,9 +2200,6 @@ namespace smt {
else { else {
card& c2 = pbj->get_card(); card& c2 = pbj->get_card();
process_card(c2, offset); process_card(c2, offset);
unsigned i = 0;
for (i = 0; i < c2.size() && c2.lit(i) != conseq; ++i) {}
// std::cout << c2.lit() << " index at " << i << " of " << c2.size();
bound = c2.k(); bound = c2.k();
} }
@ -2185,7 +2244,7 @@ namespace smt {
slack -= get_abs_coeff(alit.var()); slack -= get_abs_coeff(alit.var());
for (unsigned i = 0; 0 <= slack; ++i) { for (unsigned i = 0; 0 <= slack; ++i) {
SASSERT(i < m_active_vars.size()); SASSERT(i < m_active_vars.size());
bool_var v = m_active_vars[i]; bool_var v = m_active_vars[i];
literal lit(v, get_coeff(v) < 0); literal lit(v, get_coeff(v) < 0);
if (v != alit.var() && ctx.get_assignment(lit) == l_false) { if (v != alit.var() && ctx.get_assignment(lit) == l_false) {
@ -2196,7 +2255,7 @@ namespace smt {
SASSERT(validate_antecedents(m_antecedents)); SASSERT(validate_antecedents(m_antecedents));
ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, 0))); ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, 0)));
add_cardinality_lemma(); // add_cardinality_lemma();
return true; return true;
} }

26
src/smt/theory_pb.h
View file

@ -198,16 +198,20 @@ namespace smt {
literal_vector m_args; literal_vector m_args;
unsigned m_bound; unsigned m_bound;
unsigned m_num_propagations; unsigned m_num_propagations;
unsigned m_all_propagations;
unsigned m_compilation_threshold; unsigned m_compilation_threshold;
lbool m_compiled; lbool m_compiled;
bool m_aux;
public: public:
card(literal l, unsigned bound): card(literal l, unsigned bound, bool is_aux):
m_lit(l), m_lit(l),
m_bound(bound), m_bound(bound),
m_num_propagations(0), m_num_propagations(0),
m_all_propagations(0),
m_compilation_threshold(0), m_compilation_threshold(0),
m_compiled(l_false) m_compiled(l_false),
m_aux(is_aux)
{ {
SASSERT(bound > 0); SASSERT(bound > 0);
} }
@ -216,6 +220,7 @@ namespace smt {
literal lit(unsigned i) const { return m_args[i]; } literal lit(unsigned i) const { return m_args[i]; }
unsigned k() const { return m_bound; } unsigned k() const { return m_bound; }
unsigned size() const { return m_args.size(); } unsigned size() const { return m_args.size(); }
unsigned all_propagations() const { return m_all_propagations; }
unsigned num_propagations() const { return m_num_propagations; } unsigned num_propagations() const { return m_num_propagations; }
void add_arg(literal l); void add_arg(literal l);
@ -228,6 +233,11 @@ namespace smt {
app_ref to_expr(context& ctx); app_ref to_expr(context& ctx);
void inc_propagations(theory_pb& th); void inc_propagations(theory_pb& th);
void reset_propagations() { m_all_propagations += m_num_propagations; m_num_propagations = 0; }
bool is_aux() const { return m_aux; }
private: private:
bool validate_conflict(theory_pb& th); bool validate_conflict(theory_pb& th);
@ -293,7 +303,7 @@ namespace smt {
unsigned_vector m_ineqs_trail; unsigned_vector m_ineqs_trail;
unsigned_vector m_ineqs_lim; unsigned_vector m_ineqs_lim;
literal_vector m_literals; // temporary vector literal_vector m_literals; // temporary vector
pb_util m_util; pb_util pb;
stats m_stats; stats m_stats;
ptr_vector<ineq> m_to_compile; // inequalities to compile. ptr_vector<ineq> m_to_compile; // inequalities to compile.
unsigned m_conflict_frequency; unsigned m_conflict_frequency;
@ -302,6 +312,9 @@ namespace smt {
rational m_max_compiled_coeff; rational m_max_compiled_coeff;
bool m_cardinality_lemma; bool m_cardinality_lemma;
unsigned m_restart_lim;
unsigned m_restart_inc;
uint_set m_occs;
// internalize_atom: // internalize_atom:
literal compile_arg(expr* arg); literal compile_arg(expr* arg);
@ -330,7 +343,7 @@ namespace smt {
// be handled using cardinality constraints. // be handled using cardinality constraints.
unsigned_vector m_card_trail; unsigned_vector m_card_trail;
unsigned_vector m_card_lim; unsigned_vector m_card_lim;
bool is_cardinality_constraint(app * atom); bool is_cardinality_constraint(app * atom);
bool internalize_card(app * atom, bool gate_ctx); bool internalize_card(app * atom, bool gate_ctx);
void card2conjunction(card const& c); void card2conjunction(card const& c);
@ -339,9 +352,10 @@ namespace smt {
void watch_literal(literal lit, card* c); void watch_literal(literal lit, card* c);
void unwatch_literal(literal w, card* c); void unwatch_literal(literal w, card* c);
void add_clause(card& c, literal_vector const& lits); void add_clause(card& c, literal_vector const& lits);
void add_assign(card& c, literal_vector const& lits, literal l); void add_assign(card& c, literal l);
void remove(ptr_vector<card>& cards, card* c); void remove(ptr_vector<card>& cards, card* c);
void clear_watch(card& c); void clear_watch(card& c);
bool gc();
std::ostream& display(std::ostream& out, card const& c, bool values = false) const; std::ostream& display(std::ostream& out, card const& c, bool values = false) const;