Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/optimization_solver.h	Lines:	19	20	95.0 %
Date:	2021-05-22	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Michael Chang, Yancheng Ou, 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 "expr/node.h"
#include "expr/type_node.h"
#include "util/result.h"

namespace cvc5 {

class SmtEngine;

namespace smt {

/**
 * The optimization result of an optimization objective
 * containing:
 * - whether it's optimal or not
 * - if so, the optimal value, otherwise the value might be empty node or
 *   something suboptimal
 */
class OptimizationResult
{
 public:
  /**
   * Enum indicating whether the checkOpt result
   * is optimal or not.
   **/
  enum ResultType
  {
    // the type of the target is not supported
    UNSUPPORTED,
    // whether the value is optimal is UNKNOWN
    UNKNOWN,
    // the original set of assertions has result UNSAT
    UNSAT,
    // the value is optimal
    OPTIMAL,
    // the goal is unbounded,
    // if objective is maximize, it's +infinity
    // if objective is minimize, it's -infinity
    UNBOUNDED,
  };

  /**
   * Constructor
   * @param type the optimization outcome
   * @param value the optimized value
   **/
  OptimizationResult(ResultType type, TNode value)
      : d_type(type), d_value(value)
  {
  }
  OptimizationResult() : d_type(UNSUPPORTED), d_value() {}
  ~OptimizationResult() = default;

  /**
   * Returns an enum indicating whether
   * the result is optimal or not.
   * @return an enum showing whether the result is optimal, unbounded,
   *   unsat, unknown or unsupported.
   **/
  ResultType getType() { return d_type; }
  /**
   * Returns the optimal value.
   * @return Node containing the optimal value,
   *   if getType() is not OPTIMAL, it might return an empty node or a node
   *   containing non-optimal value
   **/
  Node getValue() { return d_value; }

 private:
  /** the indicating whether the result is optimal or something else **/
  ResultType d_type;
  /** if the result is optimal, this is storing the optimal value **/
  Node d_value;
};

/**
 * 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() { return d_type; }

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

  /** A getter for d_bvSigned **/
  bool bvIsSigned() { 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;
};

/**
 * 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:
  /**
   * Constructor
   * @param parent the smt_solver that the user added their assertions to
   **/
  OptimizationSolver(SmtEngine* parent)
      : d_parent(parent), d_objectives(), d_results()
  {
  }
  ~OptimizationSolver() = default;

  /**
   * Run the optimization loop for the pushed objective
   * NOTE: this function currently supports only single objective
   * for multiple pushed objectives it always optimizes the first one.
   * Add support for multi-obj later
   */
  OptimizationResult::ResultType checkOpt();

  /**
   * Push an objective.
   * @param target the 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 pushObjective(TNode target,
                     OptimizationObjective::ObjectiveType type,
                     bool bvSigned = false);

  /**
   * Pop the most recent objective.
   **/
  void popObjective();

  /**
   * 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 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);

  /** The parent SMT engine **/
  SmtEngine* d_parent;

