GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/constraint.h Lines: 114 120 95.0 %
Date: 2021-03-23 Branches: 42 238 17.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file constraint.h
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 Defines Constraint and ConstraintDatabase which is the internal
13
 ** representation of variables in arithmetic
14
 **
15
 ** This file defines Constraint and ConstraintDatabase.
16
 ** A Constraint is the internal representation of literals in TheoryArithmetic.
17
 ** Constraints are fundamentally a triple:
18
 **  - ArithVar associated with the constraint,
19
 **  - a DeltaRational value,
20
 **  - and a ConstraintType.
21
 **
22
 ** Literals:
23
 **   The constraint may also keep track of a node corresponding to the
24
 **   Constraint.
25
 **   This can be accessed by getLiteral() in O(1) if it has been set.
26
 **   This node must be in normal form and may be used for communication with
27
 **   the TheoryEngine.
28
 **
29
 ** In addition, Constraints keep track of the following:
30
 **  - A Constraint that is the negation of the Constraint.
31
 **  - An iterator into a set of Constraints for the ArithVar sorted by
32
 **    DeltaRational value.
33
 **  - A context dependent internal proof of the node that can be used for
34
 **    explanations.
35
 **  - Whether an equality/disequality has been split in the user context via a
36
 **    lemma.
37
 **  - Whether a constraint, be be used in explanations sent to the context
38
 **
39
 ** Looking up constraints:
40
 **  - All of the Constraints with associated nodes in the ConstraintDatabase
41
 **    can be accessed via a single hashtable lookup until the Constraint is
42
 **    removed.
43
 **  - Nodes that have not been associated to a constraints can be
44
 **    inserted/associated to existing nodes in O(log n) time.
45
 **
46
 ** Implications:
47
 **  - A Constraint can be used to find unate implications.
48
 **  - A unate implication is an implication based purely on the ArithVar
49
 **    matching  and the DeltaRational value.
50
 **    (implies (<= x c) (<= x d)) given c <= d
51
 **  - This is done using the iterator into the sorted set of constraints.
52
 **  - Given a tight constraint and previous tightest constraint, this will
53
 **    efficiently propagate internally.
54
 **
55
 ** Additing and Removing Constraints
56
 **  - Adding Constraints takes O(log n) time where n is the number of
57
 **    constraints associated with the ArithVar.
58
 **  - Removing Constraints takes O(1) time.
59
 **
60
 ** Internals:
61
 **  - Constraints are pointers to ConstraintValues.
62
 **  - Undefined Constraints are NullConstraint.
63
 **
64
 ** Assumption vs. Assertion:
65
 ** - An assertion is anything on the theory d_fact queue.
66
 **   This includes any thing propagated and returned to the fact queue.
67
 **   These can be used in external conflicts and propagations of earlier
68
 **   proofs.
69
 ** - An assumption is anything on the theory d_fact queue that has no further
70
 **   explanation i.e. this theory did not propagate it.
71
 ** - To set something an assumption, first set it as being as assertion.
72
 ** - Internal assumptions have no explanations and must be regressed out of the
73
 **   proof.
74
 **/
