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 : : * Arithmetic utilities regarding monomial sums.
11 : : */
12 : :
13 : : #include "theory/arith/arith_msum.h"
14 : :
15 : : #include "theory/arith/arith_utilities.h"
16 : : #include "theory/rewriter.h"
17 : :
18 : : using namespace cvc5::internal::kind;
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : :
23 : 2045 : bool ArithMSum::getMonomial(Node n, Node& c, Node& v)
24 : : {
25 [ + - ][ + + ]: 2045 : if (n.getKind() == Kind::MULT && n.getNumChildren() == 2 && n[0].isConst())
[ + + ][ + + ]
[ + + ][ - - ]
26 : : {
27 : 118 : c = n[0];
28 : 118 : v = n[1];
29 : 118 : return true;
30 : : }
31 : 1927 : return false;
32 : : }
33 : :
34 : 1988477 : bool ArithMSum::getMonomial(Node n, std::map<Node, Node>& msum)
35 : : {
36 [ + + ]: 1988477 : if (n.isConst())
37 : : {
38 [ + - ]: 543706 : if (msum.find(Node::null()) == msum.end())
39 : : {
40 : 543706 : msum[Node::null()] = n;
41 : 543706 : return true;
42 : : }
43 : : }
44 [ + - ]: 522100 : else if (n.getKind() == Kind::MULT && n.getNumChildren() == 2
45 [ + + ][ + + ]: 1966871 : && n[0].isConst())
[ + + ][ + + ]
[ - - ]
46 : : {
47 [ + - ]: 522066 : if (msum.find(n[1]) == msum.end())
48 : : {
49 : 522066 : msum[n[1]] = n[0];
50 : 522066 : return true;
51 : : }
52 : : }
53 : : else
54 : : {
55 [ + - ]: 922705 : if (msum.find(n) == msum.end())
56 : : {
57 : 922705 : msum[n] = Node::null();
58 : 922705 : return true;
59 : : }
60 : : }
61 : 0 : return false;
62 : : }
63 : :
64 : 1276117 : bool ArithMSum::getMonomialSum(Node n, std::map<Node, Node>& msum)
65 : : {
66 [ + + ]: 1276117 : if (n.getKind() == Kind::ADD)
67 : : {
68 [ + + ]: 1724650 : for (Node nc : n)
69 : : {
70 [ - + ]: 1218505 : if (!getMonomial(nc, msum))
71 : : {
72 : 0 : return false;
73 : : }
74 [ + - ]: 1218505 : }
75 : 506145 : return true;
76 : : }
77 : 769972 : return getMonomial(n, msum);
78 : : }
79 : :
80 : 459491 : bool ArithMSum::getMonomialSumLit(Node lit, std::map<Node, Node>& msum)
81 : : {
82 : 1378473 : if (lit.getKind() == Kind::GEQ
83 : 459491 : || (lit.getKind() == Kind::EQUAL && lit[0].getType().isRealOrInt()))
84 : : {
85 [ + - ]: 388028 : if (getMonomialSum(lit[0], msum))
86 : : {
87 : 388028 : if (lit[1].isConst() && lit[1].getConst<Rational>().isZero())
88 : : {
89 : 85809 : return true;
90 : : }
91 : : else
92 : : {
93 : : // subtract the other side
94 : 302219 : std::map<Node, Node> msum2;
95 : 302219 : NodeManager* nm = lit.getNodeManager();
96 [ + - ]: 302219 : if (getMonomialSum(lit[1], msum2))
97 : : {
98 : 302219 : for (std::map<Node, Node>::iterator it = msum2.begin();
99 [ + + ]: 627924 : it != msum2.end();
100 : 325705 : ++it)
101 : : {
102 : 325705 : std::map<Node, Node>::iterator it2 = msum.find(it->first);
103 [ + + ]: 325705 : if (it2 != msum.end())
104 : : {
105 : 100 : Rational r1 = it2->second.isNull()
106 : : ? Rational(1)
107 [ + + ]: 100 : : it2->second.getConst<Rational>();
108 : 100 : Rational r2 = it->second.isNull()
109 : : ? Rational(1)
110 [ + + ]: 100 : : it->second.getConst<Rational>();
111 : 100 : msum[it->first] = nm->mkConstRealOrInt(r1 - r2);
112 : 100 : }
113 : : else
114 : : {
115 : 325605 : msum[it->first] =
116 : 325605 : it->second.isNull()
117 [ + + ][ - - ]: 1125936 : ? nm->mkConstInt(Rational(-1))
118 [ + + ][ + + ]: 800331 : : nm->mkConstRealOrInt(-it->second.getConst<Rational>());
[ - - ]
119 : : }
120 : : }
121 : 302219 : return true;
122 : : }
123 [ - + ]: 302219 : }
124 : : }
125 : : }
126 : 71463 : return false;
127 : : }
128 : :
129 : 2006 : Node ArithMSum::mkNode(NodeManager* nm, const std::map<Node, Node>& msum)
130 : : {
131 : 2006 : std::vector<Node> children;
132 [ + + ]: 4012 : for (std::map<Node, Node>::const_iterator it = msum.begin(); it != msum.end();
133 : 2006 : ++it)
134 : : {
135 : 2006 : Node m;
136 [ + + ]: 2006 : if (!it->first.isNull())
137 : : {
138 : 1245 : m = mkCoeffTerm(it->second, it->first);
139 : : }
140 : : else
141 : : {
142 [ - + ][ - + ]: 761 : Assert(!it->second.isNull());
[ - - ]
143 : 761 : m = it->second;
144 : : }
145 : 2006 : children.push_back(m);
146 : 2006 : }
147 : 2006 : return children.size() > 1
148 : : ? nm->mkNode(Kind::ADD, children)
149 : 4012 : : (children.size() == 1 ? children[0]
150 [ - + ][ + - ]: 10030 : : nm->mkConstInt(Rational(0)));
[ - + ][ - - ]
151 : 2006 : }
152 : :
153 : 980754 : Node ArithMSum::mkCoeffTerm(Node c, Node t)
154 : : {
155 [ + + ]: 980754 : if (c.isNull())
156 : : {
157 : 491714 : return t;
158 : : }
159 [ - + ][ - + ]: 489040 : Assert(c.isConst());
[ - - ]
160 : 489040 : NodeManager* nm = t.getNodeManager();
161 : 489040 : Rational r = c.getConst<Rational>();
162 : 489040 : TypeNode tt = t.getType();
163 : : // ensure no mixed arithmetic
164 [ + + ]: 489040 : if (!r.isIntegral())
165 : : {
166 [ + + ]: 6458 : if (!tt.isReal())
167 : : {
168 [ - + ][ - + ]: 859 : Assert(tt.isInteger());
[ - - ]
169 : 859 : return nm->mkNode(Kind::MULT, c, nm->mkNode(Kind::TO_REAL, t));
170 : : }
171 : : }
172 : : return nm->mkNode(
173 : 488181 : Kind::MULT, nm->mkConstRealOrInt(tt, c.getConst<Rational>()), t);
174 : 489040 : }
175 : :
176 : 240940 : int ArithMSum::isolate(
177 : : Node v, const std::map<Node, Node>& msum, Node& veq_c, Node& val, Kind k)
178 : : {
179 [ - + ][ - + ]: 240940 : Assert(veq_c.isNull());
[ - - ]
180 : 240940 : std::map<Node, Node>::const_iterator itv = msum.find(v);
181 [ + + ]: 240940 : if (itv != msum.end())
182 : : {
183 : 237524 : bool isReal = v.getType().isReal();
184 : 237524 : NodeManager* nm = v.getNodeManager();
185 : 237524 : std::vector<Node> children;
186 : : Rational r =
187 [ + + ]: 237524 : itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>();
188 [ + + ]: 237524 : if (r.sgn() != 0)
189 : : {
190 : 237520 : TypeNode vtn = v.getType();
191 : 237520 : for (std::map<Node, Node>::const_iterator it = msum.begin();
192 [ + + ]: 760598 : it != msum.end();
193 : 523078 : ++it)
194 : : {
195 [ + + ]: 523078 : if (it->first != v)
196 : : {
197 : 285558 : Node m;
198 [ + + ]: 285558 : if (!it->first.isNull())
199 : : {
200 : 202083 : m = mkCoeffTerm(it->second, it->first);
201 : : }
202 : : else
203 : : {
204 : 83475 : m = it->second;
205 : : }
206 [ + + ][ + + ]: 285558 : if (isReal && !m.getType().isReal())
[ + + ][ + + ]
[ - - ]
207 : : {
208 [ - + ][ - + ]: 4647 : Assert(m.getType().isInteger());
[ - - ]
209 : 4647 : m = arith::castToReal(nm, m);
210 : : }
211 : 285558 : children.push_back(m);
212 : 285558 : }
213 : : }
214 : 237520 : val = children.size() > 1
215 [ + + ][ + + ]: 829468 : ? nm->mkNode(Kind::ADD, children)
216 : 177214 : : (children.size() == 1
217 : 150986 : ? children[0]
218 : 501268 : : nm->mkConstRealOrInt(v.getType(), Rational(0)));
219 [ + + ][ + + ]: 237520 : if (!r.isOne() && !r.isNegativeOne())
[ + + ]
220 : : {
221 [ + + ]: 11492 : if (vtn.isInteger())
222 : : {
223 : 6803 : veq_c = nm->mkConstRealOrInt(r.abs());
224 : : }
225 : : else
226 : : {
227 : 9378 : val = nm->mkNode(
228 : 14067 : Kind::MULT, val, nm->mkConstReal(Rational(1) / r.abs()));
229 : : }
230 : : }
231 : 237520 : val = r.sgn() == 1
232 : 790864 : ? nm->mkNode(Kind::MULT,
233 : 395432 : nm->mkConstRealOrInt(val.getType(), Rational(-1)),
234 : : val)
235 : 237520 : : val;
236 [ + + ][ + + ]: 237520 : return (r.sgn() == 1 || k == Kind::EQUAL) ? 1 : -1;
237 : 237520 : }
238 [ + + ][ + + ]: 475044 : }
239 : 3420 : return 0;
240 : : }
241 : :
242 : 12712 : int ArithMSum::isolate(
243 : : Node v, const std::map<Node, Node>& msum, Node& veq, Kind k, bool doCoeff)
244 : : {
245 : 12712 : Node veq_c;
246 : 12712 : Node val;
247 : : // isolate v in the (in)equality
248 : 12712 : int ires = isolate(v, msum, veq_c, val, k);
249 [ + - ]: 12712 : if (ires != 0)
250 : : {
251 : 12712 : NodeManager* nm = v.getNodeManager();
252 : 12712 : Node vc = v;
253 [ + + ]: 12712 : if (!veq_c.isNull())
254 : : {
255 [ + + ]: 138 : if (doCoeff)
256 : : {
257 : 112 : vc = nm->mkNode(Kind::MULT, veq_c, vc);
258 : : }
259 : : else
260 : : {
261 : 26 : return 0;
262 : : }
263 : : }
264 : 12686 : bool inOrder = ires == 1;
265 : : // ensure type is correct for equality
266 [ + + ]: 12686 : if (k == Kind::EQUAL)
267 : : {
268 : 5050 : bool vci = vc.getType().isInteger();
269 : 5050 : bool vi = val.getType().isInteger();
270 [ + + ][ - + ]: 5050 : if (!vci && vi)
271 : : {
272 : 0 : val = nm->mkNode(Kind::TO_REAL, val);
273 : : }
274 [ + + ][ + + ]: 5050 : else if (vci && !vi)
275 : : {
276 : 2 : val = nm->mkNode(Kind::TO_INTEGER, val);
277 : : }
278 [ - + ][ - - ]: 20200 : AssertEqual(val.getType(), vc.getType())
279 : 5050 : << val << " " << vc << " " << val.getType() << " " << vc.getType();
280 : : }
281 [ + + ][ + + ]: 12686 : veq = nm->mkNode(k, inOrder ? vc : val, inOrder ? val : vc);
282 [ + + ]: 12712 : }
283 : 12686 : return ires;
284 : 12712 : }
285 : :
286 : 160 : Node ArithMSum::solveEqualityFor(Node lit, Node v)
287 : : {
288 [ - + ][ - + ]: 160 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
289 : : // first look directly at sides
290 : 160 : TypeNode tn = lit[0].getType();
291 [ + + ]: 274 : for (unsigned r = 0; r < 2; r++)
292 : : {
293 [ + + ]: 217 : if (lit[r] == v)
294 : : {
295 : 103 : return lit[1 - r];
296 : : }
297 : : }
298 [ + - ]: 57 : if (tn.isRealOrInt())
299 : : {
300 : 57 : std::map<Node, Node> msum;
301 [ + - ]: 57 : if (ArithMSum::getMonomialSumLit(lit, msum))
302 : : {
303 : 57 : Node val, veqc;
304 [ + + ]: 57 : if (ArithMSum::isolate(v, msum, veqc, val, Kind::EQUAL) != 0)
305 : : {
306 [ + - ]: 48 : if (veqc.isNull())
307 : : {
308 : : // in this case, we have an integer equality with a coefficient
309 : : // on the variable we solved for that could not be eliminated,
310 : : // hence we fail.
311 : 48 : return val;
312 : : }
313 : : }
314 [ + + ][ + + ]: 105 : }
315 [ + + ]: 57 : }
316 : 9 : return Node::null();
317 : 160 : }
318 : :
319 : 0 : bool ArithMSum::decompose(Node n, Node v, Node& coeff, Node& rem)
320 : : {
321 : 0 : std::map<Node, Node> msum;
322 [ - - ]: 0 : if (getMonomialSum(n, msum))
323 : : {
324 : 0 : std::map<Node, Node>::iterator it = msum.find(v);
325 [ - - ]: 0 : if (it == msum.end())
326 : : {
327 : 0 : return false;
328 : : }
329 : : else
330 : : {
331 : 0 : coeff = it->second;
332 : 0 : msum.erase(v);
333 : 0 : rem = mkNode(n.getNodeManager(), msum);
334 : 0 : return true;
335 : : }
336 : : }
337 : 0 : return false;
338 : 0 : }
339 : :
340 : 5557 : void ArithMSum::debugPrintMonomialSum(std::map<Node, Node>& msum,
341 : : CVC5_UNUSED const char* c)
342 : : {
343 [ + + ]: 16773 : for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end(); ++it)
344 : : {
345 [ + - ]: 11216 : Trace(c) << " ";
346 [ + + ]: 11216 : if (!it->second.isNull())
347 : : {
348 [ + - ]: 4999 : Trace(c) << it->second;
349 [ + + ]: 4999 : if (!it->first.isNull())
350 : : {
351 [ + - ]: 2840 : Trace(c) << " * ";
352 : : }
353 : : }
354 [ + + ]: 11216 : if (!it->first.isNull())
355 : : {
356 [ + - ]: 9057 : Trace(c) << it->first;
357 : : }
358 [ + - ]: 11216 : Trace(c) << std::endl;
359 : : }
360 [ + - ]: 5557 : Trace(c) << std::endl;
361 : 5557 : }
362 : :
363 : : } // namespace theory
364 : : } // namespace cvc5::internal
|
