Sharing work

3 files changed, 15 insertions, 0 deletions

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index d88a7ae92..822514f38 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -63,6 +63,10 @@ public:
 
   static RewriteResponse preRewrite(TNode n);
   static RewriteResponse postRewrite(TNode n);
+  static Node rewriteEquality(TNode equality) {
+    // Arithmetic owns the domain, so this is totally ok
+    return Rewriter::rewrite(equality);
+  }
 
   static void init() { }
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c69960d37..066eb85b5 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1035,3 +1035,12 @@ void TheoryArith::presolve(){
   learner.clear();
   check(FULL_EFFORT);
 }
+
+EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
+  if (getValue(a) == getValue(b)) {
+    return EQUALITY_TRUE_IN_MODEL;
+  } else {
+    return EQUALITY_FALSE_IN_MODEL;
+  }
+
+}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 4731bea30..1ba9a50e0 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -189,6 +189,8 @@ public:
 
   std::string identify() const { return std::string("TheoryArith"); }
 
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+
 private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;