75
76
#include "cvc4_private.h"
77
78
#ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
79
#define CVC4__THEORY__ARITH__CONSTRAINT_H
80
81
#include <unordered_map>
82
#include <vector>
83
84
#include "base/configuration_private.h"
85
#include "context/cdlist.h"
86
#include "context/cdqueue.h"
87
#include "expr/node.h"
88
#include "theory/arith/arithvar.h"
89
#include "theory/arith/callbacks.h"
90
#include "theory/arith/constraint_forward.h"
91
#include "theory/arith/delta_rational.h"
92
#include "theory/arith/proof_macros.h"
93
#include "theory/trust_node.h"
94
#include "util/statistics_registry.h"
95
96
namespace CVC4 {
97
98
class ProofNodeManager;
99
100
namespace context {
101
class Context;
102
}
103
namespace theory {
104
105
class EagerProofGenerator;
106
107
namespace arith {
108
109
class Comparison;
110
class ArithCongruenceManager;
111
class ArithVariables;
112
113
/**
114
 * Logs the types of different proofs.
115
 * Current, proof types:
116
 * - NoAP             : This constraint is not known to be true.
117
 * - AssumeAP         : This is an input assertion. There is no proof.
118
 *                    : Something can be both asserted and have a proof.
119
 * - InternalAssumeAP : An internal assumption. This has no guarantee of having an external proof.
120
 *                    : This must be removed by regression.
121
 * - FarkasAP         : A proof with Farka's coefficients, i.e.
122
 *                    :  \sum lambda_i ( asNode(x_i) <= c_i  ) |= 0 < 0
123
 *                    : If proofs are on, coefficients will be logged.
124
 *                    : If proofs are off, coefficients will not be logged.
125
 *                    : A unate implication is a FarkasAP.
126
 * - TrichotomyAP     : This is any entailment using (x<= a and x >=a) => x = a
127
 *                    : Equivalently, (x > a or x < a or x = a)
128
 *                    : There are 3 candidate ways this can propagate:
129
 *                    :   !(x > a) and !(x = a) => x < a
130
 *                    :   !(x < a) and !(x = a) => x > a
131
 *                    :   !(x > a) and !(x < a) => x = a
132
 * - EqualityEngineAP : This is propagated by the equality engine.
133
 *                    : Consult this for the proof.
134
 * - IntTightenAP     : This is indicates that a bound involving integers was tightened.
135
 *                    : e.g. i < 5.5 became i <= 5, when i is an integer.
136
 * - IntHoleAP        : This is currently a catch-all for all integer specific reason.
137
 */
138
enum ArithProofType
139
  { NoAP,
140
    AssumeAP,
141
    InternalAssumeAP,
142
    FarkasAP,
143
    TrichotomyAP,
144
    EqualityEngineAP,
145
    IntTightenAP,
146
    IntHoleAP};
147
148
/**
149
 * The types of constraints.
150
 * The convex constraints are the constraints are LowerBound, Equality,
151
 * and UpperBound.
152
 */
153
enum ConstraintType {LowerBound, Equality, UpperBound, Disequality};
154
155
156
typedef context::CDList<ConstraintCP> CDConstraintList;
157
158
typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
159
160
typedef size_t ConstraintRuleID;
161
static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
162
163
typedef size_t AntecedentId;
164
static const AntecedentId AntecedentIdSentinel = std::numeric_limits<AntecedentId>::max();
165
166
167
typedef size_t AssertionOrder;
168
static const AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();
169
170
171
/**
172
 * A ValueCollection binds together convex constraints that have the same
173
 * DeltaRational value.
174
 */
175
class ValueCollection {
176
private:
177
178
  ConstraintP d_lowerBound;
179
  ConstraintP d_upperBound;
180
  ConstraintP d_equality;
181
  ConstraintP d_disequality;
182
183
public:
184
  ValueCollection();
185
186
  static ValueCollection mkFromConstraint(ConstraintP c);
187
188
  bool hasLowerBound() const;
189
  bool hasUpperBound() const;
190
  bool hasEquality() const;
191
  bool hasDisequality() const;
192
193
  bool hasConstraintOfType(ConstraintType t) const;
194
195
  ConstraintP getLowerBound() const;
196
  ConstraintP getUpperBound() const;
197
  ConstraintP getEquality() const;
198
  ConstraintP getDisequality() const;
199
200
  ConstraintP getConstraintOfType(ConstraintType t) const;
201
202
  /** Returns true if any of the constraints are non-null. */
203
  bool empty() const;
204
205
  /**
206
   * Remove the constraint of the type t from the collection.
207
   * Returns true if the ValueCollection is now empty.
208
   * If true is returned, d_value is now NULL.
209
   */
210
  void remove(ConstraintType t);
211
212
  /**
213
   * Adds a constraint to the set.
214
   * The collection must not have a constraint of that type already.
215
   */
216
  void add(ConstraintP c);
217
218
  void push_into(std::vector<ConstraintP>& vec) const;
219
220
  ConstraintP nonNull() const;
221
222
  ArithVar getVariable() const;
223
  const DeltaRational& getValue() const;
224
};
225
226
/**
227
 * A Map of ValueCollections sorted by the associated DeltaRational values.
228
 *
229
 * Discussion:
230
 * While it is more natural to consider this a set, this cannot be a set as in
231
 * sets the type of both iterator and const_iterator in sets are
232
 * "constant iterators".  We require iterators that dereference to
233
 * ValueCollection&.
234
 *
235
 * See:
236
 * http://gcc.gnu.org/onlinedocs/libstdc++/ext/lwg-defects.html#103
237
 */
238
typedef std::map<DeltaRational, ValueCollection> SortedConstraintMap;
239
typedef SortedConstraintMap::iterator SortedConstraintMapIterator;
240
typedef SortedConstraintMap::const_iterator SortedConstraintMapConstIterator;
241
242
/** A Pair associating a variables and a Sorted ConstraintSet. */
243
146448
struct PerVariableDatabase{
244
  ArithVar d_var;
245
  SortedConstraintMap d_constraints;
246
247
  // x ? c_1, x ? c_2, x ? c_3, ...
248
  // where ? is a non-empty subset of {lb, ub, eq}
249
  // c_1 < c_2 < c_3 < ...
250
251
146448
  PerVariableDatabase(ArithVar v) : d_var(v), d_constraints() {}
252
253
  bool empty() const {
254
    return d_constraints.empty();
255
  }
256
257
  static bool IsEmpty(const PerVariableDatabase& p){
258
    return p.empty();
259
  }
260
};
261
262
/**
263
 * If proofs are on, there is a vector of rationals for farkas coefficients.
264
 * This is the owner of the memory for the vector, and calls delete upon
265
 * cleanup.
266
 *
267
 */
268
struct ConstraintRule {
269
  ConstraintP d_constraint;
270
  ArithProofType d_proofType;
271
  AntecedentId d_antecedentEnd;
272
273
  /**
274
   * In this comment, we abbreviate ConstraintDatabase::d_antecedents
275
   * and d_farkasCoefficients as ans and fc.
276
   *
277
   * This list is always empty if proofs are not enabled.
278
   *
279
   * If proofs are enabled, the proof of constraint c at p in ans[p] of length n
280
   * is (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
281
   *
282
   * Farkas' proofs show a contradiction with the negation of c, c_not =
283
   * c->getNegation().
284
   *
285
   * We treat the position for NullConstraint (p-n) as the position for the
286
   * farkas coefficient for so we pretend c_not is ans[p-n]. So this correlation
287
   * for the constraints we are going to use: (c_not, ans[p-n+(1)], ... ,
288
   * ans[p-n+(n-1)], ans[p-n+(n)]) With the coefficients at positions: (fc[0],
289
   * fc[1)], ... fc[n])
290
   *
291
   * The index of the constraints in the proof are {i | i <= 0 <= n] } (with
292
   * c_not being p-n). Partition the indices into L, U, and E, the lower bounds,
293
   * the upper bounds and equalities.
294
   *
295
   * We standardize the proofs to be upper bound oriented following the
296
   * convention: A x <= b with the proof witness of the form (lambda) Ax <=
297
   * (lambda) b and lambda >= 0.
298
   *
299
   * To accomplish this cleanly, the fc coefficients must be negative for lower
300
   * bounds. The signs of equalities can be either positive or negative.
301
   *
302
   * Thus the proof corresponds to (with multiplication over inequalities):
303
   *    \sum_{u in U} fc[u] ans[p-n+u] + \sum_{e in E} fc[e] ans[p-n+e]
304
   *  + \sum_{l in L} fc[l] ans[p-n+l]
305
   * |= 0 < 0
306
   * where fc[u] > 0, fc[l] < 0, and fc[e] != 0 (i.e. it can be either +/-).
307
   *
308
   * There is no requirement that the proof is minimal.
309
   * We do however use all of the constraints by requiring non-zero
310
   * coefficients.
311
   */
312
  RationalVectorCP d_farkasCoefficients;
313
  ConstraintRule()
314
    : d_constraint(NullConstraint)
315
    , d_proofType(NoAP)
316
    , d_antecedentEnd(AntecedentIdSentinel)
317
  {
318
    d_farkasCoefficients = RationalVectorCPSentinel;
319
  }
320
321
4960021
  ConstraintRule(ConstraintP con, ArithProofType pt)
322
4960021
    : d_constraint(con)
323
    , d_proofType(pt)
324
4960021
    , d_antecedentEnd(AntecedentIdSentinel)
325
  {
326
4960021
    d_farkasCoefficients = RationalVectorCPSentinel;
327
4960021
  }
328
1667008
  ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd)
329
1667008
    : d_constraint(con)
330
    , d_proofType(pt)
331
1667008
    , d_antecedentEnd(antecedentEnd)
332
  {
333
1667008
    d_farkasCoefficients = RationalVectorCPSentinel;
334
1667008
  }
335
336
2534865
  ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs)
337
2534865
    : d_constraint(con)
338
    , d_proofType(pt)
339
2534865
    , d_antecedentEnd(antecedentEnd)
340
  {
341
2534865
    Assert(ARITH_PROOF_ON() || coeffs == RationalVectorCPSentinel);
342
2534865
    d_farkasCoefficients = coeffs;
343
2534865
  }
344
345
  void print(std::ostream& out) const;
346
  void debugPrint() const;
347
}; /* class ConstraintRule */
348
349
class Constraint {
350
351
  friend class ConstraintDatabase;
352
353
 public:
354
  /**
355
   * This begins construction of a minimal constraint.
356
   *
357
   * This should only be called by ConstraintDatabase.
358
   *
359
   * Because of circular dependencies a Constraint is not fully valid until
360
   * initialize has been called on it.
361
   */
362
  Constraint(ArithVar x,  ConstraintType t, const DeltaRational& v);
363
364
  /**
365
   * Destructor for a constraint.
366
   * This should only be called if safeToGarbageCollect() is true.
367
   */
368
  ~Constraint();
369
370
  static ConstraintType constraintTypeOfComparison(const Comparison& cmp);
371
372
15925631
  inline ConstraintType getType() const {
373
15925631
    return d_type;
374
  }
375
376
23793352
  inline ArithVar getVariable() const {
377
23793352
    return d_variable;
378
  }
379
380
40326040
  const DeltaRational& getValue() const {
381
40326040
    return d_value;
382
  }
383
384
1682095
  inline ConstraintP getNegation() const {
385
1682095
    return d_negation;
386
  }
387
388
7022007
  bool isEquality() const{
389
7022007
    return d_type == Equality;
390
  }
391
845744
  bool isDisequality() const{
392
845744
    return d_type == Disequality;
393
  }
394
5002132
  bool isLowerBound() const{
395
5002132
    return d_type == LowerBound;
396
  }
397
5084102
  bool isUpperBound() const{
398
5084102
    return d_type == UpperBound;
399
  }
400
1367262
  bool isStrictUpperBound() const{
401
1367262
    Assert(isUpperBound());
402
1367262
    return getValue().infinitesimalSgn() < 0;
403
  }
404
405
1213646
  bool isStrictLowerBound() const{
406
1213646
    Assert(isLowerBound());
407
1213646
    return getValue().infinitesimalSgn() > 0;
408
  }
409
410
1633583
  bool isSplit() const {
411
1633583
    return d_split;
412
  }
413
414
  /**
415
   * Splits the node in the user context.
416
   * Returns a lemma that is assumed to be true for the rest of the user context.
417
   * Constraint must be an equality or disequality.
418
   */
419
  TrustNode split();
420
421
10510933
  bool canBePropagated() const {
422
10510933
    return d_canBePropagated;
423
  }
424
  void setCanBePropagated();
425
426
  /**
427
   * Light wrapper for calling setCanBePropagated(),
428
   * on this and this->d_negation.
429
   */
430
344237
  void setPreregistered(){
431
344237
    setCanBePropagated();
432
344237
    d_negation->setCanBePropagated();
433
344237
  }
434
435
56794002
  bool assertedToTheTheory() const {
436
56794002
    Assert((d_assertionOrder < AssertionOrderSentinel) != d_witness.isNull());
437
56794002
    return d_assertionOrder < AssertionOrderSentinel;
438
  }
439
5862927
  TNode getWitness() const {
440
5862927
    Assert(assertedToTheTheory());
441
5862927
    return d_witness;
442
  }
443
444
5514271
  bool assertedBefore(AssertionOrder time) const {
445
5514271
    return d_assertionOrder < time;
446
  }
447
448
  /**
449
   * Sets the witness literal for a node being on the assertion stack.
450
   *
451
   * If the negation of the node is true, inConflict must be true.
452
   * If the negation of the node is false, inConflict must be false.
453
   * Hence, negationHasProof() == inConflict.
454
   *
455
   * This replaces:
456
   *   void setAssertedToTheTheory(TNode witness);
457
   *   void setAssertedToTheTheoryWithNegationTrue(TNode witness);
458
   */
459
  void setAssertedToTheTheory(TNode witness, bool inConflict);
460
461
13849493
  bool hasLiteral() const {
462
13849493
    return !d_literal.isNull();
463
  }
464
465
  void setLiteral(Node n);
466
467
1504485
  Node getLiteral() const {
468
1504485
    Assert(hasLiteral());
469
1504485
    return d_literal;
470
  }
471
472
  /** Gets a literal in the normal form suitable for proofs.
473
   * That is, (sum of non-const monomials) >< const.
474
   *
475
   * This is a sister method to `getLiteral`, which returns a normal form
476
   * literal, suitable for external solving use.
477
   */
478
  Node getProofLiteral() const;
479
480
  /**
481
   * Set the node as having a proof and being an assumption.
482
   * The node must be assertedToTheTheory().
483
   *
484
   * Precondition: negationHasProof() == inConflict.
485
   *
486
   * Replaces:
487
   *  selfExplaining().
488
   *  selfExplainingWithNegationTrue().
489
   */
490
  void setAssumption(bool inConflict);
491
492
  /** Returns true if the node is an assumption.*/
493
  bool isAssumption() const;
494
495
  /** Set the constraint to have an EqualityEngine proof. */
496
  void setEqualityEngineProof();
497
  bool hasEqualityEngineProof() const;
498
499
  /** Returns true if the node has a Farkas' proof. */
500
  bool hasFarkasProof() const;
501
502
  /**
503
   * @brief Returns whether this constraint is provable using a Farkas
504
   * proof applied to (possibly tightened) input assertions.
505
   *
506
   * An example of a constraint that has a simple Farkas proof:
507
   *    x <= 0 proven from x + y <= 0 and x - y <= 0.
508
   *
509
   * An example of another constraint that has a simple Farkas proof:
510
   *    x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y
511
   *       (integer bound-tightening is applied first!).
512
   *
513
   * An example of a constraint that might be proven **without** a simple
514
   * Farkas proof:
515
   *    x < 0 proven from not(x == 0) and not(x > 0).
516
   *
517
   * This could be proven internally by the arithmetic theory using
518
   * `TrichotomyAP` as the proof type.
519
   *
520
   */
521
  bool hasSimpleFarkasProof() const;
522
  /**
523
   * Returns whether this constraint is an assumption or a tightened
524
   * assumption.
525
   */
526
  bool isPossiblyTightenedAssumption() const;
527
528
  /** Returns true if the node has a int bound tightening proof. */
529
  bool hasIntTightenProof() const;
530
531
  /** Returns true if the node has a int hole proof. */
532
  bool hasIntHoleProof() const;
533
534
  /** Returns true if the node has a trichotomy proof. */
535
  bool hasTrichotomyProof() const;
536
537
  void printProofTree(std::ostream & out, size_t depth = 0) const;
538
539
  /**
540
   * A sets the constraint to be an internal assumption.
541
   *
542
   * This does not need to have a witness or an associated literal.
543
   * This is always itself in the explanation fringe for both conflicts
544
   * and propagation.
545
   * This cannot be converted back into a Node conflict or explanation.
546
   *
547
   * This cannot have a proof or be asserted to the theory!
548
   *
549
   */
550
  void setInternalAssumption(bool inConflict);
551
  bool isInternalAssumption() const;
552
553
  /**
554
   * Returns a explanation of the constraint that is appropriate for conflicts.
555
   *
556
   * This is not appropriate for propagation!
557
   *
558
   * This is the minimum fringe of the implication tree s.t.
559
   * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
560
   */
561
  TrustNode externalExplainByAssertions() const;
562
563
  /**
564
   * Writes an explanation of a constraint into the node builder.
565
   * Pushes back an explanation that is acceptable to send to the sat solver.
566
   * nb is assumed to be an AND.
567
   *
568
   * This is the minimum fringe of the implication tree s.t.
569
   * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
570
   *
571
   * This is not appropriate for propagation!
572
   * Use explainForPropagation() instead.
573
   */
574
2778218
  std::shared_ptr<ProofNode> externalExplainByAssertions(
575
      NodeBuilder<>& nb) const
576
  {
577
2778218
    return externalExplain(nb, AssertionOrderSentinel);
578
  }
579
580
  /* Equivalent to calling externalExplainByAssertions on all constraints in b */
581
  static Node externalExplainByAssertions(const ConstraintCPVec& b);
582
  static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b);
583
  static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c);
