GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/constraint.cpp Lines: 1075 1475 72.9 %
Date: 2021-03-22 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
487187
ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){
44
487187
  Kind k = cmp.comparisonKind();
45
487187
  switch(k){
46
135018
  case LT:
47
  case LEQ:
48
    {
49
270036
      Polynomial l = cmp.getLeft();
50
135018
      if(l.leadingCoefficientIsPositive()){ // (< x c)
51
111246
        return UpperBound;
52
      }else{
53
23772
        return LowerBound; // (< (-x) c)
54
      }
55
    }
56
136180
  case GT:
57
  case GEQ:
58
    {
59
272360
      Polynomial l = cmp.getLeft();
60
136180
      if(l.leadingCoefficientIsPositive()){
61
112201
        return LowerBound; // (> x c)
62
      }else{
63
23979
        return UpperBound; // (> (-x) c)
64
      }
65
    }
66
108103
  case EQUAL:
67
108103
    return Equality;
68
107886
  case DISTINCT:
69
107886
    return Disequality;
70
  default: Unhandled() << k;
71
  }
72
}
73
74
606783
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
606783
    d_variablePosition()
87
{
88
606783
  Assert(!initialized());
89
606783
}
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
2184956
ValueCollection::ValueCollection()
190
  : d_lowerBound(NullConstraint),
191
    d_upperBound(NullConstraint),
192
    d_equality(NullConstraint),
193
2184956
    d_disequality(NullConstraint)
194
2184956
{}
195
196
18780891
bool ValueCollection::hasLowerBound() const{
197
18780891
  return d_lowerBound != NullConstraint;
198
}
199
200
21380898
bool ValueCollection::hasUpperBound() const{
201
21380898
  return d_upperBound != NullConstraint;
202
}
203
204
4227543
bool ValueCollection::hasEquality() const{
205
4227543
  return d_equality != NullConstraint;
206
}
207
208
14806961
bool ValueCollection::hasDisequality() const {
209
14806961
  return d_disequality != NullConstraint;
210
}
211
212
3949996
ConstraintP ValueCollection::getLowerBound() const {
213
3949996
  Assert(hasLowerBound());
214
3949996
  return d_lowerBound;
215
}
216
217
4348380
ConstraintP ValueCollection::getUpperBound() const {
218
4348380
  Assert(hasUpperBound());
219
4348380
  return d_upperBound;
220
}
221
222
401243
ConstraintP ValueCollection::getEquality() const {
223
401243
  Assert(hasEquality());
224
401243
  return d_equality;
225
}
226
227
2399938
ConstraintP ValueCollection::getDisequality() const {
228
2399938
  Assert(hasDisequality());
229
2399938
  return d_disequality;
230
}
231
232
233
411035
void ValueCollection::push_into(std::vector<ConstraintP>& vec) const {
234
411035
  Debug("arith::constraint") << "push_into " << *this << endl;
235
411035
  if(hasEquality()){
236
112324
    vec.push_back(d_equality);
237
  }
238
411035
  if(hasLowerBound()){
239
190378
    vec.push_back(d_lowerBound);
240
  }
241
411035
  if(hasUpperBound()){
242
190378
    vec.push_back(d_upperBound);
243
  }
244
411035
  if(hasDisequality()){
245
112324
    vec.push_back(d_disequality);
246
  }
247
411035
}
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
3638064
bool ValueCollection::hasConstraintOfType(ConstraintType t) const{
272
3638064
  switch(t){
273
1136287
  case LowerBound:
274
1136287
    return hasLowerBound();
275
2097828
  case UpperBound:
276
2097828
    return hasUpperBound();
277
403949
  case Equality:
278
403949
    return hasEquality();
279
  case Disequality:
280
    return hasDisequality();
281
  default:
282
    Unreachable();
283
  }
284
}
285
286
200633
ArithVar ValueCollection::getVariable() const{
287
200633
  Assert(!empty());
288
200633
  return nonNull()->getVariable();
289
}
290
291
200633
const DeltaRational& ValueCollection::getValue() const{
292
200633
  Assert(!empty());
293
200633
  return nonNull()->getValue();
294
}
295
296
605404
void ValueCollection::add(ConstraintP c){
297
605404
  Assert(c != NullConstraint);
298
299
605404
  Assert(empty() || getVariable() == c->getVariable());
300
605404
  Assert(empty() || getValue() == c->getValue());
301
302
605404
  switch(c->getType()){
303
190378
  case LowerBound:
304
190378
    Assert(!hasLowerBound());
305
190378
    d_lowerBound = c;
306
190378
    break;
307
112324
  case Equality:
308
112324
    Assert(!hasEquality());
309
112324
    d_equality = c;
310
112324
    break;
311
190378
  case UpperBound:
312
190378
    Assert(!hasUpperBound());
313
190378
    d_upperBound = c;
314
190378
    break;
315
112324
  case Disequality:
316
112324
    Assert(!hasDisequality());
317
112324
    d_disequality = c;
318
112324
    break;
319
  default:
320
    Unreachable();
321
  }
322
605404
}
323
324
2833532
ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const{
325
2833532
  switch(t){
326
731937
    case LowerBound: Assert(hasLowerBound()); return d_lowerBound;
327
291625
    case Equality: Assert(hasEquality()); return d_equality;
328
1809970
    case UpperBound: Assert(hasUpperBound()); return d_upperBound;
329
    case Disequality: Assert(hasDisequality()); return d_disequality;
330
    default: Unreachable();
331
  }
332
}
333
334
605404
void ValueCollection::remove(ConstraintType t){
335
605404
  switch(t){
336
190378
  case LowerBound:
337
190378
    Assert(hasLowerBound());
338
190378
    d_lowerBound = NullConstraint;
339
190378
    break;
340
112324
  case Equality:
341
112324
    Assert(hasEquality());
342
112324
    d_equality = NullConstraint;
343
112324
    break;
344
190378
  case UpperBound:
345
190378
    Assert(hasUpperBound());
346
190378
    d_upperBound = NullConstraint;
347
190378
    break;
348
112324
  case Disequality:
349
112324
    Assert(hasDisequality());
350
112324
    d_disequality = NullConstraint;
351
112324
    break;
352
  default:
353
    Unreachable();
354
  }
355
605404
}
356
357
2217478
bool ValueCollection::empty() const{
358
  return
359
5343402
    !(hasLowerBound() ||
360
3691840
      hasUpperBound() ||
361
1799021
      hasEquality() ||
362
3450583
      hasDisequality());
363
}
364
365
401266
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
401266
  if(hasLowerBound()){
369
129328
    return d_lowerBound;
370
271938
  }else if(hasUpperBound()){
371
45142
    return d_upperBound;
372
226796
  }else if(hasEquality()){
373
226796
    return d_equality;
374
  }else if(hasDisequality()){
375
    return d_disequality;
376
  }else{
377
    return NullConstraint;
378
  }
379
}
380
381
2520400
bool Constraint::initialized() const {
382
2520400
  return d_database != NULL;
383
}
384
385
const ConstraintDatabase& Constraint::getDatabase() const{
386
  Assert(initialized());
387
  return *d_database;
388
}
389
390
605404
void Constraint::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){
391
605404
  Assert(!initialized());
392
605404
  d_database = db;
393
605404
  d_variablePosition = v;
394
605404
  d_negation = negation;
395
605404
}
396
397
1213566
Constraint::~Constraint() {
398
  // Call this instead of safeToGarbageCollect()
399
606783
  Assert(!contextDependentDataIsSet());
400
401
606783
  if(initialized()){
402
605404
    ValueCollection& vc =  d_variablePosition->second;
403
605404
    Debug("arith::constraint") << "removing" << vc << endl;
404
405
605404
    vc.remove(getType());
406
407
605404
    if(vc.empty()){
408
411035
      Debug("arith::constraint") << "erasing" << vc << endl;
409
411035
      SortedConstraintMap& perVariable = d_database->getVariableSCM(getVariable());
410
411035
      perVariable.erase(d_variablePosition);
411
    }
412
413
605404
    if(hasLiteral()){
414
488566
      d_database->d_nodetoConstraintMap.erase(getLiteral());
415
    }
416
  }
417
606783
}
418
419
26813025
const ConstraintRule& Constraint::getConstraintRule() const {
420
26813025
  Assert(hasProof());
421
26813025
  return d_database->d_watches->d_constraintProofs[d_crid];
422
}
423
424
2995711
const ValueCollection& Constraint::getValueCollection() const{
425
2995711
  return d_variablePosition->second;
426
}
427
428
429
81013
ConstraintP Constraint::getCeiling() {
430
81013
  Debug("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
431
81013
  Assert(getValue().getInfinitesimalPart().sgn() > 0);
432
433
162026
  const DeltaRational ceiling(getValue().ceiling());
434
162026
  return d_database->getConstraint(getVariable(), getType(), ceiling);
435
}
436
437
1367172
ConstraintP Constraint::getFloor() {
438
1367172
  Assert(getValue().getInfinitesimalPart().sgn() < 0);
439
440
2734344
  const DeltaRational floor(Rational(getValue().floor()));
441
2734344
  return d_database->getConstraint(getVariable(), getType(), floor);
442
}
443
444
687910
void Constraint::setCanBePropagated() {
445
687910
  Assert(!canBePropagated());
446
687910
  d_database->pushCanBePropagatedWatch(this);
447
687910
}
448
449
5716363
void Constraint::setAssertedToTheTheory(TNode witness, bool nowInConflict) {
450
5716363
  Assert(hasLiteral());
451
5716363
  Assert(!assertedToTheTheory());
452
5716363
  Assert(negationHasProof() == nowInConflict);
453
5716363
  d_database->pushAssertionOrderWatch(this, witness);
454
455
5716363
  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
5716363
}
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
11136375
bool Constraint::isInternalAssumption() const {
479
11136375
  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
11765924
bool Constraint::isAssumption() const {
506
11765924
  return getProofType() == AssumeAP;
507
}
508
509
607837
bool Constraint::hasEqualityEngineProof() const {
510
607837
  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
488566
bool Constraint::sanityChecking(Node n) const {
621
977132
  Comparison cmp = Comparison::parseNormalForm(n);
622
488566
  Kind k = cmp.comparisonKind();
623
977132
  Polynomial pleft = cmp.normalizedVariablePart();
624
488566
  Assert(k == EQUAL || k == DISTINCT || pleft.leadingCoefficientIsPositive());
625
488566
  Assert(k != EQUAL || Monomial::isMember(n[0]));
626
488566
  Assert(k != DISTINCT || Monomial::isMember(n[0][0]));
627
628
977132
  TNode left = pleft.getNode();
629
977132
  DeltaRational right = cmp.normalizedDeltaRational();
630
631
488566
  const ArithVariables& avariables = d_database->getArithVariables();
632
633
488566
  Debug("Constraint::sanityChecking") << cmp.getNode() << endl;
634
488566
  Debug("Constraint::sanityChecking") << k << endl;
635
488566
  Debug("Constraint::sanityChecking") << pleft.getNode() << endl;
636
488566
  Debug("Constraint::sanityChecking") << left << endl;
637
488566
  Debug("Constraint::sanityChecking") << right << endl;
638
488566
  Debug("Constraint::sanityChecking") << getValue() << endl;
639
488566
  Debug("Constraint::sanityChecking") << avariables.hasArithVar(left) << endl;
640
488566
  Debug("Constraint::sanityChecking") << avariables.asArithVar(left) << endl;
641
488566
  Debug("Constraint::sanityChecking") << getVariable() << endl;
642
643
644
2442830
  if(avariables.hasArithVar(left) &&
645
2442830
     avariables.asArithVar(left) == getVariable() &&
646
488566
     getValue() == right){
647
488566
    switch(getType()){
648
272360
    case LowerBound:
649
    case UpperBound:
650
      //Be overapproximate
651
272360
      return k == GT || k == GEQ ||k == LT || k == LEQ;
652
108103
    case Equality:
653
108103
      return k == EQUAL;
654
108103
    case Disequality:
655
108103
      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
2534815
bool Constraint::wellFormedFarkasProof() const {
714
2534815
  Assert(hasProof());
715
716
2534815
  const ConstraintRule& cr = getConstraintRule();
717
2534815
  if(cr.d_constraint != this){ return false; }
718
2534815
  if(cr.d_proofType != FarkasAP){ return false; }
719
720
2534815
  AntecedentId p = cr.d_antecedentEnd;
721
722
  // must have at least one antecedent
723
2534815
  ConstraintCP antecedent = d_database->d_antecedents[p];
724
2534815
  if(antecedent  == NullConstraint) { return false; }
725
726
2534815
  if (!ARITH_PROOF_ON())
727
  {
728
2204551
    return cr.d_farkasCoefficients == RationalVectorCPSentinel;
729
  }
730
330264
  Assert(ARITH_PROOF_ON());
731
732
330264
  if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
733
330264
  if(cr.d_farkasCoefficients->size() < 2){ return false; }
734
735
330264
  const ArithVariables& vars = d_database->getArithVariables();
736
737
660528
  DeltaRational rhs(0);
738
660528
  Node lhs = Polynomial::mkZero().getNode();
739
740
330264
  RationalVector::const_iterator coeffIterator = cr.d_farkasCoefficients->end()-1;
741
330264
  RationalVector::const_iterator coeffBegin = cr.d_farkasCoefficients->begin();
742
743
1145256
  while(antecedent != NullConstraint){
744
407496
    Assert(lhs.isNull() || Polynomial::isMember(lhs));
745
746
407496
    const Rational& coeff = *coeffIterator;
747
407496
    int coeffSgn = coeff.sgn();
748
749
407496
    rhs += antecedent->getValue() * coeff;
750
751
407496
    ArithVar antVar = antecedent->getVariable();
752
407496
    if(!lhs.isNull() && vars.hasNode(antVar)){
753
814992
      Node antAsNode = vars.asNode(antVar);
754
407496
      if(Polynomial::isMember(antAsNode)){
755
814992
        Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
756
814992
        Polynomial antPoly = Polynomial::parsePolynomial(antAsNode);
757
814992
        Polynomial sum = lhsPoly + (antPoly * coeff);
758
407496
        lhs = sum.getNode();
759
      }else{
760
        lhs = Node::null();
761
      }
762
    } else {
763
      lhs = Node::null();
764
    }
765
407496
    Debug("constraints::wffp") << "running sum: " << lhs << " <= " << rhs << endl;
766
767
407496
    switch( antecedent->getType() ){
768
104597
    case LowerBound:
769
      // fc[l] < 0, therefore return false if coeffSgn >= 0
770
104597
      if(coeffSgn >= 0){ return false; }
771
104597
      break;
772
60219
    case UpperBound:
773
      // fc[u] > 0, therefore return false if coeffSgn <= 0
774
60219
      if(coeffSgn <= 0){ return false; }
775
60219
      break;
776
242680
    case Equality:
777
242680
      if(coeffSgn == 0) { return false; }
778
242680
      break;
779
    case Disequality:
780
    default:
781
      return false;
782
    }
783
784
407496
    if(coeffIterator == coeffBegin){ return false; }
785
407496
    --coeffIterator;
786
407496
    --p;
787
407496
    antecedent = d_database->d_antecedents[p];
788
  }
789
330264
  if(coeffIterator != coeffBegin){ return false; }
790
791
330264
  const Rational& firstCoeff = (*coeffBegin);
792
330264
  int firstCoeffSgn = firstCoeff.sgn();
793
330264
  rhs += (getNegation()->getValue()) * firstCoeff;
794
330264
  if(!lhs.isNull() && vars.hasNode(getVariable())){
795
660528
    Node firstAsNode = vars.asNode(getVariable());
796
330264
    if(Polynomial::isMember(firstAsNode)){
797
660528
      Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
798
660528
      Polynomial firstPoly = Polynomial::parsePolynomial(firstAsNode);
799
660528
      Polynomial sum = lhsPoly + (firstPoly * firstCoeff);
800
330264
      lhs = sum.getNode();
801
    }else{
802
      lhs = Node::null();
803
    }
804
  }else{
805
    lhs = Node::null();
806
  }
807
808
330264
  switch( getNegation()->getType() ){
809
86593
  case LowerBound:
810
    // fc[l] < 0, therefore return false if coeffSgn >= 0
811
86593
    if(firstCoeffSgn >= 0){ return false; }
812
86593
    break;
813
99179
  case UpperBound:
814
    // fc[u] > 0, therefore return false if coeffSgn <= 0
815
99179
    if(firstCoeffSgn <= 0){ return false; }
816
99179
    break;
817
144492
  case Equality:
818
144492
    if(firstCoeffSgn == 0) { return false; }
819
144492
    break;
820
  case Disequality:
821
  default:
822
    return false;
823
  }
824
330264
  Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
825
  // 0 = lhs <= rhs < 0
826
990792
  return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
827
990792
         && rhs.sgn() < 0;
828
}
829
830
59798
ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
831
59798
  switch(t){
832
3281
  case LowerBound:
833
    {
834
3281
      Assert(r.infinitesimalSgn() >= 0);
835
3281
      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
3281
        Assert(r.infinitesimalSgn() == 0);
842
        // make (not (v >= r)), which is (v < r)
843
6562
        DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
844
3281
        return new Constraint(v, UpperBound, addInf);
845
      }
846
    }
847
52079
  case UpperBound:
848
    {
849
52079
      Assert(r.infinitesimalSgn() <= 0);
850
52079
      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
52079
        Assert(r.infinitesimalSgn() == 0);
857
        // make (not (v <= r)), which is (v > r)
858
104158
        DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
859
52079
        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
8995
ConstraintDatabase::ConstraintDatabase(context::Context* satContext,
873
                                       context::Context* userContext,
874
                                       const ArithVariables& avars,
875
                                       ArithCongruenceManager& cm,
876
                                       RaiseConflict raiseConflict,
877
                                       EagerProofGenerator* pfGen,
878
8995
                                       ProofNodeManager* pnm)
879
    : d_varDatabases(),
880
      d_toPropagate(satContext),
881
      d_antecedents(satContext, false),
882
8995
      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
17990
      d_negOne(-1)
891
{
892
8995
}
893
894
10080055
SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const{
895
10080055
  Assert(variableDatabaseIsSetup(v));
896
10080055
  return d_varDatabases[v]->d_constraints;
897
}
898
899
29750
void ConstraintDatabase::pushSplitWatch(ConstraintP c){
900
29750
  Assert(!c->d_split);
901
29750
  c->d_split = true;
902
29750
  d_watches->d_splitWatches.push_back(c);
903
29750
}
904
905
906
687910
void ConstraintDatabase::pushCanBePropagatedWatch(ConstraintP c){
907
687910
  Assert(!c->d_canBePropagated);
908
687910
  c->d_canBePropagated = true;
909
687910
  d_watches->d_canBePropagatedWatches.push_back(c);
910
687910
}
911
912
5716363
void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness){
913
5716363
  Assert(!c->assertedToTheTheory());
914
5716363
  c->d_assertionOrder = d_watches->d_assertionOrderWatches.size();
915
5716363
  c->d_witness = witness;
916
5716363
  d_watches->d_assertionOrderWatches.push_back(c);
917
5716363
}
918
919
920
9161442
void ConstraintDatabase::pushConstraintRule(const ConstraintRule& crp){
921
9161442
  ConstraintP c = crp.d_constraint;
922
9161442
  Assert(c->d_crid == ConstraintRuleIdSentinel);
923
9161442
  Assert(!c->hasProof());
924
9161442
  c->d_crid = d_watches->d_constraintProofs.size();
925
9161442
  d_watches->d_constraintProofs.push_back(crp);
926
9161442
}
927
928
1750295
ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){
929
  //This must always return a constraint.
930
931
1750295
  SortedConstraintMap& scm = getVariableSCM(v);
932
1750295
  pair<SortedConstraintMapIterator, bool> insertAttempt;
933
1750295
  insertAttempt = scm.insert(make_pair(r, ValueCollection()));
934
935
1750295
  SortedConstraintMapIterator pos = insertAttempt.first;
936
1750295
  ValueCollection& vc = pos->second;
937
1750295
  if(vc.hasConstraintOfType(t)){
938
1690497
    return vc.getConstraintOfType(t);
939
  }else{
940
59798
    ConstraintP c = new Constraint(v, t, r);
941
59798
    ConstraintP negC = Constraint::makeNegation(v, t, r);
942
943
59798
    SortedConstraintMapIterator negPos;
944
59798
    if(t == Equality || t == Disequality){
945
4438
      negPos = pos;
946
    }else{
947
55360
      pair<SortedConstraintMapIterator, bool> negInsertAttempt;
948
55360
      negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
949
55360
      Assert(negInsertAttempt.second
950
             || !negInsertAttempt.first->second.hasConstraintOfType(
951
                 negC->getType()));
952
55360
      negPos = negInsertAttempt.first;
953
    }
954
955
59798
    c->initialize(this, pos, negC);
956
59798
    negC->initialize(this, negPos, c);
957
958
59798
    vc.add(c);
959
59798
    negPos->second.add(negC);
960
961
59798
    return c;
962
  }
963
}
964
965
279354
ConstraintP ConstraintDatabase::ensureConstraint(ValueCollection& vc, ConstraintType t){
966
279354
  if(vc.hasConstraintOfType(t)){
967
273090
    return vc.getConstraintOfType(t);
968
  }else{
969
6264
    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
17984
ConstraintDatabase::~ConstraintDatabase(){
980
8992
  delete d_watches;
981
982
17984
  std::vector<ConstraintP> constraintList;
983
984
301728
  while(!d_varDatabases.empty()){
985
146368
    PerVariableDatabase* back = d_varDatabases.back();
986
987
146368
    SortedConstraintMap& scm = back->d_constraints;
988
146368
    SortedConstraintMapIterator i = scm.begin(), i_end = scm.end();
989
968438
    for(; i != i_end; ++i){
990
411035
      (i->second).push_into(constraintList);
991
    }
992
1357176
    while(!constraintList.empty()){
993
605404
      ConstraintP c = constraintList.back();
994
605404
      constraintList.pop_back();
995
605404
      delete c;
996
    }
997
146368
    Assert(scm.empty());
998
146368
    d_varDatabases.pop_back();
999
146368
    delete back;
1000
  }
1001
1002
8992
  Assert(d_nodetoConstraintMap.empty());
1003
8992
}
1004
1005
8995
ConstraintDatabase::Statistics::Statistics():
1006
  d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
1007
8995
  d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
1008
{
1009
8995
  smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls);
1010
8995
  smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications);
1011
1012
8995
}
1013
1014
17984
ConstraintDatabase::Statistics::~Statistics(){
1015
8992
  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls);
1016
8992
  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications);
1017
8992
}
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
146368
void ConstraintDatabase::addVariable(ArithVar v){
1028
146368
  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
146368
    Debug("arith::constraint") << "about to fail" << v << " " << d_varDatabases.size() << endl;
1047
146368
    Assert(v == d_varDatabases.size());
1048
146368
    d_varDatabases.push_back(new PerVariableDatabase(v));
1049
  }
1050
146368
}
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
606783
bool Constraint::contextDependentDataIsSet() const{
1064
606783
  return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory();
1065
}
1066
1067
14875
TrustNode Constraint::split()
1068
{
1069
14875
  Assert(isEquality() || isDisequality());
1070
1071
14875
  bool isEq = isEquality();
1072
1073
14875
  ConstraintP eq = isEq ? this : d_negation;
1074
14875
  ConstraintP diseq = isEq ? d_negation : this;
1075
1076
29750
  TNode eqNode = eq->getLiteral();
1077
14875
  Assert(eqNode.getKind() == kind::EQUAL);
1078
29750
  TNode lhs = eqNode[0];
1079
29750
  TNode rhs = eqNode[1];
1080
1081
29750
  Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs;
1082
29750
  Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
1083
29750
  Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
1084
29750
  Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs;
1085
1086
29750
  Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode;
1087
1088
14875
  TrustNode trustedLemma;
1089
14875
  if (d_database->isProofEnabled())
1090
  {
1091
    // Farkas proof that this works.
1092
1933
    auto nm = NodeManager::currentNM();
1093
3866
    auto nLeqPf = d_database->d_pnm->mkAssume(leqNode.negate());
1094
1933
    auto gtPf = d_database->d_pnm->mkNode(
1095
3866
        PfRule::MACRO_SR_PRED_TRANSFORM, {nLeqPf}, {gtNode});
1096
3866
    auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate());
1097
1933
    auto ltPf = d_database->d_pnm->mkNode(
1098
3866
        PfRule::MACRO_SR_PRED_TRANSFORM, {nGeqPf}, {ltNode});
1099
1933
    auto sumPf = d_database->d_pnm->mkNode(
1100
        PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
1101
        {gtPf, ltPf},
1102
3866
        {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
1103
1933
    auto botPf = d_database->d_pnm->mkNode(
1104
3866
        PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
1105
3866
    std::vector<Node> a = {leqNode.negate(), geqNode.negate()};
1106
3866
    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
3866
        d_database->d_pnm->mkNode(PfRule::NOT_AND, {notAndNotPf}, {});
1111
1933
    auto orPf = d_database->d_pnm->mkNode(
1112
3866
        PfRule::MACRO_SR_PRED_TRANSFORM, {orNotNotPf}, {lemma});
1113
1933
    trustedLemma = d_database->d_pfGen->mkTrustNode(lemma, orPf);
1114
  }
1115
  else
1116
  {
1117
12942
    trustedLemma = TrustNode::mkTrustLemma(lemma);
1118
  }
1119
1120
14875
  eq->d_database->pushSplitWatch(eq);
1121
14875
  diseq->d_database->pushSplitWatch(diseq);
1122
1123
29750
  return trustedLemma;
1124
}
1125
1126
977133
bool ConstraintDatabase::hasLiteral(TNode literal) const {
1127
977133
  return lookup(literal) != NullConstraint;
1128
}
1129
1130
244283
ConstraintP ConstraintDatabase::addLiteral(TNode literal){
1131
244283
  Assert(!hasLiteral(literal));
1132
244283
  bool isNot = (literal.getKind() == NOT);
1133
488566
  Node atomNode = (isNot ? literal[0] : literal);
1134
488566
  Node negationNode  = atomNode.notNode();
1135
1136
244283
  Assert(!hasLiteral(atomNode));
1137
244283
  Assert(!hasLiteral(negationNode));
1138
488566
  Comparison posCmp = Comparison::parseNormalForm(atomNode);
1139
1140
244283
  ConstraintType posType = Constraint::constraintTypeOfComparison(posCmp);
1141
1142
488566
  Polynomial nvp = posCmp.normalizedVariablePart();
1143
244283
  ArithVar v = d_avariables.asArithVar(nvp.getNode());
1144
1145
488566
  DeltaRational posDR = posCmp.normalizedDeltaRational();
1146
1147
244283
  ConstraintP posC = new Constraint(v, posType, posDR);
1148
1149
244283
  Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl;
1150
244283
  Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
1151
1152
244283
  SortedConstraintMap& scm = getVariableSCM(posC->getVariable());
1153
244283
  pair<SortedConstraintMapIterator, bool> insertAttempt;
1154
244283
  insertAttempt = scm.insert(make_pair(posC->getValue(), ValueCollection()));
1155
1156
244283
  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
244283
  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
485808
    Comparison negCmp = Comparison::parseNormalForm(negationNode);
1174
1175
242904
    ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
1176
485808
    DeltaRational negDR = negCmp.normalizedDeltaRational();
1177
1178
242904
    ConstraintP negC = new Constraint(v, negType, negDR);
1179
1180
242904
    SortedConstraintMapIterator negI;
1181
1182
242904
    if(posC->isEquality()){
1183
107886
      negI = posI;
1184
    }else{
1185
135018
      Assert(posC->isLowerBound() || posC->isUpperBound());
1186
1187
135018
      pair<SortedConstraintMapIterator, bool> negInsertAttempt;
1188
135018
      negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
1189
1190
135018
      Debug("nf::tmp") << "sdhjfgdhjkldfgljkhdfg" << endl;
1191
135018
      Debug("nf::tmp") << negC << endl;
1192
135018
      Debug("nf::tmp") << negC->getValue() << endl;
1193
1194
      //This should always succeed as the DeltaRational for the negation is unique!
1195
135018
      Assert(negInsertAttempt.second);
1196
1197
135018
      negI = negInsertAttempt.first;
1198
    }
1199
1200
242904
    (posI->second).add(posC);
1201
242904
    (negI->second).add(negC);
1202
1203
242904
    posC->initialize(this, posI, negC);
1204
242904
    negC->initialize(this, negI, posC);
1205
1206
242904
    posC->setLiteral(atomNode);
1207
242904
    negC->setLiteral(negationNode);
1208
1209
242904
    return isNot ? negC : posC;
1210
  }
1211
}
1212
1213
1214
9724340
ConstraintP ConstraintDatabase::lookup(TNode literal) const{
1215
9724340
  NodetoConstraintMap::const_iterator iter = d_nodetoConstraintMap.find(literal);
1216
9724340
  if(iter == d_nodetoConstraintMap.end()){
1217
1881597
    return NullConstraint;
1218
  }else{
1219
7842743
    return iter->second;
1220
  }
1221
}
1222
1223
4775753
void Constraint::setAssumption(bool nowInConflict){
1224
4775753
  Debug("constraints::pf") << "setAssumption(" << this << ")" << std::endl;
1225
4775753
  Assert(!hasProof());
1226
4775753
  Assert(negationHasProof() == nowInConflict);
1227
4775753
  Assert(hasLiteral());
1228
4775753
  Assert(assertedToTheTheory());
1229
1230
4775753
  d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
1231
1232
4775753
  Assert(inConflict() == nowInConflict);
1233
4775753
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1234
    Debug("constraint::conflictCommit") << "inConflict@setAssumption " << this << std::endl;
1235
  }
1236
4775753
}
1237
1238
4128970
void Constraint::tryToPropagate(){
1239
4128970
  Assert(hasProof());
1240
4128970
  Assert(!isAssumption());
1241
4128970
  Assert(!isInternalAssumption());
1242
1243
4128970
  if(canBePropagated() && !assertedToTheTheory() && !isAssumption() && !isInternalAssumption()){
1244
734509
    propagate();
1245
  }
1246
4128970
}
1247
1248
745533
void Constraint::propagate(){
1249
745533
  Assert(hasProof());
1250
745533
  Assert(canBePropagated());
1251
745533
  Assert(!assertedToTheTheory());
1252
745533
  Assert(!isAssumption());
1253
745533
  Assert(!isInternalAssumption());
1254
1255
745533
  d_database->d_toPropagate.push(this);
1256
745533
}
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
2439913
void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
1267
2439913
  Debug("constraints::pf") << "impliedByUnate(" << this << ", " << *imp << ")" << std::endl;
1268
2439913
  Assert(!hasProof());
1269
2439913
  Assert(imp->hasProof());
1270
2439913
  Assert(negationHasProof() == nowInConflict);
1271
1272
2439913
  d_database->d_antecedents.push_back(NullConstraint);
1273
2439913
  d_database->d_antecedents.push_back(imp);
1274
1275
2439913
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1276
1277
  RationalVectorP coeffs;
1278
2439913
  if (ARITH_PROOF_ON())
1279
  {
1280
318499
    std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
1281
1282
636998
    Rational first(sgns.first);
1283
636998
    Rational second(sgns.second);
1284
1285
318499
    coeffs = new RationalVector();
1286
318499
    coeffs->push_back(first);
1287
318499
    coeffs->push_back(second);
1288
  }
1289
  else
1290
  {
1291
2121414
    coeffs = RationalVectorPSentinel;
1292
  }
1293
  // no need to delete coeffs the memory is owned by ConstraintRule
1294
2439913
  d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
1295
1296
2439913
  Assert(inConflict() == nowInConflict);
1297
2439913
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1298
    Debug("constraint::conflictCommit") << "inConflict@impliedByUnate " << this << std::endl;
1299
  }
1300
1301
2439913
  if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
1302
    getConstraintRule().print(Debug("constraints::wffp"));
1303
  }
1304
2439913
  Assert(wellFormedFarkasProof());
1305
2439913
}
1306
1307
468879
void Constraint::impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool nowInConflict){
1308
468879
  Debug("constraints::pf") << "impliedByTrichotomy(" << this << ", " << *a << ", ";
1309
468879
  Debug("constraints::pf") << *b << ")" << std::endl;
1310
468879
  Assert(!hasProof());
1311
468879
  Assert(negationHasProof() == nowInConflict);
1312
468879
  Assert(a->hasProof());
1313
468879
  Assert(b->hasProof());
1314
1315
468879
  d_database->d_antecedents.push_back(NullConstraint);
1316
468879
  d_database->d_antecedents.push_back(a);
1317
468879
  d_database->d_antecedents.push_back(b);
1318
1319
468879
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1320
468879
  d_database->pushConstraintRule(ConstraintRule(this, TrichotomyAP, antecedentEnd));
1321
1322
468879
  Assert(inConflict() == nowInConflict);
1323
468879
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1324
    Debug("constraint::conflictCommit") << "inConflict@impliedByTrichotomy " << this << std::endl;
1325
  }
1326
468879
}
1327
1328
1329
94902
bool Constraint::allHaveProof(const ConstraintCPVec& b){
1330
1366342
  for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
1331
1271440
    ConstraintCP cp = *i;
1332
1271440
    if(! (cp->hasProof())){ return false; }
1333
  }
