Merge branch 'master' into fix2002fix2002

23 files changed, 272 insertions, 138 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 097b41d93..86bc66f50 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2093,6 +2093,11 @@ void SmtEngine::setDefaults() {
     if( !options::rewriteDivk.wasSetByUser()) {
       options::rewriteDivk.set( true );
     }
+    if (options::incrementalSolving())
+    {
+      // cannot do nested quantifier elimination in incremental mode
+      options::cbqiNestedQE.set(false);
+    }
     if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
     {
       options::cbqiAll.set( false );
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 107cb9672..638715ae4 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -767,6 +767,10 @@ Node TheoryBV::ppRewrite(TNode t)
   } else if (RewriteRule<ZeroExtendEqConst>::applies(t)) {
     res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
   }
+  else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
+  {
+    res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
+  }
 
   // if(t.getKind() == kind::EQUAL &&
   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 1d2e7d9a3..c6fa42ab0 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -31,7 +31,8 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-enum RewriteRuleId {
+enum RewriteRuleId
+{
 
   /// core normalization rules
   EmptyRule,
@@ -175,6 +176,7 @@ enum RewriteRuleId {
   OrSimplify,
   XorSimplify,
   BitwiseSlicing,
+  NormalizeEqPlusNeg,
   // rules to simplify bitblasting
   BBPlusNeg,
   UltPlusOne,
@@ -321,6 +323,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case ConcatToMult: out << "ConcatToMult"; return out;
   case IsPowerOfTwo: out << "IsPowerOfTwo"; return out;
   case MultSltMult: out << "MultSltMult"; return out;
+  case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out;
   default:
     Unreachable();
   }
@@ -548,6 +551,7 @@ struct AllRewriteRules {
   RewriteRule<SignExtendUltConst> rule126;
   RewriteRule<ZeroExtendUltConst> rule127;
   RewriteRule<MultSltMult> rule128;
+  RewriteRule<NormalizeEqPlusNeg> rule129;
 };
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index c2f6620aa..a02bf305f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -1451,6 +1451,84 @@ inline Node RewriteRule<BitwiseSlicing>::apply(TNode node)
   return result;
 }
 
+template <>
+inline bool RewriteRule<NormalizeEqPlusNeg>::applies(TNode node)
+{
+  return node.getKind() == kind::EQUAL
+         && (node[0].getKind() == kind::BITVECTOR_PLUS
+             || node[1].getKind() == kind::BITVECTOR_PLUS);
+}
+
+template <>
+inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")"
+                      << std::endl;
+
+  NodeBuilder<> nb_lhs(kind::BITVECTOR_PLUS);
+  NodeBuilder<> nb_rhs(kind::BITVECTOR_PLUS);
+  NodeManager *nm = NodeManager::currentNM();
+
+  if (node[0].getKind() == kind::BITVECTOR_PLUS)
+  {
+    for (const TNode &n : node[0])
+    {
+      if (n.getKind() == kind::BITVECTOR_NEG)
+        nb_rhs << n[0];
+      else
+        nb_lhs << n;
+    }
+  }
+  else
+  {
+    nb_lhs << node[0];
+  }
+
+  if (node[1].getKind() == kind::BITVECTOR_PLUS)
+  {
+    for (const TNode &n : node[1])
+    {
+      if (n.getKind() == kind::BITVECTOR_NEG)
+        nb_lhs << n[0];
+      else
+        nb_rhs << n;
+    }
+  }
+  else
+  {
+    nb_rhs << node[1];
+  }
+
+  Node zero = utils::mkZero(utils::getSize(node[0]));
+
+  Node lhs, rhs;
+  if (nb_lhs.getNumChildren() == 0)
+  {
+    lhs = zero;
+  }
+  else if (nb_lhs.getNumChildren() == 1)
+  {
+    lhs = nb_lhs[0];
+  }
+  else
+  {
+    lhs = nb_lhs.constructNode();
+  }
+  if (nb_rhs.getNumChildren() == 0)
+  {
+    rhs = zero;
+  }
+  else if (nb_rhs.getNumChildren() == 1)
+  {
+    rhs = nb_rhs[0];
+  }
+  else
+  {
+    rhs = nb_rhs.constructNode();
+  }
+  return nm->mkNode(node.getKind(), lhs, rhs);
+}
+
 // template<> inline
 // bool RewriteRule<>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_CONCAT);
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 4b79c4e79..678d87156 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -344,39 +344,46 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis
   }
 }
 
