Simplify entailment check interface (#4744)

The generality of this interface is unnecessary.

1 files changed, 2 insertions, 26 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 6fb739aa4..b0db8ab30 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -390,10 +390,8 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-std::pair<bool, Node> Theory::entailmentCheck(
-    TNode lit,
-    const EntailmentCheckParameters* params,
-    EntailmentCheckSideEffects* out) {
+std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
+{
   return make_pair(false, Node::null());
 }
 
@@ -436,27 +434,5 @@ void Theory::setupExtTheory() {
   d_extTheory = new ExtTheory(this);
 }
 
-
-EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
-  : d_tid(tid) {
-}
-
-EntailmentCheckParameters::~EntailmentCheckParameters(){}
-
-TheoryId EntailmentCheckParameters::getTheoryId() const {
-  return d_tid;
-}
-
-EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
-  : d_tid(tid)
-{}
-
-TheoryId EntailmentCheckSideEffects::getTheoryId() const {
-  return d_tid;
-}
-
-EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
-}
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */