[Optimization] support for push/pop (#6706)
authorOuyancheng <1024842937@qq.com>
Wed, 9 Jun 2021 15:53:16 +0000 (08:53 -0700)
committerGitHub <noreply@github.com>
Wed, 9 Jun 2021 15:53:16 +0000 (15:53 +0000)
commit0c982a7486ef9b6991589685f9091602e0cf5572
tree02a1aea361ee8643c962eb91a10ce37b4caf0824
parentcbb2fc4b1ec81fe5a3c00dbb030abc4631fe9db8
[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.
src/omt/integer_optimizer.h
src/omt/omt_optimizer.cpp
src/omt/omt_optimizer.h
src/smt/optimization_solver.cpp
src/smt/optimization_solver.h
test/unit/theory/theory_bv_opt_white.cpp
test/unit/theory/theory_int_opt_white.cpp
test/unit/theory/theory_opt_multigoal_white.cpp