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 : : * Congruence manager, the interface to the equality engine from the
11 : : * linear arithmetic solver
12 : : */
13 : :
14 : : #include "theory/arith/linear/congruence_manager.h"
15 : :
16 : : #include "base/output.h"
17 : : #include "options/arith_options.h"
18 : : #include "proof/conv_proof_generator.h"
19 : : #include "proof/proof_checker.h"
20 : : #include "proof/proof_node.h"
21 : : #include "proof/proof_node_manager.h"
22 : : #include "smt/env.h"
23 : : #include "theory/arith/arith_poly_norm.h"
24 : : #include "theory/arith/arith_proof_utilities.h"
25 : : #include "theory/arith/arith_subs.h"
26 : : #include "theory/arith/arith_utilities.h"
27 : : #include "theory/arith/linear/constraint.h"
28 : : #include "theory/arith/linear/partial_model.h"
29 : : #include "theory/ee_setup_info.h"
30 : : #include "theory/rewriter.h"
31 : : #include "theory/uf/equality_engine.h"
32 : : #include "theory/uf/proof_equality_engine.h"
33 : :
34 : : using namespace cvc5::internal::kind;
35 : :
36 : : namespace cvc5::internal {
37 : : namespace theory {
38 : : namespace arith::linear {
39 : :
40 : 544 : std::vector<Node> andComponents(NodeManager* nm, TNode an)
41 : : {
42 [ - + ]: 544 : if (an == nm->mkConst(true))
43 : : {
44 : 0 : return {};
45 : : }
46 [ - + ]: 544 : else if (an.getKind() != Kind::AND)
47 : : {
48 : 0 : return {an};
49 : : }
50 : 544 : std::vector<Node> a{};
51 : 544 : a.reserve(an.getNumChildren());
52 : 544 : a.insert(a.end(), an.begin(), an.end());
53 : 544 : return a;
54 : 544 : }
55 : :
56 : 28782 : ArithCongruenceManager::ArithCongruenceManager(
57 : : Env& env,
58 : : ConstraintDatabase& cd,
59 : : SetupLiteralCallBack setup,
60 : : const ArithVariables& avars,
61 : 28782 : RaiseEqualityEngineConflict raiseConflict)
62 : : : EnvObj(env),
63 : 28782 : d_inConflict(context()),
64 : 28782 : d_raiseConflict(raiseConflict),
65 : 28782 : d_keepAlive(context()),
66 : 28782 : d_propagatations(context()),
67 : 28782 : d_explanationMap(context()),
68 : 28782 : d_constraintDatabase(cd),
69 : 28782 : d_setupLiteral(setup),
70 : 28782 : d_avariables(avars),
71 : 28782 : d_ee(nullptr),
72 [ + + ]: 28782 : d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
73 : : : nullptr),
74 : : // Construct d_pfGenEe with the SAT context, since its proof include
75 : : // unclosed assumptions of theory literals.
76 : 57564 : d_pfGenEe(new EagerProofGenerator(
77 : 57564 : d_env, context(), "ArithCongruenceManager::pfGenEe")),
78 : : // Construct d_pfGenEe with the USER context, since its proofs are closed.
79 : 57564 : d_pfGenExplain(new EagerProofGenerator(
80 : 57564 : d_env, userContext(), "ArithCongruenceManager::pfGenExplain")),
81 : 28782 : d_pfee(nullptr),
82 : 86346 : d_statistics(statisticsRegistry())
83 : : {
84 : 28782 : }
85 : :
86 : 28769 : ArithCongruenceManager::~ArithCongruenceManager() {}
87 : :
88 : 28710 : void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
89 : : {
90 [ - + ][ - + ]: 28710 : Assert(ee != nullptr);
[ - - ]
91 : : // otherwise, we use the official one
92 : 28710 : d_ee = ee;
93 : : // the congruence kinds are already set up
94 : : // the proof equality engine is the one from the equality engine
95 : 28710 : d_pfee = d_ee->getProofEqualityEngine();
96 : : // have proof equality engine only if proofs are enabled
97 [ - + ][ - + ]: 28710 : Assert(isProofEnabled() == (d_pfee != nullptr));
[ - - ]
98 : 28710 : }
99 : :
100 : 28782 : ArithCongruenceManager::Statistics::Statistics(StatisticsRegistry& sr)
101 : : : d_watchedVariables(
102 : 28782 : sr.registerInt("theory::arith::congruence::watchedVariables")),
103 : : d_watchedVariableIsZero(
104 : 28782 : sr.registerInt("theory::arith::congruence::watchedVariableIsZero")),
105 : 28782 : d_watchedVariableIsNotZero(sr.registerInt(
106 : : "theory::arith::congruence::watchedVariableIsNotZero")),
107 : : d_equalsConstantCalls(
108 : 28782 : sr.registerInt("theory::arith::congruence::equalsConstantCalls")),
109 : 28782 : d_propagations(sr.registerInt("theory::arith::congruence::propagations")),
110 : : d_propagateConstraints(
111 : 28782 : sr.registerInt("theory::arith::congruence::propagateConstraints")),
112 : 28782 : d_conflicts(sr.registerInt("theory::arith::congruence::conflicts"))
113 : : {
114 : 28782 : }
115 : :
116 : 4317 : void ArithCongruenceManager::raiseConflict(Node conflict,
117 : : std::shared_ptr<ProofNode> pf)
118 : : {
119 [ - + ][ - + ]: 4317 : Assert(!inConflict());
[ - - ]
120 [ + - ]: 8634 : Trace("arith::conflict") << "difference manager conflict " << conflict
121 : 4317 : << std::endl;
122 : 4317 : d_inConflict.raise();
123 : 4317 : d_raiseConflict.raiseEEConflict(conflict, pf);
124 : 4317 : }
125 : 1375293 : bool ArithCongruenceManager::inConflict() const
126 : : {
127 : 1375293 : return d_inConflict.isRaised();
128 : : }
129 : :
130 : 5157480 : bool ArithCongruenceManager::hasMorePropagations() const
131 : : {
132 : 5157480 : return !d_propagatations.empty();
133 : : }
134 : 943063 : const Node ArithCongruenceManager::getNextPropagation()
135 : : {
136 [ - + ][ - + ]: 943063 : Assert(hasMorePropagations());
[ - - ]
137 : 943063 : Node prop = d_propagatations.front();
138 : 943063 : d_propagatations.dequeue();
139 : 943063 : return prop;
140 : 0 : }
141 : :
142 : 116552 : bool ArithCongruenceManager::canExplain(TNode n) const
143 : : {
144 : 116552 : return d_explanationMap.find(n) != d_explanationMap.end();
145 : : }
146 : :
147 : 20508 : Node ArithCongruenceManager::externalToInternal(TNode n) const
148 : : {
149 [ - + ][ - + ]: 20508 : Assert(canExplain(n));
[ - - ]
150 : 20508 : ExplainMap::const_iterator iter = d_explanationMap.find(n);
151 : 20508 : size_t pos = (*iter).second;
152 : 41016 : return d_propagatations[pos];
153 : : }
154 : :
155 : 832809 : void ArithCongruenceManager::pushBack(TNode n)
156 : : {
157 : 832809 : d_explanationMap.insert(n, d_propagatations.size());
158 : 832809 : d_propagatations.enqueue(n);
159 : :
160 : 832809 : ++(d_statistics.d_propagations);
161 : 832809 : }
162 : 174693 : void ArithCongruenceManager::pushBack(TNode n, TNode r)
163 : : {
164 : 174693 : d_explanationMap.insert(r, d_propagatations.size());
165 : 174693 : d_explanationMap.insert(n, d_propagatations.size());
166 : 174693 : d_propagatations.enqueue(n);
167 : :
168 : 174693 : ++(d_statistics.d_propagations);
169 : 174693 : }
170 : 0 : void ArithCongruenceManager::pushBack(TNode n, TNode r, TNode w)
171 : : {
172 : 0 : d_explanationMap.insert(w, d_propagatations.size());
173 : 0 : d_explanationMap.insert(r, d_propagatations.size());
174 : 0 : d_explanationMap.insert(n, d_propagatations.size());
175 : 0 : d_propagatations.enqueue(n);
176 : :
177 : 0 : ++(d_statistics.d_propagations);
178 : 0 : }
179 : :
180 : 24970 : void ArithCongruenceManager::pushBackAlias(TNode n)
181 : : {
182 [ - + ][ - + ]: 24970 : Assert(d_propagatations.size() > 0);
[ - - ]
183 : 24970 : d_explanationMap.insert(n, d_propagatations.size() - 1);
184 : 24970 : }
185 : :
186 : 666098 : void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb,
187 : : ConstraintCP ub)
188 : : {
189 [ - + ][ - + ]: 666098 : Assert(lb->isLowerBound());
[ - - ]
190 [ - + ][ - + ]: 666098 : Assert(ub->isUpperBound());
[ - - ]
191 [ - + ][ - + ]: 666098 : Assert(lb->getVariable() == ub->getVariable());
[ - - ]
192 [ - + ][ - + ]: 666098 : Assert(lb->getValue().sgn() == 0);
[ - - ]
193 [ - + ][ - + ]: 666098 : Assert(ub->getValue().sgn() == 0);
[ - - ]
194 : :
195 : 666098 : ++(d_statistics.d_watchedVariableIsZero);
196 : :
197 : 666098 : ArithVar s = lb->getVariable();
198 : 666098 : TNode eq = d_watchedEqualities[s];
199 : 666098 : ConstraintCP eqC = d_constraintDatabase.getConstraint(
200 : : s, ConstraintType::Equality, lb->getValue());
201 : 666098 : NodeBuilder reasonBuilder(nodeManager(), Kind::AND);
202 : 666098 : auto pfLb = lb->externalExplainByAssertions(reasonBuilder);
203 : 666098 : auto pfUb = ub->externalExplainByAssertions(reasonBuilder);
204 : 666098 : Node reason = mkAndFromBuilder(nodeManager(), reasonBuilder);
205 : 666098 : std::shared_ptr<ProofNode> pf{};
206 [ + + ]: 666098 : if (isProofEnabled())
207 : : {
208 [ + + ][ - - ]: 1478408 : pf = d_pnm->mkNode(
209 : 1108806 : ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eqC->getProofLiteral());
210 : 369602 : pf = ensurePredTransform(d_pnm, pf, eq);
211 : : }
212 : :
213 : 666098 : d_keepAlive.push_back(reason);
214 [ + - ]: 1332196 : Trace("arith-ee") << "Asserting an equality on " << s << ", on trichotomy"
215 : 666098 : << std::endl;
216 [ + - ]: 666098 : Trace("arith-ee") << " based on " << lb << std::endl;
217 [ + - ]: 666098 : Trace("arith-ee") << " based on " << ub << std::endl;
218 : 666098 : assertionToEqualityEngine(true, s, reason, pf);
219 : 666098 : }
220 : :
221 : 524380 : void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq)
222 : : {
223 [ + - ]: 524380 : Trace("arith::cong") << "Cong::watchedVariableIsZero: " << *eq << std::endl;
224 : :
225 [ - + ][ - + ]: 524380 : Assert(eq->isEquality());
[ - - ]
226 [ - + ][ - + ]: 524380 : Assert(eq->getValue().sgn() == 0);
[ - - ]
227 : :
228 : 524380 : ++(d_statistics.d_watchedVariableIsZero);
229 : :
230 : 524380 : ArithVar s = eq->getVariable();
231 : :
232 : : // Explain for conflict is correct as these proofs are generated
233 : : // and stored eagerly
234 : : // These will be safe for propagation later as well
235 : 524380 : NodeBuilder nb(nodeManager(), Kind::AND);
236 : : // An open proof of eq from literals now in reason.
237 [ - + ]: 524380 : if (TraceIsOn("arith::cong"))
238 : : {
239 [ - - ]: 0 : eq->printProofTree(Trace("arith::cong"));
240 : : }
241 : 524380 : auto pf = eq->externalExplainByAssertions(nb);
242 [ + + ]: 524380 : if (isProofEnabled())
243 : : {
244 : 215002 : pf = ensurePredTransform(d_pnm, pf, d_watchedEqualities[s]);
245 : : }
246 : 524380 : Node reason = mkAndFromBuilder(nodeManager(), nb);
247 : :
248 : 524380 : d_keepAlive.push_back(reason);
249 : 524380 : assertionToEqualityEngine(true, s, reason, pf);
250 : 524380 : }
251 : :
252 : 1368989 : void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c)
253 : : {
254 [ + - ]: 2737978 : Trace("arith::cong::notzero")
255 : 1368989 : << "Cong::watchedVariableCannotBeZero " << *c << std::endl;
256 : 1368989 : ++(d_statistics.d_watchedVariableIsNotZero);
257 : :
258 : 1368989 : ArithVar s = c->getVariable();
259 : 1368989 : Node disEq = d_watchedEqualities[s].negate();
260 : :
261 : : // Explain for conflict is correct as these proofs are generated and stored
262 : : // eagerly These will be safe for propagation later as well
263 : 1368989 : NodeBuilder nb(nodeManager(), Kind::AND);
264 : : // An open proof of eq from literals now in reason.
265 : 1368989 : auto pf = c->externalExplainByAssertions(nb);
266 [ - + ]: 1368989 : if (TraceIsOn("arith::cong::notzero"))
267 : : {
268 [ - - ]: 0 : Trace("arith::cong::notzero") << " original proof ";
269 [ - - ]: 0 : pf->printDebug(Trace("arith::cong::notzero"));
270 [ - - ]: 0 : Trace("arith::cong::notzero") << std::endl;
271 : : }
272 : 1368989 : Node reason = mkAndFromBuilder(nodeManager(), nb);
273 [ + + ]: 1368989 : if (isProofEnabled())
274 : : {
275 [ + + ]: 691009 : if (c->getType() == ConstraintType::Disequality)
276 : : {
277 : : // Note that the literal of c may differ from the negation of the watched
278 : : // equality, since multiple atoms may correspond to the same constraint,
279 : : // e.g. (= x 0) and (= (to_real x) 0.0). This is accounted for by the
280 : : // call below.
281 : : // We have to prove equivalence to the watched disequality.
282 : 144350 : pf = ensurePredTransform(d_pnm, pf, disEq);
283 : : }
284 : : else
285 : : {
286 [ + - ]: 1093318 : Trace("arith::cong::notzero")
287 : 546659 : << " proof modification needed" << std::endl;
288 : :
289 : : // Four cases:
290 : : // c has form x_i = d, d > 0 => multiply c by -1 in Farkas proof
291 : : // c has form x_i = d, d > 0 => multiply c by 1 in Farkas proof
292 : : // c has form x_i <= d, d < 0 => multiply c by 1 in Farkas proof
293 : : // c has form x_i >= d, d > 0 => multiply c by -1 in Farkas proof
294 : 546659 : const bool scaleCNegatively = c->getType() == ConstraintType::LowerBound
295 [ + + ][ + + ]: 572686 : || (c->getType() == ConstraintType::Equality
296 [ + + ]: 26027 : && c->getValue().sgn() > 0);
297 [ + + ]: 546659 : const int cSign = scaleCNegatively ? -1 : 1;
298 : 546659 : TNode isZero = d_watchedEqualities[s];
299 : 546659 : TypeNode type = isZero[0].getType();
300 : 546659 : const auto isZeroPf = d_pnm->mkAssume(isZero);
301 : 546659 : const auto nm = nodeManager();
302 : 2186636 : std::vector<std::shared_ptr<ProofNode>> pfs{isZeroPf, pf};
303 : : // Trick for getting correct, opposing signs.
304 : 0 : std::vector<Node> coeff{nm->mkConstInt(Rational(-1 * cSign)),
305 : 2733295 : nm->mkConstInt(Rational(cSign))};
306 : 546659 : std::vector<Node> coeffUse = getMacroSumUbCoeff(nm, pfs, coeff);
307 : : auto sumPf =
308 : 546659 : d_pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB, pfs, coeffUse);
309 : 546659 : Node fn = nm->mkConst(false);
310 : 546659 : const auto botPf = ensurePredTransform(d_pnm, sumPf, fn);
311 : 1639977 : std::vector<Node> assumption = {isZero};
312 : 546659 : pf = d_pnm->mkScope(botPf, assumption, false);
313 [ - + ]: 546659 : if (TraceIsOn("arith::cong::notzero"))
314 : : {
315 [ - - ]: 0 : Trace("arith::cong::notzero") << " new proof ";
316 [ - - ]: 0 : pf->printDebug(Trace("arith::cong::notzero"));
317 [ - - ]: 0 : Trace("arith::cong::notzero") << std::endl;
318 : : }
319 : 546659 : }
320 [ - + ][ - + ]: 691009 : Assert(pf->getResult() == disEq);
[ - - ]
321 : : }
322 : 1368989 : d_keepAlive.push_back(reason);
323 : 1368989 : assertionToEqualityEngine(false, s, reason, pf);
324 : 1368989 : }
325 : :
326 : 1370976 : bool ArithCongruenceManager::propagate(TNode x)
327 : : {
328 [ + - ]: 2741952 : Trace("arith::congruenceManager")
329 : 1370976 : << "ArithCongruenceManager::propagate(" << x << ")" << std::endl;
330 [ - + ]: 1370976 : if (inConflict())
331 : : {
332 : 0 : return true;
333 : : }
334 : :
335 : 1370976 : Node rewritten = rewrite(x);
336 : :
337 : : // Need to still propagate this!
338 [ + + ]: 1370976 : if (rewritten.getKind() == Kind::CONST_BOOLEAN)
339 : : {
340 : 3906 : pushBack(x);
341 : :
342 [ - + ]: 3906 : if (rewritten.getConst<bool>())
343 : : {
344 : 0 : return true;
345 : : }
346 : : else
347 : : {
348 : : // x rewrites to false.
349 : 3906 : ++(d_statistics.d_conflicts);
350 : 3906 : TrustNode trn = explainInternal(x);
351 : 3906 : Node conf = flattenAnd(trn.getNode());
352 [ + - ]: 7812 : Trace("arith::congruenceManager")
353 : 0 : << "rewritten to false " << x << " with explanation " << conf
354 : 3906 : << std::endl;
355 [ + + ]: 3906 : if (isProofEnabled())
356 : : {
357 : 1902 : auto pf = trn.getGenerator()->getProofFor(trn.getProven());
358 : 1902 : auto confPf = ensurePredTransform(d_pnm, pf, conf.negate());
359 : 1902 : raiseConflict(conf, confPf);
360 : 1902 : }
361 : : else
362 : : {
363 : 2004 : raiseConflict(conf);
364 : : }
365 : 3906 : return false;
366 : 3906 : }
367 : : }
368 : :
369 [ - + ][ - + ]: 1367070 : Assert(rewritten.getKind() != Kind::CONST_BOOLEAN);
[ - - ]
370 : :
371 : 1367070 : ConstraintP c = d_constraintDatabase.lookup(rewritten);
372 [ + + ]: 1367070 : if (c == NullConstraint)
373 : : {
374 : : // using setup as there may not be a corresponding congruence literal yet
375 : 43832 : d_setupLiteral(rewritten);
376 : 43832 : c = d_constraintDatabase.lookup(rewritten);
377 [ - + ][ - + ]: 43832 : Assert(c != NullConstraint);
[ - - ]
378 : : }
379 : :
380 [ + - ]: 2734140 : Trace("arith::congruenceManager")
381 : 0 : << "x is " << c->hasProof() << " " << (x == rewritten) << " "
382 : 1367070 : << c->canBePropagated() << " " << c->negationHasProof() << std::endl;
383 : :
384 [ + + ]: 1367070 : if (c->negationHasProof())
385 : : {
386 : 411 : TrustNode texpC = explainInternal(x);
387 : 411 : Node expC = texpC.getNode();
388 : 411 : ConstraintCP negC = c->getNegation();
389 : 822 : Node neg = Constraint::externalExplainByAssertions(nodeManager(), {negC});
390 : 411 : Node conf = expC.andNode(neg);
391 : 411 : Node finalPf = flattenAnd(conf);
392 : :
393 : 411 : ++(d_statistics.d_conflicts);
394 [ + + ]: 411 : if (isProofEnabled())
395 : : {
396 [ + - ]: 212 : Trace("arith-cm-proof") << "Handle conflict " << finalPf << std::endl;
397 : : // we have a proof of (=> C L1) and need a proof of
398 : : // (not (and C L2)), where L1 and L2 are contradictory literals,
399 : : // stored in proven[1] and neg respectively below.
400 : 212 : NodeManager* nm = nodeManager();
401 : 212 : std::vector<Node> conj(finalPf.begin(), finalPf.end());
402 : 424 : CDProof cdp(d_env);
403 : 212 : Node falsen = nm->mkConst(false);
404 : 212 : Node finalPfNeg = finalPf.notNode();
405 : 212 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
406 : 212 : cdp.addProof(texpC.toProofNode());
407 : 212 : Node proven = texpC.getProven();
408 [ + - ]: 212 : Trace("arith-cm-proof") << "Proven was " << proven << std::endl;
409 : 212 : Node antec = proven[0];
410 : 212 : std::vector<Node> antecc;
411 [ + - ]: 212 : if (antec.getKind() == Kind::AND)
412 : : {
413 : 212 : antecc.insert(antecc.end(), antec.begin(), antec.end());
414 : 212 : cdp.addStep(antec, ProofRule::AND_INTRO, antecc, {});
415 : : }
416 : : else
417 : : {
418 : 0 : antecc.push_back(antec);
419 : : }
420 [ + + ][ - - ]: 636 : cdp.addStep(proven[1], ProofRule::MODUS_PONENS, {antec, proven}, {});
421 : 212 : std::shared_ptr<ProofNode> pf;
422 : 212 : bool success = false;
423 [ + + ]: 286 : for (size_t i = 0; i < 2; i++)
424 : : {
425 [ + + ]: 249 : Node lit1 = i == 0 ? neg : proven[1];
426 [ + + ]: 249 : Node lit2 = i == 0 ? proven[1] : neg;
427 [ + - ]: 249 : Trace("arith-cm-proof") << "same " << lit1 << " " << lit2 << std::endl;
428 : 249 : Rational rx, ry;
429 : : // We are robust to cases where proven[1] and neg[0] are equivalent via
430 : : // arith poly norm here, where in most cases neg[0] is proven[1]
431 : 747 : if (lit1.getKind() == Kind::NOT
432 : 249 : && PolyNorm::isArithPolyNormRel(lit2, lit1[0], rx, ry))
433 : : {
434 [ + + ]: 175 : if (lit1[0] != lit2)
435 : : {
436 : 16 : Node eqa = lit2.eqNode(lit1[0]);
437 : : Node premise =
438 : 32 : PolyNorm::getArithPolyNormRelPremise(lit2, lit1[0], rx, ry);
439 : 32 : cdp.addStep(premise, ProofRule::ARITH_POLY_NORM, {}, {premise});
440 : 48 : cdp.addStep(eqa, ProofRule::ARITH_POLY_NORM_REL, {premise}, {eqa});
441 [ + + ][ - - ]: 48 : cdp.addStep(lit1[0], ProofRule::EQ_RESOLVE, {lit2, eqa}, {});
442 : 16 : }
443 : : // L1 and L2 are negation of one another, just use CONTRA
444 [ + + ][ - - ]: 525 : cdp.addStep(falsen, ProofRule::CONTRA, {lit1[0], lit1}, {});
445 : 175 : success = true;
446 : 175 : break;
447 : : }
448 [ + + ][ + + ]: 774 : }
[ + + ][ + + ]
449 [ - + ][ - + ]: 249 : if (!success && proven[1].getKind() == Kind::NOT
[ - - ]
450 : 249 : && proven[1][0].getKind() == Kind::EQUAL)
451 : : {
452 : : // The equality engine proved a disequality while arithmetic proved
453 : : // bounds implying the corresponding equality.
454 : 0 : Node peq = proven[1][0];
455 : 0 : Node triEq = peq;
456 : 0 : if (triEq[0].isConst() && !triEq[1].isConst())
457 : : {
458 : 0 : triEq = triEq[1].eqNode(triEq[0]);
459 : : }
460 : 0 : if (triEq[0].getKind() == Kind::TO_REAL && triEq[1].isConst()
461 : 0 : && triEq[1].getConst<Rational>().isIntegral())
462 : : {
463 : 0 : Node ic = nm->mkConstInt(triEq[1].getConst<Rational>());
464 : 0 : triEq = triEq[0][0].eqNode(ic);
465 : 0 : }
466 : 0 : else if (triEq[1].getKind() == Kind::TO_REAL && triEq[0].isConst()
467 : 0 : && triEq[0].getConst<Rational>().isIntegral())
468 : : {
469 : 0 : Node ic = nm->mkConstInt(triEq[0].getConst<Rational>());
470 : 0 : triEq = triEq[1][0].eqNode(ic);
471 : 0 : }
472 : 0 : if (triEq[0].getType().isRealOrInt() && triEq[1].getType().isRealOrInt()
473 : 0 : && CVC5_EQUAL(triEq[0].getType(), triEq[1].getType()))
474 : : {
475 : 0 : std::vector<Node> negc = andComponents(nm, neg);
476 : 0 : std::vector<Node> triChildren;
477 : : std::vector<Node> targets{nm->mkNode(Kind::GEQ, triEq[0], triEq[1]),
478 : 0 : nm->mkNode(Kind::LEQ, triEq[0], triEq[1])};
479 [ - - ]: 0 : for (const Node& target : targets)
480 : : {
481 : 0 : Node source;
482 [ - - ]: 0 : for (const Node& nc : negc)
483 : : {
484 [ - - ]: 0 : if (nc == target)
485 : : {
486 : 0 : source = nc;
487 : 0 : break;
488 : : }
489 : 0 : Node res = pc->checkDebug(
490 : 0 : ProofRule::MACRO_SR_PRED_TRANSFORM, {nc}, {target}, target);
491 [ - - ]: 0 : if (!res.isNull())
492 : : {
493 : 0 : source = nc;
494 : 0 : break;
495 : : }
496 [ - - ]: 0 : }
497 [ - - ]: 0 : if (source.isNull())
498 : : {
499 : 0 : triChildren.clear();
500 : 0 : break;
501 : : }
502 [ - - ]: 0 : if (source != target)
503 : : {
504 : 0 : cdp.addStep(target,
505 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
506 : : {source},
507 : : {target});
508 : : }
509 : 0 : triChildren.push_back(target);
510 [ - - ]: 0 : }
511 [ - - ]: 0 : if (triChildren.size() == 2)
512 : : {
513 : 0 : cdp.addStep(triEq, ProofRule::ARITH_TRICHOTOMY, triChildren, {});
514 [ - - ]: 0 : if (triEq != peq)
515 : : {
516 : 0 : Node res = pc->checkDebug(
517 : 0 : ProofRule::MACRO_SR_PRED_TRANSFORM, {triEq}, {peq}, peq);
518 [ - - ]: 0 : if (!res.isNull())
519 : : {
520 : 0 : cdp.addStep(
521 : : peq, ProofRule::MACRO_SR_PRED_TRANSFORM, {triEq}, {peq});
522 : : }
523 : 0 : }
524 : 0 : if (triEq == peq || cdp.hasStep(peq))
525 : : {
526 : 0 : cdp.addStep(falsen, ProofRule::CONTRA, {peq, proven[1]}, {});
527 : 0 : success = true;
528 : : }
529 : : }
530 : 0 : }
531 : 0 : }
532 [ + + ][ + - ]: 212 : if (!success && proven[1].getKind() == Kind::EQUAL)
[ + + ][ + + ]
[ - - ]
533 : : {
534 : : // otherwise typically proven[1] is of the form (= t c) or (= c t) where
535 : : // neg is the (negation of) a relation involving t.
536 : 74 : Node peq = proven[1][0].isConst() ? proven[1][1].eqNode(proven[1][0])
537 : 121 : : proven[1];
538 [ - + ][ - + ]: 37 : Assert(peq.getKind() == Kind::EQUAL);
[ - - ]
539 : : // Prefer the side that occurs in the contradictory literal.
540 : 37 : if (peq[0].getKind() == Kind::TO_REAL && !peq[1].isConst()
541 : 37 : && !ArithSubs::hasArithSubterm(neg, peq[0], false)
542 : 37 : && ArithSubs::hasArithSubterm(neg, peq[1], false))
543 : : {
544 : 0 : peq = peq[1].eqNode(peq[0]);
545 : : }
546 [ - + ]: 37 : if (peq[0].getKind() == Kind::TO_REAL)
547 : : {
548 : : // if we have (= (to_real t) c) where c is a rational, we do:
549 : : // -------------------------- ARITH_POLY_NORM_REL
550 : : // (= (to_real t) c) (= (= (to_real t) c) (= t c'))
551 : : // ------------------------------------------------- EQ_RESOLVE
552 : : // (= t c')
553 : : // where c' is integer equivalent of c.
554 : 0 : Assert(peq[1].isConst() && peq[1].getConst<Rational>().isIntegral());
555 : 0 : Node ic = nm->mkConstInt(peq[1].getConst<Rational>());
556 : 0 : Node peqi = peq[0][0].eqNode(ic);
557 : 0 : Node equiv = peq.eqNode(peqi);
558 : 0 : Rational cx, cy;
559 : : // Compute the coefficients relating the two sides. Note that
560 : : // ARITH_POLY_NORM_REL requires these to be non-zero.
561 : 0 : bool isPolyNorm = PolyNorm::isArithPolyNormRel(peq, peqi, cx, cy);
562 : 0 : Assert(isPolyNorm) << peq << " and " << peqi << " not poly norm";
563 : 0 : AlwaysAssert(isPolyNorm);
564 : : Node premise =
565 : 0 : PolyNorm::getArithPolyNormRelPremise(peq, peqi, cx, cy);
566 : 0 : cdp.addStep(premise, ProofRule::ARITH_POLY_NORM, {}, {premise});
567 : 0 : cdp.addStep(
568 : : equiv, ProofRule::ARITH_POLY_NORM_REL, {premise}, {equiv});
569 : 0 : cdp.addStep(peqi, ProofRule::EQ_RESOLVE, {peq, equiv}, {});
570 : 0 : peq = peqi;
571 : 0 : }
572 : : // We substitute t -> c within the arithmetic context of neg.
573 : : // In particular using an arithmetic context ensures that this rewrite
574 : : // should be locally handled as an ARITH_POLY_NORM step.
575 : : // Otherwise, we may require the full rewriter. For example:
576 : : // (= x f(x)) => (not (>= (+ x (* -1 f(x))) 0)) would otherwise fail if
577 : : // we applied at general substitution
578 : : // (not (>= (+ f(x) (* -1 f(f(x)))) 0)),
579 : : // whereas since x in f(x) is not in an arithmetic context, we want
580 : : // (not (>= (+ f(x) (* -1 f(x))) 0)).
581 : : // Furthermore note that we should not traverse non-linear
582 : : // multiplication here, as this inference was inferred via linear
583 : : // arithmetic which treats non-linear arithmetic as an abstraction.
584 : 37 : ArithSubsTermContext astc(false);
585 : : TConvProofGenerator tcnv(d_env,
586 : : nullptr,
587 : : TConvPolicy::FIXPOINT,
588 : : TConvCachePolicy::NEVER,
589 : : "ArithRConsTConv",
590 : 74 : &astc);
591 : 74 : Trace("arith-cm-proof") << "add step " << peq[0] << " -> " << peq[1]
592 : 37 : << ", rewrite " << neg << std::endl;
593 : 37 : tcnv.addRewriteStep(peq[0], peq[1], &cdp);
594 : 37 : std::shared_ptr<ProofNode> pfna = tcnv.getProofForRewriting(neg);
595 : 37 : Node negr = pfna->getResult()[1];
596 : 74 : Node res = pc->checkDebug(
597 : 148 : ProofRule::MACRO_SR_PRED_TRANSFORM, {negr}, {falsen}, falsen);
598 [ - + ][ - + ]: 37 : Assert(!res.isNull());
[ - - ]
599 [ + - ]: 37 : if (!res.isNull())
600 : : {
601 : 111 : cdp.addStep(
602 : : falsen, ProofRule::MACRO_SR_PRED_TRANSFORM, {negr}, {falsen});
603 : 37 : success = true;
604 [ + - ]: 37 : if (negr != neg)
605 : : {
606 : 37 : cdp.addProof(pfna);
607 [ + + ][ - - ]: 111 : cdp.addStep(
608 : : negr, ProofRule::EQ_RESOLVE, {neg, pfna->getResult()}, {});
609 : : }
610 : : }
611 : 37 : }
612 [ + - ]: 212 : if (success)
613 : : {
614 : 424 : cdp.addStep(finalPfNeg, ProofRule::SCOPE, {falsen}, conj);
615 : 212 : pf = cdp.getProofFor(finalPfNeg);
616 : : }
617 : 212 : Assert(pf != nullptr) << "Failed from " << neg << " " << proven[1];
618 : 212 : raiseConflict(finalPf, pf);
619 : 212 : }
620 : : else
621 : : {
622 : 199 : raiseConflict(finalPf);
623 : : }
624 [ + - ]: 822 : Trace("arith::congruenceManager")
625 : 411 : << "congruenceManager found a conflict " << finalPf << std::endl;
626 : 411 : return false;
627 : 411 : }
628 : :
629 : : // Cases for propagation
630 : : // C : c has a proof
631 : : // S : x == rewritten
632 : : // P : c can be propagated
633 : : //
634 : : // CSP
635 : : // 000 : propagate x, and mark C it as being explained
636 : : // 001 : propagate x, and propagate c after marking it as being explained
637 : : // 01* : propagate x, mark c but do not propagate c
638 : : // 10* : propagate x, do not mark c and do not propagate c
639 : : // 11* : drop the constraint, do not propagate x or c
640 : :
641 [ + + ][ + + ]: 1366659 : if (!c->hasProof() && x != rewritten)
[ + + ]
642 : : {
643 [ - + ]: 174693 : if (c->assertedToTheTheory())
644 : : {
645 : 0 : pushBack(x, rewritten, c->getWitness());
646 : : }
647 : : else
648 : : {
649 : 174693 : pushBack(x, rewritten);
650 : : }
651 : :
652 : 174693 : c->setEqualityEngineProof();
653 [ + + ][ + - ]: 174693 : if (c->canBePropagated() && !c->assertedToTheTheory())
[ + + ]
654 : : {
655 : : // Note that the propagation of c below is stated in terms of its
656 : : // literal, which may be distinct from rewritten. This is the case when
657 : : // several atoms correspond to c, in which case the first one that was
658 : : // set up is its literal, see Constraint::setLiteral. We thus ensure that
659 : : // the literal of c can be explained by this class as well, since
660 : : // otherwise we would explain it (trivially) by itself below, see
661 : : // Constraint::externalExplain.
662 : 24970 : pushBackAlias(c->getLiteral());
663 : 24970 : ++(d_statistics.d_propagateConstraints);
664 : 24970 : c->propagate();
665 : : }
666 : : }
667 [ + + ][ + - ]: 1191966 : else if (!c->hasProof() && x == rewritten)
[ + + ]
668 : : {
669 [ - + ]: 183193 : if (c->assertedToTheTheory())
670 : : {
671 : 0 : pushBack(x, c->getWitness());
672 : : }
673 : : else
674 : : {
675 : 183193 : pushBack(x);
676 : : }
677 : 183193 : c->setEqualityEngineProof();
678 : : }
679 [ + - ][ + + ]: 1008773 : else if (c->hasProof() && x != rewritten)
[ + + ]
680 : : {
681 [ + + ]: 645710 : if (c->assertedToTheTheory())
682 : : {
683 : 644449 : pushBack(x);
684 : : }
685 : : else
686 : : {
687 : 1261 : pushBack(x);
688 : : }
689 : : }
690 : : else
691 : : {
692 [ + - ][ + - ]: 363063 : Assert(c->hasProof() && x == rewritten);
[ - + ][ - + ]
[ - - ]
693 : : }
694 : 1366659 : return true;
695 : 1370976 : }
696 : :
697 : 24825 : TrustNode ArithCongruenceManager::explainInternal(TNode internal)
698 : : {
699 [ + + ]: 24825 : if (isProofEnabled())
700 : : {
701 : 11562 : return d_pfee->explain(internal);
702 : : }
703 : : // otherwise, explain without proof generator
704 : 13263 : Node exp = d_ee->mkExplainLit(internal);
705 : 13263 : return TrustNode::mkTrustPropExp(internal, exp, nullptr);
706 : 13263 : }
707 : :
708 : 20508 : TrustNode ArithCongruenceManager::explain(TNode external)
709 : : {
710 [ + - ]: 20508 : Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
711 : 20508 : Node internal = externalToInternal(external);
712 [ + - ]: 20508 : Trace("arith-ee") << "...internal = " << internal << std::endl;
713 : 20508 : TrustNode trn = explainInternal(internal);
714 : 20508 : if (isProofEnabled() && trn.getProven()[1] != external)
715 : : {
716 [ - + ][ - + ]: 544 : Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
[ - - ]
717 [ - + ][ - + ]: 544 : Assert(trn.getProven().getKind() == Kind::IMPLIES);
[ - - ]
718 [ - + ][ - + ]: 544 : Assert(trn.getGenerator() != nullptr);
[ - - ]
719 [ + - ]: 1088 : Trace("arith-ee") << "tweaking proof to prove " << external << " not "
720 : 544 : << trn.getProven()[1] << std::endl;
721 : 544 : std::vector<std::shared_ptr<ProofNode>> assumptionPfs;
722 : 1088 : std::vector<Node> assumptions = andComponents(nodeManager(), trn.getNode());
723 : 544 : assumptionPfs.push_back(trn.toProofNode());
724 [ + + ]: 1971 : for (const auto& a : assumptions)
725 : : {
726 : 1427 : assumptionPfs.push_back(
727 : 4281 : d_pnm->mkNode(ProofRule::TRUE_INTRO, {d_pnm->mkAssume(a)}, {}));
728 : : }
729 : : // uses substitution to true, which proves the internal form of the fact
730 : 544 : Node internalp = trn.getProven()[1];
731 : 544 : auto litPf = d_pnm->mkNode(ProofRule::MACRO_SR_PRED_TRANSFORM,
732 : : {assumptionPfs},
733 : : {internalp},
734 : 1632 : internalp);
735 : : // The internal and external forms may differ by more than rewriting, e.g.
736 : : // when external is an equality that is not in normal form, since the
737 : : // rewriter does not normalize equalities, see rewriter::normalizeEquality.
738 : : // We thus relate the two by polynomial normalization if necessary.
739 : 544 : litPf = ensurePredTransform(d_pnm, litPf, external);
740 : 1088 : auto extPf = d_pnm->mkScope(litPf, assumptions);
741 : 544 : return d_pfGenExplain->mkTrustedPropagation(external, trn.getNode(), extPf);
742 : 544 : }
743 : 19964 : return trn;
744 : 20508 : }
745 : :
746 : 136762 : void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y)
747 : : {
748 [ - + ][ - + ]: 136762 : Assert(!isWatchedVariable(s));
[ - - ]
749 : :
750 [ + - ]: 273524 : Trace("arith::congruenceManager")
751 : 136762 : << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
752 : :
753 : 136762 : ++(d_statistics.d_watchedVariables);
754 : :
755 : 136762 : d_watchedVariables.add(s);
756 : : // must ensure types are correct, thus, add TO_REAL if necessary here
757 : 273524 : std::pair<Node, Node> p = mkSameType(x, y);
758 : 136762 : Node eq = p.first.eqNode(p.second);
759 : 136762 : d_watchedEqualities.set(s, eq);
760 : 136762 : }
761 : :
762 : 3912024 : void ArithCongruenceManager::assertLitToEqualityEngine(
763 : : Node lit, TNode reason, std::shared_ptr<ProofNode> pf)
764 : : {
765 : 3912024 : bool isEquality = lit.getKind() != Kind::NOT;
766 [ + + ]: 3912024 : Node eq = isEquality ? lit : lit[0];
767 [ - + ][ - + ]: 3912024 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
768 : :
769 [ + - ]: 7824048 : Trace("arith-ee") << "Assert to Eq " << lit << ", reason " << reason
770 : 3912024 : << std::endl;
771 [ + + ]: 3912024 : if (isProofEnabled())
772 : : {
773 [ + + ]: 1781076 : if (CDProof::isSame(lit, reason))
774 : : {
775 [ + - ]: 625879 : Trace("arith-pfee") << "Asserting only, b/c implied by symm" << std::endl;
776 : : // The equality engine doesn't ref-count for us...
777 : 625879 : d_keepAlive.push_back(eq);
778 : 625879 : d_keepAlive.push_back(reason);
779 : 625879 : d_ee->assertEquality(eq, isEquality, reason);
780 : : }
781 [ + + ]: 1155197 : else if (hasProofFor(lit))
782 : : {
783 [ + - ]: 54798 : Trace("arith-pfee") << "Skipping b/c already done" << std::endl;
784 : : }
785 : : else
786 : : {
787 : 1100399 : setProofFor(lit, pf);
788 [ + - ]: 1100399 : Trace("arith-pfee") << "Actually asserting" << std::endl;
789 [ - + ]: 1100399 : if (TraceIsOn("arith-pfee"))
790 : : {
791 [ - - ]: 0 : Trace("arith-pfee") << "Proof: ";
792 [ - - ]: 0 : pf->printDebug(Trace("arith-pfee"));
793 [ - - ]: 0 : Trace("arith-pfee") << std::endl;
794 : : }
795 : : // The proof equality engine *does* ref-count for us...
796 [ + - ]: 1100399 : d_pfee->assertFact(lit, reason, d_pfGenEe.get());
797 : : }
798 : : }
799 : : else
800 : : {
801 : : // The equality engine doesn't ref-count for us...
802 : 2130948 : d_keepAlive.push_back(eq);
803 : 2130948 : d_keepAlive.push_back(reason);
804 : 2130948 : d_ee->assertEquality(eq, isEquality, reason);
805 : : }
806 : 3912024 : }
807 : :
808 : 2559467 : void ArithCongruenceManager::assertionToEqualityEngine(
809 : : bool isEquality, ArithVar s, TNode reason, std::shared_ptr<ProofNode> pf)
810 : : {
811 [ - + ][ - + ]: 2559467 : Assert(isWatchedVariable(s));
[ - - ]
812 : :
813 : 2559467 : TNode eq = d_watchedEqualities[s];
814 [ - + ][ - + ]: 2559467 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
815 : :
816 [ + + ]: 2559467 : Node lit = isEquality ? Node(eq) : eq.notNode();
817 [ + - ]: 5118934 : Trace("arith-ee") << "Assert to Eq " << eq << ", pol " << isEquality
818 : 2559467 : << ", reason " << reason << std::endl;
819 : 2559467 : assertLitToEqualityEngine(lit, reason, pf);
820 : 2559467 : }
821 : :
822 : 2255596 : bool ArithCongruenceManager::hasProofFor(TNode f) const
823 : : {
824 [ - + ][ - + ]: 2255596 : Assert(isProofEnabled());
[ - - ]
825 [ + + ]: 2255596 : if (d_pfGenEe->hasProofFor(f))
826 : : {
827 : 54798 : return true;
828 : : }
829 : 2200798 : Node sym = CDProof::getSymmFact(f);
830 [ - + ][ - + ]: 2200798 : Assert(!sym.isNull());
[ - - ]
831 : 2200798 : return d_pfGenEe->hasProofFor(sym);
832 : 2200798 : }
833 : :
834 : 1100399 : void ArithCongruenceManager::setProofFor(TNode f,
835 : : std::shared_ptr<ProofNode> pf) const
836 : : {
837 [ - + ][ - + ]: 1100399 : Assert(!hasProofFor(f));
[ - - ]
838 : 1100399 : d_pfGenEe->mkTrustNode(f, pf);
839 : 1100399 : Node symF = CDProof::getSymmFact(f);
840 : 4401596 : auto symPf = d_pnm->mkNode(ProofRule::SYMM, {pf}, {});
841 : 1100399 : d_pfGenEe->mkTrustNode(symF, symPf);
842 : 1100399 : }
843 : :
844 : 1047762 : void ArithCongruenceManager::equalsConstant(ConstraintCP c)
845 : : {
846 [ - + ][ - + ]: 1047762 : Assert(c->isEquality());
[ - - ]
847 : :
848 : 1047762 : ++(d_statistics.d_equalsConstantCalls);
849 [ + - ]: 1047762 : Trace("equalsConstant") << "equals constant " << c << std::endl;
850 : :
851 : 1047762 : ArithVar x = c->getVariable();
852 : 1047762 : Node xAsNode = d_avariables.asNode(x);
853 : 1047762 : NodeManager* nm = nodeManager();
854 : : Node asRational = nm->mkConstRealOrInt(
855 : 1047762 : xAsNode.getType(), c->getValue().getNoninfinitesimalPart());
856 : :
857 : : // No guarentee this is in normal form!
858 : : // Note though, that it happens to be in proof normal form!
859 : 1047762 : Node eq = xAsNode.eqNode(asRational);
860 : 1047762 : d_keepAlive.push_back(eq);
861 : :
862 : 1047762 : NodeBuilder nb(nodeManager(), Kind::AND);
863 : 1047762 : auto pf = c->externalExplainByAssertions(nb);
864 : 1047762 : Node reason = mkAndFromBuilder(nodeManager(), nb);
865 : 1047762 : d_keepAlive.push_back(reason);
866 : :
867 [ + - ]: 2095524 : Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason
868 : 1047762 : << std::endl;
869 : 1047762 : assertLitToEqualityEngine(eq, reason, pf);
870 : 1047762 : }
871 : :
872 : 304795 : void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub)
873 : : {
874 [ - + ][ - + ]: 304795 : Assert(lb->isLowerBound());
[ - - ]
875 [ - + ][ - + ]: 304795 : Assert(ub->isUpperBound());
[ - - ]
876 [ - + ][ - + ]: 304795 : Assert(lb->getVariable() == ub->getVariable());
[ - - ]
877 : :
878 : 304795 : ++(d_statistics.d_equalsConstantCalls);
879 [ + - ]: 609590 : Trace("equalsConstant") << "equals constant " << lb << std::endl
880 : 304795 : << ub << std::endl;
881 : :
882 : 304795 : ArithVar x = lb->getVariable();
883 : 304795 : NodeManager* nm = nodeManager();
884 : 304795 : NodeBuilder nb(nm, Kind::AND);
885 : 304795 : auto pfLb = lb->externalExplainByAssertions(nb);
886 : 304795 : auto pfUb = ub->externalExplainByAssertions(nb);
887 : 304795 : Node reason = mkAndFromBuilder(nodeManager(), nb);
888 : :
889 : 304795 : Node xAsNode = d_avariables.asNode(x);
890 : : Node asRational = nm->mkConstRealOrInt(
891 : 304795 : xAsNode.getType(), lb->getValue().getNoninfinitesimalPart());
892 : :
893 : : // No guarentee this is in normal form!
894 : : // Note though, that it happens to be in proof normal form!
895 : 304795 : Node eq = xAsNode.eqNode(asRational);
896 : 304795 : std::shared_ptr<ProofNode> pf;
897 [ + + ]: 304795 : if (isProofEnabled())
898 : : {
899 [ + + ][ - - ]: 416397 : pf = d_pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eq);
900 : : }
901 : 304795 : d_keepAlive.push_back(eq);
902 : 304795 : d_keepAlive.push_back(reason);
903 : :
904 [ + - ]: 609590 : Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason
905 : 304795 : << std::endl;
906 : :
907 : 304795 : assertLitToEqualityEngine(eq, reason, pf);
908 : 304795 : }
909 : :
910 : 9110242 : bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
911 : :
912 : : } // namespace arith::linear
913 : : } // namespace theory
914 : : } // namespace cvc5::internal
|
