1 files changed, 14 insertions, 1 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 98aa43e71..f78893324 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -162,7 +162,7 @@ inline int deltaCoeff(Kind k){
  * - (NOT (GT left right))    -> LEQ
  * If none of these match, it returns UNDEFINED_KIND.
  */
- inline Kind oldSimplifiedKind(TNode literal){
+inline Kind oldSimplifiedKind(TNode literal){
   switch(literal.getKind()){
   case kind::LT:
   case kind::GT:
@@ -195,6 +195,19 @@ inline int deltaCoeff(Kind k){
   }
 }
 
+inline Kind negateKind(Kind k){
+  switch(k){
+  case kind::LT:       return kind::GEQ;
+  case kind::GT:       return kind::LEQ;
+  case kind::LEQ:      return kind::GT;
+  case kind::GEQ:      return kind::LT;
+  case kind::EQUAL:    return kind::DISTINCT;
+  case kind::DISTINCT: return kind::EQUAL;
+  default:
+    return kind::UNDEFINED_KIND;
+  }
+}
+
 inline Node negateConjunctionAsClause(TNode conjunction){
   Assert(conjunction.getKind() == kind::AND);
   NodeBuilder<> orBuilder(kind::OR);