mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

cleanup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-06-14 18:45:16 -07:00
parent 7fbe7124f9
commit ef62a52fff
1 changed files with 1 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/opt/weighted_maxsat.cpp
View file

@ -1042,8 +1042,7 @@ namespace opt {
uint_set indices;
unsigned_vector c_indices;
for (unsigned i = 0; i < m_asms.size(); ++i) {
unsigned index = m_aux2index.find(m_asms[i]);
indices.insert(index);
indices.insert(m_aux2index.find(m_asms[i]));
}
for (unsigned i = 0; i < num_soft(); ++i) {
if (!indices.contains(i)) {
@ -1064,7 +1063,6 @@ namespace opt {
m_hs.add_exists_true(indices.size(), indices.c_ptr());
}
void update_index(obj_map<expr, unsigned>& asm2index) {
obj_map<expr, unsigned>::iterator it = asm2index.begin(), end = asm2index.end();
for (; it != end; ++it) {
@ -1082,20 +1080,12 @@ namespace opt {
return r;
}
bool is_true(model_ref& mdl, expr* e) {
expr_ref val(m);
VERIFY(mdl->eval(e, val));
return m.is_true(val);
}
bool is_one(model_ref& mdl, expr* e) {
rational r;
expr_ref val(m);
VERIFY(mdl->eval(e, val));
return a.is_numeral(val, r) && r.is_one();
}
bool is_active(unsigned i) const {
return m_aux_active[i];
}