-void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
+void InstStrategyCbqi::checkOwnership(Node q)
+{
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
     if (d_do_cbqi[q] == CEG_HANDLED)
     {
       //take full ownership of the quantified formula
       d_quantEngine->setOwner( q, this );
-      
-      //mark all nested quantifiers with id
-      if( options::cbqiNestedQE() ){
-        std::map< Node, Node > visited;
-        Node mq = getIdMarkedQuantNode( q[1], visited );
-        if( mq!=q[1] ){
-          // do not do cbqi, we are reducing this quantified formula to a marked
-          // one
-          d_do_cbqi[q] = CEG_UNHANDLED;
-          //instead do reduction
-          std::vector< Node > qqc;
-          qqc.push_back( q[0] );
-          qqc.push_back( mq );
-          if( q.getNumChildren()==3 ){
-            qqc.push_back( q[2] );
-          }
-          Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
-          Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
-          Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
-          d_quantEngine->getOutputChannel().lemma( mlem );
-        }
-      }
     }
   }
 }
 
-void InstStrategyCbqi::registerQuantifier( Node q ) {
+void InstStrategyCbqi::preRegisterQuantifier(Node q)
+{
+  // mark all nested quantifiers with id
+  if (options::cbqiNestedQE())
+  {
+    if( d_quantEngine->getOwner(q)==this )
+    {
+      std::map<Node, Node> visited;
+      Node mq = getIdMarkedQuantNode(q[1], visited);
+      if (mq != q[1])
+      {
+        // do not do cbqi, we are reducing this quantified formula to a marked
+        // one
+        d_do_cbqi[q] = CEG_UNHANDLED;
+        // instead do reduction
+        std::vector<Node> qqc;
+        qqc.push_back(q[0]);
+        qqc.push_back(mq);
+        if (q.getNumChildren() == 3)
+        {
+          qqc.push_back(q[2]);
+        }
+        Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc);
+        Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq);
+        Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+        d_quantEngine->addLemma(mlem);
+      }
+    }
+  }
   if( doCbqi( q ) ){
     if( registerCbqiLemma( q ) ){
       Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
@@ -673,7 +680,8 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   }
 }
 
