From 314f03c12ca7730d00315d2bf42b8aa5ac4e73ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Nov 2013 16:44:08 -0800 Subject: [PATCH] started new PB solver Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/opt/fu_malik.cpp | 2 +- src/smt/theory_pb.cpp | 703 ++++++++++++++++++++++++++++++++++++++++++ src/smt/theory_pb.h | 117 +++++++ 4 files changed, 822 insertions(+), 2 deletions(-) create mode 100644 src/smt/theory_pb.cpp create mode 100644 src/smt/theory_pb.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index e92899436..b52934dfe 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -63,11 +63,11 @@ def init_project_def(): add_lib('tab', ['muz', 'transforms'], 'muz/tab') add_lib('bmc', ['muz', 'transforms'], 'muz/bmc') add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc'], 'muz/fp') - add_lib('opt', ['smt'], 'opt') add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') + add_lib('opt', ['smt', 'smtlogic_tactics'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 77eb108a9..db4cb93d2 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include "fu_malik.h" -#include "smtlogics/qfbv_tactic.h" +#include "qfbv_tactic.h" #include "tactic2solver.h" #include "goal.h" #include "probe.h" diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp new file mode 100644 index 000000000..171615c95 --- /dev/null +++ b/src/smt/theory_pb.cpp @@ -0,0 +1,703 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_pb.cpp + +Abstract: + + Pseudo-Boolean theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-05 + +Notes: + + +--*/ + +#include "theory_pb.h" +#include "smt_context.h" +#include "ast_pp.h" +#include "sorting_network.h" + +namespace smt { + + theory_pb::theory_pb(ast_manager& m): + theory(m.mk_family_id("card")), + m_util(m) + {} + + theory_pb::~theory_pb() { + reset_eh(); + } + + theory * theory_pb::mk_fresh(context * new_ctx) { + return alloc(theory_pb, new_ctx->get_manager()); + } + + bool theory_pb::internalize_atom(app * atom, bool gate_ctx) { + context& ctx = get_context(); + ast_manager& m = get_manager(); + unsigned num_args = atom->get_num_args(); + SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom)); + + if (ctx.b_internalized(atom)) { + return false; + } + + m_stats.m_num_predicates++; + + SASSERT(!ctx.b_internalized(atom)); + bool_var abv = ctx.mk_bool_var(atom); + + ineq* c = alloc(ineq, atom, literal(abv)); + c->m_k = m_util.get_k(atom); + int& k = c->m_k; + arg_t& args = c->m_args; + + // extract literals and coefficients. + for (unsigned i = 0; i < num_args; ++i) { + expr* arg = atom->get_arg(i); + literal l = compile_arg(arg); + int c = m_util.get_le_coeff(atom, i); + args.push_back(std::make_pair(l, c)); + } + // turn W <= k into -W >= -k + for (unsigned i = 0; i < args.size(); ++i) { + args[i].second = -args[i].second; + } + k = -k; + lbool is_true = normalize_ineq(args, k); + + literal lit(abv); + switch(is_true) { + case l_false: + lit = ~lit; + // fall-through + case l_true: + ctx.mk_th_axiom(get_id(), 1, &lit); + TRACE("card", tout << mk_pp(atom, m) << " := " << lit << "\n";); + dealloc(c); + return true; + case l_undef: + break; + } + + // TBD: special cases: args.size() == 1 + + // maximal coefficient: + int& max_coeff = c->m_max_coeff; + max_coeff = 0; + for (unsigned i = 0; i < args.size(); ++i) { + max_coeff = std::max(max_coeff, args[i].second); + } + + // compute watch literals: + int sum = 0; + unsigned& wsz = c->m_watch_sz; + wsz = 0; + while (sum < k + max_coeff && wsz < args.size()) { + sum += args[wsz].second; + wsz++; + } + + for (unsigned i = 0; i < wsz; ++i) { + add_watch(args[i].first, c); + } + + // pre-compile threshold for cardinality + bool is_cardinality = true; + for (unsigned i = 0; is_cardinality && i < args.size(); ++i) { + is_cardinality = (args[i].second == 1); + } + if (is_cardinality) { + unsigned log = 1, n = 1; + while (n <= args.size()) { + ++log; + n *= 2; + } + c->m_compilation_threshold = args.size()*log; + TRACE("card", tout << "threshold:" << (args.size()*log) << "\n";); + } + else { + c->m_compilation_threshold = UINT_MAX; + } + m_ineqs.insert(abv, c); + m_ineqs_trail.push_back(abv); + + TRACE("card", display(tout, *c);); + + return true; + } + + literal theory_pb::compile_arg(expr* arg) { + context& ctx = get_context(); + ast_manager& m = get_manager(); + if (!ctx.b_internalized(arg)) { + ctx.internalize(arg, false); + } + bool_var bv; + bool has_bv = false; + bool negate = m.is_not(arg, arg); + if (ctx.b_internalized(arg)) { + bv = ctx.get_bool_var(arg); + if (null_theory_var == ctx.get_var_theory(bv)) { + ctx.set_var_theory(bv, get_id()); + } + has_bv = (ctx.get_var_theory(bv) == get_id()); + } + + // pre-processing should better remove negations under cardinality. + // assumes relevancy level = 2 or 0. + if (!has_bv) { + expr_ref tmp(m), fml(m); + tmp = m.mk_fresh_const("card_proxy",m.mk_bool_sort()); + fml = m.mk_iff(tmp, arg); + ctx.internalize(fml, false); + SASSERT(ctx.b_internalized(tmp)); + bv = ctx.get_bool_var(tmp); + SASSERT(null_theory_var == ctx.get_var_theory(bv)); + ctx.set_var_theory(bv, get_id()); + literal lit(ctx.get_bool_var(fml)); + ctx.mk_th_axiom(get_id(), 1, &lit); + ctx.mark_as_relevant(tmp); + } + return negate?~literal(bv):literal(bv); + } + + void theory_pb::add_watch(literal l, ineq* c) { + unsigned idx = l.index(); + ptr_vector* ineqs; + if (!m_watch.find(idx, ineqs)) { + ineqs = alloc(ptr_vector); + m_watch.insert(idx, ineqs); + } + ineqs->push_back(c); + } + + static unsigned gcd(unsigned a, unsigned b) { + while (a != b) { + if (a == 0) return b; + if (b == 0) return a; + SASSERT(a != 0 && b != 0); + if (a < b) { + b %= a; + } + else { + a %= b; + } + } + return a; + } + + lbool theory_pb::normalize_ineq(arg_t& args, int& k) { + + // normalize first all literals to be positive: + // then we can can compare them more easily. + for (unsigned i = 0; i < args.size(); ++i) { + if (args[i].first.sign()) { + args[i].first.neg(); + k -= args[i].second; + args[i].second = -args[i].second; + } + } + // sort and coalesce arguments: + std::sort(args.begin(), args.end()); + for (unsigned i = 0; i + 1 < args.size(); ++i) { + if (args[i].first == args[i+1].first) { + args[i].second += args[i+1].second; + for (unsigned j = i+1; j + 1 < args.size(); ++j) { + args[j] = args[j+1]; + } + args.resize(args.size()-1); + } + if (args[i].second == 0) { + for (unsigned j = i; j + 1 < args.size(); ++j) { + args[j] = args[j+1]; + } + args.resize(args.size()-1); + } + } + // + // Ensure all coefficients are positive: + // c*l + y >= k + // <=> + // c*(1-~l) + y >= k + // <=> + // c - c*~l + y >= k + // <=> + // -c*~l + y >= k - c + // + unsigned sum = 0; + for (unsigned i = 0; i < args.size(); ++i) { + int c = args[i].second; + if (c < 0) { + args[i].second = -c; + args[i].first = ~args[i].first; + k -= c; + } + sum += args[i].second; + } + // detect tautologies: + if (k <= 0) { + args.reset(); + return l_true; + } + // detect infeasible constraints: + if (static_cast(sum) < k) { + args.reset(); + return l_false; + } + // Ensure the largest coefficient is not larger than k: + for (unsigned i = 0; i < args.size(); ++i) { + int c = args[i].second; + if (c > k) { + args[i].second = k; + } + } + SASSERT(!args.empty()); + + // apply cutting plane reduction: + unsigned g = 0; + for (unsigned i = 0; g != 1 && i < args.size(); ++i) { + int c = args[i].second; + if (c != k) { + g = gcd(g, c); + } + } + if (g == 0) { + // all coefficients are equal to k. + for (unsigned i = 0; i < args.size(); ++i) { + SASSERT(args[i].second == k); + args[i].second = 1; + } + k = 1; + } + else if (g > 1) { + // + // Example 5x + 5y + 2z + 2u >= 5 + // becomes 3x + 3y + z + u >= 3 + // + int k_new = k / g; // k_new is the ceiling of k / g. + if (gcd(k, g) != g) { + k_new++; + } + for (unsigned i = 0; i < args.size(); ++i) { + int c = args[i].second; + if (c == k) { + c = k_new; + } + else { + c = c / g; + } + args[i].second = c; + } + k = k_new; + } + + return l_undef; + } + + void theory_pb::collect_statistics(::statistics& st) const { + st.update("pb axioms", m_stats.m_num_axioms); + st.update("pb propagations", m_stats.m_num_propagations); + st.update("pb predicates", m_stats.m_num_predicates); + st.update("pb compilations", m_stats.m_num_compiles); + } + + void theory_pb::reset_eh() { + + // m_watch; + u_map*>::iterator it = m_watch.begin(), end = m_watch.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + u_map::iterator itc = m_ineqs.begin(), endc = m_ineqs.end(); + for (; itc != endc; ++itc) { + dealloc(itc->m_value); + } + m_watch.reset(); + m_ineqs.reset(); + m_ineqs_trail.reset(); + m_ineqs_lim.reset(); + m_stats.reset(); + } + + +#if 0 + void theory_pb::propagate_assignment(ineq& c) { + if (c.m_compiled) { + return; + } + if (should_compile(c)) { + compile_ineq(c); + return; + } + context& ctx = get_context(); + ast_manager& m = get_manager(); + arg_t const& args = c.m_args; + bool_var abv = c.m_bv; + int min = c.m_current_min; + int max = c.m_current_max; + int k = c.m_k; + + TRACE("card", + tout << mk_pp(c.m_app, m) << " min: " + << min << " max: " << max << "\n";); + + // + // if min > k && abv != l_false -> force abv false + // if max <= k && abv != l_true -> force abv true + // if min == k && abv == l_true -> force positive + // unassigned literals false + // if max == k + 1 && abv == l_false -> force negative + // unassigned literals false + // + lbool aval = ctx.get_assignment(abv); + if (min > k && aval != l_false) { + literal_vector& lits = get_lits(); + int curr_min = accumulate_min(lits, c); + SASSERT(curr_min > k); + add_assign(c, lits, ~literal(abv)); + } + else if (max <= k && aval != l_true) { + literal_vector& lits = get_lits(); + int curr_max = accumulate_max(lits, c); + SASSERT(curr_max <= k); + add_assign(c, lits, literal(abv)); + } + else if (min <= k && k < min + get_max_delta(c) && aval == l_true) { + literal_vector& lits = get_lits(); + lits.push_back(~literal(abv)); + int curr_min = accumulate_min(lits, c); + if (curr_min > k) { + add_clause(c, lits); + } + else { + for (unsigned i = 0; i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (curr_min + inc > k && inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc > 0)); + } + } + } + } + else if (max - get_max_delta(c) <= k && k < max && aval == l_false) { + literal_vector& lits = get_lits(); + lits.push_back(literal(abv)); + int curr_max = accumulate_max(lits, c); + if (curr_max <= k) { + add_clause(c, lits); + } + else { + for (unsigned i = 0; i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (curr_max - abs(inc) <= k && dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + add_assign(c, lits, literal(bv, inc < 0)); + } + } + } + } + else if (aval == l_true) { + SASSERT(min < k); + literal_vector& lits = get_lits(); + int curr_min = accumulate_min(lits, c); + bool all_inc = curr_min == k; + unsigned num_incs = 0; + for (unsigned i = 0; all_inc && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) { + all_inc = inc + min > k; + num_incs++; + } + } + if (num_incs > 0) { + std::cout << "missed T propgations " << num_incs << "\n"; + } + } + else if (aval == l_false) { + literal_vector& lits = get_lits(); + lits.push_back(literal(abv)); + int curr_max = accumulate_max(lits, c); + bool all_dec = curr_max > k; + unsigned num_decs = 0; + for (unsigned i = 0; all_dec && i < args.size(); ++i) { + bool_var bv = args[i].first; + int inc = args[i].second; + if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) { + all_dec = inc + max <= k; + num_decs++; + } + } + if (num_decs > 0) { + std::cout << "missed F propgations " << num_decs << "\n"; + } + } + } +#endif + + void theory_pb::assign_eh(bool_var v, bool is_true) { + context& ctx = get_context(); + ast_manager& m = get_manager(); + ptr_vector* ineqs = 0; + ineq* c = 0; + TRACE("card", tout << "assign: " << mk_pp(ctx.bool_var2expr(v), m) << " <- " << is_true << "\n";); + + if (m_watch.find(v, ineqs)) { + for (unsigned i = 0; i < ineqs->size(); ++i) { + // TBD: assign_use(v, is_true, *(*ineqs)[i]); + } + } + if (m_ineqs.find(v, c)) { + // TBD: propagate_assignment(*c); + } + } + + struct theory_pb::sort_expr { + theory_pb& th; + context& ctx; + ast_manager& m; + expr_ref_vector m_trail; + sort_expr(theory_pb& th): + th(th), + ctx(th.get_context()), + m(th.get_manager()), + m_trail(m) {} + typedef expr* T; + typedef expr_ref_vector vector; + + T mk_ite(T a, T b, T c) { + if (m.is_true(a)) { + return b; + } + if (m.is_false(a)) { + return c; + } + if (b == c) { + return b; + } + m_trail.push_back(m.mk_ite(a, b, c)); + return m_trail.back(); + } + + T mk_le(T a, T b) { + return mk_ite(b, a, m.mk_true()); + } + + T mk_default() { + return m.mk_false(); + } + + literal internalize(ineq& ca, expr* e) { + obj_map cache; + for (unsigned i = 0; i < ca.m_args.size(); ++i) { + cache.insert(ca.m_app->get_arg(i), literal(ca.m_args[i].first)); + } + cache.insert(m.mk_false(), false_literal); + cache.insert(m.mk_true(), true_literal); + ptr_vector todo; + todo.push_back(e); + expr *a, *b, *c; + literal la, lb, lc; + while (!todo.empty()) { + expr* t = todo.back(); + if (cache.contains(t)) { + todo.pop_back(); + continue; + } + VERIFY(m.is_ite(t, a, b, c)); + unsigned sz = todo.size(); + if (!cache.find(a, la)) { + todo.push_back(a); + } + if (!cache.find(b, lb)) { + todo.push_back(b); + } + if (!cache.find(c, lc)) { + todo.push_back(c); + } + if (sz != todo.size()) { + continue; + } + todo.pop_back(); + cache.insert(t, mk_ite(ca, t, la, lb, lc)); + } + return cache.find(e); + } + + literal mk_ite(ineq& ca, expr* t, literal a, literal b, literal c) { + if (a == true_literal) { + return b; + } + else if (a == false_literal) { + return c; + } + else if (b == true_literal && c == false_literal) { + return a; + } + else if (b == false_literal && c == true_literal) { + return ~a; + } + else if (b == c) { + return b; + } + else { + literal l; + if (ctx.b_internalized(t)) { + l = literal(ctx.get_bool_var(t)); + } + else { + l = literal(ctx.mk_bool_var(t)); + } + add_clause(~l, ~a, b); + add_clause(~l, a, c); + add_clause(l, ~a, ~b); + add_clause(l, a, ~c); + TRACE("card", tout << mk_pp(t, m) << " ::= (if "; + ctx.display_detailed_literal(tout, a); + ctx.display_detailed_literal(tout << " ", b); + ctx.display_detailed_literal(tout << " ", c); + tout << ")\n";); + return l; + } + } + + + // auxiliary clauses don't get garbage collected. + void add_clause(literal a, literal b, literal c) { + literal_vector& lits = th.get_lits(); + if (a != null_literal) lits.push_back(a); + if (b != null_literal) lits.push_back(b); + if (c != null_literal) lits.push_back(c); + justification* js = 0; + TRACE("card", + ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX, 0); + } + + void add_clause(literal l1, literal l2) { + add_clause(l1, l2, null_literal); + } + + }; + + + bool theory_pb::should_compile(ineq& c) { +#if 1 + return false; +#else + return c.m_num_propagations > c.m_compilation_threshold; +#endif + } + + void theory_pb::compile_ineq(ineq& c) { + ++m_stats.m_num_compiles; + ast_manager& m = get_manager(); + context& ctx = get_context(); + app* a = c.m_app; + SASSERT(m_util.is_at_most_k(a)); + literal atmostk; + int k = m_util.get_k(a); + unsigned num_args = a->get_num_args(); + + sort_expr se(*this); + if (k >= static_cast(num_args)) { + atmostk = true_literal; + } + else if (k < 0) { + atmostk = false_literal; + } + else { + sorting_network sn(se); + expr_ref_vector in(m), out(m); + for (unsigned i = 0; i < num_args; ++i) { + in.push_back(c.m_app->get_arg(i)); + } + sn(in, out); + atmostk = ~se.internalize(c, out[k].get()); // k'th output is 0. + TRACE("card", tout << "~atmost: " << mk_pp(out[k].get(), m) << "\n";); + } + literal thl = c.m_lit; + se.add_clause(~thl, atmostk); + se.add_clause(thl, ~atmostk); + TRACE("card", tout << mk_pp(a, m) << "\n";); + // auxiliary clauses get removed when popping scopes. + // we have to recompile the circuit after back-tracking. + ctx.push_trail(value_trail(c.m_compiled)); + c.m_compiled = true; + } + + + void theory_pb::init_search_eh() { + + } + + void theory_pb::push_scope_eh() { + m_ineqs_lim.push_back(m_ineqs_trail.size()); + } + + void theory_pb::pop_scope_eh(unsigned num_scopes) { + unsigned sz = m_ineqs_lim[m_ineqs_lim.size()-num_scopes]; + while (m_ineqs_trail.size() > sz) { + SASSERT(m_ineqs.contains(m_ineqs_trail.back())); + m_ineqs.remove(m_ineqs_trail.back()); + m_ineqs_trail.pop_back(); + } + m_ineqs_lim.resize(m_ineqs_lim.size()-num_scopes); + } + + std::ostream& theory_pb::display(std::ostream& out, ineq& c) const { + ast_manager& m = get_manager(); + out << mk_pp(c.m_app, m) << "\n"; + for (unsigned i = 0; i < c.m_args.size(); ++i) { + out << c.m_args[i].second << "*" << c.m_args[i].first; + if (i + 1 < c.m_args.size()) { + out << " + "; + } + } + out << " >= " << c.m_k << "\n" + << "propagations: " << c.m_num_propagations + << " max_coeff: " << c.m_max_coeff + << " watch size: " << c.m_watch_sz + << "\n"; + return out; + } + + + literal_vector& theory_pb::get_lits() { + m_literals.reset(); + return m_literals; + } + + void theory_pb::add_assign(ineq& c, literal_vector const& lits, literal l) { + literal_vector ls; + ++c.m_num_propagations; + m_stats.m_num_propagations++; + context& ctx = get_context(); + for (unsigned i = 0; i < lits.size(); ++i) { + ls.push_back(~lits[i]); + } + ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), ls.size(), ls.c_ptr(), l))); + } + + + + void theory_pb::add_clause(ineq& c, literal_vector const& lits) { + ++c.m_num_propagations; + m_stats.m_num_axioms++; + context& ctx = get_context(); + TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + justification* js = 0; + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), + lits.size(), lits.c_ptr()); + verbose_stream() << "\n";); + // ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + } +} diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h new file mode 100644 index 000000000..432d4e497 --- /dev/null +++ b/src/smt/theory_pb.h @@ -0,0 +1,117 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_pb.h + +Abstract: + + Cardinality theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-05 + +Notes: + + This custom theory handles cardinality constraints + It performs unit propagation and switches to creating + sorting circuits if it keeps having to propagate (create new clauses). +--*/ + +#include "smt_theory.h" +#include "card_decl_plugin.h" +#include "smt_clause.h" + +namespace smt { + class theory_pb : public theory { + + struct sort_expr; + typedef svector > arg_t; + + struct stats { + unsigned m_num_axioms; + unsigned m_num_propagations; + unsigned m_num_predicates; + unsigned m_num_compiles; + void reset() { memset(this, 0, sizeof(*this)); } + stats() { reset(); } + }; + + + struct ineq { + app* m_app; + literal m_lit; // literal repesenting predicate + arg_t m_args; // encode args[0]*coeffs[0]+...+args[n-1]*coeffs[n-1] >= m_k; + int m_k; // invariants: m_k > 0, coeffs[i] > 0 + + // Watch the first few positions until the sum satisfies: + // sum coeffs[i] >= m_lower + max_coeff + + int m_max_coeff; // maximal coefficient. + unsigned m_watch_sz; // number of literals being watched. + unsigned m_num_propagations; + unsigned m_compilation_threshold; + bool m_compiled; + + ineq(app* a, literal l): + m_app(a), + m_lit(l), + m_num_propagations(0), + m_compilation_threshold(UINT_MAX), + m_compiled(false) + {} + }; + + typedef ptr_vector watch_list; + + u_map m_watch; // per literal. + u_map m_ineqs; // per inequality. + unsigned_vector m_ineqs_trail; + unsigned_vector m_ineqs_lim; + literal_vector m_literals; // temporary vector + card_util m_util; + stats m_stats; + + // internalize_atom: + lbool normalize_ineq(arg_t& args, int& k); + literal compile_arg(expr* arg); + void add_watch(literal l, ineq* c); + + std::ostream& display(std::ostream& out, ineq& c) const; + + void add_clause(ineq& c, literal_vector const& lits); + void add_assign(ineq& c, literal_vector const& lits, literal l); + literal_vector& get_lits(); + + // + // Utilities to compile cardinality + // constraints into a sorting network. + // + void compile_ineq(ineq& c); + bool should_compile(ineq& c); + unsigned get_compilation_threshold(ineq& c); + public: + theory_pb(ast_manager& m); + + virtual ~theory_pb(); + + virtual theory * mk_fresh(context * new_ctx); + virtual bool internalize_atom(app * atom, bool gate_ctx); + virtual bool internalize_term(app * term) { UNREACHABLE(); return false; } + virtual void new_eq_eh(theory_var v1, theory_var v2) { } + virtual void new_diseq_eh(theory_var v1, theory_var v2) { } + virtual bool use_diseqs() const { return false; } + virtual bool build_models() const { return false; } + virtual final_check_status final_check_eh() { return FC_DONE; } + + virtual void reset_eh(); + virtual void assign_eh(bool_var v, bool is_true); + virtual void init_search_eh(); + virtual void push_scope_eh(); + virtual void pop_scope_eh(unsigned num_scopes); + virtual void collect_statistics(::statistics & st) const; + + }; +};