diff options
| author | Ouyancheng <1024842937@qq.com> | 2021-06-15 16:20:20 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-15 23:20:20 +0000 |
| commit | c299e8661f24d3a6acb736e9e5df1b1920488ac3 (patch) | |
| tree | 3c662e58fe01fc44996d3dd8cf622be25ef5ce32 /.gitignore | |
| parent | 4ca14e808d788ef9570dda1188645783c6a11e70 (diff) | |
[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)...
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions