Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/optimization_solver.h	Lines:	20	20	100.0 %
Date:	2021-09-15	Branches:	5	10	50.0 %


/******************************************************************************
 * 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 "cvc5_private.h"

#ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
#define CVC5__SMT__OPTIMIZATION_SOLVER_H

#include "context/cdhashmap_forward.h"
#include "context/cdlist.h"
#include "expr/node.h"
#include "expr/type_node.h"
#include "util/result.h"

namespace cvc5 {

class Env;
class SmtEngine;

namespace smt {

class OptimizationObjective;
class OptimizationResult;

/**
 * The optimization result, containing:
 * - the optimization result: SAT/UNSAT/UNKNOWN
 * - the optimal value if SAT and finite
 *     (optimal value reached and it's not infinity),
 *   or an empty node if SAT and infinite
 *   otherwise the value might be empty node
 *   or something suboptimal
 * - whether the result is finite/+-infinity
 */
class OptimizationResult
{
 public:
  enum IsInfinity
  {
    FINITE = 0,
    POSTITIVE_INF,
    NEGATIVE_INF
  };
  /**
   * Constructor
   * @param type the optimization outcome
   * @param value the optimized value
   * @param isInf whether the result is FINITE/POSITIVE_INF/NEGATIVE_INF
   **/
  OptimizationResult(Result result, TNode value, IsInfinity isInf = FINITE)
      : d_result(result), d_value(value), d_infinity(isInf)
  {
  }
  OptimizationResult()
      : d_result(Result::Sat::SAT_UNKNOWN,
                 Result::UnknownExplanation::NO_STATUS),
        d_value(),
        d_infinity(FINITE)
  {
  }
  ~OptimizationResult() = default;

  /**
   * Returns an enum indicating whether
   * the result is SAT or not.
   * @return whether the result is SAT, UNSAT or SAT_UNKNOWN
   **/
  Result getResult() const { return d_result; }

  /**
   * Returns the optimal value.
   * @return Node containing the optimal value,
   *   if result is infinite, this will be an empty node,
   *   if getResult() is UNSAT, it will return an empty node,
   *   if getResult() is SAT_UNKNOWN, it will return something suboptimal
   *   or an empty node, depending on how the solver runs.
   **/
  Node getValue() const { return d_value; }

  /**
   * Checks whether the result is infinity
   * @return whether the result is FINITE/POSITIVE_INF/NEGATIVE_INF
   **/
  IsInfinity isInfinity() const { return d_infinity; }

 private:
  /** indicating whether the result is SAT, UNSAT or UNKNOWN **/
  Result d_result;
  /** if the result is finite, this is storing the value **/
  Node d_value;
  /** whether the result is finite/+infinity/-infinity **/
  IsInfinity d_infinity;
};

/**
 * To serialize the OptimizationResult.
 * @param out the stream to put the serialized result
 * @param result the OptimizationResult object to serialize
 * @return the parameter out
 **/
std::ostream& operator<<(std::ostream& out, const OptimizationResult& result);

/**
 * The optimization objective, which contains:
 * - the optimization target node,
 * - whether it's maximize/minimize
 * - and whether it's signed for BitVectors
 */
class OptimizationObjective
{
 public:
  /**
   * An enum for optimization queries.
   * Represents whether an objective should be minimized or maximized
   */
  enum ObjectiveType
  {
    MINIMIZE,
    MAXIMIZE,
  };

  /**
   * Constructor
   * @param target the optimization target node
   * @param type speficies whether it's maximize/minimize
   * @param bvSigned specifies whether it's using signed or unsigned comparison
   *    for BitVectors this parameter is only valid when the type of target node
   *    is BitVector
   **/
  OptimizationObjective(TNode target, ObjectiveType type, bool bvSigned = false)
      : d_type(type), d_target(target), d_bvSigned(bvSigned)
  {
  }
  ~OptimizationObjective() = default;

  /** A getter for d_type **/
  ObjectiveType getType() const { return d_type; }

  /** A getter for d_target **/
  Node getTarget() const { return d_target; }

