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