src/expr/codatatype_bound_variable.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * Representation of bound variables in codatatype values
  14  */
  15
  16 #include "cvc5_public.h"
  17
  18 #ifndef CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H
  19 #define CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H
  20
  21 #include <iosfwd>
  22 #include <memory>
  23
  24 #include "util/integer.h"
  25
  26 namespace cvc5 {
  27
  28 class TypeNode;
  29
  30 /**
  31  * In theory, codatatype values are represented in using a MU-notation form,
  32  * where recursive values may contain free constants indexed by their de Bruijn
  33  * indices. This is sometimes written:
  34  *    MU x. (cons 0 x).
  35  * where the MU binder is label for a term position, which x references.
  36  * Instead of constructing an explicit MU binder (which is problematic for
  37  * canonicity), we use de Bruijn indices for representing bound variables,
  38  * whose index indicates the level in which it is nested. For example, we
  39  * represent the above value as:
  40  *    (cons 0 @cbv_0)
  41  * In the above value, @cbv_0 is a pointer to its direct parent, so the above
  42  * value represents the infinite list (cons 0 (cons 0 (cons 0 ... ))).
  43  * Another example, the value:
  44  *    (cons 0 (cons 1 @cbv_1))
  45  * @cbv_1 is pointer to the top most node of this value, so this is value
  46  * represents the infinite list (cons 0 (cons 1 (cons 0 (cons 1 ...)))). The
  47  * value:
  48  *    (cons 0 (cons 1 @cbv_0))
  49  * on the other hand represents the lasso:
  50  *    (cons 0 (cons 1 (cons 1 (cons 1 ... ))))
  51  *
  52  * This class is used for representing the indexed bound variables in the above
  53  * values. It is considered a constant (isConst is true). However, constants
  54  * of codatatype type are normalized by the rewriter (see datatypes rewriter
  55  * normalizeCodatatypeConstant) to ensure their canonicity, via a variant
  56  * of Hopcroft's algorithm.
  57  */
  58 class CodatatypeBoundVariable
  59 {
  60  public:
  61   CodatatypeBoundVariable(const TypeNode& type, Integer index);
  62   ~CodatatypeBoundVariable();
  63
  64   CodatatypeBoundVariable(const CodatatypeBoundVariable& other);
  65
  66   const TypeNode& getType() const;
  67   const Integer& getIndex() const;
  68   bool operator==(const CodatatypeBoundVariable& cbv) const;
  69   bool operator!=(const CodatatypeBoundVariable& cbv) const;
  70   bool operator<(const CodatatypeBoundVariable& cbv) const;
  71   bool operator<=(const CodatatypeBoundVariable& cbv) const;
  72   bool operator>(const CodatatypeBoundVariable& cbv) const;
  73   bool operator>=(const CodatatypeBoundVariable& cbv) const;
  74
  75  private:
  76   std::unique_ptr<TypeNode> d_type;
  77   const Integer d_index;
  78 };
  79 std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv);
  80
  81 /**
  82  * Hash function for codatatype bound variables.
  83  */
  84 struct CodatatypeBoundVariableHashFunction
  85 {
  86   size_t operator()(const CodatatypeBoundVariable& cbv) const;
  87 };
  88
  89 }  // namespace cvc5
  90
  91 #endif /* CVC5__UNINTERPRETED_CONSTANT_H */