[Optimization] Use Result in OptimizationResult (#6740)
authorOuyancheng <1024842937@qq.com>
Tue, 15 Jun 2021 23:20:20 +0000 (16:20 -0700)
committerGitHub <noreply@github.com>
Tue, 15 Jun 2021 23:20:20 +0000 (23:20 +0000)
commitc299e8661f24d3a6acb736e9e5df1b1920488ac3
tree3c662e58fe01fc44996d3dd8cf622be25ef5ce32
parent4ca14e808d788ef9570dda1188645783c6a11e70
[Optimization] Use Result in OptimizationResult (#6740)

OptimizationResult now contains:
- cvc5::Result
- optimal value for objective
- whether the objective is unbounded

This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API.

Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)...
src/omt/bitvector_optimizer.cpp
src/omt/integer_optimizer.cpp
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