mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

disable ternary, fixes to propagation, make bv_rewrites for multiplier n-ary

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-26 23:43:17 -07:00
parent 5352a0106d
commit fe1b4bf5ce
12 changed files with 159 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/bv_decl_plugin.h
View file

@ -447,6 +447,7 @@ public:
app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
app * mk_bv_mul(unsigned n, expr* const* args) const { return m_manager.mk_app(get_fid(), OP_BMUL, n, args); }
app * mk_bv_udiv(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV, arg1, arg2); }
app * mk_bv_udiv_i(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV_I, arg1, arg2); }
app * mk_bv_udiv0(expr * arg) const { return m_manager.mk_app(get_fid(), OP_BUDIV0, arg); }

61
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2251,11 +2251,49 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) {
return false;
}
br_status bv_rewriter::mk_mul_hoist(unsigned num_args, expr * const * args, expr_ref & result) {
if (num_args <= 1)
return BR_FAILED;
expr* z = nullptr, *u = nullptr;
for (unsigned i = 0; i < num_args; ++i) {
// ~x = -1 - x
if (m_util.is_bv_not(args[i], z)) {
unsigned sz = m_util.get_bv_size(z);
ptr_vector<expr> new_args(num_args, args);
rational p = rational(2).expt(sz) - 1;
new_args[i] = m_util.mk_bv_sub(mk_numeral(p, sz), z);
result = m_util.mk_bv_mul(num_args, new_args.data());
return BR_REWRITE3;
}
// shl(z, u) * x = shl(x * z, u)
if (m_util.is_bv_shl(args[i], z, u)) {
ptr_vector<expr> new_args(num_args, args);
new_args[i] = z;
result = m_util.mk_bv_mul(num_args, new_args.data());
result = m_util.mk_bv_shl(result, u);
return BR_REWRITE2;
}
}
return BR_FAILED;
}
br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result) {
br_status st = mk_mul_core(num_args, args, result);
if (st != BR_FAILED && st != BR_DONE)
return st;
expr* x, * y, * z, * u;
if (st == BR_DONE && is_mul(result)) {
st = mk_mul_hoist(to_app(result)->get_num_args(), to_app(result)->get_args(), result);
if (st != BR_FAILED)
return st;
st = BR_DONE;
}
if (st == BR_FAILED) {
st = mk_mul_hoist(num_args, args, result);
if (st != BR_FAILED)
return st;
}
expr* x, * y;
if (st == BR_FAILED && num_args == 2) {
x = args[0];
y = args[1];
@ -2267,27 +2305,6 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
else {
return st;
}
// ~x = -1 - x
unsigned sz = m_util.get_bv_size(x);
if (m_util.is_bv_not(x, z)) {
numeral p = rational(2).expt(sz) - 1;
result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(p, sz), z), y);
return BR_REWRITE3;
}
if (m_util.is_bv_not(y, z)) {
numeral p = rational(2).expt(sz) - 1;
result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(p, sz), z), x);
return BR_REWRITE3;
}
// shl(z, u) * x = shl(x * z, u)
if (m_util.is_bv_shl(x, z, u)) {
result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, y), u);
return BR_REWRITE2;
}
if (m_util.is_bv_shl(y, z, u)) {
result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, x), u);
return BR_REWRITE2;
}
if (m_mul2concat) {
numeral v;
unsigned bv_size;

1
src/ast/rewriter/bv_rewriter.h
View file

@ -100,6 +100,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
br_status mk_bv_mul(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_mul(2, args, result); }
br_status mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_mul_hoist(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result);

2
src/sat/sat_cleaner.cpp
View file

@ -64,7 +64,9 @@ namespace sat {
}
TRACE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";);
break;
#if ENABLE_TERNARY
case watched::TERNARY:
#endif
case watched::CLAUSE:
// skip
break;

2
src/sat/sat_gc.cpp
View file

@ -198,7 +198,7 @@ namespace sat {
if (c.on_reinit_stack())
return false;
#if ENABLE_TERNARY
if (ENABLE_TERNARY && c.size() == 3) {
if (c.size() == 3) {
return
can_delete3(c[0],c[1],c[2]) &&
can_delete3(c[1],c[0],c[2]) &&

9
src/sat/sat_integrity_checker.cpp
View file

@ -27,10 +27,12 @@ namespace sat {
s(_s) {
}
#if ENABLE_TERNARY
// for ternary clauses
static bool contains_watched(watch_list const & wlist, literal l1, literal l2) {
return wlist.contains(watched(l1, l2));
}
#endif
// for nary clauses
static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
@ -63,6 +65,7 @@ namespace sat {
if (c.frozen())
return true;
#if ENABLE_TERNARY
if (c.size() == 3) {
CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n";
tout << "watch_list:\n";
@ -71,8 +74,10 @@ namespace sat {
VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
return true;
}
else {
#endif
{
if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {
bool on_prop_stack = false;
for (unsigned i = s.m_qhead; i < s.m_trail.size(); i++) {
@ -169,11 +174,13 @@ namespace sat {
tout << "\n";);
VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l));
break;
#if ENABLE_TERNARY
case watched::TERNARY:
VERIFY(!s.was_eliminated(w.get_literal1().var()));
VERIFY(!s.was_eliminated(w.get_literal2().var()));
VERIFY(w.get_literal1().index() < w.get_literal2().index());
break;
#endif
case watched::CLAUSE:
VERIFY(!s.get_clause(w.get_clause_offset()).was_removed());
break;

2
src/sat/sat_simplifier.cpp
View file

@ -269,7 +269,9 @@ namespace sat {
watch_list::iterator end2 = wlist.end();
for (; it2 != end2; ++it2) {
switch (it2->get_kind()) {
#if ENABLE_TERNARY
case watched::TERNARY:
#endif
case watched::CLAUSE:
// consume
break;

132
src/sat/sat_solver.cpp
View file

@ -372,15 +372,15 @@ namespace sat {
}
void solver::del_clause(clause& c) {
if (!c.is_learned()) {
if (!c.is_learned())
m_stats.m_non_learned_generation++;
}
if (c.frozen()) {
if (c.frozen())
--m_num_frozen;
}
if (!c.was_removed() && m_config.m_drat && !m_drat.is_cleaned(c)) {
if (!c.was_removed() && m_config.m_drat && !m_drat.is_cleaned(c))
m_drat.del(c);
}
dealloc_clause(&c);
if (m_searching)
m_stats.m_del_clause++;
@ -448,10 +448,10 @@ namespace sat {
if (redundant && m_par)
m_par->share_clause(*this, lits[0], lits[1]);
return nullptr;
#if ENABLE_TERNARY
case 3:
if (ENABLE_TERNARY)
return mk_ter_clause(lits, st);
Z3_fallthrough;
#endif
default:
return mk_nary_clause(num_lits, lits, st);
}
@ -545,6 +545,7 @@ namespace sat {
m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
}
#if ENABLE_TERNARY
clause * solver::mk_ter_clause(literal * lits, sat::status st) {
VERIFY(ENABLE_TERNARY);
m_stats.m_mk_ter_clause++;
@ -575,7 +576,6 @@ namespace sat {
return reinit;
}
#if ENABLE_TERNARY
bool solver::propagate_ter_clause(clause& c) {
bool reinit = false;
if (value(c[1]) == l_false && value(c[2]) == l_false) {
@ -664,9 +664,11 @@ namespace sat {
void solver::attach_clause(clause & c, bool & reinit) {
SASSERT(c.size() > 2);
reinit = false;
#if ENABLE_TERNARY
if (ENABLE_TERNARY && c.size() == 3)
reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted());
else
#endif
reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
}
@ -914,11 +916,14 @@ namespace sat {
if (m_config.m_drat) m_drat.del(l1, l2);
}
void solver::detach_clause(clause & c) {
if (ENABLE_TERNARY && c.size() == 3)
void solver::detach_clause(clause& c) {
#if ENABLE_TERNARY
if (c.size() == 3) {
detach_ter_clause(c);
else
detach_nary_clause(c);
return;
}
#endif
detach_nary_clause(c);
}
void solver::detach_nary_clause(clause & c) {
@ -927,11 +932,13 @@ namespace sat {
erase_clause_watch(get_wlist(~c[1]), cls_off);
}
#if ENABLE_TERNARY
void solver::detach_ter_clause(clause & c) {
erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
}
#endif
// -----------------------
//
@ -1060,6 +1067,22 @@ namespace sat {
return r;
}
void solver::propagate_clause(clause& c, bool update, unsigned assign_level, clause_offset cls_off) {
unsigned glue;
SASSERT(value(c[0]) == l_undef);
m_stats.m_propagate++;
c.mark_used();
assign_core(c[0], justification(assign_level, cls_off));
if (update && c.is_learned() && c.glue() > 2 && num_diff_levels_below(c.size(), c.begin(), c.glue() - 1, glue))
c.set_glue(glue); \
}
void solver::set_watch(clause& c, unsigned idx, clause_offset cls_off) {
std::swap(c[1], c[idx]);
DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
}
bool solver::propagate_literal(literal l, bool update) {
literal l1, l2;
@ -1139,6 +1162,8 @@ namespace sat {
if (c[0] == not_l)
std::swap(c[0], c[1]);
CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";);
if (c.was_removed() || c.size() == 1 || c[1] != not_l) {
// Remark: this method may be invoked when the watch lists are not in a consistent state,
// and may contain dead/removed clauses, or clauses with removed literals.
@ -1155,58 +1180,65 @@ namespace sat {
break;
}
VERIFY(c[1] == not_l);
literal* l_it = c.begin() + 2;
literal* l_end = c.end();
unsigned undef_index = 0;
unsigned assign_level = curr_level;
unsigned max_index = 1;
for (; l_it != l_end; ++l_it) {
if (value(*l_it) != l_false) {
c[1] = *l_it;
*l_it = not_l;
DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
unsigned num_undef = 0;
unsigned sz = c.size();
for (unsigned i = 2; i < sz && num_undef <= 1; ++i) {
literal lit = c[i];
switch (value(lit)) {
case l_true:
it2->set_clause(lit, cls_off);
it2++;
goto end_clause_case;
}
}
SASSERT(value(c[0]) == l_false || value(c[0]) == l_undef);
if (assign_level != scope_lvl()) {
for (unsigned i = 2; i < c.size(); ++i) {
unsigned level = lvl(c[i]);
case l_undef:
undef_index = i;
++num_undef;
break;
case l_false: {
unsigned level = lvl(lit);
if (level > assign_level) {
assign_level = level;
max_index = i;
}
break;
}
IF_VERBOSE(20, verbose_stream() << "lower assignment level " << assign_level << " scope: " << scope_lvl() << "\n");
}
}
if (value(c[0]) == l_false)
assign_level = std::max(assign_level, lvl(c[0]));
if (undef_index != 0) {
set_watch(c, undef_index, cls_off);
if (value(c[0]) == l_false && num_undef == 1) {
std::swap(c[0], c[1]);
propagate_clause(c, update, assign_level, cls_off);
}
goto end_clause_case;
}
if (value(c[0]) == l_false) {
assign_level = std::max(assign_level, lvl(c[0]));
c.mark_used();
CONFLICT_CLEANUP();
set_conflict(justification(assign_level, cls_off));
return false;
}
else {
if (max_index != 1) {
IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n");
std::swap(c[1], c[max_index]);
m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
}
else {
*it2 = *it;
it2++;
}
m_stats.m_propagate++;
c.mark_used();
assign_core(c[0], justification(assign_level, cls_off));
if (update && c.is_learned() && c.glue() > 2) {
unsigned glue;
if (num_diff_levels_below(c.size(), c.begin(), c.glue() - 1, glue)) {
c.set_glue(glue);
}
}
// value(c[0]) == l_undef
if (max_index != 1) {
IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n");
set_watch(c, max_index, cls_off);
}
else {
*it2 = *it;
it2++;
}
propagate_clause(c, update, assign_level, cls_off);
end_clause_case:
break;
}
@ -3425,6 +3457,7 @@ namespace sat {
unmark_lit(~l2);
}
}
#if ENABLE_TERNARY
else if (w.is_ternary_clause()) {
literal l2 = w.get_literal1();
literal l3 = w.get_literal2();
@ -3437,6 +3470,7 @@ namespace sat {
unmark_lit(~l2);
}
}
#endif
else {
// May miss some binary/ternary clauses, but that is ok.
// I sort the watch lists at every simplification round.
@ -3581,7 +3615,7 @@ namespace sat {
auto cleanup_watch = [&](literal lit) {
for (auto const& w : get_wlist(lit)) {
IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
IF_VERBOSE(1, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
}
};
for (bool_var v : m_vars_to_free) {

4
src/sat/sat_solver.h
View file

@ -305,9 +305,11 @@ namespace sat {
void mk_bin_clause(literal l1, literal l2, sat::status st);
void mk_bin_clause(literal l1, literal l2, bool learned) { mk_bin_clause(l1, l2, learned ? sat::status::redundant() : sat::status::asserted()); }
bool propagate_bin_clause(literal l1, literal l2);
#if ENABLE_TERNARY
clause * mk_ter_clause(literal * lits, status st);
bool attach_ter_clause(clause & c, status st);
bool propagate_ter_clause(clause& c);
#endif
clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
bool has_variables_to_reinit(clause const& c) const;
bool has_variables_to_reinit(literal l1, literal l2) const;
@ -480,6 +482,8 @@ namespace sat {
bool should_propagate() const;
bool propagate_core(bool update);
bool propagate_literal(literal l, bool update);
void propagate_clause(clause& c, bool update, unsigned assign_level, clause_offset cls_off);
void set_watch(clause& c, unsigned idx, clause_offset cls_off);
// -----------------------
//

2
src/sat/sat_types.h
View file

@ -34,7 +34,7 @@ class params_ref;
class reslimit;
class statistics;
#define ENABLE_TERNARY true
#define ENABLE_TERNARY false
namespace sat {
#define SAT_VB_LVL 10

4
src/sat/sat_watched.cpp
View file

@ -71,6 +71,7 @@ namespace sat {
VERIFY(found);
}
#if ENABLE_TERNARY
void erase_ternary_watch(watch_list& wlist, literal l1, literal l2) {
watched w(l1, l2);
watch_list::iterator it = wlist.begin(), end = wlist.end();
@ -96,6 +97,7 @@ namespace sat {
}
#endif
}
#endif
void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
watch_list::iterator end = wlist.end();
@ -118,9 +120,11 @@ namespace sat {
if (w.is_learned())
out << "*";
break;
#if ENABLE_TERNARY
case watched::TERNARY:
out << "(" << w.get_literal1() << " " << w.get_literal2() << ")";
break;
#endif
case watched::CLAUSE:
out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")";
break;

14
src/sat/sat_watched.h
View file

@ -40,7 +40,11 @@ namespace sat {
class watched {
public:
enum kind {
BINARY = 0, TERNARY, CLAUSE, EXT_CONSTRAINT
BINARY = 0,
#if ENABLE_TERNARY
TERNARY,
#endif
CLAUSE, EXT_CONSTRAINT
};
private:
size_t m_val1;
@ -55,6 +59,7 @@ namespace sat {
SASSERT(learned || is_binary_non_learned_clause());
}
#if ENABLE_TERNARY
watched(literal l1, literal l2) {
SASSERT(l1 != l2);
if (l1.index() > l2.index())
@ -65,6 +70,7 @@ namespace sat {
SASSERT(get_literal1() == l1);
SASSERT(get_literal2() == l2);
}
#endif
unsigned val2() const { return m_val2; }
@ -95,9 +101,11 @@ namespace sat {
void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); }
#if ENABLE_TERNARY
bool is_ternary_clause() const { return get_kind() == TERNARY; }
literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); }
#endif
bool is_clause() const { return get_kind() == CLAUSE; }
clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); }
@ -117,7 +125,9 @@ namespace sat {
};
static_assert(0 <= watched::BINARY && watched::BINARY <= 3, "");
#if ENABLE_TERNARY
static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, "");
#endif
static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, "");
static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, "");
@ -125,8 +135,10 @@ namespace sat {
bool operator()(watched const & w1, watched const & w2) const {
if (w2.is_binary_clause()) return false;
if (w1.is_binary_clause()) return true;
#if ENABLE_TERNARY
if (w2.is_ternary_clause()) return false;
if (w1.is_ternary_clause()) return true;
#endif
return false;
}
};