From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 02:36:24 +0000 (-0500)
Subject: Remove instantiation propagator infrastructure (#3975)
X-Git-Tag: cvc5-1.0.0~3539
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ebc297e6ff589f7b98519cd2aa23963a4e06652;p=cvc5.git

Remove instantiation propagator infrastructure (#3975)
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 57f0ec95e..5b07a7ca6 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -511,8 +511,6 @@ libcvc4_add_sources(
   theory/quantifiers/inst_match.h
   theory/quantifiers/inst_match_trie.cpp
   theory/quantifiers/inst_match_trie.h
-  theory/quantifiers/inst_propagator.cpp
-  theory/quantifiers/inst_propagator.h
   theory/quantifiers/inst_strategy_enumerative.cpp
   theory/quantifiers/inst_strategy_enumerative.h
   theory/quantifiers/instantiate.cpp
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
deleted file mode 100644
index 6566319fa..000000000
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ /dev/null
@@ -1,864 +0,0 @@
-/*********************                                                        */
-/*! \file inst_propagator.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** Propagate mechanism for instantiations
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/inst_propagator.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-
-EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){
-  d_true = NodeManager::currentNM()->mkConst( true );
-  d_false = NodeManager::currentNM()->mkConst( false );
-}
-
-bool EqualityQueryInstProp::reset( Theory::Effort e ) {
-  d_uf.clear();
-  d_uf_exp.clear();
-  d_diseq_list.clear();
-  d_uf_func_map_trie.clear();
-  return true;
-}
-
-/** contains term */
-bool EqualityQueryInstProp::hasTerm( Node a ) {
-  if( getEngine()->hasTerm( a ) ){
-    return true;
-  }else{
-    std::vector< Node > exp;
-    Node ar = getUfRepresentative( a, exp );
-    return !ar.isNull() && getEngine()->hasTerm( ar );
-  }
-}
-
-/** get the representative of the equivalence class of a */
-Node EqualityQueryInstProp::getRepresentative( Node a ) {
-  if( getEngine()->hasTerm( a ) ){
-    a = getEngine()->getRepresentative( a );
-  }
-  std::vector< Node > exp;
-  Node ar = getUfRepresentative( a, exp );
-  return ar.isNull() ? a : ar;
-}
-
-/** returns true if a and b are equal in the current context */
-bool EqualityQueryInstProp::areEqual( Node a, Node b ) {
-  if( a==b ){
-    return true;
-  }else{
-    eq::EqualityEngine* ee = getEngine();
-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      if( ee->areEqual( a, b ) ){
-        return true;
-      }
-    }
-    return false;
-  }
-}
-
-/** returns true is a and b are disequal in the current context */
-bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
-  if( a==b ){
-    return false;
-  }else{
-    eq::EqualityEngine* ee = getEngine();
-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      if( ee->areDisequal( a, b, false ) ){
-        return true;
-      }
-    }
-    return false;
-  }
-}
-
-/** get the equality engine associated with this query */
-eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
-  return d_qe->getActiveEqualityEngine();
-}
-
-/** get the equivalence class of a */
-void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {
-  //TODO?
-}
-
-TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {
-  TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
-  if( !t.isNull() ){
-    return t;
-  }else{
-    return d_uf_func_map_trie[f].existsTerm( args );
-  }
-}
-
-Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {
-  bool engine_has_a = getEngine()->hasTerm( a );
-  if( engine_has_a ){
-    a = getEngine()->getRepresentative( a );
-  }
-  //get union find representative, if this occurs in the equality engine, return it
-  unsigned prev_size = exp.size();
-  Node ar = getUfRepresentative( a, exp );
-  if( !ar.isNull() ){
-    if( engine_has_a || getEngine()->hasTerm( ar ) ){
-      Trace("qip-eq") << "getRepresentativeExp " << a << " returns " << ar << std::endl;
-      Assert(getEngine()->hasTerm(ar));
-      Assert(getEngine()->getRepresentative(ar) == ar);
-      return ar;
-    }
-  }else{
-    if( engine_has_a ){
-      return a;
-    }
-  }
-  //retract explanation
-  while( exp.size()>prev_size ){
-    exp.pop_back();
-  }
-  return Node::null();
-}
-
-bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {
-  if( areEqual( a, b ) ){
-    return true;
-  }else{
-    std::vector< Node > exp_a;
-    Node ar = getUfRepresentative( a, exp_a );
-    if( !ar.isNull() ){
-      std::vector< Node > exp_b;
-      if( ar==getUfRepresentative( b, exp_b ) ){
-        merge_exp( exp, exp_a );
-        merge_exp( exp, exp_b );
-        return true;
-      }
-    }
-    return false;
-  }
-}
-
-bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {
-  if( areDisequal( a, b ) ){
-    return true;
-  }else{
-    //Assert( getRepresentative( a )==a );
-    //Assert( getRepresentative( b )==b );
-    std::map< Node, std::vector< Node > >::iterator itd = d_diseq_list[a].find( b );
-    if( itd!=d_diseq_list[a].end() ){
-      exp.insert( exp.end(), itd->second.begin(), itd->second.end() );
-      return true;
-    }else{
-      return false;
-    }
-  }
-}
-
-TNode EqualityQueryInstProp::getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ) {
-  TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
-  if( !t.isNull() ){
-    return t;
-  }else{
-    TNode tt = d_uf_func_map_trie[f].existsTerm( args );
-    if( !tt.isNull() ){
-      //TODO?
-      return tt;
-    }else{
-      return tt;
-    }
-  }
-}
-
-Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
-  Assert(exp.empty());
-  std::map< Node, Node >::iterator it = d_uf.find( a );
-  if( it!=d_uf.end() ){
-    if( it->second==a ){
-      Assert(d_uf_exp[a].empty());
-      return it->second;
-    }else{
-      Node m = getUfRepresentative( it->second, exp );
-      Assert(!m.isNull());
-      if( m!=it->second ){
-        //update union find
-        d_uf[ a ] = m;
-        //update explanation : merge the explanation of the parent
-        merge_exp( d_uf_exp[ a ], exp );
-        Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;
-      }
-      //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset
-      exp.clear();
-      exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );
-      return m;
-    }
-  }else{
-    return Node::null();
-  }
-}
-
-// set a == b with reason, return status, modify a and b to representatives pre-merge
-int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ) {
-  if( a==b ){
-    return pol ? STATUS_NONE : STATUS_CONFLICT;
-  }
-  int status = pol ? STATUS_MERGED_UNKNOWN : STATUS_NONE;
-  Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", pol = " << pol << ", reason size = " << reason.size() << std::endl;
-  //get the representative for a
-  std::vector< Node > exp_a;
-  Node ar = getUfRepresentative( a, exp_a );
-  if( ar.isNull() ){
-    Assert(exp_a.empty());
-    ar = a;
-  }
-  if( ar==b ){
-    Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
-    if( pol ){
-      return STATUS_NONE;
-    }else{
-      merge_exp( reason, exp_a );
-      return STATUS_CONFLICT;
-    }
-  }
-  bool swap = false;
-  //get the representative for b
-  std::vector< Node > exp_b;
-  Node br = getUfRepresentative( b, exp_b );
-  if( br.isNull() ){
-    Assert(exp_b.empty());
-    br = b;
-    if( !getEngine()->hasTerm( br ) ){
-      if( ar!=a || getEngine()->hasTerm( ar ) ){
-        swap = true;
-      }
-    }else{
-      if( getEngine()->hasTerm( ar ) ){
-        status = STATUS_MERGED_KNOWN;
-      }
-    }
-  }else{
-    if( ar==br ){
-      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
-      if( pol ){
-        return STATUS_NONE;
-      }else{
-        merge_exp( reason, exp_a );
-        merge_exp( reason, exp_b );
-        return STATUS_CONFLICT;
-      }
-    }else if( getEngine()->hasTerm( ar ) ){
-      if( getEngine()->hasTerm( br ) ){
-        status = STATUS_MERGED_KNOWN;
-      }else{
-        swap = true;
-      }
-    }
-  }
-
-  if( swap ){
-    //swap
-    Node temp_r = ar;
-    ar = br;
-    br = temp_r;
-  }
-
-  Assert(!getEngine()->hasTerm(ar) || getEngine()->hasTerm(br));
-  Assert(ar != br);
-
-  std::vector< Node > exp_d;
-  if( areDisequalExp( ar, br, exp_d ) ){
-    if( pol ){
-      merge_exp( reason, exp_b );
-      merge_exp( reason, exp_b );
-      merge_exp( reason, exp_d );
-      return STATUS_CONFLICT;
-    }else{
-      return STATUS_NONE;
-    }
-  }else{
-    if( pol ){
-      //update the union find
-      Assert(d_uf_exp[ar].empty());
-      Assert(d_uf_exp[br].empty());
-
-      //registerUfTerm( ar );
-      d_uf[ar] = br;
-      merge_exp( d_uf_exp[ar], exp_a );
-      merge_exp( d_uf_exp[ar], exp_b );
-      merge_exp( d_uf_exp[ar], reason );
-
-      //registerUfTerm( br );
-      d_uf[br] = br;
-      d_uf_exp[br].clear();
-
-      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;
-      a = ar;
-      b = br;
-
-      //carry disequality list
-      std::map< Node, std::map< Node, std::vector< Node > > >::iterator itd = d_diseq_list.find( ar );
-      if( itd!=d_diseq_list.end() ){
-        for( std::map< Node, std::vector< Node > >::iterator itdd = itd->second.begin(); itdd != itd->second.end(); ++itdd ){
-          Node d = itdd->first;
-          if( d_diseq_list[br].find( d )==d_diseq_list[br].end() ){
-            merge_exp( d_diseq_list[br][d], itdd->second );
-            merge_exp( d_diseq_list[br][d], d_uf_exp[ar] );
-          }
-        }
-      }
-
-      return status;
-    }else{
-      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : disequal " << ar << " <> " << br << std::endl;
-      Assert(d_diseq_list[ar].find(br) == d_diseq_list[ar].end());
-      Assert(d_diseq_list[br].find(ar) == d_diseq_list[br].end());
-
-      merge_exp( d_diseq_list[ar][br], reason );
-      merge_exp( d_diseq_list[br][ar], reason );
-      return STATUS_NONE;
-    }
-  }
-}
-
-void EqualityQueryInstProp::registerUfTerm( TNode n ) {
-  if( d_uf.find( n )==d_uf.end() ){
-    if( !getEngine()->hasTerm( n ) ){
-      TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
-      if( !f.isNull() ){
-        std::vector< TNode > args;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          if( !getEngine()->hasTerm( n[i] ) ){
-            return;
-          }else{
-            args.push_back( n[i] );
-          }
-        }
-        d_uf_func_map_trie[f].addTerm( n, args );
-      }
-    }
-  }
-}
-
-//void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) {
-void EqualityQueryInstProp::addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ) {
-  if( is_watch ){
-    watch.push_back( n );
-  }
-  args.push_back( n );
-}
-
-bool EqualityQueryInstProp::isPropagateLiteral( Node n ) {
-  if( n==d_true || n==d_false ){
-    return false;
-  }else{
-    Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
-    if( ak==EQUAL ){
-      Node atom = n.getKind()==NOT ? n[0] : n;
-      return !atom[0].getType().isBoolean();
-    }else{
-      Assert(ak != NOT);
-      return ak!=AND && ak!=OR && ak!=ITE;
-    }
-  }
-}
-
-void EqualityQueryInstProp::setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out ) {
-  if( watch.empty() ){
-    watch.push_back( n );
-  }
-  for( unsigned j=0; j<watch.size(); j++ ){
-    Trace("qip-eval") << "Watch : " << n << " -> " << watch[j] << std::endl;
-    watch_list_out[n].push_back( watch[j] );
-  }
-}
-
-void EqualityQueryInstProp::collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list ) {
-  std::map< Node, std::vector< Node > >::iterator it = watch_list_out.find( n );
-  if( it!=watch_list_out.end() && std::find( watch_list.begin(), watch_list.end(), n )==watch_list.end() ){
-    watch_list.push_back( n );
-    for( unsigned j=0; j<it->second.size(); j++ ){
-      collectWatchList( it->second[j], watch_list_out, watch_list );
-    }
-  }
-}
-
-//this is similar to TermDb::evaluateTerm2, but tracks more information
-Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< int, std::map< Node, Node > >& visited,
-                                             bool hasPol, bool pol, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& props ) {
-  int polIndex = hasPol ? ( pol ? 1 : -1 ) : 0;
-  std::map< Node, Node >::iterator itv = visited[polIndex].find( n );
-  if( itv!=visited[polIndex].end() ){
-    return itv->second;
-  }else{
-    visited[polIndex][n] = n;
-    Node ret;
-    //check if it should be propagated in this context
-    if( hasPol && isPropagateLiteral( n ) ){
-      Assert(n.getType().isBoolean());
-      //must be Boolean
-      ret = evaluateTermExp( n, exp, visited, false, pol, watch_list_out, props );
-      if( isPropagateLiteral( ret ) ){
-        Trace("qip-eval") << "-----> propagate : " << ret << std::endl;
-        props.push_back( pol ? ret : ret.negate() );
-        ret = pol ? d_true : d_false;
-      }
-    }else{
-      Trace("qip-eval") << "evaluate term : " << n << " [" << polIndex << "]" << std::endl;
-      std::vector< Node > exp_n;
-      ret = getRepresentativeExp( n, exp_n );
-      if( ret.isNull() ){
-        //term is not known to be equal to a representative in equality engine, evaluate it
-        Kind k = n.getKind();
-        if( k!=FORALL ){
-          TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
-          std::vector< Node > args;
-          bool ret_set = false;
-          bool childChanged = false;
-          int abort_i = -1;
-          //get the child entailed polarity
-          Assert(n.getKind() != IMPLIES);
-          bool newHasPol, newPol;
-          QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
-          std::vector< Node > watch;
-          //for each child
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out, props );
-            if( c.isNull() ){
-              ret = Node::null();
-              ret_set = true;
-              break;
-            }else if( c==d_true || c==d_false ){
-              //short-circuiting
-              if( k==kind::AND || k==kind::OR ){
-                if( (k==kind::AND)==(c==d_false) ){
-                  ret = c;
-                  ret_set = true;
-                  break;
-                }else{
-                  //redundant
-                  c = Node::null();
-                  childChanged = true;
-                }
-              }else if( k==kind::ITE && i==0 ){
-                ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out, props );
-                ret_set = true;
-                break;
-              }else if( k==kind::NOT ){
-                ret = c==d_true ? d_false : d_true;
-                ret_set = true;
-                break;
-              }
-            }
-            if( !c.isNull() ){
-              childChanged = childChanged || n[i]!=c;
-              bool is_watch = watch_list_out.find( c )!=watch_list_out.end();
-              if( !f.isNull() && is_watch ){
-                // we are done if this is an UF application and an argument is unevaluated
-                addArgument( c, args, watch, is_watch );
-                abort_i = i;
-                break;
-              }else if( k==kind::AND || k==kind::OR || k==kind::ITE || ( k==EQUAL && n[0].getType().isBoolean() ) ){
-                Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl;
-                if( ( k==kind::AND || k==kind::OR  ) && c.getKind()==k ){
-                  //flatten
-                  for( unsigned j=0; j<c.getNumChildren(); j++ ){
-                    addArgument( c[j], args, watch, is_watch );
-                  }
-                }else{
-                  addArgument( c, args, watch, is_watch );
-                }
-                Trace("qip-eval-debug") << "props/args = " << props.size() << "/" << args.size() << std::endl;
-                //if we are in a branching position
-                if( hasPol && !newHasPol && args.size()>=2 ){
-                  //we are done if at least two args are unevaluated
-                  abort_i = i;
-                  break;
-                }
-              }else{
-                addArgument( c, args, watch, is_watch );
-              }
-            }
-          }
-          //add remaining children if we aborted
-          if( abort_i!=-1 ){
-            Trace("qip-eval-debug") << "..." << n << " aborted at " << abort_i << std::endl;
-            for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){
-              args.push_back( n[i] );
-            }
-          }
-          //if we have not short-circuited evaluation
-          if( !ret_set ){
-            //if it is an indexed term, return the congruent term
-            if( !f.isNull() && watch.empty() ){
-              std::vector< TNode > t_args;
-              for( unsigned i=0; i<args.size(); i++ ) {
-                Trace("qip-eval") << "arg " << i << " : " << args[i] << std::endl;
-                t_args.push_back( args[i] );
-              }
-              Assert(args.size() == n.getNumChildren());
-              //args contains terms known by the equality engine
-              TNode nn = getCongruentTerm( f, t_args );
-              Trace("qip-eval") << "  got congruent term " << nn << " for " << n << std::endl;
-              if( !nn.isNull() ){
-                //successfully constructed representative in EE
-                Assert(exp_n.empty());
-                ret = getRepresentativeExp( nn, exp_n );
-                Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
-                merge_exp( exp, exp_n );
-                ret_set = true;
-                Assert(!ret.isNull());
-                Assert(ret != n);
-                // we have that n == ret, check if the union find should be updated TODO?
-              }else{
-                watch.push_back( ret );
-              }
-            }
-            if( !ret_set ){
-              if( childChanged || args.size()!=n.getNumChildren() ){
-                Trace("qip-eval") << "return rewrite" << std::endl;
-                if( k==kind::AND || k==kind::OR ){
-                  if( args.empty() ){
-                    ret = k==kind::AND ? d_true : d_false;
-                    ret_set = true;
-                  }else if( args.size()==1 ){
-                    //need to re-evaluate (may be new propagations)
-                    ret = evaluateTermExp( args[0], exp, visited, hasPol, pol, watch_list_out, props );
-                    ret_set = true;
-                  }
-                }else{
-                  Assert(args.size() == n.getNumChildren());
-                }
-                if( !ret_set ){
-                  if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-                    args.insert( args.begin(), n.getOperator() );
-                  }
-                  ret = NodeManager::currentNM()->mkNode( k, args );
-                  setWatchList( ret, watch, watch_list_out );
-                  ret = Rewriter::rewrite( ret );
-                  //need to re-evaluate
-                  ret = evaluateTermExp( ret, exp, visited, hasPol, pol, watch_list_out, props );
-                }
-              }else{
-                ret = n;
-                setWatchList( ret, watch, watch_list_out );
-              }
-            }
-          }
-        }
-      }else{
-        Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;
-        merge_exp( exp, exp_n );
-      }
-    }
-
-    Trace("qip-eval") << "evaluated term : " << n << " [" << polIndex << "], got : " << ret << ", exp size = " << exp.size() << ", watch list size = " << watch_list_out.size() << std::endl;
-    visited[polIndex][n] = ret;
-    return ret;
-  }
-}
-
-void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {
-  //TODO : optimize
-  if( v.empty() ){
-    Assert(up_to_size == -1 || up_to_size == (int)v_to_merge.size());
-    v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );
-  }else{
-    //std::vector< Node >::iterator v_end = v.end();
-    up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;
-    for( int j=0; j<up_to_size; j++ ){
-      if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){
-        v.push_back( v_to_merge[j] );
-      }
-    }
-  }
-}
-
-
-void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {
-  d_active = true;
-  //information about the instance
-  d_q = q;
-  d_lem = lem;
-  Assert(d_terms.empty());
-  d_terms.insert( d_terms.end(), terms.begin(), terms.end() );
-  //the current lemma
-  d_curr = body;
-  d_curr_exp.push_back( body );
-}
-
-InstPropagator::InstPropagator(QuantifiersEngine* qe)
-    : d_qe(qe),
-      d_notify(*this),
-      d_qy(qe),
-      d_icount(1),
-      d_conflict(false),
-      d_has_relevant_inst(false) {}
-
-bool InstPropagator::reset( Theory::Effort e ) {
-  d_icount = 1;
-  d_ii.clear();
-  for( unsigned i=0; i<2; i++ ){
-    d_conc_to_id[i].clear();
-    d_conc_to_id[i][d_qy.d_true] = 0;
-  }
-  d_conflict = false;
-  d_watch_list.clear();
-  d_update_list.clear();
-  d_relevant_inst.clear();
-  d_has_relevant_inst = false;
-  return d_qy.reset( e );
-}
-
-bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e,
-                                         Node q,
-                                         Node lem,
-                                         std::vector<Node>& terms,
-                                         Node body)
-{
-  if( !d_conflict ){
-    if( Trace.isOn("qip-prop") ){
-      Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        Trace("qip-prop") << "  " << terms[i] << std::endl;
-      }
-    }
-    unsigned id = allocateInstantiation( q, lem, terms, body );
-    //initialize the information
-    if( cacheConclusion( id, body ) ){
-      Assert(d_update_list.empty());
-      d_update_list.push_back( id );
-      bool firstTime = true;
-      //update infos in the update list until empty
-      do {
-        unsigned uid = d_update_list.back();
-        d_update_list.pop_back();
-        if( d_ii[uid].d_active ){
-          update( uid, d_ii[uid], firstTime );
-        }
-        firstTime = false;
-      }while( !d_conflict && !d_update_list.empty() );
-    }else{
-      d_ii[id].d_active = false;
-      Trace("qip-prop") << "...duplicate." << std::endl;
-    }
-    Trace("qip-prop") << "...finished notify instantiation." << std::endl;
-    return !d_conflict;
-  }else{
-    Assert(false);
-    return false;
-  }
-}
-
-void InstPropagator::filterInstantiations() {
-  if( d_has_relevant_inst ){
-    //now, inform quantifiers engine which instances should be retracted
-    Trace("qip-prop-debug") << "...remove instantiation ids : ";
-    for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
-      if( !it->second.d_q.isNull() ){
-        if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
-          if (!d_qe->getInstantiate()->removeInstantiation(
-                  it->second.d_q, it->second.d_lem, it->second.d_terms))
-          {
-            Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
-            Assert(false);
-          }else{
-            Trace("qip-prop-debug") << it->first << " ";
-          }
-        }else{
-          //mark the quantified formula as relevant
-          d_qe->markRelevant( it->second.d_q );
-        }
-      }
-    }
-    Trace("qip-prop-debug") << std::endl;
-    Trace("quant-engine-conflict") << "-----> InstPropagator::" << ( d_conflict ? "conflict" : "propagate" ) << " with " << d_relevant_inst.size() << " instances." << std::endl;
-  }
-}
-
-unsigned InstPropagator::allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) {
-  unsigned id = d_icount;
-  d_icount++;
-  Trace("qip-prop") << "...assign id=" << id << std::endl;
-  d_ii[id].init( q, lem, terms, body );
-  return id;
-}
-
-bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
-  Assert(!d_conflict);
-  Assert(ii.d_active);
-  Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;
-  //update the evaluation of the current lemma
-  std::map< Node, std::vector< Node > > watch_list_out;
-  std::map< int, std::map< Node, Node > > visited;
-  std::vector< Node > exp;
-  std::vector< Node > props;
-  Node eval = d_qy.evaluateTermExp( ii.d_curr, exp, visited, true, true, watch_list_out, props );
-  EqualityQueryInstProp::merge_exp( ii.d_curr_exp, exp );
-  if( eval.isNull() ){
-    ii.d_active = false;
-  }else if( firstTime || eval!=ii.d_curr ){
-    std::vector< Node > watch_list;
-    d_qy.collectWatchList( eval, watch_list_out, watch_list );
-    if( Trace.isOn("qip-prop") ){
-      Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;
-      Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << std::endl; 
-      Trace("qip-prop") << "...explanation = ";
-      debugPrintExplanation( ii.d_curr_exp, "qip-prop" );
-      Trace("qip-prop") << std::endl;
-      Trace("qip-prop") << "...watch list: " << std::endl;
-      for( unsigned i=0; i<watch_list.size(); i++ ){
-        Trace("qip-prop") << "  " << watch_list[i] << std::endl;
-      }
-      Trace("qip-prop") << "...new propagations: " << std::endl;
-      for( unsigned i=0; i<props.size(); i++ ){
-        Trace("qip-prop") << "  " << props[i] << std::endl;
-      }
-      Trace("qip-prop") << std::endl;
-    }
-    //determine the status of eval
-    if( eval==d_qy.d_false ){
-      Assert(props.empty());
-      //we have inferred a conflict
-      conflict( ii.d_curr_exp );
-      return false;
-    }else{
-      for( unsigned i=0; i<props.size(); i++ ){
-        Trace("qip-prop-debug2")  << "Process propagation " << props[i] << std::endl;
-        Assert(d_qy.isPropagateLiteral(props[i]));
-        //if we haven't propagated this literal yet
-        if( cacheConclusion( id, props[i], 1 ) ){
-          //watch list for propagated literal: may not yet be purely EE representatives
-          std::vector< Node > prop_watch_list;
-          d_qy.collectWatchList( props[i], watch_list_out, prop_watch_list );
-        
-          Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];
-          bool pol = props[i].getKind()!=NOT;
-          if( lit.getKind()==EQUAL ){
-            propagate( lit[0], lit[1], pol, ii.d_curr_exp );
-          }else{
-            propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );
-          }
-          if( d_conflict ){
-            return false;
-          }
-        }
-        Trace("qip-prop-debug2")  << "Done process propagation " << props[i] << std::endl;
-      }
-      //if we have not inferred this conclusion yet
-      if( cacheConclusion( id, eval ) ){
-        ii.d_curr = eval;
-        //update the watch list
-        Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;
-        //Here, we need to be notified of enough terms such that if we are not notified, then update( id, ii ) will return no propagations.
-        //  Similar to two-watched literals, but since we are taking into account UF, we need to watch all terms on a complete path of two terms.
-        for( unsigned i=0; i<watch_list.size(); i++ ){
-          d_watch_list[ watch_list[i] ][ id ] = true;
-        }
-      }else{
-        Trace("qip-prop-debug") << "...conclusion " << eval << " is duplicate." << std::endl;
-        ii.d_active = false;
-      }
-    }
-  }else{
-    Trace("qip-prop-debug") << "...did not update." << std::endl;
-  }
-  Assert(!d_conflict);
-  return true;
-}
-
-void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {
-  if( Trace.isOn("qip-propagate") ){
-    Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";
-    debugPrintExplanation( exp, "qip-propagate" );
-    Trace("qip-propagate") << "..." << std::endl;
-  }
-  //set equal
-  int status = d_qy.setEqual( a, b, pol, exp );
-  if( status==EqualityQueryInstProp::STATUS_NONE ){
-    Trace("qip-prop-debug") << "...already equal/no conflict." << std::endl;
-    return;
-  }else if( status==EqualityQueryInstProp::STATUS_CONFLICT ){
-    Trace("qip-prop-debug") << "...conflict." << std::endl;
-    conflict( exp );
-    return;
-  }
-  if( pol ){
-    if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
-      Trace("qip-rlv-propagate")
-          << "Relevant propagation : " << a << " == " << b << std::endl;
-      Assert(d_qy.getEngine()->hasTerm(a));
-      Assert(d_qy.getEngine()->hasTerm(b));
-      Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
-      addRelevantInstances( exp, "qip-propagate" );
-      //d_has_relevant_inst = true;
-    }
-    Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl;
-    for( unsigned i=0; i<2; i++ ){
-      //update terms from watched lists
-      Node c = i==0 ? a : b;
-      std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );
-      if( it!=d_watch_list.end() ){
-        Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;
-        for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){
-          unsigned idw = itw->first;
-          if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){
-            Trace("qip-prop-debug") << "...will update " << idw << std::endl;
-            d_update_list.push_back( idw );
-          }
-        }
-        d_watch_list.erase( c );
-      }
-    }
-  }
-}
-
-void InstPropagator::conflict( std::vector< Node >& exp ) {
-  Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;
-  d_conflict = true;
-  d_relevant_inst.clear();
-  addRelevantInstances( exp, "qip-propagate" );
-  d_has_relevant_inst = true;
-}
-
-bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
-  Assert(prop_index == 0 || prop_index == 1);
-  //check if the conclusion is non-redundant
-  if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){
-    d_conc_to_id[prop_index][body] = id;
-    return true;
-  }else{
-    return false;
-  }
-}
-
-void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {
-  for( unsigned i=0; i<exp.size(); i++ ){
-    Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end());
-    Trace(c) << "  relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;
-    d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;
-  }
-}
-
-void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {
-  for( unsigned i=0; i<exp.size(); i++ ){
-    Assert(d_conc_to_id[0].find(exp[i]) != d_conc_to_id[0].end());
-    Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";
-  }
-}
-
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
deleted file mode 100644
index d69439ae6..000000000
--- a/src/theory/quantifiers/inst_propagator.h
+++ /dev/null
@@ -1,194 +0,0 @@
-/*********************                                                        */
-/*! \file inst_propagator.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Propagate mechanism for instantiations
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__QUANTIFIERS_INST_PROPAGATOR_H
-#define CVC4__QUANTIFIERS_INST_PROPAGATOR_H
-
-#include <iostream>
-#include <map>
-#include <string>
-#include <vector>
-#include "expr/node.h"
-#include "expr/node_trie.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_util.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class EqualityQueryInstProp : public EqualityQuery {
-private:
-  /** pointer to quantifiers engine */
-  QuantifiersEngine* d_qe;
-public:
-  EqualityQueryInstProp( QuantifiersEngine* qe );
-  ~EqualityQueryInstProp(){};
-  /** reset */
-  bool reset(Theory::Effort e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override {}
-  /** identify */
-  std::string identify() const override { return "EqualityQueryInstProp"; }
-  /** extends engine */
-  bool extendsEngine() override { return true; }
-  /** contains term */
-  bool hasTerm(Node a) override;
-  /** get the representative of the equivalence class of a */
-  Node getRepresentative(Node a) override;
-  /** returns true if a and b are equal in the current context */
-  bool areEqual(Node a, Node b) override;
-  /** returns true is a and b are disequal in the current context */
-  bool areDisequal(Node a, Node b) override;
-  /** get the equality engine associated with this query */
-  eq::EqualityEngine* getEngine() override;
-  /** get the equivalence class of a */
-  void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
-  /** get congruent term */
-  TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
-
- public:
-  /** get the representative of the equivalence class of a, with explanation */
-  Node getRepresentativeExp( Node a, std::vector< Node >& exp );
-  /** returns true if a and b are equal in the current context */
-  bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
-  /** returns true is a and b are disequal in the current context */
-  bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
-  /** get congruent term */
-  TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
-private:
-  /** term index */
- std::map<Node, TNodeTrie> d_uf_func_map_trie;
- /** union find for terms beyond what is stored in equality engine */
- std::map<Node, Node> d_uf;
- std::map<Node, std::vector<Node> > d_uf_exp;
- Node getUfRepresentative(Node a, std::vector<Node>& exp);
- /** disequality list, stores explanations */
- std::map<Node, std::map<Node, std::vector<Node> > > d_diseq_list;
- /** add arg */
- void addArgument(Node n,
-                  std::vector<Node>& args,
-                  std::vector<Node>& watch,
-                  bool is_watch);
- /** register term */
- void registerUfTerm(TNode n);
-
-public:
-  enum {
-    STATUS_CONFLICT,
-    STATUS_MERGED_KNOWN,
-    STATUS_MERGED_UNKNOWN,
-    STATUS_NONE,
-  };
-  /** set equal */
-  int setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason );
-  Node d_true;
-  Node d_false;
-public:
-  //for explanations
-  static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
-  //for watch list
-  static void setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out );
-  static void collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list );
-
-  Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< int, std::map< Node, Node > >& visited,
-                        bool hasPol, bool pol, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& props );
-  bool isPropagateLiteral( Node n );
-};
-
-class InstPropagator : public QuantifiersUtil {
-private:
-  /** pointer to quantifiers engine */
-  QuantifiersEngine* d_qe;
-  /** notify class */
-  class InstantiationNotifyInstPropagator : public InstantiationNotify {
-    InstPropagator& d_ip;
-  public:
-    InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
-    bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
-                             Node q,
-                             Node lem,
-                             std::vector<Node>& terms,
-                             Node body) override
-    {
-      return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
-    }
-    void filterInstantiations() override { d_ip.filterInstantiations(); }
-  };
-  InstantiationNotifyInstPropagator d_notify;
-  /** notify instantiation method */
-  bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
-                           Node q,
-                           Node lem,
-                           std::vector<Node>& terms,
-                           Node body);
-  /** remove instance ids */
-  void filterInstantiations();  
-  /** allocate instantiation */
-  unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body );
-  /** equality query */
-  EqualityQueryInstProp d_qy;
-  class InstInfo {
-  public:
-    bool d_active;
-    Node d_q;
-    Node d_lem;
-    std::vector< Node > d_terms;
-    // the current entailed body
-    Node d_curr;
-    //explanation for current entailed body
-    std::vector< Node > d_curr_exp;
-    void init( Node q, Node lem, std::vector< Node >& terms, Node body );
-  };
-  /** instantiation count/info */
-  unsigned d_icount;
-  std::map< unsigned, InstInfo > d_ii;
-  std::map< Node, unsigned > d_conc_to_id[2];
-  /** are we in conflict */
-  bool d_conflict;
-  /** watch list */
-  std::map< Node, std::map< unsigned, bool > > d_watch_list;
-  /** update list */
-  std::vector< unsigned > d_update_list;
-  /** relevant instances */
-  std::map< unsigned, bool > d_relevant_inst;
-  bool d_has_relevant_inst;
-private:
-  bool update( unsigned id, InstInfo& i, bool firstTime = false );
-  void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
-  void conflict( std::vector< Node >& exp );
-  bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
-  void addRelevantInstances( std::vector< Node >& exp, const char * c );
-  void debugPrintExplanation( std::vector< Node >& exp, const char * c );
-public:
-  InstPropagator( QuantifiersEngine* qe );
-  ~InstPropagator(){}
-  /** reset */
-  bool reset(Theory::Effort e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override {}
-  /** identify */
-  std::string identify() const override { return "InstPropagator"; }
-  /** get the notify mechanism */
-  InstantiationNotify* getInstantiationNotify() { return &d_notify; }
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 11b9bd14b..2b56cff8f 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -81,24 +81,11 @@ bool Instantiate::checkComplete()
   return true;
 }
 
