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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 toplevel 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 noncodatatype 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 mubinders with fresh variables. 
71 

* In detail, muterms 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 munotation 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 mubinders in n are replaced by a new 
87 

* variable. If n contains any subterm that is a reference to a mubinder 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 mubinders 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 mubinder. 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 precomputed 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 */ 