From 0123b63f8a429d5e16060a67ff78cc6a93a515b9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Jan 2017 16:12:46 -0800 Subject: [PATCH] experimenting with cardinalities Signed-off-by: Nikolaj Bjorner --- src/sat/sat_types.h | 75 +----------------- src/smt/theory_pb.cpp | 172 ++++++++++++++++++++++++++++++++++++++---- src/smt/theory_pb.h | 22 +++--- src/util/uint_set.h | 80 +++++++++++++++++++- 4 files changed, 246 insertions(+), 103 deletions(-) diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 28d8d761a..44d3383fb 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -25,6 +25,7 @@ Revision History: #include"z3_exception.h" #include"common_msgs.h" #include"vector.h" +#include"uint_set.h" #include namespace sat { @@ -150,79 +151,7 @@ namespace sat { return out; } - class uint_set { - svector m_in_set; - svector m_set; - public: - typedef svector::const_iterator iterator; - void insert(unsigned v) { - m_in_set.reserve(v+1, false); - if (m_in_set[v]) - return; - m_in_set[v] = true; - m_set.push_back(v); - } - - void remove(unsigned v) { - if (contains(v)) { - m_in_set[v] = false; - unsigned i = 0; - for (i = 0; i < m_set.size() && m_set[i] != v; ++i) - ; - SASSERT(i < m_set.size()); - m_set[i] = m_set.back(); - m_set.pop_back(); - } - } - - uint_set& operator=(uint_set const& other) { - m_in_set = other.m_in_set; - m_set = other.m_set; - return *this; - } - - bool contains(unsigned v) const { - return v < m_in_set.size() && m_in_set[v] != 0; - } - - bool empty() const { - return m_set.empty(); - } - - // erase some variable from the set - unsigned erase() { - SASSERT(!empty()); - unsigned v = m_set.back(); - m_set.pop_back(); - m_in_set[v] = false; - return v; - } - unsigned size() const { return m_set.size(); } - iterator begin() const { return m_set.begin(); } - iterator end() const { return m_set.end(); } - void reset() { m_set.reset(); m_in_set.reset(); } - void finalize() { m_set.finalize(); m_in_set.finalize(); } - uint_set& operator&=(uint_set const& other) { - unsigned j = 0; - for (unsigned i = 0; i < m_set.size(); ++i) { - if (other.contains(m_set[i])) { - m_set[j] = m_set[i]; - ++j; - } - else { - m_in_set[m_set[i]] = false; - } - } - m_set.resize(j); - return *this; - } - uint_set& operator|=(uint_set const& other) { - for (unsigned i = 0; i < other.m_set.size(); ++i) { - insert(other.m_set[i]); - } - return *this; - } - }; + typedef tracked_uint_set uint_set; typedef uint_set bool_var_set; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 768816925..445780360 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -26,10 +26,8 @@ Notes: #include "uint_set.h" #include "smt_model_generator.h" #include "pb_rewriter_def.h" -#include "sparse_matrix_def.h" -#include "simplex_def.h" #include "mpz.h" - +#include "smt_kernel.h" namespace smt { @@ -239,6 +237,15 @@ namespace smt { SASSERT(sz >= m_bound && m_bound > 0); } + app_ref theory_pb::card::to_expr(theory_pb& th) { + ast_manager& m = th.get_manager(); + expr_ref_vector args(m); + for (unsigned i = 0; i < size(); ++i) { + args.push_back(th.literal2expr(m_args[i])); + } + return app_ref(th.pb.mk_at_least_k(args.size(), args.c_ptr(), k()), m); + } + lbool theory_pb::card::assign(theory_pb& th, literal alit) { // literal is assigned to false. context& ctx = th.get_context(); @@ -432,7 +439,6 @@ namespace smt { theory_pb::theory_pb(ast_manager& m, theory_pb_params& p): theory(m.mk_family_id("pb")), m_params(p), - m_simplex(m.limit()), pb(m), m_max_compiled_coeff(rational(8)), m_cardinality_lemma(false), @@ -1809,6 +1815,69 @@ namespace smt { return value < 0; } + bool theory_pb::validate_implies(app_ref& A, app_ref& B) { + static bool validating = false; + if (validating) return true; + validating = true; + ast_manager& m = get_manager(); + smt_params fp; + kernel k(m, fp); + k.assert_expr(A); + k.assert_expr(m.mk_not(B)); + lbool is_sat = k.check(); + validating = false; + std::cout << is_sat << "\n"; + if (is_sat != l_false) { + std::cout << A << "\n"; + std::cout << B << "\n"; + } + SASSERT(is_sat == l_false); + return true; + } + + app_ref theory_pb::justification2expr(b_justification& js, literal conseq) { + ast_manager& m = get_manager(); + app_ref result(m.mk_true(), m); + expr_ref_vector args(m); + vector coeffs; + switch(js.get_kind()) { + + case b_justification::CLAUSE: { + clause& cls = *js.get_clause(); + justification* cjs = cls.get_justification(); + if (cjs && !is_proof_justification(*cjs)) { + break; + } + for (unsigned i = 0; i < cls.get_num_literals(); ++i) { + literal lit = cls.get_literal(i); + args.push_back(literal2expr(lit)); + } + result = m.mk_or(args.size(), args.c_ptr()); + break; + } + case b_justification::BIN_CLAUSE: + result = m.mk_or(literal2expr(conseq), literal2expr(~js.get_literal())); + break; + case b_justification::AXIOM: + break; + case b_justification::JUSTIFICATION: { + justification* j = js.get_justification(); + card_justification* pbj = 0; + if (j->get_from_theory() == get_id()) { + pbj = dynamic_cast(j); + } + if (pbj != 0) { + card& c2 = pbj->get_card(); + result = card2expr(c2); + } + break; + } + default: + break; + } + return result; + } + int theory_pb::arg_max(int& max_coeff) { max_coeff = 0; int arg_max = -1; @@ -1954,12 +2023,12 @@ namespace smt { } void theory_pb::normalize_active_coeffs() { - SASSERT(m_seen.empty()); + while (!m_active_var_set.empty()) m_active_var_set.erase(); unsigned i = 0, j = 0, sz = m_active_vars.size(); for (; i < sz; ++i) { bool_var v = m_active_vars[i]; - if (!m_seen.contains(v) && get_coeff(v) != 0) { - m_seen.insert(v); + if (!m_active_var_set.contains(v) && get_coeff(v) != 0) { + m_active_var_set.insert(v); if (j != i) { m_active_vars[j] = m_active_vars[i]; } @@ -1968,10 +2037,6 @@ namespace smt { } sz = j; m_active_vars.shrink(sz); - for (i = 0; i < sz; ++i) { - m_seen.remove(m_active_vars[i]); - } - SASSERT(m_seen.empty()); } void theory_pb::inc_coeff(literal l, int offset) { @@ -2087,6 +2152,7 @@ namespace smt { bool_var v; context& ctx = get_context(); + ast_manager& m = get_manager(); m_conflict_lvl = 0; m_cardinality_lemma = false; for (unsigned i = 0; i < confl.size(); ++i) { @@ -2109,6 +2175,8 @@ namespace smt { process_card(c, 1); + app_ref A(m), B(m), C(m); + DEBUG_CODE(A = c.to_expr(*this);); // point into stack of assigned literals literal_vector const& lits = ctx.assigned_literals(); @@ -2211,6 +2279,15 @@ namespace smt { } m_bound += offset * bound; + DEBUG_CODE( + B = justification2expr(js, conseq); + C = active2expr(); + B = m.mk_and(A, B); + validate_implies(B, C); + A = C;); + + cut(); + process_next_resolvent: // find the next marked variable in the assignment stack @@ -2235,12 +2312,49 @@ namespace smt { normalize_active_coeffs(); - literal alit = get_asserting_literal(~conseq); + if (m_bound > 0 && m_active_vars.empty()) { + return false; + } + int slack = -m_bound; for (unsigned i = 0; i < m_active_vars.size(); ++i) { bool_var v = m_active_vars[i]; slack += get_abs_coeff(v); } + +#if 1 + //std::cout << slack << " " << m_bound << "\n"; + unsigned i = 0; + literal_vector const& alits = ctx.assigned_literals(); + + literal alit = get_asserting_literal(~conseq); + slack -= get_abs_coeff(alit.var()); + + for (i = alits.size(); 0 <= slack && i > 0; ) { + --i; + literal lit = alits[i]; + bool_var v = lit.var(); + // -3*x >= k + if (m_active_var_set.contains(v) && v != alit.var()) { + int coeff = get_coeff(v); + //std::cout << coeff << " " << lit << "\n"; + if (coeff < 0 && !lit.sign()) { + slack += coeff; + m_antecedents.push_back(lit); + //std::cout << "ante: " << lit << "\n"; + } + else if (coeff > 0 && lit.sign()) { + slack -= coeff; + m_antecedents.push_back(lit); + //std::cout << "ante: " << lit << "\n"; + } + } + } + SASSERT(slack < 0); + +#else + + literal alit = get_asserting_literal(~conseq); slack -= get_abs_coeff(alit.var()); for (unsigned i = 0; 0 <= slack; ++i) { @@ -2251,10 +2365,22 @@ namespace smt { m_antecedents.push_back(~lit); slack -= get_abs_coeff(v); } + if (slack < 0) { + std::cout << i << " " << m_active_vars.size() << "\n"; + } } +#endif 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))); + DEBUG_CODE( + m_antecedents.push_back(~alit); + expr_ref_vector args(m); + for (unsigned i = 0; i < m_antecedents.size(); ++i) { + args.push_back(literal2expr(m_antecedents[i])); + } + B = m.mk_not(m.mk_and(args.size(), args.c_ptr())); + validate_implies(A, B); ); // add_cardinality_lemma(); return true; } @@ -2379,10 +2505,26 @@ namespace smt { return true; } - void theory_pb::negate(literal_vector & lits) { - for (unsigned i = 0; i < lits.size(); ++i) { - lits[i].neg(); + app_ref theory_pb::literal2expr(literal lit) { + ast_manager& m = get_manager(); + app_ref arg(m.mk_const(symbol(lit.var()), m.mk_bool_sort()), m); + return app_ref(lit.sign() ? m.mk_not(arg) : arg, m); + } + + app_ref theory_pb::active2expr() { + ast_manager& m = get_manager(); + expr_ref_vector args(m); + vector coeffs; + normalize_active_coeffs(); + for (unsigned i = 0; i < m_active_vars.size(); ++i) { + bool_var v = m_active_vars[i]; + int coeff = get_coeff(v); + literal lit(v, get_coeff(v) < 0); + args.push_back(literal2expr(lit)); + coeffs.push_back(rational(get_abs_coeff(v))); } + rational k(m_bound); + return app_ref(pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), k), m); } // display methods diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index e48816c1c..56f3d1e76 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -24,6 +24,7 @@ Notes: #include "pb_decl_plugin.h" #include "smt_clause.h" #include "theory_pb_params.h" +#include "smt_b_justification.h" #include "simplex.h" namespace smt { @@ -41,9 +42,6 @@ namespace smt { class card_justification; typedef rational numeral; - typedef simplex::simplex simplex; - typedef simplex::row row; - typedef simplex::row_iterator row_iterator; typedef unsynch_mpq_inf_manager eps_manager; typedef _scoped_numeral scoped_eps_numeral; @@ -230,7 +228,7 @@ namespace smt { void negate(); - app_ref to_expr(context& ctx); + app_ref to_expr(theory_pb& th); void inc_propagations(theory_pb& th); @@ -292,12 +290,6 @@ namespace smt { theory_pb_params m_params; svector m_var_infos; - arg_map m_ineq_rep; // Simplex: representative inequality - u_map m_ineq_row_info; // Simplex: row information per variable - uint_set m_vars; // Simplex: 0-1 variables. - simplex m_simplex; // Simplex: tableau - literal_vector m_explain_lower; // Simplex: explanations for lower bounds - literal_vector m_explain_upper; // Simplex: explanations for upper bounds unsynch_mpq_inf_manager m_mpq_inf_mgr; // Simplex: manage inf_mpq numerals mutable unsynch_mpz_manager m_mpz_mgr; // Simplex: manager mpz numerals unsigned_vector m_ineqs_trail; @@ -396,7 +388,7 @@ namespace smt { svector m_active_vars; int m_bound; literal_vector m_antecedents; - uint_set m_seen; + tracked_uint_set m_active_var_set; expr_ref_vector m_antecedent_exprs; svector m_antecedent_signs; expr_ref_vector m_cardinality_exprs; @@ -425,17 +417,21 @@ namespace smt { void cut(); bool is_proof_justification(justification const& j) const; - bool validate_lemma(); void hoist_maximal_values(); + bool validate_lemma(); void validate_final_check(); void validate_final_check(ineq& c); void validate_assign(ineq const& c, literal_vector const& lits, literal l) const; void validate_watch(ineq const& c) const; bool validate_unit_propagation(card const& c); bool validate_antecedents(literal_vector const& lits); - void negate(literal_vector & lits); + bool validate_implies(app_ref& A, app_ref& B); + app_ref active2expr(); + app_ref literal2expr(literal lit); + app_ref card2expr(card& c) { return c.to_expr(*this); } + app_ref justification2expr(b_justification& js, literal conseq); bool proofs_enabled() const { return get_manager().proofs_enabled(); } justification* justify(literal l1, literal l2); diff --git a/src/util/uint_set.h b/src/util/uint_set.h index e78a4b0b6..7ff497709 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -25,9 +25,9 @@ Revision History: COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); class uint_set : unsigned_vector { - + public: - + typedef unsigned data; uint_set() {} @@ -253,5 +253,81 @@ inline std::ostream & operator<<(std::ostream & target, const uint_set & s) { return target; } + +class tracked_uint_set { + svector m_in_set; + svector m_set; +public: + typedef svector::const_iterator iterator; + void insert(unsigned v) { + m_in_set.reserve(v+1, false); + if (m_in_set[v]) + return; + m_in_set[v] = true; + m_set.push_back(v); + } + + void remove(unsigned v) { + if (contains(v)) { + m_in_set[v] = false; + unsigned i = 0; + for (i = 0; i < m_set.size() && m_set[i] != v; ++i) + ; + SASSERT(i < m_set.size()); + m_set[i] = m_set.back(); + m_set.pop_back(); + } + } + + tracked_uint_set& operator=(tracked_uint_set const& other) { + m_in_set = other.m_in_set; + m_set = other.m_set; + return *this; + } + + bool contains(unsigned v) const { + return v < m_in_set.size() && m_in_set[v] != 0; + } + + bool empty() const { + return m_set.empty(); + } + + // erase some variable from the set + unsigned erase() { + SASSERT(!empty()); + unsigned v = m_set.back(); + m_set.pop_back(); + m_in_set[v] = false; + return v; + } + unsigned size() const { return m_set.size(); } + iterator begin() const { return m_set.begin(); } + iterator end() const { return m_set.end(); } + void reset() { m_set.reset(); m_in_set.reset(); } + void finalize() { m_set.finalize(); m_in_set.finalize(); } + tracked_uint_set& operator&=(tracked_uint_set const& other) { + unsigned j = 0; + for (unsigned i = 0; i < m_set.size(); ++i) { + if (other.contains(m_set[i])) { + m_set[j] = m_set[i]; + ++j; + } + else { + m_in_set[m_set[i]] = false; + } + } + m_set.resize(j); + return *this; + } + tracked_uint_set& operator|=(tracked_uint_set const& other) { + for (unsigned i = 0; i < other.m_set.size(); ++i) { + insert(other.m_set[i]); + } + return *this; + } +}; + + #endif /* UINT_SET_H_ */