Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : :
16 : : #include "theory/arith/linear/infer_bounds.h"
17 : :
18 : : #include "theory/rewriter.h"
19 : :
20 : : using namespace cvc5::internal::kind;
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace arith::linear {
25 : :
26 : : using namespace inferbounds;
27 : :
28 : 0 : InferBoundAlgorithm::InferBoundAlgorithm() : d_alg(None) {}
29 : :
30 : 26488 : InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a) : d_alg(a)
31 : : {
32 [ - + ][ - + ]: 26488 : Assert(a != Simplex);
[ - - ]
33 : 26488 : }
34 : :
35 : 0 : InferBoundAlgorithm::InferBoundAlgorithm(
36 : 0 : const std::optional<int>& simplexRounds)
37 : 0 : : d_alg(Simplex), d_simplexRounds(simplexRounds)
38 : : {
39 : 0 : }
40 : :
41 : 50526 : Algorithms InferBoundAlgorithm::getAlgorithm() const { return d_alg; }
42 : :
43 : 0 : const std::optional<int>& InferBoundAlgorithm::getSimplexRounds() const
44 : : {
45 : 0 : Assert(getAlgorithm() == Simplex);
46 : 0 : return d_simplexRounds;
47 : : }
48 : :
49 : 13244 : InferBoundAlgorithm InferBoundAlgorithm::mkLookup()
50 : : {
51 : 13244 : return InferBoundAlgorithm(Lookup);
52 : : }
53 : :
54 : 13244 : InferBoundAlgorithm InferBoundAlgorithm::mkRowSum()
55 : : {
56 : 13244 : return InferBoundAlgorithm(RowSum);
57 : : }
58 : :
59 : 0 : InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(
60 : : const std::optional<int>& rounds)
61 : : {
62 : 0 : return InferBoundAlgorithm(rounds);
63 : : }
64 : :
65 : 13244 : ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
66 : 13244 : : d_algorithms()
67 : : {
68 : 13244 : }
69 : :
70 : 13244 : ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters() {}
71 : :
72 : 13244 : void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms()
73 : : {
74 : 13244 : addAlgorithm(InferBoundAlgorithm::mkLookup());
75 : 13244 : addAlgorithm(InferBoundAlgorithm::mkRowSum());
76 : 13244 : }
77 : :
78 : 26488 : void ArithEntailmentCheckParameters::addAlgorithm(
79 : : const inferbounds::InferBoundAlgorithm& alg)
80 : : {
81 : 26488 : d_algorithms.push_back(alg);
82 : 26488 : }
83 : :
84 : : ArithEntailmentCheckParameters::const_iterator
85 : 13244 : ArithEntailmentCheckParameters::begin() const
86 : : {
87 : 13244 : return d_algorithms.begin();
88 : : }
89 : :
90 : : ArithEntailmentCheckParameters::const_iterator
91 : 13244 : ArithEntailmentCheckParameters::end() const
92 : : {
93 : 13244 : return d_algorithms.end();
94 : : }
95 : :
96 : 0 : InferBoundsResult::InferBoundsResult()
97 : 0 : : d_foundBound(false),
98 : 0 : d_budgetExhausted(false),
99 : 0 : d_boundIsProvenOpt(false),
100 : 0 : d_inconsistentState(false),
101 : 0 : d_reachedThreshold(false),
102 : 0 : d_value(false),
103 : 0 : d_term(Node::null()),
104 : 0 : d_upperBound(true),
105 : 0 : d_explanation(Node::null())
106 : : {
107 : 0 : }
108 : :
109 : 0 : InferBoundsResult::InferBoundsResult(Node term, bool ub)
110 : 0 : : d_foundBound(false),
111 : 0 : d_budgetExhausted(false),
112 : 0 : d_boundIsProvenOpt(false),
113 : 0 : d_inconsistentState(false),
114 : 0 : d_reachedThreshold(false),
115 : 0 : d_value(false),
116 : 0 : d_term(term),
117 : 0 : d_upperBound(ub),
118 : 0 : d_explanation(Node::null())
119 : : {
120 : 0 : }
121 : :
122 : 0 : bool InferBoundsResult::foundBound() const { return d_foundBound; }
123 : 0 : bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; }
124 : 0 : bool InferBoundsResult::inconsistentState() const
125 : : {
126 : 0 : return d_inconsistentState;
127 : : }
128 : :
129 : 0 : bool InferBoundsResult::boundIsInteger() const
130 : : {
131 [ - - ][ - - ]: 0 : return foundBound() && d_value.isIntegral();
132 : : }
133 : :
134 : 0 : bool InferBoundsResult::boundIsRational() const
135 : : {
136 [ - - ][ - - ]: 0 : return foundBound() && d_value.infinitesimalIsZero();
137 : : }
138 : :
139 : 0 : Integer InferBoundsResult::valueAsInteger() const
140 : : {
141 : 0 : Assert(boundIsInteger());
142 : 0 : return getValue().floor();
143 : : }
144 : 0 : const Rational& InferBoundsResult::valueAsRational() const
145 : : {
146 : 0 : Assert(boundIsRational());
147 : 0 : return getValue().getNoninfinitesimalPart();
148 : : }
149 : :
150 : 0 : const DeltaRational& InferBoundsResult::getValue() const { return d_value; }
151 : :
152 : 0 : Node InferBoundsResult::getTerm() const { return d_term; }
153 : :
154 : 0 : Node InferBoundsResult::getLiteral() const
155 : : {
156 : 0 : const Rational& q = getValue().getNoninfinitesimalPart();
157 : 0 : NodeManager* nm = d_term.getNodeManager();
158 : 0 : Node qnode = nm->mkConstReal(q);
159 : :
160 : : Kind k;
161 [ - - ]: 0 : if (d_upperBound)
162 : : {
163 : : // x <= q + c*delta
164 : 0 : Assert(getValue().infinitesimalSgn() <= 0);
165 [ - - ]: 0 : k = boundIsRational() ? Kind::LEQ : Kind::LT;
166 : : }
167 : : else
168 : : {
169 : : // x >= q + c*delta
170 : 0 : Assert(getValue().infinitesimalSgn() >= 0);
171 [ - - ]: 0 : k = boundIsRational() ? Kind::GEQ : Kind::GT;
172 : : }
173 : 0 : return nm->mkNode(k, getTerm(), qnode);
174 : 0 : }
175 : :
176 : : /* If there is a bound, this is a node that explains the bound. */
177 : 0 : Node InferBoundsResult::getExplanation() const { return d_explanation; }
178 : :
179 : 0 : void InferBoundsResult::setBound(const DeltaRational& dr, Node exp)
180 : : {
181 : 0 : d_foundBound = true;
182 : 0 : d_value = dr;
183 : 0 : d_explanation = exp;
184 : 0 : }
185 : :
186 : 0 : void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
187 : 0 : void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
188 : 0 : void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
189 : 0 : void InferBoundsResult::setInconsistent() { d_inconsistentState = true; }
190 : :
191 : 0 : bool InferBoundsResult::thresholdWasReached() const
192 : : {
193 : 0 : return d_reachedThreshold;
194 : : }
195 : 0 : bool InferBoundsResult::budgetIsExhausted() const { return d_budgetExhausted; }
196 : :
197 : 0 : std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr)
198 : : {
199 : 0 : os << "{InferBoundsResult " << std::endl;
200 : 0 : os << "on " << ibr.getTerm() << ", ";
201 [ - - ]: 0 : if (ibr.findUpperBound())
202 : : {
203 : 0 : os << "find upper bound, ";
204 : : }
205 : : else
206 : : {
207 : 0 : os << "find lower bound, ";
208 : : }
209 [ - - ]: 0 : if (ibr.foundBound())
210 : : {
211 : 0 : os << "found a bound: ";
212 [ - - ]: 0 : if (ibr.boundIsInteger())
213 : : {
214 : 0 : os << ibr.valueAsInteger() << "(int), ";
215 : : }
216 [ - - ]: 0 : else if (ibr.boundIsRational())
217 : : {
218 : 0 : os << ibr.valueAsRational() << "(rat), ";
219 : : }
220 : : else
221 : : {
222 : 0 : os << ibr.getValue() << "(extended), ";
223 : : }
224 : :
225 : 0 : os << "as term " << ibr.getLiteral() << ", ";
226 : 0 : os << "explanation " << ibr.getExplanation() << ", ";
227 : : }
228 : : else
229 : : {
230 : 0 : os << "did not find a bound, ";
231 : : }
232 : :
233 [ - - ]: 0 : if (ibr.boundIsOptimal())
234 : : {
235 : 0 : os << "(opt), ";
236 : : }
237 : :
238 [ - - ]: 0 : if (ibr.inconsistentState())
239 : : {
240 : 0 : os << "(inconsistent), ";
241 : : }
242 [ - - ]: 0 : if (ibr.budgetIsExhausted())
243 : : {
244 : 0 : os << "(budget exhausted), ";
245 : : }
246 [ - - ]: 0 : if (ibr.thresholdWasReached())
247 : : {
248 : 0 : os << "(reached threshold), ";
249 : : }
250 : 0 : os << "}";
251 : 0 : return os;
252 : : }
253 : :
254 : 13244 : ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
255 : 13244 : : d_simplexSideEffects(nullptr)
256 : : {
257 : 13244 : }
258 : :
259 : 13244 : ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects()
260 : : {
261 [ - + ]: 13244 : if (d_simplexSideEffects != nullptr)
262 : : {
263 [ - - ]: 0 : delete d_simplexSideEffects;
264 : 0 : d_simplexSideEffects = nullptr;
265 : : }
266 : 13244 : }
267 : :
268 : 0 : InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects()
269 : : {
270 [ - - ]: 0 : if (d_simplexSideEffects == nullptr)
271 : : {
272 : 0 : d_simplexSideEffects = new InferBoundsResult;
273 : : }
274 : 0 : return *d_simplexSideEffects;
275 : : }
276 : :
277 : : namespace inferbounds { /* namespace arith */
278 : :
279 : 0 : std::ostream& operator<<(std::ostream& os, const Algorithms a)
280 : : {
281 [ - - ][ - - ]: 0 : switch (a)
[ - ]
282 : : {
283 : 0 : case None: os << "AlgNone"; break;
284 : 0 : case Lookup: os << "AlgLookup"; break;
285 : 0 : case RowSum: os << "AlgRowSum"; break;
286 : 0 : case Simplex: os << "AlgSimplex"; break;
287 : 0 : default: Unhandled();
288 : : }
289 : :
290 : 0 : return os;
291 : : }
292 : :
293 : : } /* namespace inferbounds */
294 : :
295 : : } // namespace arith::linear
296 : : } /* namespace theory */
297 : : } // namespace cvc5::internal
|
