diff options
Diffstat (limited to 'src/theory/arith/constraint.h')
| -rw-r--r-- | src/theory/arith/constraint.h | 32 |
1 files changed, 28 insertions, 4 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index fe10ecc4a..5b49dd54d 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -828,14 +828,38 @@ public: */ Constraint getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r); + /** + * Outputs a minimal set of unate implications onto the vector for the variable. + * This outputs lemmas of the general forms + * (= p c) implies (<= p d) for c < d, or + * (= p c) implies (not (= p d)) for c != d. + */ + void outputUnateEqualityLemmas(std::vector<Node>& lemmas) const; + void outputUnateEqualityLemmas(std::vector<Node>& lemmas, ArithVar v) const; /** - * Outputs a minimal set of unate implications on the output channel - * for all variables. + * Outputs a minimal set of unate implications onto the vector for the variable. + * + * If ineqs is true, this outputs lemmas of the general form + * (<= p c) implies (<= p d) for c < d. */ - void outputAllUnateLemmas(std::vector<Node>& lemmas) const; + void outputUnateInequalityLemmas(std::vector<Node>& lemmas) const; + void outputUnateInequalityLemmas(std::vector<Node>& lemmas, ArithVar v) const; + + + void unatePropLowerBound(Constraint curr, Constraint prev); + void unatePropUpperBound(Constraint curr, Constraint prev); + void unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB); + +private: + class Statistics { + public: + IntStat d_unatePropagateCalls; + IntStat d_unatePropagateImplications; - void outputAllUnateLemmas(std::vector<Node>& lemmas, ArithVar v) const; + Statistics(); + ~Statistics(); + } d_statistics; }; /* ConstraintDatabase */ |