-void InstStrategyCegqi::registerQuantifier( Node q ) {
+void InstStrategyCegqi::preRegisterQuantifier(Node q)
+{
   if( doCbqi( q ) ){
     // get the instantiator  
     if( options::cbqiPreRegInst() ){
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 5a4db0e53..3445c3f9f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -103,8 +103,8 @@ class InstStrategyCbqi : public QuantifiersModule {
   void check(Theory::Effort e, QEffort quant_e) override;
   bool checkComplete() override;
   bool checkCompleteFor(Node q) override;
+  void checkOwnership(Node q) override;
   void preRegisterQuantifier(Node q) override;
-  void registerQuantifier(Node q) override;
   /** get next decision request */
   Node getNextDecisionRequest(unsigned& priority) override;
 };
@@ -147,8 +147,8 @@ class InstStrategyCegqi : public InstStrategyCbqi {
 
   //get instantiator for quantifier
   CegInstantiator * getInstantiator( Node q );
-  //register quantifier
-  void registerQuantifier(Node q) override;
+  /** pre-register quantifier */
+  void preRegisterQuantifier(Node q) override;
   //presolve
   void presolve() override;
 };
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 404f64471..807a7a58c 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -923,14 +923,6 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
   return addedLemmas;
 }
 
-void ConjectureGenerator::registerQuantifier( Node q ) {
-
-}
-
-void ConjectureGenerator::assertNode( Node n ) {
-
-}
-
 bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
   if( !ln.isNull() ){
     //do not consider if it is non-canonical, and either:
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 2db175fae..8a6339a85 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -428,9 +428,6 @@ public:
   void reset_round(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override;
-  void assertNode(Node n) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "ConjectureGenerator"; }
   // options
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 184add8c3..bd95b316d 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -157,7 +157,8 @@ bool InstantiationEngine::checkCompleteFor( Node q ) {
   return false;
 }
 
-void InstantiationEngine::preRegisterQuantifier( Node q ) {
+void InstantiationEngine::checkOwnership(Node q)
+{
   if( options::strictTriggers() && q.getNumChildren()==3 ){
     //if strict triggers, take ownership of this quantified formula
     bool hasPat = false;
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 32ddb19ed..e4cb986da 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -81,7 +81,7 @@ class InstantiationEngine : public QuantifiersModule {
   void reset_round(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
   bool checkCompleteFor(Node q) override;
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   void registerQuantifier(Node q) override;
   Node explain(TNode n) { return Node::null(); }
   /** add user pattern */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index d96fb4e05..b493d6a0c 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -384,10 +384,11 @@ void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
   Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; 
 }
 
-void BoundedIntegers::preRegisterQuantifier( Node f ) {
+void BoundedIntegers::checkOwnership(Node f)
+{
   //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
-  Trace("bound-int") << "preRegister quantifier " << f << std::endl;
-  
+  Trace("bound-int") << "check ownership quantifier " << f << std::endl;
+
   bool success;
   do{
     std::map< Node, unsigned > bound_lit_type_map;
@@ -546,10 +547,6 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
   }
 }
 
-void BoundedIntegers::registerQuantifier( Node q ) {
-
-}
-
 void BoundedIntegers::assertNode( Node n ) {
   Trace("bound-int-assert") << "Assert " << n << std::endl;
   Node nlit = n.getKind()==NOT ? n[0] : n;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 3e990067a..93b6436d5 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -146,8 +146,7 @@ public:
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
-  void registerQuantifier(Node q) override;
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   void assertNode(Node n) override;
   Node getNextDecisionRequest(unsigned& priority) override;
   bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 54689b32a..743e7ccc8 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -295,7 +295,6 @@ bool InstStrategyEnum::process(Node f, bool fullEffort)
   return false;
 }
 
-void InstStrategyEnum::registerQuantifier(Node q) {}
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index cf97518fc..51c0c1d0c 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -72,8 +72,6 @@ class InstStrategyEnum : public QuantifiersModule
    * quantified formulas via calls to process(...)
    */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /** Register quantifier. */
-  void registerQuantifier(Node q) override;
   /** Identify. */
   std::string identify() const override
   {
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 375754b26..c76d97255 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -32,7 +32,8 @@ QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){
 }
 
 /** add quantifier */
-void LtePartialInst::preRegisterQuantifier( Node q ) {
+void LtePartialInst::checkOwnership(Node q)
+{
   if( !q.getAttribute(LtePartialInstAttribute()) ){
     if( d_do_inst.find( q )!=d_do_inst.end() ){
       if( d_do_inst[q] ){
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 76a781e1c..2390eb40c 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -56,7 +56,7 @@ private:
 public:
   LtePartialInst( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   /** was invoked */
   bool wasInvoked() { return d_wasInvoked; }
   
@@ -64,11 +64,8 @@ public:
   bool needsCheck(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override {}
   /* check complete */
   bool checkComplete() override { return !d_wasInvoked; }
-  void assertNode(Node n) override {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "LtePartialInst"; }
 };
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 68a0f30dc..da6b0a6b4 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -31,8 +31,8 @@ QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
 
 }
 
-/** pre register quantifier */
-void QuantDSplit::preRegisterQuantifier( Node q ) {
+void QuantDSplit::checkOwnership(Node q)
+{
   int max_index = -1;
   int max_score = -1;
   if( q.getNumChildren()==3 ){
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 1ea57433a..94bfa0f20 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -34,7 +34,7 @@ private:
 public:
   QuantDSplit( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
 
   /* whether this module needs to check this round */
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index f3fdfa6f4..874baa482 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -108,19 +108,27 @@ class QuantifiersModule {
    * we are incomplete for other reasons.
    */
   virtual bool checkCompleteFor( Node q ) { return false; }
-  /** Pre register quantifier.
+  /** Check ownership
    *
-   * Called once for new quantified formulas that are
-   * pre-registered by the quantifiers theory.
+   * Called once for new quantified formulas that are registered by the
+   * quantifiers theory. The primary purpose of this function is to establish
+   * if this module is the owner of quantified formula q.
    */
-  virtual void preRegisterQuantifier( Node q ) { }
+  virtual void checkOwnership(Node q) {}
   /** Register quantifier
    *
+   * Called once for new quantified formulas q that are pre-registered by the
+   * quantifiers theory, after internal ownership of quantified formulas is
+   * finalized. This does context-dependent initialization of this module.
+   */
+  virtual void registerQuantifier(Node q) {}
+  /** Pre-register quantifier
+   *
    * Called once for new quantified formulas that are
    * pre-registered by the quantifiers theory, after
    * internal ownership of quantified formulas is finalized.
    */
-  virtual void registerQuantifier( Node q ) = 0;
+  virtual void preRegisterQuantifier(Node q) {}
   /** Assert node.
    *
    * Called when a quantified formula q is asserted to the quantifiers theory
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5016bd87f..79b7d9a99 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -83,13 +83,23 @@ void TheoryQuantifiers::finishInit()
 }
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
+  if (n.getKind() != FORALL)
+  {
+    return;
+  }
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL ){
-    if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
-      getQuantifiersEngine()->registerQuantifier( n );
-      Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << 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);
+  Debug("quantifiers-prereg")
+      << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
 }
 
 
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 4f0302bf3..b82dccd73 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -65,9 +65,6 @@ class TheoryQuantifiers : public Theory {
   void assertUniversal( Node n );
   void assertExistential( Node n );
   void computeCareGraph() override;
-
-  using BoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
-
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8e6aab06c..944010ab1 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -76,6 +76,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_term_enum(new quantifiers::TermEnumeration),
       d_conflict_c(c, false),
       // d_quants(u),
+      d_quants_prereg(u),
       d_quants_red(u),
       d_lemmas_produced_c(u),
       d_ierCounter_c(c),
@@ -734,54 +735,73 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
   }
 }
 
-bool QuantifiersEngine::registerQuantifier( Node f ){
+void QuantifiersEngine::registerQuantifierInternal(Node f)
+{
   std::map< Node, bool >::iterator it = d_quants.find( f );
   if( it==d_quants.end() ){
     Trace("quant") << "QuantifiersEngine : Register quantifier ";
     Trace("quant") << " : " << f << std::endl;
+    unsigned prev_lemma_waiting = d_lemmas_waiting.size();
     ++(d_statistics.d_num_quant);
     Assert( f.getKind()==FORALL );
+    // register with utilities
+    for (unsigned i = 0; i < d_util.size(); i++)
+    {
+      d_util[i]->registerQuantifier(f);
+    }
+    // compute attributes
+    d_quant_attr->computeAttributes(f);
 
-    //check whether we should apply a reduction
-    if( reduceQuantifier( f ) ){
-      Trace("quant") << "...reduced." << std::endl;
-      d_quants[f] = false;
-      return false;
-    }else{
-      // register with utilities
-      for (unsigned i = 0; i < d_util.size(); i++)
-      {
-        d_util[i]->registerQuantifier(f);
-      }
-      // compute attributes
-      d_quant_attr->computeAttributes(f);
-
-      for( unsigned i=0; i<d_modules.size(); i++ ){
-        Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
-        d_modules[i]->preRegisterQuantifier( f );
-      }
-      QuantifiersModule * qm = getOwner( f );
-      if( qm!=NULL ){
-        Trace("quant") << "   Owner : " << qm->identify() << std::endl;
-      }
-      //register with each module
-      for( unsigned i=0; i<d_modules.size(); i++ ){
-        Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
-        d_modules[i]->registerQuantifier( f );
-      }
-      //TODO: remove this
-      Node ceBody = d_term_util->getInstConstantBody( f );
-      Trace("quant-debug")  << "...finish." << std::endl;
-      d_quants[f] = true;
-      // flush lemmas
-      flushLemmas();
-      return true;
+    for (QuantifiersModule*& mdl : d_modules)
+    {
+      Trace("quant-debug") << "check ownership with " << mdl->identify()
+                           << "..." << std::endl;
+      mdl->checkOwnership(f);
     }
-  }else{
-    return (*it).second;
+    QuantifiersModule* qm = getOwner(f);
+    Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
+                   << std::endl;
+    // register with each module
+    for (QuantifiersModule*& mdl : d_modules)
+    {
+      Trace("quant-debug") << "register with " << mdl->identify() << "..."
+                           << std::endl;
+      mdl->registerQuantifier(f);
+      // since this is context-independent, we should not add any lemmas during
+      // this call
+      Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
+    }
+    // TODO (#2020): remove this
+    Node ceBody = d_term_util->getInstConstantBody(f);
+    Trace("quant-debug") << "...finish." << std::endl;
+    d_quants[f] = true;
+    AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
   }
 }
 
+void QuantifiersEngine::preRegisterQuantifier(Node q)
+{
+  NodeSet::const_iterator it = d_quants_prereg.find(q);
+  if (it != d_quants_prereg.end())
+  {
+    return;
+  }
+  Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
+  d_quants_prereg.insert(q);
+  // ensure that it is registered
+  registerQuantifierInternal(q);
+  // register with each module
+  for (QuantifiersModule*& mdl : d_modules)
+  {
+    Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
+                         << std::endl;
+    mdl->preRegisterQuantifier(q);
+  }
+  // flush the lemmas
+  flushLemmas();
+  Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
+}
+
 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
     std::set< Node > added;
@@ -790,31 +810,35 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 }
 
 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
+  if (reduceQuantifier(f))
+  {
+    // if we can reduce it, nothing left to do
+    return;
+  }
   if( !pol ){
-    //if not reduced
-    if( !reduceQuantifier( f ) ){
-      //do skolemization
-      Node lem = d_skolemize->process(f);
-      if (!lem.isNull())
+    // do skolemization
+    Node lem = d_skolemize->process(f);
+    if (!lem.isNull())
+    {
+      if (Trace.isOn("quantifiers-sk-debug"))
       {
-        if( Trace.isOn("quantifiers-sk-debug") ){
-          Node slem = Rewriter::rewrite( lem );
-          Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
-        }
-        getOutputChannel().lemma( lem, false, true );
+        Node slem = Rewriter::rewrite(lem);
+        Trace("quantifiers-sk-debug")
+            << "Skolemize lemma : " << slem << std::endl;
       }
+      getOutputChannel().lemma(lem, false, true);
     }
-  }else{
-    //assert to modules TODO : also for !pol?
-    //register the quantifier, assert it to each module
-    if( registerQuantifier( f ) ){
-      d_model->assertQuantifier( f );
-      for( unsigned i=0; i<d_modules.size(); i++ ){
-        d_modules[i]->assertNode( f );
-      }
-      addTermToDatabase( d_term_util->getInstConstantBody( f ), true );
-    }
+    return;
+  }
+  // ensure the quantified formula is registered
+  registerQuantifierInternal(f);
+  // assert it to each module
+  d_model->assertQuantifier(f);
+  for (QuantifiersModule*& mdl : d_modules)
+  {
+    mdl->assertNode(f);
   }
+  addTermToDatabase(d_term_util->getInstConstantBody(f), true);
 }
 
 void QuantifiersEngine::propagate( Theory::Effort level ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 456a268da..70a4ede0c 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -173,6 +173,8 @@ private:
  private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
+  /** quantifiers pre-registered */
+  NodeSet d_quants_prereg;
   /** quantifiers reduced */
   BoolMap d_quants_red;
   std::map< Node, Node > d_quants_red_lem;
@@ -277,8 +279,12 @@ public:
   void check( Theory::Effort e );
   /** notify that theories were combined */
   void notifyCombineTheories();
-  /** register quantifier */
-  bool registerQuantifier( Node f );
+  /** preRegister quantifier
+   *
+   * This function is called after registerQuantifier for quantified formulas
+   * that are pre-registered to the quantifiers theory.
+   */
+  void preRegisterQuantifier(Node q);
   /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
@@ -288,10 +294,19 @@ public:
   /** get next decision request */
   Node getNextDecisionRequest( unsigned& priority );
 private:
-  /** reduceQuantifier, return true if reduced */
-  bool reduceQuantifier( Node q );
-  /** flush lemmas */
-  void flushLemmas();
+ /** (context-indepentent) register quantifier internal
+  *
+  * This is called when a quantified formula q is pre-registered to the
+  * quantifiers theory, and updates the modules in this class with
+  * context-independent information about how to handle q. This includes basic
+  * information such as which module owns q.
+  */
+ void registerQuantifierInternal(Node q);
+ /** reduceQuantifier, return true if reduced */
+ bool reduceQuantifier(Node q);
+ /** flush lemmas */
+ void flushLemmas();
+
 public:
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );