projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cd38664) | patch
Add support for Box optimization (#6599)
authorOuyancheng <1024842937@qq.com>
Thu, 27 May 2021 07:53:58 +0000 (00:53 -0700)
committerGitHub <noreply@github.com>
Thu, 27 May 2021 07:53:58 +0000 (07:53 +0000)
commit7120cf46b38f0bede1ab8d17453ae925aa2d27fd
treeb22e054d08f0312b12b6fc62a37eb2497f8d16a6tree
parentcd386643b1113c92775950b3683c2b48f7f2bf13commit | diff
Add support for Box optimization (#6599)

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.
src/omt/bitvector_optimizer.cpp diff | blob | history
src/omt/integer_optimizer.cpp diff | blob | history
src/omt/omt_optimizer.cpp diff | blob | history
src/smt/optimization_solver.cpp diff | blob | history
src/smt/optimization_solver.h diff | blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/theory_bv_opt_white.cpp diff | blob | history
test/unit/theory/theory_int_opt_white.cpp diff | blob | history
test/unit/theory/theory_opt_multigoal_white.cpp [new file with mode: 0644] blob