GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/congruence_manager.cpp Lines: 358 404 88.6 %
Date: 2021-03-22 Branches: 729 1912 38.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file congruence_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Alex Ozdemir, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/arith/congruence_manager.h"
19
20
#include "base/output.h"
21
#include "expr/proof_node.h"
22
#include "expr/proof_node_manager.h"
23
#include "smt/smt_statistics_registry.h"
24
#include "theory/arith/arith_utilities.h"
25
#include "theory/arith/constraint.h"
26
#include "theory/arith/partial_model.h"
27
#include "theory/ee_setup_info.h"
28
#include "theory/rewriter.h"
29
#include "theory/uf/equality_engine.h"
30
#include "theory/uf/proof_equality_engine.h"
31
#include "options/arith_options.h"
32
33
namespace CVC4 {
34
namespace theory {
35
namespace arith {
36
37
8995
ArithCongruenceManager::ArithCongruenceManager(
38
    context::Context* c,
39
    context::UserContext* u,
40
    ConstraintDatabase& cd,
41
    SetupLiteralCallBack setup,
42
    const ArithVariables& avars,
43
    RaiseEqualityEngineConflict raiseConflict,
44
8995
    ProofNodeManager* pnm)
45
    : d_inConflict(c),
46
      d_raiseConflict(raiseConflict),
47
      d_notify(*this),
48
      d_keepAlive(c),
49
      d_propagatations(c),
50
      d_explanationMap(c),
51
      d_constraintDatabase(cd),
52
      d_setupLiteral(setup),
53
      d_avariables(avars),
54
      d_ee(nullptr),
55
      d_satContext(c),
56
      d_userContext(u),
57
      d_pnm(pnm),
58
      // Construct d_pfGenEe with the SAT context, since its proof include
59
      // unclosed assumptions of theory literals.
60
      d_pfGenEe(
61
8995
          new EagerProofGenerator(pnm, c, "ArithCongruenceManager::pfGenEe")),
62
      // Construct d_pfGenEe with the USER context, since its proofs are closed.
63
      d_pfGenExplain(new EagerProofGenerator(
64
8995
          pnm, u, "ArithCongruenceManager::pfGenExplain")),
65
26985
      d_pfee(nullptr)
66
{
67
8995
}
68
69
8992
ArithCongruenceManager::~ArithCongruenceManager() {}
70
71
8995
bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi)
72
{
73
8995
  esi.d_notify = &d_notify;
74
8995
  esi.d_name = "theory::arith::ArithCongruenceManager";
75
8995
  return true;
76
}
77
78
8995
void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee,
79
                                        eq::ProofEqEngine* pfee)
80
{
81
8995
  Assert(ee != nullptr);
82
8995
  d_ee = ee;
83
8995
  d_ee->addFunctionKind(kind::NONLINEAR_MULT);
84
8995
  d_ee->addFunctionKind(kind::EXPONENTIAL);
85
8995
  d_ee->addFunctionKind(kind::SINE);
86
8995
  d_ee->addFunctionKind(kind::IAND);
87
  // have proof equality engine only if proofs are enabled
88
8995
  Assert(isProofEnabled() == (pfee != nullptr));
89
8995
  d_pfee = pfee;
90
8995
}
91
92
8995
ArithCongruenceManager::Statistics::Statistics():
93
  d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
94
  d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
95
  d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
96
  d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
97
  d_propagations("theory::arith::congruence::propagations", 0),
98
  d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
99
8995
  d_conflicts("theory::arith::congruence::conflicts", 0)
100
{
101
8995
  smtStatisticsRegistry()->registerStat(&d_watchedVariables);
102
8995
  smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero);
103
8995
  smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero);
104
8995
  smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls);
105
8995
  smtStatisticsRegistry()->registerStat(&d_propagations);
106
8995
  smtStatisticsRegistry()->registerStat(&d_propagateConstraints);
107
8995
  smtStatisticsRegistry()->registerStat(&d_conflicts);
108
8995
}
109
110
17984
ArithCongruenceManager::Statistics::~Statistics(){
111
8992
  smtStatisticsRegistry()->unregisterStat(&d_watchedVariables);
112
8992
  smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero);
113
8992
  smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero);
114
8992
  smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls);
115
8992
  smtStatisticsRegistry()->unregisterStat(&d_propagations);
116
8992
  smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints);
117
8992
  smtStatisticsRegistry()->unregisterStat(&d_conflicts);
118
8992
}
119
120
8995
ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
121
8995
  : d_acm(acm)
122
8995
{}
123
124
bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerPredicate(
125
    TNode predicate, bool value)
126
{
127
  Assert(predicate.getKind() == kind::EQUAL);
128
  Debug("arith::congruences")
129
      << "ArithCongruenceNotify::eqNotifyTriggerPredicate(" << predicate << ", "
130
      << (value ? "true" : "false") << ")" << std::endl;
131
  if (value) {
132
    return d_acm.propagate(predicate);
133
  }
134
  return d_acm.propagate(predicate.notNode());
135
}
136
137
843243
bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
138
843243
  Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
139
843243
  if (value) {
140
718215
    return d_acm.propagate(t1.eqNode(t2));
141
  } else {
142
125028
    return d_acm.propagate(t1.eqNode(t2).notNode());
143
  }
144
}
145
2235
void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
146
2235
  Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
147
2235
  d_acm.propagate(t1.eqNode(t2));
148
2235
}
149
1509123
void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
150
1509123
}
151
1544184
void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyMerge(TNode t1,
152
                                                                  TNode t2)
153
{
154
1544184
}
155
282995
void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
156
282995
}
157
158
2388
void ArithCongruenceManager::raiseConflict(Node conflict,
159
                                           std::shared_ptr<ProofNode> pf)
160
{
161
2388
  Assert(!inConflict());
162
2388
  Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
163
2388
  d_inConflict.raise();
164
2388
  d_raiseConflict.raiseEEConflict(conflict, pf);
165
2388
}
166
847866
bool ArithCongruenceManager::inConflict() const{
167
847866
  return d_inConflict.isRaised();
168
}
169
170
4387958
bool ArithCongruenceManager::hasMorePropagations() const {
171
4387958
  return !d_propagatations.empty();
172
}
173
682244
const Node ArithCongruenceManager::getNextPropagation() {
174
682244
  Assert(hasMorePropagations());
175
682244
  Node prop = d_propagatations.front();
176
682244
  d_propagatations.dequeue();
177
682244
  return prop;
178
}
179
180
47106
bool ArithCongruenceManager::canExplain(TNode n) const {
181
47106
  return d_explanationMap.find(n) != d_explanationMap.end();
182
}
183
184
26532
Node ArithCongruenceManager::externalToInternal(TNode n) const{
185
26532
  Assert(canExplain(n));
186
26532
  ExplainMap::const_iterator iter = d_explanationMap.find(n);
187
26532
  size_t pos = (*iter).second;
188
26532
  return d_propagatations[pos];
189
}
190
191
634471
void ArithCongruenceManager::pushBack(TNode n){
192
634471
  d_explanationMap.insert(n, d_propagatations.size());
193
634471
  d_propagatations.enqueue(n);
194
195
634471
  ++(d_statistics.d_propagations);
196
634471
}
197
104228
void ArithCongruenceManager::pushBack(TNode n, TNode r){
198
104228
  d_explanationMap.insert(r, d_propagatations.size());
199
104228
  d_explanationMap.insert(n, d_propagatations.size());
200
104228
  d_propagatations.enqueue(n);
201
202
104228
  ++(d_statistics.d_propagations);
203
104228
}
204
void ArithCongruenceManager::pushBack(TNode n, TNode r, TNode w){
205
  d_explanationMap.insert(w, d_propagatations.size());
206
  d_explanationMap.insert(r, d_propagatations.size());
207
  d_explanationMap.insert(n, d_propagatations.size());
208
  d_propagatations.enqueue(n);
209
210
  ++(d_statistics.d_propagations);
211
}
212
213
295846
void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub){
214
295846
  Assert(lb->isLowerBound());
215
295846
  Assert(ub->isUpperBound());
216
295846
  Assert(lb->getVariable() == ub->getVariable());
217
295846
  Assert(lb->getValue().sgn() == 0);
218
295846
  Assert(ub->getValue().sgn() == 0);
219
220
295846
  ++(d_statistics.d_watchedVariableIsZero);
221
222
295846
  ArithVar s = lb->getVariable();
223
591692
  TNode eq = d_watchedEqualities[s];
224
295846
  ConstraintCP eqC = d_constraintDatabase.getConstraint(
225
295846
      s, ConstraintType::Equality, lb->getValue());
226
591692
  NodeBuilder<> reasonBuilder(Kind::AND);
227
591692
  auto pfLb = lb->externalExplainByAssertions(reasonBuilder);
228
591692
  auto pfUb = ub->externalExplainByAssertions(reasonBuilder);
229
591692
  Node reason = safeConstructNary(reasonBuilder);
230
591692
  std::shared_ptr<ProofNode> pf{};
231
295846
  if (isProofEnabled())
232
  {
233
87912
    pf = d_pnm->mkNode(
234
65934
        PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eqC->getProofLiteral()});
235
21978
    pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq});
236
  }
237
238
295846
  d_keepAlive.push_back(reason);
239
591692
  Trace("arith-ee") << "Asserting an equality on " << s << ", on trichotomy"
240
295846
                    << std::endl;
241
295846
  Trace("arith-ee") << "  based on " << lb << std::endl;
242
295846
  Trace("arith-ee") << "  based on " << ub << std::endl;
243
295846
  assertionToEqualityEngine(true, s, reason, pf);
244
295846
}
245
246
178870
void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
247
178870
  Debug("arith::cong") << "Cong::watchedVariableIsZero: " << *eq << std::endl;
248
249
178870
  Assert(eq->isEquality());
250
178870
  Assert(eq->getValue().sgn() == 0);
251
252
178870
  ++(d_statistics.d_watchedVariableIsZero);
253
254
178870
  ArithVar s = eq->getVariable();
255
256
  //Explain for conflict is correct as these proofs are generated
257
  //and stored eagerly
258
  //These will be safe for propagation later as well
259
357740
  NodeBuilder<> nb(Kind::AND);
260
  // An open proof of eq from literals now in reason.
261
178870
  if (Debug.isOn("arith::cong"))
262
  {
263
    eq->printProofTree(Debug("arith::cong"));
264
  }
265
357740
  auto pf = eq->externalExplainByAssertions(nb);
266
178870
  if (isProofEnabled())
267
  {
268
47397
    pf = d_pnm->mkNode(
269
31598
        PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {d_watchedEqualities[s]});
270
  }
271
357740
  Node reason = safeConstructNary(nb);
272
273
178870
  d_keepAlive.push_back(reason);
274
178870
  assertionToEqualityEngine(true, s, reason, pf);
275
178870
}
276
277
627020
void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
278
1254040
  Debug("arith::cong::notzero")
279
627020
      << "Cong::watchedVariableCannotBeZero " << *c << std::endl;
280
627020
  ++(d_statistics.d_watchedVariableIsNotZero);
281
282
627020
  ArithVar s = c->getVariable();
283
1254040
  Node disEq = d_watchedEqualities[s].negate();
284
285
  //Explain for conflict is correct as these proofs are generated and stored eagerly
286
  //These will be safe for propagation later as well
287
1254040
  NodeBuilder<> nb(Kind::AND);
288
  // An open proof of eq from literals now in reason.
289
1254040
  auto pf = c->externalExplainByAssertions(nb);
290
627020
  if (Debug.isOn("arith::cong::notzero"))
291
  {
292
    Debug("arith::cong::notzero") << "  original proof ";
293
    pf->printDebug(Debug("arith::cong::notzero"));
294
    Debug("arith::cong::notzero") << std::endl;
295
  }
296
1254040
  Node reason = safeConstructNary(nb);
297
627020
  if (isProofEnabled())
298
  {
299
41365
    if (c->getType() == ConstraintType::Disequality)
300
    {
301
9999
      Assert(c->getLiteral() == d_watchedEqualities[s].negate());
302
      // We have to prove equivalence to the watched disequality.
303
9999
      pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {disEq});
304
    }
305
    else
306
    {
307
62732
      Debug("arith::cong::notzero")
308
31366
          << "  proof modification needed" << std::endl;
309
310
      // Four cases:
311
      //   c has form x_i = d, d > 0     => multiply c by -1 in Farkas proof
312
      //   c has form x_i = d, d > 0     => multiply c by 1 in Farkas proof
313
      //   c has form x_i <= d, d < 0     => multiply c by 1 in Farkas proof
314
      //   c has form x_i >= d, d > 0     => multiply c by -1 in Farkas proof
315
31366
      const bool scaleCNegatively = c->getType() == ConstraintType::LowerBound
316
43353
                                    || (c->getType() == ConstraintType::Equality
317
33930
                                        && c->getValue().sgn() > 0);
318
31366
      const int cSign = scaleCNegatively ? -1 : 1;
319
62732
      TNode isZero = d_watchedEqualities[s];
320
62732
      const auto isZeroPf = d_pnm->mkAssume(isZero);
321
31366
      const auto nm = NodeManager::currentNM();
322
31366
      const auto sumPf = d_pnm->mkNode(
323
          PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
324
          {isZeroPf, pf},
325
          // Trick for getting correct, opposing signs.
326
62732
          {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))});
327
31366
      const auto botPf = d_pnm->mkNode(
328
62732
          PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
329
62732
      std::vector<Node> assumption = {isZero};
330
31366
      pf = d_pnm->mkScope(botPf, assumption, false);
331
31366
      Debug("arith::cong::notzero") << "  new proof ";
332
31366
      pf->printDebug(Debug("arith::cong::notzero"));
333
31366
      Debug("arith::cong::notzero") << std::endl;
334
    }
335
41365
    Assert(pf->getResult() == disEq);
336
  }
337
627020
  d_keepAlive.push_back(reason);
338
627020
  assertionToEqualityEngine(false, s, reason, pf);
