src/theory/quantifiers/fmf/bounded_integers.h

   1 /*********************                                                        */
   2 /*! \file bounded_integers.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Mudathir Mohamed
   6  ** This file is part of the CVC4 project.
   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.\endverbatim
  11  **
  12  ** [[ Add lengthier description here ]]
  13  ** \todo document this file
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef CVC4__BOUNDED_INTEGERS_H
  19 #define CVC4__BOUNDED_INTEGERS_H
  20
  21 #include "theory/quantifiers/quant_module.h"
  22
  23 #include "context/cdhashmap.h"
  24 #include "context/context.h"
  25 #include "expr/attribute.h"
  26 #include "theory/decision_strategy.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30
  31 class RepSetIterator;
  32 class DecisionManager;
  33
  34 /**
  35  * Attribute set to 1 for literals that comprise the bounds of a quantified
  36  * formula. For example, for:
  37  *   forall x. ( 0 <= x ^ x <= n ) => P( x )
  38  * the literals 0 <= x and x <= n are marked 1.
  39  */
  40 struct BoundIntLitAttributeId
  41 {
  42 };
  43 typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
  44
  45 namespace quantifiers {
  46
  47 class BoundedIntegers : public QuantifiersModule
  48 {
  49   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  50   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
  51   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  52   typedef context::CDHashMap<int, bool> IntBoolMap;
  53 private:
  54   //for determining bounds
  55   bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited );
  56   bool hasNonBoundVar( Node f, Node b );
  57   /** The bound type for each quantified formula, variable pair */
  58   std::map<Node, std::map<Node, BoundVarType>> d_bound_type;
  59   /**
  60    * The ordered list of variables that are finitely bound, for each quantified
  61    * formulas. Variables that occur later in this list may depend on having
  62    * finite bounds for variables earlier in this list.
  63    */
  64   std::map< Node, std::vector< Node > > d_set;
  65   std::map< Node, std::map< Node, int > > d_set_nums;
  66   std::map< Node, std::map< Node, Node > > d_range;
  67   std::map< Node, std::map< Node, Node > > d_nground_range;
  68   //integer lower/upper bounds
  69   std::map< Node, std::map< Node, Node > > d_bounds[2];
  70   //set membership range
  71   std::map< Node, std::map< Node, Node > > d_setm_range;
  72   std::map< Node, std::map< Node, Node > > d_setm_range_lit;
  73   /** set membership element choice functions
  74    *
  75    * For each set S and integer n, d_setm_choice[S][n] is the canonical
  76    * representation for the (n+1)^th member of set S. It is of the form:
  77    * witness x. (|S| <= n OR ( x in S AND
  78    *   distinct( x, d_setm_choice[S][0], ..., d_setm_choice[S][n-1] ) ) )
  79    */
  80   std::map<Node, std::vector<Node> > d_setm_choice;
  81   //fixed finite set range
  82   std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range;
  83   std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range;
  84   void process( Node q, Node n, bool pol,
  85                 std::map< Node, unsigned >& bound_lit_type_map,
  86                 std::map< int, std::map< Node, Node > >& bound_lit_map,
  87                 std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
  88                 std::map< int, std::map< Node, Node > >& bound_int_range_term,
  89                 std::map< Node, std::vector< Node > >& bound_fixed_set );
  90   bool processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases );
  91   void processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited );
  92   std::vector< Node > d_bound_quants;
  93 private:
  94  /**
  95   * This decision strategy is used for minimizing the value of an integer
  96   * arithmetic term t. It decides positively on literals of the form
  97   * t < 0, t <= 0, t <= 1, t <=2, and so on.
  98   */
  99  class IntRangeDecisionHeuristic : public DecisionStrategyFmf
 100  {
 101   public:
 102    IntRangeDecisionHeuristic(Node r,
 103                              context::Context* c,
 104                              context::Context* u,
 105                              Valuation valuation,
 106                              bool isProxy);
 107    /** make the n^th literal of this strategy */
 108    Node mkLiteral(unsigned n) override;
 109    /** identify */
 110    std::string identify() const override
 111    {
 112      return std::string("bound_int_range");
 113    }
 114    /** Returns the current proxy lemma if one exists (see below). */
 115    Node proxyCurrentRangeLemma();
 116
 117   private:
 118    /** The range we are minimizing */
 119    Node d_range;
 120    /** a proxy of the range
 121     *
 122     * When option::fmfBoundLazy is enabled, this class uses a lazy strategy
 123     * for enforcing the bounds on term t by using a fresh variable x of type
 124     * integer. The point of this variable is to serve as a proxy for t, so
 125     * that we can decide on literals of the form x <= c instead of t <= c. The
 126     * advantage of this is that we avoid unfairness, say, if t is constrained
 127     * to be strictly greater c. Then, at full effort check, we add "proxy
 128     * lemmas" of the form: (t <= c) <=> (x <= c) for the current minimal
 129     * upper bound c for x.
 130     */
 131    Node d_proxy_range;
 132    /** ranges that have been proxied
 133     *
 134     * This is a user-context-dependent cache that stores which value we have
 135     * added proxy lemmas for.
 136     */
 137    IntBoolMap d_ranges_proxied;
 138   };
 139 private:
 140   //information for minimizing ranges
 141   std::vector< Node > d_ranges;
 142   /** Decision heuristics for each integer range */
 143   std::map<Node, std::unique_ptr<IntRangeDecisionHeuristic>> d_rms;
 144
 145  private:
 146   //class to store whether bounding lemmas have been added
 147   class BoundInstTrie
 148   {
 149   public:
 150     std::map< Node, BoundInstTrie > d_children;
 151     bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){
 152       if( index>=(int)vals.size() ){
 153         return !madeNew;
 154       }else{
 155         Node n = vals[index];
 156         if( d_children.find(n)==d_children.end() ){
 157           madeNew = true;
 158         }
 159         return d_children[n].hasInstantiated(vals,index+1,madeNew);
 160       }
 161     }
 162   };
 163   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
 164
 165  public:
 166   BoundedIntegers(QuantifiersEngine* qe,
 167                   QuantifiersState& qs,
 168                   QuantifiersInferenceManager& qim,
 169                   QuantifiersRegistry& qr,
 170                   DecisionManager* dm);
 171   virtual ~BoundedIntegers();
 172
 173   void presolve() override;
 174   bool needsCheck(Theory::Effort e) override;
 175   void check(Theory::Effort e, QEffort quant_e) override;
 176   void checkOwnership(Node q) override;
 177   /**
 178    * Is v a variable of quantified formula q that this class has inferred to
 179    * have a finite bound?
 180    */
 181   bool isBound(Node q, Node v) const;
 182   /**
 183    * Get the type of bound that was inferred for variable v of quantified
 184    * formula q, or BOUND_NONE if no bound was inferred.
 185    */
 186   BoundVarType getBoundVarType(Node q, Node v) const;
 187   /**
 188    * Get the indices of bound variables, in the order they should be processed
 189    * in a RepSetIterator. For example, for q:
 190    *   forall xyz. 0 <= x < 5 ^ 0 <= z <= x+7 => P(x,y,z)
 191    * this would add {1,3} to the vector indices, indicating that x has a finite
 192    * bound, z has a finite bound assuming x has a finite bound, and y does not
 193    * have a finite bound.
 194    */
 195   void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
 196   /**
 197    * Get bound elements
 198    *
 199    * This gets the (finite) enumeration of the range of variable v of quantified
 200    * formula q and adds it into the vector elements in the context of the
 201    * iteration being performed by rsi. It returns true if it could successfully
 202    * determine this range.
 203    *
 204    * This method determines the range of a variable depending on the current
 205    * state of the iterator rsi and flag initial (which is true when rsi is
 206    * being initialized). For example, if q is:
 207    *   forall xy. 0 <= x < 5 ^ 0 <= y <= x+7 => P(x,y)
 208    * v is y, and rsi currently maps x to 4, then we add the elements 0...11 to
 209    * the vector elements.
 210    */
 211   bool getBoundElements(RepSetIterator* rsi,
 212                         bool initial,
 213                         Node q,
 214                         Node v,
 215                         std::vector<Node>& elements);
 216   /** Identify this module */
 217   std::string identify() const override { return "BoundedIntegers"; }
 218
 219  private:
 220   /**
 221    * Set that variable v of quantified formula q has a finite bound, where
 222    * bound_type indicates how that bound was inferred.
 223    */
 224   void setBoundedVar(Node f, Node v, BoundVarType bound_type);
 225   //for integer range
 226   Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
 227   Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; }
 228   void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
 229   void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
 230   bool isGroundRange(Node f, Node v);
 231   //for set range
 232   Node getSetRange( Node q, Node v, RepSetIterator * rsi );
 233   Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi );
 234   Node matchBoundVar( Node v, Node t, Node e );
 235
 236   bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
 237   /** Pointer to the decision manager */
 238   DecisionManager* d_dm;
 239 };
 240
 241 }
 242 }
 243 }
 244
 245 #endif