Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/optimization_solver.cpp	Lines:	120	187	64.2 %
Date:	2021-08-06	Branches:	143	395	36.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Yancheng Ou, Michael Chang, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The solver for optimization queries.
 */

#include "smt/optimization_solver.h"

#include "context/cdhashmap.h"
#include "context/cdlist.h"
#include "omt/omt_optimizer.h"
#include "options/base_options.h"
#include "options/language.h"
#include "options/smt_options.h"
#include "smt/assertions.h"
#include "smt/smt_engine.h"
#include "theory/smt_engine_subsolver.h"

using namespace cvc5::theory;
using namespace cvc5::omt;
namespace cvc5 {
namespace smt {

std::ostream& operator<<(std::ostream& out, const OptimizationResult& result)
{
  // check the output language first
  OutputLanguage lang = language::SetLanguage::getLanguage(out);
  if (!language::isOutputLang_smt2(lang))
  {
    Unimplemented()
        << "Only the SMTLib2 language supports optimization right now";
  }
  out << "(" << result.getResult();
  switch (result.getResult().isSat())
  {
    case Result::SAT:
    case Result::SAT_UNKNOWN:
    {
      switch (result.isInfinity())
      {
        case OptimizationResult::FINITE:
          out << "\t" << result.getValue();
          break;
        case OptimizationResult::POSTITIVE_INF: out << "\t+Inf"; break;
        case OptimizationResult::NEGATIVE_INF: out << "\t-Inf"; break;
        default: break;
      }
      break;
    }
    case Result::UNSAT: break;
    default: Unreachable();
  }
  out << ")";
  return out;
}

std::ostream& operator<<(std::ostream& out,
                         const OptimizationObjective& objective)
{
  // check the output language first
  OutputLanguage lang = language::SetLanguage::getLanguage(out);
  if (!language::isOutputLang_smt2(lang))
  {
    Unimplemented()
        << "Only the SMTLib2 language supports optimization right now";
  }
  out << "(";
  switch (objective.getType())
  {
    case OptimizationObjective::MAXIMIZE: out << "maximize "; break;
    case OptimizationObjective::MINIMIZE: out << "minimize "; break;
    default: Unreachable();
  }
  TNode target = objective.getTarget();
  TypeNode type = target.getType();
  out << target;
  if (type.isBitVector())
  {
    out << (objective.bvIsSigned() ? " :signed" : " :unsigned");
  }
  out << ")";
  return out;
}

OptimizationSolver::OptimizationSolver(SmtEngine* parent)
    : d_parent(parent),
      d_optChecker(),
      d_objectives(parent->getUserContext()),
      d_results()
{
}

Result OptimizationSolver::checkOpt(ObjectiveCombination combination)
{
  // if the results of the previous call have different size than the
  // objectives, then we should clear the pareto optimization context
  if (d_results.size() != d_objectives.size()) d_optChecker.reset();
  // initialize the result vector
  d_results.clear();
  for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
  {
    d_results.emplace_back();
  }
  switch (combination)
  {
    case BOX: return optimizeBox(); break;
    case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break;
    case PARETO: return optimizeParetoNaiveGIA(); break;
    default:
      CVC5_FATAL()
          << "Unknown objective combination, "
          << "valid objective combinations are BOX, LEXICOGRAPHIC and PARETO";
  }
  Unreachable();
}

void OptimizationSolver::addObjective(TNode target,
                                      OptimizationObjective::ObjectiveType type,
                                      bool bvSigned)
{
  if (!OMTOptimizer::nodeSupportsOptimization(target))
  {
    CVC5_FATAL()
        << "Objective failed to add: Target node does not support optimization";
  }
  d_optChecker.reset();
  d_objectives.emplace_back(target, type, bvSigned);
}

std::vector<OptimizationResult> OptimizationSolver::getValues()
{
  return d_results;
}

std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
    SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
{
  std::unique_ptr<SmtEngine> optChecker;
  // initializeSubSolver will copy the options and theories enabled
  // from the current solver to optChecker and adds timeout
  theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout);
  // we need to be in incremental mode for multiple objectives since we need to
  // push pop we need to produce models to inrement on our objective
  optChecker->setOption("incremental", "true");
  optChecker->setOption("produce-models", "true");
  // Move assertions from the parent solver to the subsolver
  std::vector<Node> p_assertions = parentSMTSolver->getExpandedAssertions();
  for (const Node& e : p_assertions)
  {
    optChecker->assertFormula(e);
  }
  return optChecker;
}

Result OptimizationSolver::optimizeBox()
{
  // resets the optChecker
  d_optChecker = createOptCheckerWithTimeout(d_parent);
  OptimizationResult partialResult;
  Result aggregatedResult(Result::Sat::SAT);
  std::unique_ptr<OMTOptimizer> optimizer;
  for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
  {
    optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]);
    // checks whether the objective type is maximize or minimize
    switch (d_objectives[i].getType())
    {
      case OptimizationObjective::MAXIMIZE:
        partialResult = optimizer->maximize(d_optChecker.get(),
                                            d_objectives[i].getTarget());
        break;
      case OptimizationObjective::MINIMIZE:
        partialResult = optimizer->minimize(d_optChecker.get(),
                                            d_objectives[i].getTarget());
        break;
      default:
        CVC5_FATAL()
            << "Optimization objective is neither MAXIMIZE nor MINIMIZE";
    }
    // match the optimization result type, and aggregate the results of
    // subproblems
    switch (partialResult.getResult().isSat())
    {
      case Result::SAT: break;
      case Result::UNSAT:
        // the assertions are unsatisfiable
        for (size_t j = 0; j < numObj; ++j)
        {
          d_results[j] = partialResult;
        }
        d_optChecker.reset();
        return partialResult.getResult();
      case Result::SAT_UNKNOWN:
        aggregatedResult = partialResult.getResult();
        break;
      default: Unreachable();
    }