584
585
  /**
586
   * This is the minimum fringe of the implication tree s.t. every constraint is
587
   * - assertedToTheTheory(),
588
   * - isInternalDecision() or
589
   * - hasEqualityEngineProof().
590
   */
591
  static void assertionFringe(ConstraintCPVec& v);
592
  static void assertionFringe(ConstraintCPVec& out, const ConstraintCPVec& in);
593
594
  /** The fringe of a farkas' proof. */
595
  bool onFringe() const {
596
    return assertedToTheTheory() || isInternalAssumption() || hasEqualityEngineProof();
597
  }
598
599
  /**
600
   * Returns an explanation of a propagation by the ConstraintDatabase.
601
   * The constraint must have a proof.
602
   * The constraint cannot be an assumption.
603
   *
604
   * This is the minimum fringe of the implication tree (excluding the
605
   * constraint itself) s.t. every constraint is assertedToTheTheory() or
606
   * hasEqualityEngineProof().
607
   *
608
   * All return conjuncts were asserted before this constraint.
609
   *
610
   * Requires the given node to rewrite to the canonical literal for this
611
   * constraint.
612
   *
613
   * @params n the literal to prove
614
   *           n must rewrite to the constraint's canonical literal
615
   *
616
   * @returns a trust node of the form:
617
   *         (=> explanation n)
618
   */
