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

bvsls refactoring

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-28 15:26:52 +00:00
parent c541694f40
commit 239849957a
2 changed files with 25 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/tactic/sls/sls_engine.cpp
View file

@ -1125,8 +1125,31 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << std::endl; verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << std::endl;
verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl; verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl;
verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl;
verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl;
lbool res = operator()();
if (res == l_true) {
report_tactic_progress("Number of flips:", m_stats.m_moves);
for (unsigned i = 0; i < g->size(); i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
{
verbose_stream() << "Terminated before all assertions were SAT!" << std::endl;
NOT_IMPLEMENTED_YET();
}
if (m_produce_models) {
model_ref mdl = m_tracker.get_model();
mc = model2model_converter(mdl.get());
TRACE("sls_model", mc->display(tout););
}
g->reset();
}
else
mc = 0;
}
lbool sls_engine::operator()() {
init_tracker(); init_tracker();
lbool res = l_undef; lbool res = l_undef;
@ -1149,25 +1172,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
} while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts); } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts);
verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
if (res == l_true) {
report_tactic_progress("Number of flips:", m_stats.m_moves);
for (unsigned i = 0; i < g->size(); i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
{
verbose_stream() << "Terminated before all assertions were SAT!" << std::endl;
NOT_IMPLEMENTED_YET();
}
if (m_produce_models) {
model_ref mdl = m_tracker.get_model();
mc = model2model_converter(mdl.get());
TRACE("sls_model", mc->display(tout););
}
g->reset();
}
else
mc = 0;
} }
unsigned sls_engine::check_restart(unsigned curr_value) unsigned sls_engine::check_restart(unsigned curr_value)

1
src/tactic/sls/sls_engine.h
View file

@ -113,6 +113,7 @@ public:
lbool search(void); lbool search(void);
lbool operator()();
void operator()(goal_ref const & g, model_converter_ref & mc); void operator()(goal_ref const & g, model_converter_ref & mc);
protected: protected: