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 : 120379 : TermCanonize::TermCanonize(TypeClassCallback* tcc)
26 : 120379 : : d_tcc(tcc), d_op_id_count(0), d_typ_id_count(0)
27 : : {
28 : 120379 : }
29 : :
30 : 539832 : int TermCanonize::getIdForOperator(Node op)
31 : : {
32 : 539832 : std::map<Node, int>::iterator it = d_op_id.find(op);
33 [ + + ]: 539832 : if (it == d_op_id.end())
34 : : {
35 : 49950 : d_op_id[op] = d_op_id_count;
36 : 49950 : d_op_id_count++;
37 : 49950 : return d_op_id[op];
38 : : }
39 : 489882 : return it->second;
40 : : }
41 : :
42 : 71930 : int TermCanonize::getIdForType(TypeNode t)
43 : : {
44 : 71930 : std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
45 [ + + ]: 71930 : if (it == d_typ_id.end())
46 : : {
47 : 5349 : d_typ_id[t] = d_typ_id_count;
48 : 5349 : d_typ_id_count++;
49 : 5349 : return d_typ_id[t];
50 : : }
51 : 66581 : return it->second;
52 : : }
53 : :
54 : 869391 : bool TermCanonize::getTermOrder(Node a, Node b)
55 : : {
56 [ + + ]: 869391 : if (a.getKind() == Kind::BOUND_VARIABLE)
57 : : {
58 [ + + ]: 113950 : if (b.getKind() == Kind::BOUND_VARIABLE)
59 : : {
60 : : // just use builtin node comparison
61 : 78037 : return a < b;
62 : : }
63 : 35913 : return true;
64 : : }
65 [ + + ]: 755441 : if (b.getKind() != Kind::BOUND_VARIABLE)
66 : : {
67 [ + + ]: 672827 : Node aop = a.hasOperator() ? a.getOperator() : a;
68 [ + + ]: 672827 : Node bop = b.hasOperator() ? b.getOperator() : b;
69 [ + - ]: 672827 : Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
70 [ + - ]: 672827 : Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
71 [ + + ]: 672827 : if (aop == bop)
72 : : {
73 [ + + ]: 402911 : if (a.getNumChildren() == b.getNumChildren())
74 : : {
75 [ + + ]: 537125 : for (size_t i = 0, size = a.getNumChildren(); i < size; i++)
76 : : {
77 [ + + ]: 536787 : if (a[i] != b[i])
78 : : {
79 : : // first distinct child determines the ordering
80 : 393154 : return getTermOrder(a[i], b[i]);
81 : : }
82 : : }
83 : : }
84 : : else
85 : : {
86 : 9419 : return a.getNumChildren() < b.getNumChildren();
87 : : }
88 : : }
89 : : else
90 : : {
91 : 269916 : return getIdForOperator(aop) < getIdForOperator(bop);
92 : : }
93 [ + + ][ + + ]: 1345316 : }
94 : 82952 : return false;
95 : : }
96 : :
97 : 9195303 : Node TermCanonize::getCanonicalFreeVar(TypeNode tn, size_t i, uint32_t tc)
98 : : {
99 [ - + ][ - + ]: 9195303 : Assert(!tn.isNull());
[ - - ]
100 : 9195303 : std::pair<TypeNode, uint32_t> key(tn, tc);
101 : 9195303 : std::vector<Node>& tvars = d_cn_free_var[key];
102 [ + + ]: 9569490 : while (tvars.size() <= i)
103 : : {
104 : 374187 : std::stringstream os;
105 [ + + ]: 374187 : if (tn.isFunction())
106 : : {
107 : 1733 : os << "f" << i;
108 : : }
109 : : else
110 : : {
111 : 372454 : std::stringstream oss;
112 : 372454 : oss << tn;
113 : 372454 : std::string typ_name = oss.str();
114 [ + + ]: 460080 : while (typ_name[0] == '(')
115 : : {
116 : 87626 : typ_name.erase(typ_name.begin());
117 : : }
118 : 372454 : os << typ_name[0] << i;
119 : 372454 : }
120 : 748374 : Node x = NodeManager::mkBoundVar(os.str().c_str(), tn);
121 : 374187 : d_fvIndex[x] = tvars.size();
122 : 374187 : tvars.push_back(x);
123 : 374187 : }
124 : 18390606 : return tvars[i];
125 : 9195303 : }
126 : :
127 : 9094189 : uint32_t TermCanonize::getTypeClass(TNode v)
128 : : {
129 [ + + ][ + + ]: 9094189 : 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 : 476237 : bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
146 : : };
147 : :
148 : 51851976 : 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 : 51851976 : std::map<TNode, Node>::iterator it = visited.find(n);
156 [ + + ]: 51851976 : if (it != visited.end())
157 : : {
158 : 12918622 : return it->second;
159 : : }
160 : :
161 [ + - ]: 38933354 : Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
162 [ + + ]: 38933354 : if (n.getKind() == Kind::BOUND_VARIABLE)
163 : : {
164 : 9094189 : uint32_t tc = getTypeClass(n);
165 : 9094189 : TypeNode tn = n.getType();
166 : 9094189 : std::pair<TypeNode, uint32_t> key(tn, tc);
167 : : // allocate variable
168 : 9094189 : unsigned vn = var_count[key];
169 : 9094189 : var_count[key]++;
170 : 9094189 : Node fv = getCanonicalFreeVar(tn, vn, tc);
171 : 9094189 : visited[n] = fv;
172 [ + - ]: 9094189 : Trace("canon-term-debug") << "...allocate variable " << fv << std::endl;
173 : 9094189 : return fv;
174 : 9094189 : }
175 [ + + ]: 29839165 : else if (n.getNumChildren() > 0)
176 : : {
177 : : // collect children
178 [ + - ]: 24358926 : Trace("canon-term-debug") << "Collect children" << std::endl;
179 : 24358926 : std::vector<Node> cchildren;
180 [ + + ]: 72870021 : for (const Node& cn : n)
181 : : {
182 : 48511095 : cchildren.push_back(cn);
183 : 48511095 : }
184 : : // if applicable, first sort by term order
185 [ + + ][ + + ]: 24358926 : if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
[ + + ]
186 : : {
187 [ + - ]: 393620 : Trace("canon-term-debug")
188 : 196810 : << "Sort based on commutative operator " << n.getKind() << std::endl;
189 : : sortTermOrder sto;
190 : 196810 : sto.d_tu = this;
191 : 196810 : std::sort(cchildren.begin(), cchildren.end(), sto);
192 : : }
193 : : // now make canonical
194 [ + - ]: 24358926 : Trace("canon-term-debug") << "Make canonical children" << std::endl;
195 [ + + ]: 72870021 : for (unsigned i = 0, size = cchildren.size(); i < size; i++)
196 : : {
197 : 97022190 : cchildren[i] = getCanonicalTerm(
198 : 97022190 : cchildren[i], apply_torder, doHoVar, var_count, visited);
199 : : }
200 [ + + ]: 24358926 : if (n.getMetaKind() == metakind::PARAMETERIZED)
201 : : {
202 : 1247501 : Node op = n.getOperator();
203 [ + + ]: 1247501 : if (doHoVar)
204 : : {
205 : 230757 : op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
206 : : }
207 [ + - ]: 1247501 : Trace("canon-term-debug") << "Insert operator " << op << std::endl;
208 : 1247501 : cchildren.insert(cchildren.begin(), op);
209 : 1247501 : }
210 [ + - ]: 48717852 : Trace("canon-term-debug")
211 : 24358926 : << "...constructing for " << n << "." << std::endl;
212 : 24358926 : Node ret = n.getNodeManager()->mkNode(n.getKind(), cchildren);
213 [ + - ]: 48717852 : Trace("canon-term-debug")
214 : 24358926 : << "...constructed " << ret << " for " << n << "." << std::endl;
215 : 24358926 : visited[n] = ret;
216 : 24358926 : return ret;
217 : 24358926 : }
218 [ + - ]: 5480239 : Trace("canon-term-debug") << "...return 0-child term." << std::endl;
219 : 5480239 : return n;
220 : : }
221 : :
222 : 3077077 : Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
223 : : {
224 : 3077077 : std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
225 : 3077077 : std::map<TNode, Node> visited;
226 : 6154154 : return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
227 : 3077077 : }
228 : :
229 : 33047 : Node TermCanonize::getCanonicalTerm(TNode n,
230 : : std::map<TNode, Node>& visited,
231 : : bool apply_torder,
232 : : bool doHoVar)
233 : : {
234 : 33047 : std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
235 : 66094 : return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
236 : 33047 : }
237 : :
238 : : } // namespace expr
239 : : } // namespace cvc5::internal
|