619
  TrustNode externalExplainForPropagation(TNode n) const;
620
621
  /**
622
   * Explain the constraint and its negation in terms of assertions.
623
   * The constraint must be in conflict.
624
   */
625
  TrustNode externalExplainConflict() const;
626
627
  /** The constraint is known to be true. */
628
163143554
  inline bool hasProof() const {
629
163143554
    return d_crid != ConstraintRuleIdSentinel;
630
  }
631
632
  /** The negation of the constraint is known to hold. */
633
52703511
  inline bool negationHasProof() const {
634
52703511
    return d_negation->hasProof();
635
  }
636
637
  /** Neither the contraint has a proof nor the negation has a proof.*/
638
184008
  bool truthIsUnknown() const {
639
184008
    return !hasProof() && !negationHasProof();
640
  }
641
642
  /** This is a synonym for hasProof(). */
643
16068989
  inline bool isTrue() const {
644
16068989
    return hasProof();
645
  }
646
647
  /** Both the constraint and its negation are true. */
648
10557862
  inline bool inConflict() const {
649
10557862
    return hasProof() && negationHasProof();
650
  }
651
652
  /**
653
   * Returns the constraint that corresponds to taking
654
   *    x r ceiling(getValue()) where r is the node's getType().
655
   * Esstentially this is an up branch.
656
   */
657
  ConstraintP getCeiling();
658
659
  /**
660
   * Returns the constraint that corresponds to taking
661
   *    x r floor(getValue()) where r is the node's getType().
662
   * Esstentially this is a down branch.
663
   */
664
  ConstraintP getFloor();
665
666
  static ConstraintP makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r);
667
668
  const ValueCollection& getValueCollection() const;
669
670
671
  ConstraintP getStrictlyWeakerUpperBound(bool hasLiteral, bool mustBeAsserted) const;
672
  ConstraintP getStrictlyWeakerLowerBound(bool hasLiteral, bool mustBeAsserted) const;
673
674
  /**
675
   * Marks a the constraint c as being entailed by a.
676
   * The Farkas proof 1*(a) + -1 (c) |= 0<0
677
   *
678
   * After calling impliedByUnate(), the caller should either raise a conflict
679
   * or try call tryToPropagate().
680
   */
681
  void impliedByUnate(ConstraintCP a, bool inConflict);
682
683
  /**
684
   * Marks a the constraint c as being entailed by a.
685
   * The reason has to do with integer bound tightening.
686
   *
687
   * After calling impliedByIntTighten(), the caller should either raise a conflict
688
   * or try call tryToPropagate().
689
   */
690
  void impliedByIntTighten(ConstraintCP a, bool inConflict);
691
692
  /**
693
   * Marks a the constraint c as being entailed by a.
694
   * The reason has to do with integer reasoning.
695
   *
696
   * After calling impliedByIntHole(), the caller should either raise a conflict
697
   * or try call tryToPropagate().
698
   */
699
  void impliedByIntHole(ConstraintCP a, bool inConflict);
700
701
  /**
702
   * Marks a the constraint c as being entailed by a.
703
   * The reason has to do with integer reasoning.
704
   *
705
   * After calling impliedByIntHole(), the caller should either raise a conflict
706
   * or try call tryToPropagate().
707
   */
708
  void impliedByIntHole(const ConstraintCPVec& b, bool inConflict);
709
710
  /**
711
   * This is a lemma of the form:
712
   *   x < d or x = d or x > d
713
   * The current constraint c is one of the above constraints and {a,b}
714
   * are the negation of the other two constraints.
715
   *
716
   * Preconditions:
717
   * - negationHasProof() == inConflict.
718
   *
719
   * After calling impliedByTrichotomy(), the caller should either raise a conflict
720
   * or try call tryToPropagate().
721
   */
722
  void impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool inConflict);
723
724
  /**
725
   * Marks the node as having a Farkas proof.
726
   *
727
   * Preconditions:
728
   * - coeffs == NULL if proofs are off.
729
   * - See the comments for ConstraintRule for the form of coeffs when
730
   *   proofs are on.
731
   * - negationHasProof() == inConflict.
732
   *
733
   * After calling impliedByFarkas(), the caller should either raise a conflict
734
   * or try call tryToPropagate().
735
   */
736
  void impliedByFarkas(const ConstraintCPVec& b, RationalVectorCP coeffs, bool inConflict);
737
738
  /**
739
   * Generates an implication node, B => getLiteral(),
740
   * where B is the result of externalExplainByAssertions(b).
741
   * Does not guarantee b is the explanation of the constraint.
742
   */
743
  Node externalImplication(const ConstraintCPVec& b) const;
744
745
  /**
746
   * Returns true if the variable is assigned the value dr,
747
   * the constraint would be satisfied.
748
   */
749
  bool satisfiedBy(const DeltaRational& dr) const;
750
751
  /**
752
   * The node must have a proof already and be eligible for propagation!
753
   * You probably want to call tryToPropagate() instead.
754
   *
755
   * Preconditions:
756
   * - hasProof()
757
   * - canBePropagated()
758
   * - !assertedToTheTheory()
759
   */
760
  void propagate();
761
762
  /**
763
   * If the constraint
764
   *   canBePropagated() and
765
   *   !assertedToTheTheory(),
766
   * the constraint is added to the database's propagation queue.
767
   *
768
   * Precondition:
769
   * - hasProof()
770
   */
771
  void tryToPropagate();
772
773
  /**
774
   * Returns a reference to the containing database.
775
   * Precondition: the constraint must be initialized.
776
   */
777
  const ConstraintDatabase& getDatabase() const;
778
779
  /** Returns the constraint rule at the position. */
780
  const ConstraintRule& getConstraintRule() const;
781
782
 private:
783
  /**  Returns true if the constraint has been initialized. */
784
  bool initialized() const;
785
786
  /**
787
   * This initializes the fields that cannot be set in the constructor due to
788
   * circular dependencies.
789
   */
790
  void initialize(ConstraintDatabase* db,
791
                  SortedConstraintMapIterator v,
792
                  ConstraintP negation);
793
794
  class ConstraintRuleCleanup
