mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Move bit-wise expressions to constraint_manager

Browse source
This commit is contained in:
Jakob Rath 2022-11-07 14:00:02 +01:00
parent 7662427d92
commit a1736473a4
4 changed files with 64 additions and 73 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/math/polysat/constraint_manager.cpp
View file

@ -31,8 +31,7 @@ namespace polysat {
// map<op_constraint_args, pvar, op_constraint_args_hash, op_constraint_args_eq> op_constraint_vars;
// };
constraint_manager::constraint_manager(bool_var_manager& bvars)
: m_bvars(bvars) /*, m_dedup(alloc(constraint_dedup))*/ {}
constraint_manager::constraint_manager(solver& s): s(s) {}
void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) {
SASSERT_EQ(get_bv2c(bv), nullptr);
@ -54,7 +53,7 @@ namespace polysat {
void constraint_manager::ensure_bvar(constraint* c) {
if (!c->has_bvar())
assign_bv2c(m_bvars.new_var(), c);
assign_bv2c(s.m_bvars.new_var(), c);
}
void constraint_manager::erase_bvar(constraint* c) {
@ -101,11 +100,11 @@ namespace polysat {
bool first = true;
for (unsigned i = 0; i < cl.size(); ++i) {
if (m_bvars.is_false(cl[i]))
if (s.m_bvars.is_false(cl[i]))
continue;
signed_constraint sc = s.lit2cnstr(cl[i]);
if (value_propagate && sc.is_currently_false(s)) {
if (m_bvars.is_true(cl[i])) {
if (s.m_bvars.is_true(cl[i])) {
s.set_conflict(sc);
return;
}
@ -113,7 +112,7 @@ namespace polysat {
continue;
}
m_bvars.watch(cl[i]).push_back(&cl);
s.m_bvars.watch(cl[i]).push_back(&cl);
std::swap(cl[!first], cl[i]);
if (!first)
return;
@ -121,10 +120,10 @@ namespace polysat {
}
if (first)
m_bvars.watch(cl[0]).push_back(&cl);
s.m_bvars.watch(cl[0]).push_back(&cl);
if (cl.size() > 1)
m_bvars.watch(cl[1]).push_back(&cl);
if (m_bvars.is_true(cl[0]))
s.m_bvars.watch(cl[1]).push_back(&cl);
if (s.m_bvars.is_true(cl[0]))
return;
if (first)
s.set_conflict(cl);
@ -135,8 +134,8 @@ namespace polysat {
void constraint_manager::unwatch(clause& cl) {
if (cl.size() <= 1)
return;
m_bvars.watch(~cl[0]).erase(&cl);
m_bvars.watch(~cl[1]).erase(&cl);
s.m_bvars.watch(~cl[0]).erase(&cl);
s.m_bvars.watch(~cl[1]).erase(&cl);
}
constraint_manager::~constraint_manager() {
@ -285,4 +284,36 @@ namespace polysat {
return ult(a + shift, b + shift);
}
pdd constraint_manager::bnot(pdd const& p) {
return -p - 1;
}
pdd constraint_manager::band(pdd const& p, pdd const& q) {
auto& m = p.manager();
unsigned sz = m.power_of_2();
// TODO: return existing r if we call again with the same arguments
pdd r = m.mk_var(s.add_var(sz));
s.assign_eh(band(p, q, r), null_dependency);
return r;
}
pdd constraint_manager::bor(pdd const& p, pdd const& q) {
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
return (p + q) - band(p, q);
}
pdd constraint_manager::bxor(pdd const& p, pdd const& q) {
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
return (p + q) - 2*band(p, q);
}
pdd constraint_manager::bnand(pdd const& p, pdd const& q) {
return bnot(band(p, q));
}
pdd constraint_manager::bnor(pdd const& p, pdd const& q) {
return bnot(bor(p, q));
}
}

11
src/math/polysat/constraint_manager.h
View file

@ -36,7 +36,7 @@ namespace polysat {
class constraint_manager {
friend class constraint;
bool_var_manager& m_bvars;
solver& s;
// Constraints indexed by their boolean variable
ptr_vector<constraint> m_bv2constraint;
@ -75,7 +75,7 @@ namespace polysat {
void erase_bvar(constraint* c);
public:
constraint_manager(bool_var_manager& bvars);
constraint_manager(solver& s);
~constraint_manager();
void store(clause* cl, solver& s, bool value_propagate);
@ -102,6 +102,13 @@ namespace polysat {
signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r);
signed_constraint band(pdd const& p, pdd const& q, pdd const& r);
pdd bnot(pdd const& p);
pdd band(pdd const& p, pdd const& q);
pdd bor(pdd const& p, pdd const& q);
pdd bxor(pdd const& p, pdd const& q);
pdd bnand(pdd const& p, pdd const& q);
pdd bnor(pdd const& p, pdd const& q);
constraint* const* begin() const { return m_constraints.data(); }
constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }

37
src/math/polysat/solver.cpp
View file

@ -36,7 +36,7 @@ namespace polysat {
m_restart(*this),
m_bvars(),
m_free_pvars(m_activity),
m_constraints(m_bvars),
m_constraints(*this),
m_search(*this) {
}
@ -166,41 +166,6 @@ namespace polysat {
return r;
}
pdd solver::bnot(pdd const& p) {
return -p - 1;
}
pdd solver::band(pdd const& p, pdd const& q) {
auto& m = p.manager();
unsigned sz = m.power_of_2();
// TODO: use existing r if we call again with the same arguments
pdd r = m.mk_var(add_var(sz));
assign_eh(m_constraints.band(p, q, r), null_dependency);
return r;
}
pdd solver::bor(pdd const& p, pdd const& q) {
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
// TODO: switch to op_constraint once supported
return (p + q) - band(p, q);
}
pdd solver::bxor(pdd const& p, pdd const& q) {
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
// TODO: switch to op_constraint once supported
return (p + q) - 2*band(p, q);
}
pdd solver::bnand(pdd const& p, pdd const& q) {
return bnot(band(p, q));
}
pdd solver::bnor(pdd const& p, pdd const& q) {
return bnot(bor(p, q));
}
void solver::assign_eh(signed_constraint c, dependency dep) {
backjump(base_level());
SASSERT(at_base_level());

36
src/math/polysat/solver.h
View file

@ -312,35 +312,23 @@ namespace polysat {
*/
pdd lshr(pdd const& p, pdd const& q);
/**
* Create expression for the bit-wise negation of p.
*/
pdd bnot(pdd const& p);
/** Create expression for the bit-wise negation of p. */
pdd bnot(pdd const& p) { return m_constraints.bnot(p); }
/**
* Create expression for bit-wise and of p, q.
*/
pdd band(pdd const& p, pdd const& q);
/** Create expression for bit-wise and of p, q. */
pdd band(pdd const& p, pdd const& q) { return m_constraints.band(p, q); }
/**
* Create expression for bit-wise or of p, q.
*/
pdd bor(pdd const& p, pdd const& q);
/** Create expression for bit-wise or of p, q. */
pdd bor(pdd const& p, pdd const& q) { return m_constraints.bor(p, q); }
/**
* Create expression for bit-wise xor of p, q.
*/
pdd bxor(pdd const& p, pdd const& q);
/** Create expression for bit-wise xor of p, q. */
pdd bxor(pdd const& p, pdd const& q) { return m_constraints.bxor(p, q); }
/**
* Create expression for bit-wise nand of p, q.
*/
pdd bnand(pdd const& p, pdd const& q);
/** Create expression for bit-wise nand of p, q. */
pdd bnand(pdd const& p, pdd const& q) { return m_constraints.bnand(p, q); }
/**
* Create expression for bit-wise nor of p, q.
*/
pdd bnor(pdd const& p, pdd const& q);
/** Create expression for bit-wise nor of p, q. */
pdd bnor(pdd const& p, pdd const& q) { return m_constraints.bnor(p, q); }
/**
* Create polynomial constant.