summaryrefslogtreecommitdiff
path: root/src/theory/arith/constraint.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r--src/theory/arith/constraint.h10
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback