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