GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/constraint.cpp Lines: 1075 1475 72.9 %
Date: 2021-03-23 Branches: 1808 6419 28.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file constraint.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Alex Ozdemir, Haniel Barbosa
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
#include "theory/arith/constraint.h"
18
19
#include <algorithm>
20
#include <ostream>
21
#include <unordered_set>
22
23
#include "base/output.h"
24
#include "expr/proof_node_manager.h"
25
#include "smt/smt_statistics_registry.h"
26
#include "theory/eager_proof_generator.h"
27
#include "theory/arith/arith_utilities.h"
28
#include "theory/arith/congruence_manager.h"
29
#include "theory/arith/normal_form.h"
30
#include "theory/arith/partial_model.h"
31
#include "theory/rewriter.h"
32
33
34
using namespace std;
35
using namespace CVC4::kind;
36
37
namespace CVC4 {
38
namespace theory {
39
namespace arith {
40
41
/** Given a simplifiedKind this returns the corresponding ConstraintType. */
42
//ConstraintType constraintTypeOfLiteral(Kind k);
43
487553
ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){
44
487553
  Kind k = cmp.comparisonKind();
45
487553
  switch(k){
46
135118
  case LT:
47
  case LEQ:
48
    {
49
270236
      Polynomial l = cmp.getLeft();
50
135118
      if(l.leadingCoefficientIsPositive()){ // (< x c)
51
111326
        return UpperBound;
52
      }else{
53
23792
        return LowerBound; // (< (-x) c)
54
      }
55
    }
56
136280
  case GT:
57
  case GEQ:
58
    {
59
272560
      Polynomial l = cmp.getLeft();
60
136280
      if(l.leadingCoefficientIsPositive()){
61
112281
        return LowerBound; // (> x c)
62
      }else{
63
23999
        return UpperBound; // (> (-x) c)
64
      }
65
    }
66
108186
  case EQUAL:
67
108186
    return Equality;
68
107969
  case DISTINCT:
69
107969
    return Disequality;
70
  default: Unhandled() << k;
71
  }
72
}
73
74
607277
Constraint::Constraint(ArithVar x,  ConstraintType t, const DeltaRational& v)
75
  : d_variable(x),
76
    d_type(t),
77
    d_value(v),
78
    d_database(NULL),
79
    d_literal(Node::null()),
80
    d_negation(NullConstraint),
81
    d_canBePropagated(false),
82
    d_assertionOrder(AssertionOrderSentinel),
83
    d_witness(TNode::null()),
84
    d_crid(ConstraintRuleIdSentinel),
85
    d_split(false),
86
607277
    d_variablePosition()
87
{
88
607277
  Assert(!initialized());
89
607277
}
90
91
92
std::ostream& operator<<(std::ostream& o, const ArithProofType apt){
93
  switch(apt){
94
  case NoAP:  o << "NoAP"; break;
95
  case AssumeAP:  o << "AssumeAP"; break;
96
  case InternalAssumeAP:  o << "InternalAssumeAP"; break;
97
  case FarkasAP:  o << "FarkasAP"; break;
98
  case TrichotomyAP:  o << "TrichotomyAP"; break;
99
  case EqualityEngineAP:  o << "EqualityEngineAP"; break;
100
  case IntTightenAP: o << "IntTightenAP"; break;
101
  case IntHoleAP: o << "IntHoleAP"; break;
102
  default: break;
103
  }
104
  return o;
105
}
106
107
std::ostream& operator<<(std::ostream& o, const ConstraintCP c){
108
  if(c == NullConstraint){
109
    return o << "NullConstraint";
110
  }else{
111
    return o << *c;
112
  }
113
}
114
115
std::ostream& operator<<(std::ostream& o, const ConstraintP c){
116
  if(c == NullConstraint){
117
    return o << "NullConstraint";
118
  }else{
119
    return o << *c;
120
  }
121
}
122
123
std::ostream& operator<<(std::ostream& o, const ConstraintType t){
124
  switch(t){
125
  case LowerBound:
126
    return o << ">=";
127
  case UpperBound:
128
    return o << "<=";
129
  case Equality:
130
    return o << "=";
131
  case Disequality:
132
    return o << "!=";
133
  default:
134
    Unreachable();
135
  }
136
}
137
138
std::ostream& operator<<(std::ostream& o, const Constraint& c){
139
  o << c.getVariable() << ' ' << c.getType() << ' ' << c.getValue();
140
  if(c.hasLiteral()){
141
    o << "(node " << c.getLiteral() << ')';
142
  }
143
  return o;
144
}
145
146
std::ostream& operator<<(std::ostream& o, const ValueCollection& vc){
147
  o << "{";
148
  bool pending = false;
149
  if(vc.hasEquality()){
150
    o << "eq: " << vc.getEquality();
151
    pending = true;
152
  }
153
  if(vc.hasLowerBound()){
154
    if(pending){
155
      o << ", ";
156
    }
157
    o << "lb: " << vc.getLowerBound();
158
    pending = true;
159
  }
160
  if(vc.hasUpperBound()){
161
    if(pending){
162
      o << ", ";
163
    }
164
    o << "ub: " << vc.getUpperBound();
165
    pending = true;
166
  }
167
  if(vc.hasDisequality()){
168
    if(pending){
169
      o << ", ";
170
    }
171
    o << "de: " << vc.getDisequality();
172
  }
173
  return o << "}";
174
}
175
176
std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){
177
  o << "[" << v.size() << "x";
178
  ConstraintCPVec::const_iterator i, end;
179
  for(i=v.begin(), end=v.end(); i != end; ++i){
180
    ConstraintCP c = *i;
181
    o << ", " << (*c);
182
  }
183
  o << "]";
184
  return o;
185
}
186
187
void Constraint::debugPrint() const { CVC4Message() << *this << endl; }
188
189
2185409
ValueCollection::ValueCollection()
190
  : d_lowerBound(NullConstraint),
191
    d_upperBound(NullConstraint),
192
    d_equality(NullConstraint),
193
2185409
    d_disequality(NullConstraint)
194
2185409
{}
195
196
18784300
bool ValueCollection::hasLowerBound() const{
197
18784300
  return d_lowerBound != NullConstraint;
198
}
199
200
21384337
bool ValueCollection::hasUpperBound() const{
201
21384337
  return d_upperBound != NullConstraint;
202
}
203
204
4229849
bool ValueCollection::hasEquality() const{
205
4229849
  return d_equality != NullConstraint;
206
}
207
208
14808995
bool ValueCollection::hasDisequality() const {
209
14808995
  return d_disequality != NullConstraint;
210
}
211
212
3950145
ConstraintP ValueCollection::getLowerBound() const {
213
3950145
  Assert(hasLowerBound());
214
3950145
  return d_lowerBound;
215
}
216
217
4348646
ConstraintP ValueCollection::getUpperBound() const {
218
4348646
  Assert(hasUpperBound());
219
4348646
  return d_upperBound;
220
}
221
222
401293
ConstraintP ValueCollection::getEquality() const {
223
401293
  Assert(hasEquality());
224
401293
  return d_equality;
225
}
226
227
2399984
ConstraintP ValueCollection::getDisequality() const {
228
2399984
  Assert(hasDisequality());
229
2399984
  return d_disequality;
230
}
231
232
233
411385
void ValueCollection::push_into(std::vector<ConstraintP>& vec) const {
234
411385
  Debug("arith::constraint") << "push_into " << *this << endl;
235
411385
  if(hasEquality()){
236
112407
    vec.push_back(d_equality);
237
  }
238
411385
  if(hasLowerBound()){
239
190542
    vec.push_back(d_lowerBound);
240
  }
241
411385
  if(hasUpperBound()){
242
190542
    vec.push_back(d_upperBound);
243
  }
244
411385
  if(hasDisequality()){
245
112407
    vec.push_back(d_disequality);
246
  }
247
411385
}
248
249
ValueCollection ValueCollection::mkFromConstraint(ConstraintP c){
250
  ValueCollection ret;
251
  Assert(ret.empty());
252
  switch(c->getType()){
253
  case LowerBound:
254
    ret.d_lowerBound = c;
255
    break;
256
  case UpperBound:
257
    ret.d_upperBound = c;
258
    break;
259
  case Equality:
260
    ret.d_equality = c;
261
    break;
262
  case Disequality:
263
    ret.d_disequality = c;
264
    break;
265
  default:
266
    Unreachable();
267
  }
268
  return ret;
269
}
270
271
3638405
bool ValueCollection::hasConstraintOfType(ConstraintType t) const{
272
3638405
  switch(t){
273
1136411
  case LowerBound:
274
1136411
    return hasLowerBound();
275
2097962
  case UpperBound:
276
2097962
    return hasUpperBound();
277
404032
  case Equality:
278
404032
    return hasEquality();
279
  case Disequality:
280
    return hasDisequality();
281
  default:
282
    Unreachable();
283
  }
284
}
285
286
200785
ArithVar ValueCollection::getVariable() const{
287
200785
  Assert(!empty());
288
200785
  return nonNull()->getVariable();
289
}
290
291
200785
const DeltaRational& ValueCollection::getValue() const{
292
200785
  Assert(!empty());
293
200785
  return nonNull()->getValue();
294
}
295
296
605898
void ValueCollection::add(ConstraintP c){
297
605898
  Assert(c != NullConstraint);
298
299
605898
  Assert(empty() || getVariable() == c->getVariable());
300
605898
  Assert(empty() || getValue() == c->getValue());
301
302
605898
  switch(c->getType()){
303
190542
  case LowerBound:
304
190542
    Assert(!hasLowerBound());
305
190542
    d_lowerBound = c;
306
190542
    break;
307
112407
  case Equality:
308
112407
    Assert(!hasEquality());
309
112407
    d_equality = c;
310
112407
    break;
311
190542
  case UpperBound:
312
190542
    Assert(!hasUpperBound());
313
190542
    d_upperBound = c;
314
190542
    break;
315
112407
  case Disequality:
316
112407
    Assert(!hasDisequality());
317
112407
    d_disequality = c;
318
112407
    break;
319
  default:
320
    Unreachable();
321
  }
322
605898
}
323
324
2833610
ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const{
325
2833610
  switch(t){
326
731967
    case LowerBound: Assert(hasLowerBound()); return d_lowerBound;
327
291625
    case Equality: Assert(hasEquality()); return d_equality;
328
1810018
    case UpperBound: Assert(hasUpperBound()); return d_upperBound;
329
    case Disequality: Assert(hasDisequality()); return d_disequality;
330
    default: Unreachable();
331
  }
332
}
333
334
605898
void ValueCollection::remove(ConstraintType t){
335
605898
  switch(t){
336
190542
  case LowerBound:
337
190542
    Assert(hasLowerBound());
338
190542
    d_lowerBound = NullConstraint;
339
190542
    break;
340
112407
  case Equality:
341
112407
    Assert(hasEquality());
342
112407
    d_equality = NullConstraint;
343
112407
    break;
344
190542
  case UpperBound:
345
190542
    Assert(hasUpperBound());
346
190542
    d_upperBound = NullConstraint;
347
190542
    break;
348
112407
  case Disequality:
349
112407
    Assert(hasDisequality());
350
112407
    d_disequality = NullConstraint;
351
112407
    break;
352
  default:
353
    Unreachable();
354
  }
355
605898
}
356
357
2219264
bool ValueCollection::empty() const{
358
  return
359
5347740
    !(hasLowerBound() ||
360
3694763
      hasUpperBound() ||
361
1800442
      hasEquality() ||
362
3453419
      hasDisequality());
363
}
364
365
401570
ConstraintP ValueCollection::nonNull() const{
366
  //This can be optimized by caching, but this is not necessary yet!
367
  /* "Premature optimization is the root of all evil." */
368
401570
  if(hasLowerBound()){
369
129436
    return d_lowerBound;
370
272134
  }else if(hasUpperBound()){
371
45194
    return d_upperBound;
372
226940
  }else if(hasEquality()){
373
226940
    return d_equality;
374
  }else if(hasDisequality()){
375
    return d_disequality;
376
  }else{
377
    return NullConstraint;
378
  }
379
}
380
381
2521930
bool Constraint::initialized() const {
382
2521930
  return d_database != NULL;
383
}
384
385
const ConstraintDatabase& Constraint::getDatabase() const{
386
  Assert(initialized());
387
  return *d_database;
388
}
389
390
605898
void Constraint::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){
391
605898
  Assert(!initialized());
392
605898
  d_database = db;
393
605898
  d_variablePosition = v;
394
605898
  d_negation = negation;
395
605898
}
396
397
1214554
Constraint::~Constraint() {
398
  // Call this instead of safeToGarbageCollect()
399
607277
  Assert(!contextDependentDataIsSet());
400
401
607277
  if(initialized()){
402
605898
    ValueCollection& vc =  d_variablePosition->second;
403
605898
    Debug("arith::constraint") << "removing" << vc << endl;
404
405
605898
    vc.remove(getType());
406
407
605898
    if(vc.empty()){
408
411385
      Debug("arith::constraint") << "erasing" << vc << endl;
409
411385
      SortedConstraintMap& perVariable = d_database->getVariableSCM(getVariable());
410
411385
      perVariable.erase(d_variablePosition);
411
    }
412
413
605898
    if(hasLiteral()){
414
488932
      d_database->d_nodetoConstraintMap.erase(getLiteral());
415
    }
416
  }
417
607277
}
418
419
26814269
const ConstraintRule& Constraint::getConstraintRule() const {
420
26814269
  Assert(hasProof());
421
26814269
  return d_database->d_watches->d_constraintProofs[d_crid];
422
}
423
424
2995896
const ValueCollection& Constraint::getValueCollection() const{
425
2995896
  return d_variablePosition->second;
426
}
427
428
429
81021
ConstraintP Constraint::getCeiling() {
430
81021
  Debug("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
431
81021
  Assert(getValue().getInfinitesimalPart().sgn() > 0);
432
433
162042
  const DeltaRational ceiling(getValue().ceiling());
434
162042
  return d_database->getConstraint(getVariable(), getType(), ceiling);
435
}
436
437
1367262
ConstraintP Constraint::getFloor() {
438
1367262
  Assert(getValue().getInfinitesimalPart().sgn() < 0);
439
440
2734524
  const DeltaRational floor(Rational(getValue().floor()));
441
2734524
  return d_database->getConstraint(getVariable(), getType(), floor);
442
}
443
444
688474
void Constraint::setCanBePropagated() {
445
688474
  Assert(!canBePropagated());
446
688474
  d_database->pushCanBePropagatedWatch(this);
447
688474
}
448
449
5716677
void Constraint::setAssertedToTheTheory(TNode witness, bool nowInConflict) {
450
5716677
  Assert(hasLiteral());
451
5716677
  Assert(!assertedToTheTheory());
452
5716677
  Assert(negationHasProof() == nowInConflict);
453
5716677
  d_database->pushAssertionOrderWatch(this, witness);
454
455
5716677
  if(Debug.isOn("constraint::conflictCommit") && nowInConflict ){
456
    Debug("constraint::conflictCommit") << "inConflict@setAssertedToTheTheory";
457
    Debug("constraint::conflictCommit") << "\t" << this << std::endl;
458
    Debug("constraint::conflictCommit") << "\t" << getNegation() << std::endl;
459
    Debug("constraint::conflictCommit") << "\t" << getNegation()->externalExplainByAssertions() << std::endl;
460
461
  }
462
5716677
}
463
464
bool Constraint::satisfiedBy(const DeltaRational& dr) const {
465
  switch(getType()){
466
  case LowerBound:
467
    return getValue() <= dr;
468
  case Equality:
469
    return getValue() == dr;
470
  case UpperBound:
471
    return getValue() >= dr;
472
  case Disequality:
473
    return getValue() != dr;
474
  }
475
  Unreachable();
476
}
477
478
11136889
bool Constraint::isInternalAssumption() const {
479
11136889
  return getProofType() == InternalAssumeAP;
480
}
481
482
TrustNode Constraint::externalExplainByAssertions() const
483
{
484
  NodeBuilder<> nb(kind::AND);
485
  auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel);
486
  Node exp = safeConstructNary(nb);
487
  if (d_database->isProofEnabled())
488
  {
489
    std::vector<Node> assumptions;
490
    if (exp.getKind() == Kind::AND)
491
    {
492
      assumptions.insert(assumptions.end(), exp.begin(), exp.end());
493
    }
494
    else
495
    {
496
      assumptions.push_back(exp);
497
    }
498
    auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
499
    return d_database->d_pfGen->mkTrustedPropagation(
500
        getLiteral(), safeConstructNary(Kind::AND, assumptions), pf);
501
  }
502
  return TrustNode::mkTrustPropExp(getLiteral(), exp);
503
}
504
505
11766483
bool Constraint::isAssumption() const {
506
11766483
  return getProofType() == AssumeAP;
507
}
508
509
607882
bool Constraint::hasEqualityEngineProof() const {
510
607882
  return getProofType() == EqualityEngineAP;
511
}
512
513
bool Constraint::hasFarkasProof() const {
514
  return getProofType() == FarkasAP;
515
}
516
517
bool Constraint::hasSimpleFarkasProof() const
518
{
519
  Debug("constraints::hsfp") << "hasSimpleFarkasProof " << this << std::endl;
520
  if (!hasFarkasProof())
521
  {
522
    Debug("constraints::hsfp") << "There is no simple Farkas proof because "
523
                                  "there is no farkas proof."
524
                               << std::endl;
525
    return false;
526
  }
527
528
  // For each antecdent ...
529
  AntecedentId i = getConstraintRule().d_antecedentEnd;
530
  for (ConstraintCP a = d_database->getAntecedent(i); a != NullConstraint;
531
       a = d_database->getAntecedent(--i))
532
  {
533
    // ... that antecdent must be an assumption OR a tightened assumption ...
534
    if (a->isPossiblyTightenedAssumption())
535
    {
536
      continue;
537
    }
538
539
    // ... otherwise, we do not have a simple Farkas proof.
540
    if (Debug.isOn("constraints::hsfp"))
541
    {
542
      Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there "
543
                                    "is an antecdent w/ rule ";
544
      a->getConstraintRule().print(Debug("constraints::hsfp"));
545
      Debug("constraints::hsfp") << std::endl;
546
    }
547
548
    return false;
549
  }
550
  return true;
551
}
552
553
bool Constraint::isPossiblyTightenedAssumption() const
554
{
555
  // ... that antecdent must be an assumption ...
556
557
  if (isAssumption()) return true;
558
  if (!hasIntTightenProof()) return false;
559
  if (getConstraintRule().d_antecedentEnd == AntecedentIdSentinel) return false;
560
  return d_database->getAntecedent(getConstraintRule().d_antecedentEnd)
561
      ->isAssumption();
562
}
563
564
bool Constraint::hasIntTightenProof() const {
565
  return getProofType() == IntTightenAP;
566
}
567
568
bool Constraint::hasIntHoleProof() const {
569
  return getProofType() == IntHoleAP;
570
}
571
572
bool Constraint::hasTrichotomyProof() const {
573
  return getProofType() == TrichotomyAP;
574
}
575
576
void Constraint::printProofTree(std::ostream& out, size_t depth) const
577
{
578
  if (ARITH_PROOF_ON())
579
  {
580
    const ConstraintRule& rule = getConstraintRule();
581
    out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
582
    out << getProofLiteral();
583
    if (assertedToTheTheory())
584
    {
585
      out << " | wit: " << getWitness();
586
    }
587
    out << "]" << ' ' << getType() << ' ' << getValue() << " ("
588
        << getProofType() << ")";
589
    if (getProofType() == FarkasAP)
590
    {
591
      out << " [";
592
      bool first = true;
593
      for (const auto& coeff : *rule.d_farkasCoefficients)
594
      {
595
        if (not first)
596
        {
597
          out << ", ";
598
        }
599
        first = false;
600
        out << coeff;
601
      }
602
      out << "]";
603
    }
604
    out << endl;
605
606
    for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i)
607
    {
608
      ConstraintCP antecdent = d_database->getAntecedent(i);
609
      if (antecdent == NullConstraint)
610
      {
611
        break;
612
      }
613
      antecdent->printProofTree(out, depth + 1);
614
    }
615
    return;
616
  }
617
  out << "Cannot print proof. This is not a proof build." << endl;
618
}
619
620
488932
bool Constraint::sanityChecking(Node n) const {
621
977864
  Comparison cmp = Comparison::parseNormalForm(n);
622
488932
  Kind k = cmp.comparisonKind();
623
977864
  Polynomial pleft = cmp.normalizedVariablePart();
624
488932
  Assert(k == EQUAL || k == DISTINCT || pleft.leadingCoefficientIsPositive());
625
488932
  Assert(k != EQUAL || Monomial::isMember(n[0]));
626
488932
  Assert(k != DISTINCT || Monomial::isMember(n[0][0]));
627
628
977864
  TNode left = pleft.getNode();
629
977864
  DeltaRational right = cmp.normalizedDeltaRational();
630
631
488932
  const ArithVariables& avariables = d_database->getArithVariables();
632
633
488932
  Debug("Constraint::sanityChecking") << cmp.getNode() << endl;
634
488932
  Debug("Constraint::sanityChecking") << k << endl;
635
488932
  Debug("Constraint::sanityChecking") << pleft.getNode() << endl;
636
488932
  Debug("Constraint::sanityChecking") << left << endl;
637
488932
  Debug("Constraint::sanityChecking") << right << endl;
638
488932
  Debug("Constraint::sanityChecking") << getValue() << endl;
639
488932
  Debug("Constraint::sanityChecking") << avariables.hasArithVar(left) << endl;
640
488932
  Debug("Constraint::sanityChecking") << avariables.asArithVar(left) << endl;
641
488932
  Debug("Constraint::sanityChecking") << getVariable() << endl;
642
643
644
2444660
  if(avariables.hasArithVar(left) &&
645
2444660
     avariables.asArithVar(left) == getVariable() &&
646
488932
     getValue() == right){
647
488932
    switch(getType()){
648
272560
    case LowerBound:
649
    case UpperBound:
650
      //Be overapproximate
651
272560
      return k == GT || k == GEQ ||k == LT || k == LEQ;
652
108186
    case Equality:
653
108186
      return k == EQUAL;
654
108186
    case Disequality:
655
108186
      return k == DISTINCT;
656
    default:
657
      Unreachable();
658
    }
659
  }else{
660
    return false;
661
  }
662
}
663
664
void ConstraintRule::debugPrint() const {
665
  print(std::cerr);
666
}
667
668
ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const {
669
  Assert(p < d_antecedents.size());
670
  return d_antecedents[p];
671
}
672
673
674
void ConstraintRule::print(std::ostream& out) const {
675
  RationalVectorCP coeffs = ARITH_NULLPROOF(d_farkasCoefficients);
676
  out << "{ConstraintRule, ";
677
  out << d_constraint << std::endl;
678
  out << "d_proofType= " << d_proofType << ", " << std::endl;
679
  out << "d_antecedentEnd= "<< d_antecedentEnd << std::endl;
680
681
  if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel)
682
  {
683
    const ConstraintDatabase& database = d_constraint->getDatabase();
684
685
    size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0;
686
    AntecedentId p = d_antecedentEnd;
687
    // must have at least one antecedent
688
    ConstraintCP antecedent = database.getAntecedent(p);
689
    while(antecedent != NullConstraint){
690
      if(coeffs != RationalVectorCPSentinel){
691
        out << coeffs->at(coeffIterator);
692
      } else {
693
        out << "_";
694
      }
695
      out << " * (" << *antecedent << ")" << std::endl;
696
697
      Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0);
698
      --p;
699
      coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffIterator-1 : 0;
700
      antecedent = database.getAntecedent(p);
701
    }
702
    if(coeffs != RationalVectorCPSentinel){
703
      out << coeffs->front();
704
    } else {
705
      out << "_";
706
    }
707
    out << " * (" << *(d_constraint->getNegation()) << ")";
708
    out << " [not d_constraint] " << endl;
709
  }
710
  out << "}";
711
}
712
713
2534865
bool Constraint::wellFormedFarkasProof() const {
714
2534865
  Assert(hasProof());
715
716
2534865
  const ConstraintRule& cr = getConstraintRule();
717
2534865
  if(cr.d_constraint != this){ return false; }
718
2534865
  if(cr.d_proofType != FarkasAP){ return false; }
719
720
2534865
  AntecedentId p = cr.d_antecedentEnd;
721
722
  // must have at least one antecedent
723
2534865
  ConstraintCP antecedent = d_database->d_antecedents[p];
724
2534865
  if(antecedent  == NullConstraint) { return false; }
725
726
2534865
  if (!ARITH_PROOF_ON())
727
  {
728
2204596
    return cr.d_farkasCoefficients == RationalVectorCPSentinel;
729
  }
730
330269
  Assert(ARITH_PROOF_ON());
731
732
330269
  if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
733
330269
  if(cr.d_farkasCoefficients->size() < 2){ return false; }
734
735
330269
  const ArithVariables& vars = d_database->getArithVariables();
736
737
660538
  DeltaRational rhs(0);
738
660538
  Node lhs = Polynomial::mkZero().getNode();
739
740
330269
  RationalVector::const_iterator coeffIterator = cr.d_farkasCoefficients->end()-1;
741
330269
  RationalVector::const_iterator coeffBegin = cr.d_farkasCoefficients->begin();
742
743
1145283
  while(antecedent != NullConstraint){
744
407507
    Assert(lhs.isNull() || Polynomial::isMember(lhs));
745
746
407507
    const Rational& coeff = *coeffIterator;
747
407507
    int coeffSgn = coeff.sgn();
748
749
407507
    rhs += antecedent->getValue() * coeff;
750
751
407507
    ArithVar antVar = antecedent->getVariable();
752
407507
    if(!lhs.isNull() && vars.hasNode(antVar)){
753
815014
      Node antAsNode = vars.asNode(antVar);
754
407507
      if(Polynomial::isMember(antAsNode)){
755
815014
        Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
756
815014
        Polynomial antPoly = Polynomial::parsePolynomial(antAsNode);
757
815014
        Polynomial sum = lhsPoly + (antPoly * coeff);
758
407507
        lhs = sum.getNode();
759
      }else{
760
        lhs = Node::null();
761
      }
762
    } else {
763
      lhs = Node::null();
764
    }
765
407507
    Debug("constraints::wffp") << "running sum: " << lhs << " <= " << rhs << endl;
766
767
407507
    switch( antecedent->getType() ){
768
104600
    case LowerBound:
769
      // fc[l] < 0, therefore return false if coeffSgn >= 0
770
104600
      if(coeffSgn >= 0){ return false; }
771
104600
      break;
772
60222
    case UpperBound:
773
      // fc[u] > 0, therefore return false if coeffSgn <= 0
774
60222
      if(coeffSgn <= 0){ return false; }
775
60222
      break;
776
242685
    case Equality:
777
242685
      if(coeffSgn == 0) { return false; }
778
242685
      break;
779
    case Disequality:
780
    default:
781
      return false;
782
    }
783
784
407507
    if(coeffIterator == coeffBegin){ return false; }
785
407507
    --coeffIterator;
786
407507
    --p;
787
407507
    antecedent = d_database->d_antecedents[p];
788
  }
789
330269
  if(coeffIterator != coeffBegin){ return false; }
790
791
330269
  const Rational& firstCoeff = (*coeffBegin);
792
330269
  int firstCoeffSgn = firstCoeff.sgn();
793
330269
  rhs += (getNegation()->getValue()) * firstCoeff;
794
330269
  if(!lhs.isNull() && vars.hasNode(getVariable())){
795
660538
    Node firstAsNode = vars.asNode(getVariable());
796
330269
    if(Polynomial::isMember(firstAsNode)){
797
660538
      Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
798
660538
      Polynomial firstPoly = Polynomial::parsePolynomial(firstAsNode);
799
660538
      Polynomial sum = lhsPoly + (firstPoly * firstCoeff);
800
330269
      lhs = sum.getNode();
801
    }else{
802
      lhs = Node::null();
803
    }
804
  }else{
805
    lhs = Node::null();
806
  }
807
808
330269
  switch( getNegation()->getType() ){
809
86595
  case LowerBound:
810
    // fc[l] < 0, therefore return false if coeffSgn >= 0
811
86595
    if(firstCoeffSgn >= 0){ return false; }
812
86595
    break;
813
99181
  case UpperBound:
814
    // fc[u] > 0, therefore return false if coeffSgn <= 0
815
99181
    if(firstCoeffSgn <= 0){ return false; }
816
99181
    break;
817
144493
  case Equality:
818
144493
    if(firstCoeffSgn == 0) { return false; }
819
144493
    break;
820
  case Disequality:
821
  default:
822
    return false;
823
  }
824
330269
  Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
825
  // 0 = lhs <= rhs < 0
826
990807
  return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
827
990807
         && rhs.sgn() < 0;
828
}
829
830
59862
ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
831
59862
  switch(t){
832
3287
  case LowerBound:
833
    {
834
3287
      Assert(r.infinitesimalSgn() >= 0);
835
3287
      if(r.infinitesimalSgn() > 0){
836
        Assert(r.getInfinitesimalPart() == 1);
837
        // make (not (v > r)), which is (v <= r)
838
        DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
839
        return new Constraint(v, UpperBound, dropInf);
840
      }else{
841
3287
        Assert(r.infinitesimalSgn() == 0);
842
        // make (not (v >= r)), which is (v < r)
843
6574
        DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
844
3287
        return new Constraint(v, UpperBound, addInf);
845
      }
846
    }
847
52137
  case UpperBound:
848
    {
849
52137
      Assert(r.infinitesimalSgn() <= 0);
850
52137
      if(r.infinitesimalSgn() < 0){
851
        Assert(r.getInfinitesimalPart() == -1);
852
        // make (not (v < r)), which is (v >= r)
853
        DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
854
        return new Constraint(v, LowerBound, dropInf);
855
      }else{
856
52137
        Assert(r.infinitesimalSgn() == 0);
857
        // make (not (v <= r)), which is (v > r)
858
104274
        DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
859
52137
        return new Constraint(v, LowerBound, addInf);
860
      }
861
    }
862
4438
  case Equality:
863
4438
    return new Constraint(v, Disequality, r);
864
  case Disequality:
865
    return new Constraint(v, Equality, r);
866
  default:
867
    Unreachable();
868
    return NullConstraint;
869
  }
870
}
871
872
8997
ConstraintDatabase::ConstraintDatabase(context::Context* satContext,
873
                                       context::Context* userContext,
874
                                       const ArithVariables& avars,
875
                                       ArithCongruenceManager& cm,
876
                                       RaiseConflict raiseConflict,
877
                                       EagerProofGenerator* pfGen,
878
8997
                                       ProofNodeManager* pnm)
879
    : d_varDatabases(),
880
      d_toPropagate(satContext),
881
      d_antecedents(satContext, false),
882
8997
      d_watches(new Watches(satContext, userContext)),
883
      d_avariables(avars),
884
      d_congruenceManager(cm),
885
      d_satContext(satContext),
886
      d_pfGen(pfGen),
887
      d_pnm(pnm),
888
      d_raiseConflict(raiseConflict),
889
      d_one(1),
890
17994
      d_negOne(-1)
891
{
892
8997
}
893
894
10080852
SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const{
895
10080852
  Assert(variableDatabaseIsSetup(v));
896
10080852
  return d_varDatabases[v]->d_constraints;
897
}
898
899
29790
void ConstraintDatabase::pushSplitWatch(ConstraintP c){
900
29790
  Assert(!c->d_split);
901
29790
  c->d_split = true;
902
29790
  d_watches->d_splitWatches.push_back(c);
903
29790
}
904
905
906
688474
void ConstraintDatabase::pushCanBePropagatedWatch(ConstraintP c){
907
688474
  Assert(!c->d_canBePropagated);
908
688474
  c->d_canBePropagated = true;
909
688474
  d_watches->d_canBePropagatedWatches.push_back(c);
910
688474
}
911
912
5716677
void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness){
913
5716677
  Assert(!c->assertedToTheTheory());
914
5716677
  c->d_assertionOrder = d_watches->d_assertionOrderWatches.size();
915
5716677
  c->d_witness = witness;
916
5716677
  d_watches->d_assertionOrderWatches.push_back(c);
917
5716677
}
918
919
920
9161894
void ConstraintDatabase::pushConstraintRule(const ConstraintRule& crp){
921
9161894
  ConstraintP c = crp.d_constraint;
922
9161894
  Assert(c->d_crid == ConstraintRuleIdSentinel);
923
9161894
  Assert(!c->hasProof());
924
9161894
  c->d_crid = d_watches->d_constraintProofs.size();
925
9161894
  d_watches->d_constraintProofs.push_back(crp);
926
9161894
}
927
928
1750401
ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){
929
  //This must always return a constraint.
930
931
1750401
  SortedConstraintMap& scm = getVariableSCM(v);
932
1750401
  pair<SortedConstraintMapIterator, bool> insertAttempt;
933
1750401
  insertAttempt = scm.insert(make_pair(r, ValueCollection()));
934
935
1750401
  SortedConstraintMapIterator pos = insertAttempt.first;
936
1750401
  ValueCollection& vc = pos->second;
937
1750401
  if(vc.hasConstraintOfType(t)){
938
1690539
    return vc.getConstraintOfType(t);
939
  }else{
940
59862
    ConstraintP c = new Constraint(v, t, r);
941
59862
    ConstraintP negC = Constraint::makeNegation(v, t, r);
942
943
59862
    SortedConstraintMapIterator negPos;
944
59862
    if(t == Equality || t == Disequality){
945
4438
      negPos = pos;
946
    }else{
947
55424
      pair<SortedConstraintMapIterator, bool> negInsertAttempt;
948
55424
      negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
949
55424
      Assert(negInsertAttempt.second
950
             || !negInsertAttempt.first->second.hasConstraintOfType(
951
                 negC->getType()));
952
55424
      negPos = negInsertAttempt.first;
953
    }
954
955
59862
    c->initialize(this, pos, negC);
956
59862
    negC->initialize(this, negPos, c);
957
958
59862
    vc.add(c);
959
59862
    negPos->second.add(negC);
960
961
59862
    return c;
962
  }
963
}
964
965
279384
ConstraintP ConstraintDatabase::ensureConstraint(ValueCollection& vc, ConstraintType t){
966
279384
  if(vc.hasConstraintOfType(t)){
967
273112
    return vc.getConstraintOfType(t);
968
  }else{
969
6272
    return getConstraint(vc.getVariable(), t, vc.getValue());
970
  }
971
}
972
973
bool ConstraintDatabase::emptyDatabase(const std::vector<PerVariableDatabase>& vec){
974
  std::vector<PerVariableDatabase>::const_iterator first = vec.begin();
975
  std::vector<PerVariableDatabase>::const_iterator last = vec.end();
976
  return std::find_if(first, last, PerVariableDatabase::IsEmpty) == last;
977
}
978
979
17988
ConstraintDatabase::~ConstraintDatabase(){
980
8994
  delete d_watches;
981
982
17988
  std::vector<ConstraintP> constraintList;
983
984
301890
  while(!d_varDatabases.empty()){
985
146448
    PerVariableDatabase* back = d_varDatabases.back();
986
987
146448
    SortedConstraintMap& scm = back->d_constraints;
988
146448
    SortedConstraintMapIterator i = scm.begin(), i_end = scm.end();
989
969218
    for(; i != i_end; ++i){
990
411385
      (i->second).push_into(constraintList);
991
    }
992
1358244
    while(!constraintList.empty()){
993
605898
      ConstraintP c = constraintList.back();
994
605898
      constraintList.pop_back();
995
605898
      delete c;
996
    }
997
146448
    Assert(scm.empty());
998
146448
    d_varDatabases.pop_back();
999
146448
    delete back;
1000
  }
1001
1002
8994
  Assert(d_nodetoConstraintMap.empty());
1003
8994
}
1004
1005
8997
ConstraintDatabase::Statistics::Statistics():
1006
  d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
1007
8997
  d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
1008
{
1009
8997
  smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls);
1010
8997
  smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications);
1011
1012
8997
}
1013
1014
17988
ConstraintDatabase::Statistics::~Statistics(){
1015
8994
  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls);
1016
8994
  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications);
1017
8994
}
1018
1019
void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){
1020
  Assert(c->safeToGarbageCollect());
1021
  ConstraintP neg = c->getNegation();
1022
  Assert(neg->safeToGarbageCollect());
1023
  delete c;
1024
  delete neg;
1025
}
1026
1027
146448
void ConstraintDatabase::addVariable(ArithVar v){
1028
146448
  if(d_reclaimable.isMember(v)){
1029
    SortedConstraintMap& scm = getVariableSCM(v);
1030
1031
    std::vector<ConstraintP> constraintList;
1032
1033
    for(SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end; ++i){
1034
      (i->second).push_into(constraintList);
1035
    }
1036
    while(!constraintList.empty()){
1037
      ConstraintP c = constraintList.back();
1038
      constraintList.pop_back();
1039
      Assert(c->safeToGarbageCollect());
1040
      delete c;
1041
    }
1042
    Assert(scm.empty());
1043
1044
    d_reclaimable.remove(v);
1045
  }else{
1046
146448
    Debug("arith::constraint") << "about to fail" << v << " " << d_varDatabases.size() << endl;
1047
146448
    Assert(v == d_varDatabases.size());
1048
146448
    d_varDatabases.push_back(new PerVariableDatabase(v));
1049
  }
1050
146448
}
1051
1052
void ConstraintDatabase::removeVariable(ArithVar v){
1053
  Assert(!d_reclaimable.isMember(v));
1054
  d_reclaimable.add(v);
1055
}
1056
1057
bool Constraint::safeToGarbageCollect() const{
1058
  // Do not call during destructor as getNegation() may be Null by this point
1059
  Assert(getNegation() != NullConstraint);
1060
  return !contextDependentDataIsSet() && ! getNegation()->contextDependentDataIsSet();
1061
}
1062
1063
607277
bool Constraint::contextDependentDataIsSet() const{
1064
607277
  return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory();
1065
}
1066
1067
14895
TrustNode Constraint::split()
1068
{
1069
14895
  Assert(isEquality() || isDisequality());
1070
1071
14895
  bool isEq = isEquality();
1072
1073
14895
  ConstraintP eq = isEq ? this : d_negation;
1074
14895
  ConstraintP diseq = isEq ? d_negation : this;
1075
1076
29790
  TNode eqNode = eq->getLiteral();
1077
14895
  Assert(eqNode.getKind() == kind::EQUAL);
1078
29790
  TNode lhs = eqNode[0];
1079
29790
  TNode rhs = eqNode[1];
1080
1081
29790
  Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs;
1082
29790
  Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
1083
29790
  Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
1084
29790
  Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs;
1085
1086
29790
  Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode;
1087
1088
14895
  TrustNode trustedLemma;
1089
14895
  if (d_database->isProofEnabled())
1090
  {
1091
    // Farkas proof that this works.
1092
1936
    auto nm = NodeManager::currentNM();
1093
3872
    auto nLeqPf = d_database->d_pnm->mkAssume(leqNode.negate());
1094
1936
    auto gtPf = d_database->d_pnm->mkNode(
1095
3872
        PfRule::MACRO_SR_PRED_TRANSFORM, {nLeqPf}, {gtNode});
1096
3872
    auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate());
1097
1936
    auto ltPf = d_database->d_pnm->mkNode(
1098
3872
        PfRule::MACRO_SR_PRED_TRANSFORM, {nGeqPf}, {ltNode});
1099
1936
    auto sumPf = d_database->d_pnm->mkNode(
1100
        PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
1101
        {gtPf, ltPf},
1102
3872
        {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
1103
1936
    auto botPf = d_database->d_pnm->mkNode(
1104
3872
        PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
1105
3872
    std::vector<Node> a = {leqNode.negate(), geqNode.negate()};
1106
3872
    auto notAndNotPf = d_database->d_pnm->mkScope(botPf, a);
1107
    // No need to ensure that the expected node aggrees with `a` because we are
1108
    // not providing an expected node.
1109
    auto orNotNotPf =
1110
3872
        d_database->d_pnm->mkNode(PfRule::NOT_AND, {notAndNotPf}, {});
1111
1936
    auto orPf = d_database->d_pnm->mkNode(
1112
3872
        PfRule::MACRO_SR_PRED_TRANSFORM, {orNotNotPf}, {lemma});
1113
1936
    trustedLemma = d_database->d_pfGen->mkTrustNode(lemma, orPf);
1114
  }
1115
  else
1116
  {
1117
12959
    trustedLemma = TrustNode::mkTrustLemma(lemma);
1118
  }
1119
1120
14895
  eq->d_database->pushSplitWatch(eq);
1121
14895
  diseq->d_database->pushSplitWatch(diseq);
1122
1123
29790
  return trustedLemma;
1124
}
1125
1126
977865
bool ConstraintDatabase::hasLiteral(TNode literal) const {
1127
977865
  return lookup(literal) != NullConstraint;
1128
}
1129
1130
244466
ConstraintP ConstraintDatabase::addLiteral(TNode literal){
1131
244466
  Assert(!hasLiteral(literal));
1132
244466
  bool isNot = (literal.getKind() == NOT);
1133
488932
  Node atomNode = (isNot ? literal[0] : literal);
1134
488932
  Node negationNode  = atomNode.notNode();
1135
1136
244466
  Assert(!hasLiteral(atomNode));
1137
244466
  Assert(!hasLiteral(negationNode));
1138
488932
  Comparison posCmp = Comparison::parseNormalForm(atomNode);
1139
1140
244466
  ConstraintType posType = Constraint::constraintTypeOfComparison(posCmp);
1141
1142
488932
  Polynomial nvp = posCmp.normalizedVariablePart();
1143
244466
  ArithVar v = d_avariables.asArithVar(nvp.getNode());
1144
1145
488932
  DeltaRational posDR = posCmp.normalizedDeltaRational();
1146
1147
244466
  ConstraintP posC = new Constraint(v, posType, posDR);
1148
1149
244466
  Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl;
1150
244466
  Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
1151
1152
244466
  SortedConstraintMap& scm = getVariableSCM(posC->getVariable());
1153
244466
  pair<SortedConstraintMapIterator, bool> insertAttempt;
1154
244466
  insertAttempt = scm.insert(make_pair(posC->getValue(), ValueCollection()));
1155
1156
244466
  SortedConstraintMapIterator posI = insertAttempt.first;
1157
  // If the attempt succeeds, i points to a new empty ValueCollection
1158
  // If the attempt fails, i points to a pre-existing ValueCollection
1159
1160
244466
  if(posI->second.hasConstraintOfType(posC->getType())){
1161
    //This is the situation where the ConstraintP exists, but
1162
    //the literal has not been  associated with it.
1163
1379
    ConstraintP hit = posI->second.getConstraintOfType(posC->getType());
1164
1379
    Debug("arith::constraint") << "hit " << hit << endl;
1165
1379
    Debug("arith::constraint") << "posC " << posC << endl;
1166
1167
1379
    delete posC;
1168
1169
1379
    hit->setLiteral(atomNode);
1170
1379
    hit->getNegation()->setLiteral(negationNode);
1171
1379
    return isNot ? hit->getNegation(): hit;
1172
  }else{
1173
486174
    Comparison negCmp = Comparison::parseNormalForm(negationNode);
1174
1175
243087
    ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
1176
486174
    DeltaRational negDR = negCmp.normalizedDeltaRational();
1177
1178
243087
    ConstraintP negC = new Constraint(v, negType, negDR);
1179
1180
243087
    SortedConstraintMapIterator negI;
1181
1182
243087
    if(posC->isEquality()){
1183
107969
      negI = posI;
1184
    }else{
1185
135118
      Assert(posC->isLowerBound() || posC->isUpperBound());
1186
1187
135118
      pair<SortedConstraintMapIterator, bool> negInsertAttempt;
1188
135118
      negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
1189
1190
135118
      Debug("nf::tmp") << "sdhjfgdhjkldfgljkhdfg" << endl;
1191
135118
      Debug("nf::tmp") << negC << endl;
1192
135118
      Debug("nf::tmp") << negC->getValue() << endl;
1193
1194
      //This should always succeed as the DeltaRational for the negation is unique!
1195
135118
      Assert(negInsertAttempt.second);
1196
1197
135118
      negI = negInsertAttempt.first;
1198
    }
1199
1200
243087
    (posI->second).add(posC);
1201
243087
    (negI->second).add(negC);
1202
1203
243087
    posC->initialize(this, posI, negC);
1204
243087
    negC->initialize(this, negI, posC);
1205
1206
243087
    posC->setLiteral(atomNode);
1207
243087
    negC->setLiteral(negationNode);
1208
1209
243087
    return isNot ? negC : posC;
1210
  }
1211
}
1212
1213
1214
9725867
ConstraintP ConstraintDatabase::lookup(TNode literal) const{
1215
9725867
  NodetoConstraintMap::const_iterator iter = d_nodetoConstraintMap.find(literal);
1216
9725867
  if(iter == d_nodetoConstraintMap.end()){
1217
1882397
    return NullConstraint;
1218
  }else{
1219
7843470
    return iter->second;
1220
  }
1221
}
1222
1223
4776013
void Constraint::setAssumption(bool nowInConflict){
1224
4776013
  Debug("constraints::pf") << "setAssumption(" << this << ")" << std::endl;
1225
4776013
  Assert(!hasProof());
1226
4776013
  Assert(negationHasProof() == nowInConflict);
1227
4776013
  Assert(hasLiteral());
1228
4776013
  Assert(assertedToTheTheory());
1229
1230
4776013
  d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
1231
1232
4776013
  Assert(inConflict() == nowInConflict);
1233
4776013
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1234
    Debug("constraint::conflictCommit") << "inConflict@setAssumption " << this << std::endl;
1235
  }
1236
4776013
}
1237
1238
4129112
void Constraint::tryToPropagate(){
1239
4129112
  Assert(hasProof());
1240
4129112
  Assert(!isAssumption());
1241
4129112
  Assert(!isInternalAssumption());
1242
1243
4129112
  if(canBePropagated() && !assertedToTheTheory() && !isAssumption() && !isInternalAssumption()){
1244
734543
    propagate();
1245
  }
1246
4129112
}
1247
1248
745567
void Constraint::propagate(){
1249
745567
  Assert(hasProof());
1250
745567
  Assert(canBePropagated());
1251
745567
  Assert(!assertedToTheTheory());
1252
745567
  Assert(!isAssumption());
1253
745567
  Assert(!isInternalAssumption());
1254
1255
745567
  d_database->d_toPropagate.push(this);
1256
745567
}
1257
1258
1259
/*
1260
 * Example:
1261
 *    x <= a and a < b
1262
 * |= x <= b
1263
 * ---
1264
 *  1*(x <= a) + (-1)*(x > b) => (0 <= a-b)
1265
 */
1266
2439947
void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
1267
2439947
  Debug("constraints::pf") << "impliedByUnate(" << this << ", " << *imp << ")" << std::endl;
1268
2439947
  Assert(!hasProof());
1269
2439947
  Assert(imp->hasProof());
1270
2439947
  Assert(negationHasProof() == nowInConflict);
1271
1272
2439947
  d_database->d_antecedents.push_back(NullConstraint);
1273
2439947
  d_database->d_antecedents.push_back(imp);
1274
1275
2439947
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1276
1277
  RationalVectorP coeffs;
1278
2439947
  if (ARITH_PROOF_ON())
1279
  {
1280
318500
    std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
1281
1282
637000
    Rational first(sgns.first);
1283
637000
    Rational second(sgns.second);
1284
1285
318500
    coeffs = new RationalVector();
1286
318500
    coeffs->push_back(first);
1287
318500
    coeffs->push_back(second);
1288
  }
1289
  else
1290
  {
1291
2121447
    coeffs = RationalVectorPSentinel;
1292
  }
1293
  // no need to delete coeffs the memory is owned by ConstraintRule
1294
2439947
  d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
1295
1296
2439947
  Assert(inConflict() == nowInConflict);
1297
2439947
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1298
    Debug("constraint::conflictCommit") << "inConflict@impliedByUnate " << this << std::endl;
1299
  }
1300
1301
2439947
  if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
1302
    getConstraintRule().print(Debug("constraints::wffp"));
1303
  }
1304
2439947
  Assert(wellFormedFarkasProof());
1305
2439947
}
1306
1307
468903
void Constraint::impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool nowInConflict){
1308
468903
  Debug("constraints::pf") << "impliedByTrichotomy(" << this << ", " << *a << ", ";
1309
468903
  Debug("constraints::pf") << *b << ")" << std::endl;
1310
468903
  Assert(!hasProof());
1311
468903
  Assert(negationHasProof() == nowInConflict);
1312
468903
  Assert(a->hasProof());
1313
468903
  Assert(b->hasProof());
1314
1315
468903
  d_database->d_antecedents.push_back(NullConstraint);
1316
468903
  d_database->d_antecedents.push_back(a);
1317
468903
  d_database->d_antecedents.push_back(b);
1318
1319
468903
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1320
468903
  d_database->pushConstraintRule(ConstraintRule(this, TrichotomyAP, antecedentEnd));
1321
1322
468903
  Assert(inConflict() == nowInConflict);
1323
468903
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1324
    Debug("constraint::conflictCommit") << "inConflict@impliedByTrichotomy " << this << std::endl;
1325
  }
1326
468903
}
1327
1328
1329
94918
bool Constraint::allHaveProof(const ConstraintCPVec& b){
1330
1366398
  for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
1331
1271480
    ConstraintCP cp = *i;
1332
1271480
    if(! (cp->hasProof())){ return false; }
1333
  }
1334
94918
  return true;
1335
}
1336
1337
1198105
void Constraint::impliedByIntTighten(ConstraintCP a, bool nowInConflict){
1338
1198105
  Debug("constraints::pf") << "impliedByIntTighten(" << this << ", " << *a << ")" << std::endl;
1339
1198105
  Assert(!hasProof());
1340
1198105
  Assert(negationHasProof() == nowInConflict);
1341
1198105
  Assert(a->hasProof());
1342
2396210
  Debug("pf::arith") << "impliedByIntTighten(" << this << ", " << a << ")"
1343
1198105
                     << std::endl;
1344
1345
1198105
  d_database->d_antecedents.push_back(NullConstraint);
1346
1198105
  d_database->d_antecedents.push_back(a);
1347
1198105
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1348
1198105
  d_database->pushConstraintRule(ConstraintRule(this, IntTightenAP, antecedentEnd));
1349
1350
1198105
  Assert(inConflict() == nowInConflict);
1351
1198105
  if(inConflict()){
1352
4133
    Debug("constraint::conflictCommit") << "inConflict impliedByIntTighten" << this << std::endl;
1353
  }
1354
1198105
}
1355
1356
void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
1357
  Debug("constraints::pf") << "impliedByIntHole(" << this << ", " << *a << ")" << std::endl;
1358
  Assert(!hasProof());
1359
  Assert(negationHasProof() == nowInConflict);
1360
  Assert(a->hasProof());
1361
  Debug("pf::arith") << "impliedByIntHole(" << this << ", " << a << ")"
1362
                     << std::endl;
1363
1364
  d_database->d_antecedents.push_back(NullConstraint);
1365
  d_database->d_antecedents.push_back(a);
1366
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1367
  d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
1368
1369
  Assert(inConflict() == nowInConflict);
1370
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1371
    Debug("constraint::conflictCommit") << "inConflict impliedByIntHole" << this << std::endl;
1372
  }
1373
}
1374
1375
void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){
1376
  Debug("constraints::pf") << "impliedByIntHole(" << this;
1377
  if (Debug.isOn("constraints::pf")) {
1378
    for (const ConstraintCP& p : b)
1379
    {
1380
      Debug("constraints::pf") << ", " << p;
1381
    }
1382
  }
1383
  Debug("constraints::pf") << ")" << std::endl;
1384
1385
  Assert(!hasProof());
1386
  Assert(negationHasProof() == nowInConflict);
1387
  Assert(allHaveProof(b));
1388
1389
  CDConstraintList& antecedents = d_database->d_antecedents;
1390
  antecedents.push_back(NullConstraint);
1391
  for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
1392
    antecedents.push_back(*i);
1393
  }
1394
  AntecedentId antecedentEnd = antecedents.size() - 1;
1395
1396
  d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
1397
1398
  Assert(inConflict() == nowInConflict);
1399
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1400
    Debug("constraint::conflictCommit") << "inConflict@impliedByIntHole[vec] " << this << std::endl;
1401
  }
1402
}
1403
1404
/*
1405
 * If proofs are off, coeffs == RationalVectorSentinal.
1406
 * If proofs are on,
1407
 *   coeffs != RationalVectorSentinal,
1408
 *   coeffs->size() = a.size() + 1,
1409
 *   for i in [0,a.size) : coeff[i] corresponds to a[i], and
1410
 *   coeff.back() corresponds to the current constraint.
1411
 */
1412
94918
void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coeffs, bool nowInConflict){
1413
94918
  Debug("constraints::pf") << "impliedByFarkas(" << this;
1414
94918
  if (Debug.isOn("constraints::pf")) {
1415
    for (const ConstraintCP& p : a)
1416
    {
1417
      Debug("constraints::pf") << ", " << p;
1418
    }
1419
  }
1420
94918
  Debug("constraints::pf") << ", <coeffs>";
1421
94918
  Debug("constraints::pf") << ")" << std::endl;
1422
94918
  Assert(!hasProof());
1423
94918
  Assert(negationHasProof() == nowInConflict);
1424
94918
  Assert(allHaveProof(a));
1425
1426
94918
  Assert(ARITH_PROOF_ON() == (coeffs != RationalVectorCPSentinel));
1427
94918
  Assert(!ARITH_PROOF_ON() || coeffs->size() == a.size() + 1);
1428
1429
94918
  Assert(a.size() >= 1);
1430
1431
94918
  d_database->d_antecedents.push_back(NullConstraint);
1432
1366398
  for(ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
1433
1271480
    ConstraintCP c_i = *i;
1434
1271480
    Assert(c_i->hasProof());
1435
1271480
    d_database->d_antecedents.push_back(c_i);
1436
  }
1437
94918
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1438
1439
  RationalVectorCP coeffsCopy;
1440
94918
  if (ARITH_PROOF_ON())
1441
  {
1442
11769
    Assert(coeffs != RationalVectorCPSentinel);
1443
11769
    coeffsCopy = new RationalVector(*coeffs);
1444
  }
1445
  else
1446
  {
1447
83149
    coeffsCopy = RationalVectorCPSentinel;
1448
  }
1449
94918
  d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
1450
1451
94918
  Assert(inConflict() == nowInConflict);
1452
94918
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1453
    Debug("constraint::conflictCommit") << "inConflict@impliedByFarkas " << this << std::endl;
1454
  }
1455
94918
  if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
1456
    getConstraintRule().print(Debug("constraints::wffp"));
1457
  }
1458
94918
  Assert(wellFormedFarkasProof());
1459
94918
}
1460
1461
1462
void Constraint::setInternalAssumption(bool nowInConflict){
1463
  Debug("constraints::pf") << "setInternalAssumption(" << this;
1464
  Debug("constraints::pf") << ")" << std::endl;
1465
  Assert(!hasProof());
1466
  Assert(negationHasProof() == nowInConflict);
1467
  Assert(!assertedToTheTheory());
1468
1469
  d_database->pushConstraintRule(ConstraintRule(this, InternalAssumeAP));
1470
1471
  Assert(inConflict() == nowInConflict);
1472
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1473
    Debug("constraint::conflictCommit") << "inConflict@setInternalAssumption " << this << std::endl;
1474
  }
1475
}
1476
1477
1478
184008
void Constraint::setEqualityEngineProof(){
1479
184008
  Debug("constraints::pf") << "setEqualityEngineProof(" << this;
1480
184008
  Debug("constraints::pf") << ")" << std::endl;
1481
184008
  Assert(truthIsUnknown());
1482
184008
  Assert(hasLiteral());
1483
184008
  d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
1484
184008
}
1485
1486
1487
3932309
SortedConstraintMap& Constraint::constraintSet() const{
1488
3932309
  Assert(d_database->variableDatabaseIsSetup(d_variable));
1489
3932309
  return (d_database->d_varDatabases[d_variable])->d_constraints;
1490
}
1491
1492
bool Constraint::antecentListIsEmpty() const{
1493
  Assert(hasProof());
1494
  return d_database->d_antecedents[getEndAntecedent()] == NullConstraint;
1495
}
1496
1497
bool Constraint::antecedentListLengthIsOne() const {
1498
  Assert(hasProof());
1499
  return !antecentListIsEmpty() &&
1500
    d_database->d_antecedents[getEndAntecedent()-1] == NullConstraint;
1501
}
1502
1503
93591
Node Constraint::externalImplication(const ConstraintCPVec& b) const{
1504
93591
  Assert(hasLiteral());
1505
187182
  Node antecedent = externalExplainByAssertions(b);
1506
187182
  Node implied = getLiteral();
1507
187182
  return antecedent.impNode(implied);
1508
}
1509
1510
1511
1053748
Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
1512
1053748
  return externalExplain(b, AssertionOrderSentinel);
1513
}
1514
1515
13396
TrustNode Constraint::externalExplainForPropagation(TNode lit) const
1516
{
1517
13396
  Assert(hasProof());
1518
13396
  Assert(!isAssumption());
1519
13396
  Assert(!isInternalAssumption());
1520
26792
  NodeBuilder<> nb(Kind::AND);
1521
26792
  auto pfFromAssumptions = externalExplain(nb, d_assertionOrder);
1522
26792
  Node n = safeConstructNary(nb);
1523
13396
  if (d_database->isProofEnabled())
1524
  {
1525
    // Check that the literal we're explaining via this constraint actually
1526
    // matches the constraint's canonical literal.
1527
1540
    Assert(Rewriter::rewrite(lit) == getLiteral());
1528
3080
    std::vector<Node> assumptions;
1529
1540
    if (n.getKind() == Kind::AND)
1530
    {
1531
932
      assumptions.insert(assumptions.end(), n.begin(), n.end());
1532
    }
1533
    else
1534
    {
1535
608
      assumptions.push_back(n);
1536
    }
1537
1540
    if (getProofLiteral() != lit)
1538
    {
1539
3147
      pfFromAssumptions = d_database->d_pnm->mkNode(
1540
2098
          PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {lit});
1541
    }
1542
3080
    auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
1543
1540
    return d_database->d_pfGen->mkTrustedPropagation(
1544
1540
        lit, safeConstructNary(Kind::AND, assumptions), pf);
1545
  }
1546
  else
1547
  {
1548
11856
    return TrustNode::mkTrustPropExp(lit, n);
1549
  }
1550
}
1551
1552
82837
TrustNode Constraint::externalExplainConflict() const
1553
{
1554
82837
  Debug("pf::arith::explain") << this << std::endl;
1555
82837
  Assert(inConflict());
1556
165674
  NodeBuilder<> nb(kind::AND);
1557
165674
  auto pf1 = externalExplainByAssertions(nb);
1558
165674
  auto not2 = getNegation()->getProofLiteral().negate();
1559
165674
  auto pf2 = getNegation()->externalExplainByAssertions(nb);
1560
165674
  Node n = safeConstructNary(nb);
1561
82837
  if (d_database->isProofEnabled())
1562
  {
1563
10834
    auto pfNot2 = d_database->d_pnm->mkNode(
1564
21668
        PfRule::MACRO_SR_PRED_TRANSFORM, {pf1}, {not2});
1565
21668
    std::vector<Node> lits;
1566
10834
    if (n.getKind() == Kind::AND)
1567
    {
1568
10834
      lits.insert(lits.end(), n.begin(), n.end());
1569
    }
1570
    else
1571
    {
1572
      lits.push_back(n);
1573
    }
1574
10834
    if (Debug.isOn("arith::pf::externalExplainConflict"))
1575
    {
1576
      Debug("arith::pf::externalExplainConflict") << "Lits:" << std::endl;
1577
      for (const auto& l : lits)
1578
      {
1579
        Debug("arith::pf::externalExplainConflict") << "  : " << l << std::endl;
1580
      }
1581
    }
1582
    std::vector<Node> contraLits = {getProofLiteral(),
1583
21668
                                    getNegation()->getProofLiteral()};
1584
    auto bot =
1585
10834
        not2.getKind() == Kind::NOT
1586
29418
            ? d_database->d_pnm->mkNode(PfRule::CONTRA, {pf2, pfNot2}, {})
1587
42308
            : d_database->d_pnm->mkNode(PfRule::CONTRA, {pfNot2, pf2}, {});
1588
10834
    if (Debug.isOn("arith::pf::tree"))
1589
    {
1590
      Debug("arith::pf::tree") << *this << std::endl;
1591
      Debug("arith::pf::tree") << *getNegation() << std::endl;
1592
      Debug("arith::pf::tree") << "\n\nTree:\n";
1593
      printProofTree(Debug("arith::pf::tree"));
1594
      getNegation()->printProofTree(Debug("arith::pf::tree"));
1595
    }
1596
21668
    auto confPf = d_database->d_pnm->mkScope(bot, lits);
1597
10834
    return d_database->d_pfGen->mkTrustNode(
1598
10834
        safeConstructNary(Kind::AND, lits), confPf, true);
1599
  }
1600
  else
1601
  {
1602
72003
    return TrustNode::mkTrustConflict(n);
1603
  }
1604
}
1605
1606
struct ConstraintCPHash {
1607
  /* Todo replace with an id */
1608
  size_t operator()(ConstraintCP c) const{
1609
    Assert(sizeof(ConstraintCP) > 0);
1610
    return ((size_t)c)/sizeof(ConstraintCP);
1611
  }
1612
};
1613
1614
void Constraint::assertionFringe(ConstraintCPVec& v){
1615
  unordered_set<ConstraintCP, ConstraintCPHash> visited;
1616
  size_t writePos = 0;
1617
1618
  if(!v.empty()){
1619
    const ConstraintDatabase* db = v.back()->d_database;
1620
    const CDConstraintList& antecedents = db->d_antecedents;
1621
    for(size_t i = 0; i < v.size(); ++i){
1622
      ConstraintCP vi = v[i];
1623
      if(visited.find(vi) == visited.end()){
1624
        Assert(vi->hasProof());
1625
        visited.insert(vi);
1626
        if(vi->onFringe()){
1627
          v[writePos] = vi;
1628
          writePos++;
1629
        }else{
1630
          Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof()
1631
                 || vi->hasIntHoleProof() || vi->hasIntTightenProof());
1632
          AntecedentId p = vi->getEndAntecedent();
1633
1634
          ConstraintCP antecedent = antecedents[p];
1635
          while(antecedent != NullConstraint){
1636
            v.push_back(antecedent);
1637
            --p;
1638
            antecedent = antecedents[p];
1639
          }
1640
        }
1641
      }
1642
    }
1643
    v.resize(writePos);
1644
  }
1645
}
1646
1647
void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
1648
  o.insert(o.end(), i.begin(), i.end());
1649
  assertionFringe(o);
1650
}
1651
1652
1053748
Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
1653
2107496
  NodeBuilder<> nb(kind::AND);
1654
1053748
  ConstraintCPVec::const_iterator i, end;
1655
2324862
  for(i = v.begin(), end = v.end(); i != end; ++i){
1656
1271114
    ConstraintCP v_i = *i;
1657
1271114
    v_i->externalExplain(nb, order);
1658
  }
1659
2107496
  return safeConstructNary(nb);
1660
}
1661
1662
5514271
std::shared_ptr<ProofNode> Constraint::externalExplain(
1663
    NodeBuilder<>& nb, AssertionOrder order) const
1664
{
1665
5514271
  if (Debug.isOn("pf::arith::explain"))
1666
  {
1667
    this->printProofTree(Debug("arith::pf::tree"));
1668
    Debug("pf::arith::explain") << "Explaining: " << this << " with rule ";
1669
    getConstraintRule().print(Debug("pf::arith::explain"));
1670
    Debug("pf::arith::explain") << std::endl;
1671
  }
1672
5514271
  Assert(hasProof());
1673
5514271
  Assert(!isAssumption() || assertedToTheTheory());
1674
5514271
  Assert(!isInternalAssumption());
1675
5514271
  std::shared_ptr<ProofNode> pf{};
1676
1677
5514271
  ProofNodeManager* pnm = d_database->d_pnm;
1678
1679
5514271
  if (assertedBefore(order))
1680
  {
1681
4906389
    Debug("pf::arith::explain") << "  already asserted" << std::endl;
1682
4906389
    nb << getWitness();
1683
4906389
    if (d_database->isProofEnabled())
1684
    {
1685
478269
      pf = pnm->mkAssume(getWitness());
1686
      // If the witness and literal differ, prove the difference through a
1687
      // rewrite.
1688
478269
      if (getWitness() != getProofLiteral())
1689
      {
1690
924450
        pf = pnm->mkNode(
1691
616300
            PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {getProofLiteral()});
1692
      }
1693
    }
1694
  }
1695
607882
  else if (hasEqualityEngineProof())
1696
  {
1697
5958
    Debug("pf::arith::explain") << "  going to ee:" << std::endl;
1698
11916
    TrustNode exp = d_database->eeExplain(this);
1699
5958
    if (d_database->isProofEnabled())
1700
    {
1701
551
      Assert(exp.getProven().getKind() == Kind::IMPLIES);
1702
1102
      std::vector<std::shared_ptr<ProofNode>> hypotheses;
1703
551
      hypotheses.push_back(exp.getGenerator()->getProofFor(exp.getProven()));
1704
551
      if (exp.getNode().getKind() == Kind::AND)
1705
      {
1706
1793
        for (const auto& h : exp.getNode())
1707
        {
1708
1320
          hypotheses.push_back(
1709
2640
              pnm->mkNode(PfRule::TRUE_INTRO, {pnm->mkAssume(h)}, {}));
1710
        }
1711
      }
1712
      else
1713
      {
1714
312
        hypotheses.push_back(pnm->mkNode(
1715
234
            PfRule::TRUE_INTRO, {pnm->mkAssume(exp.getNode())}, {}));
1716
      }
1717
1102
      pf = pnm->mkNode(
1718
551
          PfRule::MACRO_SR_PRED_TRANSFORM, {hypotheses}, {getProofLiteral()});
1719
    }
1720
11916
    Debug("pf::arith::explain")
1721
5958
        << "    explanation: " << exp.getNode() << std::endl;
1722
5958
    if (exp.getNode().getKind() == Kind::AND)
1723
    {
1724
5274
      nb.append(exp.getNode().begin(), exp.getNode().end());
1725
    }
1726
    else
1727
    {
1728
684
      nb << exp.getNode();
1729
    }
1730
  }
1731
  else
1732
  {
1733
601924
    Debug("pf::arith::explain") << "  recursion!" << std::endl;
1734
601924
    Assert(!isAssumption());
1735
601924
    AntecedentId p = getEndAntecedent();
1736
601924
    ConstraintCP antecedent = d_database->d_antecedents[p];
1737
1203848
    std::vector<std::shared_ptr<ProofNode>> children;
1738
1739
3505010
    while (antecedent != NullConstraint)
1740
    {
1741
1451543
      Debug("pf::arith::explain") << "Explain " << antecedent << std::endl;
1742
2903086
      auto pn = antecedent->externalExplain(nb, order);
1743
1451543
      if (d_database->isProofEnabled())
1744
      {
1745
116447
        children.push_back(pn);
1746
      }
1747
1451543
      --p;
1748
1451543
      antecedent = d_database->d_antecedents[p];
1749
    }
1750
1751
601924
    if (d_database->isProofEnabled())
1752
    {
1753
72544
      switch (getProofType())
1754
      {
1755
        case ArithProofType::AssumeAP:
1756
        case ArithProofType::EqualityEngineAP:
1757
        {
1758
          Unreachable() << "These should be handled above";
1759
          break;
1760
        }
1761
10845
        case ArithProofType::FarkasAP:
1762
        {
1763
          // Per docs in constraint.h,
1764
          // the 0th farkas coefficient is for the negation of the deduced
1765
          // constraint the 1st corresponds to the last antecedent the nth
1766
          // corresponds to the first antecedent Then, the farkas coefficients
1767
          // and the antecedents are in the same order.
1768
1769
          // Enumerate child proofs (negation included) in d_farkasCoefficients
1770
          // order
1771
21690
          std::vector<std::shared_ptr<ProofNode>> farkasChildren;
1772
10845
          farkasChildren.push_back(
1773
21690
              pnm->mkAssume(getNegation()->getProofLiteral()));
1774
10845
          farkasChildren.insert(
1775
21690
              farkasChildren.end(), children.rbegin(), children.rend());
1776
1777
10845
          NodeManager* nm = NodeManager::currentNM();
1778
1779
          // Enumerate d_farkasCoefficients as nodes.
1780
21690
          std::vector<Node> farkasCoeffs;
1781
72406
          for (Rational r : *getFarkasCoefficients())
1782
          {
1783
61561
            farkasCoeffs.push_back(nm->mkConst<Rational>(r));
1784
          }
1785
1786
          // Apply the scaled-sum rule.
1787
          std::shared_ptr<ProofNode> sumPf =
1788
              pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
1789
                          farkasChildren,
1790
21690
                          farkasCoeffs);
1791
1792
          // Provable rewrite the result
1793
          auto botPf = pnm->mkNode(
1794
21690
              PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
1795
1796
          // Scope out the negated constraint, yielding a proof of the
1797
          // constraint.
1798
21690
          std::vector<Node> assump{getNegation()->getProofLiteral()};
1799
21690
          auto maybeDoubleNotPf = pnm->mkScope(botPf, assump, false);
1800
1801
          // No need to ensure that the expected node aggrees with `assump`
1802
          // because we are not providing an expected node.
1803
          //
1804
          // Prove that this is the literal (may need to clean a double-not)
1805
32535
          pf = pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
1806
                           {maybeDoubleNotPf},
1807
21690
                           {getProofLiteral()});
1808
1809
10845
          break;
1810
        }
1811
57667
        case ArithProofType::IntTightenAP:
1812
        {
1813
57667
          if (isUpperBound())
1814
          {
1815
56468
            pf = pnm->mkNode(
1816
112936
                PfRule::INT_TIGHT_UB, children, {}, getProofLiteral());
1817
          }
1818
1199
          else if (isLowerBound())
1819
          {
1820
1199
            pf = pnm->mkNode(
1821
2398
                PfRule::INT_TIGHT_LB, children, {}, getProofLiteral());
1822
          }
1823
          else
1824
          {
1825
            Unreachable();
1826
          }
1827
57667
          break;
1828
        }
1829
        case ArithProofType::IntHoleAP:
1830
        {
1831
          pf = pnm->mkNode(PfRule::INT_TRUST,
1832
                           children,
1833
                           {getProofLiteral()},
1834
                           getProofLiteral());
1835
          break;
1836
        }
1837
4032
        case ArithProofType::TrichotomyAP:
1838
        {
1839
8064
          pf = pnm->mkNode(PfRule::ARITH_TRICHOTOMY,
1840
                           children,
1841
                           {getProofLiteral()},
1842
12096
                           getProofLiteral());
1843
4032
          break;
1844
        }
1845
        case ArithProofType::InternalAssumeAP:
1846
        case ArithProofType::NoAP:
1847
        default:
1848
        {
1849
          Unreachable() << getProofType()
1850
                        << " should not be visible in explanation";
1851
          break;
1852
        }
1853
      }
1854
    }
1855
  }
1856
5514271
  return pf;
1857
}
1858
1859
1391
Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
1860
2782
  NodeBuilder<> nb(kind::AND);
1861
1391
  a->externalExplainByAssertions(nb);
1862
1391
  b->externalExplainByAssertions(nb);
1863
2782
  return nb;
1864
}
1865
1866
Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){
1867
  NodeBuilder<> nb(kind::AND);
1868
  a->externalExplainByAssertions(nb);
1869
  b->externalExplainByAssertions(nb);
1870
  c->externalExplainByAssertions(nb);
1871
  return nb;
1872
}
1873
1874
701478
ConstraintP Constraint::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const {
1875
701478
  Assert(initialized());
1876
701478
  Assert(!asserted || hasLiteral);
1877
1878
701478
  SortedConstraintMapConstIterator i = d_variablePosition;
1879
701478
  const SortedConstraintMap& scm = constraintSet();
1880
701478
  SortedConstraintMapConstIterator i_begin = scm.begin();
1881
2277508
  while(i != i_begin){
1882
910880
    --i;
1883
910880
    const ValueCollection& vc = i->second;
1884
910880
    if(vc.hasLowerBound()){
1885
236602
      ConstraintP weaker = vc.getLowerBound();
1886
1887
      // asserted -> hasLiteral
1888
      // hasLiteral -> weaker->hasLiteral()
1889
      // asserted -> weaker->assertedToTheTheory()
1890
489198
      if((!hasLiteral || (weaker->hasLiteral())) &&
1891
258354
         (!asserted || ( weaker->assertedToTheTheory()))){
1892
122865
        return weaker;
1893
      }
1894
    }
1895
  }
1896
578613
  return NullConstraint;
1897
}
1898
1899
336558
ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const {
1900
336558
  SortedConstraintMapConstIterator i = d_variablePosition;
1901
336558
  const SortedConstraintMap& scm = constraintSet();
1902
336558
  SortedConstraintMapConstIterator i_end = scm.end();
1903
1904
336558
  ++i;
1905
1001282
  for(; i != i_end; ++i){
1906
439911
    const ValueCollection& vc = i->second;
1907
439911
    if(vc.hasUpperBound()){
1908
142165
      ConstraintP weaker = vc.getUpperBound();
1909
364851
      if((!hasLiteral || (weaker->hasLiteral())) &&
1910
226310
         (!asserted || ( weaker->assertedToTheTheory()))){
1911
107549
        return weaker;
1912
      }
1913
    }
1914
  }
1915
1916
229009
  return NullConstraint;
1917
}
1918
1919
7562258
ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const {
1920
7562258
  Assert(variableDatabaseIsSetup(v));
1921
7562258
  Assert(t == UpperBound || t == LowerBound);
1922
1923
7562258
  SortedConstraintMap& scm = getVariableSCM(v);
1924
7562258
  if(t == UpperBound){
1925
3774397
    SortedConstraintMapConstIterator i = scm.lower_bound(r);
1926
3774397
    SortedConstraintMapConstIterator i_end = scm.end();
1927
3774397
    Assert(i == i_end || r <= i->first);
1928
7836729
    for(; i != i_end; i++){
1929
3416775
      Assert(r <= i->first);
1930
3416775
      const ValueCollection& vc = i->second;
1931
3416775
      if(vc.hasUpperBound()){
1932
1385609
        return vc.getUpperBound();
1933
      }
1934
    }
1935
2388788
    return NullConstraint;
1936
  }else{
1937
3787861
    Assert(t == LowerBound);
1938
3787861
    if(scm.empty()){
1939
228931
      return NullConstraint;
1940
    }else{
1941
3558930
      SortedConstraintMapConstIterator i = scm.lower_bound(r);
1942
3558930
      SortedConstraintMapConstIterator i_begin = scm.begin();
1943
3558930
      SortedConstraintMapConstIterator i_end = scm.end();
1944
3558930
      Assert(i == i_end || r <= i->first);
1945
1946
3558930
      int fdj = 0;
1947
1948
3558930
      if(i == i_end){
1949
1379632
        --i;
1950
1379632
        Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1951
2179298
      }else if( (i->first) > r){
1952
561884
        if(i == i_begin){
1953
508967
          return NullConstraint;
1954
        }else{
1955
52917
          --i;
1956
52917
          Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1957
        }
1958
      }
1959
1960
      do{
1961
3506392
        Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1962
3506392
        Assert(r >= i->first);
1963
3506392
        const ValueCollection& vc = i->second;
1964
1965
3506392
        if(vc.hasLowerBound()){
1966
1541380
          return vc.getLowerBound();
1967
        }
1968
1969
1965012
        if(i == i_begin){
1970
1508583
          break;
1971
        }else{
1972
456429
          --i;
1973
456429
        }
1974
      }while(true);
1975
1508583
      return NullConstraint;
1976
    }
1977
  }
1978
}
1979
5958
TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const
1980
{
1981
5958
  Assert(c->hasLiteral());
1982
5958
  return d_congruenceManager.explain(c->getLiteral());
1983
}
1984
1985
void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder<>& nb) const
1986
{
1987
  Assert(c->hasLiteral());
1988
  // NOTE: this is not a recommended method since it ignores proofs
1989
  d_congruenceManager.explain(c->getLiteral(), nb);
1990
}
1991
1992
21575419
bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
1993
21575419
  return v < d_varDatabases.size();
1994
}
1995
1996
1997
8997
ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext):
1998
  d_constraintProofs(satContext),
1999
  d_canBePropagatedWatches(satContext),
2000
  d_assertionOrderWatches(satContext),
2001
8997
  d_splitWatches(userContext)
2002
8997
{}
2003
2004
2005
488932
void Constraint::setLiteral(Node n) {
2006
488932
  Debug("arith::constraint") << "Mapping " << *this << " to " << n << std::endl;
2007
488932
  Assert(Comparison::isNormalAtom(n));
2008
488932
  Assert(!hasLiteral());
2009
488932
  Assert(sanityChecking(n));
2010
488932
  d_literal = n;
2011
488932
  NodetoConstraintMap& map = d_database->d_nodetoConstraintMap;
2012
488932
  Assert(map.find(n) == map.end());
2013
488932
  map.insert(make_pair(d_literal, this));
2014
488932
}
2015
2016
1037927
Node Constraint::getProofLiteral() const
2017
{
2018
1037927
  Assert(d_database != nullptr);
2019
1037927
  Assert(d_database->d_avariables.hasNode(d_variable));
2020
2075854
  Node varPart = d_database->d_avariables.asNode(d_variable);
2021
  Kind cmp;
2022
1037927
  bool neg = false;
2023
1037927
  switch (d_type)
2024
  {
2025
428319
    case ConstraintType::UpperBound:
2026
    {
2027
428319
      if (d_value.infinitesimalIsZero())
2028
      {
2029
134534
        cmp = Kind::LEQ;
2030
      }
2031
      else
2032
      {
2033
293785
        cmp = Kind::LT;
2034
      }
2035
428319
      break;
2036
    }
2037
195951
    case ConstraintType::LowerBound:
2038
    {
2039
195951
      if (d_value.infinitesimalIsZero())
2040
      {
2041
156308
        cmp = Kind::GEQ;
2042
      }
2043
      else
2044
      {
2045
39643
        cmp = Kind::GT;
2046
      }
2047
195951
      break;
2048
    }
2049
322106
    case ConstraintType::Equality:
2050
    {
2051
322106
      cmp = Kind::EQUAL;
2052
322106
      break;
2053
    }
2054
91551
    case ConstraintType::Disequality:
2055
    {
2056
91551
      cmp = Kind::EQUAL;
2057
91551
      neg = true;
2058
91551
      break;
2059
    }
2060
    default: Unreachable() << d_type;
2061
  }
2062
1037927
  NodeManager* nm = NodeManager::currentNM();
2063
2075854
  Node constPart = nm->mkConst<Rational>(d_value.getNoninfinitesimalPart());
2064
2075854
  Node posLit = nm->mkNode(cmp, varPart, constPart);
2065
2075854
  return neg ? posLit.negate() : posLit;
2066
}
2067
2068
38102
void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
2069
                                 ConstraintP a,
2070
                                 ConstraintP b,
2071
                                 bool negateSecond) const
2072
{
2073
76204
  Node la = a->getLiteral();
2074
76204
  Node lb = b->getLiteral();
2075
76204
  Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la);
2076
38102
  if (isProofEnabled())
2077
  {
2078
5542
    Assert(b->getNegation()->getType() != ConstraintType::Disequality);
2079
5542
    auto nm = NodeManager::currentNM();
2080
5542
    auto pf_neg_la = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
2081
11084
                                   {d_pnm->mkAssume(la.negate())},
2082
22168
                                   {a->getNegation()->getProofLiteral()});
2083
5542
    auto pf_neg_lb = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
2084
11084
                                   {d_pnm->mkAssume(lb.negate())},
2085
22168
                                   {b->getNegation()->getProofLiteral()});
2086
5542
    int sndSign = negateSecond ? -1 : 1;
2087
    auto bot_pf =
2088
5542
        d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
2089
5542
                      {d_pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
2090
                                     {pf_neg_la, pf_neg_lb},
2091
                                     {nm->mkConst<Rational>(-1 * sndSign),
2092
22168
                                      nm->mkConst<Rational>(sndSign)})},
2093
27710
                      {nm->mkConst(false)});
2094
11084
    std::vector<Node> as;
2095
16626
    std::transform(orN.begin(), orN.end(), std::back_inserter(as), [](Node n) {
2096
      return n.negate();
2097
16626
    });
2098
    // No need to ensure that the expected node aggrees with `as` because we
2099
    // are not providing an expected node.
2100
5542
    auto pf = d_pnm->mkNode(
2101
        PfRule::MACRO_SR_PRED_TRANSFORM,
2102
16626
        {d_pnm->mkNode(PfRule::NOT_AND, {d_pnm->mkScope(bot_pf, as)}, {})},
2103
27710
        {orN});
2104
5542
    out.push_back(d_pfGen->mkTrustNode(orN, pf));
2105
  }
2106
  else
2107
  {
2108
32560
    out.push_back(TrustNode::mkTrustLemma(orN));
2109
  }
2110
38102
}
2111
2112
36216
void ConstraintDatabase::implies(std::vector<TrustNode>& out,
2113
                                 ConstraintP a,
2114
                                 ConstraintP b) const
2115
{
2116
72432
  Node la = a->getLiteral();
2117
72432
  Node lb = b->getLiteral();
2118
2119
72432
  Node neg_la = (la.getKind() == kind::NOT)? la[0] : la.notNode();
2120
2121
36216
  Assert(lb != neg_la);
2122
36216
  Assert(b->getNegation()->getType() == ConstraintType::LowerBound
2123
         || b->getNegation()->getType() == ConstraintType::UpperBound);
2124
36216
  proveOr(out,
2125
          a->getNegation(),
2126
          b,
2127
36216
          b->getNegation()->getType() == ConstraintType::LowerBound);
2128
36216
}
2129
2130
1886
void ConstraintDatabase::mutuallyExclusive(std::vector<TrustNode>& out,
2131
                                           ConstraintP a,
2132
                                           ConstraintP b) const
2133
{
2134
3772
  Node la = a->getLiteral();
2135
3772
  Node lb = b->getLiteral();
2136
2137
3772
  Node neg_la = la.negate();
2138
3772
  Node neg_lb = lb.negate();
2139
1886
  proveOr(out, a->getNegation(), b->getNegation(), true);
2140
1886
}
2141
2142
56171
void ConstraintDatabase::outputUnateInequalityLemmas(
2143
    std::vector<TrustNode>& out, ArithVar v) const
2144
{
2145
56171
  SortedConstraintMap& scm = getVariableSCM(v);
2146
56171
  SortedConstraintMapConstIterator scm_iter = scm.begin();
2147
56171
  SortedConstraintMapConstIterator scm_end = scm.end();
2148
56171
  ConstraintP prev = NullConstraint;
2149
  //get transitive unates
2150
  //Only lower bounds or upperbounds should be done.
2151
309661
  for(; scm_iter != scm_end; ++scm_iter){
2152
126745
    const ValueCollection& vc = scm_iter->second;
2153
126745
    if(vc.hasUpperBound()){
2154
61962
      ConstraintP ub = vc.getUpperBound();
2155
61962
      if(ub->hasLiteral()){
2156
61962
        if(prev != NullConstraint){
2157
29448
          implies(out, prev, ub);
2158
        }
2159
61962
        prev = ub;
2160
      }
2161
    }
2162
  }
2163
56171
}
2164
2165
56171
void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<TrustNode>& out,
2166
                                                   ArithVar v) const