339
627020
}
340
341
342
845478
bool ArithCongruenceManager::propagate(TNode x){
343
845478
  Debug("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<<x<<")"<<std::endl;
344
845478
  if(inConflict()){
345
    return true;
346
  }
347
348
1690956
  Node rewritten = Rewriter::rewrite(x);
349
350
  //Need to still propagate this!
351
845478
  if(rewritten.getKind() == kind::CONST_BOOLEAN){
352
2335
    pushBack(x);
353
354
2335
    if(rewritten.getConst<bool>()){
355
100
      return true;
356
    }else{
357
      // x rewrites to false.
358
2235
      ++(d_statistics.d_conflicts);
359
4470
      TrustNode trn = explainInternal(x);
360
4470
      Node conf = flattenAnd(trn.getNode());
361
2235
      Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
362
2235
      if (isProofEnabled())
363
      {
364
752
        auto pf = trn.getGenerator()->getProofFor(trn.getProven());
365
376
        auto confPf = d_pnm->mkNode(
366
752
            PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {conf.negate()});
367
376
        raiseConflict(conf, confPf);
368
      }
369
      else
370
      {
371
1859
        raiseConflict(conf);
372
      }
373
2235
      return false;
374
    }
375
  }
376
377
843143
  Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
378
379
843143
  ConstraintP c = d_constraintDatabase.lookup(rewritten);
380
843143
  if(c == NullConstraint){
381
    //using setup as there may not be a corresponding congruence literal yet
382
17109
    d_setupLiteral(rewritten);
383
17109
    c = d_constraintDatabase.lookup(rewritten);
384
17109
    Assert(c != NullConstraint);
385
  }
386
387
1686286
  Debug("arith::congruenceManager")<< "x is "
388
1686286
                                   <<  c->hasProof() << " "
389
1686286
                                   << (x == rewritten) << " "
390
1686286
                                   << c->canBePropagated() << " "
391
843143
                                   << c->negationHasProof() << std::endl;
392
393
843143
  if(c->negationHasProof()){
394
306
    TrustNode texpC = explainInternal(x);
395
306
    Node expC = texpC.getNode();
396
153
    ConstraintCP negC = c->getNegation();
397
306
    Node neg = Constraint::externalExplainByAssertions({negC});
398
306
    Node conf = expC.andNode(neg);
399
306
    Node final = flattenAnd(conf);
400
401
153
    ++(d_statistics.d_conflicts);
402
153
    raiseConflict(final);
403
153
    Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
404
153
    return false;
405
  }
406
407
  // Cases for propagation
408
  // C : c has a proof
409
  // S : x == rewritten
410
  // P : c can be propagated
411
  //
412
  // CSP
413
  // 000 : propagate x, and mark C it as being explained
414
  // 001 : propagate x, and propagate c after marking it as being explained
415
  // 01* : propagate x, mark c but do not propagate c
416
  // 10* : propagate x, do not mark c and do not propagate c
417
  // 11* : drop the constraint, do not propagate x or c
418
419
842990
  if(!c->hasProof() && x != rewritten){
420
104228
    if(c->assertedToTheTheory()){
421
      pushBack(x, rewritten, c->getWitness());
422
    }else{
423
104228
      pushBack(x, rewritten);
424
    }
425
426
104228
    c->setEqualityEngineProof();
427
104228
    if(c->canBePropagated() && !c->assertedToTheTheory()){
428
429
11024
      ++(d_statistics.d_propagateConstraints);
430
11024
      c->propagate();
431
    }
432
738762
  }else if(!c->hasProof() && x == rewritten){
433
79752
    if(c->assertedToTheTheory()){
434
      pushBack(x, c->getWitness());
435
    }else{
436
79752
      pushBack(x);
437
    }
438
79752
    c->setEqualityEngineProof();
439
659010
  }else if(c->hasProof() && x != rewritten){
440
552384
    if(c->assertedToTheTheory()){
441
551051
      pushBack(x);
442
    }else{
443
1333
      pushBack(x);
444
    }
445
  }else{
446
106626
    Assert(c->hasProof() && x == rewritten);
447
  }
448
842990
  return true;
449
}
450
451
void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
452
  if (literal.getKind() != kind::NOT) {
453
    d_ee->explainEquality(literal[0], literal[1], true, assumptions);
454
  } else {
455
    d_ee->explainEquality(literal[0][0], literal[0][1], false, assumptions);
456
  }
457
}
458
459
void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
460
  std::set<TNode>::const_iterator it = s.begin();
461
  std::set<TNode>::const_iterator it_end = s.end();
462
  for(; it != it_end; ++it) {
463
    nb << *it;
464
  }
465
}
466
467
28920
TrustNode ArithCongruenceManager::explainInternal(TNode internal)
468
{
469
28920
  if (isProofEnabled())
470
  {
471
4313
    return d_pfee->explain(internal);
472
  }
473
  // otherwise, explain without proof generator
474
49214
  Node exp = d_ee->mkExplainLit(internal);
475
24607
  return TrustNode::mkTrustPropExp(internal, exp, nullptr);
476
}
477
478
26532
TrustNode ArithCongruenceManager::explain(TNode external)
479
{
480
26532
  Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
481
53064
  Node internal = externalToInternal(external);
482
26532
  Trace("arith-ee") << "...internal = " << internal << std::endl;
483
53064
  TrustNode trn = explainInternal(internal);
484
26532
  if (isProofEnabled() && trn.getProven()[1] != external)
485
  {
486
418
    Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
487
418
    Assert(trn.getProven().getKind() == Kind::IMPLIES);
488
418
    Assert(trn.getGenerator() != nullptr);
489
836
    Trace("arith-ee") << "tweaking proof to prove " << external << " not "
490
418
                      << trn.getProven()[1] << std::endl;
491
836
    std::vector<std::shared_ptr<ProofNode>> assumptionPfs;
492
836
    std::vector<Node> assumptions = andComponents(trn.getNode());
493
418
    assumptionPfs.push_back(trn.toProofNode());
494
1559
    for (const auto& a : assumptions)
495
    {
496
1141
      assumptionPfs.push_back(
497
2282
          d_pnm->mkNode(PfRule::TRUE_INTRO, {d_pnm->mkAssume(a)}, {}));
498
    }
499
418
    auto litPf = d_pnm->mkNode(
500
836
        PfRule::MACRO_SR_PRED_TRANSFORM, {assumptionPfs}, {external});
501
836
    auto extPf = d_pnm->mkScope(litPf, assumptions);
502
418
    return d_pfGenExplain->mkTrustedPropagation(external, trn.getNode(), extPf);
503
  }
504
26114
  return trn;
505
}
506
507
void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
508
  Node internal = externalToInternal(external);
