Added Theory::presolve().

1 files changed, 7 insertions, 1 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7958d977e..8ee5c91d7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -305,10 +305,16 @@ public:
     } catch(const theory::Interrupted&) {
       Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
     }
-    // Return wheather we have a conflict
+    // Return whether we have a conflict
     return d_theoryOut.d_conflictNode.get().isNull();
   }
 
+  /**
+   * Calls presolve() on all active theories and returns true
+   * if one of the theories discovers a conflict.
+   */
+  bool presolve();
+
   inline const std::vector<TNode>& getPropagatedLiterals() const {
     return d_theoryOut.d_propagatedLiterals;
   }