1334
94902
  return true;
1335
}
1336
1337
1198015
void Constraint::impliedByIntTighten(ConstraintCP a, bool nowInConflict){
1338
1198015
  Debug("constraints::pf") << "impliedByIntTighten(" << this << ", " << *a << ")" << std::endl;
1339
1198015
  Assert(!hasProof());
1340
1198015
  Assert(negationHasProof() == nowInConflict);
1341
1198015
  Assert(a->hasProof());
1342
2396030
  Debug("pf::arith") << "impliedByIntTighten(" << this << ", " << a << ")"
1343
1198015
                     << std::endl;
1344
1345
1198015
  d_database->d_antecedents.push_back(NullConstraint);
1346
1198015
  d_database->d_antecedents.push_back(a);
1347
1198015
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1348
1198015
  d_database->pushConstraintRule(ConstraintRule(this, IntTightenAP, antecedentEnd));
1349
1350
1198015
  Assert(inConflict() == nowInConflict);
1351
1198015
  if(inConflict()){
1352
4133
    Debug("constraint::conflictCommit") << "inConflict impliedByIntTighten" << this << std::endl;
1353
  }
1354
1198015
}
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
94902
void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coeffs, bool nowInConflict){
1413
94902
  Debug("constraints::pf") << "impliedByFarkas(" << this;
1414
94902
  if (Debug.isOn("constraints::pf")) {
1415
    for (const ConstraintCP& p : a)
1416
    {
1417
      Debug("constraints::pf") << ", " << p;
1418
    }
1419
  }
1420
94902
  Debug("constraints::pf") << ", <coeffs>";
1421
94902
  Debug("constraints::pf") << ")" << std::endl;
1422
94902
  Assert(!hasProof());
1423
94902
  Assert(negationHasProof() == nowInConflict);
1424
94902
  Assert(allHaveProof(a));
1425
1426
94902
  Assert(ARITH_PROOF_ON() == (coeffs != RationalVectorCPSentinel));
1427
94902
  Assert(!ARITH_PROOF_ON() || coeffs->size() == a.size() + 1);
1428
1429
94902
  Assert(a.size() >= 1);
1430
1431
94902
  d_database->d_antecedents.push_back(NullConstraint);
1432
1366342
  for(ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
1433
1271440
    ConstraintCP c_i = *i;
1434
1271440
    Assert(c_i->hasProof());
1435
1271440
    d_database->d_antecedents.push_back(c_i);
1436
  }
1437
94902
  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1438
1439
  RationalVectorCP coeffsCopy;
1440
94902
  if (ARITH_PROOF_ON())
1441
  {
1442
11765
    Assert(coeffs != RationalVectorCPSentinel);
1443
11765
    coeffsCopy = new RationalVector(*coeffs);
1444
  }
1445
  else
1446
  {
1447
83137
    coeffsCopy = RationalVectorCPSentinel;
1448
  }
1449
94902
  d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
1450
1451
94902
  Assert(inConflict() == nowInConflict);
1452
94902
  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
1453
    Debug("constraint::conflictCommit") << "inConflict@impliedByFarkas " << this << std::endl;
1454
  }
