mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

inherit incremental override on the solver state

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-12 14:33:23 -08:00
parent deda8f46f8
commit dbe7828f1d
3 changed files with 16 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/sat/sat_asymm_branch.cpp
View file

@ -134,7 +134,6 @@ namespace sat {
s.propagate(false);
if (s.m_inconsistent)
break;
// std::cout << m_elim_literals - elim << "\n";
if (m_elim_literals == elim)
break;
}
@ -232,19 +231,6 @@ namespace sat {
}
}
if (!m_to_delete.empty()) {
#if 0
std::cout << "delete " << m_to_delete << "\n";
std::cout << "pos\n";
for (literal l : m_pos) {
std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
}
std::cout << "neg\n";
for (literal l : m_neg) {
std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
}
std::cout << "\n";
#endif
unsigned j = 0;
for (unsigned i = 0; i < c.size(); ++i) {
if (!m_to_delete.contains(c[i])) {

2
src/sat/sat_simplifier.cpp
View file

@ -1782,7 +1782,7 @@ namespace sat {
// eliminate variable
++s.m_stats.m_elim_var_res;
VERIFY(!s.is_external(v));
VERIFY(!is_external(v));
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
save_clauses(mc_entry, m_pos_cls);
save_clauses(mc_entry, m_neg_cls);

18
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -36,6 +36,7 @@ Notes:
#include "ast/ast_util.h"
#include "tactic/core/propagate_values_tactic.h"
#include "sat/sat_params.hpp"
#include "sat/sat_simplifier_params.hpp"
// incremental SAT solver.
class inc_sat_solver : public solver {
@ -88,7 +89,17 @@ public:
m_internalized_fmls(m) {
updt_params(p);
init_preprocess();
m_solver.set_incremental(incremental_mode);
m_solver.set_incremental(incremental_mode && !override_incremental());
}
bool override_incremental() const {
sat_simplifier_params p(m_params);
std::cout << "override: " << p.override_incremental() << "\n";
return p.override_incremental();
}
bool is_incremental() const {
return m_solver.get_config().m_incremental;
}
virtual ~inc_sat_solver() {}
@ -99,7 +110,7 @@ public:
}
ast_translation tr(m, dst_m);
m_solver.pop_to_base_level();
inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, m_solver.get_config().m_incremental);
inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental());
result->m_solver.copy(m_solver);
result->m_fmls_head = m_fmls_head;
for (expr* f : m_fmls) result->m_fmls.push_back(tr(f));
@ -272,6 +283,7 @@ public:
m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
m_params.set_bool("xor_solver", p1.xor_solver());
m_solver.updt_params(m_params);
m_solver.set_incremental(is_incremental() && !override_incremental());
}
virtual void collect_statistics(statistics & st) const {
@ -517,7 +529,7 @@ private:
m_pc = g->pc();
m_mc = g->mc();
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, m_solver.get_config().m_incremental, is_lemma);
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma);
m_goal2sat.get_interpreted_atoms(atoms);
if (!atoms.empty()) {
std::stringstream strm;