mirror of
https://github.com/Z3Prover/z3
synced 2026-02-21 15:57:35 +00:00
eddb75b2e7
* Initial plan * Migrate iterator-based for loops to range-based for loops in 11 files Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix compilation error in aig_exporter.cpp - use correct iterator API Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Revert changes to z3++.h as requested Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
68 lines
1.8 KiB
C++
68 lines
1.8 KiB
C++
/*++
|
|
Copyright (c) 2014 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
bvsls_opt_engine.h
|
|
|
|
Abstract:
|
|
|
|
Optimization extensions to bvsls
|
|
|
|
Author:
|
|
|
|
Christoph (cwinter) 2014-03-28
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "ast/sls/sls_bv_engine.h"
|
|
|
|
class bvsls_opt_engine : public sls_engine {
|
|
sls_tracker & m_hard_tracker;
|
|
sls_tracker m_obj_tracker;
|
|
sls_evaluator m_obj_evaluator;
|
|
model_ref m_best_model;
|
|
mpz m_best_model_score;
|
|
unsigned m_obj_bv_sz;
|
|
expr * m_obj_e;
|
|
|
|
public:
|
|
bvsls_opt_engine(ast_manager & m, params_ref const & p);
|
|
|
|
class optimization_result {
|
|
public:
|
|
lbool is_sat;
|
|
expr_ref optimum;
|
|
optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {}
|
|
};
|
|
|
|
optimization_result optimize(expr_ref const & objective, model_ref initial_model = model_ref(), bool maximize=true);
|
|
|
|
void get_model(model_ref & result) { result = m_best_model; }
|
|
|
|
protected:
|
|
void setup_opt_tracker(expr_ref const & objective, bool _max);
|
|
expr_ref maximize();
|
|
|
|
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
|
|
mpz & best_score, unsigned & best_const, mpz & best_value);
|
|
|
|
mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz & score,
|
|
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
|
|
mpz const & max_score, expr * objective);
|
|
|
|
mpz top_score() {
|
|
mpz res(0);
|
|
obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
|
|
for (auto* e : top_exprs)
|
|
m_mpz_manager.add(res, m_obj_tracker.get_value(e), res);
|
|
return res;
|
|
}
|
|
|
|
void save_model(mpz const & score);
|
|
bool randomize_wrt_hard();
|
|
};
|
|
|