mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

remove reference to tactic.h

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-22 13:17:04 -08:00
parent 7adb402a3f
commit cd331b8a56
3 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/sls/bvsls_opt_engine.cpp
View file

@ -68,7 +68,8 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
if (is_sat != l_true) { if (is_sat != l_true) {
do { do {
checkpoint(); if (!m_manager.inc())
return res;
IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
is_sat = search(); is_sat = search();
@ -136,7 +137,8 @@ expr_ref bvsls_opt_engine::maximize()
while (m_mpz_manager.lt(score, max_score) && check_restart(m_stats.m_moves)) while (m_mpz_manager.lt(score, max_score) && check_restart(m_stats.m_moves))
{ {
checkpoint(); if (!m_manager.inc())
goto bailout;
m_stats.m_moves++; m_stats.m_moves++;
m_mpz_manager.set(old_score, score); m_mpz_manager.set(old_score, score);
new_const = (unsigned)-1; new_const = (unsigned)-1;

13
src/ast/sls/sls_engine.cpp
View file

@ -23,7 +23,6 @@ Notes:
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
#include "model/model_pp.h" #include "model/model_pp.h"
#include "tactic/tactic.h"
#include "util/luby.h" #include "util/luby.h"
#include "params/sls_params.hpp" #include "params/sls_params.hpp"
@ -91,14 +90,12 @@ void sls_engine::collect_statistics(statistics& st) const {
st.update("sls moves/sec", m_stats.m_moves / seconds); st.update("sls moves/sec", m_stats.m_moves / seconds);
} }
void sls_engine::checkpoint() {
tactic::checkpoint(m_manager);
}
bool sls_engine::full_eval(model & mdl) { bool sls_engine::full_eval(model & mdl) {
model::scoped_model_completion _scm(mdl, true); model::scoped_model_completion _scm(mdl, true);
for (expr* a : m_assertions) { for (expr* a : m_assertions) {
checkpoint(); if (!m_manager.inc())
return false;
if (!mdl.is_true(a)) { if (!mdl.is_true(a)) {
TRACE("sls", tout << "Evaluation: false\n";); TRACE("sls", tout << "Evaluation: false\n";);
return false; return false;
@ -422,7 +419,8 @@ lbool sls_engine::search() {
unsigned sz = m_assertions.size(); unsigned sz = m_assertions.size();
while (check_restart(m_stats.m_moves)) { while (check_restart(m_stats.m_moves)) {
checkpoint(); if (!m_manager.inc())
return l_undef;
m_stats.m_moves++; m_stats.m_moves++;
// Andreas: Every base restart interval ... // Andreas: Every base restart interval ...
@ -532,7 +530,8 @@ lbool sls_engine::operator()() {
lbool res = l_undef; lbool res = l_undef;
do { do {
checkpoint(); if (!m_manager.inc())
return l_undef;
// report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); // report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
res = search(); res = search();

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

@ -117,7 +117,6 @@ public:
unsynch_mpz_manager& get_mpz_manager() { return m_mpz_manager; } unsynch_mpz_manager& get_mpz_manager() { return m_mpz_manager; }
protected: protected:
void checkpoint();
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value); double & best_score, unsigned & best_const, mpz & best_value);