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
|
/********************* */
/*! \file optimization_solver.h
** \verbatim
** Top contributors (to current version):
** Michael Chang, Yancheng Ou
** This file is part of the CVC4 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.\endverbatim
**
** \brief The solver for optimization queries
**/
#include "cvc4_private.h"
#ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
#define CVC5__SMT__OPTIMIZATION_SOLVER_H
#include "expr/node.h"
#include "expr/type_node.h"
#include "smt/assertions.h"
#include "util/result.h"
namespace cvc5 {
class SmtEngine;
namespace smt {
/**
* An enum for optimization queries.
*
* Represents whether an objective should be minimized or maximized
*/
enum class ObjectiveType
{
OBJECTIVE_MINIMIZE,
OBJECTIVE_MAXIMIZE,
OBJECTIVE_UNDEFINED
};
/**
* An enum for optimization queries.
*
* Represents the result of a checkopt query
* (unimplemented) OPT_OPTIMAL: if value was found
*/
enum class OptResult
{
// the original set of assertions has result UNKNOWN
OPT_UNKNOWN,
// the original set of assertions has result UNSAT
OPT_UNSAT,
// the optimization loop finished and optimal
OPT_OPTIMAL,
// the goal is unbounded, so it would be -inf or +inf
OPT_UNBOUNDED,
// The last value is here as a preparation for future work
// in which pproximate optimizations will be supported.
// if the solver halted early and value is only approximate
OPT_SAT_APPROX
};
/**
* The optimization objective, which contains:
* - the optimization target node,
* - whether it's maximize/minimize
* - and whether it's signed for BitVectors
**/
class Objective
{
public:
/**
* Constructor
* @param n 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
**/
Objective(Node n, ObjectiveType type, bool bvSigned = false);
~Objective(){};
/** A getter for d_type **/
ObjectiveType getType();
/** A getter for d_node **/
Node getNode();
/** A getter for d_bvSigned **/
bool getSigned();
private:
/** The type of objective this is, either OBJECTIVE_MAXIMIZE OR
* OBJECTIVE_MINIMIZE **/
ObjectiveType d_type;
/** The node associated to the term that was used to construct the objective.
* **/
Node d_node;
/** 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);
~OptimizationSolver();
/** Runs the optimization loop for the activated objective **/
OptResult checkOpt();
/**
* Activates an objective: will be optimized for
* @param obj 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 activateObj(const Node& obj,
const ObjectiveType type,
bool bvSigned = false);
/** Gets the value of the optimized objective after checkopt is called **/
Node objectiveGetValue();
private:
/** The parent SMT engine **/
SmtEngine* d_parent;
/** The objectives to optimize for **/
Objective d_activatedObjective;
/** A saved value of the objective from the last sat call. **/
Node d_savedValue;
};
} // namespace smt
} // namespace cvc5
#endif /* CVC5__SMT__OPTIMIZATION_SOLVER_H */
|
