diff options
| author | Ouyancheng <1024842937@qq.com> | 2021-05-27 00:53:58 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-27 07:53:58 +0000 |
| commit | 7120cf46b38f0bede1ab8d17453ae925aa2d27fd (patch) | |
| tree | b22e054d08f0312b12b6fc62a37eb2497f8d16a6 /src/omt/omt_optimizer.cpp | |
| parent | cd386643b1113c92775950b3683c2b48f7f2bf13 (diff) | |
Add support for Box optimization (#6599)
Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.
Diffstat (limited to 'src/omt/omt_optimizer.cpp')
| -rw-r--r-- | src/omt/omt_optimizer.cpp | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index bcf84cb53..08f1809ec 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Yancheng Ou, Michael Chang, Aina Niemetz + * Yancheng Ou, Aina Niemetz * * This file is part of the cvc5 project. * @@ -47,7 +47,8 @@ std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective( } else { - return nullptr; + Unimplemented() << "Target type " << objectiveType + << " does not support optimization"; } } @@ -81,7 +82,8 @@ Node OMTOptimizer::mkStrongIncrementalExpression( } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } case OptimizationObjective::MAXIMIZE: @@ -102,7 +104,8 @@ Node OMTOptimizer::mkStrongIncrementalExpression( } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } default: @@ -143,7 +146,8 @@ Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } case OptimizationObjective::MAXIMIZE: @@ -164,7 +168,8 @@ Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } default: |