1 files changed, 1 insertions, 63 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index db643d96b..7516ea529 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -13,76 +13,14 @@
  **/
 
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
+
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
 
-QuantifiersModule::QuantifiersModule(
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    quantifiers::QuantifiersRegistry& qr,
-    QuantifiersEngine* qe)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
-{
-}
-
-QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
-{
-  return QEFFORT_NONE;
-}
-
-eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
-{
-  return d_qstate.getEqualityEngine();
-}
-
-bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
-{
-  return d_qstate.areEqual(n1, n2);
-}
-
-bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
-{
-  return d_qstate.areDisequal(n1, n2);
-}
-
-TNode QuantifiersModule::getRepresentative(TNode n) const
-{
-  return d_qstate.getRepresentative(n);
-}
-
-QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
-{
-  return d_quantEngine;
-}
-
-quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
-{
-  return d_quantEngine->getTermDatabase();
-}
-
-quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
-{
-  return d_quantEngine->getTermUtil();
-}
-
-quantifiers::QuantifiersState& QuantifiersModule::getState()
-{
-  return d_qstate;
-}
-
-quantifiers::QuantifiersInferenceManager&
-QuantifiersModule::getInferenceManager()
-{
-  return d_qim;
-}
-
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
   initialize( n, computeEq );
 }