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.

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;