795
  {
796
   public:
797
9161894
    inline void operator()(ConstraintRule* crp)
798
    {
799
9161894
      Assert(crp != NULL);
800
9161894
      ConstraintP constraint = crp->d_constraint;
801
9161894
      Assert(constraint->d_crid != ConstraintRuleIdSentinel);
802
9161894
      constraint->d_crid = ConstraintRuleIdSentinel;
803
9161894
      ARITH_PROOF({
804
        if (crp->d_farkasCoefficients != RationalVectorCPSentinel)
805
        {
806
          delete crp->d_farkasCoefficients;
807
        }
808
      });
809
9161894
    }
810
  };
811
812
  class CanBePropagatedCleanup
813
  {
814
   public:
815
688474
    inline void operator()(ConstraintP* p)
816
    {
817
688474
      ConstraintP constraint = *p;
818
688474
      Assert(constraint->d_canBePropagated);
819
688474
      constraint->d_canBePropagated = false;
820
688474
    }
821
  };
822
823
  class AssertionOrderCleanup
824
  {
825
   public:
826
5716677
    inline void operator()(ConstraintP* p)
827
    {
828
5716677
      ConstraintP constraint = *p;
829
5716677
      Assert(constraint->assertedToTheTheory());
830
5716677
      constraint->d_assertionOrder = AssertionOrderSentinel;
831
5716677
      constraint->d_witness = TNode::null();
832
5716677
      Assert(!constraint->assertedToTheTheory());
833
5716677
    }
834
  };
835
836
  class SplitCleanup
837
  {
838
   public:
839
29790
    inline void operator()(ConstraintP* p)
840
    {
841
29790
      ConstraintP constraint = *p;
842
29790
      Assert(constraint->d_split);
843
29790
      constraint->d_split = false;
844
29790
    }
845
  };
846
847
  /**
848
   * Returns true if the node is safe to garbage collect.
849
   * Both it and its negation must have no context dependent data set.
850
   */
851
  bool safeToGarbageCollect() const;
852
853
  /**
854
   * Returns true if the constraint has no context dependent data set.
855
   */
856
  bool contextDependentDataIsSet() const;
857
858
  /**
859
   * Returns true if the node correctly corresponds to the constraint that is
860
   * being set.
861
   */
862
  bool sanityChecking(Node n) const;
863
864
  /** Returns a reference to the map for d_variable. */
865
  SortedConstraintMap& constraintSet() const;
866
867
  /** Returns coefficients for the proofs for farkas cancellation. */
868
  static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);
869
870
  Node externalExplain(AssertionOrder order) const;
871
  /**
872
   * Returns an explanation of that was assertedBefore(order).
873
   * The constraint must have a proof.
874
   * The constraint cannot be selfExplaining().
875
   *
876
   * This is the minimum fringe of the implication tree
877
   * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
878
   */
879
  std::shared_ptr<ProofNode> externalExplain(NodeBuilder<>& nb,
880
                                             AssertionOrder order) const;
881
882
  static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
883
884
23583798
  inline ArithProofType getProofType() const {
885
23583798
    return getConstraintRule().d_proofType;
886
  }
887
888
601924
  inline AntecedentId getEndAntecedent() const {
889
601924
    return getConstraintRule().d_antecedentEnd;
890
  }
891
892
10845
  inline RationalVectorCP getFarkasCoefficients() const
893
  {
894
10845
    return ARITH_NULLPROOF(getConstraintRule().d_farkasCoefficients);
895
  }
896
897
  void debugPrint() const;
898
899
  /**
900
   * The proof of the node is empty.
901
   * The proof must be a special proof. Either
902
   *   isSelfExplaining() or
903
   *    hasEqualityEngineProof()
904
   */
905
  bool antecentListIsEmpty() const;
906
907
  bool antecedentListLengthIsOne() const;
908
909
  /** Return true if every element in b has a proof. */
910
  static bool allHaveProof(const ConstraintCPVec& b);
911
912
  /** Precondition: hasFarkasProof()
913
   * Computes the combination implied by the farkas coefficients. Sees if it is
914
   * a contradiction.
915
   */
916
917
  bool wellFormedFarkasProof() const;
918
919
  /** The ArithVar associated with the constraint. */
920
  const ArithVar d_variable;
921
922
  /** The type of the Constraint. */
923
  const ConstraintType d_type;
924
925
  /** The DeltaRational value with the constraint. */
926
  const DeltaRational d_value;
927
928
  /** A pointer to the associated database for the Constraint. */
929
  ConstraintDatabase* d_database;
930
931
  /**
932
   * The node to be communicated with the TheoryEngine.
933
   *
934
   * This is not context dependent, but may be set once.
935
   *
936
   * This must be set if the constraint canBePropagated().
937
   * This must be set if the constraint assertedToTheTheory().
938
   * Otherwise, this may be null().
939
   */
940
  Node d_literal;
941
942
  /** Pointer to the negation of the Constraint. */
943
  ConstraintP d_negation;
944
945
  /**
946
   * This is true if the associated node can be propagated.
947
   *
948
   * This should be enabled if the node has been preregistered.
949
   *
950
   * Sat Context Dependent.
951
   * This is initially false.
952
   */
953
  bool d_canBePropagated;
954
955
  /**
956
   * This is the order the constraint was asserted to the theory.
957
   * If this has been set, the node can be used in conflicts.
958
   * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the
959
   * explanation of d.
960
   *
961
   * This should be set after the literal is dequeued by Theory::get().
962
   *
963
   * Sat Context Dependent.
964
   * This is initially AssertionOrderSentinel.
965
   */
966
  AssertionOrder d_assertionOrder;
967
968
  /**
969
   * This is guaranteed to be on the fact queue.
970
   * For example if x + y = x + 1 is on the fact queue, then use this
971
   */
972
  TNode d_witness;
973
974
  /**
975
   * The position of the constraint in the constraint rule id.
976
   *
977
   * Sat Context Dependent.
978
   * This is initially
979
   */
980
  ConstraintRuleID d_crid;
