mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fixes for input4/5 #2416
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
06ee09a113
commit
2bd8d3b485
|
@ -3159,14 +3159,18 @@ namespace sat {
|
|||
// -------------------------------
|
||||
// set literals equivalent
|
||||
|
||||
bool ba_solver::set_root(literal l, literal r) {
|
||||
if (s().is_assumption(l.var())) {
|
||||
return false;
|
||||
}
|
||||
void ba_solver::reserve_roots() {
|
||||
m_root_vars.reserve(s().num_vars(), false);
|
||||
for (unsigned i = m_roots.size(); i < 2 * s().num_vars(); ++i) {
|
||||
m_roots.push_back(to_literal(i));
|
||||
}
|
||||
}
|
||||
|
||||
bool ba_solver::set_root(literal l, literal r) {
|
||||
if (s().is_assumption(l.var())) {
|
||||
return false;
|
||||
}
|
||||
reserve_roots();
|
||||
m_roots[l.index()] = r;
|
||||
m_roots[(~l).index()] = ~r;
|
||||
m_root_vars[l.var()] = true;
|
||||
|
@ -3175,7 +3179,7 @@ namespace sat {
|
|||
|
||||
void ba_solver::flush_roots() {
|
||||
if (m_roots.empty()) return;
|
||||
|
||||
reserve_roots();
|
||||
// validate();
|
||||
m_visited.resize(s().num_vars()*2, false);
|
||||
m_constraint_removed = false;
|
||||
|
|
|
@ -328,6 +328,7 @@ namespace sat {
|
|||
void update_psm(constraint& c) const;
|
||||
void mutex_reduction();
|
||||
void update_pure();
|
||||
void reserve_roots();
|
||||
|
||||
unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); }
|
||||
|
||||
|
|
Loading…
Reference in a new issue