  /** A getter for d_bvSigned **/
  bool bvIsSigned() const { return d_bvSigned; }

 private:
  /**
   * The type of objective,
   * it's either MAXIMIZE OR MINIMIZE
   **/
  ObjectiveType d_type;

  /**
   * The node associated to the term that was used to construct the objective.
   **/
  Node d_target;

  /**
   * Specify whether to use signed or unsigned comparison
   * for BitVectors (only for BitVectors), this variable is defaulted to false
   **/
  bool d_bvSigned;
};

/**
 * To serialize the OptimizationObjective.
 * @param out the stream to put the serialized result
 * @param objective the OptimizationObjective object to serialize
 * @return the parameter out
 **/
std::ostream& operator<<(std::ostream& out,
                         const OptimizationObjective& objective);

/**
 * A solver for optimization queries.
 *
 * This class is responsible for responding to optmization queries. It
 * spawns a subsolver SmtEngine that captures the parent assertions and
 * implements a linear optimization loop. Supports activateObjective,
 * checkOpt, and objectiveGetValue in that order.
 */
class OptimizationSolver
{
 public:
  /**
   * An enum specifying how multiple objectives are dealt with.
   * Definition:
   *   phi(x, y): set of assertions with variables x and y
   *
   * Box: treat the objectives as independent objectives
   *   v_x = max(x) s.t. phi(x, y) = sat
   *   v_y = max(y) s.t. phi(x, y) = sat
   *
   * Lexicographic: optimize the objectives one-by-one, in the order they are
   * added:
   *   v_x = max(x) s.t. phi(x, y) = sat
   *   v_y = max(y) s.t. phi(v_x, y) = sat
   *
   * Pareto: optimize multiple goals to a state such that
   * further optimization of one goal will worsen the other goal(s)
   *   (v_x, v_y) s.t. phi(v_x, v_y) = sat, and
   *     forall (x, y), (phi(x, y) = sat) -> (x <= v_x or y <= v_y)
   **/
  enum ObjectiveCombination
  {
    BOX,
    LEXICOGRAPHIC,
    PARETO,
  };
  /**
   * Constructor
   * @param parent the smt_solver that the user added their assertions to
   **/
  OptimizationSolver(SmtEngine* parent);
  ~OptimizationSolver() = default;

  /**
   * Run the optimization loop for the added objective
   * For multiple objective combination, it defaults to lexicographic,
   * possible combinations: BOX, LEXICOGRAPHIC, PARETO
   * @param combination BOX / LEXICOGRAPHIC / PARETO
   */
  Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC);

  /**
   * Add an optimization objective.
   * @param target Node representing the expression that will be optimized for
   * @param type specifies whether it's maximize or minimize
   * @param bvSigned specifies whether we should use signed/unsigned
   *   comparison for BitVectors (only effective for BitVectors)
   *   and its default is false
   **/
  void addObjective(TNode target,
                    OptimizationObjective::ObjectiveType type,
                    bool bvSigned = false);

  /**
   * Returns the values of the optimized objective after checkOpt is called
   * @return a vector of Optimization Result,
   *   each containing the outcome and the value.
   **/
  std::vector<OptimizationResult> getValues();

 private:
  /**
   * Initialize an SMT subsolver for offline optimization purpose
   * @param env the environment, which determines options and logic for the
   * subsolver
   * @param parentSMTSolver the parental solver containing the assertions
   * @param needsTimeout specifies whether it needs timeout for each single
   *    query
   * @param timeout the timeout value, given in milliseconds (ms)
   * @return a unique_pointer of SMT subsolver
   **/
  static std::unique_ptr<SmtEngine> createOptCheckerWithTimeout(
      SmtEngine* parentSMTSolver,
      bool needsTimeout = false,
      unsigned long timeout = 0);

  /**
   * Optimize multiple goals in Box order
   * @return SAT if all of the objectives are optimal (could be infinite);
   *   UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
   *   SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
   **/
  Result optimizeBox();

  /**
   * Optimize multiple goals in Lexicographic order,
   * using iterative implementation
   * @return SAT if the objectives are optimal,
   *     if one of the objectives is unbounded (result is infinite),
   *     the optimization will stop at that objective;
   *   UNSAT if any of the objectives is UNSAT
   *     and optimization will stop at that objective;
   *   SAT_UNKNOWN if any of the objectives is UNKNOWN
   *     and optimization will stop at that objective;
   *   If the optimization is stopped at an objective,
   *     all objectives following that objective will be SAT_UNKNOWN.
   **/
  Result optimizeLexicographicIterative();

  /**
   * Optimize multiple goals in Pareto order
   * Using a variant of linear search called Guided Improvement Algorithm
   * Could be called multiple times to iterate through the Pareto front
   *
   * Definition:
   * Pareto front: Set of all possible Pareto optimal solutions
   *
   * Reference:
   * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm.
   *  Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009.
   *
   * @return if it finds a new Pareto optimal result it will return SAT;
   *   if it exhausts the results in the Pareto front it will return UNSAT;
   *   if the underlying SMT solver returns SAT_UNKNOWN,
   *   it will return SAT_UNKNOWN.
   **/
  Result optimizeParetoNaiveGIA();

  /** A pointer to the parent SMT engine **/
  SmtEngine* d_parent;

  /** A subsolver for offline optimization **/
  std::unique_ptr<SmtEngine> d_optChecker;

  /** The objectives to optimize for **/
  context::CDList<OptimizationObjective> d_objectives;

  /** The results of the optimizations from the last checkOpt call **/
  std::vector<OptimizationResult> d_results;
};

}  // namespace smt
}  // namespace cvc5

