Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of term canonize.
11 : : */
12 : :
13 : : #include "expr/term_canonize.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : // TODO #1216: move the code in this include
18 : : #include "theory/quantifiers/term_util.h"
19 : :
20 : : using namespace cvc5::internal::kind;
21 : :
22 : : namespace cvc5::internal {
23 : : namespace expr {
24 : :
25 : 119612 : TermCanonize::TermCanonize(TypeClassCallback* tcc)
26 : 119612 : : d_tcc(tcc), d_op_id_count(0), d_typ_id_count(0)
27 : : {
28 : 119612 : }
29 : :
30 : 523094 : int TermCanonize::getIdForOperator(Node op)
31 : : {
32 : 523094 : std::map<Node, int>::iterator it = d_op_id.find(op);
33 [ + + ]: 523094 : if (it == d_op_id.end())
34 : : {
35 : 49271 : d_op_id[op] = d_op_id_count;
36 : 49271 : d_op_id_count++;
37 : 49271 : return d_op_id[op];
38 : : }
39 : 473823 : return it->second;
40 : : }
41 : :
42 : 71848 : int TermCanonize::getIdForType(TypeNode t)
43 : : {
44 : 71848 : std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
45 [ + + ]: 71848 : if (it == d_typ_id.end())
46 : : {
47 : 5210 : d_typ_id[t] = d_typ_id_count;
48 : 5210 : d_typ_id_count++;
49 : 5210 : return d_typ_id[t];
50 : : }
51 : 66638 : return it->second;
52 : : }
53 : :
54 : 858312 : bool TermCanonize::getTermOrder(Node a, Node b)
55 : : {
56 [ + + ]: 858312 : if (a.getKind() == Kind::BOUND_VARIABLE)
57 : : {
58 [ + + ]: 115498 : if (b.getKind() == Kind::BOUND_VARIABLE)
59 : : {
60 : : // just use builtin node comparison
61 : 80873 : return a < b;
62 : : }
63 : 34625 : return true;
64 : : }
65 [ + + ]: 742814 : if (b.getKind() != Kind::BOUND_VARIABLE)
66 : : {
67 [ + + ]: 661280 : Node aop = a.hasOperator() ? a.getOperator() : a;
68 [ + + ]: 661280 : Node bop = b.hasOperator() ? b.getOperator() : b;
69 [ + - ]: 661280 : Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
70 [ + - ]: 661280 : Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
71 [ + + ]: 661280 : if (aop == bop)
72 : : {
73 [ + + ]: 399733 : if (a.getNumChildren() == b.getNumChildren())
74 : : {
75 [ + + ]: 535303 : for (size_t i = 0, size = a.getNumChildren(); i < size; i++)
76 : : {
77 [ + + ]: 534965 : if (a[i] != b[i])
78 : : {
79 : : // first distinct child determines the ordering
80 : 391112 : return getTermOrder(a[i], b[i]);
81 : : }
82 : : }
83 : : }
84 : : else
85 : : {
86 : 8283 : return a.getNumChildren() < b.getNumChildren();
87 : : }
88 : : }
89 : : else
90 : : {
91 : 261547 : return getIdForOperator(aop) < getIdForOperator(bop);
92 : : }
93 [ + + ][ + + ]: 1322222 : }
94 : 81872 : return false;
95 : : }
96 : :
97 : 9104267 : Node TermCanonize::getCanonicalFreeVar(TypeNode tn, size_t i, uint32_t tc)
98 : : {
99 [ - + ][ - + ]: 9104267 : Assert(!tn.isNull());
[ - - ]
100 : 9104267 : std::pair<TypeNode, uint32_t> key(tn, tc);
101 : 9104267 : std::vector<Node>& tvars = d_cn_free_var[key];
102 [ + + ]: 9467054 : while (tvars.size() <= i)
103 : : {
104 : 362787 : std::stringstream os;
105 [ + + ]: 362787 : if (tn.isFunction())
106 : : {
107 : 1622 : os << "f" << i;
108 : : }
109 : : else
110 : : {
111 : 361165 : std::stringstream oss;
112 : 361165 : oss << tn;
113 : 361165 : std::string typ_name = oss.str();
114 [ + + ]: 446030 : while (typ_name[0] == '(')
115 : : {
116 : 84865 : typ_name.erase(typ_name.begin());
117 : : }
118 : 361165 : os << typ_name[0] << i;
119 : 361165 : }
120 : 725574 : Node x = NodeManager::mkBoundVar(os.str().c_str(), tn);
121 : 362787 : d_fvIndex[x] = tvars.size();
122 : 362787 : tvars.push_back(x);
123 : 362787 : }
124 : 18208534 : return tvars[i];
125 : 9104267 : }
126 : :
127 : 8799388 : uint32_t TermCanonize::getTypeClass(TNode v)
128 : : {
129 [ + + ][ + + ]: 8799388 : return d_tcc == nullptr ? 0 : d_tcc->getTypeClass(v);
[ - - ]
130 : : }
131 : :
132 : 0 : size_t TermCanonize::getIndexForFreeVariable(Node v) const
133 : : {
134 : 0 : std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
135 [ - - ]: 0 : if (it == d_fvIndex.end())
136 : : {
137 : 0 : return 0;
138 : : }
139 : 0 : return it->second;
140 : : }
141 : :
142 : : struct sortTermOrder
143 : : {
144 : : TermCanonize* d_tu;
145 : 467200 : bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
146 : : };
147 : :
148 : 50180913 : Node TermCanonize::getCanonicalTerm(
149 : : TNode n,
150 : : bool apply_torder,
151 : : bool doHoVar,
152 : : std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
153 : : std::map<TNode, Node>& visited)
154 : : {
155 : 50180913 : std::map<TNode, Node>::iterator it = visited.find(n);
156 [ + + ]: 50180913 : if (it != visited.end())
157 : : {
158 : 12500108 : return it->second;
159 : : }
160 : :
161 [ + - ]: 37680805 : Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
162 [ + + ]: 37680805 : if (n.getKind() == Kind::BOUND_VARIABLE)
163 : : {
164 : 8799388 : uint32_t tc = getTypeClass(n);
165 : 8799388 : TypeNode tn = n.getType();
166 : 8799388 : std::pair<TypeNode, uint32_t> key(tn, tc);
167 : : // allocate variable
168 : 8799388 : unsigned vn = var_count[key];
169 : 8799388 : var_count[key]++;
170 : 8799388 : Node fv = getCanonicalFreeVar(tn, vn, tc);
171 : 8799388 : visited[n] = fv;
172 [ + - ]: 8799388 : Trace("canon-term-debug") << "...allocate variable " << fv << std::endl;
173 : 8799388 : return fv;
174 : 8799388 : }
175 [ + + ]: 28881417 : else if (n.getNumChildren() > 0)
176 : : {
177 : : // collect children
178 [ + - ]: 23569617 : Trace("canon-term-debug") << "Collect children" << std::endl;
179 : 23569617 : std::vector<Node> cchildren;
180 [ + + ]: 70506347 : for (const Node& cn : n)
181 : : {
182 : 46936730 : cchildren.push_back(cn);
183 : 46936730 : }
184 : : // if applicable, first sort by term order
185 [ + + ][ + + ]: 23569617 : if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
[ + + ]
186 : : {
187 [ + - ]: 384666 : Trace("canon-term-debug")
188 : 192333 : << "Sort based on commutative operator " << n.getKind() << std::endl;
189 : : sortTermOrder sto;
190 : 192333 : sto.d_tu = this;
191 : 192333 : std::sort(cchildren.begin(), cchildren.end(), sto);
192 : : }
193 : : // now make canonical
194 [ + - ]: 23569617 : Trace("canon-term-debug") << "Make canonical children" << std::endl;
195 [ + + ]: 70506347 : for (unsigned i = 0, size = cchildren.size(); i < size; i++)
196 : : {
197 : 93873460 : cchildren[i] = getCanonicalTerm(
198 : 93873460 : cchildren[i], apply_torder, doHoVar, var_count, visited);
199 : : }
200 [ + + ]: 23569617 : if (n.getMetaKind() == metakind::PARAMETERIZED)
201 : : {
202 : 1217074 : Node op = n.getOperator();
203 [ + + ]: 1217074 : if (doHoVar)
204 : : {
205 : 234056 : op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
206 : : }
207 [ + - ]: 1217074 : Trace("canon-term-debug") << "Insert operator " << op << std::endl;
208 : 1217074 : cchildren.insert(cchildren.begin(), op);
209 : 1217074 : }
210 [ + - ]: 47139234 : Trace("canon-term-debug")
211 : 23569617 : << "...constructing for " << n << "." << std::endl;
212 : 23569617 : Node ret = n.getNodeManager()->mkNode(n.getKind(), cchildren);
213 [ + - ]: 47139234 : Trace("canon-term-debug")
214 : 23569617 : << "...constructed " << ret << " for " << n << "." << std::endl;
215 : 23569617 : visited[n] = ret;
216 : 23569617 : return ret;
217 : 23569617 : }
218 [ + - ]: 5311800 : Trace("canon-term-debug") << "...return 0-child term." << std::endl;
219 : 5311800 : return n;
220 : : }
221 : :
222 : 2976831 : Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
223 : : {
224 : 2976831 : std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
225 : 2976831 : std::map<TNode, Node> visited;
226 : 5953662 : return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
227 : 2976831 : }
228 : :
229 : 33296 : Node TermCanonize::getCanonicalTerm(TNode n,
230 : : std::map<TNode, Node>& visited,
231 : : bool apply_torder,
232 : : bool doHoVar)
233 : : {
234 : 33296 : std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
235 : 66592 : return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
236 : 33296 : }
237 : :
238 : : } // namespace expr
239 : : } // namespace cvc5::internal
|
