diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-06 20:00:03 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-06 20:00:03 -0800 |
| commit | 136a30c2b8cb06d607c5544a3911f120216b3663 (patch) | |
| tree | ddd15ffc52632c6d7f2b21882b0664e165511995 /src/theory/arith/constraint.h | |
| parent | 14fc21fc1101587810e64b0ed78ce03622e2939d (diff) | |
Arith Constraint Proof Loggin (#2732)
* Arith Constraint Proof Logging
Also a tiny documentation update.
* Debug.isOn check around iterated output
* reference iteratees
Diffstat (limited to 'src/theory/arith/constraint.h')
| -rw-r--r-- | src/theory/arith/constraint.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 5eef9663e..d411f2d34 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -928,7 +928,11 @@ private: /** Return true if every element in b has a proof. */ static bool allHaveProof(const ConstraintCPVec& b); - /** Precondition: hasFarkasProof() */ + /** Precondition: hasFarkasProof() + * Computes the combination implied by the farkas coefficients. Sees if it is + * a contradiction. + */ + bool wellFormedFarkasProof() const; }; /* class ConstraintValue */ |