diff options
| author | Ouyancheng <1024842937@qq.com> | 2021-04-30 14:40:49 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-30 14:40:49 -0700 |
| commit | 67a1510b8e6306993d7efb7671b8f0aa53a45deb (patch) | |
| tree | 39745800f0d4ecdbb286516be26cd971db53cfd9 /src/omt/integer_optimizer.h | |
| parent | 327a24508ed1d02a3fa233e680ffd0b30aa685a9 (diff) | |
Refactor optimization result and objective classes + add preliminary support for multiple objectives (#6459)
This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.
* Refactor optimization result and objective classes
* Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses
Diffstat (limited to 'src/omt/integer_optimizer.h')
| -rw-r--r-- | src/omt/integer_optimizer.h | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h index d92bdb8eb..48d162494 100644 --- a/src/omt/integer_optimizer.h +++ b/src/omt/integer_optimizer.h @@ -28,19 +28,20 @@ class OMTOptimizerInteger : public OMTOptimizer public: OMTOptimizerInteger() = default; virtual ~OMTOptimizerInteger() = default; - std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver, - Node target) override; - std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver, - Node target) override; + smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + TNode target) override; + smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + TNode target) override; private: /** * Handles the optimization query specified by objType - * (objType = OBJECTIVE_MINIMIZE / OBJECTIVE_MAXIMIZE) + * (objType = MINIMIZE / MAXIMIZE) **/ - std::pair<smt::OptResult, Node> optimize(SmtEngine* parentSMTSolver, - Node target, - smt::ObjectiveType objType); + smt::OptimizationResult optimize( + SmtEngine* parentSMTSolver, + TNode target, + smt::OptimizationObjective::ObjectiveType objType); }; } // namespace cvc5::omt |