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 : 1834 : bool ArithMSum::getMonomial(Node n, Node& c, Node& v)
24 : : {
25 [ + - ][ + - ]: 1834 : if (n.getKind() == Kind::MULT && n.getNumChildren() == 2 && n[0].isConst())
[ + + ][ + - ]
[ + + ][ - - ]
26 : : {
27 : 831 : c = n[0];
28 : 831 : v = n[1];
29 : 831 : return true;
30 : : }
31 : 1003 : return false;
32 : : }
33 : :
34 : 1998634 : bool ArithMSum::getMonomial(Node n, std::map<Node, Node>& msum)
35 : : {
36 [ + + ]: 1998634 : if (n.isConst())
37 : : {
38 [ + - ]: 555364 : if (msum.find(Node::null()) == msum.end())
39 : : {
40 : 555364 : msum[Node::null()] = n;
41 : 555364 : return true;
42 : : }
43 : : }
44 [ + - ]: 540214 : else if (n.getKind() == Kind::MULT && n.getNumChildren() == 2
45 [ + + ][ + + ]: 1983484 : && n[0].isConst())
[ + + ][ + + ]
[ - - ]
46 : : {
47 [ + - ]: 540198 : if (msum.find(n[1]) == msum.end())
48 : : {
49 : 540198 : msum[n[1]] = n[0];
50 : 540198 : return true;
51 : : }
52 : : }
53 : : else
54 : : {
55 [ + - ]: 903072 : if (msum.find(n) == msum.end())
56 : : {
57 : 903072 : msum[n] = Node::null();
58 : 903072 : return true;
59 : : }
60 : : }
61 : 0 : return false;
62 : : }
63 : :
64 : 1264675 : bool ArithMSum::getMonomialSum(Node n, std::map<Node, Node>& msum)
65 : : {
66 [ + + ]: 1264675 : if (n.getKind() == Kind::ADD)
67 : : {
68 [ + + ]: 1773409 : for (Node nc : n)
69 : : {
70 [ - + ]: 1253684 : if (!getMonomial(nc, msum))
71 : : {
72 : 0 : return false;
73 : : }
74 [ + - ]: 1253684 : }
75 : 519725 : return true;
76 : : }
77 : 744950 : return getMonomial(n, msum);
78 : : }
79 : :
80 : 423590 : bool ArithMSum::getMonomialSumLit(Node lit, std::map<Node, Node>& msum)
81 : : {
82 : 1270770 : if (lit.getKind() == Kind::GEQ
83 : 423590 : || (lit.getKind() == Kind::EQUAL && lit[0].getType().isRealOrInt()))
84 : : {
85 [ + - ]: 374151 : if (getMonomialSum(lit[0], msum))
86 : : {
87 : 374151 : if (lit[1].isConst() && lit[1].getConst<Rational>().isZero())
88 : : {
89 : 88334 : return true;
90 : : }
91 : : else
92 : : {
93 : : // subtract the other side
94 : 285817 : std::map<Node, Node> msum2;
95 : 285817 : NodeManager* nm = lit.getNodeManager();
96 [ + - ]: 285817 : if (getMonomialSum(lit[1], msum2))
97 : : {
98 : 285817 : for (std::map<Node, Node>::iterator it = msum2.begin();
99 [ + + ]: 588765 : it != msum2.end();
100 : 302948 : ++it)
101 : : {
102 : 302948 : std::map<Node, Node>::iterator it2 = msum.find(it->first);
103 [ + + ]: 302948 : if (it2 != msum.end())
104 : : {
105 : 1465 : Rational r1 = it2->second.isNull()
106 : : ? Rational(1)
107 [ + + ]: 1465 : : it2->second.getConst<Rational>();
108 : 1465 : Rational r2 = it->second.isNull()
109 : : ? Rational(1)
110 [ + + ]: 1465 : : it->second.getConst<Rational>();
111 : 1465 : msum[it->first] = nm->mkConstRealOrInt(r1 - r2);
112 : 1465 : }
113 : : else
114 : : {
115 : 301483 : msum[it->first] =
116 : 301483 : it->second.isNull()
117 [ + + ][ - - ]: 1044552 : ? nm->mkConstInt(Rational(-1))
118 [ + + ][ + + ]: 743069 : : nm->mkConstRealOrInt(-it->second.getConst<Rational>());
[ - - ]
119 : : }
120 : : }
121 : 285817 : return true;
122 : : }
123 [ - + ]: 285817 : }
124 : : }
125 : : }
126 : 49439 : return false;
127 : : }
128 : :
129 : 2033 : Node ArithMSum::mkNode(NodeManager* nm, const std::map<Node, Node>& msum)
130 : : {
131 : 2033 : std::vector<Node> children;
132 [ + + ]: 4066 : for (std::map<Node, Node>::const_iterator it = msum.begin(); it != msum.end();
133 : 2033 : ++it)
134 : : {
135 : 2033 : Node m;
136 [ + + ]: 2033 : if (!it->first.isNull())
137 : : {
138 : 1277 : m = mkCoeffTerm(it->second, it->first);
139 : : }
140 : : else
141 : : {
142 [ - + ][ - + ]: 756 : Assert(!it->second.isNull());
[ - - ]
143 : 756 : m = it->second;
144 : : }
145 : 2033 : children.push_back(m);
146 : 2033 : }
147 : 2033 : return children.size() > 1
148 : : ? nm->mkNode(Kind::ADD, children)
149 : 4066 : : (children.size() == 1 ? children[0]
150 [ - + ][ + - ]: 10165 : : nm->mkConstInt(Rational(0)));
[ - + ][ - - ]
151 : 2033 : }
152 : :
153 : 954173 : Node ArithMSum::mkCoeffTerm(Node c, Node t)
154 : : {
155 [ + + ]: 954173 : if (c.isNull())
156 : : {
157 : 469871 : return t;
158 : : }
159 [ - + ][ - + ]: 484302 : Assert(c.isConst());
[ - - ]
160 : 484302 : NodeManager* nm = t.getNodeManager();
161 : 484302 : Rational r = c.getConst<Rational>();
162 : 484302 : TypeNode tt = t.getType();
163 : : // ensure no mixed arithmetic
164 [ + + ]: 484302 : if (!r.isIntegral())
165 : : {
166 [ + + ]: 6901 : if (!tt.isReal())
167 : : {
168 [ - + ][ - + ]: 884 : Assert(tt.isInteger());
[ - - ]
169 : 884 : return nm->mkNode(Kind::MULT, c, nm->mkNode(Kind::TO_REAL, t));
170 : : }
171 : : }
172 : : return nm->mkNode(
173 : 483418 : Kind::MULT, nm->mkConstRealOrInt(tt, c.getConst<Rational>()), t);
174 : 484302 : }
175 : :
176 : 225306 : int ArithMSum::isolate(
177 : : Node v, const std::map<Node, Node>& msum, Node& veq_c, Node& val, Kind k)
178 : : {
179 [ - + ][ - + ]: 225306 : Assert(veq_c.isNull());
[ - - ]
180 : 225306 : std::map<Node, Node>::const_iterator itv = msum.find(v);
181 [ + + ]: 225306 : if (itv != msum.end())
182 : : {
183 : 221879 : bool isReal = v.getType().isReal();
184 : 221879 : NodeManager* nm = v.getNodeManager();
185 : 221879 : std::vector<Node> children;
186 : : Rational r =
187 [ + + ]: 221879 : itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>();
188 [ + + ]: 221879 : if (r.sgn() != 0)
189 : : {
190 : 221875 : TypeNode vtn = v.getType();
191 : 221875 : for (std::map<Node, Node>::const_iterator it = msum.begin();
192 [ + + ]: 716055 : it != msum.end();
193 : 494180 : ++it)
194 : : {
195 [ + + ]: 494180 : if (it->first != v)
196 : : {
197 : 272305 : Node m;
198 [ + + ]: 272305 : if (!it->first.isNull())
199 : : {
200 : 192461 : m = mkCoeffTerm(it->second, it->first);
201 : : }
202 : : else
203 : : {
204 : 79844 : m = it->second;
205 : : }
206 [ + + ][ + + ]: 272305 : if (isReal && !m.getType().isReal())
[ + + ][ + + ]
[ - - ]
207 : : {
208 [ - + ][ - + ]: 4517 : Assert(m.getType().isInteger());
[ - - ]
209 : 4517 : m = arith::castToReal(nm, m);
210 : : }
211 : 272305 : children.push_back(m);
212 : 272305 : }
213 : : }
214 : 221875 : val = children.size() > 1
215 [ + + ][ + + ]: 774348 : ? nm->mkNode(Kind::ADD, children)
216 : 165299 : : (children.size() == 1
217 : 138778 : ? children[0]
218 : 470271 : : nm->mkConstRealOrInt(v.getType(), Rational(0)));
219 [ + + ][ + + ]: 221875 : if (!r.isOne() && !r.isNegativeOne())
[ + + ]
220 : : {
221 [ + + ]: 13616 : if (vtn.isInteger())
222 : : {
223 : 7960 : veq_c = nm->mkConstRealOrInt(r.abs());
224 : : }
225 : : else
226 : : {
227 : 11312 : val = nm->mkNode(
228 : 16968 : Kind::MULT, val, nm->mkConstReal(Rational(1) / r.abs()));
229 : : }
230 : : }
231 : 221875 : val = r.sgn() == 1
232 : 738334 : ? nm->mkNode(Kind::MULT,
233 : 369167 : nm->mkConstRealOrInt(val.getType(), Rational(-1)),
234 : : val)
235 : 221875 : : val;
236 [ + + ][ + + ]: 221875 : return (r.sgn() == 1 || k == Kind::EQUAL) ? 1 : -1;
237 : 221875 : }
238 [ + + ][ + + ]: 443754 : }
239 : 3431 : return 0;
240 : : }
241 : :
242 : 13057 : int ArithMSum::isolate(
243 : : Node v, const std::map<Node, Node>& msum, Node& veq, Kind k, bool doCoeff)
244 : : {
245 : 13057 : Node veq_c;
246 : 13057 : Node val;
247 : : // isolate v in the (in)equality
248 : 13057 : int ires = isolate(v, msum, veq_c, val, k);
249 [ + - ]: 13057 : if (ires != 0)
250 : : {
251 : 13057 : NodeManager* nm = v.getNodeManager();
252 : 13057 : Node vc = v;
253 [ + + ]: 13057 : if (!veq_c.isNull())
254 : : {
255 [ + + ]: 851 : if (doCoeff)
256 : : {
257 : 825 : vc = nm->mkNode(Kind::MULT, veq_c, vc);
258 : : }
259 : : else
260 : : {
261 : 26 : return 0;
262 : : }
263 : : }
264 : 13031 : bool inOrder = ires == 1;
265 : : // ensure type is correct for equality
266 [ + + ]: 13031 : if (k == Kind::EQUAL)
267 : : {
268 : 5373 : bool vci = vc.getType().isInteger();
269 : 5373 : bool vi = val.getType().isInteger();
270 [ + + ][ - + ]: 5373 : if (!vci && vi)
271 : : {
272 : 0 : val = nm->mkNode(Kind::TO_REAL, val);
273 : : }
274 [ + + ][ - + ]: 5373 : else if (vci && !vi)
275 : : {
276 : 0 : val = nm->mkNode(Kind::TO_INTEGER, val);
277 : : }
278 [ - + ][ - - ]: 21492 : AssertEqual(val.getType(), vc.getType())
279 : 5373 : << val << " " << vc << " " << val.getType() << " " << vc.getType();
280 : : }
281 [ + + ][ + + ]: 13031 : veq = nm->mkNode(k, inOrder ? vc : val, inOrder ? val : vc);
282 [ + + ]: 13057 : }
283 : 13031 : return ires;
284 : 13057 : }
285 : :
286 : 156 : Node ArithMSum::solveEqualityFor(Node lit, Node v)
287 : : {
288 [ - + ][ - + ]: 156 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
289 : : // first look directly at sides
290 : 156 : TypeNode tn = lit[0].getType();
291 [ + + ]: 262 : for (unsigned r = 0; r < 2; r++)
292 : : {
293 [ + + ]: 209 : if (lit[r] == v)
294 : : {
295 : 103 : return lit[1 - r];
296 : : }
297 : : }
298 [ + - ]: 53 : if (tn.isRealOrInt())
299 : : {
300 : 53 : std::map<Node, Node> msum;
301 [ + - ]: 53 : if (ArithMSum::getMonomialSumLit(lit, msum))
302 : : {
303 : 53 : Node val, veqc;
304 [ + + ]: 53 : if (ArithMSum::isolate(v, msum, veqc, val, Kind::EQUAL) != 0)
305 : : {
306 [ + - ]: 44 : 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 : 44 : return val;
312 : : }
313 : : }
314 [ + + ][ + + ]: 97 : }
315 [ + + ]: 53 : }
316 : 9 : return Node::null();
317 : 156 : }
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 : 5613 : void ArithMSum::debugPrintMonomialSum(std::map<Node, Node>& msum,
341 : : CVC5_UNUSED const char* c)
342 : : {
343 [ + + ]: 16893 : for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end(); ++it)
344 : : {
345 [ + - ]: 11280 : Trace(c) << " ";
346 [ + + ]: 11280 : if (!it->second.isNull())
347 : : {
348 [ + - ]: 5011 : Trace(c) << it->second;
349 [ + + ]: 5011 : if (!it->first.isNull())
350 : : {
351 [ + - ]: 2868 : Trace(c) << " * ";
352 : : }
353 : : }
354 [ + + ]: 11280 : if (!it->first.isNull())
355 : : {
356 [ + - ]: 9137 : Trace(c) << it->first;
357 : : }
358 [ + - ]: 11280 : Trace(c) << std::endl;
359 : : }
360 [ + - ]: 5613 : Trace(c) << std::endl;
361 : 5613 : }
362 : :
363 : : } // namespace theory
364 : : } // namespace cvc5::internal
|
