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