mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 19:53:34 +00:00
323 lines
12 KiB
C++
323 lines
12 KiB
C++
/*++
|
|
Copyright (c) 2013 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
opt_context.h
|
|
|
|
Abstract:
|
|
Facility for running optimization problem.
|
|
|
|
Author:
|
|
|
|
Anh-Dung Phan (t-anphan) 2013-10-16
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#ifndef OPT_CONTEXT_H_
|
|
#define OPT_CONTEXT_H_
|
|
|
|
#include "ast/ast.h"
|
|
#include "ast/arith_decl_plugin.h"
|
|
#include "ast/bv_decl_plugin.h"
|
|
#include "tactic/model_converter.h"
|
|
#include "tactic/tactic.h"
|
|
#include "qe/qsat.h"
|
|
#include "opt/opt_solver.h"
|
|
#include "opt/opt_pareto.h"
|
|
#include "opt/optsmt.h"
|
|
#include "opt/opt_lns.h"
|
|
#include "opt/maxsmt.h"
|
|
#include "cmd_context/cmd_context.h"
|
|
|
|
|
|
namespace opt {
|
|
|
|
class opt_solver;
|
|
|
|
/**
|
|
\brief base class required by MaxSMT solvers.
|
|
By implementing a base class, you can invoke the MaxSMT solvers
|
|
independent of the overall optimization infrastructure.
|
|
The caller has to supply a solver object that encapsulates
|
|
an incremental SAT or SMT solver. The MaxSMT solvers may assume that
|
|
the solver object should be in a satisfiable state and contain an initial model.
|
|
*/
|
|
|
|
class maxsat_context {
|
|
public:
|
|
virtual generic_model_converter& fm() = 0; // converter that removes fresh names introduced by simplification.
|
|
virtual bool sat_enabled() const = 0; // is using th SAT solver core enabled?
|
|
virtual solver& get_solver() = 0; // retrieve solver object (SAT or SMT solver)
|
|
virtual ast_manager& get_manager() const = 0;
|
|
virtual params_ref& params() = 0;
|
|
virtual void enable_sls(bool force) = 0; // stochastic local search
|
|
virtual symbol const& maxsat_engine() const = 0; // retrieve maxsat engine configuration parameter.
|
|
virtual void get_base_model(model_ref& _m) = 0; // retrieve model from initial satisfiability call.
|
|
virtual smt::context& smt_context() = 0; // access SMT context for SMT based MaxSMT solver (wmax requires SMT core)
|
|
virtual unsigned num_objectives() = 0;
|
|
virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0;
|
|
virtual void set_model(model_ref& _m) = 0;
|
|
};
|
|
|
|
/**
|
|
\brief main context object for optimization.
|
|
Hard and soft assertions, and objectives are registered with this context.
|
|
It handles combinations of objectives.
|
|
*/
|
|
|
|
class context :
|
|
public opt_wrapper,
|
|
public pareto_callback,
|
|
public maxsat_context {
|
|
typedef map<symbol, maxsmt*, symbol_hash_proc, symbol_eq_proc> map_t;
|
|
typedef map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> map_id;
|
|
typedef vector<std::pair<inf_eps, inf_eps> > bounds_t;
|
|
enum objective_t {
|
|
O_MAXIMIZE,
|
|
O_MINIMIZE,
|
|
O_MAXSMT
|
|
};
|
|
|
|
struct objective {
|
|
objective_t m_type;
|
|
app_ref m_term; // for maximize, minimize term
|
|
expr_ref_vector m_terms; // for maxsmt
|
|
vector<rational> m_weights; // for maxsmt
|
|
adjust_value m_adjust_value;
|
|
symbol m_id; // for maxsmt
|
|
unsigned m_index; // for maximize/minimize index
|
|
|
|
objective(bool is_max, app_ref& t, unsigned idx):
|
|
m_type(is_max?O_MAXIMIZE:O_MINIMIZE),
|
|
m_term(t),
|
|
m_terms(t.get_manager()),
|
|
m_id(),
|
|
m_index(idx)
|
|
{
|
|
if (!is_max) {
|
|
m_adjust_value.set_negate(true);
|
|
}
|
|
}
|
|
|
|
objective(ast_manager& m, symbol id):
|
|
m_type(O_MAXSMT),
|
|
m_term(m),
|
|
m_terms(m),
|
|
m_id(id),
|
|
m_index(0)
|
|
{}
|
|
};
|
|
|
|
class scoped_state {
|
|
ast_manager& m;
|
|
arith_util m_arith;
|
|
bv_util m_bv;
|
|
unsigned_vector m_hard_lim;
|
|
unsigned_vector m_objectives_lim;
|
|
unsigned_vector m_objectives_term_trail;
|
|
unsigned_vector m_objectives_term_trail_lim;
|
|
map_id m_indices;
|
|
|
|
public:
|
|
expr_ref_vector m_hard;
|
|
vector<objective> m_objectives;
|
|
|
|
scoped_state(ast_manager& m):
|
|
m(m),
|
|
m_arith(m),
|
|
m_bv(m),
|
|
m_hard(m)
|
|
{}
|
|
void push();
|
|
void pop();
|
|
void add(expr* hard);
|
|
bool set(ptr_vector<expr> & hard);
|
|
unsigned add(expr* soft, rational const& weight, symbol const& id);
|
|
unsigned add(app* obj, bool is_max);
|
|
unsigned get_index(symbol const& id) { return m_indices[id]; }
|
|
};
|
|
|
|
ast_manager& m;
|
|
arith_util m_arith;
|
|
bv_util m_bv;
|
|
expr_ref_vector m_hard_constraints;
|
|
ref<opt_solver> m_opt_solver;
|
|
ref<solver> m_solver;
|
|
ref<solver> m_sat_solver;
|
|
scoped_ptr<pareto_base> m_pareto;
|
|
scoped_ptr<lns> m_lns;
|
|
scoped_ptr<qe::qmax> m_qmax;
|
|
sref_vector<model> m_box_models;
|
|
unsigned m_box_index;
|
|
params_ref m_params;
|
|
optsmt m_optsmt;
|
|
map_t m_maxsmts;
|
|
scoped_state m_scoped_state;
|
|
vector<objective> m_objectives;
|
|
model_ref m_model;
|
|
model_converter_ref m_model_converter;
|
|
generic_model_converter_ref m_fm;
|
|
obj_map<func_decl, unsigned> m_objective_fns;
|
|
obj_map<func_decl, expr*> m_objective_orig;
|
|
func_decl_ref_vector m_objective_refs;
|
|
tactic_ref m_simplify;
|
|
bool m_enable_sat;
|
|
bool m_enable_sls;
|
|
bool m_is_clausal;
|
|
bool m_pp_neat;
|
|
symbol m_maxsat_engine;
|
|
symbol m_logic;
|
|
svector<symbol> m_labels;
|
|
std::string m_unknown;
|
|
public:
|
|
context(ast_manager& m);
|
|
virtual ~context();
|
|
unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
|
|
unsigned add_objective(app* t, bool is_max);
|
|
void add_hard_constraint(expr* f);
|
|
|
|
void get_hard_constraints(expr_ref_vector& hard);
|
|
expr_ref get_objective(unsigned i);
|
|
|
|
virtual void push();
|
|
virtual void pop(unsigned n);
|
|
virtual bool empty() { return m_scoped_state.m_objectives.empty(); }
|
|
virtual void set_hard_constraints(ptr_vector<expr> & hard);
|
|
virtual lbool optimize();
|
|
virtual void set_model(model_ref& _m) { m_model = _m; }
|
|
virtual void get_model_core(model_ref& _m);
|
|
virtual void get_box_model(model_ref& _m, unsigned index);
|
|
virtual void fix_model(model_ref& _m);
|
|
virtual void collect_statistics(statistics& stats) const;
|
|
virtual proof* get_proof() { return 0; }
|
|
virtual void get_labels(svector<symbol> & r);
|
|
virtual void get_unsat_core(ptr_vector<expr> & r);
|
|
virtual std::string reason_unknown() const;
|
|
virtual void set_reason_unknown(char const* msg) { m_unknown = msg; }
|
|
|
|
virtual void display_assignment(std::ostream& out);
|
|
virtual bool is_pareto() { return m_pareto.get() != 0; }
|
|
virtual void set_logic(symbol const& s) { m_logic = s; }
|
|
void set_clausal(bool f) { m_is_clausal = f; }
|
|
|
|
void display(std::ostream& out);
|
|
static void collect_param_descrs(param_descrs & r);
|
|
virtual void updt_params(params_ref const& p);
|
|
params_ref& get_params() { return m_params; }
|
|
|
|
expr_ref get_lower(unsigned idx);
|
|
expr_ref get_upper(unsigned idx);
|
|
|
|
void get_lower(unsigned idx, expr_ref_vector& es) { to_exprs(get_lower_as_num(idx), es); }
|
|
void get_upper(unsigned idx, expr_ref_vector& es) { to_exprs(get_upper_as_num(idx), es); }
|
|
|
|
std::string to_string() const;
|
|
|
|
|
|
virtual unsigned num_objectives() { return m_scoped_state.m_objectives.size(); }
|
|
virtual expr_ref mk_gt(unsigned i, model_ref& model);
|
|
virtual expr_ref mk_ge(unsigned i, model_ref& model);
|
|
virtual expr_ref mk_le(unsigned i, model_ref& model);
|
|
|
|
virtual smt::context& smt_context() { return m_opt_solver->get_context(); }
|
|
virtual generic_model_converter& fm() { return *m_fm; }
|
|
virtual bool sat_enabled() const { return 0 != m_sat_solver.get(); }
|
|
virtual solver& get_solver();
|
|
virtual ast_manager& get_manager() const { return this->m; }
|
|
virtual params_ref& params() { return m_params; }
|
|
virtual void enable_sls(bool force);
|
|
virtual symbol const& maxsat_engine() const { return m_maxsat_engine; }
|
|
virtual void get_base_model(model_ref& _m);
|
|
|
|
|
|
virtual bool verify_model(unsigned id, model* mdl, rational const& v);
|
|
|
|
void get_lns_literals(expr_ref_vector& lits);
|
|
|
|
private:
|
|
lbool execute(objective const& obj, bool committed, bool scoped);
|
|
lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
|
|
lbool execute_maxsat(symbol const& s, bool committed, bool scoped);
|
|
lbool execute_lex();
|
|
lbool execute_box();
|
|
lbool execute_pareto();
|
|
lbool execute_lns();
|
|
lbool adjust_unknown(lbool r);
|
|
bool scoped_lex();
|
|
expr_ref to_expr(inf_eps const& n);
|
|
void to_exprs(inf_eps const& n, expr_ref_vector& es);
|
|
|
|
void reset_maxsmts();
|
|
void import_scoped_state();
|
|
void normalize();
|
|
void internalize();
|
|
bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
|
|
bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
|
|
bool is_maxsat(expr* fml, expr_ref_vector& terms,
|
|
vector<rational>& weights, rational& offset, bool& neg,
|
|
symbol& id, expr_ref& orig_term, unsigned& index);
|
|
void purify(app_ref& term);
|
|
app* purify(generic_model_converter_ref& fm, expr* e);
|
|
bool is_mul_const(expr* e);
|
|
expr* mk_maximize(unsigned index, app* t);
|
|
expr* mk_minimize(unsigned index, app* t);
|
|
expr* mk_maxsat(unsigned index, unsigned num_fmls, expr* const* fmls);
|
|
expr* mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args);
|
|
void to_fmls(expr_ref_vector& fmls);
|
|
void from_fmls(expr_ref_vector const& fmls);
|
|
void simplify_fmls(expr_ref_vector& fmls);
|
|
void mk_atomic(expr_ref_vector& terms);
|
|
|
|
void update_lower() { update_bound(true); }
|
|
void update_bound(bool is_lower);
|
|
|
|
inf_eps get_lower_as_num(unsigned idx);
|
|
inf_eps get_upper_as_num(unsigned idx);
|
|
|
|
|
|
struct is_bv;
|
|
bool probe_bv();
|
|
|
|
struct is_propositional_fn;
|
|
bool is_propositional(expr* e);
|
|
|
|
void init_solver();
|
|
void update_solver();
|
|
void setup_arith_solver();
|
|
void add_maxsmt(symbol const& id, unsigned index);
|
|
void set_simplify(tactic *simplify);
|
|
void set_pareto(pareto_base* p);
|
|
void clear_state();
|
|
|
|
bool is_numeral(expr* e, rational& n) const;
|
|
|
|
void display_objective(std::ostream& out, objective const& obj) const;
|
|
void display_bounds(std::ostream& out, bounds_t const& b) const;
|
|
|
|
std::string to_string(bool is_internal, expr_ref_vector const& hard, vector<objective> const& objectives) const;
|
|
std::string to_string_internal() const;
|
|
|
|
|
|
void validate_lex();
|
|
void validate_maxsat(symbol const& id);
|
|
void validate_model();
|
|
|
|
void display_benchmark();
|
|
|
|
// pareto
|
|
void yield();
|
|
expr_ref mk_ge(expr* t, expr* s);
|
|
expr_ref mk_cmp(bool is_ge, model_ref& mdl, objective const& obj);
|
|
|
|
|
|
// quantifiers
|
|
bool is_qsat_opt();
|
|
lbool run_qsat_opt();
|
|
};
|
|
|
|
}
|
|
|
|
#endif
|