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

#5641

Browse source 
mark all literals duplicated in dual solver as external
This commit is contained in:
Nikolaj Bjorner 2021-12-26 15:06:04 -08:00
parent fcee2f5aa5
commit 0bd6725711
3 changed files with 16 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/euf_relevancy.cpp
View file

@ -59,7 +59,7 @@ namespace euf {
void solver::ensure_dual_solver() {
if (m_dual_solver)
return;
m_dual_solver = alloc(sat::dual_solver, s().rlimit());
m_dual_solver = alloc(sat::dual_solver, s(), s().rlimit());
for (unsigned i = s().num_user_scopes(); i-- > 0; )
m_dual_solver->push();
}
@ -95,7 +95,7 @@ namespace euf {
return true;
if (!m_dual_solver)
return true;
if (!(*m_dual_solver)(s()))
if (!(*m_dual_solver)())
return false;
init_relevant_expr_ids();

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

@ -18,7 +18,8 @@ Author:
namespace sat {
dual_solver::dual_solver(reslimit& l):
dual_solver::dual_solver(solver& s, reslimit& l):
s(s),
m_solver(m_params, l)
{
SASSERT(!m_solver.get_config().m_drat);
@ -69,6 +70,7 @@ namespace sat {
if (null_bool_var == w) {
w = m_solver.mk_var();
m_solver.set_external(w);
s.set_external(v);
m_ext2var.setx(v, w, null_bool_var);
m_var2ext.setx(w, v, null_bool_var);
m_vars.push_back(v);
@ -122,7 +124,7 @@ namespace sat {
m_solver.mk_clause(sz, m_lits.data(), status::input());
}
void dual_solver::add_assumptions(solver const& s) {
void dual_solver::add_assumptions() {
flush();
m_lits.reset();
for (bool_var v : m_tracked_vars)
@ -134,14 +136,14 @@ namespace sat {
}
}
bool dual_solver::operator()(solver const& s) {
bool dual_solver::operator()() {
m_core.reset();
m_core.append(m_units);
if (m_roots.empty())
return true;
m_solver.user_push();
m_solver.add_clause(m_roots.size(), m_roots.data(), status::input());
add_assumptions(s);
add_assumptions();
lbool is_sat = m_solver.check(m_lits.size(), m_lits.data());
if (is_sat == l_false)
for (literal lit : m_solver.get_core())
@ -149,7 +151,8 @@ namespace sat {
if (is_sat == l_true) {
TRACE("dual", display(s, tout); s.display(tout););
IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
IF_VERBOSE(0, display(s, verbose_stream()); s.display(verbose_stream()););
IF_VERBOSE(0, verbose_stream() << "assumptions: " << m_lits << "\n");
IF_VERBOSE(0, display(verbose_stream()); s.display(verbose_stream()););
UNREACHABLE();
return false;
}
@ -158,7 +161,7 @@ namespace sat {
return is_sat == l_false;
}
std::ostream& dual_solver::display(solver const& s, std::ostream& out) const {
std::ostream& dual_solver::display(std::ostream& out) const {
for (unsigned v = 0; v < m_solver.num_vars(); ++v) {
bool_var w = m_var2ext.get(v, null_bool_var);
if (w == null_bool_var)

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

@ -29,6 +29,7 @@ namespace sat {
set_bool("core.minimize", false);
}
};
solver& s;
dual_params m_params;
solver m_solver;
lim_svector<literal> m_units, m_roots;
@ -46,14 +47,14 @@ namespace sat {
literal ext2lit(literal lit);
literal lit2ext(literal lit);
void add_assumptions(solver const& s);
void add_assumptions();
std::ostream& display(solver const& s, std::ostream& out) const;
std::ostream& display(std::ostream& out) const;
void flush();
public:
dual_solver(reslimit& l);
dual_solver(solver& s, reslimit& l);
void push();
void pop(unsigned num_scopes);
@ -76,7 +77,7 @@ namespace sat {
/*
* Extract a minimized subset of relevant literals from a model for s.
*/
bool operator()(solver const& s);
bool operator()();
literal_vector const& core() const { return m_core; }
};