mirror of
https://github.com/Z3Prover/z3
synced 2025-07-17 01:46:39 +00:00
Less allocation during lookup, remove unused argument
This commit is contained in:
parent
b5af2164f4
commit
be20c0d54e
11 changed files with 45 additions and 25 deletions
|
@ -50,7 +50,7 @@ namespace polysat {
|
||||||
/** The boolean variable associated to this constraint */
|
/** The boolean variable associated to this constraint */
|
||||||
sat::bool_var m_bvar = sat::null_bool_var;
|
sat::bool_var m_bvar = sat::null_bool_var;
|
||||||
|
|
||||||
constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
|
constraint(ckind_t k): m_kind(k) {}
|
||||||
|
|
||||||
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
|
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
|
||||||
|
|
||||||
|
|
|
@ -231,7 +231,7 @@ namespace polysat {
|
||||||
}
|
}
|
||||||
|
|
||||||
/** Look up constraint among stored constraints. */
|
/** Look up constraint among stored constraints. */
|
||||||
constraint* constraint_manager::dedup(constraint* c1) {
|
constraint* constraint_manager::dedup_store(constraint* c1) {
|
||||||
constraint* c2 = nullptr;
|
constraint* c2 = nullptr;
|
||||||
if (m_dedup.constraints.find(c1, c2)) {
|
if (m_dedup.constraints.find(c1, c2)) {
|
||||||
dealloc(c1);
|
dealloc(c1);
|
||||||
|
@ -246,6 +246,15 @@ namespace polysat {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** Find stored constraint */
|
||||||
|
constraint* constraint_manager::dedup_find(constraint* c1) const {
|
||||||
|
constraint* c = nullptr;
|
||||||
|
if (!m_dedup.constraints.find(c1, c)) {
|
||||||
|
SASSERT(c == nullptr);
|
||||||
|
}
|
||||||
|
return c;
|
||||||
|
}
|
||||||
|
|
||||||
void constraint_manager::gc() {
|
void constraint_manager::gc() {
|
||||||
LOG_H1("gc");
|
LOG_H1("gc");
|
||||||
gc_clauses();
|
gc_clauses();
|
||||||
|
@ -294,7 +303,7 @@ namespace polysat {
|
||||||
pdd lhs = a;
|
pdd lhs = a;
|
||||||
pdd rhs = b;
|
pdd rhs = b;
|
||||||
ule_constraint::simplify(is_positive, lhs, rhs);
|
ule_constraint::simplify(is_positive, lhs, rhs);
|
||||||
return { dedup(alloc(ule_constraint, *this, lhs, rhs)), is_positive };
|
return { dedup_store(alloc(ule_constraint, lhs, rhs)), is_positive };
|
||||||
}
|
}
|
||||||
|
|
||||||
signed_constraint constraint_manager::eq(pdd const& p) {
|
signed_constraint constraint_manager::eq(pdd const& p) {
|
||||||
|
@ -305,9 +314,17 @@ namespace polysat {
|
||||||
return ~ule(b, a);
|
return ~ule(b, a);
|
||||||
}
|
}
|
||||||
|
|
||||||
signed_constraint constraint_manager::find_eq(pdd const& p) /* const */ {
|
signed_constraint constraint_manager::find_eq(pdd const& p) const {
|
||||||
// TODO: implement as lookup rather than allocating/deduping constraint
|
return find_ule(p, p.manager().zero());
|
||||||
return eq(p);
|
}
|
||||||
|
|
||||||
|
signed_constraint constraint_manager::find_ule(pdd const& a, pdd const& b) const {
|
||||||
|
bool is_positive = true;
|
||||||
|
pdd lhs = a;
|
||||||
|
pdd rhs = b;
|
||||||
|
ule_constraint::simplify(is_positive, lhs, rhs);
|
||||||
|
ule_constraint tmp(lhs, rhs); // TODO: this still allocates ule_constraint::m_vars
|
||||||
|
return { dedup_find(&tmp), is_positive };
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -322,19 +339,19 @@ namespace polysat {
|
||||||
}
|
}
|
||||||
|
|
||||||
signed_constraint constraint_manager::umul_ovfl(pdd const& a, pdd const& b) {
|
signed_constraint constraint_manager::umul_ovfl(pdd const& a, pdd const& b) {
|
||||||
return { dedup(alloc(umul_ovfl_constraint, *this, a, b)), true };
|
return { dedup_store(alloc(umul_ovfl_constraint, a, b)), true };
|
||||||
}
|
}
|
||||||
|
|
||||||
signed_constraint constraint_manager::smul_ovfl(pdd const& a, pdd const& b) {
|
signed_constraint constraint_manager::smul_ovfl(pdd const& a, pdd const& b) {
|
||||||
return { dedup(alloc(smul_fl_constraint, *this, a, b, true)), true };
|
return { dedup_store(alloc(smul_fl_constraint, a, b, true)), true };
|
||||||
}
|
}
|
||||||
|
|
||||||
signed_constraint constraint_manager::smul_udfl(pdd const& a, pdd const& b) {
|
signed_constraint constraint_manager::smul_udfl(pdd const& a, pdd const& b) {
|
||||||
return { dedup(alloc(smul_fl_constraint, *this, a, b, false)), true };
|
return { dedup_store(alloc(smul_fl_constraint, a, b, false)), true };
|
||||||
}
|
}
|
||||||
|
|
||||||
signed_constraint constraint_manager::mk_op_constraint(op_constraint::code op, pdd const& p, pdd const& q, pdd const& r) {
|
signed_constraint constraint_manager::mk_op_constraint(op_constraint::code op, pdd const& p, pdd const& q, pdd const& r) {
|
||||||
return { dedup(alloc(op_constraint, *this, op, p, q, r)), true };
|
return { dedup_store(alloc(op_constraint, op, p, q, r)), true };
|
||||||
}
|
}
|
||||||
|
|
||||||
// To do signed comparison of bitvectors, flip the msb and do unsigned comparison:
|
// To do signed comparison of bitvectors, flip the msb and do unsigned comparison:
|
||||||
|
@ -410,6 +427,8 @@ namespace polysat {
|
||||||
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
|
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
|
||||||
// b ≠ 0 ==> r < b
|
// b ≠ 0 ==> r < b
|
||||||
// b = 0 ==> q = -1
|
// b = 0 ==> q = -1
|
||||||
|
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
|
||||||
|
// Maybe we need something like an op_constraint for better propagation.
|
||||||
s.add_clause(eq(b * q + r - a), false);
|
s.add_clause(eq(b * q + r - a), false);
|
||||||
s.add_clause(~umul_ovfl(b, q), false);
|
s.add_clause(~umul_ovfl(b, q), false);
|
||||||
// r <= b*q+r
|
// r <= b*q+r
|
||||||
|
|
|
@ -67,9 +67,9 @@ namespace polysat {
|
||||||
constraint* get_bv2c(sat::bool_var bv) const;
|
constraint* get_bv2c(sat::bool_var bv) const;
|
||||||
|
|
||||||
void store(constraint* c);
|
void store(constraint* c);
|
||||||
void erase(constraint* c);
|
|
||||||
|
|
||||||
constraint* dedup(constraint* c);
|
constraint* dedup_store(constraint* c);
|
||||||
|
constraint* dedup_find(constraint* c) const;
|
||||||
|
|
||||||
void gc_constraints();
|
void gc_constraints();
|
||||||
void gc_clauses();
|
void gc_clauses();
|
||||||
|
@ -103,7 +103,8 @@ namespace polysat {
|
||||||
signed_constraint lookup(sat::literal lit) const;
|
signed_constraint lookup(sat::literal lit) const;
|
||||||
|
|
||||||
/** Find constraint p == 0; returns null if it doesn't exist yet */
|
/** Find constraint p == 0; returns null if it doesn't exist yet */
|
||||||
signed_constraint find_eq(pdd const& p) /* const */;
|
signed_constraint find_eq(pdd const& p) const;
|
||||||
|
signed_constraint find_ule(pdd const& a, pdd const& b) const;
|
||||||
|
|
||||||
signed_constraint eq(pdd const& p);
|
signed_constraint eq(pdd const& p);
|
||||||
signed_constraint ule(pdd const& a, pdd const& b);
|
signed_constraint ule(pdd const& a, pdd const& b);
|
||||||
|
|
|
@ -25,8 +25,8 @@ Additional possible functionality on constraints:
|
||||||
|
|
||||||
namespace polysat {
|
namespace polysat {
|
||||||
|
|
||||||
op_constraint::op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r) :
|
op_constraint::op_constraint(code c, pdd const& p, pdd const& q, pdd const& r) :
|
||||||
constraint(m, ckind_t::op_t), m_op(c), m_p(p), m_q(q), m_r(r) {
|
constraint(ckind_t::op_t), m_op(c), m_p(p), m_q(q), m_r(r) {
|
||||||
m_vars.append(p.free_vars());
|
m_vars.append(p.free_vars());
|
||||||
for (auto v : q.free_vars())
|
for (auto v : q.free_vars())
|
||||||
if (!m_vars.contains(v))
|
if (!m_vars.contains(v))
|
||||||
|
|
|
@ -35,7 +35,7 @@ namespace polysat {
|
||||||
pdd m_q;
|
pdd m_q;
|
||||||
pdd m_r;
|
pdd m_r;
|
||||||
|
|
||||||
op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r);
|
op_constraint(code c, pdd const& p, pdd const& q, pdd const& r);
|
||||||
lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
|
lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
|
||||||
clause_ref produce_lemma(solver& s, assignment const& a);
|
clause_ref produce_lemma(solver& s, assignment const& a);
|
||||||
|
|
||||||
|
|
|
@ -15,8 +15,8 @@ Author:
|
||||||
|
|
||||||
namespace polysat {
|
namespace polysat {
|
||||||
|
|
||||||
smul_fl_constraint::smul_fl_constraint(constraint_manager& m, pdd const& p, pdd const& q, bool is_overflow):
|
smul_fl_constraint::smul_fl_constraint(pdd const& p, pdd const& q, bool is_overflow):
|
||||||
constraint(m, ckind_t::smul_fl_t), m_is_overflow(is_overflow), m_p(p), m_q(q) {
|
constraint(ckind_t::smul_fl_t), m_is_overflow(is_overflow), m_p(p), m_q(q) {
|
||||||
simplify();
|
simplify();
|
||||||
m_vars.append(m_p.free_vars());
|
m_vars.append(m_p.free_vars());
|
||||||
for (auto v : m_q.free_vars())
|
for (auto v : m_q.free_vars())
|
||||||
|
|
|
@ -25,7 +25,7 @@ namespace polysat {
|
||||||
pdd m_q;
|
pdd m_q;
|
||||||
|
|
||||||
void simplify();
|
void simplify();
|
||||||
smul_fl_constraint(constraint_manager& m, pdd const& p, pdd const& q, bool is_overflow);
|
smul_fl_constraint(pdd const& p, pdd const& q, bool is_overflow);
|
||||||
|
|
||||||
public:
|
public:
|
||||||
~smul_fl_constraint() override {}
|
~smul_fl_constraint() override {}
|
||||||
|
|
|
@ -135,8 +135,8 @@ namespace {
|
||||||
|
|
||||||
namespace polysat {
|
namespace polysat {
|
||||||
|
|
||||||
ule_constraint::ule_constraint(constraint_manager& m, pdd const& l, pdd const& r) :
|
ule_constraint::ule_constraint(pdd const& l, pdd const& r) :
|
||||||
constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
|
constraint(ckind_t::ule_t), m_lhs(l), m_rhs(r) {
|
||||||
|
|
||||||
m_vars.append(m_lhs.free_vars());
|
m_vars.append(m_lhs.free_vars());
|
||||||
for (auto v : m_rhs.free_vars())
|
for (auto v : m_rhs.free_vars())
|
||||||
|
|
|
@ -25,7 +25,7 @@ namespace polysat {
|
||||||
pdd m_lhs;
|
pdd m_lhs;
|
||||||
pdd m_rhs;
|
pdd m_rhs;
|
||||||
|
|
||||||
ule_constraint(constraint_manager& m, pdd const& l, pdd const& r);
|
ule_constraint(pdd const& l, pdd const& r);
|
||||||
static void simplify(bool& is_positive, pdd& lhs, pdd& rhs);
|
static void simplify(bool& is_positive, pdd& lhs, pdd& rhs);
|
||||||
static bool is_always_true(bool is_positive, pdd const& lhs, pdd const& rhs) { return eval(lhs, rhs) == to_lbool(is_positive); }
|
static bool is_always_true(bool is_positive, pdd const& lhs, pdd const& rhs) { return eval(lhs, rhs) == to_lbool(is_positive); }
|
||||||
static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { return is_always_true(!is_positive, lhs, rhs); }
|
static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { return is_always_true(!is_positive, lhs, rhs); }
|
||||||
|
|
|
@ -15,8 +15,8 @@ Author:
|
||||||
|
|
||||||
namespace polysat {
|
namespace polysat {
|
||||||
|
|
||||||
umul_ovfl_constraint::umul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q):
|
umul_ovfl_constraint::umul_ovfl_constraint(pdd const& p, pdd const& q):
|
||||||
constraint(m, ckind_t::umul_ovfl_t), m_p(p), m_q(q) {
|
constraint(ckind_t::umul_ovfl_t), m_p(p), m_q(q) {
|
||||||
simplify();
|
simplify();
|
||||||
m_vars.append(m_p.free_vars());
|
m_vars.append(m_p.free_vars());
|
||||||
for (auto v : m_q.free_vars())
|
for (auto v : m_q.free_vars())
|
||||||
|
|
|
@ -23,7 +23,7 @@ namespace polysat {
|
||||||
pdd m_p;
|
pdd m_p;
|
||||||
pdd m_q;
|
pdd m_q;
|
||||||
|
|
||||||
umul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q);
|
umul_ovfl_constraint(pdd const& p, pdd const& q);
|
||||||
void simplify();
|
void simplify();
|
||||||
static bool is_always_true(bool is_positive, pdd const& p, pdd const& q) { return eval(p, q) == to_lbool(is_positive); }
|
static bool is_always_true(bool is_positive, pdd const& p, pdd const& q) { return eval(p, q) == to_lbool(is_positive); }
|
||||||
static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); }
|
static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); }
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue