mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

'clean

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-30 13:14:48 -07:00
parent d64bc795f0
commit a764d528a1
5 changed files with 17 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_config.cpp
View file

@ -192,7 +192,7 @@ namespace sat {
m_drat_check_unsat = p.drat_check_unsat(); m_drat_check_unsat = p.drat_check_unsat();
m_drat_check_sat = p.drat_check_sat(); m_drat_check_sat = p.drat_check_sat();
m_drat_file = p.drat_file(); m_drat_file = p.drat_file();
m_drat = (m_drat_check_unsat || m_drat_file != symbol("") || m_drat_check_sat) && p.threads() == 1; m_drat = (m_drat_check_unsat || m_drat_file.is_non_empty_string() || m_drat_check_sat) && p.threads() == 1;
m_drat_binary = p.drat_binary(); m_drat_binary = p.drat_binary();
m_drat_activity = p.drat_activity(); m_drat_activity = p.drat_activity();
m_dyn_sub_res = p.dyn_sub_res(); m_dyn_sub_res = p.dyn_sub_res();

2
src/sat/sat_solver.cpp
View file

@ -392,6 +392,8 @@ namespace sat {
} }
void solver::drat_log_unit(literal lit, justification j) { void solver::drat_log_unit(literal lit, justification j) {
if (!m_ext)
return;
extension::scoped_drating _sd(*m_ext.get()); extension::scoped_drating _sd(*m_ext.get());
if (j.get_kind() == justification::EXT_JUSTIFICATION) if (j.get_kind() == justification::EXT_JUSTIFICATION)
fill_ext_antecedents(lit, j, false); fill_ext_antecedents(lit, j, false);

3
src/sat/smt/q_mbi.cpp
View file

@ -127,6 +127,7 @@ namespace q {
proj = solver_project(*mdl1, *qb); proj = solver_project(*mdl1, *qb);
if (!proj) if (!proj)
break; break;
TRACE("q", tout << "project: " << proj << "\n";);
m_qs.add_clause(~qlit, ~ctx.mk_literal(proj)); m_qs.add_clause(~qlit, ~ctx.mk_literal(proj));
m_solver->assert_expr(m.mk_not(proj)); m_solver->assert_expr(m.mk_not(proj));
} }
@ -136,6 +137,7 @@ namespace q {
proj = solver_project(*mdl0, *qb); proj = solver_project(*mdl0, *qb);
if (!proj) if (!proj)
return l_undef; return l_undef;
TRACE("q", tout << "project-base: " << proj << "\n";);
m_qs.add_clause(~qlit, ~ctx.mk_literal(proj)); m_qs.add_clause(~qlit, ~ctx.mk_literal(proj));
} }
// TODO: add as top-level clause for relevancy // TODO: add as top-level clause for relevancy
@ -251,7 +253,6 @@ namespace q {
if (!m_model->eval_expr(bounds, mbounds, true)) if (!m_model->eval_expr(bounds, mbounds, true))
return; return;
mbounds = subst(mbounds, qb.vars); mbounds = subst(mbounds, qb.vars);
std::cout << "restrict with bounds " << mbounds << " " << vbounds << "\n";
m_solver->assert_expr(mbounds); m_solver->assert_expr(mbounds);
qb.domain_eqs.push_back(vbounds); qb.domain_eqs.push_back(vbounds);
} }

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

@ -18,9 +18,15 @@ Author:
namespace sat { namespace sat {
dual_solver::no_drat_params::no_drat_params() {
set_sym("drat.file", symbol());
}
dual_solver::dual_solver(reslimit& l): dual_solver::dual_solver(reslimit& l):
m_solver(params_ref(), l) m_solver(m_params, l)
{} {
SASSERT(!m_solver.get_config().m_drat);
}
void dual_solver::push() { void dual_solver::push() {
m_solver.user_push(); m_solver.user_push();

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

@ -23,6 +23,10 @@ Author:
namespace sat { namespace sat {
class dual_solver { class dual_solver {
struct no_drat_params : public params_ref {
no_drat_params();
};
no_drat_params m_params;
solver m_solver; solver m_solver;
lim_svector<literal> m_units, m_roots; lim_svector<literal> m_units, m_roots;
lim_svector<bool_var> m_tracked_vars; lim_svector<bool_var> m_tracked_vars;