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

unit optimization

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-09-28 20:01:33 -07:00
parent 15f6124fbd
commit ef6542823b
2 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/sat_dual_solver.cpp
View file

@ -26,17 +26,20 @@ namespace sat {
m_solver.user_push();
m_roots_lim.push_back(m_roots.size());
m_tracked_lim.push_back(m_tracked_stack.size());
m_units_lim.push_back(m_units.size());
}
void dual_solver::pop(unsigned num_scopes) {
m_solver.user_pop(num_scopes);
unsigned old_sz = m_roots_lim.size() - num_scopes;
m_roots.shrink(m_roots_lim[old_sz]);
m_roots_lim.shrink(old_sz);
for (unsigned v = m_tracked_stack.size(); v-- > m_tracked_lim[old_sz]; )
m_is_tracked[v] = false;
m_roots.shrink(m_roots_lim[old_sz]);
m_tracked_stack.shrink(m_tracked_lim[old_sz]);
m_units.shrink(m_units_lim[old_sz]);
m_roots_lim.shrink(old_sz);
m_tracked_lim.shrink(old_sz);
m_units_lim.shrink(old_sz);
}
bool_var dual_solver::ext2var(bool_var v) {
@ -87,6 +90,7 @@ namespace sat {
m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
lbool is_sat = m_solver.check(m_lits.size(), m_lits.c_ptr());
m_core.reset();
m_core.append(m_units);
if (is_sat == l_false)
for (literal lit : m_solver.get_core())
m_core.push_back(lit2ext(lit));

4
src/sat/smt/sat_dual_solver.h
View file

@ -21,12 +21,12 @@ namespace sat {
class dual_solver {
solver m_solver;
literal_vector m_roots, m_lits, m_core;
literal_vector m_roots, m_lits, m_core, m_units;
bool_var_vector m_is_tracked;
unsigned_vector m_tracked_stack;
unsigned_vector m_ext2var;
unsigned_vector m_var2ext;
unsigned_vector m_roots_lim, m_tracked_lim;
unsigned_vector m_roots_lim, m_tracked_lim, m_units_lim;
void add_literal(literal lit);
bool_var ext2var(bool_var v);