diff options
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r-- | src/theory/arith/constraint.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 795798450..0e0b35020 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -96,6 +96,13 @@ namespace CVC4 { namespace theory { namespace arith { +class Comparison; +} +} +} +namespace CVC4 { +namespace theory { +namespace arith { /** * Logs the types of different proofs. @@ -448,6 +455,7 @@ private: void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation); + class ConstraintRuleCleanup { public: inline void operator()(ConstraintRule* crp){ @@ -517,6 +525,8 @@ private: public: + static ConstraintType constraintTypeOfComparison(const Comparison& cmp); + inline ConstraintType getType() const { return d_type; } |