diff options
author | Ouyancheng <1024842937@qq.com> | 2021-05-04 17:34:54 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-05 00:34:54 +0000 |
commit | f9eee2d3a33c38bec3efb5dda91d43ef55c992d7 (patch) | |
tree | 9e0bac7b510d15a20cd497a783ed47277f46abb7 /src/smt | |
parent | 8a7c43f82b17a444c2f9518bc27f4ea8afe21201 (diff) |
Add helper functions for multi-objective optimization + refactoring (#6473)
add 3 helper functions
judge whether a node is optimizable
make strong improvement expression according to optimization objective
make weak improvement expression according to optimization objective
optChecker is now created by optimizationSolver instead of the minimize/maximize functions
Slightly refactors function signatures so that they are accepting OptimizationObjective instead of accepting target, type in separate parameters.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/optimization_solver.cpp | 34 | ||||
-rw-r--r-- | src/smt/optimization_solver.h | 13 |
2 files changed, 43 insertions, 4 deletions
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 1c8fe6514..e66e4e2ca 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -16,7 +16,10 @@ #include "smt/optimization_solver.h" #include "omt/omt_optimizer.h" +#include "options/smt_options.h" #include "smt/assertions.h" +#include "smt/smt_engine.h" +#include "theory/smt_engine_subsolver.h" using namespace cvc5::theory; using namespace cvc5::omt; @@ -27,19 +30,22 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt() { Assert(d_objectives.size() == 1); // NOTE: currently we are only dealing with single obj - std::unique_ptr<OMTOptimizer> optimizer = OMTOptimizer::getOptimizerForNode( - d_objectives[0].getTarget(), d_objectives[0].bvIsSigned()); + std::unique_ptr<OMTOptimizer> optimizer = + OMTOptimizer::getOptimizerForObjective(d_objectives[0]); if (!optimizer) return OptimizationResult::UNSUPPORTED; OptimizationResult optResult; + std::unique_ptr<SmtEngine> optChecker = createOptCheckerWithTimeout(d_parent); if (d_objectives[0].getType() == OptimizationObjective::MAXIMIZE) { - optResult = optimizer->maximize(d_parent, d_objectives[0].getTarget()); + optResult = + optimizer->maximize(optChecker.get(), d_objectives[0].getTarget()); } else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE) { - optResult = optimizer->minimize(d_parent, d_objectives[0].getTarget()); + optResult = + optimizer->minimize(optChecker.get(), d_objectives[0].getTarget()); } d_results[0] = optResult; @@ -65,5 +71,25 @@ std::vector<OptimizationResult> OptimizationSolver::getValues() return d_results; } +std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout( + SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) +{ + std::unique_ptr<SmtEngine> optChecker; + // initializeSubSolver will copy the options and theories enabled + // from the current solver to optChecker and adds timeout + theory::initializeSubsolver(optChecker, needsTimeout, timeout); + // we need to be in incremental mode for multiple objectives since we need to + // push pop we need to produce models to inrement on our objective + optChecker->setOption("incremental", "true"); + optChecker->setOption("produce-models", "true"); + // Move assertions from the parent solver to the subsolver + std::vector<Node> p_assertions = parentSMTSolver->getExpandedAssertions(); + for (const Node& e : p_assertions) + { + optChecker->assertFormula(e); + } + return optChecker; +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 0babd7a4a..3037c2924 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -208,6 +208,19 @@ class OptimizationSolver std::vector<OptimizationResult> getValues(); private: + /** + * Initialize an SMT subsolver for offline optimization purpose + * @param parentSMTSolver the parental solver containing the assertions + * @param needsTimeout specifies whether it needs timeout for each single + * query + * @param timeout the timeout value, given in milliseconds (ms) + * @return a unique_pointer of SMT subsolver + **/ + static std::unique_ptr<SmtEngine> createOptCheckerWithTimeout( + SmtEngine* parentSMTSolver, + bool needsTimeout = false, + unsigned long timeout = 0); + /** The parent SMT engine **/ SmtEngine* d_parent; |