src/theory/evaluator.h

   1 /*********************                                                        */
   2 /*! \file evaluator.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli
   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
  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 "util/bitvector.h"
  29 #include "util/rational.h"
  30 #include "util/regexp.h"
  31
  32 namespace CVC4 {
  33 namespace theory {
  34
  35 /**
  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.
  38  */
  39 struct EvalResult
  40 {
  41   /* Describes which type of result is being stored */
  42   enum
  43   {
  44     BOOL,
  45     BITVECTOR,
  46     RATIONAL,
  47     STRING,
  48     INVALID
  49   } d_tag;
  50
  51   /* Stores the actual result */
  52   union
  53   {
  54     bool d_bool;
  55     BitVector d_bv;
  56     Rational d_rat;
  57     String d_str;
  58   };
  59
  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) {}
  66
  67   EvalResult& operator=(const EvalResult& other);
  68
  69   ~EvalResult();
  70
  71   /**
  72    * Converts the result to a Node. If the result is not valid, this function
  73    * returns the null node.
  74    */
  75   Node toNode() const;
  76 };
  77
  78 /**
  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.
  82  */
  83 class Evaluator
  84 {
  85  public:
  86   /**
  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.
  91    *
  92    * The nodes in the vals must be constant values, that is, they must return
  93    * true for isConst().
  94    */
  95   Node eval(TNode n,
  96             const std::vector<Node>& args,
  97             const std::vector<Node>& vals) const;
  98   /**
  99    * Same as above, but with a precomputed visited map.
 100    */
 101   Node eval(
 102       TNode n,
 103       const std::vector<Node>& args,
 104       const std::vector<Node>& vals,
 105       const std::unordered_map<Node, Node, NodeHashFunction>& visited) const;
 106
 107  private:
 108   /**
 109    * Evaluates node `n` under the substitution described by the variable names
 110    * `args` and the corresponding values `vals`. The internal version returns
 111    * an EvalResult which has slightly less overhead for recursive calls.
 112    *
 113    * The method returns an invalid EvalResult if the result of the substitution
 114    * on n does not result in a constant value that is one of those supported in
 115    * the EvalResult class. Notice that e.g. datatype constants are not supported
 116    * in this class.
 117    *
 118    * This method additionally adds subterms of n that could not be evaluated
 119    * (in the above sense) to the map evalAsNode. For each such subterm n', we
 120    * store the node corresponding to the result of applying the substitution
 121    * `args` to `vals` and rewriting. Notice that this map contains an entry
 122    * for n in the case that it cannot be evaluated.
 123    */
 124   EvalResult evalInternal(
 125       TNode n,
 126       const std::vector<Node>& args,
 127       const std::vector<Node>& vals,
 128       std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode,
 129       std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results) const;
 130   /** reconstruct
 131    *
 132    * This function reconstructs the result of evaluating n using a combination
 133    * of evaluation results (eresults) and substitution+rewriting (evalAsNode).
 134    *
 135    * Arguments eresults and evalAsNode are built within the context of the
 136    * above method for some args and vals. This method ensures that the return
 137    * value is equivalent to the rewritten form of n * { args -> vals }.
 138    */
 139   Node reconstruct(
 140       TNode n,
 141       std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
 142       std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const;
 143 };
 144
 145 }  // namespace theory
 146 }  // namespace CVC4
 147
 148 #endif /* CVC4__THEORY__EVALUATOR_H */