1455
94902
  if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
1456
    getConstraintRule().print(Debug("constraints::wffp"));
1457
  }
1458
94902
  Assert(wellFormedFarkasProof());
1459
94902
}
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
183980
void Constraint::setEqualityEngineProof(){
1479
183980
  Debug("constraints::pf") << "setEqualityEngineProof(" << this;
1480
183980
  Debug("constraints::pf") << ")" << std::endl;
1481
183980
  Assert(truthIsUnknown());
1482
183980
  Assert(hasLiteral());
1483
183980
  d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
1484
183980
}
1485
1486
1487
3932041
SortedConstraintMap& Constraint::constraintSet() const{
1488
3932041
  Assert(d_database->variableDatabaseIsSetup(d_variable));
1489
3932041
  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
93582
Node Constraint::externalImplication(const ConstraintCPVec& b) const{
1504
93582
  Assert(hasLiteral());
1505
187164
  Node antecedent = externalExplainByAssertions(b);
1506
187164
  Node implied = getLiteral();
1507
187164
  return antecedent.impNode(implied);
1508
}
1509
1510
1511
1053681
Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
1512
1053681
  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
82815
TrustNode Constraint::externalExplainConflict() const
1553
{
1554
82815
  Debug("pf::arith::explain") << this << std::endl;
1555
82815
  Assert(inConflict());
1556
165630
  NodeBuilder<> nb(kind::AND);
1557
165630
  auto pf1 = externalExplainByAssertions(nb);
1558
165630
  auto not2 = getNegation()->getProofLiteral().negate();
1559
165630
  auto pf2 = getNegation()->externalExplainByAssertions(nb);
1560
165630
  Node n = safeConstructNary(nb);
1561
82815
  if (d_database->isProofEnabled())
1562
  {
1563
10830
    auto pfNot2 = d_database->d_pnm->mkNode(
1564
21660
        PfRule::MACRO_SR_PRED_TRANSFORM, {pf1}, {not2});
1565
21660
    std::vector<Node> lits;
1566
10830
    if (n.getKind() == Kind::AND)
1567
    {
1568
10830
      lits.insert(lits.end(), n.begin(), n.end());
1569
    }
1570
    else
1571
    {
1572
      lits.push_back(n);
1573
    }
1574
10830
    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
21660
                                    getNegation()->getProofLiteral()};
1584
    auto bot =
1585
10830
        not2.getKind() == Kind::NOT
1586
29406
            ? d_database->d_pnm->mkNode(PfRule::CONTRA, {pf2, pfNot2}, {})
1587
42292
            : d_database->d_pnm->mkNode(PfRule::CONTRA, {pfNot2, pf2}, {});
1588
10830
    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
21660
    auto confPf = d_database->d_pnm->mkScope(bot, lits);
1597
10830
    return d_database->d_pfGen->mkTrustNode(
1598
10830
        safeConstructNary(Kind::AND, lits), confPf, true);
1599
  }
1600
  else
1601
  {
1602
71985
    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
1053681
Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
1653
2107362
  NodeBuilder<> nb(kind::AND);
1654
1053681
  ConstraintCPVec::const_iterator i, end;
1655
2324719
  for(i = v.begin(), end = v.end(); i != end; ++i){
1656
1271038
    ConstraintCP v_i = *i;
1657
1271038
    v_i->externalExplain(nb, order);
1658
  }
1659
2107362
  return safeConstructNary(nb);
1660
}
1661
1662
5513967
std::shared_ptr<ProofNode> Constraint::externalExplain(
1663
    NodeBuilder<>& nb, AssertionOrder order) const
1664
{
1665
5513967
  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
5513967
  Assert(hasProof());
1673
5513967
  Assert(!isAssumption() || assertedToTheTheory());
1674
5513967
  Assert(!isInternalAssumption());
1675
5513967
  std::shared_ptr<ProofNode> pf{};
1676
1677
5513967
  ProofNodeManager* pnm = d_database->d_pnm;
1678
1679
5513967
  if (assertedBefore(order))
1680
  {
1681
4906130
    Debug("pf::arith::explain") << "  already asserted" << std::endl;
1682
4906130
    nb << getWitness();
1683
4906130
    if (d_database->isProofEnabled())
1684
    {
1685
478252
      pf = pnm->mkAssume(getWitness());
1686
      // If the witness and literal differ, prove the difference through a
1687
      // rewrite.
1688
478252
      if (getWitness() != getProofLiteral())
1689
      {
1690
924417
        pf = pnm->mkNode(
1691
616278
            PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {getProofLiteral()});
1692
      }
1693
    }
1694
  }
1695
607837
  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
601879
    Debug("pf::arith::explain") << "  recursion!" << std::endl;
1734
601879
    Assert(!isAssumption());
1735
601879
    AntecedentId p = getEndAntecedent();
1736
601879
    ConstraintCP antecedent = d_database->d_antecedents[p];
1737
1203758
    std::vector<std::shared_ptr<ProofNode>> children;
1738
1739
3504823
    while (antecedent != NullConstraint)
1740
    {
1741
1451472
      Debug("pf::arith::explain") << "Explain " << antecedent << std::endl;
1742
2902944
      auto pn = antecedent->externalExplain(nb, order);
1743
1451472
      if (d_database->isProofEnabled())
1744
      {
1745
116436
        children.push_back(pn);
1746
      }
1747
1451472
      --p;
1748
1451472
      antecedent = d_database->d_antecedents[p];
1749
    }
1750
1751
601879
    if (d_database->isProofEnabled())
1752
    {
1753
72539
      switch (getProofType())
1754
      {
1755
        case ArithProofType::AssumeAP:
1756
        case ArithProofType::EqualityEngineAP:
1757
        {
1758
          Unreachable() << "These should be handled above";
1759
          break;
1760
        }
1761
10841
        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
21682
          std::vector<std::shared_ptr<ProofNode>> farkasChildren;
1772
10841
          farkasChildren.push_back(
1773
21682
              pnm->mkAssume(getNegation()->getProofLiteral()));
1774
10841
          farkasChildren.insert(
1775
21682
              farkasChildren.end(), children.rbegin(), children.rend());
1776
1777
10841
          NodeManager* nm = NodeManager::currentNM();
1778
1779
          // Enumerate d_farkasCoefficients as nodes.
1780
21682
          std::vector<Node> farkasCoeffs;
1781
72388
          for (Rational r : *getFarkasCoefficients())
1782
          {
1783
61547
            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
21682
                          farkasCoeffs);
1791
1792
          // Provable rewrite the result
1793
          auto botPf = pnm->mkNode(
1794
21682
              PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
1795
1796
          // Scope out the negated constraint, yielding a proof of the
1797
          // constraint.
1798
21682
          std::vector<Node> assump{getNegation()->getProofLiteral()};
1799
21682
          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
32523
          pf = pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
1806
                           {maybeDoubleNotPf},
1807
21682
                           {getProofLiteral()});
1808
1809
10841
          break;
1810
        }
1811
57666
        case ArithProofType::IntTightenAP:
1812
        {
1813
57666
          if (isUpperBound())
1814
          {
1815
56467
            pf = pnm->mkNode(
1816
112934
                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
57666
          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
5513967
  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
701430
ConstraintP Constraint::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const {
1875
701430
  Assert(initialized());
1876
701430
  Assert(!asserted || hasLiteral);
1877
1878
701430
  SortedConstraintMapConstIterator i = d_variablePosition;
1879
701430
  const SortedConstraintMap& scm = constraintSet();
1880
701430
  SortedConstraintMapConstIterator i_begin = scm.begin();
1881
2277380
  while(i != i_begin){
1882
910834
    --i;
1883
910834
    const ValueCollection& vc = i->second;
1884
910834
    if(vc.hasLowerBound()){
1885
236592
      ConstraintP weaker = vc.getLowerBound();
1886
1887
      // asserted -> hasLiteral
1888
      // hasLiteral -> weaker->hasLiteral()
1889
      // asserted -> weaker->assertedToTheTheory()
1890
489176
      if((!hasLiteral || (weaker->hasLiteral())) &&
1891
258348
         (!asserted || ( weaker->assertedToTheTheory()))){
1892
122859
        return weaker;
1893
      }
1894
    }
1895
  }
1896
578571
  return NullConstraint;
1897
}
1898
1899
336506
ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const {
1900
336506
  SortedConstraintMapConstIterator i = d_variablePosition;
1901
336506
  const SortedConstraintMap& scm = constraintSet();
1902
336506
  SortedConstraintMapConstIterator i_end = scm.end();
1903
1904
336506
  ++i;
1905
1001154
  for(; i != i_end; ++i){
1906
439839
    const ValueCollection& vc = i->second;
1907
439839
    if(vc.hasUpperBound()){
1908
142127
      ConstraintP weaker = vc.getUpperBound();
1909
364745
      if((!hasLiteral || (weaker->hasLiteral())) &&
1910
226260
         (!asserted || ( weaker->assertedToTheTheory()))){
1911
107515
        return weaker;
1912
      }
1913
    }
1914
  }
1915
1916
228991
  return NullConstraint;
1917
}
1918
1919
7562136
ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const {
1920
7562136
  Assert(variableDatabaseIsSetup(v));
1921
7562136
  Assert(t == UpperBound || t == LowerBound);
1922
1923
7562136
  SortedConstraintMap& scm = getVariableSCM(v);
1924
7562136
  if(t == UpperBound){
1925
3774329
    SortedConstraintMapConstIterator i = scm.lower_bound(r);
1926
3774329
    SortedConstraintMapConstIterator i_end = scm.end();
1927
3774329
    Assert(i == i_end || r <= i->first);
1928
7836505
    for(; i != i_end; i++){
1929
3416659
      Assert(r <= i->first);
1930
3416659
      const ValueCollection& vc = i->second;
1931
3416659
      if(vc.hasUpperBound()){
1932
1385571
        return vc.getUpperBound();
1933
      }
1934
    }
1935
2388758
    return NullConstraint;
1936
  }else{
1937
3787807
    Assert(t == LowerBound);
1938
3787807
    if(scm.empty()){
1939
228931
      return NullConstraint;
1940
    }else{
1941
3558876
      SortedConstraintMapConstIterator i = scm.lower_bound(r);
1942
3558876
      SortedConstraintMapConstIterator i_begin = scm.begin();
1943
3558876
      SortedConstraintMapConstIterator i_end = scm.end();
1944
3558876
      Assert(i == i_end || r <= i->first);
1945
1946
3558876
      int fdj = 0;
1947
1948
3558876
      if(i == i_end){
1949
1379676
        --i;
1950
1379676
        Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1951
2179200
      }else if( (i->first) > r){
1952
561835
        if(i == i_begin){
1953
508929
          return NullConstraint;
1954
        }else{
1955
52906
          --i;
1956
52906
          Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1957
        }
1958
      }
1959
1960
      do{
1961
3506376
        Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1962
3506376
        Assert(r >= i->first);
1963
3506376
        const ValueCollection& vc = i->second;
1964
1965
3506376
        if(vc.hasLowerBound()){
1966
1541341
          return vc.getLowerBound();
1967
        }
1968
1969
1965035
        if(i == i_begin){
1970
1508606
          break;
1971
        }else{
1972
456429
          --i;
1973
456429
        }
1974
      }while(true);
1975
1508606
      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
21574232
bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
1993
21574232
  return v < d_varDatabases.size();
1994
}
1995
1996
1997
8995
ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext):
1998
  d_constraintProofs(satContext),
1999
  d_canBePropagatedWatches(satContext),
2000
  d_assertionOrderWatches(satContext),
2001
8995
  d_splitWatches(userContext)
2002
8995
{}
2003
2004
2005
488566
void Constraint::setLiteral(Node n) {
2006
488566
  Debug("arith::constraint") << "Mapping " << *this << " to " << n << std::endl;
2007
488566
  Assert(Comparison::isNormalAtom(n));
2008
488566
  Assert(!hasLiteral());
2009
488566
  Assert(sanityChecking(n));
2010
488566
  d_literal = n;
2011
488566
  NodetoConstraintMap& map = d_database->d_nodetoConstraintMap;
2012
488566
  Assert(map.find(n) == map.end());
2013
488566
  map.insert(make_pair(d_literal, this));
2014
488566
}
2015
2016
1037856
Node Constraint::getProofLiteral() const
2017
{
2018
1037856
  Assert(d_database != nullptr);
2019
1037856
  Assert(d_database->d_avariables.hasNode(d_variable));
2020
2075712
  Node varPart = d_database->d_avariables.asNode(d_variable);
2021
  Kind cmp;
2022
1037856
  bool neg = false;
2023
1037856
  switch (d_type)
2024
  {
2025
428286
    case ConstraintType::UpperBound:
2026
    {
2027
428286
      if (d_value.infinitesimalIsZero())
2028
      {
2029
134513
        cmp = Kind::LEQ;
2030
      }
2031
      else
2032
      {
2033
293773
        cmp = Kind::LT;
2034
      }
2035
428286
      break;
2036
    }
2037
195933
    case ConstraintType::LowerBound:
2038
    {
2039
195933
      if (d_value.infinitesimalIsZero())
2040
      {
2041
156300
        cmp = Kind::GEQ;
2042
      }
2043
      else
2044
      {
2045
39633
        cmp = Kind::GT;
2046
      }
2047
195933
      break;
2048
    }
2049
322094
    case ConstraintType::Equality:
2050
    {
2051
322094
      cmp = Kind::EQUAL;
2052
322094
      break;
2053
    }
2054
91543
    case ConstraintType::Disequality:
2055
    {
2056
91543
      cmp = Kind::EQUAL;
2057
91543
      neg = true;
2058
91543
      break;
2059
    }
2060
    default: Unreachable() << d_type;
2061
  }
2062
1037856
  NodeManager* nm = NodeManager::currentNM();
2063
2075712
  Node constPart = nm->mkConst<Rational>(d_value.getNoninfinitesimalPart());
2064
2075712
  Node posLit = nm->mkNode(cmp, varPart, constPart);
2065
2075712
  return neg ? posLit.negate() : posLit;
2066
}
2067
2068
38050
void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
2069
                                 ConstraintP a,
2070
                                 ConstraintP b,
2071
                                 bool negateSecond) const
2072
{
2073
76100
  Node la = a->getLiteral();
2074
76100
  Node lb = b->getLiteral();
2075
76100
  Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la);
2076
38050
  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
32508
    out.push_back(TrustNode::mkTrustLemma(orN));
2109
  }
2110
38050
}
2111
2112
36172
void ConstraintDatabase::implies(std::vector<TrustNode>& out,
2113
                                 ConstraintP a,
2114
                                 ConstraintP b) const
2115
{
2116
72344
  Node la = a->getLiteral();
2117
72344
  Node lb = b->getLiteral();
2118
2119
72344
  Node neg_la = (la.getKind() == kind::NOT)? la[0] : la.notNode();
2120
2121
36172
  Assert(lb != neg_la);
2122
36172
  Assert(b->getNegation()->getType() == ConstraintType::LowerBound
2123
         || b->getNegation()->getType() == ConstraintType::UpperBound);
2124
36172
  proveOr(out,
2125
          a->getNegation(),
2126
          b,
2127
36172
          b->getNegation()->getType() == ConstraintType::LowerBound);
2128
36172
}
2129
2130
1878
void ConstraintDatabase::mutuallyExclusive(std::vector<TrustNode>& out,
2131
                                           ConstraintP a,
2132
                                           ConstraintP b) const
2133
{
2134
3756
  Node la = a->getLiteral();
2135
3756
  Node lb = b->getLiteral();
2136
2137
3756
  Node neg_la = la.negate();
2138
3756
  Node neg_lb = lb.negate();
2139
1878
  proveOr(out, a->getNegation(), b->getNegation(), true);
2140
1878
}
2141
2142
56153
void ConstraintDatabase::outputUnateInequalityLemmas(
2143
    std::vector<TrustNode>& out, ArithVar v) const
2144
{
2145
56153
  SortedConstraintMap& scm = getVariableSCM(v);
2146
56153
  SortedConstraintMapConstIterator scm_iter = scm.begin();
2147
56153
  SortedConstraintMapConstIterator scm_end = scm.end();
2148
56153
  ConstraintP prev = NullConstraint;
2149
  //get transitive unates
2150
  //Only lower bounds or upperbounds should be done.
2151
309507
  for(; scm_iter != scm_end; ++scm_iter){
2152
126677
    const ValueCollection& vc = scm_iter->second;
2153
126677
    if(vc.hasUpperBound()){
2154
61936
      ConstraintP ub = vc.getUpperBound();
2155
61936
      if(ub->hasLiteral()){
2156
61936
        if(prev != NullConstraint){
2157
29436
          implies(out, prev, ub);
2158
        }
2159
61936
        prev = ub;
2160
      }
2161
    }
2162
  }
2163
56153
}
2164
2165
56153
void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<TrustNode>& out,
2166
                                                   ArithVar v) const
2167
{
2168
112306
  vector<ConstraintP> equalities;
2169
2170
56153
  SortedConstraintMap& scm = getVariableSCM(v);
2171
56153
  SortedConstraintMapConstIterator scm_iter = scm.begin();
2172
56153
  SortedConstraintMapConstIterator scm_end = scm.end();
2173
2174
309507
  for(; scm_iter != scm_end; ++scm_iter){
2175
126677
    const ValueCollection& vc = scm_iter->second;
2176
126677
    if(vc.hasEquality()){
2177
15729
      ConstraintP eq = vc.getEquality();
2178
15729
      if(eq->hasLiteral()){
2179
15729
        equalities.push_back(eq);
2180
      }
2181
    }
2182
  }
2183
2184
56153
  vector<ConstraintP>::const_iterator i, j, eq_end = equalities.end();
2185
71882
  for(i = equalities.begin(); i != eq_end; ++i){
2186
15729
    ConstraintP at_i = *i;
2187
17607
    for(j= i + 1; j != eq_end; ++j){
2188
1878
      ConstraintP at_j = *j;
2189
2190
1878
      mutuallyExclusive(out, at_i, at_j);
2191
    }
2192
  }
2193
2194
71882
  for(i = equalities.begin(); i != eq_end; ++i){
2195
15729
    ConstraintP eq = *i;
2196
15729
    const ValueCollection& vc = eq->getValueCollection();
2197
15729
    Assert(vc.hasEquality() && vc.getEquality()->hasLiteral());
2198
2199
15729
    bool hasLB = vc.hasLowerBound() && vc.getLowerBound()->hasLiteral();
2200
15729
    bool hasUB = vc.hasUpperBound() && vc.getUpperBound()->hasLiteral();
2201
2202
15729
    ConstraintP lb = hasLB ?
2203
15729
      vc.getLowerBound() : eq->getStrictlyWeakerLowerBound(true, false);
2204
15729
    ConstraintP ub = hasUB ?
2205
15729
      vc.getUpperBound() : eq->getStrictlyWeakerUpperBound(true, false);
2206
2207
15729
    if(hasUB && hasLB && !eq->isSplit()){
2208
115
      out.push_back(eq->split());
2209
    }
2210
15729
    if(lb != NullConstraint){
2211
2601
      implies(out, eq, lb);
2212
    }
2213
15729
    if(ub != NullConstraint){
2214
4135
      implies(out, eq, ub);
2215
    }
2216
  }
2217
56153
}
2218
2219
7407
void ConstraintDatabase::outputUnateEqualityLemmas(
2220
    std::vector<TrustNode>& lemmas) const
2221
{
2222
63560
  for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
2223
56153
    outputUnateEqualityLemmas(lemmas, v);
2224
  }
2225
7407
}
2226
2227
7407
void ConstraintDatabase::outputUnateInequalityLemmas(
2228
    std::vector<TrustNode>& lemmas) const
2229
{
2230
63560
  for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
2231
56153
    outputUnateInequalityLemmas(lemmas, v);
2232
  }
2233
7407
}
2234
2235
4666609
bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){
2236
4666609
  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
4666609
  }else if(!cons->isTrue()){
2242
2433908
    ++d_statistics.d_unatePropagateImplications;
2243
2433908
    Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
2244
2433908
    cons->impliedByUnate(ant, false);
2245
2433908
    cons->tryToPropagate();
2246
2433908
    return false;
2247
  } else {
2248
2232701
    return false;
2249
  }
2250
}
2251
2252
1017153
void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev){
2253
1017153
  Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl;
2254
1017153
  Assert(curr != prev);
2255
1017153
  Assert(curr != NullConstraint);
2256
1017153
  bool hasPrev = ! (prev == NullConstraint);
2257
1017153
  Assert(!hasPrev || curr->getValue() > prev->getValue());
2258
2259
1017153
  ++d_statistics.d_unatePropagateCalls;
2260
2261
1017153
  const SortedConstraintMap& scm = curr->constraintSet();
2262
1017153
  const SortedConstraintMapConstIterator scm_begin = scm.begin();
2263
1017153
  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
6101305
  while(scm_i != scm_begin){
2270
2760714
    --scm_i; // move the iterator back
2271
2272
2760714
    const ValueCollection& vc = scm_i->second;
2273
2274
    //If it has the previous element, do nothing and stop!
2275
3561500
    if(hasPrev &&
2276
800786
       vc.hasConstraintOfType(prev->getType())
2277
3272919
       && vc.getConstraintOfType(prev->getType()) == prev){
2278
218638
      break;
2279
    }
2280
2281
    //Don't worry about implying the negation of upperbound.
2282
    //These should all be handled by propagating the LowerBounds!
2283
2542076
    if(vc.hasLowerBound()){
2284
976986
      ConstraintP lb = vc.getLowerBound();
2285
976986
      if(handleUnateProp(curr, lb)){ return; }
2286
    }
2287
2542076
    if(vc.hasDisequality()){
2288
237775
      ConstraintP dis = vc.getDisequality();
2289
237775
      if(handleUnateProp(curr, dis)){ return; }
2290
    }
2291
  }
2292
}
2293
2294
1000480
void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev){
2295
1000480
  Debug("arith::unate") << "unatePropUpperBound " << curr << " " << prev << endl;
2296
1000480
  Assert(curr != prev);
2297
1000480
  Assert(curr != NullConstraint);
2298
1000480
  bool hasPrev = ! (prev == NullConstraint);
2299
1000480
  Assert(!hasPrev || curr->getValue() < prev->getValue());
2300
2301
1000480
  ++d_statistics.d_unatePropagateCalls;
2302
2303
1000480
  const SortedConstraintMap& scm = curr->constraintSet();
2304
1000480
  const SortedConstraintMapConstIterator scm_end = scm.end();
2305
1000480
  SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2306
1000480
  ++scm_i;
2307
7035458
  for(; scm_i != scm_end; ++scm_i){
2308
3187460
    const ValueCollection& vc = scm_i->second;
2309
2310
    //If it has the previous element, do nothing and stop!
2311
3750806
    if(hasPrev &&
2312
3543821
       vc.hasConstraintOfType(prev->getType()) &&
2313
356361
       vc.getConstraintOfType(prev->getType()) == prev){
2314
169971
      break;
2315
    }
2316
    //Don't worry about implying the negation of upperbound.
2317
    //These should all be handled by propagating the UpperBounds!
2318
3017489
    if(vc.hasUpperBound()){
2319
1208773
      ConstraintP ub = vc.getUpperBound();
2320
1208773
      if(handleUnateProp(curr, ub)){ return; }
2321
    }
2322
3017489
    if(vc.hasDisequality()){
2323
270135
      ConstraintP dis = vc.getDisequality();
2324
270135
      if(handleUnateProp(curr, dis)){ return; }
2325
    }
2326
  }
2327
}
2328
2329
876472
void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB){
2330
876472
  Debug("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " " << prevUB << endl;
2331
876472
  Assert(curr != prevLB);
2332
876472
  Assert(curr != prevUB);
2333
876472
  Assert(curr != NullConstraint);
2334
876472
  bool hasPrevLB = ! (prevLB == NullConstraint);
2335
876472
  bool hasPrevUB = ! (prevUB == NullConstraint);
2336
876472
  Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue());
2337
876472
  Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue());
2338
2339
876472
  ++d_statistics.d_unatePropagateCalls;
2340
2341
876472
  const SortedConstraintMap& scm = curr->constraintSet();
2342
876472
  SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition;
2343
876472
  SortedConstraintMapConstIterator scm_last = hasPrevUB ? prevUB->d_variablePosition : scm.end();
2344
876472
  SortedConstraintMapConstIterator scm_i;
2345
876472
  if(hasPrevLB){
2346
168310
    scm_i = prevLB->d_variablePosition;
2347
168310
    if(scm_i != scm_curr){ // If this does not move this past scm_curr, move it one forward
2348
36789
      ++scm_i;
2349
    }
2350
  }else{
2351
708162
    scm_i = scm.begin();
2352
  }
2353
2354
2707290
  for(; scm_i != scm_curr; ++scm_i){
2355
    // between the previous LB and the curr
2356
915409
    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
915409
    if(vc.hasLowerBound()){
2361
339976
      ConstraintP lb = vc.getLowerBound();
2362
339976
      if(handleUnateProp(curr, lb)){ return; }
2363
    }
2364
915409
    if(vc.hasDisequality()){
2365
312989
      ConstraintP dis = vc.getDisequality();
2366
312989
      if(handleUnateProp(curr, dis)){ return; }
2367
    }
2368
  }