2167
{
2168
112342
  vector<ConstraintP> equalities;
2169
2170
56171
  SortedConstraintMap& scm = getVariableSCM(v);
2171
56171
  SortedConstraintMapConstIterator scm_iter = scm.begin();
2172
56171
  SortedConstraintMapConstIterator scm_end = scm.end();
2173
2174
309661
  for(; scm_iter != scm_end; ++scm_iter){
2175
126745
    const ValueCollection& vc = scm_iter->second;
2176
126745
    if(vc.hasEquality()){
2177
15753
      ConstraintP eq = vc.getEquality();
2178
15753
      if(eq->hasLiteral()){
2179
15753
        equalities.push_back(eq);
2180
      }
2181
    }
2182
  }
2183
2184
56171
  vector<ConstraintP>::const_iterator i, j, eq_end = equalities.end();
2185
71924
  for(i = equalities.begin(); i != eq_end; ++i){
2186
15753
    ConstraintP at_i = *i;
2187
17639
    for(j= i + 1; j != eq_end; ++j){
2188
1886
      ConstraintP at_j = *j;
2189
2190
1886
      mutuallyExclusive(out, at_i, at_j);
2191
    }
2192
  }
2193
2194
71924
  for(i = equalities.begin(); i != eq_end; ++i){
2195
15753
    ConstraintP eq = *i;
2196
15753
    const ValueCollection& vc = eq->getValueCollection();
2197
15753
    Assert(vc.hasEquality() && vc.getEquality()->hasLiteral());
2198
2199
15753
    bool hasLB = vc.hasLowerBound() && vc.getLowerBound()->hasLiteral();
2200
15753
    bool hasUB = vc.hasUpperBound() && vc.getUpperBound()->hasLiteral();
2201
2202
15753
    ConstraintP lb = hasLB ?
2203
15753
      vc.getLowerBound() : eq->getStrictlyWeakerLowerBound(true, false);
2204
15753
    ConstraintP ub = hasUB ?
2205
15753
      vc.getUpperBound() : eq->getStrictlyWeakerUpperBound(true, false);
2206
2207
15753
    if(hasUB && hasLB && !eq->isSplit()){
2208
115
      out.push_back(eq->split());
2209
    }
2210
15753
    if(lb != NullConstraint){
2211
2615
      implies(out, eq, lb);
2212
    }
2213
15753
    if(ub != NullConstraint){
2214
4153
      implies(out, eq, ub);
2215
    }
2216
  }
2217
56171
}
2218
2219
7409
void ConstraintDatabase::outputUnateEqualityLemmas(
2220
    std::vector<TrustNode>& lemmas) const
2221
{
2222
63580
  for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
2223
56171
    outputUnateEqualityLemmas(lemmas, v);
2224
  }
2225
7409
}
2226
2227
7409
void ConstraintDatabase::outputUnateInequalityLemmas(
2228
    std::vector<TrustNode>& lemmas) const
2229
{
2230
63580
  for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
2231
56171
    outputUnateInequalityLemmas(lemmas, v);
2232
  }
2233
7409
}
2234
2235
4666765
bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){
2236
4666765
  if(cons->negationHasProof()){
2237
    Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
2238
    cons->impliedByUnate(ant, true);
2239
    d_raiseConflict.raiseConflict(cons, InferenceId::UNKNOWN);
2240
    return true;
2241
4666765
  }else if(!cons->isTrue()){
2242
2433936
    ++d_statistics.d_unatePropagateImplications;
2243
2433936
    Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
2244
2433936
    cons->impliedByUnate(ant, false);
2245
2433936
    cons->tryToPropagate();
2246
2433936
    return false;
2247
  } else {
2248
2232829
    return false;
2249
  }
2250
}
2251
2252
1017197
void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev){
2253
1017197
  Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl;
2254
1017197
  Assert(curr != prev);
2255
1017197
  Assert(curr != NullConstraint);
2256
1017197
  bool hasPrev = ! (prev == NullConstraint);
2257
1017197
  Assert(!hasPrev || curr->getValue() > prev->getValue());
2258
2259
1017197
  ++d_statistics.d_unatePropagateCalls;
2260
2261
1017197
  const SortedConstraintMap& scm = curr->constraintSet();
2262
1017197
  const SortedConstraintMapConstIterator scm_begin = scm.begin();
2263
1017197
  SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2264
2265
  //Ignore the first ValueCollection
2266
  // NOPE: (>= p c) then (= p c) NOPE
2267
  // NOPE: (>= p c) then (not (= p c)) NOPE
2268
2269
6101477
  while(scm_i != scm_begin){
2270
2760782
    --scm_i; // move the iterator back
2271
2272
2760782
    const ValueCollection& vc = scm_i->second;
2273
2274
    //If it has the previous element, do nothing and stop!
2275
3561578
    if(hasPrev &&
2276
800796
       vc.hasConstraintOfType(prev->getType())
2277
3272993
       && vc.getConstraintOfType(prev->getType()) == prev){
2278
218642
      break;
2279
    }
2280
2281
    //Don't worry about implying the negation of upperbound.
2282
    //These should all be handled by propagating the LowerBounds!
2283
2542140
    if(vc.hasLowerBound()){
2284
976998
      ConstraintP lb = vc.getLowerBound();
2285
976998
      if(handleUnateProp(curr, lb)){ return; }
2286
    }
2287
2542140
    if(vc.hasDisequality()){
2288
237783
      ConstraintP dis = vc.getDisequality();
2289
237783
      if(handleUnateProp(curr, dis)){ return; }
2290
    }
2291
  }
2292
}
2293
2294
1000518
void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev){
2295
1000518
  Debug("arith::unate") << "unatePropUpperBound " << curr << " " << prev << endl;
2296
1000518
  Assert(curr != prev);
2297
1000518
  Assert(curr != NullConstraint);
2298
1000518
  bool hasPrev = ! (prev == NullConstraint);
2299
1000518
  Assert(!hasPrev || curr->getValue() < prev->getValue());
2300
2301
1000518
  ++d_statistics.d_unatePropagateCalls;
2302
2303
1000518
  const SortedConstraintMap& scm = curr->constraintSet();
2304
1000518
  const SortedConstraintMapConstIterator scm_end = scm.end();
2305
1000518
  SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2306
1000518
  ++scm_i;
2307
7035772
  for(; scm_i != scm_end; ++scm_i){
2308
3187602
    const ValueCollection& vc = scm_i->second;
2309
2310
    //If it has the previous element, do nothing and stop!
2311
3750960
    if(hasPrev &&
2312
3543971
       vc.hasConstraintOfType(prev->getType()) &&
2313
356369
       vc.getConstraintOfType(prev->getType()) == prev){
2314
169975
      break;
2315
    }
2316
    //Don't worry about implying the negation of upperbound.
2317
    //These should all be handled by propagating the UpperBounds!
2318
3017627
    if(vc.hasUpperBound()){
2319
1208831
      ConstraintP ub = vc.getUpperBound();
2320
1208831
      if(handleUnateProp(curr, ub)){ return; }
2321
    }
2322
3017627
    if(vc.hasDisequality()){
2323
270147
      ConstraintP dis = vc.getDisequality();
2324
270147
      if(handleUnateProp(curr, dis)){ return; }
2325
    }
2326
  }
2327
}
2328
2329
876558
void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB){
2330
876558
  Debug("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " " << prevUB << endl;
2331
876558
  Assert(curr != prevLB);
2332
876558
  Assert(curr != prevUB);
2333
876558
  Assert(curr != NullConstraint);
2334
876558
  bool hasPrevLB = ! (prevLB == NullConstraint);
2335
876558
  bool hasPrevUB = ! (prevUB == NullConstraint);
2336
876558
  Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue());
2337
876558
  Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue());
2338
2339
876558
  ++d_statistics.d_unatePropagateCalls;
2340
2341
876558
  const SortedConstraintMap& scm = curr->constraintSet();
2342
876558
  SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition;
2343
876558
  SortedConstraintMapConstIterator scm_last = hasPrevUB ? prevUB->d_variablePosition : scm.end();
2344
876558
  SortedConstraintMapConstIterator scm_i;
2345
876558
  if(hasPrevLB){
2346
168332
    scm_i = prevLB->d_variablePosition;
2347
168332
    if(scm_i != scm_curr){ // If this does not move this past scm_curr, move it one forward
2348
36799
      ++scm_i;
2349
    }
2350
  }else{
2351
708226
    scm_i = scm.begin();
2352
  }
2353
2354
2707460
  for(; scm_i != scm_curr; ++scm_i){
2355
    // between the previous LB and the curr
2356
915451
    const ValueCollection& vc = scm_i->second;
2357
2358
    //Don't worry about implying the negation of upperbound.
2359
    //These should all be handled by propagating the LowerBounds!
2360
915451
    if(vc.hasLowerBound()){
2361
339986
      ConstraintP lb = vc.getLowerBound();
2362
339986
      if(handleUnateProp(curr, lb)){ return; }
2363
    }
2364
915451
    if(vc.hasDisequality()){
2365
312997
      ConstraintP dis = vc.getDisequality();
2366
312997
      if(handleUnateProp(curr, dis)){ return; }
2367
    }
2368
  }
2369
876558
  Assert(scm_i == scm_curr);
2370
876558
  if(!hasPrevUB || scm_i != scm_last){
2371
852012
    ++scm_i;
2372
  } // hasPrevUB implies scm_i != scm_last
2373
2374
4619144
  for(; scm_i != scm_last; ++scm_i){
2375
    // between the curr and the previous UB imply the upperbounds and disequalities.
2376
1871293
    const ValueCollection& vc = scm_i->second;
2377
2378
    //Don't worry about implying the negation of upperbound.
2379
    //These should all be handled by propagating the UpperBounds!
2380
1871293
    if(vc.hasUpperBound()){
2381
705232
      ConstraintP ub = vc.getUpperBound();
2382
705232
      if(handleUnateProp(curr, ub)){ return; }
2383
    }
2384
1871293
    if(vc.hasDisequality()){
2385
614791
      ConstraintP dis = vc.getDisequality();
2386
614791
      if(handleUnateProp(curr, dis)){ return; }
2387
    }
2388
  }
2389
}
2390
2391
318500
std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca, ConstraintCP cb){
2392
318500
  ConstraintType a = ca->getType();
2393
318500
  ConstraintType b = cb->getType();
2394
2395
318500
  Assert(a != Disequality);
2396
318500
  Assert(b != Disequality);
2397
2398
318500
  int a_sgn = (a == LowerBound) ? -1 : ((a == UpperBound) ? 1 : 0);
2399
318500
  int b_sgn = (b == LowerBound) ? -1 : ((b == UpperBound) ? 1 : 0);
2400
2401
318500
  if(a_sgn == 0 && b_sgn == 0){
2402
102925
    Assert(a == Equality);
2403
102925
    Assert(b == Equality);
2404
102925
    Assert(ca->getValue() != cb->getValue());
2405
205850
    if(ca->getValue() < cb->getValue()){
2406
36768
      a_sgn = 1;
2407
36768
      b_sgn = -1;
2408
    }else{
2409
66157
      a_sgn = -1;
2410
66157
      b_sgn = 1;
2411
    }
2412
215575
  }else if(a_sgn == 0){
2413
38806
    Assert(b_sgn != 0);
2414
38806
    Assert(a == Equality);
2415
38806
    a_sgn = -b_sgn;
2416
176769
  }else if(b_sgn == 0){
2417
107087
    Assert(a_sgn != 0);
2418
107087
    Assert(b == Equality);
2419
107087
    b_sgn = -a_sgn;
2420
  }
2421
318500
  Assert(a_sgn != 0);
2422
318500
  Assert(b_sgn != 0);
2423
2424
637000
  Debug("arith::unateFarkasSigns") << "Constraint::unateFarkasSigns("<<a <<", " << b << ") -> "
2425
318500
                                   << "("<<a_sgn<<", "<< b_sgn <<")"<< endl;
2426
318500
  return make_pair(a_sgn, b_sgn);
2427
}
2428
2429
}/* CVC4::theory::arith namespace */
2430
}/* CVC4::theory namespace */
2431
26685
}/* CVC4 namespace */