1 /********************* */
4 ** Top contributors (to current version):
5 ** Andres Noetzli, Andrew Reynolds, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief The Evaluator class
14 ** The Evaluator class can be used to evaluate terms with constant leaves
15 ** quickly, without going through the rewriter.
18 #include "cvc4_private.h"
20 #ifndef CVC4__THEORY__EVALUATOR_H
21 #define CVC4__THEORY__EVALUATOR_H
26 #include "base/output.h"
27 #include "expr/node.h"
28 #include "expr/uninterpreted_constant.h"
29 #include "util/bitvector.h"
30 #include "util/rational.h"
31 #include "util/string.h"
37 * Struct that holds the result of an evaluation. The actual value is stored in
38 * a union to avoid the overhead of a class hierarchy with virtual methods.
42 /* Describes which type of result is being stored */
53 /* Stores the actual result */
60 UninterpretedConstant d_uc
;
63 EvalResult(const EvalResult
& other
);
64 EvalResult() : d_tag(INVALID
) {}
65 EvalResult(bool b
) : d_tag(BOOL
), d_bool(b
) {}
66 EvalResult(const BitVector
& bv
) : d_tag(BITVECTOR
), d_bv(bv
) {}
67 EvalResult(const Rational
& i
) : d_tag(RATIONAL
), d_rat(i
) {}
68 EvalResult(const String
& str
) : d_tag(STRING
), d_str(str
) {}
69 EvalResult(const UninterpretedConstant
& u
) : d_tag(UCONST
), d_uc(u
) {}
71 EvalResult
& operator=(const EvalResult
& other
);
76 * Converts the result to a Node. If the result is not valid, this function
77 * returns the null node.
83 * The class that performs the actual evaluation of a term under a
84 * substitution. Right now, the class does not cache anything between different
85 * calls to `eval` but this might change in the future.
91 * Evaluates node `n` under the substitution described by the variable names
92 * `args` and the corresponding values `vals`. This method uses evaluation
93 * for subterms that evaluate to constants supported in the EvalResult
94 * class and substitution with rewriting for the others.
96 * The nodes in vals are typically intended to be constant, although this
99 * If the parameter useRewriter is true, then we may invoke calls to the
100 * rewriter for computing the result of this method.
102 * The result of this call is either equivalent to:
103 * (1) Rewriter::rewrite(n.substitute(args,vars))
105 * If useRewriter is true, then we are always in the first case. If
106 * useRewriter is false, then we may be in case (2) if computing the
107 * rewritten, substituted form of n could not be determined by evaluation.
110 const std::vector
<Node
>& args
,
111 const std::vector
<Node
>& vals
,
112 bool useRewriter
= true) const;
114 * Same as above, but with a precomputed visited map.
117 const std::vector
<Node
>& args
,
118 const std::vector
<Node
>& vals
,
119 const std::unordered_map
<Node
, Node
, NodeHashFunction
>& visited
,
120 bool useRewriter
= true) const;
124 * Evaluates node `n` under the substitution described by the variable names
125 * `args` and the corresponding values `vals`. The internal version returns
126 * an EvalResult which has slightly less overhead for recursive calls.
128 * The method returns an invalid EvalResult if the result of the substitution
129 * on n does not result in a constant value that is one of those supported in
130 * the EvalResult class. Notice that e.g. datatype constants are not supported
133 * This method additionally adds subterms of n that could not be evaluated
134 * (in the above sense) to the map evalAsNode. For each such subterm n', we
135 * store the node corresponding to the result of applying the substitution
136 * `args` to `vals` and rewriting. Notice that this map contains an entry
137 * for n in the case that it cannot be evaluated.
139 EvalResult
evalInternal(
141 const std::vector
<Node
>& args
,
142 const std::vector
<Node
>& vals
,
143 std::unordered_map
<TNode
, Node
, NodeHashFunction
>& evalAsNode
,
144 std::unordered_map
<TNode
, EvalResult
, TNodeHashFunction
>& results
,
145 bool useRewriter
) const;
148 * This function reconstructs the result of evaluating n using a combination
149 * of evaluation results (eresults) and substitution+rewriting (evalAsNode).
151 * Arguments eresults and evalAsNode are built within the context of the
152 * above method for some args and vals. This method ensures that the return
153 * value is equivalent to the rewritten form of n * { args -> vals }.
157 std::unordered_map
<TNode
, EvalResult
, TNodeHashFunction
>& eresults
,
158 std::unordered_map
<TNode
, Node
, NodeHashFunction
>& evalAsNode
) const;
161 } // namespace theory
164 #endif /* CVC4__THEORY__EVALUATOR_H */