#endif /* CVC5__SMT__OPTIMIZATION_SOLVER_H */


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 "cvc5_private.h"
17
18		#ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
19		#define CVC5__SMT__OPTIMIZATION_SOLVER_H
20
21		#include "context/cdhashmap_forward.h"
22		#include "context/cdlist.h"
23		#include "expr/node.h"
24		#include "expr/type_node.h"
25		#include "util/result.h"
26
27		namespace cvc5 {
28
29		class Env;
30		class SmtEngine;
31
32		namespace smt {
33
34		class OptimizationObjective;
35		class OptimizationResult;
36
37		/**
38		* The optimization result, containing:
39		* - the optimization result: SAT/UNSAT/UNKNOWN
40		* - the optimal value if SAT and finite
41		* (optimal value reached and it's not infinity),
42		* or an empty node if SAT and infinite
43		* otherwise the value might be empty node
44		* or something suboptimal
45		* - whether the result is finite/+-infinity
46		*/
47	170	class OptimizationResult
48		{
49		public:
50		enum IsInfinity
51		{
52		FINITE = 0,
53		POSTITIVE_INF,
54		NEGATIVE_INF
55		};
56		/**
57		* Constructor
58		* @param type the optimization outcome
59		* @param value the optimized value
60		* @param isInf whether the result is FINITE/POSITIVE_INF/NEGATIVE_INF
61		**/
62	88	OptimizationResult(Result result, TNode value, IsInfinity isInf = FINITE)
63	88	: d_result(result), d_value(value), d_infinity(isInf)
64		{
65	88	}
66	56	OptimizationResult()
67	56	: d_result(Result::Sat::SAT_UNKNOWN,
68		Result::UnknownExplanation::NO_STATUS),
69		d_value(),
70	56	d_infinity(FINITE)
71		{
72	56	}
73	214	~OptimizationResult() = default;
74
75		/**
76		* Returns an enum indicating whether
77		* the result is SAT or not.
78		* @return whether the result is SAT, UNSAT or SAT_UNKNOWN
79		**/
80	64	Result getResult() const { return d_result; }
81
82		/**
83		* Returns the optimal value.
84		* @return Node containing the optimal value,
85		* if result is infinite, this will be an empty node,
86		* if getResult() is UNSAT, it will return an empty node,
87		* if getResult() is SAT_UNKNOWN, it will return something suboptimal
88		* or an empty node, depending on how the solver runs.
89		**/
90	140	Node getValue() const { return d_value; }
91
92		/**
93		* Checks whether the result is infinity
94		* @return whether the result is FINITE/POSITIVE_INF/NEGATIVE_INF
95		**/
96	30	IsInfinity isInfinity() const { return d_infinity; }
97
98		private:
99		/ indicating whether the result is SAT, UNSAT or UNKNOWN /
100		Result d_result;
101		/ if the result is finite, this is storing the value /
102		Node d_value;
103		/ whether the result is finite/+infinity/-infinity /
104		IsInfinity d_infinity;
105		};
106
107		/**
108		* To serialize the OptimizationResult.
109		* @param out the stream to put the serialized result
110		* @param result the OptimizationResult object to serialize
111		* @return the parameter out
112		**/
113		std::ostream& operator<<(std::ostream& out, const OptimizationResult& result);
114
115		/**
116		* The optimization objective, which contains:
117		* - the optimization target node,
118		* - whether it's maximize/minimize
119		* - and whether it's signed for BitVectors
120		*/
121		class OptimizationObjective
122		{
123		public:
124		/**
125		* An enum for optimization queries.
126		* Represents whether an objective should be minimized or maximized
127		*/
128		enum ObjectiveType
129		{
130		MINIMIZE,
131		MAXIMIZE,
132		};
133
134		/**
135		* Constructor
136		* @param target the optimization target node
137		* @param type speficies whether it's maximize/minimize
138		* @param bvSigned specifies whether it's using signed or unsigned comparison
139		* for BitVectors this parameter is only valid when the type of target node
140		* is BitVector
141		**/
142	40	OptimizationObjective(TNode target, ObjectiveType type, bool bvSigned = false)
143	40	: d_type(type), d_target(target), d_bvSigned(bvSigned)
144		{
145	40	}
146	40	~OptimizationObjective() = default;
147
148		/ A getter for d_type /
149	86	ObjectiveType getType() const { return d_type; }
150
151		/ A getter for d_target /
152	226	Node getTarget() const { return d_target; }
153
154		/ A getter for d_bvSigned /
155	78	bool bvIsSigned() const { return d_bvSigned; }
156
157		private:
158		/**
159		* The type of objective,
160		* it's either MAXIMIZE OR MINIMIZE
161		**/
162		ObjectiveType d_type;
163
164		/**
165		* The node associated to the term that was used to construct the objective.
166		**/
167		Node d_target;
168
169		/**
170		* Specify whether to use signed or unsigned comparison
171		* for BitVectors (only for BitVectors), this variable is defaulted to false
172		**/
173		bool d_bvSigned;
174		};
175
176		/**
177		* To serialize the OptimizationObjective.
178		* @param out the stream to put the serialized result
179		* @param objective the OptimizationObjective object to serialize
180		* @return the parameter out
181		**/
182		std::ostream& operator<<(std::ostream& out,
183		const OptimizationObjective& objective);
184
185		/**
186		* A solver for optimization queries.
187		*
188		* This class is responsible for responding to optmization queries. It
189		* spawns a subsolver SmtEngine that captures the parent assertions and
190		* implements a linear optimization loop. Supports activateObjective,
191		* checkOpt, and objectiveGetValue in that order.
192		*/
193		class OptimizationSolver
194		{
195		public:
196		/**
197		* An enum specifying how multiple objectives are dealt with.
198		* Definition:
199		* phi(x, y): set of assertions with variables x and y
200		*
201		* Box: treat the objectives as independent objectives
202		* v_x = max(x) s.t. phi(x, y) = sat
203		* v_y = max(y) s.t. phi(x, y) = sat
204		*
205		* Lexicographic: optimize the objectives one-by-one, in the order they are
206		* added:
207		* v_x = max(x) s.t. phi(x, y) = sat
208		* v_y = max(y) s.t. phi(v_x, y) = sat
209		*
210		* Pareto: optimize multiple goals to a state such that
211		* further optimization of one goal will worsen the other goal(s)
212		* (v_x, v_y) s.t. phi(v_x, v_y) = sat, and
213		* forall (x, y), (phi(x, y) = sat) -> (x <= v_x or y <= v_y)
214		**/
215		enum ObjectiveCombination
216		{
217		BOX,
218		LEXICOGRAPHIC,
219		PARETO,
220		};
221		/**
222		* Constructor
223		* @param parent the smt_solver that the user added their assertions to
224		**/
225		OptimizationSolver(SmtEngine* parent);
226	26	~OptimizationSolver() = default;
227
228		/**
229		* Run the optimization loop for the added objective
230		* For multiple objective combination, it defaults to lexicographic,
231		* possible combinations: BOX, LEXICOGRAPHIC, PARETO
232		* @param combination BOX / LEXICOGRAPHIC / PARETO
233		*/
234		Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC);
235
236		/**
237		* Add an optimization objective.
238		* @param target Node representing the expression that will be optimized for
239		* @param type specifies whether it's maximize or minimize
240		* @param bvSigned specifies whether we should use signed/unsigned
241		* comparison for BitVectors (only effective for BitVectors)
242		* and its default is false
243		**/
244		void addObjective(TNode target,
245		OptimizationObjective::ObjectiveType type,
246		bool bvSigned = false);
247
248		/**
249		* Returns the values of the optimized objective after checkOpt is called
250		* @return a vector of Optimization Result,
251		* each containing the outcome and the value.
252		**/
253		std::vector<OptimizationResult> getValues();
254
255		private:
256		/**
257		* Initialize an SMT subsolver for offline optimization purpose
258		* @param env the environment, which determines options and logic for the
259		* subsolver
260		* @param parentSMTSolver the parental solver containing the assertions
261		* @param needsTimeout specifies whether it needs timeout for each single
262		* query
263		* @param timeout the timeout value, given in milliseconds (ms)
264		* @return a unique_pointer of SMT subsolver
265		**/
266		static std::unique_ptr<SmtEngine> createOptCheckerWithTimeout(
267		SmtEngine* parentSMTSolver,
268		bool needsTimeout = false,
269		unsigned long timeout = 0);
270
271		/**
272		* Optimize multiple goals in Box order
273		* @return SAT if all of the objectives are optimal (could be infinite);
274		* UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
275		* SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
276		**/
277		Result optimizeBox();
278
279		/**
280		* Optimize multiple goals in Lexicographic order,
281		* using iterative implementation
282		* @return SAT if the objectives are optimal,
283		* if one of the objectives is unbounded (result is infinite),
284		* the optimization will stop at that objective;
285		* UNSAT if any of the objectives is UNSAT
286		* and optimization will stop at that objective;
287		* SAT_UNKNOWN if any of the objectives is UNKNOWN
288		* and optimization will stop at that objective;
289		* If the optimization is stopped at an objective,
290		* all objectives following that objective will be SAT_UNKNOWN.
291		**/
292		Result optimizeLexicographicIterative();
293
294		/**
295		* Optimize multiple goals in Pareto order
296		* Using a variant of linear search called Guided Improvement Algorithm
297		* Could be called multiple times to iterate through the Pareto front
298		*
299		* Definition:
300		* Pareto front: Set of all possible Pareto optimal solutions
301		*
302		* Reference:
303		* D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm.
304		* Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009.
305		*
306		* @return if it finds a new Pareto optimal result it will return SAT;
307		* if it exhausts the results in the Pareto front it will return UNSAT;
308		* if the underlying SMT solver returns SAT_UNKNOWN,
309		* it will return SAT_UNKNOWN.
310		**/
311		Result optimizeParetoNaiveGIA();
312
313		/ A pointer to the parent SMT engine /
314		SmtEngine* d_parent;
315
316		/ A subsolver for offline optimization /
317		std::unique_ptr<SmtEngine> d_optChecker;
318
319		/ The objectives to optimize for /
320		context::CDList<OptimizationObjective> d_objectives;
321
322		/ The results of the optimizations from the last checkOpt call /
323		std::vector<OptimizationResult> d_results;
324		};
325
326		} // namespace smt
327		} // namespace cvc5
328
329		#endif /* CVC5__SMT__OPTIMIZATION_SOLVER_H */