1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 "util/bitvector.h"
29 #include "util/rational.h"
30 #include "util/regexp.h"
36 * Struct that holds the result of an evaluation. The actual value is stored in
37 * a union to avoid the overhead of a class hierarchy with virtual methods.
41 /* Describes which type of result is being stored */
51 /* Stores the actual result */
60 EvalResult(const EvalResult
& other
);
61 EvalResult() : d_tag(INVALID
) {}
62 EvalResult(bool b
) : d_tag(BOOL
), d_bool(b
) {}
63 EvalResult(const BitVector
& bv
) : d_tag(BITVECTOR
), d_bv(bv
) {}
64 EvalResult(const Rational
& i
) : d_tag(RATIONAL
), d_rat(i
) {}
65 EvalResult(const String
& str
) : d_tag(STRING
), d_str(str
) {}
67 EvalResult
& operator=(const EvalResult
& other
);
72 * Converts the result to a Node. If the result is not valid, this function
73 * returns the null node.
79 * The class that performs the actual evaluation of a term under a
80 * substitution. Right now, the class does not cache anything between different
81 * calls to `eval` but this might change in the future.
87 * Evaluates node `n` under the substitution described by the variable names
88 * `args` and the corresponding values `vals`. This method uses evaluation
89 * for subterms that evaluate to constants supported in the EvalResult
90 * class and substitution with rewriting for the others.
92 * The nodes in the vals must be constant values, that is, they must return
96 const std::vector
<Node
>& args
,
97 const std::vector
<Node
>& vals
);
101 * Evaluates node `n` under the substitution described by the variable names
102 * `args` and the corresponding values `vals`. The internal version returns
103 * an EvalResult which has slightly less overhead for recursive calls.
105 * The method returns an invalid EvalResult if the result of the substitution
106 * on n does not result in a constant value that is one of those supported in
107 * the EvalResult class. Notice that e.g. datatype constants are not supported
110 * This method additionally adds subterms of n that could not be evaluated
111 * (in the above sense) to the map evalAsNode. For each such subterm n', we
112 * store the node corresponding to the result of applying the substitution
113 * `args` to `vals` and rewriting. Notice that this map contains an entry
114 * for n in the case that it cannot be evaluated.
116 EvalResult
evalInternal(
118 const std::vector
<Node
>& args
,
119 const std::vector
<Node
>& vals
,
120 std::unordered_map
<TNode
, Node
, NodeHashFunction
>& evalAsNode
);
123 } // namespace theory
126 #endif /* CVC4__THEORY__EVALUATOR_H */