From e36eba116877f537060d1428b77fc7d75798ff9f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Dec 2016 09:58:23 -0800 Subject: [PATCH] added cardinality solver Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 5 + src/smt/theory_pb.cpp | 456 +++++++++++++++++++++++++++++++++++++--- src/smt/theory_pb.h | 113 ++++++---- 3 files changed, 501 insertions(+), 73 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index e6d4d0c07..f8d8cbaf8 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3342,6 +3342,11 @@ namespace smt { bool context::restart(lbool& status, unsigned curr_lvl) { + std::cout << "restart: " << m_lemmas.size() << "\n"; + for (unsigned i = 0; i < m_lemmas.size(); ++i) { + display_clause(std::cout, m_lemmas[i]); std::cout << "\n"; + } + if (m_last_search_failure != OK) { if (status != l_false) { // build candidate model before returning diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 7b066f1be..9c162164f 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -228,41 +228,193 @@ namespace smt { return true; } - // cardinality + // ----------------------------- + // cardinality constraints - // - // - lbool theory_pb::cardinality::assign_at_least(theory_pb& th, literal lit) { - // literal is assigned to false. + void theory_pb::card::negate() { + m_lit.neg(); + unsigned sz = size(); + for (unsigned i = 0; i < sz; ++i) { + m_args[i].neg(); + } + m_bound = sz - m_bound + 1; + } + + lbool theory_pb::card::assign(theory_pb& th, literal lit) { + TRACE("pb", tout << "assign: " << m_lit << " " << ~lit << " " << m_bound << "\n";); + // literal is assigned to false. context& ctx = th.get_context(); - SASSERT(m_type == le_t); SASSERT(m_bound > 0); - SASSERT(m_args.size() >= 2*m_bound); - SASSERT(m_watch_sum < m_bound); + SASSERT(ctx.get_assignment(lit) == l_false); unsigned index = m_bound + 1; - bool all_false = true; for (unsigned i = 0; i <= m_bound; ++i) { if (m_args[i] == lit) { index = i; break; } - all_false &= (value(args[i]) == l_false); } + SASSERT(index <= m_bound); + SASSERT(m_args[index] == lit); + + unsigned sz = size(); - for (unsigned i = m_bound + 1; i < m_args.size(); ++i) { - if (value(m_args[i]) != l_false) { + // find a literal to swap with: + for (unsigned i = m_bound + 1; i < sz; ++i) { + literal lit2 = m_args[i]; + if (ctx.get_assignment(lit2) != l_false) { + TRACE("pb", tout << "swap " << lit2 << "\n";); std::swap(m_args[index], m_args[i]); - // watch m_args[index] now - // end-clause-case + if (ctx.get_assignment(m_args[0]) == l_false) { + std::swap(m_args[0], m_args[index]); + } + th.watch_literal(lit2, this); + return l_undef; } } - if (all_false) { - - } + // conflict + if (0 != index && ctx.get_assignment(m_args[0]) == l_false) { + TRACE("pb", tout << "conflict " << m_args[0] << " " << lit << "\n";); + set_conflict(th, m_args[0], lit); + return l_false; + } - return l_undef; + TRACE("pb", tout << "no swap " << index << " " << lit << "\n";); + // there are no literals to swap with, + // prepare for unit propagation by swapping the false literal into + // position 0. Then literals in positions 1..m_bound have to be + // assigned l_true. + if (index != 0) { + std::swap(m_args[index], m_args[0]); + } + SASSERT(m_args[0] == lit); + literal_vector lits; + lits.push_back(~lit); + for (unsigned i = m_bound + 1; i < sz; ++i) { + SASSERT(ctx.get_assignment(m_args[i]) == l_false); + lits.push_back(~m_args[i]); + } + + for (unsigned i = 1; i <= m_bound; ++i) { + literal lit2 = m_args[i]; + lbool value = ctx.get_assignment(lit2); + switch (value) { + case l_true: + break; + case l_false: + TRACE("pb", tout << "conflict: " << lit << " " << lit2 << "\n";); + set_conflict(th, lit, lit2); + return l_false; + case l_undef: + SASSERT(validate_assign(th, lits, lit2)); + th.add_assign(*this, lits, lit2); + break; + } + } + + return l_true; } + + void theory_pb::card::set_conflict(theory_pb& th, literal l1, literal l2) { + SASSERT(validate_conflict(th)); + context& ctx = th.get_context(); + literal_vector lits; + SASSERT(ctx.get_assignment(l1) == l_false); + SASSERT(ctx.get_assignment(l2) == l_false); + lits.push_back(l1); + lits.push_back(l2); + unsigned sz = size(); + for (unsigned i = m_bound + 1; i < sz; ++i) { + SASSERT(ctx.get_assignment(m_args[i]) == l_false); + lits.push_back(m_args[i]); + } + th.add_clause(*this, lits); + } + + bool theory_pb::card::validate_conflict(theory_pb& th) { + context& ctx = th.get_context(); + unsigned num_false = 0; + for (unsigned i = 0; i < size(); ++i) { + if (ctx.get_assignment(m_args[i]) == l_false) { + ++num_false; + } + } + return size() - num_false < m_bound; + } + + bool theory_pb::card::validate_assign(theory_pb& th, literal_vector const& lits, literal l) { + context& ctx = th.get_context(); + SASSERT(ctx.get_assignment(l) == l_undef); + for (unsigned i = 0; i < lits.size(); ++i) { + SASSERT(ctx.get_assignment(lits[i]) == l_true); + } + return size() - lits.size() <= m_bound; + } + + void theory_pb::card::init_watch(theory_pb& th, bool is_true) { + context& ctx = th.get_context(); + + if (lit().sign() == is_true) { + negate(); + } + // put the non-false literals into the head. + unsigned i = 0, j = 0, sz = size(); + for (i = 0; i < sz; ++i) { + if (ctx.get_assignment(lit(i)) != l_false) { + if (j != i) { + std::swap(m_args[i], m_args[j]); + } + ++j; + } + } + // j is the number of non-false, sz - j the number of false. + if (j < m_bound) { + set_conflict(th, m_args[m_bound], m_args[m_bound-1]); + } + else if (j == m_bound) { + literal_vector lits(size() - m_bound, m_args.c_ptr() + m_bound); + for (i = 0; i < j; ++i) { + if (ctx.get_assignment(lit(i)) == l_undef) { + th.add_assign(*this, lits, lit(i)); + } + } + } + else { + for (unsigned i = 0; i <= m_bound; ++i) { + th.watch_literal(lit(i), this); + } + } + } + + + void theory_pb::card::add_arg(literal lit) { + if (lit == false_literal) { + return; + } + else if (lit == true_literal) { + if (m_bound > 0) { + --m_bound; + } + } + else { + m_args.push_back(lit); + } + + } + + void theory_pb::card::inc_propagations(theory_pb& th) { + ++m_num_propagations; + if (m_compiled == l_false && m_num_propagations >= m_compilation_threshold) { + // m_compiled = l_undef; + // th.m_to_compile.push_back(&c); + } + } + + + + + // ------------------------ + // theory_pb theory_pb::theory_pb(ast_manager& m, theory_pb_params& p): theory(m.mk_family_id("pb")), @@ -281,6 +433,7 @@ namespace smt { reset_eh(); } + theory * theory_pb::mk_fresh(context * new_ctx) { return alloc(theory_pb, new_ctx->get_manager(), m_params); } @@ -451,6 +604,7 @@ namespace smt { bool theory_pb::internalize_atom(app * atom, bool gate_ctx) { context& ctx = get_context(); + TRACE("pb", tout << mk_pp(atom, get_manager()) << "\n";); if (ctx.b_internalized(atom)) { return false; } @@ -462,12 +616,16 @@ namespace smt { ctx.set_var_theory(abv, get_id()); return true; } + + if (internalize_card(atom, gate_ctx)) { + return true; + } + SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || m_util.is_ge(atom) || m_util.is_at_least_k(atom) || m_util.is_eq(atom)); - unsigned num_args = atom->get_num_args(); bool_var abv = ctx.mk_bool_var(atom); ctx.set_var_theory(abv, get_id()); @@ -680,7 +838,7 @@ namespace smt { return negate?~literal(bv):literal(bv); } - void theory_pb::del_watch(watch_list& watch, unsigned index, ineq& c, unsigned ineq_index) { + void theory_pb::del_watch(ineq_watch& watch, unsigned index, ineq& c, unsigned ineq_index) { SASSERT(c.is_ge()); if (index < watch.size()) { std::swap(watch[index], watch[watch.size()-1]); @@ -730,6 +888,7 @@ namespace smt { } } + void theory_pb::watch_literal(literal lit, ineq* c) { init_watch(lit.var()); ptr_vector* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()]; @@ -740,6 +899,7 @@ namespace smt { ineqs->push_back(c); } + void theory_pb::watch_var(bool_var v, ineq* c) { init_watch(v); ptr_vector* ineqs = m_var_infos[v].m_var_watch; @@ -774,6 +934,182 @@ namespace smt { } } + // ---------------------------- + // cardinality constraints + + class theory_pb::card_justification : public theory_propagation_justification { + card& m_card; + public: + card_justification(card& c, family_id fid, region & r, + unsigned num_lits, literal const * lits, literal consequent): + theory_propagation_justification(fid, r, num_lits, lits, consequent), + m_card(c) + {} + card& get_card() { return m_card; } + }; + + + bool theory_pb::is_cardinality_constraint(app * atom) { + if (m_util.is_ge(atom) && m_util.has_unit_coefficients(atom)) { + return true; + } + if (m_util.is_at_most_k(atom)) { + return true; + } + // TBD: other conditions + return false; + } + + bool theory_pb::internalize_card(app * atom, bool gate_ctx) { + if (!is_cardinality_constraint(atom)) { + return false; + } + context& ctx = get_context(); + unsigned num_args = atom->get_num_args(); + bool_var abv = ctx.mk_bool_var(atom); + ctx.set_var_theory(abv, get_id()); + unsigned bound = m_util.get_k(atom).get_unsigned(); + + card* c = alloc(card, literal(abv), bound); + + for (unsigned i = 0; i < num_args; ++i) { + expr* arg = atom->get_arg(i); + c->add_arg(compile_arg(arg)); + } + + literal lit(abv); + + if (c->k() == 0) { + ctx.mk_th_axiom(get_id(), 1, &lit); + dealloc(c); + } + else if (c->k() > c->size()) { + lit.neg(); + ctx.mk_th_axiom(get_id(), 1, &lit); + dealloc(c); + } + else if (c->k() == c->size()) { + literal_vector lits; + for (unsigned i = 0; i < c->size(); ++i) { + lits.push_back(~c->lit(i)); + } + lits.push_back(lit); + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + lit.neg(); + for (unsigned i = 0; i < c->size(); ++i) { + literal lits2[2] = { lit, c->lit(i) }; + ctx.mk_th_axiom(get_id(), 2, lits2); + } + dealloc(c); + } + else { + SASSERT(0 < c->k() && c->k() < c->size()); + + // initialize compilation thresholds, TBD + + init_watch(abv); + m_var_infos[abv].m_card = c; + m_card_trail.push_back(abv); + } + return true; + } + + void theory_pb::watch_literal(literal lit, card* c) { + init_watch(lit.var()); + ptr_vector* cards = m_var_infos[lit.var()].m_lit_cwatch[lit.sign()]; + if (cards == 0) { + cards = alloc(ptr_vector); + m_var_infos[lit.var()].m_lit_cwatch[lit.sign()] = cards; + } + cards->push_back(c); + } + + + void theory_pb::unwatch_literal(literal lit, card* c) { + if (m_var_infos.size() <= static_cast(lit.var())) { + return; + } + ptr_vector* cards = m_var_infos[lit.var()].m_lit_cwatch[lit.sign()]; + if (cards) { + remove(*cards, c); + } + } + + void theory_pb::remove(ptr_vector& cards, card* c) { + for (unsigned j = 0; j < cards.size(); ++j) { + if (cards[j] == c) { + std::swap(cards[j], cards[cards.size()-1]); + cards.pop_back(); + break; + } + } + } + + std::ostream& theory_pb::display(std::ostream& out, card const& c, bool values) const { + ast_manager& m = get_manager(); + context& ctx = get_context(); + out << c.lit(); + if (c.lit() != null_literal) { + if (values) { + out << "@(" << ctx.get_assignment(c.lit()); + if (ctx.get_assignment(c.lit()) != l_undef) { + out << ":" << ctx.get_assign_level(c.lit()); + } + out << ")"; + } + ctx.display_literal_verbose(out, c.lit()); out << "\n"; + } + else { + out << " "; + } + for (unsigned i = 0; i < c.size(); ++i) { + literal l = c.lit(i); + out << l; + if (values) { + out << "@(" << ctx.get_assignment(l); + if (ctx.get_assignment(l) != l_undef) { + out << ":" << ctx.get_assign_level(l); + } + out << ") "; + } + } + out << " >= " << c.k() << "\n"; + if (c.num_propagations()) out << "propagations: " << c.num_propagations() << "\n"; + return out; + } + + + void theory_pb::add_clause(card& c, literal_vector const& lits) { + m_stats.m_num_conflicts++; + context& ctx = get_context(); + justification* js = 0; + if (proofs_enabled()) { + js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); + } + c.inc_propagations(*this); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + } + + void theory_pb::add_assign(card& c, literal_vector const& lits, literal l) { + c.inc_propagations(*this); + m_stats.m_num_propagations++; + context& ctx = get_context(); + TRACE("pb", tout << "#prop:" << c.num_propagations() << " - " << lits << " " << c.lit() << " => " << l << "\n";); + + ctx.assign(l, ctx.mk_justification( + card_justification( + c, get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), l))); + } + + void theory_pb::clear_watch(card& c) { + for (unsigned i = 0; i <= c.k(); ++i) { + literal w = c.lit(i); + unwatch_literal(w, &c); + } + } + + // + void theory_pb::collect_statistics(::statistics& st) const { st.update("pb conflicts", m_stats.m_num_conflicts); st.update("pb propagations", m_stats.m_num_propagations); @@ -791,6 +1127,8 @@ namespace smt { } m_ineqs_trail.reset(); m_ineqs_lim.reset(); + m_card_trail.reset(); + m_card_lim.reset(); m_stats.reset(); m_to_compile.reset(); } @@ -807,6 +1145,7 @@ namespace smt { void theory_pb::assign_eh(bool_var v, bool is_true) { ptr_vector* ineqs = 0; + context& ctx = get_context(); literal nlit(v, is_true); init_watch(v); TRACE("pb", tout << "assign: " << ~nlit << "\n";); @@ -867,6 +1206,39 @@ namespace smt { assign_eq(*c, is_true); } } + + ptr_vector* cards = m_var_infos[v].m_lit_cwatch[nlit.sign()]; + if (cards != 0 && !ctx.inconsistent()) { + ptr_vector::iterator it = cards->begin(), it2 = it, end = cards->end(); + for (; it != end; ++it) { + if (ctx.get_assignment((*it)->lit()) != l_true) { + continue; + } + switch ((*it)->assign(*this, nlit)) { + case l_false: // conflict + for (; it != end; ++it, ++it2) { + *it2 = *it; + } + cards->set_end(it2); + return; + case l_undef: // watch literal was swapped + break; + case l_true: // unit propagation, keep watching the literal + if (it2 != it) { + *it2 = *it; + } + ++it2; + break; + } + } + cards->set_end(it2); + } + + card* crd = m_var_infos[v].m_card; + if (crd != 0 && !ctx.inconsistent()) { + crd->init_watch(*this, is_true); + } + } literal_vector& theory_pb::get_all_literals(ineq& c, bool negate) { @@ -931,6 +1303,7 @@ namespace smt { } }; + class theory_pb::negate_ineq : public trail { ineq& c; public: @@ -953,7 +1326,6 @@ namespace smt { ctx.push_trail(value_trail(c.m_nfixed)); ctx.push_trail(rewatch_vars(*this, c)); - clear_watch(c); SASSERT(c.is_ge()); unsigned sz = c.size(); if (c.lit().sign() == is_true) { @@ -1112,7 +1484,7 @@ namespace smt { inequalities are unit literals and formulas in negation normal form (inequalities are closed under negation). */ - bool theory_pb::assign_watch_ge(bool_var v, bool is_true, watch_list& watch, unsigned watch_index) { + bool theory_pb::assign_watch_ge(bool_var v, bool is_true, ineq_watch& watch, unsigned watch_index) { bool removed = false; context& ctx = get_context(); ineq& c = *watch[watch_index]; @@ -1343,6 +1715,7 @@ namespace smt { void theory_pb::push_scope_eh() { m_ineqs_lim.push_back(m_ineqs_trail.size()); + m_card_lim.push_back(m_card_trail.size()); } void theory_pb::pop_scope_eh(unsigned num_scopes) { @@ -1370,6 +1743,20 @@ namespace smt { dealloc(c); } m_ineqs_lim.resize(new_lim); + + + new_lim = m_card_lim.size() - num_scopes; + sz = m_card_lim[new_lim]; + while (m_card_trail.size() > sz) { + bool_var v = m_card_trail.back(); + m_card_trail.pop_back(); + card* c = m_var_infos[v].m_card; + clear_watch(*c); + m_var_infos[v].m_card = 0; + dealloc(c); + } + + m_card_lim.resize(new_lim); } void theory_pb::clear_watch(ineq& c) { @@ -1454,11 +1841,8 @@ namespace smt { inc_propagations(c); m_stats.m_num_propagations++; context& ctx = get_context(); - TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - "; - for (unsigned i = 0; i < lits.size(); ++i) { - tout << lits[i] << " "; - } - tout << "=> " << l << "\n"; + TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - " << lits; + tout << " => " << l << "\n"; display(tout, c, true);); ctx.assign(l, ctx.mk_justification( @@ -1466,7 +1850,7 @@ namespace smt { c, get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), l))); } - + void theory_pb::add_clause(ineq& c, literal_vector const& lits) { inc_propagations(c); @@ -2113,9 +2497,9 @@ namespace smt { } void theory_pb::display_watch(std::ostream& out, bool_var v, bool sign) const { - watch_list const* w = m_var_infos[v].m_lit_watch[sign]; + ineq_watch const* w = m_var_infos[v].m_lit_watch[sign]; if (!w) return; - watch_list const& wl = *w; + ineq_watch const& wl = *w; out << "watch: " << literal(v, sign) << " |-> "; for (unsigned i = 0; i < wl.size(); ++i) { out << wl[i]->lit() << " "; @@ -2129,10 +2513,10 @@ namespace smt { display_watch(out, vi, true); } for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { - watch_list const* w = m_var_infos[vi].m_var_watch; + ineq_watch const* w = m_var_infos[vi].m_var_watch; if (!w) continue; out << "watch (v): " << literal(vi) << " |-> "; - watch_list const& wl = *w; + ineq_watch const& wl = *w; for (unsigned i = 0; i < wl.size(); ++i) { out << wl[i]->lit() << " "; } @@ -2144,6 +2528,14 @@ namespace smt { display(out, *c, true); } } + + for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { + card* c = m_var_infos[vi].m_card; + if (c) { + display(out, *c, true); + } + } + } diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 4ad9feb06..f86615e6c 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -37,6 +37,9 @@ namespace smt { class negate_ineq; class remove_var; class undo_bound; + + class card_justification; + typedef rational numeral; typedef simplex::simplex simplex; typedef simplex::row row; @@ -181,55 +184,55 @@ namespace smt { }; - enum card_t { - eq_t, - le_t, - ge_t - }; - - struct cardinality { + // cardinality constraint args >= bound + class card { literal m_lit; // literal repesenting predicate - card_t m_type; literal_vector m_args; unsigned m_bound; - unsigned m_watch_sum; unsigned m_num_propagations; unsigned m_compilation_threshold; lbool m_compiled; - cardinality(literal l, card_t t, unsigned bound): + public: + card(literal l, unsigned bound): m_lit(l), - m_type(t), m_bound(bound), - m_watch_sum(0), m_num_propagations(0), m_compilation_threshold(0), - m_compiled(0) - {} + m_compiled(l_false) + { + } + + literal lit() const { return m_lit; } + literal lit(unsigned i) const { return m_args[i]; } + unsigned k() const { return m_bound; } + unsigned size() const { return m_args.size(); } + unsigned num_propagations() const { return m_num_propagations; } + void add_arg(literal l); + + void init_watch(theory_pb& th, bool is_true); - std::ostream& display(std::ostream& out) const; + lbool assign(theory_pb& th, literal lit); + + void negate(); app_ref to_expr(context& ctx); - lbool assign_at_least(literal lit); - // - // lit occurs within m_bound positions - // m_bound <= m_args.size()/2 - // m_lit is pos - // type at least: m_args >= m_bound - // lit occurs with opposite sign in m_args - // type at most: m_args <= m_bound - // lit occurs with same sign in m_args - // search for literal above m_bound, such that - // either lit' is positive, type = ge_t - // lit' is negative, type = le_t - // lit' is unassigned - // swap lit and lit' in watch list - // If there is a single unassigned lit', and no other to swap, perform unit propagation - // If there are no literals to swap with, then create conflict clause - // + void inc_propagations(theory_pb& th); + private: + + bool validate_conflict(theory_pb& th); + + bool validate_assign(theory_pb& th, literal_vector const& lits, literal l); + + void set_conflict(theory_pb& th, literal l1, literal l2); }; + typedef ptr_vector card_watch; + typedef ptr_vector ineq_watch; + typedef map arg_map; + + struct row_info { unsigned m_slack; // slack variable in simplex tableau numeral m_bound; // bound @@ -239,18 +242,21 @@ namespace smt { row_info(): m_slack(0) {} }; - typedef ptr_vector watch_list; - typedef map arg_map; struct var_info { - watch_list* m_lit_watch[2]; - watch_list* m_var_watch; - ineq* m_ineq; + ineq_watch* m_lit_watch[2]; + ineq_watch* m_var_watch; + ineq* m_ineq; + + card_watch* m_lit_cwatch[2]; + card* m_card; - var_info(): m_var_watch(0), m_ineq(0) + var_info(): m_var_watch(0), m_ineq(0), m_card(0) { m_lit_watch[0] = 0; m_lit_watch[1] = 0; + m_lit_cwatch[0] = 0; + m_lit_cwatch[1] = 0; } void reset() { @@ -258,6 +264,9 @@ namespace smt { dealloc(m_lit_watch[1]); dealloc(m_var_watch); dealloc(m_ineq); + dealloc(m_lit_cwatch[0]); + dealloc(m_lit_cwatch[1]); + dealloc(m_card); } }; @@ -287,9 +296,11 @@ namespace smt { // internalize_atom: literal compile_arg(expr* arg); - void add_watch(ineq& c, unsigned index); - void del_watch(watch_list& watch, unsigned index, ineq& c, unsigned ineq_index); void init_watch(bool_var v); + + // general purpose pb constraints + void add_watch(ineq& c, unsigned index); + void del_watch(ineq_watch& watch, unsigned index, ineq& c, unsigned ineq_index); void init_watch_literal(ineq& c); void init_watch_var(ineq& c); void clear_watch(ineq& c); @@ -298,11 +309,31 @@ namespace smt { void unwatch_literal(literal w, ineq* c); void unwatch_var(bool_var v, ineq* c); void remove(ptr_vector& ineqs, ineq* c); - bool assign_watch_ge(bool_var v, bool is_true, watch_list& watch, unsigned index); + + bool assign_watch_ge(bool_var v, bool is_true, ineq_watch& watch, unsigned index); void assign_watch(bool_var v, bool is_true, ineq& c); void assign_ineq(ineq& c, bool is_true); void assign_eq(ineq& c, bool is_true); + // cardinality constraints + // these are cheaper to handle than general purpose PB constraints + // and in the common case PB constraints with small coefficients can + // be handled using cardinality constraints. + + unsigned_vector m_card_trail; + unsigned_vector m_card_lim; + bool is_cardinality_constraint(app * atom); + bool internalize_card(app * atom, bool gate_ctx); + + void watch_literal(literal lit, card* c); + void unwatch_literal(literal w, card* c); + void add_clause(card& c, literal_vector const& lits); + void add_assign(card& c, literal_vector const& lits, literal l); + void remove(ptr_vector& cards, card* c); + void clear_watch(card& c); + std::ostream& display(std::ostream& out, card const& c, bool values = false) const; + + // simplex: literal set_explain(literal_vector& explains, unsigned var, literal expl); bool update_bound(bool_var v, literal explain, bool is_lower, mpq_inf const& bound);