projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 898f11d) | patch
Add some printing functions for OptimizationObjective and OptimizationResult (#6809)
authorOuyancheng <1024842937@qq.com>
Tue, 6 Jul 2021 03:22:14 +0000 (20:22 -0700)
committerGitHub <noreply@github.com>
Tue, 6 Jul 2021 03:22:14 +0000 (22:22 -0500)
commit80efd9fb51d25a7e2f3de802b41e4802e42596d7
tree48a2c7f45d730fc9a6018e96ae712fdf6e004fe4tree
parent898f11d0945bdaaa8bb79a536b66b266c78f1daacommit | diff
Add some printing functions for OptimizationObjective and OptimizationResult (#6809)

Implement the operator << with std::ostream for OptimizationObjective and OptimizationResult. Currently only supports SMTLib2 or Sygus as output languages.
Objective: (maximize [node] :signed) or (minimize [node]) or ...
Result: (sat [expr]) or (unsat) or (unknown([explanation]) [expr/null])
src/smt/optimization_solver.cpp diff | blob | history
src/smt/optimization_solver.h diff | blob | history