509
510
  std::vector<TNode> assumptions;
511
  explain(internal, assumptions);
512
  std::set<TNode> assumptionSet;
513
  assumptionSet.insert(assumptions.begin(), assumptions.end());
514
515
  enqueueIntoNB(assumptionSet, out);
516
}
517
518
55150
void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
519
55150
  Assert(!isWatchedVariable(s));
520
521
110300
  Debug("arith::congruenceManager")
522
55150
    << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
523
524
525
55150
  ++(d_statistics.d_watchedVariables);
526
527
55150
  d_watchedVariables.add(s);
528
529
110300
  Node eq = x.eqNode(y);
530
55150
  d_watchedEqualities.set(s, eq);
531
55150
}
532
533
2059473
void ArithCongruenceManager::assertLitToEqualityEngine(
534
    Node lit, TNode reason, std::shared_ptr<ProofNode> pf)
535
{
536
2059473
  bool isEquality = lit.getKind() != Kind::NOT;
537
4118946
  Node eq = isEquality ? lit : lit[0];
538
2059473
  Assert(eq.getKind() == Kind::EQUAL);
539
540
4118946
  Trace("arith-ee") << "Assert to Eq " << lit << ", reason " << reason
541
2059473
                    << std::endl;
542
2059473
  if (isProofEnabled())
543
  {
544
157539
    if (CDProof::isSame(lit, reason))
545
    {
546
72396
      Trace("arith-pfee") << "Asserting only, b/c implied by symm" << std::endl;
547
      // The equality engine doesn't ref-count for us...
548
72396
      d_keepAlive.push_back(eq);
549
72396
      d_keepAlive.push_back(reason);
550
72396
      d_ee->assertEquality(eq, isEquality, reason);
551
    }
552
85143
    else if (hasProofFor(lit))
553
    {
554
1190
      Trace("arith-pfee") << "Skipping b/c already done" << std::endl;
555
    }
556
    else
557
    {
558
83953
      setProofFor(lit, pf);
559
83953
      Trace("arith-pfee") << "Actually asserting" << std::endl;
560
83953
      if (Debug.isOn("arith-pfee"))
561
      {
562
        Trace("arith-pfee") << "Proof: ";
563
        pf->printDebug(Trace("arith-pfee"));
564
        Trace("arith-pfee") << std::endl;
565
      }
566
      // The proof equality engine *does* ref-count for us...
567
83953
      d_pfee->assertFact(lit, reason, d_pfGenEe.get());
568
    }
569
  }
570
  else
571
  {
572
    // The equality engine doesn't ref-count for us...
573
1901934
    d_keepAlive.push_back(eq);
574
1901934
    d_keepAlive.push_back(reason);
575
1901934
    d_ee->assertEquality(eq, isEquality, reason);
576
  }
577
2059473
}
578
579
1101736
void ArithCongruenceManager::assertionToEqualityEngine(
580
    bool isEquality, ArithVar s, TNode reason, std::shared_ptr<ProofNode> pf)
581
{
582
1101736
  Assert(isWatchedVariable(s));
583
584
2203472
  TNode eq = d_watchedEqualities[s];
585
1101736
  Assert(eq.getKind() == kind::EQUAL);
586
587
2203472
  Node lit = isEquality ? Node(eq) : eq.notNode();
588
2203472
  Trace("arith-ee") << "Assert to Eq " << eq << ", pol " << isEquality
589
1101736
                    << ", reason " << reason << std::endl;
590
1101736
  assertLitToEqualityEngine(lit, reason, pf);
591
1101736
}
592
593
169096
bool ArithCongruenceManager::hasProofFor(TNode f) const
594
{
595
169096
  Assert(isProofEnabled());
596
169096
  if (d_pfGenEe->hasProofFor(f))
597
  {
598
1190
    return true;
599
  }
600
335812
  Node sym = CDProof::getSymmFact(f);
601
167906
  Assert(!sym.isNull());
602
167906
  return d_pfGenEe->hasProofFor(sym);
603
}
604
605
83953
void ArithCongruenceManager::setProofFor(TNode f,
606
                                         std::shared_ptr<ProofNode> pf) const
607
{
608
83953
  Assert(!hasProofFor(f));
609
83953
  d_pfGenEe->mkTrustNode(f, pf);
610
167906
  Node symF = CDProof::getSymmFact(f);
611
167906
  auto symPf = d_pnm->mkNode(PfRule::SYMM, {pf}, {});
612
83953
  d_pfGenEe->mkTrustNode(symF, symPf);
613
83953
}
614
615
758932
void ArithCongruenceManager::equalsConstant(ConstraintCP c){
616
758932
  Assert(c->isEquality());
617
618
758932
  ++(d_statistics.d_equalsConstantCalls);
619
758932
  Debug("equalsConstant") << "equals constant " << c << std::endl;
620
621
758932
  ArithVar x = c->getVariable();
622
1517864
  Node xAsNode = d_avariables.asNode(x);
623
1517864
  Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart());
624
625
  // No guarentee this is in normal form!
626
  // Note though, that it happens to be in proof normal form!
627
1517864
  Node eq = xAsNode.eqNode(asRational);
628
758932
  d_keepAlive.push_back(eq);
629
630
1517864
  NodeBuilder<> nb(Kind::AND);
631
1517864
  auto pf = c->externalExplainByAssertions(nb);
632
1517864
  Node reason = safeConstructNary(nb);
633
758932
  d_keepAlive.push_back(reason);
634
635
758932
  Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
636
758932
  assertLitToEqualityEngine(eq, reason, pf);
637
758932
}
638
639
198805
void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
640
198805
  Assert(lb->isLowerBound());
641
198805
  Assert(ub->isUpperBound());
642
198805
  Assert(lb->getVariable() == ub->getVariable());
643
644
198805
  ++(d_statistics.d_equalsConstantCalls);
645
397610
  Debug("equalsConstant") << "equals constant " << lb << std::endl
646
198805
                          << ub << std::endl;
647
648
198805
  ArithVar x = lb->getVariable();
649
397610
  NodeBuilder<> nb(Kind::AND);
650
397610
  auto pfLb = lb->externalExplainByAssertions(nb);
651
397610
  auto pfUb = ub->externalExplainByAssertions(nb);
652
397610
  Node reason = safeConstructNary(nb);
653
654
397610
  Node xAsNode = d_avariables.asNode(x);
655
397610
  Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
656
657
  // No guarentee this is in normal form!
658
  // Note though, that it happens to be in proof normal form!
659
397610
  Node eq = xAsNode.eqNode(asRational);
660
397610
  std::shared_ptr<ProofNode> pf;
661
198805
  if (isProofEnabled())
662
  {
663
17381
    pf = d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eq});
664
  }
665
198805
  d_keepAlive.push_back(eq);
666
198805
  d_keepAlive.push_back(reason);
667
668
198805
  Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
669
670
198805
  assertLitToEqualityEngine(eq, reason, pf);
671
198805
}
672
673
3595792
bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
674
675
418
std::vector<Node> andComponents(TNode an)
676
{
677
418
  auto nm = NodeManager::currentNM();
678
418
  if (an == nm->mkConst(true))
679
  {
680
    return {};
681
  }
682
418
  else if (an.getKind() != Kind::AND)
683
  {
684
    return {an};
685
  }
686
836
  std::vector<Node> a{};
687
418
  a.reserve(an.getNumChildren());
688
418
  a.insert(a.end(), an.begin(), an.end());
689
418
  return a;
690
}
691
692
}/* CVC4::theory::arith namespace */
693
}/* CVC4::theory namespace */
694
26676
}/* CVC4 namespace */