summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/optimization_solver.cpp13
-rw-r--r--src/smt/optimization_solver.h24
-rw-r--r--test/unit/theory/theory_bv_opt_white.cpp21
-rw-r--r--test/unit/theory/theory_int_opt_white.cpp16
-rw-r--r--test/unit/theory/theory_opt_multigoal_white.cpp16
5 files changed, 45 insertions, 45 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback