mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
updates and fixes to copying and cardinalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
6caef86738
commit
fb84ba8c34
5 changed files with 144 additions and 128 deletions
|
|
@ -202,8 +202,7 @@ namespace sat {
|
|||
for (unsigned i = 0; i < p.size(); ++i) {
|
||||
wlits.push_back(p[i]);
|
||||
}
|
||||
bool_var v = p.lit() == null_literal ? null_bool_var : p.lit().var();
|
||||
result.add_pb_ge(v, wlits, p.k());
|
||||
result.add_pb_ge(p.lit(), wlits, p.k());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -439,21 +438,18 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::display(std::ostream& out, pb const& p, bool values) const {
|
||||
if (p.lit() != null_literal) out << p.lit();
|
||||
out << "[watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
|
||||
if (p.lit() != null_literal) out << p.lit() << " == ";
|
||||
if (p.lit() != null_literal && values) {
|
||||
out << "[watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
|
||||
out << "@(" << value(p.lit());
|
||||
if (value(p.lit()) != l_undef) {
|
||||
out << ":" << lvl(p.lit());
|
||||
}
|
||||
out << "): ";
|
||||
}
|
||||
else {
|
||||
out << ": ";
|
||||
}
|
||||
for (unsigned i = 0; i < p.size(); ++i) {
|
||||
literal l = p[i].second;
|
||||
unsigned w = p[i].first;
|
||||
for (wliteral wl : p) {
|
||||
literal l = wl.second;
|
||||
unsigned w = wl.first;
|
||||
if (w > 1) out << w << " * ";
|
||||
out << l;
|
||||
if (values) {
|
||||
|
|
@ -476,11 +472,10 @@ namespace sat {
|
|||
for (unsigned i = 0; i < m_xors.size(); ++i) {
|
||||
literal_vector lits;
|
||||
xor& x = *m_xors[i];
|
||||
for (unsigned i = 0; i < x.size(); ++i) {
|
||||
lits.push_back(x[i]);
|
||||
for (literal l : x) {
|
||||
lits.push_back(l);
|
||||
}
|
||||
bool_var v = x.lit() == null_literal ? null_bool_var : x.lit().var();
|
||||
result.add_xor(v, lits);
|
||||
result.add_xor(x.lit(), lits);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1011,53 +1006,63 @@ namespace sat {
|
|||
m_stats.reset();
|
||||
}
|
||||
|
||||
void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
|
||||
void card_extension::add_at_least(literal lit, literal_vector const& lits, unsigned k) {
|
||||
unsigned index = 4*m_cards.size();
|
||||
SASSERT(is_card_index(index));
|
||||
literal lit = v == null_bool_var ? null_literal : literal(v, false);
|
||||
card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
|
||||
m_cards.push_back(c);
|
||||
if (v == null_bool_var) {
|
||||
if (lit == null_literal) {
|
||||
// it is an axiom.
|
||||
init_watch(*c, true);
|
||||
m_card_axioms.push_back(c);
|
||||
}
|
||||
else {
|
||||
get_wlist(literal(v, false)).push_back(index);
|
||||
get_wlist(literal(v, true)).push_back(index);
|
||||
get_wlist(lit).push_back(index);
|
||||
get_wlist(~lit).push_back(index);
|
||||
m_index_trail.push_back(index);
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
|
||||
literal lit = v == null_bool_var ? null_literal : literal(v, false);
|
||||
add_at_least(lit, lits, k);
|
||||
}
|
||||
|
||||
void card_extension::add_pb_ge(literal lit, svector<wliteral> const& wlits, unsigned k) {
|
||||
unsigned index = 4*m_pbs.size() + 0x3;
|
||||
SASSERT(is_pb_index(index));
|
||||
pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
|
||||
m_pbs.push_back(p);
|
||||
if (lit == null_literal) {
|
||||
init_watch(*p, true);
|
||||
m_pb_axioms.push_back(p);
|
||||
}
|
||||
else {
|
||||
get_wlist(lit).push_back(index);
|
||||
get_wlist(~lit).push_back(index);
|
||||
m_index_trail.push_back(index);
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k) {
|
||||
unsigned index = 4*m_pbs.size() + 0x3;
|
||||
SASSERT(is_pb_index(index));
|
||||
literal lit = v == null_bool_var ? null_literal : literal(v, false);
|
||||
pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
|
||||
m_pbs.push_back(p);
|
||||
if (v == null_bool_var) {
|
||||
init_watch(*p, true);
|
||||
m_pb_axioms.push_back(p);
|
||||
}
|
||||
else {
|
||||
get_wlist(literal(v, false)).push_back(index);
|
||||
get_wlist(literal(v, true)).push_back(index);
|
||||
m_index_trail.push_back(index);
|
||||
}
|
||||
add_pb_ge(lit, wlits, k);
|
||||
}
|
||||
|
||||
|
||||
void card_extension::add_xor(bool_var v, literal_vector const& lits) {
|
||||
unsigned index = 4*m_xors.size() + 0x1;
|
||||
SASSERT(is_xor_index(index));
|
||||
SASSERT(v != null_bool_var);
|
||||
xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, literal(v, false), lits);
|
||||
m_xors.push_back(x);
|
||||
get_wlist(literal(v, false)).push_back(index);
|
||||
get_wlist(literal(v, true)).push_back(index);
|
||||
m_index_trail.push_back(index);
|
||||
add_xor(literal(v, false), lits);
|
||||
}
|
||||
|
||||
void card_extension::add_xor(literal lit, literal_vector const& lits) {
|
||||
unsigned index = 4*m_xors.size() + 0x1;
|
||||
SASSERT(is_xor_index(index));
|
||||
xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, lit, lits);
|
||||
m_xors.push_back(x);
|
||||
get_wlist(lit).push_back(index);
|
||||
get_wlist(~lit).push_back(index);
|
||||
m_index_trail.push_back(index);
|
||||
}
|
||||
|
||||
void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) {
|
||||
SASSERT(value(l) == l_true);
|
||||
|
|
@ -1412,18 +1417,20 @@ namespace sat {
|
|||
void card_extension::clauses_modifed() {}
|
||||
lbool card_extension::get_phase(bool_var v) { return l_undef; }
|
||||
|
||||
extension* card_extension::copy(solver* s) {
|
||||
card_extension* result = alloc(card_extension);
|
||||
result->set_solver(s);
|
||||
void card_extension::copy_card(card_extension& result) {
|
||||
for (unsigned i = 0; i < m_cards.size(); ++i) {
|
||||
literal_vector lits;
|
||||
card& c = *m_cards[i];
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
lits.push_back(c[i]);
|
||||
}
|
||||
bool_var v = c.lit() == null_literal ? null_bool_var : c.lit().var();
|
||||
result->add_at_least(v, lits, c.k());
|
||||
result.add_at_least(c.lit(), lits, c.k());
|
||||
}
|
||||
}
|
||||
extension* card_extension::copy(solver* s) {
|
||||
card_extension* result = alloc(card_extension);
|
||||
result->set_solver(s);
|
||||
copy_card(*result);
|
||||
copy_xor(*result);
|
||||
copy_pb(*result);
|
||||
return result;
|
||||
|
|
@ -1498,16 +1505,18 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::display(std::ostream& out, card const& c, bool values) const {
|
||||
out << c.lit() << "[" << c.size() << "]";
|
||||
if (c.lit() != null_literal && values) {
|
||||
out << "@(" << value(c.lit());
|
||||
if (value(c.lit()) != l_undef) {
|
||||
out << ":" << lvl(c.lit());
|
||||
if (c.lit() != null_literal) {
|
||||
if (values) {
|
||||
out << c.lit() << "[" << c.size() << "]";
|
||||
out << "@(" << value(c.lit());
|
||||
if (value(c.lit()) != l_undef) {
|
||||
out << ":" << lvl(c.lit());
|
||||
}
|
||||
out << "): ";
|
||||
}
|
||||
else {
|
||||
out << c.lit() << " == ";
|
||||
}
|
||||
out << "): ";
|
||||
}
|
||||
else {
|
||||
out << ": ";
|
||||
}
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
literal l = c[i];
|
||||
|
|
@ -1527,6 +1536,15 @@ namespace sat {
|
|||
}
|
||||
|
||||
std::ostream& card_extension::display(std::ostream& out) const {
|
||||
for (card* c : m_cards) {
|
||||
display(out, *c, false);
|
||||
}
|
||||
for (pb* p : m_pbs) {
|
||||
display(out, *p, false);
|
||||
}
|
||||
for (xor* x : m_xors) {
|
||||
display(out, *x, false);
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -108,6 +108,8 @@ namespace sat {
|
|||
literal lit() const { return m_lit; }
|
||||
literal operator[](unsigned i) const { return m_lits[i]; }
|
||||
unsigned size() const { return m_size; }
|
||||
literal const* begin() const { return m_lits; }
|
||||
literal const* end() const { return (literal const*)m_lits + m_size; }
|
||||
void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
|
||||
void negate() { m_lits[0].neg(); }
|
||||
};
|
||||
|
|
@ -167,7 +169,7 @@ namespace sat {
|
|||
void reset_marked_literals();
|
||||
void unwatch_literal(literal w, card& c);
|
||||
void get_card_antecedents(literal l, card const& c, literal_vector & r);
|
||||
|
||||
void copy_card(card_extension& result);
|
||||
|
||||
// xor specific functionality
|
||||
void copy_xor(card_extension& result);
|
||||
|
|
@ -244,6 +246,10 @@ namespace sat {
|
|||
void display(std::ostream& out, pb const& p, bool values) const;
|
||||
void display(std::ostream& out, xor const& c, bool values) const;
|
||||
|
||||
void add_at_least(literal l, literal_vector const& lits, unsigned k);
|
||||
void add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k);
|
||||
void add_xor(literal l, literal_vector const& lits);
|
||||
|
||||
public:
|
||||
card_extension();
|
||||
virtual ~card_extension();
|
||||
|
|
|
|||
|
|
@ -1102,11 +1102,9 @@ namespace sat {
|
|||
|
||||
unsigned simplifier::get_num_non_learned_bin(literal l) const {
|
||||
unsigned r = 0;
|
||||
watch_list const & wlist = get_wlist(~l);
|
||||
watch_list::const_iterator it = wlist.begin();
|
||||
watch_list::const_iterator end = wlist.end();
|
||||
for (; it != end; ++it) {
|
||||
if (it->is_binary_non_learned_clause())
|
||||
watch_list const & wlist = get_wlist(~l);
|
||||
for (auto & w : wlist) {
|
||||
if (w.is_binary_non_learned_clause())
|
||||
r++;
|
||||
}
|
||||
return r;
|
||||
|
|
@ -1133,10 +1131,7 @@ namespace sat {
|
|||
|
||||
void simplifier::order_vars_for_elim(bool_var_vector & r) {
|
||||
svector<bool_var_and_cost> tmp;
|
||||
bool_var_set::iterator it = m_elim_todo.begin();
|
||||
bool_var_set::iterator end = m_elim_todo.end();
|
||||
for (; it != end; ++it) {
|
||||
bool_var v = *it;
|
||||
for (bool_var v : m_elim_todo) {
|
||||
if (is_external(v))
|
||||
continue;
|
||||
if (was_eliminated(v))
|
||||
|
|
@ -1149,17 +1144,10 @@ namespace sat {
|
|||
m_elim_todo.reset();
|
||||
std::stable_sort(tmp.begin(), tmp.end(), bool_var_and_cost_lt());
|
||||
TRACE("elim_vars",
|
||||
svector<bool_var_and_cost>::iterator it = tmp.begin();
|
||||
svector<bool_var_and_cost>::iterator end = tmp.end();
|
||||
for (; it != end; ++it) {
|
||||
tout << "(" << it->first << ", " << it->second << ") ";
|
||||
}
|
||||
for (auto& p : tmp) tout << "(" << p.first << ", " << p.second << ") ";
|
||||
tout << "\n";);
|
||||
svector<bool_var_and_cost>::iterator it2 = tmp.begin();
|
||||
svector<bool_var_and_cost>::iterator end2 = tmp.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
r.push_back(it2->first);
|
||||
}
|
||||
for (auto& p : tmp)
|
||||
r.push_back(p.first);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -1175,11 +1163,9 @@ namespace sat {
|
|||
}
|
||||
|
||||
watch_list & wlist = get_wlist(~l);
|
||||
watch_list::iterator it2 = wlist.begin();
|
||||
watch_list::iterator end2 = wlist.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
if (it2->is_binary_non_learned_clause()) {
|
||||
r.push_back(clause_wrapper(l, it2->get_literal()));
|
||||
for (auto & w : wlist) {
|
||||
if (w.is_binary_non_learned_clause()) {
|
||||
r.push_back(clause_wrapper(l, w.get_literal()));
|
||||
SASSERT(r.back().size() == 2);
|
||||
}
|
||||
}
|
||||
|
|
@ -1199,7 +1185,7 @@ namespace sat {
|
|||
bool res = true;
|
||||
unsigned sz = c1.size();
|
||||
m_elim_counter -= sz;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal l2 = c1[i];
|
||||
if (l == l2)
|
||||
continue;
|
||||
|
|
@ -1210,7 +1196,7 @@ namespace sat {
|
|||
literal not_l = ~l;
|
||||
sz = c2.size();
|
||||
m_elim_counter -= sz;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal l2 = c2[i];
|
||||
if (not_l == l2)
|
||||
continue;
|
||||
|
|
@ -1223,7 +1209,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
sz = c1.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal l2 = c1[i];
|
||||
if (l == l2)
|
||||
continue;
|
||||
|
|
@ -1234,10 +1220,9 @@ namespace sat {
|
|||
|
||||
void simplifier::save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs) {
|
||||
model_converter & mc = s.m_mc;
|
||||
clause_wrapper_vector::const_iterator it = cs.begin();
|
||||
clause_wrapper_vector::const_iterator end = cs.end();
|
||||
for (; it != end; ++it)
|
||||
mc.insert(mc_entry, *it);
|
||||
for (auto & e : cs) {
|
||||
mc.insert(mc_entry, e);
|
||||
}
|
||||
}
|
||||
|
||||
void simplifier::add_non_learned_binary_clause(literal l1, literal l2) {
|
||||
|
|
@ -1273,11 +1258,9 @@ namespace sat {
|
|||
*/
|
||||
void simplifier::remove_bin_clauses(literal l) {
|
||||
watch_list & wlist = get_wlist(~l);
|
||||
watch_list::iterator it = wlist.begin();
|
||||
watch_list::iterator end = wlist.end();
|
||||
for (; it != end; ++it) {
|
||||
if (it->is_binary_clause()) {
|
||||
literal l2 = it->get_literal();
|
||||
for (auto & w : wlist) {
|
||||
if (w.is_binary_clause()) {
|
||||
literal l2 = w.get_literal();
|
||||
watch_list & wlist2 = get_wlist(~l2);
|
||||
watch_list::iterator it2 = wlist2.begin();
|
||||
watch_list::iterator itprev = it2;
|
||||
|
|
@ -1292,7 +1275,7 @@ namespace sat {
|
|||
itprev++;
|
||||
}
|
||||
wlist2.set_end(itprev);
|
||||
m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned()));
|
||||
m_sub_bin_todo.erase(bin_clause(l, l2, w.is_learned()));
|
||||
}
|
||||
}
|
||||
TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";);
|
||||
|
|
@ -1484,13 +1467,10 @@ namespace sat {
|
|||
bool_var_vector vars;
|
||||
order_vars_for_elim(vars);
|
||||
|
||||
bool_var_vector::iterator it = vars.begin();
|
||||
bool_var_vector::iterator end = vars.end();
|
||||
for (; it != end; ++it) {
|
||||
for (bool_var v : vars) {
|
||||
checkpoint();
|
||||
if (m_elim_counter < 0)
|
||||
return;
|
||||
bool_var v = *it;
|
||||
if (try_eliminate(v)) {
|
||||
m_num_elim_vars++;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -96,6 +96,9 @@ namespace sat {
|
|||
if (src.was_eliminated(v)) {
|
||||
m_eliminated[v] = true;
|
||||
}
|
||||
m_phase[v] = src.m_phase[v];
|
||||
m_prev_phase[v] = src.m_prev_phase[v];
|
||||
// m_activity[v] = src.m_activity[v], but then update case_split_queue ?
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -117,14 +120,14 @@ namespace sat {
|
|||
unsigned sz = src.m_watches.size();
|
||||
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
|
||||
literal l = ~to_literal(l_idx);
|
||||
if (src.was_eliminated(l.var())) continue;
|
||||
watch_list const & wlist = src.m_watches[l_idx];
|
||||
watch_list::const_iterator it = wlist.begin();
|
||||
watch_list::const_iterator end = wlist.end();
|
||||
for (; it != end; ++it) {
|
||||
if (!it->is_binary_non_learned_clause())
|
||||
for (auto & wi : wlist) {
|
||||
if (!wi.is_binary_non_learned_clause())
|
||||
continue;
|
||||
literal l2 = it->get_literal();
|
||||
if (l.index() > l2.index())
|
||||
literal l2 = wi.get_literal();
|
||||
if (l.index() > l2.index() ||
|
||||
src.was_eliminated(l2.var()))
|
||||
continue;
|
||||
mk_clause_core(l, l2);
|
||||
}
|
||||
|
|
@ -133,16 +136,24 @@ namespace sat {
|
|||
|
||||
{
|
||||
literal_vector buffer;
|
||||
// copy clause
|
||||
clause_vector::const_iterator it = src.m_clauses.begin();
|
||||
clause_vector::const_iterator end = src.m_clauses.end();
|
||||
for (; it != end; ++it) {
|
||||
clause const & c = *(*it);
|
||||
// copy clauses
|
||||
for (clause* c : src.m_clauses) {
|
||||
buffer.reset();
|
||||
for (unsigned i = 0; i < c.size(); i++)
|
||||
buffer.push_back(c[i]);
|
||||
for (literal l : *c) buffer.push_back(l);
|
||||
mk_clause_core(buffer);
|
||||
}
|
||||
// copy high quality lemmas
|
||||
for (clause* c : src.m_learned) {
|
||||
if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) {
|
||||
buffer.reset();
|
||||
for (literal l : *c) buffer.push_back(l);
|
||||
clause* c1 = mk_clause_core(buffer.size(), buffer.c_ptr(), true);
|
||||
if (c1) {
|
||||
c1->set_glue(c->glue());
|
||||
c1->set_psm(c->psm());
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
m_user_scope_literals.reset();
|
||||
|
|
|
|||
|
|
@ -45,7 +45,6 @@ class inc_sat_solver : public solver {
|
|||
sat::solver m_solver;
|
||||
goal2sat m_goal2sat;
|
||||
params_ref m_params;
|
||||
bool m_optimize_model; // parameter
|
||||
expr_ref_vector m_fmls;
|
||||
expr_ref_vector m_asmsf;
|
||||
unsigned_vector m_fmls_lim;
|
||||
|
|
@ -77,7 +76,7 @@ public:
|
|||
inc_sat_solver(ast_manager& m, params_ref const& p):
|
||||
m(m),
|
||||
m_solver(p, m.limit()),
|
||||
m_params(p), m_optimize_model(false),
|
||||
m_params(p),
|
||||
m_fmls(m),
|
||||
m_asmsf(m),
|
||||
m_fmls_head(0),
|
||||
|
|
@ -96,20 +95,24 @@ public:
|
|||
virtual ~inc_sat_solver() {}
|
||||
|
||||
virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
|
||||
ast_translation tr(m, dst_m);
|
||||
if (m_num_scopes > 0) {
|
||||
throw default_exception("Cannot translate sat solver at non-base level");
|
||||
}
|
||||
ast_translation tr(m, dst_m);
|
||||
m_solver.pop_to_base_level();
|
||||
inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p);
|
||||
expr_ref fml(dst_m);
|
||||
for (unsigned i = 0; i < m_fmls.size(); ++i) {
|
||||
fml = tr(m_fmls[i].get());
|
||||
result->m_fmls.push_back(fml);
|
||||
}
|
||||
for (unsigned i = 0; i < m_asmsf.size(); ++i) {
|
||||
fml = tr(m_asmsf[i].get());
|
||||
result->m_asmsf.push_back(fml);
|
||||
}
|
||||
result->m_solver.copy(m_solver);
|
||||
result->m_fmls_head = m_fmls_head;
|
||||
for (expr* f : m_fmls) result->m_fmls.push_back(tr(f));
|
||||
for (expr* f : m_asmsf) result->m_asmsf.push_back(tr(f));
|
||||
for (auto & kv : m_map) result->m_map.insert(tr(kv.m_key), kv.m_value);
|
||||
for (unsigned l : m_fmls_lim) result->m_fmls_lim.push_back(l);
|
||||
for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
|
||||
for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
|
||||
for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
|
||||
if (m_mc0.get()) result->m_mc0 = m_mc0->translate(tr);
|
||||
result->m_internalized = m_internalized;
|
||||
result->m_internalized_converted = m_internalized_converted;
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
@ -272,7 +275,6 @@ public:
|
|||
m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
|
||||
m_params.set_bool("xor_solver", p1.xor_solver());
|
||||
m_solver.updt_params(m_params);
|
||||
m_optimize_model = m_params.get_bool("optimize_model", false);
|
||||
|
||||
}
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
|
|
@ -383,9 +385,9 @@ public:
|
|||
// extract original fixed variables
|
||||
u_map<expr*> asm2dep;
|
||||
extract_asm2dep(dep2asm, asm2dep);
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
for (auto v : vars) {
|
||||
expr_ref cons(m);
|
||||
if (extract_fixed_variable(dep2asm, asm2dep, vars[i], bool_var2conseq, lconseq, cons)) {
|
||||
if (extract_fixed_variable(dep2asm, asm2dep, v, bool_var2conseq, lconseq, cons)) {
|
||||
conseq.push_back(cons);
|
||||
}
|
||||
}
|
||||
|
|
@ -407,11 +409,10 @@ public:
|
|||
}
|
||||
vector<sat::literal_vector> ls_mutexes;
|
||||
m_solver.find_mutexes(ls, ls_mutexes);
|
||||
for (unsigned i = 0; i < ls_mutexes.size(); ++i) {
|
||||
sat::literal_vector const ls_mutex = ls_mutexes[i];
|
||||
for (sat::literal_vector const& ls_mutex : ls_mutexes) {
|
||||
expr_ref_vector mutex(m);
|
||||
for (unsigned j = 0; j < ls_mutex.size(); ++j) {
|
||||
mutex.push_back(lit2var.find(ls_mutex[j].index()));
|
||||
for (sat::literal l : ls_mutex) {
|
||||
mutex.push_back(lit2var.find(l.index()));
|
||||
}
|
||||
mutexes.push_back(mutex);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue