GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/evaluator.h Lines: 5 6 83.3 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file evaluator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
11
 **
12
 ** \brief The Evaluator class
13
 **
14
 ** The Evaluator class can be used to evaluate terms with constant leaves
15
 ** quickly, without going through the rewriter.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__EVALUATOR_H
21
#define CVC4__THEORY__EVALUATOR_H
22
23
#include <utility>
24
#include <vector>
25
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"
32
33
namespace CVC4 {
34
namespace theory {
35
36
/**
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.
39
 */
40
struct EvalResult
41
{
42
  /* Describes which type of result is being stored */
43
  enum
44
  {
45
    BOOL,
46
    BITVECTOR,
47
    RATIONAL,
48
    STRING,
49
    UCONST,
50
    INVALID
51
  } d_tag;
52
53
  /* Stores the actual result */
54
  union
55
  {
56
    bool d_bool;
57
    BitVector d_bv;
58
    Rational d_rat;
59
    String d_str;
60
    UninterpretedConstant d_uc;
61
  };
62
63
  EvalResult(const EvalResult& other);
64
10365880
  EvalResult() : d_tag(INVALID) {}
65
4537622
  EvalResult(bool b) : d_tag(BOOL), d_bool(b) {}
66
2290206
  EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
67
1042177
  EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
68
331197
  EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
69
  EvalResult(const UninterpretedConstant& u) : d_tag(UCONST), d_uc(u) {}
70
71
  EvalResult& operator=(const EvalResult& other);
72
73
  ~EvalResult();
74
75
  /**
76
   * Converts the result to a Node. If the result is not valid, this function
77
   * returns the null node.
78
   */
79
  Node toNode() const;
80
};
81
82
/**
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.
86
 */
87
class Evaluator
88
{
89
 public:
90
  /**
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.
95
   *
96
   * The nodes in vals are typically intended to be constant, although this
97
   * is not required.
98
   *
99
   * If the parameter useRewriter is true, then we may invoke calls to the
100
   * rewriter for computing the result of this method.
101
   *
102
   * The result of this call is either equivalent to:
103
   * (1) Rewriter::rewrite(n.substitute(args,vars))
104
   * (2) Node::null().
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.
108
   */
109
  Node eval(TNode n,
110
            const std::vector<Node>& args,
111
            const std::vector<Node>& vals,
112
            bool useRewriter = true) const;
113
  /**
114
   * Same as above, but with a precomputed visited map.
115
   */
116
  Node eval(TNode n,
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;
121
122
 private:
123
  /**
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.
127
   *
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
131
   * in this class.
132
   *
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.
138
   */
139
  EvalResult evalInternal(
140
      TNode n,
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;
146
  /** reconstruct
147
   *
148
   * This function reconstructs the result of evaluating n using a combination
149
   * of evaluation results (eresults) and substitution+rewriting (evalAsNode).
150
   *
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 }.
154
   */
155
  Node reconstruct(
156
      TNode n,
157
      std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
158
      std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const;
159
};
160
161
}  // namespace theory
162
}  // namespace CVC4
163
164
#endif /* CVC4__THEORY__EVALUATOR_H */