Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Alex Ozdemir, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Defines Constraint and ConstraintDatabase which is the internal
14 : : * representation of variables in arithmetic
15 : : *
16 : : * This file defines Constraint and ConstraintDatabase.
17 : : * A Constraint is the internal representation of literals in TheoryArithmetic.
18 : : * Constraints are fundamentally a triple:
19 : : * - ArithVar associated with the constraint,
20 : : * - a DeltaRational value,
21 : : * - and a ConstraintType.
22 : : *
23 : : * Literals:
24 : : * The constraint may also keep track of a node corresponding to the
25 : : * Constraint.
26 : : * This can be accessed by getLiteral() in O(1) if it has been set.
27 : : * This node must be in normal form and may be used for communication with
28 : : * the TheoryEngine.
29 : : *
30 : : * In addition, Constraints keep track of the following:
31 : : * - A Constraint that is the negation of the Constraint.
32 : : * - An iterator into a set of Constraints for the ArithVar sorted by
33 : : * DeltaRational value.
34 : : * - A context dependent internal proof of the node that can be used for
35 : : * explanations.
36 : : * - Whether an equality/disequality has been split in the user context via a
37 : : * lemma.
38 : : * - Whether a constraint, be be used in explanations sent to the context
39 : : *
40 : : * Looking up constraints:
41 : : * - All of the Constraints with associated nodes in the ConstraintDatabase
42 : : * can be accessed via a single hashtable lookup until the Constraint is
43 : : * removed.
44 : : * - Nodes that have not been associated to a constraints can be
45 : : * inserted/associated to existing nodes in O(log n) time.
46 : : *
47 : : * Implications:
48 : : * - A Constraint can be used to find unate implications.
49 : : * - A unate implication is an implication based purely on the ArithVar
50 : : * matching and the DeltaRational value.
51 : : * (implies (<= x c) (<= x d)) given c <= d
52 : : * - This is done using the iterator into the sorted set of constraints.
53 : : * - Given a tight constraint and previous tightest constraint, this will
54 : : * efficiently propagate internally.
55 : : *
56 : : * Additing and Removing Constraints
57 : : * - Adding Constraints takes O(log n) time where n is the number of
58 : : * constraints associated with the ArithVar.
59 : : * - Removing Constraints takes O(1) time.
60 : : *
61 : : * Internals:
62 : : * - Constraints are pointers to ConstraintValues.
63 : : * - Undefined Constraints are NullConstraint.
64 : : *
65 : : * Assumption vs. Assertion:
66 : : * - An assertion is anything on the theory d_fact queue.
67 : : * This includes any thing propagated and returned to the fact queue.
68 : : * These can be used in external conflicts and propagations of earlier
69 : : * proofs.
70 : : * - An assumption is anything on the theory d_fact queue that has no further
71 : : * explanation i.e. this theory did not propagate it.
72 : : * - To set something an assumption, first set it as being as assertion.
73 : : * - Internal assumptions have no explanations and must be regressed out of the
74 : : * proof.
75 : : */
76 : :
77 : : #include "cvc5_private.h"
78 : :
79 : : #ifndef CVC5__THEORY__ARITH__CONSTRAINT_H
80 : : #define CVC5__THEORY__ARITH__CONSTRAINT_H
81 : :
82 : : #include <unordered_map>
83 : : #include <vector>
84 : :
85 : : #include "base/configuration_private.h"
86 : : #include "context/cdlist.h"
87 : : #include "context/cdqueue.h"
88 : : #include "expr/node.h"
89 : : #include "proof/trust_node.h"
90 : : #include "smt/env_obj.h"
91 : : #include "theory/arith/linear/arithvar.h"
92 : : #include "theory/arith/linear/callbacks.h"
93 : : #include "theory/arith/linear/constraint_forward.h"
94 : : #include "theory/arith/delta_rational.h"
95 : : #include "util/statistics_stats.h"
96 : :
97 : : namespace cvc5::context {
98 : : class Context;
99 : : }
100 : : namespace cvc5::internal {
101 : :
102 : : class ProofNodeManager;
103 : : class EagerProofGenerator;
104 : :
105 : : namespace theory {
106 : :
107 : : namespace arith::linear {
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 : : typedef context::CDList<ConstraintCP> CDConstraintList;
156 : :
157 : : typedef std::unordered_map<Node, ConstraintP> NodetoConstraintMap;
158 : :
159 : : typedef size_t ConstraintRuleID;
160 : : static constexpr ConstraintRuleID ConstraintRuleIdSentinel =
161 : : std::numeric_limits<ConstraintRuleID>::max();
162 : :
163 : : typedef size_t AntecedentId;
164 : : static constexpr AntecedentId AntecedentIdSentinel =
165 : : std::numeric_limits<AntecedentId>::max();
166 : :
167 : : typedef size_t AssertionOrder;
168 : : static constexpr AssertionOrder AssertionOrderSentinel =
169 : : std::numeric_limits<AssertionOrder>::max();
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 : : 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 : 358718 : PerVariableDatabase(ArithVar v) : d_var(v), d_constraints() {}
252 : :
253 : 0 : bool empty() const {
254 : 0 : return d_constraints.empty();
255 : : }
256 : :
257 : 0 : static bool IsEmpty(const PerVariableDatabase& p){
258 : 0 : 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 : :
314 : : ConstraintRule();
315 : : ConstraintRule(ConstraintP con, ArithProofType pt);
316 : : ConstraintRule(ConstraintP con,
317 : : ArithProofType pt,
318 : : AntecedentId antecedentEnd);
319 : : ConstraintRule(ConstraintP con,
320 : : ArithProofType pt,
321 : : AntecedentId antecedentEnd,
322 : : RationalVectorCP coeffs);
323 : :
324 : : void print(std::ostream& out, bool produceProofs) const;
325 : : }; /* class ConstraintRule */
326 : :
327 : : class Constraint {
328 : :
329 : : friend class ConstraintDatabase;
330 : :
331 : : public:
332 : : /**
333 : : * This begins construction of a minimal constraint.
334 : : *
335 : : * This should only be called by ConstraintDatabase.
336 : : *
337 : : * Because of circular dependencies a Constraint is not fully valid until
338 : : * initialize has been called on it.
339 : : */
340 : : Constraint(ArithVar x,
341 : : ConstraintType t,
342 : : const DeltaRational& v,
343 : : bool produceProofs);
344 : :
345 : : /**
346 : : * Destructor for a constraint.
347 : : * This should only be called if safeToGarbageCollect() is true.
348 : : */
349 : : ~Constraint();
350 : :
351 : : static ConstraintType constraintTypeOfComparison(const Comparison& cmp);
352 : :
353 : 42813010 : inline ConstraintType getType() const {
354 : 42813010 : return d_type;
355 : : }
356 : :
357 : 54627774 : inline ArithVar getVariable() const {
358 : 54627774 : return d_variable;
359 : : }
360 : :
361 : 90412024 : const DeltaRational& getValue() const {
362 : 90412024 : return d_value;
363 : : }
364 : :
365 : 9116730 : inline ConstraintP getNegation() const {
366 : 9116730 : return d_negation;
367 : : }
368 : :
369 : 14506730 : bool isEquality() const{
370 : 14506730 : return d_type == Equality;
371 : : }
372 : 1432944 : bool isDisequality() const{
373 : 1432944 : return d_type == Disequality;
374 : : }
375 : 10702566 : bool isLowerBound() const{
376 : 10702566 : return d_type == LowerBound;
377 : : }
378 : 10147779 : bool isUpperBound() const{
379 : 10147779 : return d_type == UpperBound;
380 : : }
381 : 2479778 : bool isStrictUpperBound() const{
382 [ - + ][ - + ]: 2479778 : Assert(isUpperBound());
[ - - ]
383 : 2479778 : return getValue().infinitesimalSgn() < 0;
384 : : }
385 : :
386 : 2606616 : bool isStrictLowerBound() const{
387 [ - + ][ - + ]: 2606616 : Assert(isLowerBound());
[ - - ]
388 : 2606616 : return getValue().infinitesimalSgn() > 0;
389 : : }
390 : :
391 : 3304852 : bool isSplit() const {
392 : 3304852 : return d_split;
393 : : }
394 : :
395 : : /**
396 : : * Splits the node in the user context.
397 : : * Returns a lemma that is assumed to be true for the rest of the user context.
398 : : * Constraint must be an equality or disequality.
399 : : */
400 : : TrustNode split();
401 : :
402 : 16445376 : bool canBePropagated() const {
403 : 16445376 : return d_canBePropagated;
404 : : }
405 : : void setCanBePropagated();
406 : :
407 : : /**
408 : : * Light wrapper for calling setCanBePropagated(),
409 : : * on this and this->d_negation.
410 : : */
411 : 891191 : void setPreregistered(){
412 : 891191 : setCanBePropagated();
413 : 891191 : d_negation->setCanBePropagated();
414 : 891191 : }
415 : :
416 : 104989951 : bool assertedToTheTheory() const {
417 [ - + ][ - + ]: 104989951 : Assert((d_assertionOrder < AssertionOrderSentinel) != d_witness.isNull());
[ - - ]
418 : 104989951 : return d_assertionOrder < AssertionOrderSentinel;
419 : : }
420 : 10987052 : TNode getWitness() const {
421 [ - + ][ - + ]: 10987052 : Assert(assertedToTheTheory());
[ - - ]
422 : 10987052 : return d_witness;
423 : : }
424 : :
425 : 9026415 : bool assertedBefore(AssertionOrder time) const {
426 : 9026415 : return d_assertionOrder < time;
427 : : }
428 : :
429 : : /**
430 : : * Sets the witness literal for a node being on the assertion stack.
431 : : *
432 : : * If the negation of the node is true, inConflict must be true.
433 : : * If the negation of the node is false, inConflict must be false.
434 : : * Hence, negationHasProof() == inConflict.
435 : : *
436 : : * This replaces:
437 : : * void setAssertedToTheTheory(TNode witness);
438 : : * void setAssertedToTheTheoryWithNegationTrue(TNode witness);
439 : : */
440 : : void setAssertedToTheTheory(TNode witness, bool inConflict);
441 : :
442 : 27408358 : bool hasLiteral() const {
443 : 27408358 : return !d_literal.isNull();
444 : : }
445 : :
446 : : void setLiteral(Node n);
447 : :
448 : 3213119 : Node getLiteral() const {
449 [ - + ][ - + ]: 3213119 : Assert(hasLiteral());
[ - - ]
450 : 3213119 : return d_literal;
451 : : }
452 : :
453 : : /** Gets a literal in the normal form suitable for proofs.
454 : : * That is, (sum of non-const monomials) >< const.
455 : : *
456 : : * This is a sister method to `getLiteral`, which returns a normal form
457 : : * literal, suitable for external solving use.
458 : : */
459 : : Node getProofLiteral() const;
460 : :
461 : : /**
462 : : * Set the node as having a proof and being an assumption.
463 : : * The node must be assertedToTheTheory().
464 : : *
465 : : * Precondition: negationHasProof() == inConflict.
466 : : *
467 : : * Replaces:
468 : : * selfExplaining().
469 : : * selfExplainingWithNegationTrue().
470 : : */
471 : : void setAssumption(bool inConflict);
472 : :
473 : : /** Returns true if the node is an assumption.*/
474 : : bool isAssumption() const;
475 : :
476 : : /** Whether we produce proofs */
477 : 20567263 : bool isProofProducing() const { return d_produceProofs; }
478 : :
479 : : /** Set the constraint to have an EqualityEngine proof. */
480 : : void setEqualityEngineProof();
481 : : bool hasEqualityEngineProof() const;
482 : :
483 : : /** Returns true if the node has a Farkas' proof. */
484 : : bool hasFarkasProof() const;
485 : :
486 : : /**
487 : : * @brief Returns whether this constraint is provable using a Farkas
488 : : * proof applied to (possibly tightened) input assertions.
489 : : *
490 : : * An example of a constraint that has a simple Farkas proof:
491 : : * x <= 0 proven from x + y <= 0 and x - y <= 0.
492 : : *
493 : : * An example of another constraint that has a simple Farkas proof:
494 : : * x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y
495 : : * (integer bound-tightening is applied first!).
496 : : *
497 : : * An example of a constraint that might be proven **without** a simple
498 : : * Farkas proof:
499 : : * x < 0 proven from not(x == 0) and not(x > 0).
500 : : *
501 : : * This could be proven internally by the arithmetic theory using
502 : : * `TrichotomyAP` as the proof type.
503 : : *
504 : : */
505 : : bool hasSimpleFarkasProof() const;
506 : : /**
507 : : * Returns whether this constraint is an assumption or a tightened
508 : : * assumption.
509 : : */
510 : : bool isPossiblyTightenedAssumption() const;
511 : :
512 : : /** Returns true if the node has a int bound tightening proof. */
513 : : bool hasIntTightenProof() const;
514 : :
515 : : /** Returns true if the node has a int hole proof. */
516 : : bool hasIntHoleProof() const;
517 : :
518 : : /** Returns true if the node has a trichotomy proof. */
519 : : bool hasTrichotomyProof() const;
520 : :
521 : : void printProofTree(std::ostream & out, size_t depth = 0) const;
522 : :
523 : : /**
524 : : * A sets the constraint to be an internal assumption.
525 : : *
526 : : * This does not need to have a witness or an associated literal.
527 : : * This is always itself in the explanation fringe for both conflicts
528 : : * and propagation.
529 : : * This cannot be converted back into a Node conflict or explanation.
530 : : *
531 : : * This cannot have a proof or be asserted to the theory!
532 : : *
533 : : */
534 : : void setInternalAssumption(bool inConflict);
535 : : bool isInternalAssumption() const;
536 : :
537 : : /**
538 : : * Returns a explanation of the constraint that is appropriate for conflicts.
539 : : *
540 : : * This is not appropriate for propagation!
541 : : *
542 : : * This is the minimum fringe of the implication tree s.t.
543 : : * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
544 : : */
545 : : TrustNode externalExplainByAssertions() const;
546 : :
547 : : /**
548 : : * Writes an explanation of a constraint into the node builder.
549 : : * Pushes back an explanation that is acceptable to send to the sat solver.
550 : : * nb is assumed to be an AND.
551 : : *
552 : : * This is the minimum fringe of the implication tree s.t.
553 : : * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
554 : : *
555 : : * This is not appropriate for propagation!
556 : : * Use explainForPropagation() instead.
557 : : */
558 : 5883232 : std::shared_ptr<ProofNode> externalExplainByAssertions(NodeBuilder& nb) const
559 : : {
560 : 5883232 : return externalExplain(nb, AssertionOrderSentinel);
561 : : }
562 : :
563 : : /* Equivalent to calling externalExplainByAssertions on all constraints in b */
564 : : static Node externalExplainByAssertions(NodeManager* nm,
565 : : const ConstraintCPVec& b);
566 : : static Node externalExplainByAssertions(NodeManager* nm,
567 : : ConstraintCP a,
568 : : ConstraintCP b);
569 : : static Node externalExplainByAssertions(NodeManager* nm,
570 : : ConstraintCP a,
571 : : ConstraintCP b,
572 : : ConstraintCP c);
573 : :
574 : : /**
575 : : * This is the minimum fringe of the implication tree s.t. every constraint is
576 : : * - assertedToTheTheory(),
577 : : * - isInternalDecision() or
578 : : * - hasEqualityEngineProof().
579 : : */
580 : : static void assertionFringe(ConstraintCPVec& v);
581 : : static void assertionFringe(ConstraintCPVec& out, const ConstraintCPVec& in);
582 : :
583 : : /** The fringe of a farkas' proof. */
584 : 0 : bool onFringe() const {
585 [ - - ][ - - ]: 0 : return assertedToTheTheory() || isInternalAssumption() || hasEqualityEngineProof();
[ - - ]
586 : : }
587 : :
588 : : /**
589 : : * Returns an explanation of a propagation by the ConstraintDatabase.
590 : : * The constraint must have a proof.
591 : : * The constraint cannot be an assumption.
592 : : *
593 : : * This is the minimum fringe of the implication tree (excluding the
594 : : * constraint itself) s.t. every constraint is assertedToTheTheory() or
595 : : * hasEqualityEngineProof().
596 : : *
597 : : * All return conjuncts were asserted before this constraint.
598 : : *
599 : : * Requires the given node to rewrite to the canonical literal for this
600 : : * constraint.
601 : : *
602 : : * @params n the literal to prove
603 : : * n must rewrite to the constraint's canonical literal
604 : : *
605 : : * @returns a trust node of the form:
606 : : * (=> explanation n)
607 : : */
608 : : TrustNode externalExplainForPropagation(TNode n) const;
609 : :
610 : : /**
611 : : * Explain the constraint and its negation in terms of assertions.
612 : : * The constraint must be in conflict.
613 : : */
614 : : TrustNode externalExplainConflict() const;
615 : :
616 : : /** The constraint is known to be true. */
617 : 289242130 : inline bool hasProof() const {
618 : 289242130 : return d_crid != ConstraintRuleIdSentinel;
619 : : }
620 : :
621 : : /** The negation of the constraint is known to hold. */
622 : 96172256 : inline bool negationHasProof() const {
623 : 96172256 : return d_negation->hasProof();
624 : : }
625 : :
626 : : /** Neither the contraint has a proof nor the negation has a proof.*/
627 : 372704 : bool truthIsUnknown() const {
628 [ + - ][ + - ]: 372704 : return !hasProof() && !negationHasProof();
629 : : }
630 : :
631 : : /** This is a synonym for hasProof(). */
632 : 28560989 : inline bool isTrue() const {
633 : 28560989 : return hasProof();
634 : : }
635 : :
636 : : /** Both the constraint and its negation are true. */
637 : 19187702 : inline bool inConflict() const {
638 [ + - ][ + + ]: 19187702 : return hasProof() && negationHasProof();
639 : : }
640 : :
641 : : /**
642 : : * Returns the constraint that corresponds to taking
643 : : * x r ceiling(getValue()) where r is the node's getType().
644 : : * Esstentially this is an up branch.
645 : : */
646 : : ConstraintP getCeiling();
647 : :
648 : : /**
649 : : * Returns the constraint that corresponds to taking
650 : : * x r floor(getValue()) where r is the node's getType().
651 : : * Esstentially this is a down branch.
652 : : */
653 : : ConstraintP getFloor();
654 : :
655 : : static ConstraintP makeNegation(ArithVar v,
656 : : ConstraintType t,
657 : : const DeltaRational& r,
658 : : bool produceProofs);
659 : :
660 : : const ValueCollection& getValueCollection() const;
661 : :
662 : :
663 : : ConstraintP getStrictlyWeakerUpperBound(bool hasLiteral, bool mustBeAsserted) const;
664 : : ConstraintP getStrictlyWeakerLowerBound(bool hasLiteral, bool mustBeAsserted) const;
665 : :
666 : : /**
667 : : * Marks a the constraint c as being entailed by a.
668 : : * The Farkas proof 1*(a) + -1 (c) |= 0<0
669 : : *
670 : : * After calling impliedByUnate(), the caller should either raise a conflict
671 : : * or try call tryToPropagate().
672 : : */
673 : : void impliedByUnate(NodeManager* nm, ConstraintCP a, bool inConflict);
674 : :
675 : : /**
676 : : * Marks a the constraint c as being entailed by a.
677 : : * The reason has to do with integer bound tightening.
678 : : *
679 : : * After calling impliedByIntTighten(), the caller should either raise a conflict
680 : : * or try call tryToPropagate().
681 : : */
682 : : void impliedByIntTighten(ConstraintCP a, bool inConflict);
683 : :
684 : : /**
685 : : * Marks a the constraint c as being entailed by a.
686 : : * The reason has to do with integer reasoning.
687 : : *
688 : : * After calling impliedByIntHole(), the caller should either raise a conflict
689 : : * or try call tryToPropagate().
690 : : */
691 : : void impliedByIntHole(ConstraintCP a, bool inConflict);
692 : :
693 : : /**
694 : : * Marks a the constraint c as being entailed by a.
695 : : * The reason has to do with integer reasoning.
696 : : *
697 : : * After calling impliedByIntHole(), the caller should either raise a conflict
698 : : * or try call tryToPropagate().
699 : : */
700 : : void impliedByIntHole(const ConstraintCPVec& b, bool inConflict);
701 : :
702 : : /**
703 : : * This is a lemma of the form:
704 : : * x < d or x = d or x > d
705 : : * The current constraint c is one of the above constraints and {a,b}
706 : : * are the negation of the other two constraints.
707 : : *
708 : : * Preconditions:
709 : : * - negationHasProof() == inConflict.
710 : : *
711 : : * After calling impliedByTrichotomy(), the caller should either raise a conflict
712 : : * or try call tryToPropagate().
713 : : */
714 : : void impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool inConflict);
715 : :
716 : : /**
717 : : * Marks the node as having a Farkas proof.
718 : : *
719 : : * Preconditions:
720 : : * - coeffs == NULL if proofs are off.
721 : : * - See the comments for ConstraintRule for the form of coeffs when
722 : : * proofs are on.
723 : : * - negationHasProof() == inConflict.
724 : : *
725 : : * After calling impliedByFarkas(), the caller should either raise a conflict
726 : : * or try call tryToPropagate().
727 : : */
728 : : void impliedByFarkas(NodeManager* nm,
729 : : const ConstraintCPVec& b,
730 : : RationalVectorCP coeffs,
731 : : bool inConflict);
732 : :
733 : : /**
734 : : * Generates an implication node, B => getLiteral(),
735 : : * where B is the result of externalExplainByAssertions(b).
736 : : * Does not guarantee b is the explanation of the constraint.
737 : : */
738 : : Node externalImplication(NodeManager* nm, const ConstraintCPVec& b) const;
739 : :
740 : : /**
741 : : * Returns true if the variable is assigned the value dr,
742 : : * the constraint would be satisfied.
743 : : */
744 : : bool satisfiedBy(const DeltaRational& dr) const;
745 : :
746 : : /**
747 : : * The node must have a proof already and be eligible for propagation!
748 : : * You probably want to call tryToPropagate() instead.
749 : : *
750 : : * Preconditions:
751 : : * - hasProof()
752 : : * - canBePropagated()
753 : : * - !assertedToTheTheory()
754 : : */
755 : : void propagate();
756 : :
757 : : /**
758 : : * If the constraint
759 : : * canBePropagated() and
760 : : * !assertedToTheTheory(),
761 : : * the constraint is added to the database's propagation queue.
762 : : *
763 : : * Precondition:
764 : : * - hasProof()
765 : : */
766 : : void tryToPropagate();
767 : :
768 : : /**
769 : : * Returns a reference to the containing database.
770 : : * Precondition: the constraint must be initialized.
771 : : */
772 : : const ConstraintDatabase& getDatabase() const;
773 : :
774 : : /** Returns the constraint rule at the position. */
775 : : const ConstraintRule& getConstraintRule() const;
776 : :
777 : : private:
778 : : /** Returns true if the constraint has been initialized. */
779 : : bool initialized() const;
780 : :
781 : : /**
782 : : * This initializes the fields that cannot be set in the constructor due to
783 : : * circular dependencies.
784 : : */
785 : : void initialize(ConstraintDatabase* db,
786 : : SortedConstraintMapIterator v,
787 : : ConstraintP negation);
788 : :
789 : : class ConstraintRuleCleanup
790 : : {
791 : : public:
792 : 16748079 : inline void operator()(ConstraintRule& crp)
793 : : {
794 : 16748079 : ConstraintP constraint = crp.d_constraint;
795 [ - + ][ - + ]: 16748079 : Assert(constraint->d_crid != ConstraintRuleIdSentinel);
[ - - ]
796 : 16748079 : constraint->d_crid = ConstraintRuleIdSentinel;
797 [ + + ]: 16748079 : if (constraint->isProofProducing())
798 : : {
799 [ + + ]: 11218666 : if (crp.d_farkasCoefficients != RationalVectorCPSentinel)
800 : : {
801 [ + - ]: 2649480 : delete crp.d_farkasCoefficients;
802 : : }
803 : : }
804 : 16748079 : }
805 : : };
806 : :
807 : : class CanBePropagatedCleanup
808 : : {
809 : : public:
810 : 1781822 : inline void operator()(ConstraintP& constraint)
811 : : {
812 [ - + ][ - + ]: 1781822 : Assert(constraint->d_canBePropagated);
[ - - ]
813 : 1781822 : constraint->d_canBePropagated = false;
814 : 1781822 : }
815 : : };
816 : :
817 : : class AssertionOrderCleanup
818 : : {
819 : : public:
820 : 10947854 : inline void operator()(ConstraintP& constraint)
821 : : {
822 [ - + ][ - + ]: 10947854 : Assert(constraint->assertedToTheTheory());
[ - - ]
823 : 10947854 : constraint->d_assertionOrder = AssertionOrderSentinel;
824 : 10947854 : constraint->d_witness = TNode::null();
825 [ - + ][ - + ]: 10947854 : Assert(!constraint->assertedToTheTheory());
[ - - ]
826 : 10947854 : }
827 : : };
828 : :
829 : : class SplitCleanup
830 : : {
831 : : public:
832 : 72154 : inline void operator()(ConstraintP& constraint)
833 : : {
834 [ - + ][ - + ]: 72154 : Assert(constraint->d_split);
[ - - ]
835 : 72154 : constraint->d_split = false;
836 : 72154 : }
837 : : };
838 : :
839 : : /**
840 : : * Returns true if the node is safe to garbage collect.
841 : : * Both it and its negation must have no context dependent data set.
842 : : */
843 : : bool safeToGarbageCollect() const;
844 : :
845 : : /**
846 : : * Returns true if the constraint has no context dependent data set.
847 : : */
848 : : bool contextDependentDataIsSet() const;
849 : :
850 : : /**
851 : : * Returns true if the node correctly corresponds to the constraint that is
852 : : * being set.
853 : : */
854 : : bool sanityChecking(Node n) const;
855 : :
856 : : /** Returns a reference to the map for d_variable. */
857 : : SortedConstraintMap& constraintSet() const;
858 : :
859 : : /** Returns coefficients for the proofs for farkas cancellation. */
860 : : static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);
861 : :
862 : : Node externalExplain(AssertionOrder order) const;
863 : : /**
864 : : * Returns an explanation of that was assertedBefore(order).
865 : : * The constraint must have a proof.
866 : : * The constraint cannot be selfExplaining().
867 : : *
868 : : * This is the minimum fringe of the implication tree
869 : : * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
870 : : */
871 : : std::shared_ptr<ProofNode> externalExplain(NodeBuilder& nb,
872 : : AssertionOrder order) const;
873 : :
874 : : static Node externalExplain(NodeManager* nm,
875 : : const ConstraintCPVec& b,
876 : : AssertionOrder order);
877 : :
878 : 40762063 : inline ArithProofType getProofType() const {
879 : 40762063 : return getConstraintRule().d_proofType;
880 : : }
881 : :
882 : 1315683 : inline AntecedentId getEndAntecedent() const {
883 : 1315683 : return getConstraintRule().d_antecedentEnd;
884 : : }
885 : :
886 : 55723 : inline RationalVectorCP getFarkasCoefficients() const
887 : : {
888 [ + - ]: 55723 : return d_produceProofs ? getConstraintRule().d_farkasCoefficients : nullptr;
889 : : }
890 : :
891 : : /**
892 : : * The proof of the node is empty.
893 : : * The proof must be a special proof. Either
894 : : * isSelfExplaining() or
895 : : * hasEqualityEngineProof()
896 : : */
897 : : bool antecentListIsEmpty() const;
898 : :
899 : : bool antecedentListLengthIsOne() const;
900 : :
901 : : /** Return true if every element in b has a proof. */
902 : : static bool allHaveProof(const ConstraintCPVec& b);
903 : :
904 : : /** Precondition: hasFarkasProof()
905 : : * Computes the combination implied by the farkas coefficients. Sees if it is
906 : : * a contradiction.
907 : : */
908 : :
909 : : bool wellFormedFarkasProof(NodeManager* nm) const;
910 : :
911 : : /** The ArithVar associated with the constraint. */
912 : : const ArithVar d_variable;
913 : :
914 : : /** The type of the Constraint. */
915 : : const ConstraintType d_type;
916 : :
917 : : /** The DeltaRational value with the constraint. */
918 : : const DeltaRational d_value;
919 : :
920 : : /** A pointer to the associated database for the Constraint. */
921 : : ConstraintDatabase* d_database;
922 : :
923 : : /**
924 : : * The node to be communicated with the TheoryEngine.
925 : : *
926 : : * This is not context dependent, but may be set once.
927 : : *
928 : : * This must be set if the constraint canBePropagated().
929 : : * This must be set if the constraint assertedToTheTheory().
930 : : * Otherwise, this may be null().
931 : : */
932 : : Node d_literal;
933 : :
934 : : /** Pointer to the negation of the Constraint. */
935 : : ConstraintP d_negation;
936 : :
937 : : /**
938 : : * This is true if the associated node can be propagated.
939 : : *
940 : : * This should be enabled if the node has been preregistered.
941 : : *
942 : : * Sat Context Dependent.
943 : : * This is initially false.
944 : : */
945 : : bool d_canBePropagated;
946 : :
947 : : /**
948 : : * This is the order the constraint was asserted to the theory.
949 : : * If this has been set, the node can be used in conflicts.
950 : : * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the
951 : : * explanation of d.
952 : : *
953 : : * This should be set after the literal is dequeued by Theory::get().
954 : : *
955 : : * Sat Context Dependent.
956 : : * This is initially AssertionOrderSentinel.
957 : : */
958 : : AssertionOrder d_assertionOrder;
959 : :
960 : : /**
961 : : * This is guaranteed to be on the fact queue.
962 : : * For example if x + y = x + 1 is on the fact queue, then use this
963 : : */
964 : : TNode d_witness;
965 : :
966 : : /**
967 : : * The position of the constraint in the constraint rule id.
968 : : *
969 : : * Sat Context Dependent.
970 : : * This is initially
971 : : */
972 : : ConstraintRuleID d_crid;
973 : :
974 : : /**
975 : : * True if the equality has been split.
976 : : * Only meaningful if ConstraintType == Equality.
977 : : *
978 : : * User Context Dependent.
979 : : * This is initially false.
980 : : */
981 : : bool d_split;
982 : :
983 : : /**
984 : : * Position in sorted constraint set for the variable.
985 : : * Unset if d_type is Disequality.
986 : : */
987 : : SortedConstraintMapIterator d_variablePosition;
988 : :
989 : : /** Whether to produce proofs, */
990 : : bool d_produceProofs;
991 : :
992 : : }; /* class ConstraintValue */
993 : :
994 : : std::ostream& operator<<(std::ostream& o, const Constraint& c);
995 : : std::ostream& operator<<(std::ostream& o, const ConstraintP c);
996 : : std::ostream& operator<<(std::ostream& o, const ConstraintCP c);
997 : : std::ostream& operator<<(std::ostream& o, const ConstraintType t);
998 : : std::ostream& operator<<(std::ostream& o, const ValueCollection& c);
999 : : std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v);
1000 : : std::ostream& operator<<(std::ostream& o, const ArithProofType);
1001 : :
1002 : : class ConstraintDatabase : protected EnvObj
1003 : : {
1004 : : private:
1005 : : /**
1006 : : * The map from ArithVars to their unique databases.
1007 : : * When the vector changes size, we cannot allow the maps to move so this
1008 : : * is a vector of pointers.
1009 : : */
1010 : : std::vector<PerVariableDatabase*> d_varDatabases;
1011 : :
1012 : : SortedConstraintMap& getVariableSCM(ArithVar v) const;
1013 : :
1014 : : /** Maps literals to constraints.*/
1015 : : NodetoConstraintMap d_nodetoConstraintMap;
1016 : :
1017 : : /**
1018 : : * A queue of propagated constraints.
1019 : : * ConstraintCP are pointers.
1020 : : * The elements of the queue do not require destruction.
1021 : : */
1022 : : context::CDQueue<ConstraintCP> d_toPropagate;
1023 : :
1024 : : /**
1025 : : * Proofs are lists of valid constraints terminated by the first null
1026 : : * sentinel value in the proof list.
1027 : : * We abbreviate d_antecedents as ans in the comment.
1028 : : *
1029 : : * The proof at p in ans[p] of length n is
1030 : : * (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
1031 : : *
1032 : : * The proof at p corresponds to the conjunction:
1033 : : * (and x_i)
1034 : : *
1035 : : * So the proof of a Constraint c corresponds to the horn clause:
1036 : : * (implies (and x_i) c)
1037 : : * where (and x_i) is the proof at c.d_crid d_antecedentEnd.
1038 : : *
1039 : : * Constraints are pointers so this list is designed not to require any destruction.
1040 : : */
1041 : : CDConstraintList d_antecedents;
1042 : :
1043 : : typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup>
1044 : : ConstraintRuleList;
1045 : : typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup>
1046 : : CBPList;
1047 : : typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup>
1048 : : AOList;
1049 : : typedef context::CDList<ConstraintP, Constraint::SplitCleanup> SplitList;
1050 : :
1051 : : /**
1052 : : * The watch lists are collected together as they need to be garbage collected
1053 : : * carefully.
1054 : : */
1055 : : struct Watches{
1056 : :
1057 : : /**
1058 : : * Contains the exact list of constraints that have a proof.
1059 : : * Upon pop, this unsets d_crid to NoAP.
1060 : : *
1061 : : * The index in this list is the proper ordering of the proofs.
1062 : : */
1063 : : ConstraintRuleList d_constraintProofs;
1064 : :
1065 : : /**
1066 : : * Contains the exact list of constraints that can be used for propagation.
1067 : : */
1068 : : CBPList d_canBePropagatedWatches;
1069 : :
1070 : : /**
1071 : : * Contains the exact list of constraints that have been asserted to the theory.
1072 : : */
1073 : : AOList d_assertionOrderWatches;
1074 : :
1075 : :
1076 : : /**
1077 : : * Contains the exact list of atoms that have been preregistered.
1078 : : * This is a pointer as it must be destroyed before the elements of
1079 : : * d_varDatabases.
1080 : : */
1081 : : SplitList d_splitWatches;
1082 : : Watches(context::Context* satContext, context::Context* userContext);
1083 : : };
1084 : : Watches* d_watches;
1085 : :
1086 : : void pushSplitWatch(ConstraintP c);
1087 : : void pushCanBePropagatedWatch(ConstraintP c);
1088 : : void pushAssertionOrderWatch(ConstraintP c, TNode witness);
1089 : :
1090 : : /** Assumes that antecedents have already been pushed. */
1091 : : void pushConstraintRule(const ConstraintRule& crp);
1092 : :
1093 : : /** Returns true if all of the entries of the vector are empty. */
1094 : : static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec);
1095 : :
1096 : : /** Map from nodes to arithvars. */
1097 : : const ArithVariables& d_avariables;
1098 : :
1099 : 3820613 : const ArithVariables& getArithVariables() const{
1100 : 3820613 : return d_avariables;
1101 : : }
1102 : :
1103 : : ArithCongruenceManager& d_congruenceManager;
1104 : :
1105 : : /** Owned by the TheoryArithPrivate, used here. */
1106 : : EagerProofGenerator* d_pfGen;
1107 : : /** Owned by the TheoryArithPrivate, used here. */
1108 : : ProofNodeManager* d_pnm;
1109 : :
1110 : : RaiseConflict d_raiseConflict;
1111 : :
1112 : :
1113 : : const Rational d_one;
1114 : : const Rational d_negOne;
1115 : :
1116 : : friend class Constraint;
1117 : :
1118 : : public:
1119 : : ConstraintDatabase(Env& env,
1120 : : const ArithVariables& variables,
1121 : : ArithCongruenceManager& dm,
1122 : : RaiseConflict conflictCallBack,
1123 : : EagerProofGenerator* pfGen);
1124 : :
1125 : : ~ConstraintDatabase();
1126 : :
1127 : : /** Adds a literal to the database. */
1128 : : ConstraintP addLiteral(TNode lit);
1129 : :
1130 : : /**
1131 : : * If hasLiteral() is true, returns the constraint.
1132 : : * Otherwise, returns NullConstraint.
1133 : : */
1134 : : ConstraintP lookup(TNode literal) const;
1135 : :
1136 : : /**
1137 : : * Returns true if the literal has been added to the database.
1138 : : * This is a hash table lookup.
1139 : : * It does not look in the database for an equivalent corresponding constraint.
1140 : : */
1141 : : bool hasLiteral(TNode literal) const;
1142 : :
1143 : 8146178 : bool hasMorePropagations() const{
1144 : 8146178 : return !d_toPropagate.empty();
1145 : : }
1146 : :
1147 : 1349626 : ConstraintCP nextPropagation(){
1148 [ - + ][ - + ]: 1349626 : Assert(hasMorePropagations());
[ - - ]
1149 : :
1150 : 1349626 : ConstraintCP p = d_toPropagate.front();
1151 : 1349626 : d_toPropagate.pop();
1152 : :
1153 : 1349626 : return p;
1154 : : }
1155 : :
1156 : : void addVariable(ArithVar v);
1157 : : bool variableDatabaseIsSetup(ArithVar v) const;
1158 : : void removeVariable(ArithVar v);
1159 : :
1160 : : /**
1161 : : * Returns a constraint with the variable v, the constraint type t, and a value
1162 : : * dominated by r (explained below) if such a constraint exists in the database.
1163 : : * If no such constraint exists, NullConstraint is returned.
1164 : : *
1165 : : * t must be either UpperBound or LowerBound.
1166 : : * The returned value v is dominated:
1167 : : * If t is UpperBound, r <= v
1168 : : * If t is LowerBound, r >= v
1169 : : *
1170 : : * variableDatabaseIsSetup(v) must be true.
1171 : : */
1172 : : ConstraintP getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const;
1173 : :
1174 : : /** Returns the constraint, if it exists */
1175 : : ConstraintP lookupConstraint(ArithVar v, ConstraintType t, const DeltaRational& r) const;
1176 : :
1177 : : /**
1178 : : * Returns a constraint with the variable v, the constraint type t and the value r.
1179 : : * If there is such a constraint in the database already, it is returned.
1180 : : * If there is no such constraint, this constraint is added to the database.
1181 : : *
1182 : : */
1183 : : ConstraintP getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r);
1184 : :
1185 : : /**
1186 : : * Returns a constraint of the given type for the value and variable
1187 : : * for the given ValueCollection, vc.
1188 : : * This is made if there is no such constraint.
1189 : : */
1190 : : ConstraintP ensureConstraint(ValueCollection& vc, ConstraintType t);
1191 : :
1192 : :
1193 : : void deleteConstraintAndNegation(ConstraintP c);
1194 : :
1195 : : /** Given constraints `a` and `b` such that `a OR b` by unate reasoning,
1196 : : * adds a TrustNode to `out` which proves `a OR b` as a lemma.
1197 : : *
1198 : : * Example: `x <= 5` OR `5 <= x`.
1199 : : */
1200 : : void proveOr(std::vector<TrustNode>& out,
1201 : : ConstraintP a,
1202 : : ConstraintP b,
1203 : : bool negateSecond) const;
1204 : : /** Given constraints `a` and `b` such that `a` implies `b` by unate
1205 : : * reasoning, adds a TrustNode to `out` which proves `-a OR b` as a lemma.
1206 : : *
1207 : : * Example: `x >= 5` -> `x >= 4`.
1208 : : */
1209 : : void implies(std::vector<TrustNode>& out, ConstraintP a, ConstraintP b) const;
1210 : : /** Given constraints `a` and `b` such that `not(a AND b)` by unate reasoning,
1211 : : * adds a TrustNode to `out` which proves `-a OR -b` as a lemma.
1212 : : *
1213 : : * Example: `x >= 4` -> `x <= 3`.
1214 : : */
1215 : : void mutuallyExclusive(std::vector<TrustNode>& out,
1216 : : ConstraintP a,
1217 : : ConstraintP b) const;
1218 : :
1219 : : /**
1220 : : * Outputs a minimal set of unate implications onto the vector for the variable.
1221 : : * This outputs lemmas of the general forms
1222 : : * (= p c) implies (<= p d) for c < d, or
1223 : : * (= p c) implies (not (= p d)) for c != d.
1224 : : */
1225 : : void outputUnateEqualityLemmas(std::vector<TrustNode>& lemmas) const;
1226 : : void outputUnateEqualityLemmas(std::vector<TrustNode>& lemmas,
1227 : : ArithVar v) const;
1228 : :
1229 : : /**
1230 : : * Outputs a minimal set of unate implications onto the vector for the variable.
1231 : : *
1232 : : * If ineqs is true, this outputs lemmas of the general form
1233 : : * (<= p c) implies (<= p d) for c < d.
1234 : : */
1235 : : void outputUnateInequalityLemmas(std::vector<TrustNode>& lemmas) const;
1236 : : void outputUnateInequalityLemmas(std::vector<TrustNode>& lemmas,
1237 : : ArithVar v) const;
1238 : :
1239 : : void unatePropLowerBound(ConstraintP curr, ConstraintP prev);
1240 : : void unatePropUpperBound(ConstraintP curr, ConstraintP prev);
1241 : : void unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB);
1242 : :
1243 : : /** AntecendentID must be in range. */
1244 : : ConstraintCP getAntecedent(AntecedentId p) const;
1245 : :
1246 : 11788566 : bool isProofEnabled() const { return d_pnm != nullptr; }
1247 : :
1248 : : private:
1249 : : /** returns true if cons is now in conflict. */
1250 : : bool handleUnateProp(ConstraintP ant, ConstraintP cons);
1251 : :
1252 : : DenseSet d_reclaimable;
1253 : :
1254 : : class Statistics {
1255 : : public:
1256 : : IntStat d_unatePropagateCalls;
1257 : : IntStat d_unatePropagateImplications;
1258 : :
1259 : : Statistics(StatisticsRegistry& sr);
1260 : : } d_statistics;
1261 : :
1262 : : }; /* ConstraintDatabase */
1263 : :
1264 : : } // namespace arith
1265 : : } // namespace theory
1266 : : } // namespace cvc5::internal
1267 : :
1268 : : #endif /* CVC5__THEORY__ARITH__CONSTRAINT_H */
|