  /** The objectives to optimize for **/
  std::vector<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		* Michael Chang, Yancheng Ou, 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 "expr/node.h"
22		#include "expr/type_node.h"
23		#include "util/result.h"
24
25		namespace cvc5 {
26
27		class SmtEngine;
28
29		namespace smt {
30
31		/**
32		* The optimization result of an optimization objective
33		* containing:
34		* - whether it's optimal or not
35		* - if so, the optimal value, otherwise the value might be empty node or
36		* something suboptimal
37		*/
38	54	class OptimizationResult
39		{
40		public:
41		/**
42		* Enum indicating whether the checkOpt result
43		* is optimal or not.
44		**/
45		enum ResultType
46		{
47		// the type of the target is not supported
48		UNSUPPORTED,
49		// whether the value is optimal is UNKNOWN
50		UNKNOWN,
51		// the original set of assertions has result UNSAT
52		UNSAT,
53		// the value is optimal
54		OPTIMAL,
55		// the goal is unbounded,
56		// if objective is maximize, it's +infinity
57		// if objective is minimize, it's -infinity
58		UNBOUNDED,
59		};
60
61		/**
62		* Constructor
63		* @param type the optimization outcome
64		* @param value the optimized value
65		**/
66	36	OptimizationResult(ResultType type, TNode value)
67	36	: d_type(type), d_value(value)
68		{
69	36	}
70	18	OptimizationResult() : d_type(UNSUPPORTED), d_value() {}
71	72	~OptimizationResult() = default;
72
73		/**
74		* Returns an enum indicating whether
75		* the result is optimal or not.
76		* @return an enum showing whether the result is optimal, unbounded,
77		* unsat, unknown or unsupported.
78		**/
79	18	ResultType getType() { return d_type; }
80		/**
81		* Returns the optimal value.
82		* @return Node containing the optimal value,
83		* if getType() is not OPTIMAL, it might return an empty node or a node
84		* containing non-optimal value
85		**/
86	18	Node getValue() { return d_value; }
87
88		private:
89		/ the indicating whether the result is optimal or something else /
90		ResultType d_type;
91		/ if the result is optimal, this is storing the optimal value /
92		Node d_value;
93		};
94
95		/**
96		* The optimization objective, which contains:
97		* - the optimization target node,
98		* - whether it's maximize/minimize
99		* - and whether it's signed for BitVectors
100		*/
101		class OptimizationObjective
102		{
103		public:
104		/**
105		* An enum for optimization queries.
106		* Represents whether an objective should be minimized or maximized
107		*/
108		enum ObjectiveType
109		{
110		MINIMIZE,
111		MAXIMIZE,
112		};
113
114		/**
115		* Constructor
116		* @param target the optimization target node
117		* @param type speficies whether it's maximize/minimize
118		* @param bvSigned specifies whether it's using signed or unsigned comparison
119		* for BitVectors this parameter is only valid when the type of target node
120		* is BitVector
121		**/
122	18	OptimizationObjective(TNode target, ObjectiveType type, bool bvSigned = false)
123	18	: d_type(type), d_target(target), d_bvSigned(bvSigned)
124		{
125	18	}
126	18	~OptimizationObjective() = default;
127
128		/ A getter for d_type /
129	28	ObjectiveType getType() { return d_type; }
130
131		/ A getter for d_target /
132	36	Node getTarget() { return d_target; }
133
134		/ A getter for d_bvSigned /
135	10	bool bvIsSigned() { return d_bvSigned; }
136
137		private:
138		/**
139		* The type of objective,
140		* it's either MAXIMIZE OR MINIMIZE
141		**/
142		ObjectiveType d_type;
143
144		/**
145		* The node associated to the term that was used to construct the objective.
146		**/
147		Node d_target;
148
149		/**
150		* Specify whether to use signed or unsigned comparison
151		* for BitVectors (only for BitVectors), this variable is defaulted to false
152		**/
153		bool d_bvSigned;
154		};
155
156		/**
157		* A solver for optimization queries.
158		*
159		* This class is responsible for responding to optmization queries. It
160		* spawns a subsolver SmtEngine that captures the parent assertions and
161		* implements a linear optimization loop. Supports activateObjective,
162		* checkOpt, and objectiveGetValue in that order.
163		*/
164		class OptimizationSolver
165		{
166		public:
167		/**
168		* Constructor
169		* @param parent the smt_solver that the user added their assertions to
170		**/
171	18	OptimizationSolver(SmtEngine* parent)
172	18	: d_parent(parent), d_objectives(), d_results()
173		{
174	18	}
175	18	~OptimizationSolver() = default;
176
177		/**
178		* Run the optimization loop for the pushed objective
179		* NOTE: this function currently supports only single objective
180		* for multiple pushed objectives it always optimizes the first one.
181		* Add support for multi-obj later
182		*/
183		OptimizationResult::ResultType checkOpt();
184
185		/**
186		* Push an objective.
187		* @param target the Node representing the expression that will be optimized
188		*for
189		* @param type specifies whether it's maximize or minimize
190		* @param bvSigned specifies whether we should use signed/unsigned
191		* comparison for BitVectors (only effective for BitVectors)
192		* and its default is false
193		**/
194		void pushObjective(TNode target,
195		OptimizationObjective::ObjectiveType type,
196		bool bvSigned = false);
197
198		/**
199		* Pop the most recent objective.
200		**/
201		void popObjective();
202
203		/**
204		* Returns the values of the optimized objective after checkOpt is called
205		* @return a vector of Optimization Result,
206		* each containing the outcome and the value.
207		**/
208		std::vector<OptimizationResult> getValues();
209
210		private:
211		/**
212		* Initialize an SMT subsolver for offline optimization purpose
213		* @param parentSMTSolver the parental solver containing the assertions
214		* @param needsTimeout specifies whether it needs timeout for each single
215		* query
216		* @param timeout the timeout value, given in milliseconds (ms)
217		* @return a unique_pointer of SMT subsolver
218		**/
219		static std::unique_ptr<SmtEngine> createOptCheckerWithTimeout(
220		SmtEngine* parentSMTSolver,
221		bool needsTimeout = false,
222		unsigned long timeout = 0);
223
224		/ The parent SMT engine /
225		SmtEngine* d_parent;
226
227		/ The objectives to optimize for /
228		std::vector<OptimizationObjective> d_objectives;
229
230		/ The results of the optimizations from the last checkOpt call /
231		std::vector<OptimizationResult> d_results;
232		};
233
234		} // namespace smt
235		} // namespace cvc5
236
237		#endif /* CVC5__SMT__OPTIMIZATION_SOLVER_H */