981
982
  /**
983
   * True if the equality has been split.
984
   * Only meaningful if ConstraintType == Equality.
985
   *
986
   * User Context Dependent.
987
   * This is initially false.
988
   */
989
  bool d_split;
990
991
  /**
992
   * Position in sorted constraint set for the variable.
993
   * Unset if d_type is Disequality.
994
   */
995
  SortedConstraintMapIterator d_variablePosition;
996
997
}; /* class ConstraintValue */
998
999
std::ostream& operator<<(std::ostream& o, const Constraint& c);
1000
std::ostream& operator<<(std::ostream& o, const ConstraintP c);
1001
std::ostream& operator<<(std::ostream& o, const ConstraintCP c);
1002
std::ostream& operator<<(std::ostream& o, const ConstraintType t);
1003
std::ostream& operator<<(std::ostream& o, const ValueCollection& c);
1004
std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v);
1005
std::ostream& operator<<(std::ostream& o, const ArithProofType);
1006
1007
1008
class ConstraintDatabase {
1009
private:
1010
  /**
1011
   * The map from ArithVars to their unique databases.
1012
   * When the vector changes size, we cannot allow the maps to move so this
1013
   * is a vector of pointers.
1014
   */
1015
  std::vector<PerVariableDatabase*> d_varDatabases;
1016
1017
  SortedConstraintMap& getVariableSCM(ArithVar v) const;
1018
1019
  /** Maps literals to constraints.*/
1020
  NodetoConstraintMap d_nodetoConstraintMap;
1021
1022
  /**
1023
   * A queue of propagated constraints.
1024
   * ConstraintCP are pointers.
1025
   * The elements of the queue do not require destruction.
1026
   */
1027
  context::CDQueue<ConstraintCP> d_toPropagate;
1028
1029
  /**
1030
   * Proofs are lists of valid constraints terminated by the first null
1031
   * sentinel value in the proof list.
1032
   * We abbreviate d_antecedents as ans in the comment.
1033
   *
1034
   * The proof at p in ans[p] of length n is
1035
   *  (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
1036
   *
1037
   * The proof at p corresponds to the conjunction:
1038
   *  (and x_i)
1039
   *
1040
   * So the proof of a Constraint c corresponds to the horn clause:
1041
   *  (implies (and x_i) c)
1042
   * where (and x_i) is the proof at c.d_crid d_antecedentEnd.
1043
   *
1044
   * Constraints are pointers so this list is designed not to require any destruction.
1045
   */
1046
  CDConstraintList d_antecedents;
1047
1048
  typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup> ConstraintRuleList;
1049
  typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup> CBPList;
1050
  typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup> AOList;
1051
  typedef context::CDList<ConstraintP, Constraint::SplitCleanup> SplitList;
1052
1053
1054
1055
  /**
1056
   * The watch lists are collected together as they need to be garbage collected
1057
   * carefully.
1058
   */
1059
8994
  struct Watches{
1060
1061
    /**
1062
     * Contains the exact list of constraints that have a proof.
1063
     * Upon pop, this unsets d_crid to NoAP.
1064
     *
1065
     * The index in this list is the proper ordering of the proofs.
1066
     */
1067
    ConstraintRuleList d_constraintProofs;
1068
1069
    /**
1070
     * Contains the exact list of constraints that can be used for propagation.
1071
     */
1072
    CBPList d_canBePropagatedWatches;
1073
1074
    /**
1075
     * Contains the exact list of constraints that have been asserted to the theory.
1076
     */
1077
    AOList d_assertionOrderWatches;
1078
1079
1080
    /**
1081
     * Contains the exact list of atoms that have been preregistered.
1082
     * This is a pointer as it must be destroyed before the elements of
1083
     * d_varDatabases.
1084
     */
1085
    SplitList d_splitWatches;
1086
    Watches(context::Context* satContext, context::Context* userContext);
1087
  };
1088
  Watches* d_watches;
1089
1090
  void pushSplitWatch(ConstraintP c);
1091
  void pushCanBePropagatedWatch(ConstraintP c);
1092
  void pushAssertionOrderWatch(ConstraintP c, TNode witness);
1093
1094
  /** Assumes that antecedents have already been pushed. */
1095
  void pushConstraintRule(const ConstraintRule& crp);
1096
1097
  /** Returns true if all of the entries of the vector are empty. */
1098
  static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec);
1099
1100
  /** Map from nodes to arithvars. */
1101
  const ArithVariables& d_avariables;
1102
1103
819201
  const ArithVariables& getArithVariables() const{
1104
819201
    return d_avariables;
1105
  }
1106
1107
  ArithCongruenceManager& d_congruenceManager;
1108
1109
  const context::Context * const d_satContext;
1110
  /** Owned by the TheoryArithPrivate, used here. */
1111
  EagerProofGenerator* d_pfGen;
1112
  /** Owned by the TheoryArithPrivate, used here. */
1113
  ProofNodeManager* d_pnm;
1114
1115
  RaiseConflict d_raiseConflict;
1116
1117
1118
  const Rational d_one;
1119
  const Rational d_negOne;
1120
1121
  friend class Constraint;
1122
1123
 public:
1124
  ConstraintDatabase(context::Context* satContext,
1125
                     context::Context* userContext,
1126
                     const ArithVariables& variables,
1127
                     ArithCongruenceManager& dm,
1128
                     RaiseConflict conflictCallBack,
1129
                     EagerProofGenerator* pfGen,
1130
                     ProofNodeManager* pnm);
1131
1132
  ~ConstraintDatabase();
1133
1134
  /** Adds a literal to the database. */
1135
  ConstraintP addLiteral(TNode lit);
1136
1137
  /**
1138
   * If hasLiteral() is true, returns the constraint.
1139
   * Otherwise, returns NullConstraint.
1140
   */
1141
  ConstraintP lookup(TNode literal) const;
1142
1143
  /**
1144
   * Returns true if the literal has been added to the database.
1145
   * This is a hash table lookup.
1146
   * It does not look in the database for an equivalent corresponding constraint.
1147
   */
1148
  bool hasLiteral(TNode literal) const;
1149
1150
4470760
  bool hasMorePropagations() const{
1151
4470760
    return !d_toPropagate.empty();
1152
  }
1153
1154
723578
  ConstraintCP nextPropagation(){
1155
723578
    Assert(hasMorePropagations());
1156
1157
723578
    ConstraintCP p = d_toPropagate.front();
1158
723578
    d_toPropagate.pop();
1159
1160
723578
    return p;
1161
  }
1162
1163
  void addVariable(ArithVar v);
1164
  bool variableDatabaseIsSetup(ArithVar v) const;
1165
  void removeVariable(ArithVar v);
1166
1167
  /** Get an explanation and proof for this constraint from the equality engine
1168
   */
1169
  TrustNode eeExplain(ConstraintCP c) const;
1170
  /** Get an explanation for this constraint from the equality engine */
1171
  void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const;
1172
1173
  /**
1174
   * Returns a constraint with the variable v, the constraint type t, and a value
1175
   * dominated by r (explained below) if such a constraint exists in the database.
1176
   * If no such constraint exists, NullConstraint is returned.
1177
   *
1178
   * t must be either UpperBound or LowerBound.
1179
   * The returned value v is dominated:
1180
   *  If t is UpperBound, r <= v
1181
   *  If t is LowerBound, r >= v
1182
   *
1183
   * variableDatabaseIsSetup(v) must be true.
1184
   */
1185
  ConstraintP getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const;
1186
1187
  /** Returns the constraint, if it exists */
1188
  ConstraintP lookupConstraint(ArithVar v, ConstraintType t, const DeltaRational& r) const;
1189
1190
  /**
1191
   * Returns a constraint with the variable v, the constraint type t and the value r.
1192
   * If there is such a constraint in the database already, it is returned.
1193
   * If there is no such constraint, this constraint is added to the database.
1194
   *
1195
   */
1196
  ConstraintP getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r);
1197
1198
  /**
1199
   * Returns a constraint of the given type for the value and variable
1200
   * for the given ValueCollection, vc.
1201
   * This is made if there is no such constraint.
1202
   */
1203
  ConstraintP ensureConstraint(ValueCollection& vc, ConstraintType t);
1204
1205
1206
  void deleteConstraintAndNegation(ConstraintP c);
1207
1208
  /** Given constraints `a` and `b` such that `a OR b` by unate reasoning,
1209
   *  adds a TrustNode to `out` which proves `a OR b` as a lemma.
1210
   *
1211
   *  Example: `x <= 5` OR `5 <= x`.
1212
   */
1213
  void proveOr(std::vector<TrustNode>& out,
1214
               ConstraintP a,
1215
               ConstraintP b,
1216
               bool negateSecond) const;
1217
  /** Given constraints `a` and `b` such that `a` implies `b` by unate
1218
   * reasoning, adds a TrustNode to `out` which proves `-a OR b` as a lemma.
1219
   *
1220
   *  Example: `x >= 5` -> `x >= 4`.
1221
   */
1222
  void implies(std::vector<TrustNode>& out, ConstraintP a, ConstraintP b) const;
1223
  /** Given constraints `a` and `b` such that `not(a AND b)` by unate reasoning,
1224
   *  adds a TrustNode to `out` which proves `-a OR -b` as a lemma.
1225
   *
1226
   *  Example: `x >= 4` -> `x <= 3`.
1227
   */
1228
  void mutuallyExclusive(std::vector<TrustNode>& out,
1229
                         ConstraintP a,
1230
                         ConstraintP b) const;
1231
1232
  /**
1233
   * Outputs a minimal set of unate implications onto the vector for the variable.
1234
   * This outputs lemmas of the general forms
1235
   *     (= p c) implies (<= p d) for c < d, or
1236
   *     (= p c) implies (not (= p d)) for c != d.
1237
   */
1238
  void outputUnateEqualityLemmas(std::vector<TrustNode>& lemmas) const;
1239
  void outputUnateEqualityLemmas(std::vector<TrustNode>& lemmas,
1240
                                 ArithVar v) const;
1241
1242
  /**
1243
   * Outputs a minimal set of unate implications onto the vector for the variable.
1244
   *
1245
   * If ineqs is true, this outputs lemmas of the general form
1246
   *     (<= p c) implies (<= p d) for c < d.
1247
   */
1248
  void outputUnateInequalityLemmas(std::vector<TrustNode>& lemmas) const;
1249
  void outputUnateInequalityLemmas(std::vector<TrustNode>& lemmas,
1250
                                   ArithVar v) const;
1251
1252
  void unatePropLowerBound(ConstraintP curr, ConstraintP prev);
1253
  void unatePropUpperBound(ConstraintP curr, ConstraintP prev);
1254
  void unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB);
1255
1256
  /** AntecendentID must be in range. */
1257
  ConstraintCP getAntecedent(AntecedentId p) const;
1258
1259
7115044
  bool isProofEnabled() const { return d_pnm != nullptr; }
1260
1261
 private:
1262
  /** returns true if cons is now in conflict. */
1263
  bool handleUnateProp(ConstraintP ant, ConstraintP cons);
1264
1265
  DenseSet d_reclaimable;
1266
1267
  class Statistics {
1268
  public:
1269
    IntStat d_unatePropagateCalls;
1270
    IntStat d_unatePropagateImplications;
1271
1272
    Statistics();
1273
    ~Statistics();
1274
  } d_statistics;
1275
1276
}; /* ConstraintDatabase */
1277
1278
1279
}/* CVC4::theory::arith namespace */
1280
}/* CVC4::theory namespace */
1281
}/* CVC4 namespace */
1282
1283
#endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */