[Optimization] Use Result in OptimizationResult (#6740)

OptimizationResult now contains: 
- cvc5::Result
- optimal value for objective
- whether the objective is unbounded

This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API. 

Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)... 

3 files changed, 39 insertions, 46 deletions

diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index c23ce79dd..5cd29878e 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -57,9 +57,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
 
   d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, (uint32_t)0x3FFFFFA1));
@@ -78,9 +78,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
 
   d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
   std::cout << "opt value is: " << val << std::endl;
@@ -105,9 +105,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
 
   d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
   std::cout << "opt value is: " << val << std::endl;
@@ -130,9 +130,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
 
   d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // expect the maxmum x =
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
@@ -154,9 +154,9 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
 
   d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // expect the maximum x = 18
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index cf0434ddc..583f908e7 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -62,9 +62,9 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // We expect max_cost == 99
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
@@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // We expect max_cost == 99
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
@@ -125,10 +125,10 @@ TEST_F(TestTheoryWhiteIntOpt, result)
   d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
   // This should return OPT_UNSAT since 0 > x > 100 is impossible.
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
   // We expect our check to have returned UNSAT
-  ASSERT_EQ(r, OptimizationResult::UNSAT);
+  ASSERT_EQ(r.isSat(), Result::UNSAT);
   d_smtEngine->resetAssertions();
 }
 
@@ -157,9 +157,9 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
 
   d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE);
 
-  OptimizationResult::ResultType r = d_optslv->checkOpt();
+  Result r = d_optslv->checkOpt();
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index 73c6d9e7e..9a091fb3b 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -54,11 +54,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
   // y <= x
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
 
-  // Box optimization
   OptimizationSolver optSolver(d_smtEngine.get());
 
-  optSolver.setObjectiveCombination(OptimizationSolver::BOX);
-
   // minimize x
   optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
   // maximize y with `signed` comparison over bit-vectors.
@@ -66,9 +63,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
   // maximize z
   optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = optSolver.checkOpt();
+  // Box optimization
+  Result r = optSolver.checkOpt(OptimizationSolver::BOX);
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   std::vector<OptimizationResult> results = optSolver.getValues();
 
@@ -100,8 +98,6 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex)
 
   OptimizationSolver optSolver(d_smtEngine.get());
 
-  optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
-
   // minimize x
   optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
   // maximize y with `signed` comparison over bit-vectors.
@@ -109,9 +105,9 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex)
   // maximize z
   optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = optSolver.checkOpt();
+  Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   std::vector<OptimizationResult> results = optSolver.getValues();
 
@@ -180,18 +176,17 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
     (maximize b)
    */
   OptimizationSolver optSolver(d_smtEngine.get());
-  optSolver.setObjectiveCombination(OptimizationSolver::PARETO);
   optSolver.addObjective(a, OptimizationObjective::MAXIMIZE);
   optSolver.addObjective(b, OptimizationObjective::MAXIMIZE);
 
-  OptimizationResult::ResultType r;
+  Result r;
 
   // all possible result pairs <a, b>
   std::set<std::pair<uint32_t, uint32_t>> possibleResults = {
       {1, 3}, {2, 2}, {3, 1}};
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   std::vector<OptimizationResult> results = optSolver.getValues();
   std::pair<uint32_t, uint32_t> res = {
       results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -205,8 +200,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.count(res), 1);
   possibleResults.erase(res);
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   res = {
       results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -220,8 +215,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.count(res), 1);
   possibleResults.erase(res);
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   res = {
       results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -235,8 +230,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.count(res), 1);
   possibleResults.erase(res);
 
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::UNSAT);
+  r = optSolver.checkOpt(OptimizationSolver::PARETO);
+  ASSERT_EQ(r.isSat(), Result::UNSAT);
   ASSERT_EQ(possibleResults.size(), 0);
 }
 
@@ -254,11 +249,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
   // y <= x
   d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
 
-  // Lexico optimization
   OptimizationSolver optSolver(d_smtEngine.get());
 
-  optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
-
   // minimize x
   optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
 
@@ -270,9 +262,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
   // maximize z
   optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
 
-  OptimizationResult::ResultType r = optSolver.checkOpt();
+  // Lexico optimization
+  Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
 
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  ASSERT_EQ(r.isSat(), Result::SAT);
 
   std::vector<OptimizationResult> results = optSolver.getValues();
 
@@ -290,16 +283,16 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
   d_smtEngine->pop();
 
   // now we only have one objective: (minimize x)
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   ASSERT_EQ(results.size(), 1);
   ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
 
   // resetting the assertions also resets the optimization objectives
   d_smtEngine->resetAssertions();
-  r = optSolver.checkOpt();
-  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
+  ASSERT_EQ(r.isSat(), Result::SAT);
   results = optSolver.getValues();
   ASSERT_EQ(results.size(), 0);
 }