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