From 0c982a7486ef9b6991589685f9091602e0cf5572 Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Wed, 9 Jun 2021 08:53:16 -0700 Subject: [Optimization] support for push/pop (#6706) Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop). SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function. --- src/omt/omt_optimizer.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'src/omt/omt_optimizer.cpp') diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index 08f1809ec..2145492db 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -30,7 +30,7 @@ bool OMTOptimizer::nodeSupportsOptimization(TNode node) } std::unique_ptr OMTOptimizer::getOptimizerForObjective( - OptimizationObjective& objective) + const OptimizationObjective& objective) { // the datatype of the target node TypeNode objectiveType = objective.getTarget().getType(true); @@ -53,7 +53,10 @@ std::unique_ptr OMTOptimizer::getOptimizerForObjective( } Node OMTOptimizer::mkStrongIncrementalExpression( - NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective) + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " @@ -114,10 +117,11 @@ Node OMTOptimizer::mkStrongIncrementalExpression( Unreachable(); } -Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, - TNode lhs, - TNode rhs, - OptimizationObjective& objective) +Node OMTOptimizer::mkWeakIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " -- cgit v1.2.3