1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9a987c9d7..8bc67616f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -83,6 +83,9 @@ namespace theory {
   namespace eq {
     class EqualityEngine;
   }
+
+  class EntailmentCheckParameters;
+  class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 class DecisionEngine;
 class RemoveITE;
@@ -755,6 +758,12 @@ public:
    */
   Node getModelValue(TNode var);
 
+  /**
+   * Forwards an entailmentCheck according to the given theoryOfMode mode.
+   * See theory.h for documentation on entailmentCheck().
+   */
+  std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
+
 private:
 
   /** Default visitor for pre-registration */