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 utilities for monomials.
11 : : */
12 : :
13 : : #include "theory/arith/nl/ext/monomial.h"
14 : :
15 : : #include "theory/arith/arith_utilities.h"
16 : : #include "theory/arith/nl/nl_lemma_utils.h"
17 : : #include "theory/rewriter.h"
18 : :
19 : : using namespace cvc5::internal::kind;
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace arith {
24 : : namespace nl {
25 : :
26 : : // Returns a[key] if key is in a or value otherwise.
27 : 238267 : unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value)
28 : : {
29 : 238267 : NodeMultiset::const_iterator it = a.find(key);
30 [ + + ]: 238267 : return (it == a.end()) ? value : it->second;
31 : : }
32 : : // Given two multisets return the multiset difference a \ b.
33 : 22974 : NodeMultiset diffMultiset(const NodeMultiset& a, const NodeMultiset& b)
34 : : {
35 : 22974 : NodeMultiset difference;
36 [ + + ]: 62116 : for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
37 : : {
38 : 39142 : Node key = it_a->first;
39 : 39142 : const unsigned a_value = it_a->second;
40 : 39142 : const unsigned b_value = getCountWithDefault(b, key, 0);
41 [ + + ]: 39142 : if (a_value > b_value)
42 : : {
43 : 29867 : difference[key] = a_value - b_value;
44 : : }
45 : 39142 : }
46 : 22974 : return difference;
47 : 0 : }
48 : :
49 : : // Return a vector containing a[key] repetitions of key in a multiset a.
50 : 22974 : std::vector<Node> ExpandMultiset(const NodeMultiset& a)
51 : : {
52 : 22974 : std::vector<Node> expansion;
53 [ + + ]: 52841 : for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
54 : : {
55 : 29867 : expansion.insert(expansion.end(), it_a->second, it_a->first);
56 : : }
57 : 22974 : return expansion;
58 : 0 : }
59 : :
60 : : // status 0 : n equal, -1 : n superset, 1 : n subset
61 : 141863 : void MonomialIndex::addTerm(Node n,
62 : : const std::vector<Node>& reps,
63 : : MonomialDb* nla,
64 : : int status,
65 : : unsigned argIndex)
66 : : {
67 [ + + ]: 141863 : if (status == 0)
68 : : {
69 [ + + ]: 29391 : if (argIndex == reps.size())
70 : : {
71 : 13583 : d_monos.push_back(n);
72 : : }
73 : : else
74 : : {
75 : 15808 : d_data[reps[argIndex]].addTerm(n, reps, nla, status, argIndex + 1);
76 : : }
77 : : }
78 : 141863 : for (std::map<Node, MonomialIndex>::iterator it = d_data.begin();
79 [ + + ]: 270859 : it != d_data.end();
80 : 128996 : ++it)
81 : : {
82 [ + + ][ + + ]: 128996 : if (status != 0 || argIndex == reps.size() || it->first != reps[argIndex])
[ + + ][ + + ]
83 : : {
84 : : // if we do not contain this variable, then if we were a superset,
85 : : // fail (-2), otherwise we are subset. if we do contain this
86 : : // variable, then if we were equal, we are superset since variables
87 : : // are ordered, otherwise we remain the same.
88 : : int new_status =
89 : 113188 : std::find(reps.begin(), reps.end(), it->first) == reps.end()
90 [ + + ][ + + ]: 120772 : ? (status >= 0 ? 1 : -2)
91 [ + + ]: 7584 : : (status == 0 ? -1 : status);
92 [ + + ]: 113188 : if (new_status != -2)
93 : : {
94 : 112472 : it->second.addTerm(n, reps, nla, new_status, argIndex);
95 : : }
96 : : }
97 : : }
98 : : // compare for subsets
99 [ + + ]: 294411 : for (unsigned i = 0; i < d_monos.size(); i++)
100 : : {
101 : 152548 : Node m = d_monos[i];
102 [ + + ]: 152548 : if (m != n)
103 : : {
104 : : // we are superset if we are equal and haven't traversed all variables
105 [ + + ][ + + ]: 138965 : int cstatus = status == 0 ? (argIndex == reps.size() ? 0 : -1) : status;
106 [ + - ]: 277930 : Trace("nl-ext-mindex-debug") << " compare " << n << " and " << m
107 : 138965 : << ", status = " << cstatus << std::endl;
108 : 138965 : if (cstatus <= 0 && nla->isMonomialSubset(m, n))
109 : : {
110 : 14159 : nla->registerMonomialSubset(m, n);
111 [ + - ]: 14159 : Trace("nl-ext-mindex-debug") << "...success" << std::endl;
112 : : }
113 : 124806 : else if (cstatus >= 0 && nla->isMonomialSubset(n, m))
114 : : {
115 : 8815 : nla->registerMonomialSubset(n, m);
116 [ + - ]: 8815 : Trace("nl-ext-mindex-debug") << "...success (rev)" << std::endl;
117 : : }
118 : : }
119 : 152548 : }
120 : 141863 : }
121 : :
122 : 33012 : MonomialDb::MonomialDb()
123 : : {
124 : 33012 : }
125 : :
126 : 200032 : void MonomialDb::registerMonomial(Node n)
127 : : {
128 [ + + ]: 200032 : if (std::find(d_monomials.begin(), d_monomials.end(), n) != d_monomials.end())
129 : : {
130 : 186449 : return;
131 : : }
132 : 13583 : d_monomials.push_back(n);
133 [ + - ]: 13583 : Trace("nl-ext-debug") << "Register monomial : " << n << std::endl;
134 : 13583 : Kind k = n.getKind();
135 [ + + ]: 13583 : if (k == Kind::NONLINEAR_MULT)
136 : : {
137 : : // get exponent count
138 : 4605 : unsigned nchild = n.getNumChildren();
139 [ + + ]: 15289 : for (unsigned i = 0; i < nchild; i++)
140 : : {
141 : 10684 : d_m_exp[n][n[i]]++;
142 : 10684 : if (i == 0 || n[i] != n[i - 1])
143 : : {
144 : 8505 : d_m_vlist[n].push_back(n[i]);
145 : : }
146 : : }
147 : 4605 : d_m_degree[n] = nchild;
148 : : }
149 [ + + ]: 8978 : else if (n.isConst())
150 : : {
151 [ - + ][ - + ]: 1675 : Assert(n.getConst<Rational>().isOne());
[ - - ]
152 : 1675 : d_m_exp[n].clear();
153 : 1675 : d_m_vlist[n].clear();
154 : 1675 : d_m_degree[n] = 0;
155 : : }
156 : : else
157 : : {
158 [ + - ][ + - ]: 7303 : Assert(k != Kind::ADD && k != Kind::MULT);
[ - + ][ - + ]
[ - - ]
159 : 7303 : d_m_exp[n][n] = 1;
160 : 7303 : d_m_vlist[n].push_back(n);
161 : 7303 : d_m_degree[n] = 1;
162 : : }
163 : 13583 : std::sort(d_m_vlist[n].begin(), d_m_vlist[n].end());
164 [ + - ]: 13583 : Trace("nl-ext-mindex") << "Add monomial to index : " << n << std::endl;
165 : 13583 : d_m_index.addTerm(n, d_m_vlist[n], this);
166 : : }
167 : :
168 : 22974 : void MonomialDb::registerMonomialSubset(Node a, Node b)
169 : : {
170 [ - + ][ - + ]: 22974 : Assert(isMonomialSubset(a, b));
[ - - ]
171 : :
172 : 22974 : const NodeMultiset& a_exponent_map = getMonomialExponentMap(a);
173 : 22974 : const NodeMultiset& b_exponent_map = getMonomialExponentMap(b);
174 : :
175 : : std::vector<Node> diff_children =
176 : 22974 : ExpandMultiset(diffMultiset(b_exponent_map, a_exponent_map));
177 [ - + ][ - + ]: 22974 : Assert(!diff_children.empty());
[ - - ]
178 : :
179 : 22974 : d_m_contain_parent[a].push_back(b);
180 : 22974 : d_m_contain_children[b].push_back(a);
181 : :
182 : : // currently use real type here
183 : 22974 : TypeNode tn = a.getNodeManager()->realType();
184 : 22974 : Node mult_term = safeConstructNaryType(tn, Kind::MULT, diff_children);
185 : : Node nlmult_term =
186 : 22974 : safeConstructNaryType(tn, Kind::NONLINEAR_MULT, diff_children);
187 : 22974 : d_m_contain_mult[a][b] = mult_term;
188 : 22974 : d_m_contain_umult[a][b] = nlmult_term;
189 [ + - ]: 45948 : Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b
190 : 22974 : << ", difference is " << mult_term << std::endl;
191 : 22974 : }
192 : :
193 : 163891 : bool MonomialDb::isMonomialSubset(Node am, Node bm) const
194 : : {
195 : 163891 : const NodeMultiset& a = getMonomialExponentMap(am);
196 : 163891 : const NodeMultiset& b = getMonomialExponentMap(bm);
197 [ + + ]: 199900 : for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
198 : : {
199 : 153952 : Node key = it_a->first;
200 : 153952 : const unsigned a_value = it_a->second;
201 : 153952 : const unsigned b_value = getCountWithDefault(b, key, 0);
202 [ + + ]: 153952 : if (a_value > b_value)
203 : : {
204 : 117943 : return false;
205 : : }
206 [ + + ]: 153952 : }
207 : 45948 : return true;
208 : : }
209 : :
210 : 562319 : const NodeMultiset& MonomialDb::getMonomialExponentMap(Node monomial) const
211 : : {
212 : 562319 : MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
213 [ - + ][ - + ]: 562319 : Assert(it != d_m_exp.end());
[ - - ]
214 : 562319 : return it->second;
215 : : }
216 : :
217 : 1355886 : unsigned MonomialDb::getExponent(Node monomial, Node v) const
218 : : {
219 : 1355886 : MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
220 [ - + ]: 1355886 : if (it == d_m_exp.end())
221 : : {
222 : 0 : return 0;
223 : : }
224 : 1355886 : std::map<Node, unsigned>::const_iterator itv = it->second.find(v);
225 [ - + ]: 1355886 : if (itv == it->second.end())
226 : : {
227 : 0 : return 0;
228 : : }
229 : 1355886 : return itv->second;
230 : : }
231 : :
232 : 2381514 : const std::vector<Node>& MonomialDb::getVariableList(Node monomial) const
233 : : {
234 : : std::map<Node, std::vector<Node> >::const_iterator itvl =
235 : 2381514 : d_m_vlist.find(monomial);
236 [ - + ][ - + ]: 2381514 : Assert(itvl != d_m_vlist.end());
[ - - ]
237 : 2381514 : return itvl->second;
238 : : }
239 : :
240 : 81768 : unsigned MonomialDb::getDegree(Node monomial) const
241 : : {
242 : 81768 : std::map<Node, unsigned>::const_iterator it = d_m_degree.find(monomial);
243 [ - + ][ - + ]: 81768 : Assert(it != d_m_degree.end());
[ - - ]
244 : 81768 : return it->second;
245 : : }
246 : :
247 : 2765 : void MonomialDb::sortByDegree(std::vector<Node>& ms) const
248 : : {
249 : 2765 : SortNonlinearDegree snlad(d_m_degree);
250 : 2765 : std::sort(ms.begin(), ms.end(), snlad);
251 : 2765 : }
252 : :
253 : 7165 : void MonomialDb::sortVariablesByModel(std::vector<Node>& ms, NlModel& m)
254 : : {
255 : 7165 : SortNlModel smv;
256 : 7165 : smv.d_nlm = &m;
257 : 7165 : smv.d_isConcrete = false;
258 : 7165 : smv.d_isAbsolute = true;
259 : 7165 : smv.d_reverse_order = true;
260 [ + + ]: 45208 : for (const Node& msc : ms)
261 : : {
262 : 38043 : std::sort(d_m_vlist[msc].begin(), d_m_vlist[msc].end(), smv);
263 : : }
264 : 7165 : }
265 : :
266 : 814 : const std::map<Node, std::vector<Node> >& MonomialDb::getContainsChildrenMap()
267 : : {
268 : 814 : return d_m_contain_children;
269 : : }
270 : :
271 : 2765 : const std::map<Node, std::vector<Node> >& MonomialDb::getContainsParentMap()
272 : : {
273 : 2765 : return d_m_contain_parent;
274 : : }
275 : :
276 : 367068 : Node MonomialDb::getContainsDiff(Node a, Node b) const
277 : : {
278 : : std::map<Node, std::map<Node, Node> >::const_iterator it =
279 : 367068 : d_m_contain_mult.find(a);
280 [ - + ]: 367068 : if (it == d_m_contain_mult.end())
281 : : {
282 : 0 : return Node::null();
283 : : }
284 : 367068 : std::map<Node, Node>::const_iterator it2 = it->second.find(b);
285 [ - + ]: 367068 : if (it2 == it->second.end())
286 : : {
287 : 0 : return Node::null();
288 : : }
289 : 367068 : return it2->second;
290 : : }
291 : :
292 : 874 : Node MonomialDb::getContainsDiffNl(Node a, Node b) const
293 : : {
294 : : std::map<Node, std::map<Node, Node> >::const_iterator it =
295 : 874 : d_m_contain_umult.find(a);
296 [ - + ]: 874 : if (it == d_m_contain_umult.end())
297 : : {
298 : 0 : return Node::null();
299 : : }
300 : 874 : std::map<Node, Node>::const_iterator it2 = it->second.find(b);
301 [ - + ]: 874 : if (it2 == it->second.end())
302 : : {
303 : 0 : return Node::null();
304 : : }
305 : 874 : return it2->second;
306 : : }
307 : :
308 : 25840 : Node MonomialDb::mkMonomialRemFactor(Node n,
309 : : const NodeMultiset& n_exp_rem) const
310 : : {
311 : 25840 : std::vector<Node> children;
312 : 25840 : const NodeMultiset& exponent_map = getMonomialExponentMap(n);
313 : 25840 : for (NodeMultiset::const_iterator itme2 = exponent_map.begin();
314 [ + + ]: 71013 : itme2 != exponent_map.end();
315 : 45173 : ++itme2)
316 : : {
317 : 45173 : Node v = itme2->first;
318 : 45173 : unsigned inc = itme2->second;
319 [ + - ]: 90346 : Trace("nl-ext-mono-factor")
320 : 45173 : << "..." << inc << " factors of " << v << std::endl;
321 : 45173 : unsigned count_in_n_exp_rem = getCountWithDefault(n_exp_rem, v, 0);
322 [ - + ][ - + ]: 45173 : Assert(count_in_n_exp_rem <= inc);
[ - - ]
323 : 45173 : inc -= count_in_n_exp_rem;
324 [ + - ]: 90346 : Trace("nl-ext-mono-factor")
325 : 45173 : << "......rem, now " << inc << " factors of " << v << std::endl;
326 : 45173 : children.insert(children.end(), inc, v);
327 : 45173 : }
328 : 25840 : Node ret = safeConstructNaryType(n.getType(), Kind::MULT, children);
329 [ + - ]: 25840 : Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl;
330 : 51680 : return ret;
331 : 25840 : }
332 : :
333 : : } // namespace nl
334 : : } // namespace arith
335 : : } // namespace theory
336 : : } // namespace cvc5::internal
|
