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