Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/optimization_solver.cpp	Lines:	122	189	64.6 %
Date:	2021-09-18	Branches:	144	393	36.6 %


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