1 /********************* */
2 /*! \file infer_bounds.cpp
4 ** Original author: Tim King
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/arith/infer_bounds.h"
19 #include "theory/rewriter.h"
25 using namespace inferbounds
;
27 InferBoundAlgorithm::InferBoundAlgorithm()
31 InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a
)
37 InferBoundAlgorithm::InferBoundAlgorithm(const Maybe
<int>& simplexRounds
)
41 Algorithms
InferBoundAlgorithm::getAlgorithm() const{
45 const Maybe
<int>& InferBoundAlgorithm::getSimplexRounds() const{
46 Assert(getAlgorithm() == Simplex
);
47 return d_simplexRounds
;
51 InferBoundAlgorithm
InferBoundAlgorithm::mkLookup(){
52 return InferBoundAlgorithm(Lookup
);
55 InferBoundAlgorithm
InferBoundAlgorithm::mkRowSum(){
56 return InferBoundAlgorithm(RowSum
);
59 InferBoundAlgorithm
InferBoundAlgorithm::mkSimplex(const Maybe
<int>& rounds
){
60 return InferBoundAlgorithm(rounds
);
63 ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
64 : EntailmentCheckParameters(theory::THEORY_ARITH
)
68 ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
72 void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
73 addAlgorithm(InferBoundAlgorithm::mkLookup());
74 addAlgorithm(InferBoundAlgorithm::mkRowSum());
77 void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm
& alg
){
78 d_algorithms
.push_back(alg
);
81 ArithEntailmentCheckParameters::const_iterator
ArithEntailmentCheckParameters::begin() const{
82 return d_algorithms
.begin();
85 ArithEntailmentCheckParameters::const_iterator
ArithEntailmentCheckParameters::end() const{
86 return d_algorithms
.end();
90 // SimplexInferBoundsParameters::SimplexInferBoundsParameters()
92 // , d_upperBound(true)
96 // SimplexInferBoundsParameters::~SimplexInferBoundsParameters(){}
100 // int SimplexInferBoundsParameters::getSimplexRoundParameter() const {
101 // return d_parameter;
104 // bool SimplexInferBoundsParameters::findLowerBound() const {
105 // return ! findUpperBound();
108 // bool SimplexInferBoundsParameters::findUpperBound() const {
109 // return d_upperBound;
112 // void SimplexInferBoundsParameters::setThreshold(const DeltaRational& th){
114 // d_useThreshold = true;
117 // bool SimplexInferBoundsParameters::useThreshold() const{
118 // return d_useThreshold;
121 // const DeltaRational& SimplexInferBoundsParameters::getThreshold() const{
122 // return d_threshold;
125 // SimplexInferBoundsParameters::SimplexInferBoundsParameters(int p, bool ub)
127 // , d_upperBound(ub)
128 // , d_useThreshold(false)
133 InferBoundsResult::InferBoundsResult()
134 : d_foundBound(false)
135 , d_budgetExhausted(false)
136 , d_boundIsProvenOpt(false)
137 , d_inconsistentState(false)
138 , d_reachedThreshold(false)
140 , d_term(Node::null())
142 , d_explanation(Node::null())
145 InferBoundsResult::InferBoundsResult(Node term
, bool ub
)
146 : d_foundBound(false)
147 , d_budgetExhausted(false)
148 , d_boundIsProvenOpt(false)
149 , d_inconsistentState(false)
150 , d_reachedThreshold(false)
154 , d_explanation(Node::null())
157 bool InferBoundsResult::foundBound() const {
160 bool InferBoundsResult::boundIsOptimal() const {
161 return d_boundIsProvenOpt
;
163 bool InferBoundsResult::inconsistentState() const {
164 return d_inconsistentState
;
167 bool InferBoundsResult::boundIsInteger() const{
168 return foundBound() && d_value
.isIntegral();
171 bool InferBoundsResult::boundIsRational() const {
172 return foundBound() && d_value
.infinitesimalIsZero();
175 Integer
InferBoundsResult::valueAsInteger() const{
176 Assert(boundIsInteger());
177 return getValue().floor();
179 const Rational
& InferBoundsResult::valueAsRational() const{
180 Assert(boundIsRational());
181 return getValue().getNoninfinitesimalPart();
184 const DeltaRational
& InferBoundsResult::getValue() const{
188 Node
InferBoundsResult::getTerm() const { return d_term
; }
190 Node
InferBoundsResult::getLiteral() const{
191 const Rational
& q
= getValue().getNoninfinitesimalPart();
192 NodeManager
* nm
= NodeManager::currentNM();
193 Node qnode
= nm
->mkConst(q
);
198 Assert(getValue().infinitesimalSgn() <= 0);
199 k
= boundIsRational() ? kind::LEQ
: kind::LT
;
202 Assert(getValue().infinitesimalSgn() >= 0);
203 k
= boundIsRational() ? kind::GEQ
: kind::GT
;
205 Node atom
= nm
->mkNode(k
, getTerm(), qnode
);
206 Node lit
= Rewriter::rewrite(atom
);
210 /* If there is a bound, this is a node that explains the bound. */
211 Node
InferBoundsResult::getExplanation() const{
212 return d_explanation
;
216 void InferBoundsResult::setBound(const DeltaRational
& dr
, Node exp
){
222 //bool InferBoundsResult::foundBound() const { return d_foundBound; }
223 //bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; }
224 //bool InferBoundsResult::inconsistentState() const { return d_inconsistentState; }
227 void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted
= true; }
228 void InferBoundsResult::setReachedThreshold() { d_reachedThreshold
= true; }
229 void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt
= true; }
230 void InferBoundsResult::setInconsistent() { d_inconsistentState
= true; }
232 bool InferBoundsResult::thresholdWasReached() const{
233 return d_reachedThreshold
;
235 bool InferBoundsResult::budgetIsExhausted() const{
236 return d_budgetExhausted
;
239 std::ostream
& operator<<(std::ostream
& os
, const InferBoundsResult
& ibr
){
240 os
<< "{InferBoundsResult " << std::endl
;
241 os
<< "on " << ibr
.getTerm() << ", ";
242 if(ibr
.findUpperBound()){
243 os
<< "find upper bound, ";
245 os
<< "find lower bound, ";
247 if(ibr
.foundBound()){
248 os
<< "found a bound: ";
249 if(ibr
.boundIsInteger()){
250 os
<< ibr
.valueAsInteger() << "(int), ";
251 }else if(ibr
.boundIsRational()){
252 os
<< ibr
.valueAsRational() << "(rat), ";
254 os
<< ibr
.getValue() << "(extended), ";
257 os
<< "as term " << ibr
.getLiteral() << ", ";
258 os
<< "explanation " << ibr
.getExplanation() << ", ";
260 os
<< "did not find a bound, ";
263 if(ibr
.boundIsOptimal()){
267 if(ibr
.inconsistentState()){
268 os
<< "(inconsistent), ";
270 if(ibr
.budgetIsExhausted()){
271 os
<< "(budget exhausted), ";
273 if(ibr
.thresholdWasReached()){
274 os
<< "(reached threshold), ";
281 ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
282 : EntailmentCheckSideEffects(theory::THEORY_ARITH
)
283 , d_simplexSideEffects (NULL
)
286 ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
287 if(d_simplexSideEffects
!= NULL
){
288 delete d_simplexSideEffects
;
289 d_simplexSideEffects
= NULL
;
293 InferBoundsResult
& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
294 if(d_simplexSideEffects
== NULL
){
295 d_simplexSideEffects
= new InferBoundsResult
;
297 return *d_simplexSideEffects
;
300 namespace inferbounds
{ /* namespace arith */
302 std::ostream
& operator<<(std::ostream
& os
, const Algorithms a
){
304 case None
: os
<< "AlgNone"; break;
305 case Lookup
: os
<< "AlgLookup"; break;
306 case RowSum
: os
<< "AlgRowSum"; break;
307 case Simplex
: os
<< "AlgSimplex"; break;
315 } /* namespace inferbounds */
317 } /* namespace arith */
318 } /* namespace theory */
319 } /* namespace CVC4 */