-void Instantiate::addNotify(InstantiationNotify* in)
-{
-  d_inst_notify.push_back(in);
-}
-
 void Instantiate::addRewriter(InstantiationRewriter* ir)
 {
   d_instRewrite.push_back(ir);
 }
 
-void Instantiate::notifyFlushLemmas()
-{
-  for (InstantiationNotify*& in : d_inst_notify)
-  {
-    in->filterInstantiations();
-  }
-}
-
 bool Instantiate::addInstantiation(
     Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts)
 {
@@ -320,23 +307,6 @@ bool Instantiate::addInstantiation(
           orig_body, q[1], maxInstLevel + 1);
     }
   }
-  QuantifiersModule::QEffort elevel = d_qe->getCurrentQEffort();
-  if (elevel > QuantifiersModule::QEFFORT_CONFLICT
-      && elevel < QuantifiersModule::QEFFORT_NONE
-      && !d_inst_notify.empty())
-  {
-    // notify listeners
-    for (InstantiationNotify*& in : d_inst_notify)
-    {
-      if (!in->notifyInstantiation(elevel, q, lem, terms, body))
-      {
-        Trace("inst-add-debug") << "...we are in conflict." << std::endl;
-        d_qe->setConflict();
-        Assert(d_qe->getNumLemmasWaiting() > 0);
-        break;
-      }
-    }
-  }
   if (options::trackInstLemmas())
   {
     if (options::incrementalSolving())
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 4936693d1..cd3993756 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -34,41 +34,6 @@ namespace quantifiers {
 class TermDb;
 class TermUtil;
 
-/** instantiation notify
- *
- * This class is a listener for all instantiations generated with quantifiers.
- * By default, no notify classes are used. For an example of an instantiation
- * notify class, see quantifiers/inst_propagate.h, which has a notify class
- * that recognizes when the set of enqueued instantiations form a conflict.
- */
-class InstantiationNotify
-{
- public:
-  InstantiationNotify() {}
-  virtual ~InstantiationNotify() {}
-  /** notify instantiation
-   *
-   * This is called when an instantiation of quantified formula q is
-   * instantiated by a substitution whose range is terms at quantifier effort
-   * quant_e. Furthermore:
-   *   body is the substituted, preprocessed body of the quantified formula,
-   *   lem is the instantiation lemma ( ~q V body ) after rewriting.
-   */
-  virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
-                                   Node q,
-                                   Node lem,
-                                   std::vector<Node>& terms,
-                                   Node body) = 0;
-  /** filter instantiations
-   *
-   * This is called just before the quantifiers engine flushes its lemmas to the
-   * output channel. During this call, the instantiation notify object may
-   * call, e.g. QuantifiersEngine::getInstantiate()->removeInstantiation
-   * to remove instantiations that should not be sent on the output channel.
-   */
-  virtual void filterInstantiations() = 0;
-};
-
 /** Instantiation rewriter
  *
  * This class is used for cases where instantiation lemmas can be rewritten by
@@ -129,15 +94,7 @@ class Instantiate : public QuantifiersUtil
   /** check incomplete */
   bool checkComplete() override;
 
-  //--------------------------------------notify/rewrite objects
-  /** add instantiation notify
-   *
-   * Adds an instantiation notify class to listen to the instantiations reported
-   * to this class.
-   */
-  void addNotify(InstantiationNotify* in);
-  /** get number of instantiation notify added to this class */
-  bool hasNotify() const { return !d_inst_notify.empty(); }
+  //--------------------------------------rewrite objects
   /** add instantiation rewriter */
   void addRewriter(InstantiationRewriter* ir);
   /** notify flush lemmas
@@ -146,7 +103,7 @@ class Instantiate : public QuantifiersUtil
    * the output channel.
    */
   void notifyFlushLemmas();
-  //--------------------------------------end notify objects
+  //--------------------------------------end rewrite objects
 
   /** do instantiation specified by m
    *
@@ -368,8 +325,6 @@ class Instantiate : public QuantifiersUtil
   TermDb* d_term_db;
   /** cache of term util for quantifiers engine */
   TermUtil* d_term_util;
-  /** instantiation notify classes */
-  std::vector<InstantiationNotify*> d_inst_notify;
   /** instantiation rewriter classes */
   std::vector<InstantiationRewriter*> d_instRewrite;
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1db0937ff..b3ee7ad49 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -24,7 +24,6 @@
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/inst_propagator.h"
 #include "theory/quantifiers/inst_strategy_enumerative.h"
 #include "theory/quantifiers/local_theory_ext.h"
 #include "theory/quantifiers/quant_conflict_find.h"
@@ -45,8 +44,7 @@ class QuantifiersEnginePrivate
 {
  public:
   QuantifiersEnginePrivate()
-      : d_inst_prop(nullptr),
-        d_rel_dom(nullptr),
+      : d_rel_dom(nullptr),
         d_alpha_equiv(nullptr),
         d_inst_engine(nullptr),
         d_model_engine(nullptr),
@@ -63,8 +61,6 @@ class QuantifiersEnginePrivate
   }
   ~QuantifiersEnginePrivate() {}
   //------------------------------ private quantifier utilities
-  /** quantifiers instantiation propagator */
-  std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
   /** relevant domain */
   std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
   //------------------------------ end private quantifier utilities
@@ -218,15 +214,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
 
   if (options::ceGuidedInst()) {
     d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
-  }
-
-  if( options::instPropagate() ){
-    // notice that this option is incompatible with options::qcfAllConflict()
-    d_private->d_inst_prop.reset(new quantifiers::InstPropagator(this));
-    d_util.push_back(d_private->d_inst_prop.get());
-    d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify());
-  }
-  
+  }  
 
   d_util.push_back(d_instantiate.get());
 
@@ -1125,15 +1113,6 @@ options::UserPatMode QuantifiersEngine::getInstUserPatMode()
 
 void QuantifiersEngine::flushLemmas(){
   if( !d_lemmas_waiting.empty() ){
-    //filter based on notify classes
-    if (d_instantiate->hasNotify())
-    {
-      unsigned prev_lem_sz = d_lemmas_waiting.size();
-      d_instantiate->notifyFlushLemmas();
-      if( prev_lem_sz!=d_lemmas_waiting.size() ){
-        Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
-      }
-    }
     //take default output channel if none is provided
     d_hasAddedLemma = true;
     for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
diff --git a/test/regress/regress1/quantifiers/inst-prop-simp.smt2 b/test/regress/regress1/quantifiers/inst-prop-simp.smt2
index 2a713c352..375acc035 100644
--- a/test/regress/regress1/quantifiers/inst-prop-simp.smt2
+++ b/test/regress/regress1/quantifiers/inst-prop-simp.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --inst-prop
-; EXPECT: unsat
 (set-logic UFLIA)
 (set-info :status unsat)