1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
|
/******************************************************************************
* 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 */
|
