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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
|
/********************* */
/*! \file term_util.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Mathias Preiner
** This file is part of the CVC4 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.\endverbatim
**
** \brief term utilities class
**/
#include "cvc4_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
#define CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
#include <map>
#include "expr/attribute.h"
#include "expr/node.h"
namespace cvc5 {
namespace theory {
// attribute for "contains instantiation constants from"
struct InstConstantAttributeId {};
typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
struct BoundVarAttributeId {};
typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute;
struct InstVarNumAttributeId {};
typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
struct TermDepthAttributeId {};
typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
struct ContainsUConstAttributeId {};
typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
/**
* for quantifier instantiation level.
*/
struct QuantInstLevelAttributeId {};
typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t>
QuantInstLevelAttribute;
/** Attribute for id number */
struct QuantIdNumAttributeId {};
typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
namespace quantifiers {
// TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
class TermUtil
{
public:
TermUtil() {}
~TermUtil() {}
// for inst constant
public:
/** Get the index of BOUND_VARIABLE v in quantifier q */
static size_t getVariableNum(Node q, Node v);
static Node getInstConstAttr( Node n );
static bool hasInstConstAttr( Node n );
static Node getBoundVarAttr( Node n );
static bool hasBoundVarAttr( Node n );
private:
/** get bound vars */
static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited );
public:
//remove quantifiers
static Node getRemoveQuantifiers( Node n );
//quantified simplify (treat free variables in n as quantified and run rewriter)
static Node getQuantSimplify( Node n );
private:
/** adds the set of nodes of kind k in n to vars */
static void computeVarContainsInternal(Node n,
Kind k,
std::vector<Node>& vars);
public:
/** adds the set of nodes of kind INST_CONSTANT in n to ics */
static void computeInstConstContains(Node n, std::vector<Node>& ics);
/** adds the set of nodes of kind BOUND_VARIABLE in n to vars */
static void computeVarContains(Node n, std::vector<Node>& vars);
/** adds the set of (top-level) nodes of kind FORALL in n to quants */
static void computeQuantContains(Node n, std::vector<Node>& quants);
/**
* Adds the set of nodes of kind INST_CONSTANT in n that belong to quantified
* formula q to vars.
*/
static void computeInstConstContainsForQuant(Node q,
Node n,
std::vector<Node>& vars);
public:
/** contains uninterpreted constant */
static bool containsUninterpretedConstant( Node n );
/** get the term depth of n */
static int getTermDepth( Node n );
/** simple negate */
static Node simpleNegate( Node n );
/** is the kind k a negation kind?
*
* A kind k is a negation kind if <k>( <k>( n ) ) = n.
*/
static bool isNegate(Kind k);
/**
* Make negated term, returns the negation of n wrt Kind notk, eliminating
* double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x.
*/
static Node mkNegate(Kind notk, Node n);
/** is k associative?
*
* If flag reqNAry is true, then we additionally require that k is an
* n-ary operator.
*/
static bool isAssoc(Kind k, bool reqNAry = false);
/** is k commutative?
*
* If flag reqNAry is true, then we additionally require that k is an
* n-ary operator.
*/
static bool isComm(Kind k, bool reqNAry = false);
/** is k non-additive?
* Returns true if
* <k>( <k>( T1, x, T2 ), x ) =
* <k>( T1, x, T2 )
* always holds, where T1 and T2 are vectors.
*/
static bool isNonAdditive( Kind k );
/** is k a bool connective? */
static bool isBoolConnective( Kind k );
/** is n a bool connective term? */
static bool isBoolConnectiveTerm( TNode n );
/** is the kind k antisymmetric?
* If so, return true and store its inverse kind in dk.
*/
static bool isAntisymmetric(Kind k, Kind& dk);
/** has offset arg
* Returns true if there is a Kind ok and offset
* such that
* <ik>( ... t_{arg-1}, n, t_{arg+1}... ) =
* <ok>( ... t_{arg-1}, n+offset, t_{arg+1}...)
* always holds.
* If so, this function returns true and stores
* offset and ok in the respective fields.
*/
static bool hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok);
/** is idempotent arg
* Returns true if
* <k>( ... t_{arg-1}, n, t_{arg+1}...) =
* <k>( ... t_{arg-1}, t_{arg+1}...)
* always holds.
*/
static bool isIdempotentArg(Node n, Kind ik, int arg);
/** is singular arg
* Returns true if
* <k>( ... t_{arg-1}, n, t_{arg+1}...) = ret
* always holds for some constant ret, which is returned by this function.
*/
static Node isSingularArg(Node n, Kind ik, unsigned arg);
/** get type value with simple value
* This gets the Node that represents value val for Type tn
* This is used to get simple values, e.g. -1,0,1,
* in a uniform way per type.
*/
static Node mkTypeValue(TypeNode tn, int32_t val);
/** make type value with simple offset
* Returns the value of ( val + getTypeValue( tn, offset ) ),
* where + is the additive operator for the type.
* Stores the status (0: success, -1: failure) in status.
*/
static Node mkTypeValueOffset(TypeNode tn,
Node val,
int32_t offset,
int32_t& status);
/** make the "max" value for type tn
* For example,
* the max value for Bool is true,
* the max value for BitVector is 1..1.
*/
static Node mkTypeMaxValue(TypeNode tn);
/**
* Make const, returns pol ? mkTypeValue(tn,0) : mkTypeMaxValue(tn).
* In other words, this returns either the minimum element of tn if pol is
* true, and the maximum element in pol is false. The type tn should have
* minimum and maximum elements, for example tn is Bool or BitVector.
*/
static Node mkTypeConst(TypeNode tn, bool pol);
};/* class TermUtil */
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H */
|
