mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix xor handling, and defaults for cardinality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
ac59e7b6d3
commit
5f5819f029
|
|
@ -419,8 +419,8 @@ struct pb2bv_rewriter::imp {
|
|||
bv(m),
|
||||
m_trail(m),
|
||||
m_args(m),
|
||||
m_keep_cardinality_constraints(true),
|
||||
m_min_arity(8)
|
||||
m_keep_cardinality_constraints(false),
|
||||
m_min_arity(2)
|
||||
{}
|
||||
|
||||
bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
|
||||
|
|
@ -618,12 +618,12 @@ struct pb2bv_rewriter::imp {
|
|||
m_fresh(m),
|
||||
m_num_translated(0),
|
||||
m_rw(*this, m) {
|
||||
m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", true));
|
||||
m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", false));
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_params.append(p);
|
||||
m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", true));
|
||||
m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", false));
|
||||
}
|
||||
void collect_param_descrs(param_descrs& r) const {
|
||||
r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
|
||||
|
|
|
|||
|
|
@ -270,7 +270,6 @@ namespace opt {
|
|||
#endif
|
||||
solver& s = get_solver();
|
||||
s.assert_expr(m_hard_constraints);
|
||||
display_benchmark();
|
||||
IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
|
||||
lbool is_sat = s.check_sat(0,0);
|
||||
TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
|
||||
|
|
@ -1002,8 +1001,9 @@ namespace opt {
|
|||
TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
|
||||
return false;
|
||||
}
|
||||
if (!m_arith.is_numeral(val, r)) {
|
||||
TRACE("opt", tout << "model does not evaluate objective to a value\n";);
|
||||
unsigned bv_size;
|
||||
if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) {
|
||||
TRACE("opt", tout << "model does not evaluate objective to a value, but to " << val << "\n";);
|
||||
return false;
|
||||
}
|
||||
if (r != v) {
|
||||
|
|
@ -1199,6 +1199,9 @@ namespace opt {
|
|||
}
|
||||
|
||||
void context::display_benchmark() {
|
||||
display(verbose_stream());
|
||||
return;
|
||||
|
||||
if (opt_params(m_params).dump_benchmarks() &&
|
||||
sat_enabled() &&
|
||||
m_objectives.size() == 1 &&
|
||||
|
|
@ -1208,6 +1211,8 @@ namespace opt {
|
|||
unsigned sz = o.m_terms.size();
|
||||
inc_sat_display(verbose_stream(), get_solver(), sz, o.m_terms.c_ptr(), o.m_weights.c_ptr());
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
void context::display(std::ostream& out) {
|
||||
|
|
|
|||
|
|
@ -146,7 +146,7 @@ namespace sat {
|
|||
set_conflict(c, lit);
|
||||
break;
|
||||
default:
|
||||
m_stats.m_num_propagations++;
|
||||
m_stats.m_num_card_propagations++;
|
||||
m_num_propagations_since_pop++;
|
||||
//TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
|
||||
SASSERT(validate_unit_propagation(c));
|
||||
|
|
@ -183,8 +183,10 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::set_conflict(card& c, literal lit) {
|
||||
m_stats.m_num_card_conflicts++;
|
||||
TRACE("sat", display(tout, c, true); );
|
||||
SASSERT(validate_conflict(c));
|
||||
SASSERT(value(lit) == l_false);
|
||||
s().set_conflict(justification::mk_ext_justification(c.index()), ~lit);
|
||||
SASSERT(s().inconsistent());
|
||||
}
|
||||
|
|
@ -223,6 +225,7 @@ namespace sat {
|
|||
if (x.lit() != null_literal && x.lit().sign() == is_true) {
|
||||
x.negate();
|
||||
}
|
||||
TRACE("sat", display(tout, x, true););
|
||||
unsigned sz = x.size();
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < sz && j < 2; ++i) {
|
||||
|
|
@ -234,7 +237,16 @@ namespace sat {
|
|||
switch (j) {
|
||||
case 0:
|
||||
if (!parity(x, 0)) {
|
||||
set_conflict(x, x[0]);
|
||||
literal_set litset;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
litset.insert(x[i]);
|
||||
}
|
||||
literal_vector const& lits = s().m_trail;
|
||||
unsigned idx = lits.size()-1;
|
||||
while (!litset.contains(lits[idx])) {
|
||||
--idx;
|
||||
}
|
||||
set_conflict(x, lits[idx]);
|
||||
}
|
||||
break;
|
||||
case 1:
|
||||
|
|
@ -249,14 +261,16 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::assign(xor& x, literal lit) {
|
||||
SASSERT(!s().inconsistent());
|
||||
switch (value(lit)) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
set_conflict(x, lit);
|
||||
SASSERT(s().inconsistent());
|
||||
break;
|
||||
default:
|
||||
m_stats.m_num_propagations++;
|
||||
m_stats.m_num_xor_propagations++;
|
||||
m_num_propagations_since_pop++;
|
||||
if (s().m_config.m_drat) {
|
||||
svector<drat::premise> ps;
|
||||
|
|
@ -269,6 +283,7 @@ namespace sat {
|
|||
ps.push_back(drat::premise(drat::s_ext(), x.lit()));
|
||||
s().m_drat.add(lits, ps);
|
||||
}
|
||||
TRACE("sat", display(tout << lit << " ", x, true););
|
||||
s().assign(lit, justification::mk_ext_justification(x.index()));
|
||||
break;
|
||||
}
|
||||
|
|
@ -290,8 +305,11 @@ namespace sat {
|
|||
|
||||
|
||||
void card_extension::set_conflict(xor& x, literal lit) {
|
||||
m_stats.m_num_xor_conflicts++;
|
||||
TRACE("sat", display(tout, x, true); );
|
||||
if (value(lit) == l_true) lit.neg();
|
||||
SASSERT(validate_conflict(x));
|
||||
TRACE("sat", display(tout << lit << " ", x, true););
|
||||
s().set_conflict(justification::mk_ext_justification(x.index()), ~lit);
|
||||
SASSERT(s().inconsistent());
|
||||
}
|
||||
|
|
@ -332,7 +350,7 @@ namespace sat {
|
|||
assign(x, p ? ~x[0] : x[0]);
|
||||
}
|
||||
else if (!parity(x, 0)) {
|
||||
set_conflict(x, x[0]);
|
||||
set_conflict(x, ~x[1]);
|
||||
}
|
||||
return s().inconsistent() ? l_false : l_true;
|
||||
}
|
||||
|
|
@ -410,6 +428,7 @@ namespace sat {
|
|||
m_bound = 0;
|
||||
literal consequent = s().m_not_l;
|
||||
justification js = s().m_conflict;
|
||||
TRACE("sat", tout << consequent << " " << js << "\n";);
|
||||
m_conflict_lvl = s().get_max_lvl(consequent, js);
|
||||
if (consequent != null_literal) {
|
||||
consequent.neg();
|
||||
|
|
@ -418,7 +437,6 @@ namespace sat {
|
|||
literal_vector const& lits = s().m_trail;
|
||||
unsigned idx = lits.size()-1;
|
||||
int offset = 1;
|
||||
|
||||
DEBUG_CODE(active2pb(m_A););
|
||||
|
||||
unsigned init_marks = m_num_marks;
|
||||
|
|
@ -490,17 +508,18 @@ namespace sat {
|
|||
card& c = index2card(index);
|
||||
m_bound += offset * c.k();
|
||||
process_card(c, offset);
|
||||
++m_stats.m_num_card_resolves;
|
||||
}
|
||||
else {
|
||||
// jus.push_back(js);
|
||||
m_lemma.reset();
|
||||
m_bound += offset;
|
||||
inc_coeff(consequent, offset);
|
||||
get_xor_antecedents(idx, m_lemma);
|
||||
// get_antecedents(consequent, index, m_lemma);
|
||||
get_xor_antecedents(consequent, idx, js, m_lemma);
|
||||
for (unsigned i = 0; i < m_lemma.size(); ++i) {
|
||||
process_antecedent(~m_lemma[i], offset);
|
||||
}
|
||||
++m_stats.m_num_xor_resolves;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
@ -666,7 +685,6 @@ namespace sat {
|
|||
CTRACE("sat", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";);
|
||||
s().mark(m_lemma[i].var());
|
||||
}
|
||||
m_stats.m_num_conflicts++;
|
||||
|
||||
return true;
|
||||
|
||||
|
|
@ -797,19 +815,17 @@ namespace sat {
|
|||
The idea is to collect premises based on xor resolvents.
|
||||
Variables that are repeated an even number of times cancel out.
|
||||
*/
|
||||
void card_extension::get_xor_antecedents(unsigned index, literal_vector& r) {
|
||||
literal_vector const& lits = s().m_trail;
|
||||
literal l = lits[index + 1];
|
||||
void card_extension::get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r) {
|
||||
unsigned level = lvl(l);
|
||||
bool_var v = l.var();
|
||||
SASSERT(s().m_justification[v].get_kind() == justification::EXT_JUSTIFICATION);
|
||||
SASSERT(!is_card_index(s().m_justification[v].get_ext_justification_idx()));
|
||||
SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION);
|
||||
SASSERT(!is_card_index(js.get_ext_justification_idx()));
|
||||
TRACE("sat", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";);
|
||||
|
||||
unsigned num_marks = 0;
|
||||
unsigned count = 0;
|
||||
while (true) {
|
||||
++count;
|
||||
justification js = s().m_justification[v];
|
||||
if (js.get_kind() == justification::EXT_JUSTIFICATION) {
|
||||
unsigned idx = js.get_ext_justification_idx();
|
||||
if (is_card_index(idx)) {
|
||||
|
|
@ -838,7 +854,7 @@ namespace sat {
|
|||
r.push_back(l);
|
||||
}
|
||||
while (num_marks > 0) {
|
||||
l = lits[index];
|
||||
l = s().m_trail[index];
|
||||
v = l.var();
|
||||
unsigned n = get_parity(v);
|
||||
if (n > 0) {
|
||||
|
|
@ -859,6 +875,7 @@ namespace sat {
|
|||
}
|
||||
--index;
|
||||
--num_marks;
|
||||
js = s().m_justification[v];
|
||||
}
|
||||
|
||||
// now walk the defined literals
|
||||
|
|
@ -874,6 +891,7 @@ namespace sat {
|
|||
reset_parity(lit.var());
|
||||
}
|
||||
m_parity_trail.reset();
|
||||
TRACE("sat", tout << r << "\n";);
|
||||
}
|
||||
|
||||
void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
|
||||
|
|
@ -1274,8 +1292,12 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::collect_statistics(statistics& st) const {
|
||||
st.update("cardinality propagations", m_stats.m_num_propagations);
|
||||
st.update("cardinality conflicts", m_stats.m_num_conflicts);
|
||||
st.update("cardinality propagations", m_stats.m_num_card_propagations);
|
||||
st.update("cardinality conflicts", m_stats.m_num_card_conflicts);
|
||||
st.update("cardinality resolves", m_stats.m_num_card_resolves);
|
||||
st.update("xor propagations", m_stats.m_num_xor_propagations);
|
||||
st.update("xor conflicts", m_stats.m_num_xor_conflicts);
|
||||
st.update("xor resolves", m_stats.m_num_xor_resolves);
|
||||
}
|
||||
|
||||
bool card_extension::validate_conflict(card& c) {
|
||||
|
|
@ -1310,6 +1332,7 @@ namespace sat {
|
|||
val += coeff;
|
||||
}
|
||||
}
|
||||
CTRACE("sat", val >= 0, active2pb(m_A); display(tout, m_A););
|
||||
return val < 0;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -30,8 +30,12 @@ namespace sat {
|
|||
friend class local_search;
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_propagations;
|
||||
unsigned m_num_conflicts;
|
||||
unsigned m_num_card_propagations;
|
||||
unsigned m_num_card_conflicts;
|
||||
unsigned m_num_card_resolves;
|
||||
unsigned m_num_xor_propagations;
|
||||
unsigned m_num_xor_conflicts;
|
||||
unsigned m_num_xor_resolves;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
|
@ -172,7 +176,7 @@ namespace sat {
|
|||
bool is_card_index(unsigned idx) const { return 0 == (idx & 0x1); }
|
||||
card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 1]; }
|
||||
xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 1]; }
|
||||
void get_xor_antecedents(unsigned index, literal_vector& r);
|
||||
void get_xor_antecedents(literal l, unsigned inddex, justification js, literal_vector& r);
|
||||
|
||||
|
||||
template<typename T>
|
||||
|
|
|
|||
|
|
@ -42,19 +42,21 @@ namespace sat {
|
|||
m_index_in_unsat_stack.resize(num_constraints(), 0);
|
||||
coefficient_in_ob_constraint.resize(num_vars() + 1, 0);
|
||||
|
||||
uint_set is_neighbor;
|
||||
for (bool_var v = 0; v < num_vars(); ++v) {
|
||||
is_neighbor.reset();
|
||||
bool pol = true;
|
||||
var_info& vi = m_vars[v];
|
||||
for (unsigned k = 0; k < 2; pol = !pol, k++) {
|
||||
for (unsigned i = 0; i < m_vars[v].m_watch[pol].size(); ++i) {
|
||||
constraint const& c = m_constraints[m_vars[v].m_watch[pol][i]];
|
||||
for (unsigned j = 0; j < c.size(); ++j) {
|
||||
bool_var w = c[j].var();
|
||||
if (w == v || is_neighbor.contains(w)) continue;
|
||||
is_neighbor.insert(w);
|
||||
vi.m_neighbors.push_back(w);
|
||||
if (m_config.mode() == local_search_mode::gsat) {
|
||||
uint_set is_neighbor;
|
||||
for (bool_var v = 0; v < num_vars(); ++v) {
|
||||
is_neighbor.reset();
|
||||
bool pol = true;
|
||||
var_info& vi = m_vars[v];
|
||||
for (unsigned k = 0; k < 2; pol = !pol, k++) {
|
||||
for (unsigned i = 0; i < m_vars[v].m_watch[pol].size(); ++i) {
|
||||
constraint const& c = m_constraints[m_vars[v].m_watch[pol][i]];
|
||||
for (unsigned j = 0; j < c.size(); ++j) {
|
||||
bool_var w = c[j].var();
|
||||
if (w == v || is_neighbor.contains(w)) continue;
|
||||
is_neighbor.insert(w);
|
||||
vi.m_neighbors.push_back(w);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -69,7 +71,7 @@ namespace sat {
|
|||
void local_search::init_cur_solution() {
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
// use bias half the time.
|
||||
if (m_rand() % 100 < 50) {
|
||||
if (m_rand() % 100 < 10) {
|
||||
m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias);
|
||||
}
|
||||
}
|
||||
|
|
@ -345,12 +347,12 @@ namespace sat {
|
|||
return check(0, 0);
|
||||
}
|
||||
|
||||
#define PROGRESS(tries, flips) \
|
||||
if (tries % 10 == 0 || m_unsat_stack.empty()) { \
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \
|
||||
<< " :flips " << flips \
|
||||
<< " :unsat " << m_unsat_stack.size() \
|
||||
<< " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \
|
||||
#define PROGRESS(tries, flips) \
|
||||
if (tries % 10 == 0 || m_unsat_stack.empty()) { \
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \
|
||||
<< " :flips " << flips \
|
||||
<< " :unsat " << m_unsat_stack.size() \
|
||||
<< " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \
|
||||
}
|
||||
|
||||
void local_search::walksat() {
|
||||
|
|
|
|||
|
|
@ -100,7 +100,8 @@ namespace sat {
|
|||
vector<watch_list> m_watches; // literal: watch structure
|
||||
svector<lit_info> m_lits; // literal: attributes.
|
||||
float m_weighted_new_binaries; // metric associated with current lookahead1 literal.
|
||||
svector<prefix> m_prefix; // var: prefix where variable participates in propagation
|
||||
unsigned m_prefix; // where we are in search tree
|
||||
svector<prefix> m_vprefix; // var: prefix where variable participates in propagation
|
||||
indexed_uint_set m_freevars;
|
||||
svector<search_mode> m_search_modes; // stack of modes
|
||||
search_mode m_search_mode; // mode of search
|
||||
|
|
@ -131,6 +132,34 @@ namespace sat {
|
|||
}
|
||||
};
|
||||
|
||||
// ----------------------------------------
|
||||
// prefix updates. I use low order bits and
|
||||
// skip bit 0 in a bid to reduce details.
|
||||
|
||||
void flip_prefix() {
|
||||
if (m_trail_lim.size() < 32) {
|
||||
unsigned mask = (1 << m_trail_lim.size());
|
||||
m_prefix &= mask | (mask - 1);
|
||||
}
|
||||
}
|
||||
|
||||
void prune_prefix() {
|
||||
if (m_trail_lim.size() < 32) {
|
||||
m_prefix &= (1 << m_trail_lim.size()) - 1;
|
||||
}
|
||||
}
|
||||
|
||||
void update_prefix(literal l) {
|
||||
bool_var x = l.var();
|
||||
|
||||
unsigned p = m_prefix[x].m_prefix;
|
||||
if (m_prefix[x].m_length >= m_trail_lim.size() ||
|
||||
((p | m_prefix) != m_prefix)) {
|
||||
m_prefix[x].m_length = m_trail_lim.size();
|
||||
m_prefix[x].m_prefix = m_prefix;
|
||||
}
|
||||
}
|
||||
|
||||
// ----------------------------------------
|
||||
|
||||
void add_binary(literal l1, literal l2) {
|
||||
|
|
@ -222,6 +251,8 @@ namespace sat {
|
|||
assign(v); // v \/ ~u, u \/ v => v is a unit literal
|
||||
}
|
||||
else if (add_tc1(v, u)) {
|
||||
update_prefix(u);
|
||||
update_prefix(v);
|
||||
add_binary(u, v);
|
||||
}
|
||||
}
|
||||
|
|
@ -715,7 +746,7 @@ namespace sat {
|
|||
m_lits.push_back(lit_info());
|
||||
m_lits.push_back(lit_info());
|
||||
m_rating.push_back(0);
|
||||
m_prefix.push_back(prefix());
|
||||
m_vprefix.push_back(prefix());
|
||||
m_freevars.insert(v);
|
||||
}
|
||||
|
||||
|
|
@ -1154,7 +1185,8 @@ namespace sat {
|
|||
|
||||
bool backtrack(literal_vector& trail) {
|
||||
if (trail.empty()) return false;
|
||||
pop();
|
||||
pop();
|
||||
flip_prefix();
|
||||
assign(~trail.back());
|
||||
propagate();
|
||||
trail.pop_back();
|
||||
|
|
@ -1221,6 +1253,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
out << std::hex << "Prefix: " << m_prefix << std::dec << "\n";
|
||||
display_values(out);
|
||||
display_binary(out);
|
||||
display_clauses(out);
|
||||
|
|
|
|||
|
|
@ -48,6 +48,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver");
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -282,6 +282,7 @@ void * memory::allocate(size_t s) {
|
|||
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
||||
synchronize_counters(true);
|
||||
}
|
||||
|
||||
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue