From: Ouyancheng <1024842937@qq.com>
Date: Fri, 28 May 2021 21:00:16 +0000 (-0700)
Subject: (Optimization) remove popObjective, add resetObjectives, rename pushObjective =>... 
X-Git-Tag: cvc5-1.0.0~1676
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f62b46414cc47762857a4e3241318733ca8c973d;p=cvc5.git

(Optimization) remove popObjective, add resetObjectives, rename pushObjective => addObjective (#6634)

In order for OptimizationSolver to support pushing & popping,
we could remove popObjective because it might be difficult to handle cases like:

optSlv->pushObjective(...);
optSlv->push();
optSlv->popObjective();
optSlv->pop();
In this case we need to add back the popped objective...
If push/pop is supported, pop does not bring back objectives if you resetObjective
but it will revert the objs you add.
just like assertFormula and resetAssertions.
---

diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index 5f50c76c1..ffc49710a 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -55,24 +55,25 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt()
   Unreachable();
 }
 
-void OptimizationSolver::pushObjective(
-    TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned)
+void OptimizationSolver::addObjective(TNode target,
+                                      OptimizationObjective::ObjectiveType type,
+                                      bool bvSigned)
 {
   if (!OMTOptimizer::nodeSupportsOptimization(target))
   {
     CVC5_FATAL()
-        << "Objective not pushed: Target node does not support optimization";
+        << "Objective failed to add: Target node does not support optimization";
   }
   d_optChecker.reset();
   d_objectives.emplace_back(target, type, bvSigned);
   d_results.emplace_back(OptimizationResult::UNKNOWN, Node());
 }
 
-void OptimizationSolver::popObjective()
+void OptimizationSolver::resetObjectives()
 {
   d_optChecker.reset();
-  d_objectives.pop_back();
-  d_results.pop_back();
+  d_objectives.clear();
+  d_results.clear();
 }
 
 std::vector<OptimizationResult> OptimizationSolver::getValues()
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index b0f4de1c5..64591d8f1 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -171,12 +171,13 @@ class OptimizationSolver
    *   v_x = max(x) s.t. phi(x, y) = sat
    *   v_y = max(y) s.t. phi(x, y) = sat
    *
-   * Lexicographic: optimize the objectives one-by-one, in the order they push
-   *   v_x = max(x) s.t. phi(x, y) = sat
+   * Lexicographic: optimize the objectives one-by-one, in the order they are
+   * added:
+   *   v_x = max(x) s.t. phi(x, y) = sat 
    *   v_y = max(y) s.t. phi(v_x, y) = sat
    *
    * Pareto: optimize multiple goals to a state such that
-   *   further optimization of one goal will worsen the other goal(s)
+   * further optimization of one goal will worsen the other goal(s)
    *   (v_x, v_y) s.t. phi(v_x, v_y) = sat, and
    *     forall (x, y), (phi(x, y) = sat) -> (x <= v_x or y <= v_y)
    **/
@@ -194,7 +195,7 @@ class OptimizationSolver
   ~OptimizationSolver() = default;
 
   /**
-   * Run the optimization loop for the pushed objective
+   * 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)
@@ -202,22 +203,21 @@ class OptimizationSolver
   OptimizationResult::ResultType checkOpt();
 
   /**
-   * Push an objective.
-   * @param target the Node representing the expression that will be optimized
-   *for
+   * Add an optimization objective.
+   * @param target Node representing the expression that will be optimized for
    * @param type specifies whether it's maximize or minimize
    * @param bvSigned specifies whether we should use signed/unsigned
    *   comparison for BitVectors (only effective for BitVectors)
    *   and its default is false
    **/
-  void pushObjective(TNode target,
-                     OptimizationObjective::ObjectiveType type,
-                     bool bvSigned = false);
+  void addObjective(TNode target,
+                    OptimizationObjective::ObjectiveType type,
+                    bool bvSigned = false);
 
   /**
-   * Pop the most recently successfully-pushed objective.
+   * Clear all the added optimization objectives
    **/
-  void popObjective();
+  void resetObjectives();
 
   /**
    * Returns the values of the optimized objective after checkOpt is called
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index 42dcb9fee..66efe7eff 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -55,7 +55,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
 
-  d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false);
+  d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, (uint32_t)0x3FFFFFA1));
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, signed_min)
@@ -76,7 +76,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
 
-  d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, true);
+  d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -87,7 +87,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
 
   // expect the minimum x = -1
   ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000));
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
@@ -103,7 +103,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
 
-  d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, false);
+  d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -114,7 +114,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 2u));
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, signed_max)
@@ -128,7 +128,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
 
-  d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, true);
+  d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -137,7 +137,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
   // expect the maxmum x =
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 10u));
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, min_boundary)
@@ -152,7 +152,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
   // that existed previously
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
 
-  d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false);
+  d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -161,9 +161,8 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
   // expect the maximum x = 18
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 18u));
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
-
 }  // namespace test
 }  // namespace cvc5
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index efb963f16..f16db0c0e 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -60,7 +60,7 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   d_smtEngine->assertFormula(lowb);
 
   // We activate our objective so the subsolver knows to optimize it
-  d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
+  d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("99"));
 
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, min)
@@ -91,7 +91,7 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   d_smtEngine->assertFormula(lowb);
 
   // We activate our objective so the subsolver knows to optimize it
-  d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE);
+  d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -101,7 +101,7 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("1"));
 
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, result)
@@ -122,14 +122,14 @@ TEST_F(TestTheoryWhiteIntOpt, result)
   d_smtEngine->assertFormula(lowb);
 
   // We activate our objective so the subsolver knows to optimize it
-  d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
+  d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
   // This should return OPT_UNSAT since 0 > x > 100 is impossible.
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
   // We expect our check to have returned UNSAT
   ASSERT_EQ(r, OptimizationResult::UNSAT);
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, open_interval)
@@ -155,7 +155,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
   */
   Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2);
 
-  d_optslv->pushObjective(cost3, OptimizationObjective::MINIMIZE);
+  d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE);
 
   OptimizationResult::ResultType r = d_optslv->checkOpt();
 
@@ -164,7 +164,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
   // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("112"));
-  d_optslv->popObjective();
+  d_optslv->resetObjectives();
 }
 
 }  // namespace test
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index ed3de10a9..1950d9ae2 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -60,11 +60,11 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
   optSolver.setObjectiveCombination(OptimizationSolver::BOX);
 
   // minimize x
-  optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false);
+  optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
   // maximize y with `signed` comparison over bit-vectors.
-  optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true);
+  optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
   // maximize z
-  optSolver.pushObjective(z, OptimizationObjective::MAXIMIZE, false);
+  optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
   OptimizationResult::ResultType r = optSolver.checkOpt();
 
@@ -103,11 +103,11 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex)
   optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
 
   // minimize x
-  optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false);
+  optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
   // maximize y with `signed` comparison over bit-vectors.
-  optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true);
+  optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
   // maximize z
-  optSolver.pushObjective(z, OptimizationObjective::MAXIMIZE, false);
+  optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
   OptimizationResult::ResultType r = optSolver.checkOpt();
 
@@ -181,8 +181,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
    */
   OptimizationSolver optSolver(d_smtEngine.get());
   optSolver.setObjectiveCombination(OptimizationSolver::PARETO);
-  optSolver.pushObjective(a, OptimizationObjective::MAXIMIZE);
-  optSolver.pushObjective(b, OptimizationObjective::MAXIMIZE);
+  optSolver.addObjective(a, OptimizationObjective::MAXIMIZE);
+  optSolver.addObjective(b, OptimizationObjective::MAXIMIZE);
 
   OptimizationResult::ResultType r;