1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
/********************* */
/*! \file evaluator.h
** \verbatim
** Top contributors (to current version):
** Andres Noetzli, Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The Evaluator class
**
** The Evaluator class can be used to evaluate terms with constant leaves
** quickly, without going through the rewriter.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__EVALUATOR_H
#define CVC4__THEORY__EVALUATOR_H
#include <utility>
#include <vector>
#include "base/output.h"
#include "expr/node.h"
#include "util/bitvector.h"
#include "util/rational.h"
#include "util/string.h"
namespace CVC4 {
namespace theory {
/**
* Struct that holds the result of an evaluation. The actual value is stored in
* a union to avoid the overhead of a class hierarchy with virtual methods.
*/
struct EvalResult
{
/* Describes which type of result is being stored */
enum
{
BOOL,
BITVECTOR,
RATIONAL,
STRING,
INVALID
} d_tag;
/* Stores the actual result */
union
{
bool d_bool;
BitVector d_bv;
Rational d_rat;
String d_str;
};
EvalResult(const EvalResult& other);
EvalResult() : d_tag(INVALID) {}
EvalResult(bool b) : d_tag(BOOL), d_bool(b) {}
EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
EvalResult& operator=(const EvalResult& other);
~EvalResult();
/**
* Converts the result to a Node. If the result is not valid, this function
* returns the null node.
*/
Node toNode() const;
};
/**
* The class that performs the actual evaluation of a term under a
* substitution. Right now, the class does not cache anything between different
* calls to `eval` but this might change in the future.
*/
class Evaluator
{
public:
/**
* Evaluates node `n` under the substitution described by the variable names
* `args` and the corresponding values `vals`. This method uses evaluation
* for subterms that evaluate to constants supported in the EvalResult
* class and substitution with rewriting for the others.
*
* The nodes in vals are typically intended to be constant, although this
* is not required.
*
* If the parameter useRewriter is true, then we may invoke calls to the
* rewriter for computing the result of this method.
*
* The result of this call is either equivalent to:
* (1) Rewriter::rewrite(n.substitute(args,vars))
* (2) Node::null().
* If useRewriter is true, then we are always in the first case. If
* useRewriter is false, then we may be in case (2) if computing the
* rewritten, substituted form of n could not be determined by evaluation.
*/
Node eval(TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
bool useRewriter = true) const;
/**
* Same as above, but with a precomputed visited map.
*/
Node eval(TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
const std::unordered_map<Node, Node, NodeHashFunction>& visited,
bool useRewriter = true) const;
private:
/**
* Evaluates node `n` under the substitution described by the variable names
* `args` and the corresponding values `vals`. The internal version returns
* an EvalResult which has slightly less overhead for recursive calls.
*
* The method returns an invalid EvalResult if the result of the substitution
* on n does not result in a constant value that is one of those supported in
* the EvalResult class. Notice that e.g. datatype constants are not supported
* in this class.
*
* This method additionally adds subterms of n that could not be evaluated
* (in the above sense) to the map evalAsNode. For each such subterm n', we
* store the node corresponding to the result of applying the substitution
* `args` to `vals` and rewriting. Notice that this map contains an entry
* for n in the case that it cannot be evaluated.
*/
EvalResult evalInternal(
TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode,
std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results,
bool useRewriter) const;
/** reconstruct
*
* This function reconstructs the result of evaluating n using a combination
* of evaluation results (eresults) and substitution+rewriting (evalAsNode).
*
* Arguments eresults and evalAsNode are built within the context of the
* above method for some args and vals. This method ensures that the return
* value is equivalent to the rewritten form of n * { args -> vals }.
*/
Node reconstruct(
TNode n,
std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const;
};
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__EVALUATOR_H */
|
