src/theory/arith/infer_bounds.cpp

   1 /*********************                                                        */
   2 /*! \file infer_bounds.cpp
   3  ** \verbatim
   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
  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 InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
  32   : d_alg(a)
  33 {
  34   Assert(a != Simplex);
  35 }
  36
  37 InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds)
  38   : d_alg(Simplex)
  39 {}
  40
  41 Algorithms InferBoundAlgorithm::getAlgorithm() const{
  42   return d_alg;
  43 }
  44
  45 const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{
  46   Assert(getAlgorithm() == Simplex);
  47   return d_simplexRounds;
  48 }
  49
  50
  51 InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
  52   return InferBoundAlgorithm(Lookup);
  53 }
  54
  55 InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
  56   return InferBoundAlgorithm(RowSum);
  57 }
  58
  59 InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
  60   return InferBoundAlgorithm(rounds);
  61 }
  62
  63 ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
  64   : EntailmentCheckParameters(theory::THEORY_ARITH)
  65   , d_algorithms()
  66 {}
  67
  68 ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
  69 {}
  70
  71
  72 void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
  73   addAlgorithm(InferBoundAlgorithm::mkLookup());
  74   addAlgorithm(InferBoundAlgorithm::mkRowSum());
  75 }
  76
  77 void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){
  78   d_algorithms.push_back(alg);
  79 }
  80
  81 ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{
  82   return d_algorithms.begin();
  83 }
  84
  85 ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{
  86   return d_algorithms.end();
  87 }
  88
  89
  90 // SimplexInferBoundsParameters::SimplexInferBoundsParameters()
  91 //   : d_parameter(1)
  92 //   , d_upperBound(true)
  93 //   , d_threshold()
  94 // {}
  95
  96 // SimplexInferBoundsParameters::~SimplexInferBoundsParameters(){}
  97
  98
  99
 100 // int SimplexInferBoundsParameters::getSimplexRoundParameter() const {
 101 //   return d_parameter;
 102 // }
 103
 104 // bool SimplexInferBoundsParameters::findLowerBound() const {
 105 //   return ! findUpperBound();
 106 // }
 107
 108 // bool SimplexInferBoundsParameters::findUpperBound() const {
 109 //   return d_upperBound;
 110 // }
 111
 112 // void SimplexInferBoundsParameters::setThreshold(const DeltaRational& th){
 113 //   d_threshold = th;
 114 //   d_useThreshold = true;
 115 // }
 116
 117 // bool SimplexInferBoundsParameters::useThreshold() const{
 118 //   return d_useThreshold;
 119 // }
 120
 121 // const DeltaRational& SimplexInferBoundsParameters::getThreshold() const{
 122 //   return d_threshold;
 123 // }
 124
 125 // SimplexInferBoundsParameters::SimplexInferBoundsParameters(int p, bool ub)
 126 //   : d_parameter(p)
 127 //   , d_upperBound(ub)
 128 //   , d_useThreshold(false)
 129 //   , d_threshold()
 130 // {}
 131
 132
 133 InferBoundsResult::InferBoundsResult()
 134   : d_foundBound(false)
 135   , d_budgetExhausted(false)
 136   , d_boundIsProvenOpt(false)
 137   , d_inconsistentState(false)
 138   , d_reachedThreshold(false)
 139   , d_value(false)
 140   , d_term(Node::null())
 141   , d_upperBound(true)
 142   , d_explanation(Node::null())
 143 {}
 144
 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)
 151   , d_value(false)
 152   , d_term(term)
 153   , d_upperBound(ub)
 154   , d_explanation(Node::null())
 155 {}
 156
 157 bool InferBoundsResult::foundBound() const {
 158   return d_foundBound;
 159 }
 160 bool InferBoundsResult::boundIsOptimal() const {
 161   return d_boundIsProvenOpt;
 162 }
 163 bool InferBoundsResult::inconsistentState() const {
 164   return d_inconsistentState;
 165 }
 166
 167 bool InferBoundsResult::boundIsInteger() const{
 168   return foundBound() && d_value.isIntegral();
 169 }
 170
 171 bool InferBoundsResult::boundIsRational() const {
 172   return foundBound() && d_value.infinitesimalIsZero();
 173 }
 174
 175 Integer InferBoundsResult::valueAsInteger() const{
 176   Assert(boundIsInteger());
 177   return getValue().floor();
 178 }
 179 const Rational& InferBoundsResult::valueAsRational() const{
 180   Assert(boundIsRational());
 181   return getValue().getNoninfinitesimalPart();
 182 }
 183
 184 const DeltaRational& InferBoundsResult::getValue() const{
 185   return d_value;
 186 }
 187
 188 Node InferBoundsResult::getTerm() const { return d_term; }
 189
 190 Node InferBoundsResult::getLiteral() const{
 191   const Rational& q = getValue().getNoninfinitesimalPart();
 192   NodeManager* nm = NodeManager::currentNM();
 193   Node qnode = nm->mkConst(q);
 194
 195   Kind k;
 196   if(d_upperBound){
 197     // x <= q + c*delta
 198     Assert(getValue().infinitesimalSgn() <= 0);
 199     k = boundIsRational() ? kind::LEQ : kind::LT;
 200   }else{
 201     // x >= q + c*delta
 202     Assert(getValue().infinitesimalSgn() >= 0);
 203     k = boundIsRational() ? kind::GEQ : kind::GT;
 204   }
 205   Node atom = nm->mkNode(k, getTerm(), qnode);
 206   Node lit = Rewriter::rewrite(atom);
 207   return lit;
 208 }
 209
 210 /* If there is a bound, this is a node that explains the bound. */
 211 Node InferBoundsResult::getExplanation() const{
 212   return d_explanation;
 213 }
 214
 215
 216 void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
 217   d_foundBound = true;
 218   d_value = dr;
 219   d_explanation = exp;
 220 }
 221
 222 //bool InferBoundsResult::foundBound() const { return d_foundBound; }
 223 //bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; }
 224 //bool InferBoundsResult::inconsistentState() const { return d_inconsistentState; }
 225
 226
 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; }
 231
 232 bool InferBoundsResult::thresholdWasReached() const{
 233   return d_reachedThreshold;
 234 }
 235 bool InferBoundsResult::budgetIsExhausted() const{
 236   return d_budgetExhausted;
 237 }
 238
 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, ";
 244   }else{
 245     os << "find lower bound, ";
 246   }
 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), ";
 253     }else{
 254       os << ibr.getValue() << "(extended), ";
 255     }
 256
 257     os << "as term " << ibr.getLiteral() << ", ";
 258     os << "explanation " << ibr.getExplanation() << ", ";
 259   }else {
 260     os << "did not find a bound, ";
 261   }
 262
 263   if(ibr.boundIsOptimal()){
 264     os << "(opt), ";
 265   }
 266
 267   if(ibr.inconsistentState()){
 268     os << "(inconsistent), ";
 269   }
 270   if(ibr.budgetIsExhausted()){
 271     os << "(budget exhausted), ";
 272   }
 273   if(ibr.thresholdWasReached()){
 274     os << "(reached threshold), ";
 275   }
 276   os << "}";
 277   return os;
 278 }
 279
 280
 281 ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
 282   : EntailmentCheckSideEffects(theory::THEORY_ARITH)
 283   , d_simplexSideEffects (NULL)
 284 {}
 285
 286 ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
 287   if(d_simplexSideEffects != NULL){
 288     delete d_simplexSideEffects;
 289     d_simplexSideEffects = NULL;
 290   }
 291 }
 292
 293 InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
 294   if(d_simplexSideEffects == NULL){
 295     d_simplexSideEffects = new InferBoundsResult;
 296   }
 297   return *d_simplexSideEffects;
 298 }
 299
 300 namespace inferbounds { /* namespace arith */
 301
 302 std::ostream& operator<<(std::ostream& os,  const Algorithms a){
 303   switch(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;
 308   default:
 309     Unhandled();
 310   }
 311
 312   return os;
 313 }
 314
 315 } /* namespace inferbounds */
 316
 317 } /* namespace arith */
 318 } /* namespace theory */
 319 } /* namespace CVC4 */