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