src/theory/arith/infer_bounds.h

   1 /*********************                                                        */
   2 /*! \file infer_bounds.h
   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-2020 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 "cvc4_private.h"
  19
  20 #pragma once
  21
  22 #include <ostream>
  23
  24 #include "expr/node.h"
  25 #include "theory/arith/delta_rational.h"
  26 #include "theory/theory.h"
  27 #include "util/integer.h"
  28 #include "util/maybe.h"
  29 #include "util/rational.h"
  30
  31
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace arith {
  35
  36 namespace inferbounds {
  37   enum Algorithms {None = 0, Lookup, RowSum, Simplex};
  38   enum SimplexParamKind { Unbounded, NumVars, Direct};
  39
  40 class InferBoundAlgorithm {
  41 private:
  42   Algorithms d_alg;
  43   Maybe<int> d_simplexRounds;
  44   InferBoundAlgorithm(Algorithms a);
  45   InferBoundAlgorithm(const Maybe<int>& simplexRounds);
  46
  47 public:
  48   InferBoundAlgorithm();
  49
  50   Algorithms getAlgorithm() const;
  51   const Maybe<int>& getSimplexRounds() const;
  52
  53   static InferBoundAlgorithm mkLookup();
  54   static InferBoundAlgorithm mkRowSum();
  55   static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
  56 };
  57
  58 std::ostream& operator<<(std::ostream& os, const Algorithms a);
  59 } /* namespace inferbounds */
  60
  61 class ArithEntailmentCheckParameters
  62 {
  63  private:
  64   typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg;
  65   VecInferBoundAlg d_algorithms;
  66
  67 public:
  68   typedef VecInferBoundAlg::const_iterator const_iterator;
  69
  70   ArithEntailmentCheckParameters();
  71   ~ArithEntailmentCheckParameters();
  72
  73   void addLookupRowSumAlgorithms();
  74   void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg);
  75
  76   const_iterator begin() const;
  77   const_iterator end() const;
  78 };
  79
  80
  81
  82 class InferBoundsResult {
  83 public:
  84   InferBoundsResult();
  85   InferBoundsResult(Node term, bool ub);
  86
  87   void setBound(const DeltaRational& dr, Node exp);
  88   bool foundBound() const;
  89
  90   void setIsOptimal();
  91   bool boundIsOptimal() const;
  92
  93   void setInconsistent();
  94   bool inconsistentState() const;
  95
  96   const DeltaRational& getValue() const;
  97   bool boundIsRational() const;
  98   const Rational& valueAsRational() const;
  99   bool boundIsInteger() const;
 100   Integer valueAsInteger() const;
 101
 102   Node getTerm() const;
 103   Node getLiteral() const;
 104   void setTerm(Node t){ d_term = t; }
 105
 106   /* If there is a bound, this is a node that explains the bound. */
 107   Node getExplanation() const;
 108
 109   bool budgetIsExhausted() const;
 110   void setBudgetExhausted();
 111
 112   bool thresholdWasReached() const;
 113   void setReachedThreshold();
 114
 115   bool findUpperBound() const { return d_upperBound; }
 116
 117   void setFindLowerBound() { d_upperBound = false; }
 118   void setFindUpperBound() { d_upperBound = true; }
 119 private:
 120   /* was a bound found */
 121   bool d_foundBound;
 122
 123   /* was the budget exhausted */
 124   bool d_budgetExhausted;
 125
 126   /* does the bound have to be optimal*/
 127   bool d_boundIsProvenOpt;
 128
 129   /* was this started on an inconsistent state. */
 130   bool d_inconsistentState;
 131
 132   /* reached the threshold. */
 133   bool d_reachedThreshold;
 134
 135   /* the value of the bound */
 136   DeltaRational d_value;
 137
 138   /* The input term. */
 139   Node d_term;
 140
 141   /* Was the bound found an upper or lower bound.*/
 142   bool d_upperBound;
 143
 144   /* Explanation of the bound. */
 145   Node d_explanation;
 146 };
 147
 148 std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr);
 149
 150 class ArithEntailmentCheckSideEffects
 151 {
 152  public:
 153   ArithEntailmentCheckSideEffects();
 154   ~ArithEntailmentCheckSideEffects();
 155
 156   InferBoundsResult& getSimplexSideEffects();
 157
 158 private:
 159   InferBoundsResult* d_simplexSideEffects;
 160 };
 161
 162
 163 } /* namespace arith */
 164 } /* namespace theory */
 165 } /* namespace CVC4 */