projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8b3de13) | patch
Add Lexicographic + Pareto Optimizations (#6626)
authorOuyancheng <1024842937@qq.com>
Thu, 27 May 2021 22:02:48 +0000 (15:02 -0700)
committerGitHub <noreply@github.com>
Thu, 27 May 2021 22:02:48 +0000 (22:02 +0000)
commit631032b15327c28c44b51490dceb434a38f3419a
tree047fd4ea2d87af473ce68b998d89bf52f6daeacdtree
parent8b3de13131d24bf400ba5f36fc234008d950f345commit | diff
Add Lexicographic + Pareto Optimizations (#6626)

Lexicographic optimizations: Optimize the objectives one-by-one, in the order they are pushed.
Pareto optimizations: Optimize the objectives to the extend that further optimization on any objective will worsen the other objective.
Units tests are of course added.

Lexicographic optimization is using iterative implementation, pretty similar to the naive box optimization.
src/smt/optimization_solver.cpp diff | blob | history
src/smt/optimization_solver.h diff | blob | history
test/unit/theory/theory_opt_multigoal_white.cpp diff | blob | history