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