(Optimization) remove popObjective, add resetObjectives, rename pushObjective =>...
authorOuyancheng <1024842937@qq.com>
Fri, 28 May 2021 21:00:16 +0000 (14:00 -0700)
committerGitHub <noreply@github.com>
Fri, 28 May 2021 21:00:16 +0000 (21:00 +0000)
commitf62b46414cc47762857a4e3241318733ca8c973d
tree5e69ae109fb2a0223b6722c2ec8352b164e4e54c
parent40089fc79491a0608f36e6af9db69d2c12c37e3e
(Optimization) remove popObjective, add resetObjectives, rename pushObjective => addObjective (#6634)

In order for OptimizationSolver to support pushing & popping,
we could remove popObjective because it might be difficult to handle cases like:

optSlv->pushObjective(...);
optSlv->push();
optSlv->popObjective();
optSlv->pop();
In this case we need to add back the popped objective...
If push/pop is supported, pop does not bring back objectives if you resetObjective
but it will revert the objs you add.
just like assertFormula and resetAssertions.
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