Age | Commit message (Collapse) | Author |
|
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.
|
|
Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.
|
|
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.
|
|
for multiple objectives (#6459)
This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.
* Refactor optimization result and objective classes
* Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses
|
|
|
|
Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
|