src/theory/arith/infer_bounds.h

   1 /*********************                                                        */
   2 /*! \file infer_bounds.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 : public EntailmentCheckParameters {
  62 private:
  63   typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg;
  64   VecInferBoundAlg d_algorithms;
  65
  66 public:
  67   typedef VecInferBoundAlg::const_iterator const_iterator;
  68
  69   ArithEntailmentCheckParameters();
  70   ~ArithEntailmentCheckParameters();
  71
  72   void addLookupRowSumAlgorithms();
  73   void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg);
  74
  75   const_iterator begin() const;
  76   const_iterator end() const;
  77 };
  78
  79
  80
  81 class InferBoundsResult {
  82 public:
  83   InferBoundsResult();
  84   InferBoundsResult(Node term, bool ub);
  85
  86   void setBound(const DeltaRational& dr, Node exp);
  87   bool foundBound() const;
  88
  89   void setIsOptimal();
  90   bool boundIsOptimal() const;
  91
  92   void setInconsistent();
  93   bool inconsistentState() const;
  94
  95   const DeltaRational& getValue() const;
  96   bool boundIsRational() const;
  97   const Rational& valueAsRational() const;
  98   bool boundIsInteger() const;
  99   Integer valueAsInteger() const;
 100
 101   Node getTerm() const;
 102   Node getLiteral() const;
 103   void setTerm(Node t){ d_term = t; }
 104
 105   /* If there is a bound, this is a node that explains the bound. */
 106   Node getExplanation() const;
 107
 108   bool budgetIsExhausted() const;
 109   void setBudgetExhausted();
 110
 111   bool thresholdWasReached() const;
 112   void setReachedThreshold();
 113
 114   bool findUpperBound() const { return d_upperBound; }
 115
 116   void setFindLowerBound() { d_upperBound = false; }
 117   void setFindUpperBound() { d_upperBound = true; }
 118 private:
 119   /* was a bound found */
 120   bool d_foundBound;
 121
 122   /* was the budget exhausted */
 123   bool d_budgetExhausted;
 124
 125   /* does the bound have to be optimal*/
 126   bool d_boundIsProvenOpt;
 127
 128   /* was this started on an inconsistent state. */
 129   bool d_inconsistentState;
 130
 131   /* reached the threshold. */
 132   bool d_reachedThreshold;
 133
 134   /* the value of the bound */
 135   DeltaRational d_value;
 136
 137   /* The input term. */
 138   Node d_term;
 139
 140   /* Was the bound found an upper or lower bound.*/
 141   bool d_upperBound;
 142
 143   /* Explanation of the bound. */
 144   Node d_explanation;
 145 };
 146
 147 std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr);
 148
 149 class ArithEntailmentCheckSideEffects : public EntailmentCheckSideEffects{
 150 public:
 151   ArithEntailmentCheckSideEffects();
 152   ~ArithEntailmentCheckSideEffects();
 153
 154   InferBoundsResult& getSimplexSideEffects();
 155
 156 private:
 157   InferBoundsResult* d_simplexSideEffects;
 158 };
 159
 160
 161 } /* namespace arith */
 162 } /* namespace theory */
 163 } /* namespace CVC4 */