mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

#5223

Browse source 
unreachable code in dual solver
This commit is contained in:
Nikolaj Bjorner 2021-05-29 09:49:47 -07:00
parent 3024fe7baf
commit 4d41db2920
3 changed files with 21 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -101,6 +101,17 @@ namespace sat {
m_solver.mk_clause(sz, m_lits.data(), status::input()); m_solver.mk_clause(sz, m_lits.data(), status::input());
} }
void dual_solver::add_assumptions(solver const& s) {
m_lits.reset();
for (bool_var v : m_tracked_vars)
m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
for (auto lit : m_units) {
bool_var w = m_ext2var.get(lit.var(), null_bool_var);
if (w != null_bool_var)
m_lits.push_back(ext2lit(lit));
}
}
bool dual_solver::operator()(solver const& s) { bool dual_solver::operator()(solver const& s) {
m_core.reset(); m_core.reset();
m_core.append(m_units); m_core.append(m_units);
@ -108,9 +119,7 @@ namespace sat {
return true; return true;
m_solver.user_push(); m_solver.user_push();
m_solver.add_clause(m_roots.size(), m_roots.data(), status::input()); m_solver.add_clause(m_roots.size(), m_roots.data(), status::input());
m_lits.reset(); add_assumptions(s);
for (bool_var v : m_tracked_vars)
m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
lbool is_sat = m_solver.check(m_lits.size(), m_lits.data()); lbool is_sat = m_solver.check(m_lits.size(), m_lits.data());
if (is_sat == l_false) if (is_sat == l_false)
for (literal lit : m_solver.get_core()) for (literal lit : m_solver.get_core())

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

@ -42,6 +42,8 @@ namespace sat {
literal ext2lit(literal lit); literal ext2lit(literal lit);
literal lit2ext(literal lit); literal lit2ext(literal lit);
void add_assumptions(solver const& s);
std::ostream& display(solver const& s, std::ostream& out) const; std::ostream& display(solver const& s, std::ostream& out) const;
public: public:

7
src/sat/tactic/goal2sat.cpp
View file

@ -137,6 +137,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
if (relevancy_enabled()) if (relevancy_enabled())
ensure_euf()->add_root(n, lits); ensure_euf()->add_root(n, lits);
} }
void add_dual_root(sat::literal lit) {
add_dual_root(1, &lit);
}
void mk_clause(sat::literal l) { void mk_clause(sat::literal l) {
mk_clause(1, &l); mk_clause(1, &l);
@ -199,6 +203,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
// create fake variable to represent true; // create fake variable to represent true;
m_true = sat::literal(add_var(false, m.mk_true()), false); m_true = sat::literal(add_var(false, m.mk_true()), false);
mk_clause(m_true); // v is true mk_clause(m_true); // v is true
add_dual_root(1, &m_true);
} }
return m_true; return m_true;
} }
@ -223,6 +228,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
if (!m_expr2var_replay || !m_expr2var_replay->find(t, v)) if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))
v = add_var(true, t); v = add_var(true, t);
m_map.insert(t, v); m_map.insert(t, v);
if (relevancy_enabled() && (m.is_true(t) || m.is_false(t)))
add_dual_root(sat::literal(v, m.is_false(t)));
return v; return v;
} }