1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * Representation of bound variables in codatatype values
16 #include "cvc5_public.h"
18 #ifndef CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H
19 #define CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H
24 #include "util/integer.h"
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:
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:
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
48 * (cons 0 (cons 1 @cbv_0))
49 * on the other hand represents the lasso:
50 * (cons 0 (cons 1 (cons 1 (cons 1 ... ))))
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.
58 class CodatatypeBoundVariable
61 CodatatypeBoundVariable(const TypeNode
& type
, Integer index
);
62 ~CodatatypeBoundVariable();
64 CodatatypeBoundVariable(const CodatatypeBoundVariable
& other
);
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;
76 std::unique_ptr
<TypeNode
> d_type
;
77 const Integer d_index
;
79 std::ostream
& operator<<(std::ostream
& out
, const CodatatypeBoundVariable
& cbv
);
82 * Hash function for codatatype bound variables.
84 struct CodatatypeBoundVariableHashFunction
86 size_t operator()(const CodatatypeBoundVariable
& cbv
) const;
91 #endif /* CVC5__UNINTERPRETED_CONSTANT_H */