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