GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fmf/bounded_integers.h Lines: 14 14 100.0 %
Date: 2021-03-23 Branches: 10 16 62.5 %

Line Exec Source
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
630
 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
499477
   std::string identify() const override
111
   {
112
499477
     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
148
  class BoundInstTrie
148
  {
149
  public:
150
    std::map< Node, BoundInstTrie > d_children;
151
2784
    bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){
152
2784
      if( index>=(int)vals.size() ){
153
1252
        return !madeNew;
154
      }else{
155
3064
        Node n = vals[index];
156
1532
        if( d_children.find(n)==d_children.end() ){
157
58
          madeNew = true;
158
        }
159
1532
        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
10636
  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
624
  Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
227
624
  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