GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_bound_inference.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_bound_inference.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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
 ** \brief Quantifiers bound inference
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
18
#define CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
19
20
#include <vector>
21
#include "expr/node.h"
22
23
namespace CVC4 {
24
namespace theory {
25
26
class RepSetIterator;
27
28
namespace quantifiers {
29
30
class BoundedIntegers;
31
32
/** Types of bounds that can be inferred for quantified formulas */
33
enum BoundVarType
34
{
35
  // a variable has a finite bound because it has finite cardinality
36
  BOUND_FINITE,
37
  // a variable has a finite bound because it is in an integer range, e.g.
38
  //   forall x. u <= x <= l => P(x)
39
  BOUND_INT_RANGE,
40
  // a variable has a finite bound because it is a member of a set, e.g.
41
  //   forall x. x in S => P(x)
42
  BOUND_SET_MEMBER,
43
  // a variable has a finite bound because only a fixed set of terms are
44
  // relevant for it in the domain of the quantified formula, e.g.
45
  //   forall x. ( x = t1 OR ... OR x = tn ) => P(x)
46
  BOUND_FIXED_SET,
47
  // a bound has not been inferred for the variable
48
  BOUND_NONE
49
};
50
51
/**
52
 * This class is the central utility for determining if the domain of a
53
 * quantified formula is finite, or whether its domain can be restricted to
54
 * a finite subdomain based on one of the above types.
55
 */
56
8992
class QuantifiersBoundInference
57
{
58
 public:
59
  /**
60
   * @param cardMax The maximum cardinality we consider to be small enough
61
   * to "complete" below.
62
   * @param isFmf Whether finite model finding (for uninterpreted sorts) is
63
   * enabled.
64
   */
65
  QuantifiersBoundInference(unsigned cardMax, bool isFmf = false);
66
  /** finish initialize */
67
  void finishInit(BoundedIntegers* b);
68
  /** may complete type
69
   *
70
   * Returns true if the type tn is closed enumerable, is interpreted as a
71
   * finite type, and has cardinality less than some reasonable value
72
   * (currently < 1000). This method caches the results of whether each type
73
   * may be completed.
74
   */
75
  bool mayComplete(TypeNode tn);
76
  /**
77
   * Static version of the above method where maximum cardinality is
78
   * configurable.
79
   */
80
  static bool mayComplete(TypeNode tn, unsigned cardMax);
81
  /** does variable v of quantified formula q have a finite bound? */
82
  bool isFiniteBound(Node q, Node v);
83
  /** get bound var type
84
   *
85
   * This returns the type of bound that was inferred for variable v of
86
   * quantified formula q.
87
   */
88
  BoundVarType getBoundVarType(Node q, Node v);
89
  /**
90
   * Get the indices of bound variables, in the order they should be processed
91
   * in a RepSetIterator.
92
   *
93
   * For details, see BoundedIntegers::getBoundVarIndices.
94
   */
95
  void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
96
  /**
97
   * Get bound elements
98
   *
99
   * This gets the (finite) enumeration of the range of variable v of quantified
100
   * formula q and adds it into the vector elements in the context of the
101
   * iteration being performed by rsi. It returns true if it could successfully
102
   * determine this range.
103
   *
104
   * For details, see BoundedIntegers::getBoundElements.
105
   */
106
  bool getBoundElements(RepSetIterator* rsi,
107
                        bool initial,
108
                        Node q,
109
                        Node v,
110
                        std::vector<Node>& elements) const;
111
112
 private:
113
  /** The maximum cardinality for which we complete */
114
  unsigned d_cardMax;
115
  /** Whether finite model finding is enabled */
116
  bool d_isFmf;
117
  /** may complete */
118
  std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
119
  /** The bounded integers module, which may help infer bounds */
120
  BoundedIntegers* d_bint;
121
};
122
123
}  // namespace quantifiers
124
}  // namespace theory
125
}  // namespace CVC4
126
127
#endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */