GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/datatypes_rewriter.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 7 20 35.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file datatypes_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Mathias Preiner
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 Rewriter for the theory of (co)inductive datatypes
13
 **
14
 ** Rewriter for the theory of (co)inductive datatypes.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
20
#define CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
21
22
#include "theory/theory_rewriter.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace datatypes {
27
28
469327
class DatatypesRewriter : public TheoryRewriter
29
{
30
 public:
31
  RewriteResponse postRewrite(TNode in) override;
32
  RewriteResponse preRewrite(TNode in) override;
33
34
  /** normalize codatatype constant
35
   *
36
   * This returns the normal form of the codatatype constant n. This runs a
37
   * DFA minimization algorithm based on the private functions below.
38
   *
39
   * In particular, we first call collectRefs to setup initial information
40
   * about what terms occur in n. Then, we run a DFA minimization algorithm to
41
   * partition these subterms in equivalence classes. Finally, we call
42
   * normalizeCodatatypeConstantEqc to construct the normalized codatatype
43
   * constant that is equivalent to n.
44
   */
45
  static Node normalizeCodatatypeConstant(Node n);
46
  /** normalize constant
47
   *
48
   * This method returns the normal form of n, which calls the above function
49
   * on all top-level codatatype subterms of n.
50
   */
51
  static Node normalizeConstant(Node n);
52
53
 private:
54
  /** rewrite constructor term in */
55
  static RewriteResponse rewriteConstructor(TNode in);
56
  /** rewrite selector term in */
57
  static RewriteResponse rewriteSelector(TNode in);
58
  /** rewrite tester term in */
59
  static RewriteResponse rewriteTester(TNode in);
60
61
  /** collect references
62
   *
63
   * This function, given as input a codatatype term n, collects the necessary
64
   * information for constructing a (canonical) codatatype constant that is
65
   * equivalent to n if one exists, or null otherwise.
66
   *
67
   * In particular it returns a term ret such that all non-codatatype datatype
68
   * subterms of n are replaced by a constant that is equal to them via a
69
   * (mutually) recursive call to normalizeConstant above. Additionally, this
70
   * function replaces references to mu-binders with fresh variables.
71
   * In detail, mu-terms are represented by uninterpreted constants of datatype
72
   * type that carry their Debruijn index.
73
   *
74
   * Consider the example of a codatatype representing a stream of integers:
75
   *   Stream := cons( head : Int, tail : Stream )
76
   * The stream 1,0,1,0,1,0... when written in mu-notation is the term:
77
   *   mu x. cons( 1, mu y. cons( 0, x ) )
78
   * This is represented in CVC4 by the Node:
79
   *   cons( 1, cons( 0, c[1] ) )
80
   * where c[1] is a uninterpreted constant datatype with Debruijn index 1,
81
   * indicating that c[1] is nested underneath 1 level on the path to the
82
   * term which it binds. On the other hand, the stream 1,0,0,0,0,... is
83
   * represented by the codatatype term:
84
   *   cons( 1, cons( 0, c[0] ) )
85
   *
86
   * Subterms that are references to mu-binders in n are replaced by a new
87
   * variable. If n contains any subterm that is a reference to a mu-binder not
88
   * bound in n, then we return null. For example we return null when n is:
89
   *   cons( 1, cons( 0, c[2] ) )
90
   * since c[2] is not bound by this codatatype term.
91
   *
92
   * All valid references to mu-binders are replaced by a variable that is
93
   * unique for the term it references. For example, for the infinite tree
94
   * codatatype: Tree : node( data : Int, left : Tree, right : Tree ) If n is
95
   * the term: node( 0, c[0], node( 1, c[0], c[1] ) ) then the return value ret
96
   * of this function is: node( 0, x, node( 1, y, x ) ) where x refers to the
97
   * root of the term and y refers to the right tree of the root.
98
   *
99
   * The argument sk stores the current set of node that we are traversing
100
   * beneath. The argument rf_pending stores, for each node that we are
101
   * traversing beneath either null or the free variable that we are using to
102
   * refer to its mu-binder. The remaining arguments store information that is
103
   * relevant when performing normalization of n using the value of ret:
104
   *
105
   * rf : maps subterms of n to the corresponding term in ret for all subterms
106
   * where the corresponding term in ret is different.
107
   * terms : stores all subterms of ret.
108
   * cdts : for each term t in terms, stores whether t is a codatatype.
109
   */
110
  static Node collectRef(Node n,
111
                         std::vector<Node>& sk,
112
                         std::map<Node, Node>& rf,
113
                         std::vector<Node>& rf_pending,
114
                         std::vector<Node>& terms,
115
                         std::map<Node, bool>& cdts);
116
  /** normalize codatatype constant eqc
117
   *
118
   * This recursive function returns a codatatype constant that is equivalent to
119
   * n based on a pre-computed partition of the subterms of n into equivalence
120
   * classes, as stored in the mapping eqc, which maps the subterms of n to
121
   * equivalence class ids. The arguments eqc_stack and depth store information
122
   * about the traversal in a term we have recursed, where
123
   *
124
   * eqc_stack : maps the depth of each term we have traversed to its
125
   * equivalence class id. depth : the number of levels which we have traversed.
126
   */
127
  static Node normalizeCodatatypeConstantEqc(Node n,
128
                                             std::map<int, int>& eqc_stack,
129
                                             std::map<Node, int>& eqc,
130
                                             int depth);
131
  /** replace debruijn
132
   *
133
   * This function, given codatatype term n, returns a node
134
   * where all subterms of n that have Debruijn indices that refer to a
135
   * term of input depth are replaced by orig. For example, for the infinite
136
   * Tree datatype, replaceDebruijn( node( 0, c[0], node( 1, c[0], c[1] ) ), t,
137
   * Tree, 0 ) returns node( 0, t, node( 1, c[0], t ) ).
138
   */
139
  static Node replaceDebruijn(Node n,
140
                              Node orig,
141
                              TypeNode orig_tn,
142
                              unsigned depth);
143
}; /* class DatatypesRewriter */
144
145
}/* CVC4::theory::datatypes namespace */
146
}/* CVC4::theory namespace */
147
}/* CVC4 namespace */
148
149
#endif /* CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */