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 : : #include "expr/bound_var_manager.h"
18 : : // TODO #1216: move the code in this include
19 : : #include "theory/quantifiers/term_util.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace expr {
25 : :
26 : 86417 : TermCanonize::TermCanonize(TypeClassCallback* tcc) : d_tcc(tcc) {}
27 : :
28 : 744897 : bool TermCanonize::getTermOrder(Node a, Node b)
29 : : {
30 [ + + ]: 744897 : if (a.getKind() == Kind::BOUND_VARIABLE)
31 : : {
32 [ + + ]: 110381 : if (b.getKind() == Kind::BOUND_VARIABLE)
33 : : {
34 : : // just use builtin node comparison
35 : 79571 : return a < b;
36 : : }
37 : 30810 : return true;
38 : : }
39 [ + + ]: 634516 : if (b.getKind() != Kind::BOUND_VARIABLE)
40 : : {
41 [ + + ]: 562638 : Node aop = a.hasOperator() ? a.getOperator() : a;
42 [ + + ]: 562638 : Node bop = b.hasOperator() ? b.getOperator() : b;
43 [ + - ]: 562638 : Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
44 [ + - ]: 562638 : Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
45 [ + + ]: 562638 : if (aop == bop)
46 : : {
47 [ + + ]: 345867 : if (a.getNumChildren() == b.getNumChildren())
48 : : {
49 [ + + ]: 463886 : for (size_t i = 0, size = a.getNumChildren(); i < size; i++)
50 : : {
51 [ + + ]: 463548 : if (a[i] != b[i])
52 : : {
53 : : // first distinct child determines the ordering
54 : 338643 : return getTermOrder(a[i], b[i]);
55 : : }
56 : : }
57 : : }
58 : : else
59 : : {
60 : 6886 : return a.getNumChildren() < b.getNumChildren();
61 : : }
62 : : }
63 : : else
64 : : {
65 : 216771 : return aop < bop;
66 : : }
67 [ + + ][ + + ]: 1124938 : }
68 : 72216 : return false;
69 : : }
70 : :
71 : 9570823 : Node TermCanonize::getCanonicalFreeVar(TypeNode tn, size_t i, uint32_t tc)
72 : : {
73 [ - + ][ - + ]: 9570823 : Assert(!tn.isNull());
[ - - ]
74 : 9570823 : std::pair<TypeNode, uint32_t> key(tn, tc);
75 : 9570823 : std::vector<Node>& tvars = d_cn_free_var[key];
76 [ + + ]: 9940231 : while (tvars.size() <= i)
77 : : {
78 : 369408 : std::stringstream os;
79 [ + + ]: 369408 : if (tn.isFunction())
80 : : {
81 : 1217 : os << "f" << i;
82 : : }
83 : : else
84 : : {
85 : 368191 : std::stringstream oss;
86 : 368191 : oss << tn;
87 : 368191 : std::string typ_name = oss.str();
88 [ + + ]: 455525 : while (typ_name[0] == '(')
89 : : {
90 : 87334 : typ_name.erase(typ_name.begin());
91 : : }
92 : 368191 : os << typ_name[0] << i;
93 : 368191 : }
94 : 369408 : NodeManager* nm = tn.getNodeManager();
95 : 369408 : BoundVarManager* bvm = nm->getBoundVarManager();
96 : : Node cacheVal = BoundVarManager::getCacheValue(
97 : 738816 : BoundVarManager::getCacheValue(nm, tc), i);
98 : 738816 : Node x = bvm->mkBoundVar(BoundVarId::TERM_CANONIZE, cacheVal, os.str(), tn);
99 : 369408 : d_fvIndex[x] = tvars.size();
100 : 369408 : tvars.push_back(x);
101 : 369408 : }
102 : 19141646 : return tvars[i];
103 : 9570823 : }
104 : :
105 : 9482320 : uint32_t TermCanonize::getTypeClass(TNode v)
106 : : {
107 [ + + ][ + + ]: 9482320 : return d_tcc == nullptr ? 0 : d_tcc->getTypeClass(v);
[ - - ]
108 : : }
109 : :
110 : 0 : size_t TermCanonize::getIndexForFreeVariable(Node v) const
111 : : {
112 : 0 : std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
113 [ - - ]: 0 : if (it == d_fvIndex.end())
114 : : {
115 : 0 : return 0;
116 : : }
117 : 0 : return it->second;
118 : : }
119 : :
120 : : struct sortTermOrder
121 : : {
122 : : TermCanonize* d_tu;
123 : 405922 : bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
124 : : };
125 : :
126 : 54008554 : Node TermCanonize::getCanonicalTerm(
127 : : TNode n,
128 : : bool apply_torder,
129 : : bool doHoVar,
130 : : std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
131 : : std::map<TNode, Node>& visited)
132 : : {
133 : 54008554 : std::map<TNode, Node>::iterator it = visited.find(n);
134 [ + + ]: 54008554 : if (it != visited.end())
135 : : {
136 : 13558861 : return it->second;
137 : : }
138 : :
139 [ + - ]: 40449693 : Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
140 [ + + ]: 40449693 : if (n.getKind() == Kind::BOUND_VARIABLE)
141 : : {
142 : 9482320 : uint32_t tc = getTypeClass(n);
143 : 9482320 : TypeNode tn = n.getType();
144 : 9482320 : std::pair<TypeNode, uint32_t> key(tn, tc);
145 : : // allocate variable
146 : 9482320 : unsigned vn = var_count[key];
147 : 9482320 : var_count[key]++;
148 : 9482320 : Node fv = getCanonicalFreeVar(tn, vn, tc);
149 : 9482320 : visited[n] = fv;
150 [ + - ]: 9482320 : Trace("canon-term-debug") << "...allocate variable " << fv << std::endl;
151 : 9482320 : return fv;
152 : 9482320 : }
153 [ + + ]: 30967373 : else if (n.getNumChildren() > 0)
154 : : {
155 : : // collect children
156 [ + - ]: 25354501 : Trace("canon-term-debug") << "Collect children" << std::endl;
157 : 25354501 : std::vector<Node> cchildren;
158 [ + + ]: 75954747 : for (const Node& cn : n)
159 : : {
160 : 50600246 : cchildren.push_back(cn);
161 : 50600246 : }
162 : : // now make canonical
163 [ + - ]: 25354501 : Trace("canon-term-debug") << "Make canonical children" << std::endl;
164 [ + + ]: 75954747 : for (unsigned i = 0, size = cchildren.size(); i < size; i++)
165 : : {
166 : 101200492 : cchildren[i] = getCanonicalTerm(
167 : 101200492 : cchildren[i], apply_torder, doHoVar, var_count, visited);
168 : : }
169 : : // if applicable, sort by term order
170 [ + + ][ + + ]: 25354501 : if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
[ + + ]
171 : : {
172 [ + - ]: 330680 : Trace("canon-term-debug")
173 : 165340 : << "Sort based on commutative operator " << n.getKind() << std::endl;
174 : : sortTermOrder sto;
175 : 165340 : sto.d_tu = this;
176 : 165340 : std::sort(cchildren.begin(), cchildren.end(), sto);
177 : : }
178 [ + + ]: 25354501 : if (n.getMetaKind() == metakind::PARAMETERIZED)
179 : : {
180 : 1218897 : Node op = n.getOperator();
181 [ + + ]: 1218897 : if (doHoVar)
182 : : {
183 : 194307 : op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
184 : : }
185 [ + - ]: 1218897 : Trace("canon-term-debug") << "Insert operator " << op << std::endl;
186 : 1218897 : cchildren.insert(cchildren.begin(), op);
187 : 1218897 : }
188 [ + - ]: 50709002 : Trace("canon-term-debug")
189 : 25354501 : << "...constructing for " << n << "." << std::endl;
190 : 25354501 : Node ret = n.getNodeManager()->mkNode(n.getKind(), cchildren);
191 [ + - ]: 50709002 : Trace("canon-term-debug")
192 : 25354501 : << "...constructed " << ret << " for " << n << "." << std::endl;
193 : 25354501 : visited[n] = ret;
194 : 25354501 : return ret;
195 : 25354501 : }
196 [ + - ]: 5612872 : Trace("canon-term-debug") << "...return 0-child term." << std::endl;
197 : 5612872 : return n;
198 : : }
199 : :
200 : 3189109 : Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
201 : : {
202 : 3189109 : std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
203 : 3189109 : std::map<TNode, Node> visited;
204 : 6378218 : return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
205 : 3189109 : }
206 : :
207 : 24892 : Node TermCanonize::getCanonicalTerm(TNode n,
208 : : std::map<TNode, Node>& visited,
209 : : bool apply_torder,
210 : : bool doHoVar)
211 : : {
212 : 24892 : std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
213 : 49784 : return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
214 : 24892 : }
215 : :
216 : : } // namespace expr
217 : : } // namespace cvc5::internal
|