2369
876472
  Assert(scm_i == scm_curr);
2370
876472
  if(!hasPrevUB || scm_i != scm_last){
2371
851932
    ++scm_i;
2372
  } // hasPrevUB implies scm_i != scm_last
2373
2374
4618882
  for(; scm_i != scm_last; ++scm_i){
2375
    // between the curr and the previous UB imply the upperbounds and disequalities.
2376
1871205
    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
1871205
    if(vc.hasUpperBound()){
2381
705190
      ConstraintP ub = vc.getUpperBound();
2382
705190
      if(handleUnateProp(curr, ub)){ return; }
2383
    }
2384
1871205
    if(vc.hasDisequality()){
2385
614785
      ConstraintP dis = vc.getDisequality();
2386
614785
      if(handleUnateProp(curr, dis)){ return; }
2387
    }
2388
  }
2389
}
2390
2391
318499
std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca, ConstraintCP cb){
2392
318499
  ConstraintType a = ca->getType();
2393
318499
  ConstraintType b = cb->getType();
2394
2395
318499
  Assert(a != Disequality);
2396
318499
  Assert(b != Disequality);
2397
2398
318499
  int a_sgn = (a == LowerBound) ? -1 : ((a == UpperBound) ? 1 : 0);
2399
318499
  int b_sgn = (b == LowerBound) ? -1 : ((b == UpperBound) ? 1 : 0);
2400
2401
318499
  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
215574
  }else if(a_sgn == 0){
2413
38806
    Assert(b_sgn != 0);
2414
38806
    Assert(a == Equality);
2415
38806
    a_sgn = -b_sgn;
2416
176768
  }else if(b_sgn == 0){
2417
107086
    Assert(a_sgn != 0);
2418
107086
    Assert(b == Equality);
2419
107086
    b_sgn = -a_sgn;
2420
  }
2421
318499
  Assert(a_sgn != 0);
2422
318499
  Assert(b_sgn != 0);
2423
2424
636998
  Debug("arith::unateFarkasSigns") << "Constraint::unateFarkasSigns("<<a <<", " << b << ") -> "
2425
318499
                                   << "("<<a_sgn<<", "<< b_sgn <<")"<< endl;
2426
318499
  return make_pair(a_sgn, b_sgn);
2427
}
2428
2429
}/* CVC4::theory::arith namespace */
2430
}/* CVC4::theory namespace */
2431
26676
}/* CVC4 namespace */