mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
This commit is contained in:
parent
1173c93150
commit
f333d78f01
|
@ -656,6 +656,7 @@ namespace sat {
|
|||
s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
|
||||
if (s.inconsistent())
|
||||
return;
|
||||
m_use_list.reserve(s.num_vars());
|
||||
unsigned new_trail_sz = s.m_trail.size();
|
||||
for (unsigned i = old_trail_sz; i < new_trail_sz; i++) {
|
||||
literal l = s.m_trail[i];
|
||||
|
|
|
@ -40,15 +40,17 @@ namespace sat {
|
|||
|
||||
class use_list {
|
||||
vector<clause_use_list> m_use_list;
|
||||
|
||||
public:
|
||||
void init(unsigned num_vars);
|
||||
void reserve(unsigned num_vars) { while (m_use_list.size() <= 2*num_vars) m_use_list.push_back(clause_use_list()); }
|
||||
void insert(clause & c);
|
||||
void block(clause & c);
|
||||
void unblock(clause & c);
|
||||
void erase(clause & c);
|
||||
void erase(clause & c, literal l);
|
||||
clause_use_list & get(literal l) { return m_use_list[l.index()]; }
|
||||
clause_use_list const & get(literal l) const { return m_use_list[l.index()]; }
|
||||
clause_use_list& get(literal l) { return m_use_list[l.index()]; }
|
||||
clause_use_list const& get(literal l) const { return m_use_list[l.index()]; }
|
||||
void finalize() { m_use_list.finalize(); }
|
||||
std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); }
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue