src/theory/evaluator.h

   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-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
  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   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) {}
  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 */