    d_results[i] = partialResult;
  }
  // kill optChecker after optimization ends
  d_optChecker.reset();
  return aggregatedResult;
}

Result OptimizationSolver::optimizeLexicographicIterative()
{
  // resets the optChecker
  d_optChecker = createOptCheckerWithTimeout(d_parent);
  // partialResult defaults to SAT if no objective is present
  // NOTE: the parenthesis around Result(Result::SAT) is required,
  // otherwise the compiler will report "parameter declarator cannot be
  // qualified". For more details:
  // https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it
  // https://en.wikipedia.org/wiki/Most_vexing_parse
  OptimizationResult partialResult((Result(Result::SAT)), TNode());
  std::unique_ptr<OMTOptimizer> optimizer;
  for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
  {
    optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]);
    // checks if the objective is maximize or minimize
    switch (d_objectives[i].getType())
    {
      case OptimizationObjective::MAXIMIZE:
        partialResult = optimizer->maximize(d_optChecker.get(),
                                            d_objectives[i].getTarget());
        break;
      case OptimizationObjective::MINIMIZE:
        partialResult = optimizer->minimize(d_optChecker.get(),
                                            d_objectives[i].getTarget());
        break;
      default:
        CVC5_FATAL()
            << "Optimization objective is neither MAXIMIZE nor MINIMIZE";
    }

    d_results[i] = partialResult;

    // checks the optimization result of the current objective
    switch (partialResult.getResult().isSat())
    {
      case Result::SAT:
        // assert target[i] == value[i] and proceed
        d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode(
            kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue()));
        break;
      case Result::UNSAT:
        d_optChecker.reset();
        return partialResult.getResult();
      case Result::SAT_UNKNOWN:
        d_optChecker.reset();
        return partialResult.getResult();
      default: Unreachable();
    }

    // if the result for the current objective is unbounded
    // (result is not finite) then just stop
    if (partialResult.isInfinity() != OptimizationResult::FINITE) break;
  }
  // kill optChecker in case pareto misuses it
  d_optChecker.reset();
  // now all objectives are optimal, just return SAT as the overall result
  return partialResult.getResult();
}

