mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b573b94f84
commit
ba05f79415
|
@ -28,6 +28,7 @@ namespace opt {
|
|||
lbool is_sat;
|
||||
m_answer.reset();
|
||||
m_msolver = 0;
|
||||
m_s = &s;
|
||||
if (m_soft_constraints.empty()) {
|
||||
m_msolver = 0;
|
||||
is_sat = s.check_sat(0, 0);
|
||||
|
@ -80,8 +81,9 @@ namespace opt {
|
|||
}
|
||||
|
||||
void maxsmt::commit_assignment() {
|
||||
SASSERT(m_s);
|
||||
for (unsigned i = 0; i < m_answer.size(); ++i) {
|
||||
s->assert_expr(m_answer[i].get());
|
||||
m_s->assert_expr(m_answer[i].get());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -41,14 +41,14 @@ namespace opt {
|
|||
|
||||
class maxsmt {
|
||||
ast_manager& m;
|
||||
solver* s;
|
||||
solver* m_s;
|
||||
volatile bool m_cancel;
|
||||
expr_ref_vector m_soft_constraints;
|
||||
expr_ref_vector m_answer;
|
||||
vector<rational> m_weights;
|
||||
scoped_ptr<maxsmt_solver> m_msolver;
|
||||
public:
|
||||
maxsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
|
||||
maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
|
||||
|
||||
lbool operator()(solver& s);
|
||||
|
||||
|
|
|
@ -51,8 +51,13 @@ namespace opt {
|
|||
}
|
||||
|
||||
lbool context::optimize() {
|
||||
// TBD: add configuration parameter to select between box and pareto
|
||||
return optimize_box();
|
||||
// TBD: does not work...
|
||||
if (m_params.get_bool("pareto", false)) {
|
||||
return optimize_pareto();
|
||||
}
|
||||
else {
|
||||
return optimize_box();
|
||||
}
|
||||
}
|
||||
|
||||
lbool context::optimize_box() {
|
||||
|
|
|
@ -3,6 +3,7 @@ def_module_params('opt',
|
|||
export=True,
|
||||
params=(('timeout', UINT, UINT_MAX, 'set timeout'),
|
||||
('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
|
||||
('pareto', BOOL, False, 'return a Pareto front (as opposed to a bounding box)'),
|
||||
))
|
||||
|
||||
|
||||
|
|
|
@ -204,13 +204,7 @@ namespace opt {
|
|||
lbool optsmt::operator()(opt_solver& solver) {
|
||||
s = &solver;
|
||||
s->reset_objectives();
|
||||
m_lower.reset();
|
||||
m_upper.reset();
|
||||
m_vars.reset();
|
||||
for (unsigned i = 0; i < m_objs.size(); ++i) {
|
||||
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
|
||||
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
|
||||
}
|
||||
|
||||
// First check_sat call to initialize theories
|
||||
lbool is_sat = s->check_sat(0, 0);
|
||||
|
@ -297,6 +291,8 @@ namespace opt {
|
|||
SASSERT(is_app(t2));
|
||||
m_objs.push_back(to_app(t2));
|
||||
m_is_max.push_back(is_max);
|
||||
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
|
||||
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
|
||||
}
|
||||
|
||||
void optsmt::updt_params(params_ref& p) {
|
||||
|
|
|
@ -51,7 +51,7 @@ namespace opt {
|
|||
void display_assignment(std::ostream& out) const;
|
||||
void display_range_assignment(std::ostream& out) const;
|
||||
|
||||
unsigned get_num_objectives() const { return m_vars.size(); }
|
||||
unsigned get_num_objectives() const { return m_objs.size(); }
|
||||
void commit_assignment(unsigned index);
|
||||
inf_eps get_value(unsigned index) const;
|
||||
inf_eps get_lower(unsigned index) const;
|
||||
|
|
Loading…
Reference in a new issue