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

mk-var during copy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-31 20:34:41 -07:00
parent ed7d969366
commit fa9cf0fa0c
2 changed files with 23 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/sat/sat_solver.cpp
View file

@ -86,7 +86,7 @@ namespace sat {
m_cuber = nullptr; m_cuber = nullptr;
m_local_search = nullptr; m_local_search = nullptr;
m_mc.set_solver(this); m_mc.set_solver(this);
mk_var(false, false); // reserve var 0 to internal. mk_var(false, false);
} }
solver::~solver() { solver::~solver() {
@ -121,6 +121,7 @@ namespace sat {
m_justification.reset(); m_justification.reset();
m_decision.reset(); m_decision.reset();
m_eliminated.reset(); m_eliminated.reset();
m_external.reset();
m_activity.reset(); m_activity.reset();
m_mark.reset(); m_mark.reset();
m_lit_mark.reset(); m_lit_mark.reset();
@ -137,6 +138,7 @@ namespace sat {
m_qhead = 0; m_qhead = 0;
m_trail.reset(); m_trail.reset();
m_scopes.reset(); m_scopes.reset();
mk_var(false, false);
if (src.inconsistent()) { if (src.inconsistent()) {
set_conflict(); set_conflict();
@ -1240,10 +1242,9 @@ namespace sat {
while (is_sat == l_undef && !should_cancel()) { while (is_sat == l_undef && !should_cancel()) {
if (inconsistent()) is_sat = resolve_conflict_core(); if (inconsistent()) is_sat = resolve_conflict_core();
else if (should_propagate()) propagate(true); else if (should_propagate()) propagate(true);
else if (m_conflicts_since_init > 0 && do_cleanup(false)) continue; else if (do_cleanup(false)) continue;
else if (should_gc()) do_gc(); else if (should_gc()) do_gc();
else if (should_rephase()) do_rephase(); else if (should_rephase()) do_rephase();
else if (should_reorder()) do_reorder();
else if (should_restart()) do_restart(!m_config.m_restart_fast); else if (should_restart()) do_restart(!m_config.m_restart_fast);
else if (should_simplify()) do_simplify(); else if (should_simplify()) do_simplify();
else if (!decide()) is_sat = final_check(); else if (!decide()) is_sat = final_check();
@ -1601,6 +1602,19 @@ namespace sat {
} }
lbool solver::bounded_search() { lbool solver::bounded_search() {
#if 0
lbool is_sat = l_undef;
while (is_sat == l_undef && !should_cancel()) {
if (inconsistent()) is_sat = resolve_conflict_core();
else if (should_propagate()) propagate(true);
else if (do_cleanup(false)) continue;
else if (should_gc()) do_gc();
else if (should_rephase()) do_rephase();
else if (should_restart()) return l_undef;
else if (!decide()) is_sat = final_check();
}
return is_sat;
#else
while (true) { while (true) {
checkpoint(); checkpoint();
bool done = false; bool done = false;
@ -1619,6 +1633,7 @@ namespace sat {
} }
} }
} }
#endif
} }
bool solver::should_propagate() const { bool solver::should_propagate() const {
@ -2168,7 +2183,7 @@ namespace sat {
IF_VERBOSE(1, verbose_stream() << str); IF_VERBOSE(1, verbose_stream() << str);
} }
void solver::do_restart(bool to_base) { void solver::do_restart(bool to_base) {
m_stats.m_restart++; m_stats.m_restart++;
m_restarts++; m_restarts++;
if (m_conflicts_since_init >= m_restart_next_out && get_verbosity_level() >= 1) { if (m_conflicts_since_init >= m_restart_next_out && get_verbosity_level() >= 1) {
@ -4308,6 +4323,8 @@ namespace sat {
// //
// ----------------------- // -----------------------
bool solver::do_cleanup(bool force) { bool solver::do_cleanup(bool force) {
if (m_conflicts_since_init == 0 && !force)
return false;
if (at_base_lvl() && !inconsistent() && m_cleaner(force)) { if (at_base_lvl() && !inconsistent() && m_cleaner(force)) {
if (m_ext) if (m_ext)
m_ext->clauses_modifed(); m_ext->clauses_modifed();

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

@ -817,9 +817,9 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
} }
void goal2sat::get_interpreted_funs(func_decl_ref_vector& atoms) { void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) {
if (m_imp) { if (m_imp) {
atoms.append(m_imp->interpreted_funs()); funs.append(m_imp->interpreted_funs());
} }
} }