GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/infer_bounds.cpp Lines: 33 137 24.1 %
Date: 2021-03-23 Branches: 7 217 3.2 %

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