src/theory/arith/infer_bounds.cpp

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