src/expr/term_context_node.h

   1 /*********************                                                        */
   2 /*! \file term_context_node.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Gereon Kremer
   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 Term context node utility.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__EXPR__TERM_CONTEXT_NODE_H
  18 #define CVC4__EXPR__TERM_CONTEXT_NODE_H
  19
  20 #include "expr/node.h"
  21
  22 namespace CVC4 {
  23
  24 class TCtxStack;
  25 class TermContext;
  26
  27 /**
  28  * A (term-context) sensitive term. This is a wrapper around a Node that
  29  * additionally has a term context identifier, see getTermContext(). It depends
  30  * on a pointer to a TermContext callback class (see term_context.h).
  31  */
  32 class TCtxNode
  33 {
  34   friend class TCtxStack;
  35
  36  public:
  37   TCtxNode(Node n, const TermContext* tctx);
  38   /** get number of children */
  39   size_t getNumChildren() const;
  40   /** get child at index i */
  41   TCtxNode getChild(size_t i) const;
  42   /** get node */
  43   Node getNode() const;
  44   /** get context */
  45   uint32_t getContextId() const;
  46   /** get term context */
  47   const TermContext* getTermContext() const;
  48   //---------------------- utility methods
  49   /**
  50    * Get node hash, which is a unique node representation of this TCtxNode.
  51    * This method calls the method below on the data members of this class.
  52    */
  53   Node getNodeHash() const;
  54   /**
  55    * Get node hash, which is a unique node representation of the pair (n, val).
  56    * In particular, this returns (SEXPR n (CONST_RATIONAL val)).
  57    */
  58   static Node computeNodeHash(Node n, uint32_t val);
  59   /**
  60    * Decompose node hash, which is an inverse of the above operation. In
  61    * particular, given input h, this returns a node n and sets val to a value
  62    * such that computeNodeHash(n, val) returns h.
  63    */
  64   static Node decomposeNodeHash(Node h, uint32_t& val);
  65   //---------------------- end utility methods
  66  private:
  67   /** private constructor */
  68   TCtxNode(Node n, uint32_t val, const TermContext* tctx);
  69   /** The node */
  70   Node d_node;
  71   /** The term context identifier */
  72   uint32_t d_val;
  73   /** The term context */
  74   const TermContext* d_tctx;
  75 };
  76
  77 }  // namespace CVC4
  78
  79 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */