diff options
author | Ouyancheng <1024842937@qq.com> | 2021-06-09 08:53:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-09 15:53:16 +0000 |
commit | 0c982a7486ef9b6991589685f9091602e0cf5572 (patch) | |
tree | 02a1aea361ee8643c962eb91a10ce37b4caf0824 /src | |
parent | cbb2fc4b1ec81fe5a3c00dbb030abc4631fe9db8 (diff) |
[Optimization] support for push/pop (#6706)
Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop).
SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function.
Diffstat (limited to 'src')
-rw-r--r-- | src/omt/integer_optimizer.h | 9 | ||||
-rw-r--r-- | src/omt/omt_optimizer.cpp | 16 | ||||
-rw-r--r-- | src/omt/omt_optimizer.h | 6 | ||||
-rw-r--r-- | src/smt/optimization_solver.cpp | 20 | ||||
-rw-r--r-- | src/smt/optimization_solver.h | 21 |
5 files changed, 35 insertions, 37 deletions
diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h index 34605cc71..0b62c0816 100644 --- a/src/omt/integer_optimizer.h +++ b/src/omt/integer_optimizer.h @@ -36,13 +36,12 @@ class OMTOptimizerInteger : public OMTOptimizer private: /** * Handles the optimization query specified by objType - * isMinimize = true will trigger minimization, + * isMinimize = true will trigger minimization, * otherwise trigger maximization **/ - smt::OptimizationResult optimize( - SmtEngine* optChecker, - TNode target, - bool isMinimize); + smt::OptimizationResult optimize(SmtEngine* optChecker, + TNode target, + bool isMinimize); }; } // namespace cvc5::omt diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index 08f1809ec..2145492db 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -30,7 +30,7 @@ bool OMTOptimizer::nodeSupportsOptimization(TNode node) } std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective( - OptimizationObjective& objective) + const OptimizationObjective& objective) { // the datatype of the target node TypeNode objectiveType = objective.getTarget().getType(true); @@ -53,7 +53,10 @@ std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective( } Node OMTOptimizer::mkStrongIncrementalExpression( - NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective) + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " @@ -114,10 +117,11 @@ Node OMTOptimizer::mkStrongIncrementalExpression( Unreachable(); } -Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, - TNode lhs, - TNode rhs, - OptimizationObjective& objective) +Node OMTOptimizer::mkWeakIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h index 1052865b0..1e8d9e763 100644 --- a/src/omt/omt_optimizer.h +++ b/src/omt/omt_optimizer.h @@ -46,7 +46,7 @@ class OMTOptimizer * and this is the optimizer for targetNode **/ static std::unique_ptr<OMTOptimizer> getOptimizerForObjective( - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Given the lhs and rhs expressions, with an optimization objective, @@ -70,7 +70,7 @@ class OMTOptimizer NodeManager* nm, TNode lhs, TNode rhs, - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Given the lhs and rhs expressions, with an optimization objective, @@ -94,7 +94,7 @@ class OMTOptimizer NodeManager* nm, TNode lhs, TNode rhs, - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Minimize the target node with constraints encoded in optChecker diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index ffc49710a..e85ea82ef 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -15,6 +15,8 @@ #include "smt/optimization_solver.h" +#include "context/cdhashmap.h" +#include "context/cdlist.h" #include "omt/omt_optimizer.h" #include "options/smt_options.h" #include "smt/assertions.h" @@ -29,7 +31,7 @@ namespace smt { OptimizationSolver::OptimizationSolver(SmtEngine* parent) : d_parent(parent), d_optChecker(), - d_objectives(), + d_objectives(parent->getUserContext()), d_results(), d_objectiveCombination(LEXICOGRAPHIC) { @@ -37,10 +39,14 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent) OptimizationResult::ResultType OptimizationSolver::checkOpt() { + // if the results of the previous call have different size than the + // objectives, then we should clear the pareto optimization context + if (d_results.size() != d_objectives.size()) d_optChecker.reset(); + // initialize the result vector + d_results.clear(); for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { - // reset the optimization results - d_results[i] = OptimizationResult(); + d_results.emplace_back(); } switch (d_objectiveCombination) { @@ -66,14 +72,6 @@ void OptimizationSolver::addObjective(TNode target, } d_optChecker.reset(); d_objectives.emplace_back(target, type, bvSigned); - d_results.emplace_back(OptimizationResult::UNKNOWN, Node()); -} - -void OptimizationSolver::resetObjectives() -{ - d_optChecker.reset(); - 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 64591d8f1..6d138deb2 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -18,6 +18,8 @@ #ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H #define CVC5__SMT__OPTIMIZATION_SOLVER_H +#include "context/cdhashmap_forward.h" +#include "context/cdlist.h" #include "expr/node.h" #include "expr/type_node.h" #include "util/result.h" @@ -74,14 +76,14 @@ class OptimizationResult * @return an enum showing whether the result is optimal, unbounded, * unsat or unknown. **/ - ResultType getType() { return d_type; } + ResultType getType() const { return d_type; } /** * Returns the optimal value. * @return Node containing the optimal value, * if getType() is not OPTIMAL, it might return an empty node or a node * containing non-optimal value **/ - Node getValue() { return d_value; } + Node getValue() const { return d_value; } private: /** the indicating whether the result is optimal or something else **/ @@ -124,13 +126,13 @@ class OptimizationObjective ~OptimizationObjective() = default; /** A getter for d_type **/ - ObjectiveType getType() { return d_type; } + ObjectiveType getType() const { return d_type; } /** A getter for d_target **/ - Node getTarget() { return d_target; } + Node getTarget() const { return d_target; } /** A getter for d_bvSigned **/ - bool bvIsSigned() { return d_bvSigned; } + bool bvIsSigned() const { return d_bvSigned; } private: /** @@ -173,7 +175,7 @@ class OptimizationSolver * * Lexicographic: optimize the objectives one-by-one, in the order they are * added: - * v_x = max(x) s.t. phi(x, y) = sat + * 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 @@ -215,11 +217,6 @@ class OptimizationSolver bool bvSigned = false); /** - * Clear all the added optimization objectives - **/ - void resetObjectives(); - - /** * Returns the values of the optimized objective after checkOpt is called * @return a vector of Optimization Result, * each containing the outcome and the value. @@ -293,7 +290,7 @@ class OptimizationSolver std::unique_ptr<SmtEngine> d_optChecker; /** The objectives to optimize for **/ - std::vector<OptimizationObjective> d_objectives; + context::CDList<OptimizationObjective> d_objectives; /** The results of the optimizations from the last checkOpt call **/ std::vector<OptimizationResult> d_results; |