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

add code review and replacement for mk_int

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-17 14:19:17 -07:00
parent 572197aede
commit 4b35c75712
4 changed files with 38 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/math/dd/dd_bdd.cpp
View file

@ -896,6 +896,9 @@ namespace dd {
std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); }
// NSB code review:
// this function should be removed and replaced by functionality where the
// client maintains what are the variables.
bdd bdd_manager::mk_int(rational const& val, unsigned w) {
bdd b = mk_true();
for (unsigned k = w; k-- > 0;)
@ -981,6 +984,22 @@ namespace dd {
return eq;
}
bdd bdd_manager::mk_eq(bddv const& a, rational const& n) {
SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(a.size()));
bdd b = mk_true();
for (unsigned i = a.size(); i-- > 0; )
b &= n.get_bit(i) ? a[i] : !a[i];
return b;
}
bdd bdd_manager::mk_eq(unsigned_vector const& vars, rational const& n) {
SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(vars.size()));
bdd b = mk_true();
for (unsigned i = vars.size(); i-- > 0; )
b &= n.get_bit(i) ? mk_var(vars[i]) : mk_nvar(vars[i]);
return b;
}
bdd bdd_manager::mk_ule(bddv const& a, bddv const& b) {
SASSERT(a.size() == b.size());
bdd lt = mk_false();

2
src/math/dd/dd_bdd.h
View file

@ -236,6 +236,8 @@ namespace dd {
bdd mk_slt(bddv const& a, bddv const& b); // { return mk_sle(a, b) && !mk_eq(a, b); }
bdd mk_sgt(bddv const& a, bddv const& b); // { return mk_slt(b, a); }
bdd mk_eq(bddv const& a, bddv const& b);
bdd mk_eq(bddv const& a, rational const& v);
bdd mk_eq(unsigned_vector const& vars, rational const& v);
bddv mk_num(rational const& n, unsigned num_bits);
bddv mk_ones(unsigned num_bits);
bddv mk_zero(unsigned num_bits);

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

@ -24,11 +24,23 @@ namespace polysat {
dd::pdd_manager& solver::sz2pdd(unsigned sz) {
m_pdd.reserve(sz + 1);
if (!m_pdd[sz])
if (!m_pdd[sz])
m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz));
return *m_pdd[sz];
}
vector<bdd>& solver::sz2bits(unsigned sz) {
m_bits.reserve(sz + 1);
auto* bits = m_bits[sz];
if (!bits) {
m_bits.set(sz, alloc(vector<bdd>));
bits = m_bits[sz];
for (unsigned i = 0; i < sz; ++i)
bits->push_back(m_bdd.mk_var(i));
}
return *bits;
}
bool solver::is_viable(pvar v, rational const& val) {
return m_viable[v].contains_int(val, size(v));
}
@ -37,7 +49,8 @@ namespace polysat {
LOG("pvar " << v << " /= " << val);
TRACE("polysat", tout << "v" << v << " /= " << val << "\n";);
SASSERT(is_viable(v, val));
intersect_viable(v, !m_bdd.mk_int(val, size(v)));
auto& bits = sz2bits(size(v));
intersect_viable(v, !m_bdd.mk_eq(bits, val));
}
void solver::intersect_viable(pvar v, bdd vals) {

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

@ -44,6 +44,7 @@ namespace polysat {
reslimit& m_lim;
scoped_ptr_vector<dd::pdd_manager> m_pdd;
scoped_ptr_vector<vector<bdd>> m_bits;
dd::bdd_manager m_bdd;
dep_value_manager m_value_manager;
small_object_allocator m_alloc;
@ -142,6 +143,7 @@ namespace polysat {
void del_var();
dd::pdd_manager& sz2pdd(unsigned sz);
vector<bdd>& sz2bits(unsigned sz);
void push_level();
void pop_levels(unsigned num_levels);