1 files changed, 2 insertions, 25 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index ac6e194eb..f24a4bb2b 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -38,8 +38,6 @@ using namespace CVC4::theory::quantifiers;
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
     Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
 {
-  d_numInstantiations = 0;
-  d_baseDecLevel = -1;
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
   out.handleUserAttribute( "fun-def", this );
@@ -71,13 +69,6 @@ void TheoryQuantifiers::preRegisterTerm(TNode n) {
     return;
   }
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if (options::cbqi() && !options::recurseCbqi()
-      && TermUtil::hasInstConstAttr(n))
-  {
-    Debug("quantifiers-prereg")
-        << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl;
-    return;
-  }
   // Preregister the quantified formula.
   // This initializes the modules used for handling n in this user context.
   getQuantifiersEngine()->preRegisterQuantifier(n);
@@ -135,7 +126,7 @@ void TheoryQuantifiers::check(Effort e) {
     Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
     switch(assertion.getKind()) {
     case kind::FORALL:
-      assertUniversal( assertion );
+      getQuantifiersEngine()->assertQuantifier(assertion, true);
       break;
     case kind::INST_CLOSURE:
       getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
@@ -150,7 +141,7 @@ void TheoryQuantifiers::check(Effort e) {
       {
         switch( assertion[0].getKind()) {
         case kind::FORALL:
-          assertExistential( assertion );
+          getQuantifiersEngine()->assertQuantifier(assertion[0], false);
           break;
         case kind::EQUAL:
           //do nothing
@@ -171,20 +162,6 @@ void TheoryQuantifiers::check(Effort e) {
   getQuantifiersEngine()->check( e );
 }
 
-void TheoryQuantifiers::assertUniversal( Node n ){
-  Assert( n.getKind()==FORALL );
-  if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
-    getQuantifiersEngine()->assertQuantifier( n, true );
-  }
-}
-
-void TheoryQuantifiers::assertExistential( Node n ){
-  Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
-  if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){
-    getQuantifiersEngine()->assertQuantifier( n[0], false );
-  }
-}
-
 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
   QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
 }