1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6     optsmt.h
7 
8 Abstract:
9 
10     Objective optimization method.
11 
12 Author:
13 
14     Anh-Dung Phan (t-anphan) 2013-10-16
15 
16 Notes:
17 
18 --*/
19 #pragma once
20 
21 #include "opt/opt_solver.h"
22 
23 namespace opt {
24     /**
25        Takes solver with hard constraints added.
26        Returns an optimal assignment to objective functions.
27     */
28 
29     class context;
30 
31     class optsmt {
32         ast_manager&     m;
33         context&         m_context;
34         opt_solver*      m_s;
35         vector<inf_eps>  m_lower;
36         vector<inf_eps>  m_upper;
37         app_ref_vector   m_objs;
38         expr_ref_vector  m_lower_fmls;
39         svector<smt::theory_var> m_vars;
40         symbol           m_optsmt_engine;
41         model_ref        m_model, m_best_model;
42         svector<symbol>  m_labels;
43         sref_vector<model> m_models;
44     public:
optsmt(ast_manager & m,context & ctx)45         optsmt(ast_manager& m, context& ctx):
46             m(m), m_context(ctx), m_s(nullptr), m_objs(m), m_lower_fmls(m) {}
47 
48         void setup(opt_solver& solver);
49 
50         lbool box();
51 
52         lbool lex(unsigned obj_index, bool is_maximize);
53 
54         bool is_unbounded(unsigned obj_index, bool is_maximize);
55 
56         unsigned add(app* t);
57 
58         void updt_params(params_ref& p);
59 
get_num_objectives()60         unsigned get_num_objectives() const { return m_objs.size(); }
61         void commit_assignment(unsigned index);
62         inf_eps get_lower(unsigned index) const;
63         inf_eps get_upper(unsigned index) const;
64         void    get_model(model_ref& mdl, svector<symbol>& labels);
get_model(unsigned index)65         model*  get_model(unsigned index) const { return m_models[index]; }
66 
67 
68         void update_lower(unsigned idx, inf_eps const& r);
69 
70         void update_upper(unsigned idx, inf_eps const& r);
71 
72         void reset();
73 
74         lbool basic_opt();
75 
76         bool can_increment_delta(vector<inf_eps> const& lower, unsigned i);
77 
78     private:
79 
80         lbool geometric_opt();
81 
82         lbool symba_opt();
83 
84         lbool geometric_lex(unsigned idx, bool is_maximize);
85 
86         void set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls);
87 
88         expr_ref update_lower();
89 
90         void update_lower_lex(unsigned idx, inf_eps const& r, bool is_maximize);
91 
92         lbool update_upper();
93 
94     };
95 
96 };
97 
98