mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
experimenting with cardinalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
49d7fd4f9c
commit
0123b63f8a
4 changed files with 246 additions and 103 deletions
|
|
@ -25,6 +25,7 @@ Revision History:
|
|||
#include"z3_exception.h"
|
||||
#include"common_msgs.h"
|
||||
#include"vector.h"
|
||||
#include"uint_set.h"
|
||||
#include<iomanip>
|
||||
|
||||
namespace sat {
|
||||
|
|
@ -150,79 +151,7 @@ namespace sat {
|
|||
return out;
|
||||
}
|
||||
|
||||
class uint_set {
|
||||
svector<char> m_in_set;
|
||||
svector<unsigned> m_set;
|
||||
public:
|
||||
typedef svector<unsigned>::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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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<rational> 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<card_justification*>(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<rational> 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
|
||||
|
|
|
|||
|
|
@ -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::mpz_ext> simplex;
|
||||
typedef simplex::row row;
|
||||
typedef simplex::row_iterator row_iterator;
|
||||
typedef unsynch_mpq_inf_manager eps_manager;
|
||||
typedef _scoped_numeral<eps_manager> 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<var_info> m_var_infos;
|
||||
arg_map m_ineq_rep; // Simplex: representative inequality
|
||||
u_map<row_info> 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<bool_var> 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<bool> 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);
|
||||
|
|
|
|||
|
|
@ -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<char> m_in_set;
|
||||
svector<unsigned> m_set;
|
||||
public:
|
||||
typedef svector<unsigned>::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_ */
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue