src/theory/arith/bound_inference.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Gereon Kremer
   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  * Extract bounds on variables from theory atoms.
  14  */
  15
  16 #ifndef CVC5__THEORY__ARITH__BOUND_INFERENCE_H
  17 #define CVC5__THEORY__ARITH__BOUND_INFERENCE_H
  18
  19 #include <map>
  20 #include <utility>
  21 #include <vector>
  22
  23 #include "expr/node.h"
  24 #include "smt/env_obj.h"
  25
  26 namespace cvc5 {
  27 namespace theory {
  28 namespace arith {
  29
  30   struct Bounds
  31   {
  32     /** The lower bound value */
  33     Node lower_value;
  34     /** Whether the lower bound is strict or weak */
  35     bool lower_strict = true;
  36     /** The lower bound as constraint */
  37     Node lower_bound;
  38     /** The origin of the lower bound */
  39     Node lower_origin;
  40     /** The upper bound value */
  41     Node upper_value;
  42     /** Whether the upper bound is strict or weak */
  43     bool upper_strict = true;
  44     /** The upper bound as constraint */
  45     Node upper_bound;
  46     /** The origin of the upper bound */
  47     Node upper_origin;
  48   };
  49
  50   /** Print the current bounds. */
  51   std::ostream& operator<<(std::ostream& os, const Bounds& b);
  52
  53   /**
  54    * A utility class that extracts direct bounds on arithmetic terms from theory
  55    * atoms.
  56    */
  57   class BoundInference : protected EnvObj
  58   {
  59    public:
  60     BoundInference(Env& env);
  61     void reset();
  62
  63     /**
  64      * Get the current interval for lhs. Creates a new (full) interval if
  65      * necessary.
  66      */
  67     Bounds& get_or_add(const Node& lhs);
  68     /**
  69      * Get the current interval for lhs. Returns a full interval if no interval
  70      * was derived yet.
  71      */
  72     Bounds get(const Node& lhs) const;
  73
  74     /** Return the current term bounds as an interval assignment. */
  75     const std::map<Node, Bounds>& get() const;
  76
  77     /**
  78      * Add a new theory atom. Return true if the theory atom induces a new
  79      * term bound.
  80      * If onlyVariables is true, the left hand side needs to be a single
  81      * variable to induce a bound.
  82      */
  83     bool add(const Node& n, bool onlyVariables = true);
  84
  85     /**
  86      * Post-processes a set of nodes and replaces bounds by their origins.
  87      * This utility sometimes creates new bounds, either due to tightening of
  88      * integer terms or because an equality was derived from two weak
  89      * inequalities. While the origins of these new bounds are recorded in
  90      * lower_origin and upper_origin, this method can be used to conveniently
  91      * replace these new nodes by their origins.
  92      * This can be used, for example, when constructing conflicts.
  93      */
  94     void replaceByOrigins(std::vector<Node>& nodes) const;
  95
  96    private:
  97     /** The currently strictest bounds for every lhs. */
  98     std::map<Node, Bounds> d_bounds;
  99
 100     /** Updates the lower bound for the given lhs */
 101     void update_lower_bound(const Node& origin,
 102                             const Node& lhs,
 103                             const Node& value,
 104                             bool strict);
 105     /** Updates the upper bound for the given lhs */
 106     void update_upper_bound(const Node& origin,
 107                             const Node& lhs,
 108                             const Node& value,
 109                             bool strict);
 110   };
 111
 112 /** Print the current variable bounds. */
 113 std::ostream& operator<<(std::ostream& os, const BoundInference& bi);
 114
 115 }  // namespace arith
 116 }  // namespace theory
 117 }  // namespace cvc5
 118
 119 #endif