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 : 429 : std::vector<Node> andComponents(NodeManager* nm, TNode an)
41 : : {
42 [ - + ]: 429 : if (an == nm->mkConst(true))
43 : : {
44 : 0 : return {};
45 : : }
46 [ - + ]: 429 : else if (an.getKind() != Kind::AND)
47 : : {
48 : 0 : return {an};
49 : : }
50 : 429 : std::vector<Node> a{};
51 : 429 : a.reserve(an.getNumChildren());
52 : 429 : a.insert(a.end(), an.begin(), an.end());
53 : 429 : return a;
54 : 429 : }
55 : :
56 : 50263 : ArithCongruenceManager::ArithCongruenceManager(
57 : : Env& env,
58 : : ConstraintDatabase& cd,
59 : : SetupLiteralCallBack setup,
60 : : const ArithVariables& avars,
61 : 50263 : RaiseEqualityEngineConflict raiseConflict)
62 : : : EnvObj(env),
63 : 50263 : d_inConflict(context()),
64 : 50263 : d_raiseConflict(raiseConflict),
65 : 50263 : d_keepAlive(context()),
66 : 50263 : d_propagatations(context()),
67 : 50263 : d_explanationMap(context()),
68 : 50263 : d_constraintDatabase(cd),
69 : 50263 : d_setupLiteral(setup),
70 : 50263 : d_avariables(avars),
71 : 50263 : d_ee(nullptr),
72 [ + + ]: 50263 : 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 : 100526 : d_pfGenEe(new EagerProofGenerator(
77 : 100526 : d_env, context(), "ArithCongruenceManager::pfGenEe")),
78 : : // Construct d_pfGenEe with the USER context, since its proofs are closed.
79 : 100526 : d_pfGenExplain(new EagerProofGenerator(
80 : 100526 : d_env, userContext(), "ArithCongruenceManager::pfGenExplain")),
81 : 50263 : d_pfee(nullptr),
82 : 150789 : d_statistics(statisticsRegistry())
83 : : {
84 : 50263 : }
85 : :
86 : 49918 : ArithCongruenceManager::~ArithCongruenceManager() {}
87 : :
88 : 50191 : void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
89 : : {
90 [ - + ][ - + ]: 50191 : Assert(ee != nullptr);
[ - - ]
91 : : // otherwise, we use the official one
92 : 50191 : d_ee = ee;
93 : : // the congruence kinds are already set up
94 : : // the proof equality engine is the one from the equality engine
95 : 50191 : d_pfee = d_ee->getProofEqualityEngine();
96 : : // have proof equality engine only if proofs are enabled
97 [ - + ][ - + ]: 50191 : Assert(isProofEnabled() == (d_pfee != nullptr));
[ - - ]
98 : 50191 : }
99 : :
100 : 50263 : ArithCongruenceManager::Statistics::Statistics(StatisticsRegistry& sr)
101 : : : d_watchedVariables(
102 : 50263 : sr.registerInt("theory::arith::congruence::watchedVariables")),
103 : : d_watchedVariableIsZero(
104 : 50263 : sr.registerInt("theory::arith::congruence::watchedVariableIsZero")),
105 : 50263 : d_watchedVariableIsNotZero(sr.registerInt(
106 : : "theory::arith::congruence::watchedVariableIsNotZero")),
107 : : d_equalsConstantCalls(
108 : 50263 : sr.registerInt("theory::arith::congruence::equalsConstantCalls")),
109 : 50263 : d_propagations(sr.registerInt("theory::arith::congruence::propagations")),
110 : : d_propagateConstraints(
111 : 50263 : sr.registerInt("theory::arith::congruence::propagateConstraints")),
112 : 50263 : d_conflicts(sr.registerInt("theory::arith::congruence::conflicts"))
113 : : {
114 : 50263 : }
115 : :
116 : 4200 : void ArithCongruenceManager::raiseConflict(Node conflict,
117 : : std::shared_ptr<ProofNode> pf)
118 : : {
119 [ - + ][ - + ]: 4200 : Assert(!inConflict());
[ - - ]
120 [ + - ]: 4200 : Trace("arith::conflict") << "difference manager conflict " << conflict << std::endl;
121 : 4200 : d_inConflict.raise();
122 : 4200 : d_raiseConflict.raiseEEConflict(conflict, pf);
123 : 4200 : }
124 : 1708261 : bool ArithCongruenceManager::inConflict() const{
125 : 1708261 : return d_inConflict.isRaised();
126 : : }
127 : :
128 : 8078477 : bool ArithCongruenceManager::hasMorePropagations() const {
129 : 8078477 : return !d_propagatations.empty();
130 : : }
131 : 1235771 : const Node ArithCongruenceManager::getNextPropagation() {
132 [ - + ][ - + ]: 1235771 : Assert(hasMorePropagations());
[ - - ]
133 : 1235771 : Node prop = d_propagatations.front();
134 : 1235771 : d_propagatations.dequeue();
135 : 1235771 : return prop;
136 : 0 : }
137 : :
138 : 107436 : bool ArithCongruenceManager::canExplain(TNode n) const {
139 : 107436 : return d_explanationMap.find(n) != d_explanationMap.end();
140 : : }
141 : :
142 : 37222 : Node ArithCongruenceManager::externalToInternal(TNode n) const{
143 [ - + ][ - + ]: 37222 : Assert(canExplain(n));
[ - - ]
144 : 37222 : ExplainMap::const_iterator iter = d_explanationMap.find(n);
145 : 37222 : size_t pos = (*iter).second;
146 : 74444 : return d_propagatations[pos];
147 : : }
148 : :
149 : 1082583 : void ArithCongruenceManager::pushBack(TNode n){
150 : 1082583 : d_explanationMap.insert(n, d_propagatations.size());
151 : 1082583 : d_propagatations.enqueue(n);
152 : :
153 : 1082583 : ++(d_statistics.d_propagations);
154 : 1082583 : }
155 : 211890 : void ArithCongruenceManager::pushBack(TNode n, TNode r){
156 : 211890 : d_explanationMap.insert(r, d_propagatations.size());
157 : 211890 : d_explanationMap.insert(n, d_propagatations.size());
158 : 211890 : d_propagatations.enqueue(n);
159 : :
160 : 211890 : ++(d_statistics.d_propagations);
161 : 211890 : }
162 : 0 : void ArithCongruenceManager::pushBack(TNode n, TNode r, TNode w){
163 : 0 : d_explanationMap.insert(w, d_propagatations.size());
164 : 0 : d_explanationMap.insert(r, d_propagatations.size());
165 : 0 : d_explanationMap.insert(n, d_propagatations.size());
166 : 0 : d_propagatations.enqueue(n);
167 : :
168 : 0 : ++(d_statistics.d_propagations);
169 : 0 : }
170 : :
171 : 701028 : void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub){
172 [ - + ][ - + ]: 701028 : Assert(lb->isLowerBound());
[ - - ]
173 [ - + ][ - + ]: 701028 : Assert(ub->isUpperBound());
[ - - ]
174 [ - + ][ - + ]: 701028 : Assert(lb->getVariable() == ub->getVariable());
[ - - ]
175 [ - + ][ - + ]: 701028 : Assert(lb->getValue().sgn() == 0);
[ - - ]
176 [ - + ][ - + ]: 701028 : Assert(ub->getValue().sgn() == 0);
[ - - ]
177 : :
178 : 701028 : ++(d_statistics.d_watchedVariableIsZero);
179 : :
180 : 701028 : ArithVar s = lb->getVariable();
181 : 701028 : TNode eq = d_watchedEqualities[s];
182 : 701028 : ConstraintCP eqC = d_constraintDatabase.getConstraint(
183 : : s, ConstraintType::Equality, lb->getValue());
184 : 701028 : NodeBuilder reasonBuilder(nodeManager(), Kind::AND);
185 : 701028 : auto pfLb = lb->externalExplainByAssertions(reasonBuilder);
186 : 701028 : auto pfUb = ub->externalExplainByAssertions(reasonBuilder);
187 : 701028 : Node reason = mkAndFromBuilder(nodeManager(), reasonBuilder);
188 : 701028 : std::shared_ptr<ProofNode> pf{};
189 [ + + ]: 701028 : if (isProofEnabled())
190 : : {
191 [ + + ][ - - ]: 1392324 : pf = d_pnm->mkNode(
192 : 1044243 : ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eqC->getProofLiteral());
193 : 348081 : pf = ensurePredTransform(d_pnm, pf, eq);
194 : : }
195 : :
196 : 701028 : d_keepAlive.push_back(reason);
197 [ + - ]: 1402056 : Trace("arith-ee") << "Asserting an equality on " << s << ", on trichotomy"
198 : 701028 : << std::endl;
199 [ + - ]: 701028 : Trace("arith-ee") << " based on " << lb << std::endl;
200 [ + - ]: 701028 : Trace("arith-ee") << " based on " << ub << std::endl;
201 : 701028 : assertionToEqualityEngine(true, s, reason, pf);
202 : 701028 : }
203 : :
204 : 519910 : void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
205 [ + - ]: 519910 : Trace("arith::cong") << "Cong::watchedVariableIsZero: " << *eq << std::endl;
206 : :
207 [ - + ][ - + ]: 519910 : Assert(eq->isEquality());
[ - - ]
208 [ - + ][ - + ]: 519910 : Assert(eq->getValue().sgn() == 0);
[ - - ]
209 : :
210 : 519910 : ++(d_statistics.d_watchedVariableIsZero);
211 : :
212 : 519910 : ArithVar s = eq->getVariable();
213 : :
214 : : //Explain for conflict is correct as these proofs are generated
215 : : //and stored eagerly
216 : : //These will be safe for propagation later as well
217 : 519910 : NodeBuilder nb(nodeManager(), Kind::AND);
218 : : // An open proof of eq from literals now in reason.
219 [ - + ]: 519910 : if (TraceIsOn("arith::cong"))
220 : : {
221 [ - - ]: 0 : eq->printProofTree(Trace("arith::cong"));
222 : : }
223 : 519910 : auto pf = eq->externalExplainByAssertions(nb);
224 [ + + ]: 519910 : if (isProofEnabled())
225 : : {
226 : 187109 : pf = ensurePredTransform(d_pnm, pf, d_watchedEqualities[s]);
227 : : }
228 : 519910 : Node reason = mkAndFromBuilder(nodeManager(), nb);
229 : :
230 : 519910 : d_keepAlive.push_back(reason);
231 : 519910 : assertionToEqualityEngine(true, s, reason, pf);
232 : 519910 : }
233 : :
234 : 1494178 : void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
235 [ + - ]: 2988356 : Trace("arith::cong::notzero")
236 : 1494178 : << "Cong::watchedVariableCannotBeZero " << *c << std::endl;
237 : 1494178 : ++(d_statistics.d_watchedVariableIsNotZero);
238 : :
239 : 1494178 : ArithVar s = c->getVariable();
240 : 1494178 : Node disEq = d_watchedEqualities[s].negate();
241 : :
242 : : //Explain for conflict is correct as these proofs are generated and stored eagerly
243 : : //These will be safe for propagation later as well
244 : 1494178 : NodeBuilder nb(nodeManager(), Kind::AND);
245 : : // An open proof of eq from literals now in reason.
246 : 1494178 : auto pf = c->externalExplainByAssertions(nb);
247 [ - + ]: 1494178 : if (TraceIsOn("arith::cong::notzero"))
248 : : {
249 [ - - ]: 0 : Trace("arith::cong::notzero") << " original proof ";
250 [ - - ]: 0 : pf->printDebug(Trace("arith::cong::notzero"));
251 [ - - ]: 0 : Trace("arith::cong::notzero") << std::endl;
252 : : }
253 : 1494178 : Node reason = mkAndFromBuilder(nodeManager(), nb);
254 [ + + ]: 1494178 : if (isProofEnabled())
255 : : {
256 [ + + ]: 673265 : if (c->getType() == ConstraintType::Disequality)
257 : : {
258 [ - + ][ - + ]: 156402 : Assert(c->getLiteral() == d_watchedEqualities[s].negate());
[ - - ]
259 : : // We have to prove equivalence to the watched disequality.
260 : 156402 : pf = ensurePredTransform(d_pnm, pf, disEq);
261 : : }
262 : : else
263 : : {
264 [ + - ]: 1033726 : Trace("arith::cong::notzero")
265 : 516863 : << " proof modification needed" << std::endl;
266 : :
267 : : // Four cases:
268 : : // c has form x_i = d, d > 0 => multiply c by -1 in Farkas proof
269 : : // c has form x_i = d, d > 0 => multiply c by 1 in Farkas proof
270 : : // c has form x_i <= d, d < 0 => multiply c by 1 in Farkas proof
271 : : // c has form x_i >= d, d > 0 => multiply c by -1 in Farkas proof
272 : 516863 : const bool scaleCNegatively = c->getType() == ConstraintType::LowerBound
273 [ + + ][ + + ]: 535035 : || (c->getType() == ConstraintType::Equality
274 [ + + ]: 18172 : && c->getValue().sgn() > 0);
275 [ + + ]: 516863 : const int cSign = scaleCNegatively ? -1 : 1;
276 : 516863 : TNode isZero = d_watchedEqualities[s];
277 : 516863 : TypeNode type = isZero[0].getType();
278 : 516863 : const auto isZeroPf = d_pnm->mkAssume(isZero);
279 : 516863 : const auto nm = nodeManager();
280 : 2067452 : std::vector<std::shared_ptr<ProofNode>> pfs{isZeroPf, pf};
281 : : // Trick for getting correct, opposing signs.
282 : 0 : std::vector<Node> coeff{nm->mkConstInt(Rational(-1 * cSign)),
283 : 2584315 : nm->mkConstInt(Rational(cSign))};
284 : 516863 : std::vector<Node> coeffUse = getMacroSumUbCoeff(nm, pfs, coeff);
285 : : auto sumPf =
286 : 516863 : d_pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB, pfs, coeffUse);
287 : 516863 : Node fn = nm->mkConst(false);
288 : 516863 : const auto botPf = ensurePredTransform(d_pnm, sumPf, fn);
289 : 1550589 : std::vector<Node> assumption = {isZero};
290 : 516863 : pf = d_pnm->mkScope(botPf, assumption, false);
291 [ - + ]: 516863 : if (TraceIsOn("arith::cong::notzero"))
292 : : {
293 [ - - ]: 0 : Trace("arith::cong::notzero") << " new proof ";
294 [ - - ]: 0 : pf->printDebug(Trace("arith::cong::notzero"));
295 [ - - ]: 0 : Trace("arith::cong::notzero") << std::endl;
296 : : }
297 : 516863 : }
298 [ - + ][ - + ]: 673265 : Assert(pf->getResult() == disEq);
[ - - ]
299 : : }
300 : 1494178 : d_keepAlive.push_back(reason);
301 : 1494178 : assertionToEqualityEngine(false, s, reason, pf);
302 : 1494178 : }
303 : :
304 : :
305 : 1704061 : bool ArithCongruenceManager::propagate(TNode x){
306 [ + - ]: 1704061 : Trace("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<<x<<")"<<std::endl;
307 [ - + ]: 1704061 : if(inConflict()){
308 : 0 : return true;
309 : : }
310 : :
311 : 1704061 : Node rewritten = rewrite(x);
312 : :
313 : : //Need to still propagate this!
314 [ + + ]: 1704061 : if (rewritten.getKind() == Kind::CONST_BOOLEAN)
315 : : {
316 : 3758 : pushBack(x);
317 : :
318 [ - + ]: 3758 : if(rewritten.getConst<bool>()){
319 : 0 : return true;
320 : : }else{
321 : : // x rewrites to false.
322 : 3758 : ++(d_statistics.d_conflicts);
323 : 3758 : TrustNode trn = explainInternal(x);
324 : 3758 : Node conf = flattenAnd(trn.getNode());
325 [ + - ]: 3758 : Trace("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
326 [ + + ]: 3758 : if (isProofEnabled())
327 : : {
328 : 1956 : auto pf = trn.getGenerator()->getProofFor(trn.getProven());
329 : 1956 : auto confPf = ensurePredTransform(d_pnm, pf, conf.negate());
330 : 1956 : raiseConflict(conf, confPf);
331 : 1956 : }
332 : : else
333 : : {
334 : 1802 : raiseConflict(conf);
335 : : }
336 : 3758 : return false;
337 : 3758 : }
338 : : }
339 : :
340 [ - + ][ - + ]: 1700303 : Assert(rewritten.getKind() != Kind::CONST_BOOLEAN);
[ - - ]
341 : :
342 : 1700303 : ConstraintP c = d_constraintDatabase.lookup(rewritten);
343 [ + + ]: 1700303 : if(c == NullConstraint){
344 : : //using setup as there may not be a corresponding congruence literal yet
345 : 41746 : d_setupLiteral(rewritten);
346 : 41746 : c = d_constraintDatabase.lookup(rewritten);
347 [ - + ][ - + ]: 41746 : Assert(c != NullConstraint);
[ - - ]
348 : : }
349 : :
350 [ + - ]: 3400606 : Trace("arith::congruenceManager")<< "x is "
351 : 0 : << c->hasProof() << " "
352 : 0 : << (x == rewritten) << " "
353 : 0 : << c->canBePropagated() << " "
354 : 1700303 : << c->negationHasProof() << std::endl;
355 : :
356 [ + + ]: 1700303 : if(c->negationHasProof()){
357 : 442 : TrustNode texpC = explainInternal(x);
358 : 442 : Node expC = texpC.getNode();
359 : 442 : ConstraintCP negC = c->getNegation();
360 : 884 : Node neg = Constraint::externalExplainByAssertions(nodeManager(), {negC});
361 : 442 : Node conf = expC.andNode(neg);
362 : 442 : Node finalPf = flattenAnd(conf);
363 : :
364 : 442 : ++(d_statistics.d_conflicts);
365 [ + + ]: 442 : if (isProofEnabled())
366 : : {
367 [ + - ]: 220 : Trace("arith-cm-proof") << "Handle conflict " << finalPf << std::endl;
368 : : // we have a proof of (=> C L1) and need a proof of
369 : : // (not (and C L2)), where L1 and L2 are contradictory literals,
370 : : // stored in proven[1] and neg respectively below.
371 : 220 : NodeManager* nm = nodeManager();
372 : 220 : std::vector<Node> conj(finalPf.begin(), finalPf.end());
373 : 440 : CDProof cdp(d_env);
374 : 220 : Node falsen = nm->mkConst(false);
375 : 220 : Node finalPfNeg = finalPf.notNode();
376 : 220 : cdp.addProof(texpC.toProofNode());
377 : 220 : Node proven = texpC.getProven();
378 [ + - ]: 220 : Trace("arith-cm-proof") << "Proven was " << proven << std::endl;
379 : 220 : Node antec = proven[0];
380 : 220 : std::vector<Node> antecc;
381 [ + - ]: 220 : if (antec.getKind() == Kind::AND)
382 : : {
383 : 220 : antecc.insert(antecc.end(), antec.begin(), antec.end());
384 : 220 : cdp.addStep(antec, ProofRule::AND_INTRO, antecc, {});
385 : : }
386 : : else
387 : : {
388 : 0 : antecc.push_back(antec);
389 : : }
390 [ + + ][ - - ]: 660 : cdp.addStep(proven[1], ProofRule::MODUS_PONENS, {antec, proven}, {});
391 : 220 : std::shared_ptr<ProofNode> pf;
392 : 220 : bool success = false;
393 [ + + ]: 296 : for (size_t i = 0; i < 2; i++)
394 : : {
395 [ + + ]: 259 : Node lit1 = i == 0 ? neg : proven[1];
396 [ + + ]: 259 : Node lit2 = i == 0 ? proven[1] : neg;
397 [ + - ]: 259 : Trace("arith-cm-proof") << "same " << lit1 << " " << lit2 << std::endl;
398 : 259 : Rational rx, ry;
399 : : // We are robust to cases where proven[1] and neg[0] are equivalent via
400 : : // arith poly norm here, where in most cases neg[0] is proven[1]
401 : 777 : if (lit1.getKind() == Kind::NOT
402 : 259 : && PolyNorm::isArithPolyNormRel(lit2, lit1[0], rx, ry))
403 : : {
404 [ + + ]: 183 : if (lit1[0] != lit2)
405 : : {
406 : 38 : Node eqa = lit2.eqNode(lit1[0]);
407 : : Node premise =
408 : 76 : PolyNorm::getArithPolyNormRelPremise(lit2, lit1[0], rx, ry);
409 : 76 : cdp.addStep(premise, ProofRule::ARITH_POLY_NORM, {}, {premise});
410 : 114 : cdp.addStep(eqa, ProofRule::ARITH_POLY_NORM_REL, {premise}, {eqa});
411 [ + + ][ - - ]: 114 : cdp.addStep(lit1[0], ProofRule::EQ_RESOLVE, {lit2, eqa}, {});
412 : 38 : }
413 : : // L1 and L2 are negation of one another, just use CONTRA
414 [ + + ][ - - ]: 549 : cdp.addStep(falsen, ProofRule::CONTRA, {lit1[0], lit1}, {});
415 : 183 : success = true;
416 : 183 : break;
417 : : }
418 [ + + ][ + + ]: 808 : }
[ + + ][ + + ]
419 [ + + ][ + - ]: 220 : if (!success && proven[1].getKind() == Kind::EQUAL)
[ + + ][ + + ]
[ - - ]
420 : : {
421 : : // otherwise typically proven[1] is of the form (= t c) or (= c t) where
422 : : // neg is the (negation of) a relation involving t.
423 : 74 : Node peq = proven[1][0].isConst() ? proven[1][1].eqNode(proven[1][0])
424 : 89 : : proven[1];
425 [ - + ][ - + ]: 37 : Assert (peq.getKind()==Kind::EQUAL);
[ - - ]
426 [ + + ]: 37 : if (peq[0].getKind()==Kind::TO_REAL)
427 : : {
428 : : // if we have (= (to_real t) c) where c is a rational, we do:
429 : : // -------------------------- ARITH_POLY_NORM_REL
430 : : // (= (to_real t) c) (= (= (to_real t) c) (= t c'))
431 : : // ------------------------------------------------- EQ_RESOLVE
432 : : // (= t c')
433 : : // where c' is integer equivalent of c.
434 : 4 : Assert (peq[1].isConst() && peq[1].getConst<Rational>().isIntegral());
435 : 4 : Node ic = nm->mkConstInt(peq[1].getConst<Rational>());
436 : 8 : Node peqi = peq[0][0].eqNode(ic);
437 : 4 : Node equiv = peq.eqNode(peqi);
438 : 4 : Rational cx, cy;
439 : 8 : Node premise = PolyNorm::getArithPolyNormRelPremise(peq, peqi, cx, cy);
440 : 8 : cdp.addStep(premise, ProofRule::ARITH_POLY_NORM, {}, {premise});
441 : 12 : cdp.addStep(equiv, ProofRule::ARITH_POLY_NORM_REL, {premise}, {equiv});
442 [ + + ][ - - ]: 12 : cdp.addStep(peqi, ProofRule::EQ_RESOLVE, {peq, equiv}, {});
443 : 4 : peq = peqi;
444 : 4 : }
445 : 37 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
446 : : // We substitute t -> c within the arithmetic context of neg.
447 : : // In particular using an arithmetic context ensures that this rewrite
448 : : // should be locally handled as an ARITH_POLY_NORM step.
449 : : // Otherwise, we may require the full rewriter. For example:
450 : : // (= x f(x)) => (not (>= (+ x (* -1 f(x))) 0)) would otherwise fail if
451 : : // we applied at general substitution
452 : : // (not (>= (+ f(x) (* -1 f(f(x)))) 0)),
453 : : // whereas since x in f(x) is not in an arithmetic context, we want
454 : : // (not (>= (+ f(x) (* -1 f(x))) 0)).
455 : : // Furthermore note that we should not traverse non-linear
456 : : // multiplication here, as this inference was inferred via linear
457 : : // arithmetic which treats non-linear arithmetic as an abstraction.
458 : 37 : ArithSubsTermContext astc(false);
459 : : TConvProofGenerator tcnv(d_env,
460 : : nullptr,
461 : : TConvPolicy::FIXPOINT,
462 : : TConvCachePolicy::NEVER,
463 : : "ArithRConsTConv",
464 : 74 : &astc);
465 : 74 : Trace("arith-cm-proof") << "add step " << peq[0] << " -> " << peq[1]
466 : 37 : << ", rewrite " << neg << std::endl;
467 : 37 : tcnv.addRewriteStep(peq[0], peq[1], &cdp);
468 : 37 : std::shared_ptr<ProofNode> pfna = tcnv.getProofForRewriting(neg);
469 : 37 : Node negr = pfna->getResult()[1];
470 : 74 : Node res = pc->checkDebug(
471 : 148 : ProofRule::MACRO_SR_PRED_TRANSFORM, {negr}, {falsen}, falsen);
472 [ - + ][ - + ]: 37 : Assert(!res.isNull());
[ - - ]
473 [ + - ]: 37 : if (!res.isNull())
474 : : {
475 : 111 : cdp.addStep(
476 : : falsen, ProofRule::MACRO_SR_PRED_TRANSFORM, {negr}, {falsen});
477 : 37 : success = true;
478 [ + - ]: 37 : if (negr != neg)
479 : : {
480 : 37 : cdp.addProof(pfna);
481 [ + + ][ - - ]: 111 : cdp.addStep(
482 : : negr, ProofRule::EQ_RESOLVE, {neg, pfna->getResult()}, {});
483 : : }
484 : : }
485 : 37 : }
486 [ + - ]: 220 : if (success)
487 : : {
488 : 440 : cdp.addStep(finalPfNeg, ProofRule::SCOPE, {falsen}, conj);
489 : 220 : pf = cdp.getProofFor(finalPfNeg);
490 : : }
491 : 220 : Assert(pf != nullptr) << "Failed from " << neg << " " << proven[1];
492 : 220 : raiseConflict(finalPf, pf);
493 : 220 : }
494 : : else
495 : : {
496 : 222 : raiseConflict(finalPf);
497 : : }
498 [ + - ]: 884 : Trace("arith::congruenceManager")
499 : 442 : << "congruenceManager found a conflict " << finalPf << std::endl;
500 : 442 : return false;
501 : 442 : }
502 : :
503 : : // Cases for propagation
504 : : // C : c has a proof
505 : : // S : x == rewritten
506 : : // P : c can be propagated
507 : : //
508 : : // CSP
509 : : // 000 : propagate x, and mark C it as being explained
510 : : // 001 : propagate x, and propagate c after marking it as being explained
511 : : // 01* : propagate x, mark c but do not propagate c
512 : : // 10* : propagate x, do not mark c and do not propagate c
513 : : // 11* : drop the constraint, do not propagate x or c
514 : :
515 [ + + ][ + + ]: 1699861 : if(!c->hasProof() && x != rewritten){
[ + + ]
516 [ - + ]: 211890 : if(c->assertedToTheTheory()){
517 : 0 : pushBack(x, rewritten, c->getWitness());
518 : : }else{
519 : 211890 : pushBack(x, rewritten);
520 : : }
521 : :
522 : 211890 : c->setEqualityEngineProof();
523 [ + + ][ + - ]: 211890 : if(c->canBePropagated() && !c->assertedToTheTheory()){
[ + + ]
524 : :
525 : 33343 : ++(d_statistics.d_propagateConstraints);
526 : 33343 : c->propagate();
527 : : }
528 [ + + ][ + - ]: 1487971 : }else if(!c->hasProof() && x == rewritten){
[ + + ]
529 [ - + ]: 165674 : if(c->assertedToTheTheory()){
530 : 0 : pushBack(x, c->getWitness());
531 : : }else{
532 : 165674 : pushBack(x);
533 : : }
534 : 165674 : c->setEqualityEngineProof();
535 [ + - ][ + + ]: 1322297 : }else if(c->hasProof() && x != rewritten){
[ + + ]
536 [ + + ]: 913151 : if(c->assertedToTheTheory()){
537 : 911483 : pushBack(x);
538 : : }else{
539 : 1668 : pushBack(x);
540 : : }
541 : : }else{
542 [ + - ][ + - ]: 409146 : Assert(c->hasProof() && x == rewritten);
[ - + ][ - + ]
[ - - ]
543 : : }
544 : 1699861 : return true;
545 : 1704061 : }
546 : :
547 : 41422 : TrustNode ArithCongruenceManager::explainInternal(TNode internal)
548 : : {
549 [ + + ]: 41422 : if (isProofEnabled())
550 : : {
551 : 20471 : return d_pfee->explain(internal);
552 : : }
553 : : // otherwise, explain without proof generator
554 : 20951 : Node exp = d_ee->mkExplainLit(internal);
555 : 20951 : return TrustNode::mkTrustPropExp(internal, exp, nullptr);
556 : 20951 : }
557 : :
558 : 37222 : TrustNode ArithCongruenceManager::explain(TNode external)
559 : : {
560 [ + - ]: 37222 : Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
561 : 37222 : Node internal = externalToInternal(external);
562 [ + - ]: 37222 : Trace("arith-ee") << "...internal = " << internal << std::endl;
563 : 37222 : TrustNode trn = explainInternal(internal);
564 : 37222 : if (isProofEnabled() && trn.getProven()[1] != external)
565 : : {
566 [ - + ][ - + ]: 429 : Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
[ - - ]
567 [ - + ][ - + ]: 429 : Assert(trn.getProven().getKind() == Kind::IMPLIES);
[ - - ]
568 [ - + ][ - + ]: 429 : Assert(trn.getGenerator() != nullptr);
[ - - ]
569 [ + - ]: 858 : Trace("arith-ee") << "tweaking proof to prove " << external << " not "
570 : 429 : << trn.getProven()[1] << std::endl;
571 : 429 : std::vector<std::shared_ptr<ProofNode>> assumptionPfs;
572 : 858 : std::vector<Node> assumptions = andComponents(nodeManager(), trn.getNode());
573 : 429 : assumptionPfs.push_back(trn.toProofNode());
574 [ + + ]: 1504 : for (const auto& a : assumptions)
575 : : {
576 : 1075 : assumptionPfs.push_back(
577 : 3225 : d_pnm->mkNode(ProofRule::TRUE_INTRO, {d_pnm->mkAssume(a)}, {}));
578 : : }
579 : : // uses substitution to true
580 : 429 : auto litPf = d_pnm->mkNode(ProofRule::MACRO_SR_PRED_TRANSFORM,
581 : : {assumptionPfs},
582 : : {external},
583 : 1287 : external);
584 : 858 : auto extPf = d_pnm->mkScope(litPf, assumptions);
585 : 429 : return d_pfGenExplain->mkTrustedPropagation(external, trn.getNode(), extPf);
586 : 429 : }
587 : 36793 : return trn;
588 : 37222 : }
589 : :
590 : 136734 : void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
591 [ - + ][ - + ]: 136734 : Assert(!isWatchedVariable(s));
[ - - ]
592 : :
593 [ + - ]: 273468 : Trace("arith::congruenceManager")
594 : 136734 : << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
595 : :
596 : :
597 : 136734 : ++(d_statistics.d_watchedVariables);
598 : :
599 : 136734 : d_watchedVariables.add(s);
600 : : // must ensure types are correct, thus, add TO_REAL if necessary here
601 : 273468 : std::pair<Node, Node> p = mkSameType(x, y);
602 : 136734 : Node eq = p.first.eqNode(p.second);
603 : 136734 : d_watchedEqualities.set(s, eq);
604 : 136734 : }
605 : :
606 : 4365734 : void ArithCongruenceManager::assertLitToEqualityEngine(
607 : : Node lit, TNode reason, std::shared_ptr<ProofNode> pf)
608 : : {
609 : 4365734 : bool isEquality = lit.getKind() != Kind::NOT;
610 [ + + ]: 4365734 : Node eq = isEquality ? lit : lit[0];
611 [ - + ][ - + ]: 4365734 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
612 : :
613 [ + - ]: 8731468 : Trace("arith-ee") << "Assert to Eq " << lit << ", reason " << reason
614 : 4365734 : << std::endl;
615 [ + + ]: 4365734 : if (isProofEnabled())
616 : : {
617 [ + + ]: 1816351 : if (CDProof::isSame(lit, reason))
618 : : {
619 [ + - ]: 729478 : Trace("arith-pfee") << "Asserting only, b/c implied by symm" << std::endl;
620 : : // The equality engine doesn't ref-count for us...
621 : 729478 : d_keepAlive.push_back(eq);
622 : 729478 : d_keepAlive.push_back(reason);
623 : 729478 : d_ee->assertEquality(eq, isEquality, reason);
624 : : }
625 [ + + ]: 1086873 : else if (hasProofFor(lit))
626 : : {
627 [ + - ]: 30356 : Trace("arith-pfee") << "Skipping b/c already done" << std::endl;
628 : : }
629 : : else
630 : : {
631 : 1056517 : setProofFor(lit, pf);
632 [ + - ]: 1056517 : Trace("arith-pfee") << "Actually asserting" << std::endl;
633 [ - + ]: 1056517 : if (TraceIsOn("arith-pfee"))
634 : : {
635 [ - - ]: 0 : Trace("arith-pfee") << "Proof: ";
636 [ - - ]: 0 : pf->printDebug(Trace("arith-pfee"));
637 [ - - ]: 0 : Trace("arith-pfee") << std::endl;
638 : : }
639 : : // The proof equality engine *does* ref-count for us...
640 [ + - ]: 1056517 : d_pfee->assertFact(lit, reason, d_pfGenEe.get());
641 : : }
642 : : }
643 : : else
644 : : {
645 : : // The equality engine doesn't ref-count for us...
646 : 2549383 : d_keepAlive.push_back(eq);
647 : 2549383 : d_keepAlive.push_back(reason);
648 : 2549383 : d_ee->assertEquality(eq, isEquality, reason);
649 : : }
650 : 4365734 : }
651 : :
652 : 2715116 : void ArithCongruenceManager::assertionToEqualityEngine(
653 : : bool isEquality, ArithVar s, TNode reason, std::shared_ptr<ProofNode> pf)
654 : : {
655 [ - + ][ - + ]: 2715116 : Assert(isWatchedVariable(s));
[ - - ]
656 : :
657 : 2715116 : TNode eq = d_watchedEqualities[s];
658 [ - + ][ - + ]: 2715116 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
659 : :
660 [ + + ]: 2715116 : Node lit = isEquality ? Node(eq) : eq.notNode();
661 [ + - ]: 5430232 : Trace("arith-ee") << "Assert to Eq " << eq << ", pol " << isEquality
662 : 2715116 : << ", reason " << reason << std::endl;
663 : 2715116 : assertLitToEqualityEngine(lit, reason, pf);
664 : 2715116 : }
665 : :
666 : 2143390 : bool ArithCongruenceManager::hasProofFor(TNode f) const
667 : : {
668 [ - + ][ - + ]: 2143390 : Assert(isProofEnabled());
[ - - ]
669 [ + + ]: 2143390 : if (d_pfGenEe->hasProofFor(f))
670 : : {
671 : 30356 : return true;
672 : : }
673 : 2113034 : Node sym = CDProof::getSymmFact(f);
674 [ - + ][ - + ]: 2113034 : Assert(!sym.isNull());
[ - - ]
675 : 2113034 : return d_pfGenEe->hasProofFor(sym);
676 : 2113034 : }
677 : :
678 : 1056517 : void ArithCongruenceManager::setProofFor(TNode f,
679 : : std::shared_ptr<ProofNode> pf) const
680 : : {
681 [ - + ][ - + ]: 1056517 : Assert(!hasProofFor(f));
[ - - ]
682 : 1056517 : d_pfGenEe->mkTrustNode(f, pf);
683 : 1056517 : Node symF = CDProof::getSymmFact(f);
684 : 4226068 : auto symPf = d_pnm->mkNode(ProofRule::SYMM, {pf}, {});
685 : 1056517 : d_pfGenEe->mkTrustNode(symF, symPf);
686 : 1056517 : }
687 : :
688 : 1316479 : void ArithCongruenceManager::equalsConstant(ConstraintCP c){
689 [ - + ][ - + ]: 1316479 : Assert(c->isEquality());
[ - - ]
690 : :
691 : 1316479 : ++(d_statistics.d_equalsConstantCalls);
692 [ + - ]: 1316479 : Trace("equalsConstant") << "equals constant " << c << std::endl;
693 : :
694 : 1316479 : ArithVar x = c->getVariable();
695 : 1316479 : Node xAsNode = d_avariables.asNode(x);
696 : 1316479 : NodeManager* nm = nodeManager();
697 : : Node asRational = nm->mkConstRealOrInt(
698 : 1316479 : xAsNode.getType(), c->getValue().getNoninfinitesimalPart());
699 : :
700 : : // No guarentee this is in normal form!
701 : : // Note though, that it happens to be in proof normal form!
702 : 1316479 : Node eq = xAsNode.eqNode(asRational);
703 : 1316479 : d_keepAlive.push_back(eq);
704 : :
705 : 1316479 : NodeBuilder nb(nodeManager(), Kind::AND);
706 : 1316479 : auto pf = c->externalExplainByAssertions(nb);
707 : 1316479 : Node reason = mkAndFromBuilder(nodeManager(), nb);
708 : 1316479 : d_keepAlive.push_back(reason);
709 : :
710 [ + - ]: 1316479 : Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
711 : 1316479 : assertLitToEqualityEngine(eq, reason, pf);
712 : 1316479 : }
713 : :
714 : 334139 : void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
715 [ - + ][ - + ]: 334139 : Assert(lb->isLowerBound());
[ - - ]
716 [ - + ][ - + ]: 334139 : Assert(ub->isUpperBound());
[ - - ]
717 [ - + ][ - + ]: 334139 : Assert(lb->getVariable() == ub->getVariable());
[ - - ]
718 : :
719 : 334139 : ++(d_statistics.d_equalsConstantCalls);
720 [ + - ]: 668278 : Trace("equalsConstant") << "equals constant " << lb << std::endl
721 : 334139 : << ub << std::endl;
722 : :
723 : 334139 : ArithVar x = lb->getVariable();
724 : 334139 : NodeManager* nm = nodeManager();
725 : 334139 : NodeBuilder nb(nm, Kind::AND);
726 : 334139 : auto pfLb = lb->externalExplainByAssertions(nb);
727 : 334139 : auto pfUb = ub->externalExplainByAssertions(nb);
728 : 334139 : Node reason = mkAndFromBuilder(nodeManager(), nb);
729 : :
730 : 334139 : Node xAsNode = d_avariables.asNode(x);
731 : : Node asRational = nm->mkConstRealOrInt(
732 : 334139 : xAsNode.getType(), lb->getValue().getNoninfinitesimalPart());
733 : :
734 : : // No guarentee this is in normal form!
735 : : // Note though, that it happens to be in proof normal form!
736 : 334139 : Node eq = xAsNode.eqNode(asRational);
737 : 334139 : std::shared_ptr<ProofNode> pf;
738 [ + + ]: 334139 : if (isProofEnabled())
739 : : {
740 [ + + ][ - - ]: 441435 : pf = d_pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eq);
741 : : }
742 : 334139 : d_keepAlive.push_back(eq);
743 : 334139 : d_keepAlive.push_back(reason);
744 : :
745 [ + - ]: 334139 : Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
746 : :
747 : 334139 : assertLitToEqualityEngine(eq, reason, pf);
748 : 334139 : }
749 : :
750 : 9691414 : bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
751 : :
752 : : } // namespace arith
753 : : } // namespace theory
754 : : } // namespace cvc5::internal
|
