<commit_before>/*++
Copyright (c) 2014 Microsoft Corporation

Module Name:

    bvsls_opt_engine.cpp

Abstract:

    Optimization extensions to bvsls

Author:

    Christoph (cwinter) 2014-03-28

Notes:

--*/
#include "sls_compilation_settings.h"
#include "nnf.h"
#include "bvsls_opt_engine.h"

bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
    sls_engine(m, p),
    m_hard_tracker(sls_engine::m_tracker),
    m_obj_tracker(m, m_bv_util, m_mpz_manager, m_powers),
    m_obj_evaluator(m, m_bv_util, m_obj_tracker, m_mpz_manager, m_powers)
{
    m_best_model = alloc(model, m);
}

bvsls_opt_engine::~bvsls_opt_engine()
{    
}

bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
    expr_ref const & objective, 
    model_ref initial_model, 
    bool _maximize)
{
    SASSERT(m_bv_util.is_bv(objective));
    TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " <<
                            mk_ismt2_pp(objective, m()) << std::endl;);
    m_hard_tracker.initialize(m_assertions);
    m_restart_limit = _RESTART_LIMIT_;
    setup_opt_tracker(objective, _maximize);

    if (initial_model.get() != 0) {
        TRACE("sls_opt", tout << "Initial model provided: " << std::endl;
                        for (unsigned i = 0; i < initial_model->get_num_constants(); i++) {
                            func_decl * fd = initial_model->get_constant(i);
                            expr * val = initial_model->get_const_interp(fd);
                            tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl;
                        });
        m_hard_tracker.set_model(initial_model);
    }    
   
    optimization_result res(m_manager);
    lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;    

    for (m_stats.m_restarts = 0;
         m_stats.m_restarts < m_max_restarts;
         m_stats.m_restarts++)
    {
        mpz old_best;
        m_mpz_manager.set(old_best, m_best_model_score);

        if (!is_sat) {
            do {
                checkpoint();

                IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
                is_sat = search();

                if (is_sat == l_undef)
                    m_hard_tracker.randomize(m_assertions);
            } 
            while (is_sat != l_true && 
                   m_stats.m_restarts++ < m_max_restarts);
        }

        if (is_sat == l_true) {
            IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
            res.is_sat = l_true;
            m_obj_tracker.set_model(m_hard_tracker.get_model());
            m_obj_evaluator.update_all();
            expr_ref local_best = maximize();
            if ((_maximize && m_mpz_manager.gt(m_best_model_score, old_best)) ||
                (!_maximize && m_mpz_manager.lt(m_best_model_score, old_best))) 
            {
                res.optimum = local_best;
            }
        }
        
        m_hard_tracker.randomize(m_assertions);
        m_evaluator.update_all();
        is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
    }    
<commit_msg>bvsls opt engine bugfix/debugging<commit_after>/*++
Copyright (c) 2014 Microsoft Corporation

Module Name:

    bvsls_opt_engine.cpp

Abstract:

    Optimization extensions to bvsls

Author:

    Christoph (cwinter) 2014-03-28

Notes:

--*/
#include "sls_compilation_settings.h"
#include "nnf.h"
#include "bvsls_opt_engine.h"

bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
    sls_engine(m, p),
    m_hard_tracker(sls_engine::m_tracker),
    m_obj_tracker(m, m_bv_util, m_mpz_manager, m_powers),
    m_obj_evaluator(m, m_bv_util, m_obj_tracker, m_mpz_manager, m_powers)
{
    m_best_model = alloc(model, m);
}

bvsls_opt_engine::~bvsls_opt_engine()
{    
}

bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
    expr_ref const & objective, 
    model_ref initial_model, 
    bool _maximize)
{
    SASSERT(m_bv_util.is_bv(objective));
    TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " <<
                            mk_ismt2_pp(objective, m()) << std::endl;);
    m_hard_tracker.initialize(m_assertions);
    m_restart_limit = _RESTART_LIMIT_;
    setup_opt_tracker(objective, _maximize);

    if (initial_model.get() != 0) {
        TRACE("sls_opt", tout << "Initial model provided: " << std::endl;
                        for (unsigned i = 0; i < initial_model->get_num_constants(); i++) {
                            func_decl * fd = initial_model->get_constant(i);
                            expr * val = initial_model->get_const_interp(fd);
                            tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl;
                        });
        m_hard_tracker.set_model(initial_model);
        m_evaluator.update_all();
    }
   
    optimization_result res(m_manager);
    lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;    

    TRACE("sls_opt", tout << "initial model is sat? " << is_sat << std::endl;);

    for (m_stats.m_restarts = 0;
         m_stats.m_restarts < m_max_restarts;
         m_stats.m_restarts++)
    {
        mpz old_best;
        m_mpz_manager.set(old_best, m_best_model_score);

        if (is_sat != l_true) {
            do {
                checkpoint();

                IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
                is_sat = search();

                if (is_sat == l_undef)
                    m_hard_tracker.randomize(m_assertions);
            } 
            while (is_sat != l_true && 
                   m_stats.m_restarts++ < m_max_restarts);
        }

        if (is_sat == l_true) {
            IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
            res.is_sat = l_true;
            m_obj_tracker.set_model(m_hard_tracker.get_model());
            m_obj_evaluator.update_all();
            expr_ref local_best = maximize();
            if ((_maximize && m_mpz_manager.gt(m_best_model_score, old_best)) ||
                (!_maximize && m_mpz_manager.lt(m_best_model_score, old_best))) 
            {
                res.optimum = local_best;
            }
        }
        
        m_hard_tracker.randomize(m_assertions);
        m_evaluator.update_all();
        is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
    }    

{'fraction_non_alphanumeric': 0.1242800848742043, 'fraction_numerical': 0.005759321006365566, 'mean_word_length': 2.353150406504065, 'pattern_counts': {'":': 2, '<': 83, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3850910', 'n_tokens_mistral': 2449, 'n_tokens_neox': 2328, 'n_words': 351}