Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/omt/omt_optimizer.h	Lines:	2	2	100.0 %
Date:	2021-09-17	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Yancheng Ou
 *
 * 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 base class for optimizers of individual cvc5 type.
 */

#ifndef CVC5__OMT__OMT_OPTIMIZER_H
#define CVC5__OMT__OMT_OPTIMIZER_H

#include "smt/optimization_solver.h"

namespace cvc5::omt {

/**
 * The base class for optimizers of individual CVC type
 */
class OMTOptimizer
{
 public:
  virtual ~OMTOptimizer() = default;

  /**
   * Returns whether node supports optimization
   * Currently supported: BitVectors, Integers (preliminary).
   * @param node the target node to check for optimizability
   * @return whether node supports optimization
   **/
  static bool nodeSupportsOptimization(TNode node);

  /**
   * Given an optimization objective,
   * retrieve an optimizer specific for the optimization target
   * @param objective the an OptimizationObjective object containing
   *   the optimization target, whether it's maximized or minimized
   *   and whether it's signed for BV (only applies when the target type is BV)
   * @return a unique_pointer pointing to a derived class of OMTOptimizer
   *   and this is the optimizer for targetNode
   **/
  static std::unique_ptr<OMTOptimizer> getOptimizerForObjective(
      const smt::OptimizationObjective& objective);

  /**
   * Given the lhs and rhs expressions, with an optimization objective,
   * makes an incremental expression stating that
   *   lhs `better than` rhs
   * under the context specified by objective
   * for minimize, it would be lhs < rhs
   * for maximize, it would be lhs > rhs
   *
   * Note: the types of lhs and rhs nodes must match or be convertable
   *   to the type of the optimization target!
   *
   * @param nm the NodeManager to manage the made expression
   * @param lhs the left hand side of the expression
   * @param rhs the right hand side of the expression
   * @param objective the optimization objective
   *   stating whether it's maximize / minimize etc.
   * @return an expression stating lhs `better than` rhs,
   **/
  static Node mkStrongIncrementalExpression(
      NodeManager* nm,
      TNode lhs,
      TNode rhs,
      const smt::OptimizationObjective& objective);

  /**
   * Given the lhs and rhs expressions, with an optimization objective,
   * makes an incremental expression stating that
   *   lhs `better than or equal to` rhs
   * under the context specified by objective
   * for minimize, it would be lhs <= rhs
   * for maximize, it would be lhs >= rhs
   *
   * Note: the types of lhs and rhs nodes must match or be convertable
   *   to the type of the optimization target!
   *
   * @param nm the NodeManager to manage the made expression
   * @param lhs the left hand side of the expression
   * @param rhs the right hand side of the expression
   * @param objective the optimization objective
   *   stating whether it's maximize / minimize etc.
   * @return an expression stating lhs `better than or equal to` rhs,
   **/
  static Node mkWeakIncrementalExpression(
      NodeManager* nm,
      TNode lhs,
      TNode rhs,
      const smt::OptimizationObjective& objective);

  /**
   * Minimize the target node with constraints encoded in optChecker
   *
   * @param optChecker an SMT solver encoding the assertions as the
   *   constraints
   * @param target the target expression to optimize
   * @return smt::OptimizationResult the result of optimization, containing
   *   whether it's optimal and the optimized value.
   **/
  virtual smt::OptimizationResult minimize(SmtEngine* optChecker,
                                           TNode target) = 0;
  /**
   * Maximize the target node with constraints encoded in optChecker
   *
   * @param optChecker an SMT solver encoding the assertions as the
   *   constraints
   * @param target the target expression to optimize
   * @return smt::OptimizationResult the result of optimization, containing
   *   whether it's optimal and the optimized value.
   **/
  virtual smt::OptimizationResult maximize(SmtEngine* optChecker,
                                           TNode target) = 0;
};

}  // namespace cvc5::omt

#endif /* CVC5__OMT__OMT_OPTIMIZER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Yancheng Ou
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 base class for optimizers of individual cvc5 type.
14		*/
15
16		#ifndef CVC5__OMT__OMT_OPTIMIZER_H
17		#define CVC5__OMT__OMT_OPTIMIZER_H
18
19		#include "smt/optimization_solver.h"
20
21		namespace cvc5::omt {
22
23		/**
24		* The base class for optimizers of individual CVC type
25		*/
26	38	class OMTOptimizer
27		{
28		public:
29	38	virtual ~OMTOptimizer() = default;
30
31		/**
32		* Returns whether node supports optimization
33		* Currently supported: BitVectors, Integers (preliminary).
34		* @param node the target node to check for optimizability
35		* @return whether node supports optimization
36		**/
37		static bool nodeSupportsOptimization(TNode node);
38
39		/**
40		* Given an optimization objective,
41		* retrieve an optimizer specific for the optimization target
42		* @param objective the an OptimizationObjective object containing
43		* the optimization target, whether it's maximized or minimized
44		* and whether it's signed for BV (only applies when the target type is BV)
45		* @return a unique_pointer pointing to a derived class of OMTOptimizer
46		* and this is the optimizer for targetNode
47		**/
48		static std::unique_ptr<OMTOptimizer> getOptimizerForObjective(
49		const smt::OptimizationObjective& objective);
50
51		/**
52		* Given the lhs and rhs expressions, with an optimization objective,
53		* makes an incremental expression stating that
54		* lhs `better than` rhs
55		* under the context specified by objective
56		* for minimize, it would be lhs < rhs
57		* for maximize, it would be lhs > rhs
58		*
59		* Note: the types of lhs and rhs nodes must match or be convertable
60		* to the type of the optimization target!
61		*
62		* @param nm the NodeManager to manage the made expression
63		* @param lhs the left hand side of the expression
64		* @param rhs the right hand side of the expression
65		* @param objective the optimization objective
66		* stating whether it's maximize / minimize etc.
67		* @return an expression stating lhs `better than` rhs,
68		**/
69		static Node mkStrongIncrementalExpression(
70		NodeManager* nm,
71		TNode lhs,
72		TNode rhs,
73		const smt::OptimizationObjective& objective);
74
75		/**
76		* Given the lhs and rhs expressions, with an optimization objective,
77		* makes an incremental expression stating that
78		* lhs `better than or equal to` rhs
79		* under the context specified by objective
80		* for minimize, it would be lhs <= rhs
81		* for maximize, it would be lhs >= rhs
82		*
83		* Note: the types of lhs and rhs nodes must match or be convertable
84		* to the type of the optimization target!
85		*
86		* @param nm the NodeManager to manage the made expression
87		* @param lhs the left hand side of the expression
88		* @param rhs the right hand side of the expression
89		* @param objective the optimization objective
90		* stating whether it's maximize / minimize etc.
91		* @return an expression stating lhs `better than or equal to` rhs,
92		**/
93		static Node mkWeakIncrementalExpression(
94		NodeManager* nm,
95		TNode lhs,
96		TNode rhs,
97		const smt::OptimizationObjective& objective);
98
99		/**
100		* Minimize the target node with constraints encoded in optChecker
101		*
102		* @param optChecker an SMT solver encoding the assertions as the
103		* constraints
104		* @param target the target expression to optimize
105		* @return smt::OptimizationResult the result of optimization, containing
106		* whether it's optimal and the optimized value.
107		**/
108		virtual smt::OptimizationResult minimize(SmtEngine* optChecker,
109		TNode target) = 0;
110		/**
111		* Maximize the target node with constraints encoded in optChecker
112		*
113		* @param optChecker an SMT solver encoding the assertions as the
114		* constraints
115		* @param target the target expression to optimize
116		* @return smt::OptimizationResult the result of optimization, containing
117		* whether it's optimal and the optimized value.
118		**/
119		virtual smt::OptimizationResult maximize(SmtEngine* optChecker,
120		TNode target) = 0;
121		};
122
123		} // namespace cvc5::omt
124
125		#endif /* CVC5__OMT__OMT_OPTIMIZER_H */