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-2018 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`. 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.
  91    */
  92   Node eval(TNode n,
  93             const std::vector<Node>& args,
  94             const std::vector<Node>& vals);
  95
  96  private:
  97   /**
  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
 103    * evaluator.
 104    */
 105   EvalResult evalInternal(TNode n,
 106                           const std::vector<Node>& args,
 107                           const std::vector<Node>& vals);
 108 };
 109
 110 }  // namespace theory
 111 }  // namespace CVC4
 112
 113 #endif /* __CVC4__THEORY__EVALUATOR_H */