diff options
Diffstat (limited to 'src/smt/optimization_solver.h')
| -rw-r--r-- | src/smt/optimization_solver.h | 121 |
1 files changed, 63 insertions, 58 deletions
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 6d138deb2..d13168780 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -33,63 +33,75 @@ namespace smt { /** * The optimization result of an optimization objective * containing: - * - whether it's optimal or not - * - if so, the optimal value, otherwise the value might be empty node or - * something suboptimal + * - the optimization result: SAT/UNSAT/UNKNOWN + * - the optimal value if SAT and bounded + * (optimal value reached and it's not infinity), + * or an empty node if SAT and unbounded + * (optimal value is +inf for maximum or -inf for minimum), + * otherwise the value might be empty node + * or something suboptimal + * - whether the objective is unbounded */ class OptimizationResult { public: /** - * Enum indicating whether the checkOpt result - * is optimal or not. - **/ - enum ResultType - { - // whether the value is optimal is UNKNOWN - UNKNOWN, - // the original set of assertions has result UNSAT - UNSAT, - // the value is optimal - OPTIMAL, - // the goal is unbounded, - // if objective is maximize, it's +infinity - // if objective is minimize, it's -infinity - UNBOUNDED, - }; - - /** * Constructor * @param type the optimization outcome * @param value the optimized value + * @param unbounded whether the objective is unbounded **/ - OptimizationResult(ResultType type, TNode value) - : d_type(type), d_value(value) + OptimizationResult(Result result, TNode value, bool unbounded = false) + : d_result(result), d_value(value), d_unbounded(unbounded) + { + } + OptimizationResult() + : d_result(Result::Sat::SAT_UNKNOWN, + Result::UnknownExplanation::NO_STATUS), + d_value(), + d_unbounded(false) { } - OptimizationResult() : d_type(UNKNOWN), d_value() {} ~OptimizationResult() = default; /** * Returns an enum indicating whether - * the result is optimal or not. - * @return an enum showing whether the result is optimal, unbounded, - * unsat or unknown. + * the result is SAT or not. + * @return whether the result is SAT, UNSAT or SAT_UNKNOWN **/ - ResultType getType() const { return d_type; } + Result getResult() const { return d_result; } + /** * Returns the optimal value. * @return Node containing the optimal value, - * if getType() is not OPTIMAL, it might return an empty node or a node - * containing non-optimal value + * if result is unbounded, this will be an empty node, + * if getResult() is UNSAT, it will return an empty node, + * if getResult() is SAT_UNKNOWN, it will return something suboptimal + * or an empty node, depending on how the solver runs. **/ Node getValue() const { return d_value; } + /** + * Checks whether the objective is unbouned + * @return whether the objective is unbounded + * if the objective is unbounded (this function returns true), + * then the optimal value is: + * +inf, if it's maximize; + * -inf, if it's minimize + **/ + bool isUnbounded() const { return d_unbounded; } + private: - /** the indicating whether the result is optimal or something else **/ - ResultType d_type; - /** if the result is optimal, this is storing the optimal value **/ + /** indicating whether the result is SAT, UNSAT or UNKNOWN **/ + Result d_result; + /** if the result is bounded, this is storing the value **/ Node d_value; + /** whether the objective is unbounded + * If this is true, then: + * if objective is maximize, it's +infinity; + * if objective is minimize, it's -infinity + **/ + bool d_unbounded; }; /** @@ -199,10 +211,10 @@ class OptimizationSolver /** * Run the optimization loop for the added objective * For multiple objective combination, it defaults to lexicographic, - * and combination could be set by calling - * setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO) + * possible combinations: BOX, LEXICOGRAPHIC, PARETO + * @param combination BOX / LEXICOGRAPHIC / PARETO */ - OptimizationResult::ResultType checkOpt(); + Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC); /** * Add an optimization objective. @@ -223,11 +235,6 @@ class OptimizationSolver **/ std::vector<OptimizationResult> getValues(); - /** - * Sets the objective combination - **/ - void setObjectiveCombination(ObjectiveCombination combination); - private: /** * Initialize an SMT subsolver for offline optimization purpose @@ -244,26 +251,26 @@ class OptimizationSolver /** * Optimize multiple goals in Box order - * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED; - * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN; - * UNKNOWN if any of the objective is UNKNOWN. + * @return SAT if all of the objectives are optimal or unbounded; + * UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN; + * SAT_UNKNOWN if any of the objective is SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeBox(); + Result optimizeBox(); /** * Optimize multiple goals in Lexicographic order, * using iterative implementation - * @return OPTIMAL if all objectives are OPTIMAL and bounded; - * UNBOUNDED if one of the objectives is UNBOUNDED + * @return SAT if the objectives are optimal, + * if one of the objectives is unbounded, + * the optimization will stop at that objective; + * UNSAT if any of the objectives is UNSAT * and optimization will stop at that objective; - * UNSAT if one of the objectives is UNSAT - * and optimization will stop at that objective; - * UNKNOWN if one of the objectives is UNKNOWN + * SAT_UNKNOWN if any of the objectives is UNKNOWN * and optimization will stop at that objective; * If the optimization is stopped at an objective, - * all objectives following that objective will be UNKNOWN. + * all objectives following that objective will be SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeLexicographicIterative(); + Result optimizeLexicographicIterative(); /** * Optimize multiple goals in Pareto order @@ -277,11 +284,12 @@ class OptimizationSolver * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm. * Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009. * - * @return if it finds a new Pareto optimal result it will return OPTIMAL; + * @return if it finds a new Pareto optimal result it will return SAT; * if it exhausts the results in the Pareto front it will return UNSAT; - * if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN. + * if the underlying SMT solver returns SAT_UNKNOWN, + * it will return SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeParetoNaiveGIA(); + Result optimizeParetoNaiveGIA(); /** A pointer to the parent SMT engine **/ SmtEngine* d_parent; @@ -294,9 +302,6 @@ class OptimizationSolver /** The results of the optimizations from the last checkOpt call **/ std::vector<OptimizationResult> d_results; - - /** The current objective combination method **/ - ObjectiveCombination d_objectiveCombination; }; } // namespace smt |