From b573b94f84b0b75560a8c61227794c5692280180 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Nov 2013 21:59:38 -0800 Subject: [PATCH] nits Signed-off-by: Nikolaj Bjorner --- src/opt/fu_malik.cpp | 2 +- src/opt/opt_context.cpp | 4 ++-- src/opt/opt_context.h | 5 +++-- src/opt/opt_solver.h | 7 ------- src/opt/optsmt.cpp | 10 ++-------- src/opt/optsmt.h | 6 +++--- src/opt/weighted_maxsat.cpp | 2 +- src/solver/solver.h | 8 ++++++++ 8 files changed, 20 insertions(+), 24 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 6bfe1d5cc..725fa6072 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -138,7 +138,7 @@ namespace opt { lbool operator()() { lbool is_sat = s.check_sat(0,0); if (!m_soft.empty() && is_sat == l_true) { - opt_solver::scoped_push _sp(s); + solver::scoped_push _sp(s); lbool is_sat = l_true; do { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 7808a3d0c..2c64f8277 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -51,13 +51,13 @@ namespace opt { } lbool context::optimize() { - // TBD: add configurtion parameter + // TBD: add configuration parameter to select between box and pareto return optimize_box(); } lbool context::optimize_box() { opt_solver& s = *m_solver.get(); - opt_solver::scoped_push _sp(s); + solver::scoped_push _sp(s); for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { s.assert_expr(m_hard_constraints[i].get()); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 15f59efc8..c54259115 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -49,8 +49,6 @@ namespace opt { void add_objective(app* t, bool is_max) { m_optsmt.add(t, is_max); } void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); } lbool optimize(); - lbool optimize_pareto(); - lbool optimize_box(); void set_cancel(bool f); void reset_cancel() { set_cancel(false); } void cancel() { set_cancel(true); } @@ -59,6 +57,9 @@ namespace opt { void display_range_assignment(std::ostream& out); static void collect_param_descrs(param_descrs & r); void updt_params(params_ref& p); + private: + lbool optimize_pareto(); + lbool optimize_box(); }; } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index fa9a5e031..1fffa1b5b 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -85,13 +85,6 @@ namespace opt { ~toggle_objective(); }; - class scoped_push { - solver& s; - public: - scoped_push(solver& s):s(s) { s.push(); } - ~scoped_push() { s.pop(1); } - }; - smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat. smt::theory_opt& get_optimizer(); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 1d3aa1f77..e291b76a5 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -37,8 +37,6 @@ Notes: --*/ -#ifndef _OPT_OBJECTIVE_H_ -#define _OPT_OBJECTIVE_H_ #include "optsmt.h" #include "opt_solver.h" @@ -90,7 +88,6 @@ namespace opt { lbool optsmt::farkas_opt() { smt::theory_opt& opt = s->get_optimizer(); - IF_VERBOSE(1, verbose_stream() << typeid(opt).name() << "\n";); if (typeid(smt::theory_inf_arith) != typeid(opt)) { return l_undef; } @@ -138,7 +135,7 @@ namespace opt { expr_ref bound(m); expr_ref_vector bounds(m); - opt_solver::scoped_push _push(*s); + solver::scoped_push _push(*s); // // NB: we have to create all bound expressions before calling check_sat @@ -218,7 +215,7 @@ namespace opt { // First check_sat call to initialize theories lbool is_sat = s->check_sat(0, 0); if (is_sat == l_true && !m_objs.empty()) { - opt_solver::scoped_push _push(*s); + solver::scoped_push _push(*s); for (unsigned i = 0; i < m_objs.size(); ++i) { m_vars.push_back(s->add_objective(m_objs[i].get())); @@ -289,8 +286,6 @@ namespace opt { } } - - void optsmt::add(app* t, bool is_max) { expr_ref t1(t, m), t2(m); th_rewriter rw(m); @@ -311,4 +306,3 @@ namespace opt { } -#endif diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 2dae59a4f..189da0e0e 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -16,8 +16,8 @@ Author: Notes: --*/ -#ifndef _OPT_OBJECTIVES_H_ -#define _OPT_OBJECTIVES_H_ +#ifndef _OPTSMT_H_ +#define _OPTSMT_H_ #include "opt_solver.h" @@ -52,7 +52,7 @@ namespace opt { void display_range_assignment(std::ostream& out) const; unsigned get_num_objectives() const { return m_vars.size(); } - void commit_assignment(unsigned i); + void commit_assignment(unsigned index); inf_eps get_value(unsigned index) const; inf_eps get_lower(unsigned index) const; inf_eps get_upper(unsigned index) const; diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index a03d60ae1..206117224 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -315,7 +315,7 @@ namespace opt { smt::theory_weighted_maxsat& wth = ensure_theory(); lbool result; { - opt_solver::scoped_push _s(s); + solver::scoped_push _s(s); for (unsigned i = 0; i < m_soft.size(); ++i) { wth.assert_weighted(m_soft[i].get(), m_weights[i]); } diff --git a/src/solver/solver.h b/src/solver/solver.h index e047bace1..bd1a26adb 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -130,6 +130,14 @@ public: \brief Display the content of this solver. */ virtual void display(std::ostream & out) const; + + class scoped_push { + solver& s; + public: + scoped_push(solver& s):s(s) { s.push(); } + ~scoped_push() { s.pop(1); } + }; + }; #endif