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 : : * The Evaluator class.
11 : : *
12 : : * The Evaluator class can be used to evaluate terms with constant leaves
13 : : * quickly, without going through the rewriter.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__EVALUATOR_H
19 : : #define CVC5__THEORY__EVALUATOR_H
20 : :
21 : : #include <utility>
22 : : #include <vector>
23 : :
24 : : #include "base/output.h"
25 : : #include "expr/node.h"
26 : : #include "util/bitvector.h"
27 : : #include "util/rational.h"
28 : : #include "util/string.h"
29 : : #include "util/uninterpreted_sort_value.h"
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : :
34 : : /**
35 : : * Struct that holds the result of an evaluation. The actual value is stored in
36 : : * a union to avoid the overhead of a class hierarchy with virtual methods.
37 : : */
38 : : struct EvalResult
39 : : {
40 : : /* Describes which type of result is being stored */
41 : : enum
42 : : {
43 : : BOOL,
44 : : BITVECTOR,
45 : : RATIONAL,
46 : : STRING,
47 : : UVALUE,
48 : : INVALID
49 : : } d_tag;
50 : :
51 : : /* Stores the actual result */
52 : : union
53 : : {
54 : : bool d_bool;
55 : : BitVector d_bv;
56 : : Rational d_rat;
57 : : String d_str;
58 : : UninterpretedSortValue d_av;
59 : : };
60 : :
61 : : EvalResult(const EvalResult& other);
62 : 64527952 : EvalResult() : d_tag(INVALID) {}
63 : 19350143 : EvalResult(bool b) : d_tag(BOOL), d_bool(b) {}
64 : 1150401 : EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
65 : 5417270 : EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
66 : 155084 : EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
67 : 169 : EvalResult(const UninterpretedSortValue& av) : d_tag(UVALUE), d_av(av) {}
68 : :
69 : : EvalResult& operator=(const EvalResult& other);
70 : :
71 : : ~EvalResult();
72 : :
73 : : /**
74 : : * Converts the result to a Node. If the result is not valid, this function
75 : : * returns the null node. This method takes a type to distinguish integer
76 : : * and real constants, which are both represented as RATIONAL results.
77 : : */
78 : : Node toNode(const TypeNode& tn) const;
79 : : };
80 : :
81 : : class Rewriter;
82 : :
83 : : /**
84 : : * The class that performs the actual evaluation of a term under a
85 : : * substitution. Right now, the class does not cache anything between different
86 : : * calls to `eval` but this might change in the future.
87 : : */
88 : : class Evaluator
89 : : {
90 : : public:
91 : : /**
92 : : * @param rr (optional) the rewriter to use when a node cannot be evaluated.
93 : : * @param strAlphaCard The assumed cardinality of the alphabet for strings.
94 : : */
95 : : Evaluator(Rewriter* rr, uint32_t strAlphaCard = 196608);
96 : : /**
97 : : * Evaluates node `n` under the substitution described by the variable names
98 : : * `args` and the corresponding values `vals`. This method uses evaluation
99 : : * for subterms that evaluate to constants supported in the EvalResult
100 : : * class and substitution with rewriting for the others.
101 : : *
102 : : * The nodes in vals are typically intended to be constant, although this
103 : : * is not required.
104 : : *
105 : : * If the parameter useRewriter is true, then we may invoke calls to the
106 : : * rewriter for computing the result of this method.
107 : : *
108 : : * The result of this call is either equivalent to:
109 : : * (1) rewrite(n.substitute(args,vars))
110 : : * (2) Node::null().
111 : : * If d_rr is non-null, then we are always in the first case. If
112 : : * useRewriter is null, then we may be in case (2) if computing the
113 : : * rewritten, substituted form of n could not be determined by evaluation.
114 : : */
115 : : Node eval(TNode n,
116 : : const std::vector<Node>& args,
117 : : const std::vector<Node>& vals) const;
118 : : /**
119 : : * Same as above, but with a precomputed visited map.
120 : : */
121 : : Node eval(TNode n,
122 : : const std::vector<Node>& args,
123 : : const std::vector<Node>& vals,
124 : : const std::unordered_map<Node, Node>& visited) const;
125 : :
126 : : private:
127 : : /**
128 : : * Evaluates node `n` under the substitution described by the variable names
129 : : * `args` and the corresponding values `vals`. The internal version returns
130 : : * an EvalResult which has slightly less overhead for recursive calls.
131 : : *
132 : : * The method returns an invalid EvalResult if the result of the substitution
133 : : * on n does not result in a constant value that is one of those supported in
134 : : * the EvalResult class. Notice that e.g. datatype constants are not supported
135 : : * in this class.
136 : : *
137 : : * This method additionally adds subterms of n that could not be evaluated
138 : : * (in the above sense) to the map evalAsNode. For each such subterm n', we
139 : : * store the node corresponding to the result of applying the substitution
140 : : * `args` to `vals` and rewriting. Notice that this map contains an entry
141 : : * for n in the case that it cannot be evaluated.
142 : : */
143 : : EvalResult evalInternal(TNode n,
144 : : const std::vector<Node>& args,
145 : : const std::vector<Node>& vals,
146 : : std::unordered_map<TNode, Node>& evalAsNode,
147 : : std::unordered_map<TNode, EvalResult>& results) const;
148 : : /** reconstruct
149 : : *
150 : : * This function reconstructs the result of evaluating n using a combination
151 : : * of evaluation results (eresults) and substitution+rewriting (evalAsNode).
152 : : *
153 : : * Arguments eresults and evalAsNode are built within the context of the
154 : : * above method for some args and vals. This method ensures that the return
155 : : * value is equivalent to the rewritten form of n * { args -> vals }.
156 : : */
157 : : Node reconstruct(TNode n,
158 : : std::unordered_map<TNode, EvalResult>& eresults,
159 : : std::unordered_map<TNode, Node>& evalAsNode) const;
160 : : /**
161 : : * Process unhandled, called when n cannot be evaluated. This updates
162 : : * evalAsNode and results with the proper entries for this case. The term
163 : : * nv is the (Node) value of n if it exists, otherwise if needsReconstruct
164 : : * is true, the value of n is reconstructed based on evalAsNode and results.
165 : : */
166 : : void processUnhandled(TNode n,
167 : : TNode nv,
168 : : std::unordered_map<TNode, Node>& evalAsNode,
169 : : std::unordered_map<TNode, EvalResult>& results,
170 : : bool needsReconstruct) const;
171 : : /** The (optional) rewriter to be used */
172 : : Rewriter* d_rr;
173 : : /** The cardinality of the alphabet of strings */
174 : : uint32_t d_alphaCard;
175 : : };
176 : :
177 : : } // namespace theory
178 : : } // namespace cvc5::internal
179 : :
180 : : #endif /* CVC5__THEORY__EVALUATOR_H */
|
