mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
perf improvements
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e183f8b743
commit
4695ca16c8
|
@ -610,7 +610,7 @@ struct pb2bv_rewriter::imp {
|
|||
m_keep_pb_constraints(false),
|
||||
m_pb_num_system(false),
|
||||
m_pb_totalizer(false),
|
||||
m_min_arity(2)
|
||||
m_min_arity(3)
|
||||
{}
|
||||
|
||||
bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
|
||||
|
|
|
@ -213,13 +213,13 @@ namespace sat {
|
|||
return true;
|
||||
}
|
||||
|
||||
// ----------------------------
|
||||
// ----------------------------
|
||||
// card
|
||||
|
||||
bool ba_solver::init_watch(card& c) {
|
||||
clear_watch(c);
|
||||
literal root = c.lit();
|
||||
if (root != null_literal && value(root) == l_false) {
|
||||
clear_watch(c);
|
||||
c.negate();
|
||||
root.neg();
|
||||
}
|
||||
|
@ -240,6 +240,10 @@ namespace sat {
|
|||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (value(c[i]) != l_false) {
|
||||
if (j != i) {
|
||||
if (c.is_watched() && j <= bound && i > bound) {
|
||||
unwatch_literal(c[j], c);
|
||||
watch_literal(c[i], c);
|
||||
}
|
||||
c.swap(i, j);
|
||||
}
|
||||
++j;
|
||||
|
@ -255,6 +259,7 @@ namespace sat {
|
|||
// j is the number of non-false, sz - j the number of false.
|
||||
|
||||
if (j < bound) {
|
||||
if (c.is_watched()) clear_watch(c);
|
||||
SASSERT(0 < bound && bound < sz);
|
||||
literal alit = c[j];
|
||||
|
||||
|
@ -280,14 +285,19 @@ namespace sat {
|
|||
return false;
|
||||
}
|
||||
else {
|
||||
if (c.is_watched()) return true;
|
||||
clear_watch(c);
|
||||
for (unsigned i = 0; i <= bound; ++i) {
|
||||
watch_literal(c[i], c);
|
||||
}
|
||||
c.set_watch();
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
void ba_solver::clear_watch(card& c) {
|
||||
if (c.is_clear()) return;
|
||||
c.clear_watch();
|
||||
unsigned sz = std::min(c.k() + 1, c.size());
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unwatch_literal(c[i], c);
|
||||
|
@ -747,6 +757,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void ba_solver::clear_watch(pb& p) {
|
||||
p.clear_watch();
|
||||
for (unsigned i = 0; i < p.num_watch(); ++i) {
|
||||
unwatch_literal(p[i].second, p);
|
||||
}
|
||||
|
@ -896,6 +907,7 @@ namespace sat {
|
|||
// xr:
|
||||
|
||||
void ba_solver::clear_watch(xr& x) {
|
||||
x.clear_watch();
|
||||
unwatch_literal(x[0], x);
|
||||
unwatch_literal(x[1], x);
|
||||
unwatch_literal(~x[0], x);
|
||||
|
|
|
@ -63,6 +63,7 @@ namespace sat {
|
|||
tag_t m_tag;
|
||||
bool m_removed;
|
||||
literal m_lit;
|
||||
literal m_watch;
|
||||
unsigned m_glue;
|
||||
unsigned m_psm;
|
||||
unsigned m_size;
|
||||
|
@ -70,7 +71,8 @@ namespace sat {
|
|||
bool m_learned;
|
||||
unsigned m_id;
|
||||
public:
|
||||
constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz): m_tag(t), m_removed(false), m_lit(l), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
|
||||
constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz):
|
||||
m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
|
||||
ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
|
||||
unsigned id() const { return m_id; }
|
||||
tag_t tag() const { return m_tag; }
|
||||
|
@ -87,6 +89,10 @@ namespace sat {
|
|||
void set_psm(unsigned p) { m_psm = p; }
|
||||
void set_learned(bool f) { m_learned = f; }
|
||||
bool learned() const { return m_learned; }
|
||||
bool is_watched() const { return m_watch == m_lit && m_lit != null_literal; }
|
||||
void set_watch() { m_watch = m_lit; }
|
||||
void clear_watch() { m_watch = null_literal; }
|
||||
bool is_clear() const { return m_watch == null_literal && m_lit != null_literal; }
|
||||
|
||||
size_t obj_size() const { return m_obj_size; }
|
||||
card& to_card();
|
||||
|
|
Loading…
Reference in a new issue