Result OptimizationSolver::optimizeParetoNaiveGIA()
{
  // initial call to Pareto optimizer, create the checker
  if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
  NodeManager* nm = d_optChecker->getNodeManager();

  // checks whether the current set of assertions are satisfied or not
  Result satResult = d_optChecker->checkSat();

  switch (satResult.isSat())
  {
    case Result::Sat::UNSAT:
    case Result::Sat::SAT_UNKNOWN: return satResult;
    case Result::Sat::SAT:
    {
      // if satisfied, use d_results to store the initial results
      // they will be gradually updated and optimized
      // until no more optimal value could be found
      for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
      {
        d_results[i] = OptimizationResult(
            satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
      }
      break;
    }
    default: Unreachable();
  }

  Result lastSatResult = satResult;

  // a vector storing assertions saying that no objective is worse
  std::vector<Node> noWorseObj;
  // a vector storing assertions saying that there is at least one objective
  // that could be improved
  std::vector<Node> someObjBetter;
  d_optChecker->push();

  while (satResult.isSat() == Result::Sat::SAT)
  {
    noWorseObj.clear();
    someObjBetter.clear();

    for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
    {
      // for maximize value[i] <= obj[i],
      // for minimize obj[i] <= value[i]
      noWorseObj.push_back(
          OMTOptimizer::mkWeakIncrementalExpression(nm,
                                                    d_objectives[i].getTarget(),
                                                    d_results[i].getValue(),
                                                    d_objectives[i]));
      // for maximize value[i] < obj[i],
      // for minimize obj[i] < value[i]
      someObjBetter.push_back(OMTOptimizer::mkStrongIncrementalExpression(
          nm,
          d_objectives[i].getTarget(),
          d_results[i].getValue(),
          d_objectives[i]));
    }
    d_optChecker->assertFormula(nm->mkAnd(noWorseObj));
    d_optChecker->assertFormula(nm->mkOr(someObjBetter));
    // checks if previous assertions + noWorseObj + someObjBetter are satisfied
    satResult = d_optChecker->checkSat();

    switch (satResult.isSat())
    {
      case Result::Sat::UNSAT:
        // if result is UNSAT, it means no more improvement could be made,
        // then the results stored in d_results are one of the Pareto optimal
        // results
        break;
      case Result::Sat::SAT_UNKNOWN:
        // if result is UNKNOWN, abort the current session and return UNKNOWN
        d_optChecker.reset();
        return satResult;
      case Result::Sat::SAT:
      {
        lastSatResult = satResult;
        // if result is SAT, update d_results to the more optimal values
        for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
        {
          d_results[i] = OptimizationResult(
              satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
        }
        break;
      }
      default: Unreachable();
    }
  }

  d_optChecker->pop();

  // before we return:
  // assert that some objective could be better
  // in order not to get the same optimal solution
  // for the next run.
  d_optChecker->assertFormula(nm->mkOr(someObjBetter));

  return lastSatResult;
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Yancheng Ou, Michael Chang, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* The solver for optimization queries.
14		*/
15
16		#include "smt/optimization_solver.h"
17
18		#include "context/cdhashmap.h"
19		#include "context/cdlist.h"
20		#include "omt/omt_optimizer.h"
21		#include "options/base_options.h"
22		#include "options/language.h"
23		#include "options/smt_options.h"
24		#include "smt/assertions.h"
25		#include "smt/smt_engine.h"
26		#include "theory/smt_engine_subsolver.h"
27
28		using namespace cvc5::theory;
29		using namespace cvc5::omt;
30		namespace cvc5 {
31		namespace smt {
32
33		std::ostream& operator<<(std::ostream& out, const OptimizationResult& result)
34		{
35		// check the output language first
36		OutputLanguage lang = language::SetLanguage::getLanguage(out);
37		if (!language::isOutputLang_smt2(lang))
38		{
39		Unimplemented()
40		<< "Only the SMTLib2 language supports optimization right now";
41		}
42		out << "(" << result.getResult();
43		switch (result.getResult().isSat())
44		{
45		case Result::SAT:
46		case Result::SAT_UNKNOWN:
47		{
48		switch (result.isInfinity())
49		{
50		case OptimizationResult::FINITE:
51		out << "\t" << result.getValue();
52		break;
53		case OptimizationResult::POSTITIVE_INF: out << "\t+Inf"; break;
54		case OptimizationResult::NEGATIVE_INF: out << "\t-Inf"; break;
55		default: break;
56		}
57		break;
58		}
59		case Result::UNSAT: break;
60		default: Unreachable();
61		}
62		out << ")";
63		return out;
64		}
65
66		std::ostream& operator<<(std::ostream& out,
67		const OptimizationObjective& objective)
68		{
69		// check the output language first
70		OutputLanguage lang = language::SetLanguage::getLanguage(out);
71		if (!language::isOutputLang_smt2(lang))
72		{
73		Unimplemented()
74		<< "Only the SMTLib2 language supports optimization right now";
75		}
76		out << "(";
77		switch (objective.getType())
78		{
79		case OptimizationObjective::MAXIMIZE: out << "maximize "; break;
80		case OptimizationObjective::MINIMIZE: out << "minimize "; break;
81		default: Unreachable();
82		}
83		TNode target = objective.getTarget();
84		TypeNode type = target.getType();
85		out << target;
86		if (type.isBitVector())
87		{
88		out << (objective.bvIsSigned() ? " :signed" : " :unsigned");
89		}
90		out << ")";
91		return out;
92		}
93
94	26	OptimizationSolver::OptimizationSolver(SmtEngine* parent)
95		: d_parent(parent),
96		d_optChecker(),
97	26	d_objectives(parent->getUserContext()),
98	52	d_results()
99		{
100	26	}
101
102	36	Result OptimizationSolver::checkOpt(ObjectiveCombination combination)
103		{
104		// if the results of the previous call have different size than the
105		// objectives, then we should clear the pareto optimization context
106	36	if (d_results.size() != d_objectives.size()) d_optChecker.reset();
107		// initialize the result vector
108	36	d_results.clear();
109	90	for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
110		{
111	54	d_results.emplace_back();
112		}
113	36	switch (combination)
114		{
115	2	case BOX: return optimizeBox(); break;
116	26	case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break;
117	8	case PARETO: return optimizeParetoNaiveGIA(); break;
118		default:
119		CVC5_FATAL()
120		<< "Unknown objective combination, "
121		<< "valid objective combinations are BOX, LEXICOGRAPHIC and PARETO";
122		}
123		Unreachable();
124		}
125
126	40	void OptimizationSolver::addObjective(TNode target,
127		OptimizationObjective::ObjectiveType type,
128		bool bvSigned)
129		{
130	40	if (!OMTOptimizer::nodeSupportsOptimization(target))
131		{
132		CVC5_FATAL()
133		<< "Objective failed to add: Target node does not support optimization";
134		}
135	40	d_optChecker.reset();
136	40	d_objectives.emplace_back(target, type, bvSigned);
137	40	}
138
139	34	std::vector<OptimizationResult> OptimizationSolver::getValues()
140		{
141	34	return d_results;
142		}
143
144	30	std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
145		SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
146		{
147	30	std::unique_ptr<SmtEngine> optChecker;
148		// initializeSubSolver will copy the options and theories enabled
149		// from the current solver to optChecker and adds timeout
150	30	theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout);
151		// we need to be in incremental mode for multiple objectives since we need to
152		// push pop we need to produce models to inrement on our objective
153	30	optChecker->setOption("incremental", "true");
154	30	optChecker->setOption("produce-models", "true");
155		// Move assertions from the parent solver to the subsolver
156	60	std::vector<Node> p_assertions = parentSMTSolver->getExpandedAssertions();
157	86	for (const Node& e : p_assertions)
158		{
159	56	optChecker->assertFormula(e);
160		}
161	60	return optChecker;
162		}
163
164	2	Result OptimizationSolver::optimizeBox()
165		{
166		// resets the optChecker
167	2	d_optChecker = createOptCheckerWithTimeout(d_parent);
168	4	OptimizationResult partialResult;
169	4	Result aggregatedResult(Result::Sat::SAT);
170	4	std::unique_ptr<OMTOptimizer> optimizer;
171	8	for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
172		{
173	6	optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]);
174		// checks whether the objective type is maximize or minimize
175	6	switch (d_objectives[i].getType())
176		{
177	4	case OptimizationObjective::MAXIMIZE:
178	8	partialResult = optimizer->maximize(d_optChecker.get(),
179	8	d_objectives[i].getTarget());
180	4	break;
181	2	case OptimizationObjective::MINIMIZE:
182	4	partialResult = optimizer->minimize(d_optChecker.get(),
183	4	d_objectives[i].getTarget());
184	2	break;
185		default:
186		CVC5_FATAL()
187		<< "Optimization objective is neither MAXIMIZE nor MINIMIZE";
188		}
189		// match the optimization result type, and aggregate the results of
190		// subproblems
191	6	switch (partialResult.getResult().isSat())
192		{
193	6	case Result::SAT: break;
194		case Result::UNSAT:
195		// the assertions are unsatisfiable
196		for (size_t j = 0; j < numObj; ++j)
197		{
198		d_results[j] = partialResult;
199		}
200		d_optChecker.reset();
201		return partialResult.getResult();
202		case Result::SAT_UNKNOWN:
203		aggregatedResult = partialResult.getResult();
204		break;
205		default: Unreachable();
206		}
207
208	6	d_results[i] = partialResult;
209		}
210		// kill optChecker after optimization ends
211	2	d_optChecker.reset();
212	2	return aggregatedResult;
213		}
214
215	26	Result OptimizationSolver::optimizeLexicographicIterative()
216		{
217		// resets the optChecker
218	26	d_optChecker = createOptCheckerWithTimeout(d_parent);
219		// partialResult defaults to SAT if no objective is present
220		// NOTE: the parenthesis around Result(Result::SAT) is required,
221		// otherwise the compiler will report "parameter declarator cannot be
222		// qualified". For more details:
223		// https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it
224		// https://en.wikipedia.org/wiki/Most_vexing_parse
225	52	OptimizationResult partialResult((Result(Result::SAT)), TNode());
226	52	std::unique_ptr<OMTOptimizer> optimizer;
227	56	for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
228		{
229	32	optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]);
230		// checks if the objective is maximize or minimize
231	32	switch (d_objectives[i].getType())
232		{
233	16	case OptimizationObjective::MAXIMIZE:
234	32	partialResult = optimizer->maximize(d_optChecker.get(),
235	32	d_objectives[i].getTarget());
236	16	break;
237	16	case OptimizationObjective::MINIMIZE:
238	32	partialResult = optimizer->minimize(d_optChecker.get(),
239	32	d_objectives[i].getTarget());
240	16	break;
241		default:
242		CVC5_FATAL()
243		<< "Optimization objective is neither MAXIMIZE nor MINIMIZE";
244		}
245
246	32	d_results[i] = partialResult;
247
248		// checks the optimization result of the current objective
249	32	switch (partialResult.getResult().isSat())
250		{
251	30	case Result::SAT:
252		// assert target[i] == value[i] and proceed
253	120	d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode(
254	120	kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue()));
255	30	break;
256	2	case Result::UNSAT:
257	2	d_optChecker.reset();
258	2	return partialResult.getResult();
259		case Result::SAT_UNKNOWN:
260		d_optChecker.reset();
261		return partialResult.getResult();
262		default: Unreachable();
263		}
264
265		// if the result for the current objective is unbounded
266		// (result is not finite) then just stop
267	30	if (partialResult.isInfinity() != OptimizationResult::FINITE) break;
268		}
269		// kill optChecker in case pareto misuses it
270	24	d_optChecker.reset();
271		// now all objectives are optimal, just return SAT as the overall result
272	24	return partialResult.getResult();
273		}
274
275	8	Result OptimizationSolver::optimizeParetoNaiveGIA()
276		{
277		// initial call to Pareto optimizer, create the checker
278	8	if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
279	8	NodeManager* nm = d_optChecker->getNodeManager();
280
281		// checks whether the current set of assertions are satisfied or not
282	16	Result satResult = d_optChecker->checkSat();
283
284	8	switch (satResult.isSat())
285		{
286	2	case Result::Sat::UNSAT:
287	2	case Result::Sat::SAT_UNKNOWN: return satResult;
288	6	case Result::Sat::SAT:
289		{
290		// if satisfied, use d_results to store the initial results
291		// they will be gradually updated and optimized
292		// until no more optimal value could be found
293	18	for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
294		{
295	12	d_results[i] = OptimizationResult(
296	24	satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
297		}
298	6	break;
299		}
300		default: Unreachable();
301		}
302
303	12	Result lastSatResult = satResult;
304
305		// a vector storing assertions saying that no objective is worse
306	12	std::vector<Node> noWorseObj;
307		// a vector storing assertions saying that there is at least one objective
308		// that could be improved
309	12	std::vector<Node> someObjBetter;
310	6	d_optChecker->push();
311
312	30	while (satResult.isSat() == Result::Sat::SAT)
313		{
314	12	noWorseObj.clear();
315	12	someObjBetter.clear();
316
317	36	for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
318		{
319		// for maximize value[i] <= obj[i],
320		// for minimize obj[i] <= value[i]
321	24	noWorseObj.push_back(
322	120	OMTOptimizer::mkWeakIncrementalExpression(nm,
323	48	d_objectives[i].getTarget(),
324	48	d_results[i].getValue(),
325		d_objectives[i]));
326		// for maximize value[i] < obj[i],
327		// for minimize obj[i] < value[i]
328	96	someObjBetter.push_back(OMTOptimizer::mkStrongIncrementalExpression(
329		nm,
330	48	d_objectives[i].getTarget(),
331	48	d_results[i].getValue(),
332		d_objectives[i]));
333		}
334	12	d_optChecker->assertFormula(nm->mkAnd(noWorseObj));
335	12	d_optChecker->assertFormula(nm->mkOr(someObjBetter));
336		// checks if previous assertions + noWorseObj + someObjBetter are satisfied
337	12	satResult = d_optChecker->checkSat();
338
339	12	switch (satResult.isSat())
340		{
341	6	case Result::Sat::UNSAT:
342		// if result is UNSAT, it means no more improvement could be made,
343		// then the results stored in d_results are one of the Pareto optimal
344		// results
345	6	break;
346		case Result::Sat::SAT_UNKNOWN:
347		// if result is UNKNOWN, abort the current session and return UNKNOWN
348		d_optChecker.reset();
349		return satResult;
350	6	case Result::Sat::SAT:
351		{
352	6	lastSatResult = satResult;
353		// if result is SAT, update d_results to the more optimal values
354	18	for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
355		{
356	12	d_results[i] = OptimizationResult(
357	24	satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
358		}
359	6	break;
360		}
361		default: Unreachable();
362		}
363		}
364
365	6	d_optChecker->pop();
366
367		// before we return:
368		// assert that some objective could be better
369		// in order not to get the same optimal solution
370		// for the next run.
371	6	d_optChecker->assertFormula(nm->mkOr(someObjBetter));
372
373	6	return lastSatResult;
374		}
375
376		} // namespace smt
377	29322	} // namespace cvc5