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`. The function returns a null
89 * node if there is a subterm that is not constant under the substitution or
90 * if an operator is not supported by the evaluator.
93 const std::vector
<Node
>& args
,
94 const std::vector
<Node
>& vals
);
98 * Evaluates node `n` under the substitution described by the variable names
99 * `args` and the corresponding values `vals`. The internal version returns
100 * an EvalResult which has slightly less overhead for recursive calls. The
101 * function returns an invalid result if there is a subterm that is not
102 * constant under the substitution or if an operator is not supported by the
105 EvalResult
evalInternal(TNode n
,
106 const std::vector
<Node
>& args
,
107 const std::vector
<Node
>& vals
);
110 } // namespace theory
113 #endif /* __CVC4__THEORY__EVALUATOR_H */