Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Term context utilities.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__EXPR__TERM_CONTEXT_H
19 : : #define CVC5__EXPR__TERM_CONTEXT_H
20 : :
21 : : #include "expr/node.h"
22 : : #include "theory/theory_id.h"
23 : :
24 : : namespace cvc5::internal {
25 : :
26 : : /**
27 : : * This is an abstract class for computing "term context identifiers". A term
28 : : * context identifier is a hash value that identifies some property of the
29 : : * context in which a term occurs. Common examples of the implementation of
30 : : * such a mapping are implemented in the subclasses below.
31 : : *
32 : : * A term context identifier is intended to be information that can be locally
33 : : * computed from the parent's hash, and hence does not rely on maintaining
34 : : * paths.
35 : : *
36 : : * In the below documentation, we write t @ [p] to a term at a given position,
37 : : * where p is a list of indices. For example, the atomic subterms of:
38 : : * (and P (not Q))
39 : : * are P @ [0] and Q @ [1,0].
40 : : */
41 : : class TermContext
42 : : {
43 : : public:
44 : 128979 : TermContext() {}
45 : 128459 : virtual ~TermContext() {}
46 : : /** The default initial value of root terms. */
47 : : virtual uint32_t initialValue() const = 0;
48 : : /**
49 : : * Returns the term context identifier of the index^th child of t, where tval
50 : : * is the term context identifier of t.
51 : : */
52 : : virtual uint32_t computeValue(TNode t, uint32_t tval, size_t index) const = 0;
53 : : /**
54 : : * Returns the term context identifier of the operator of t, where tval
55 : : * is the term context identifier of t.
56 : : */
57 : : virtual uint32_t computeValueOp(TNode t, uint32_t tval) const;
58 : : };
59 : :
60 : : /**
61 : : * Remove term formulas (rtf) term context.
62 : : *
63 : : * Computes whether we are inside a term (as opposed to being part of Boolean
64 : : * skeleton) and whether we are inside a quantifier. For example, for:
65 : : * (and (= a b) (forall ((x Int)) (P x)))
66 : : * we have the following mappings (term -> inTerm,inQuant)
67 : : * (= a b) @ [0] -> false, false
68 : : * a @ [0,1] -> true, false
69 : : * (P x) @ [1,1] -> false, true
70 : : * x @ [1,1,0] -> true, true
71 : : * Notice that the hash of a child can be computed from the parent's hash only,
72 : : * and hence this can be implemented as an instance of the abstract class.
73 : : */
74 : : class RtfTermContext : public TermContext
75 : : {
76 : : public:
77 : 101190 : RtfTermContext() {}
78 : : /** The initial value: not in a term context or beneath a quantifier. */
79 : : uint32_t initialValue() const override;
80 : : /** Compute the value of the index^th child of t whose hash is tval */
81 : : uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
82 : : /** get hash value from the flags */
83 : : static uint32_t getValue(bool inQuant, bool inTerm);
84 : : /** get flags from the hash value */
85 : : static void getFlags(uint32_t val, bool& inQuant, bool& inTerm);
86 : :
87 : : private:
88 : : /**
89 : : * Returns true if the children of t should be considered in a "term" context,
90 : : * which is any context beneath a symbol that does not belong to the Boolean
91 : : * theory as well as other exceptions like equality, separation logic
92 : : * connectives and bit-vector eager atoms.
93 : : */
94 : : static bool hasNestedTermChildren(TNode t);
95 : : };
96 : :
97 : : /**
98 : : * Simpler version of above that only computes whether we are inside a
99 : : * quantifier.
100 : : */
101 : : class InQuantTermContext : public TermContext
102 : : {
103 : : public:
104 : : InQuantTermContext() {}
105 : : /** The initial value: not beneath a quantifier. */
106 : : uint32_t initialValue() const override;
107 : : /** Compute the value of the index^th child of t whose hash is tval */
108 : : uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
109 : : /** get hash value from the flags */
110 : : static uint32_t getValue(bool inQuant);
111 : : /** get flags from the hash value */
112 : : static bool inQuant(uint32_t val, bool& inQuant);
113 : : };
114 : :
115 : : /**
116 : : * Polarity term context.
117 : : *
118 : : * This class computes the polarity of a term-context-sensitive term, which is
119 : : * one of {true, false, none}. This corresponds to the value that can be
120 : : * assigned to that term while preservering satisfiability of the overall
121 : : * formula, or none if such a value does not exist. If not "none", this
122 : : * typically corresponds to whether the number of NOT the formula is beneath is
123 : : * even, although special cases exist (e.g. the first child of IMPLIES).
124 : : *
125 : : * For example, given the formula:
126 : : * (and P (not (= (f x) 0)))
127 : : * assuming the root of this formula has true polarity, we have that:
128 : : * P @ [0] -> true
129 : : * (not (= (f x) 0)) @ [1] -> true
130 : : * (= (f x) 0) @ [1,0] -> false
131 : : * (f x) @ [1,0,0]), x @ [1,0,0,0]), 0 @ [1,0,1] -> none
132 : : *
133 : : * Notice that a term-context-sensitive Node is not one-to-one with Node.
134 : : * In particular, given the formula:
135 : : * (and P (not P))
136 : : * We have that the P at path [0] has polarity true and the P at path [1,0] has
137 : : * polarity false.
138 : : *
139 : : * Finally, notice that polarity does not correspond to a value that the
140 : : * formula entails. Thus, for the formula:
141 : : * (or P Q)
142 : : * we have that
143 : : * P @ [0] -> true
144 : : * Q @ [1] -> true
145 : : * although neither is entailed.
146 : : *
147 : : * Notice that the hash of a child can be computed from the parent's hash only.
148 : : */
149 : : class PolarityTermContext : public TermContext
150 : : {
151 : : public:
152 : 3947 : PolarityTermContext() {}
153 : : /** The initial value: true polarity. */
154 : : uint32_t initialValue() const override;
155 : : /** Compute the value of the index^th child of t whose hash is tval */
156 : : uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
157 : : /**
158 : : * Get hash value from the flags, where hasPol false means no polarity.
159 : : */
160 : : static uint32_t getValue(bool hasPol, bool pol);
161 : : /**
162 : : * get flags from the hash value. If we have no polarity, both hasPol and pol
163 : : * are set to false.
164 : : */
165 : : static void getFlags(uint32_t val, bool& hasPol, bool& pol);
166 : : };
167 : :
168 : : /**
169 : : * Similar to InQuantTermContext, but computes whether we are below a theory
170 : : * leaf of given theory id.
171 : : */
172 : : class TheoryLeafTermContext : public TermContext
173 : : {
174 : : public:
175 : 19238 : TheoryLeafTermContext(theory::TheoryId id) : d_theoryId(id) {}
176 : : /** The initial value: not beneath a theory leaf. */
177 : : uint32_t initialValue() const override;
178 : : /** Compute the value of the index^th child of t whose hash is tval */
179 : : uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
180 : :
181 : : private:
182 : : theory::TheoryId d_theoryId;
183 : : };
184 : :
185 : : /**
186 : : * Boolean skeleton term context.
187 : : * Returns 0 for terms that are part of a Boolean skeleton, 1 otherwise.
188 : : */
189 : : class BoolSkeletonTermContext : public TermContext
190 : : {
191 : : public:
192 : 611 : BoolSkeletonTermContext() {}
193 : : /** The initial value: assumed to be 0, i.e. in the Boolean skeleton. */
194 : : uint32_t initialValue() const override;
195 : : /** Compute the value of the index^th child of t whose hash is tval */
196 : : uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
197 : : };
198 : :
199 : : /**
200 : : * Returns 1 if we are in a term of Kind k, 0 otherwise.
201 : : */
202 : : class WithinKindTermContext : public TermContext
203 : : {
204 : : public:
205 : 3993 : WithinKindTermContext(Kind k) : d_kind(k) {}
206 : : /** The initial value: not within kind. */
207 : : uint32_t initialValue() const override;
208 : : /** Compute the value of the index^th child of t whose hash is tval */
209 : : uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
210 : :
211 : : protected:
212 : : /** The kind */
213 : : Kind d_kind;
214 : : };
215 : : } // namespace cvc5::internal
216 : :
217 : : #endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
|
