Remove deprecated quantifiers modules (#5820)

9 files changed, 0 insertions, 956 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 53420d395..1f7fc8bac 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -622,8 +622,6 @@ libcvc4_add_sources(
   theory/output_channel.h
   theory/quantifiers/alpha_equivalence.cpp
   theory/quantifiers/alpha_equivalence.h
-  theory/quantifiers/anti_skolem.cpp
-  theory/quantifiers/anti_skolem.h
   theory/quantifiers/bv_inverter.cpp
   theory/quantifiers/bv_inverter.h
   theory/quantifiers/bv_inverter_utils.cpp
@@ -677,8 +675,6 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/trigger_trie.h
   theory/quantifiers/ematching/var_match_generator.cpp
   theory/quantifiers/ematching/var_match_generator.h
-  theory/quantifiers/equality_infer.cpp
-  theory/quantifiers/equality_infer.h
   theory/quantifiers/equality_query.cpp
   theory/quantifiers/equality_query.h
   theory/quantifiers/expr_miner.cpp
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 3499da7de..d3b3502fc 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1829,14 +1829,6 @@ header = "options/quantifiers_options.h"
   name = "agg"
   help = "Aggressively split quantified formulas."
 
-[[option]]
-  name       = "quantAntiSkolem"
-  category   = "regular"
-  long       = "quant-anti-skolem"
-  type       = "bool"
-  default    = "false"
-  help       = "perform anti-skolemization for quantified formulas"
-
 ### Higher-order options
 
 [[option]]
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
deleted file mode 100644
index c91ba419b..000000000
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ /dev/null
@@ -1,305 +0,0 @@
-/*********************                                                        */
-/*! \file anti_skolem.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Implementation of anti-skolemization, e.g.:
- **          ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ]  ) => forall x. exists y. ( P[ y ] ^ Q[ y ] )
- **/
-
-#include "theory/quantifiers/anti_skolem.h"
-
-#include "expr/term_canonize.h"
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers_engine.h"
-
-using namespace std;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-struct sortTypeOrder {
-  expr::TermCanonize* d_tu;
-  bool operator() (TypeNode i, TypeNode j) {
-    return d_tu->getIdForType( i )<d_tu->getIdForType( j );
-  }
-};
-
-void QuantAntiSkolem::SkQuantTypeCache::add( std::vector< TypeNode >& typs, Node q, unsigned index ) {
-  if( index==typs.size() ){
-    Assert(std::find(d_quants.begin(), d_quants.end(), q) == d_quants.end());
-    d_quants.push_back( q );
-  }else{
-    d_children[typs[index]].add( typs, q, index+1 );
-  }
-}
-
-void QuantAntiSkolem::SkQuantTypeCache::sendLemmas( QuantAntiSkolem * ask ) {
-  for( std::map< TypeNode, SkQuantTypeCache >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
-    it->second.sendLemmas( ask );
-  }
-  if( !d_quants.empty() ){
-    ask->sendAntiSkolemizeLemma( d_quants );
-  }
-}
-
-bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Node >& quants, unsigned index ) {
-  if( index==quants.size() ){
-    if( !d_valid.get() ){
-      d_valid.set( true );
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    Node n = quants[index];
-    std::map< Node, CDSkQuantCache* >::iterator it = d_data.find( n );
-    CDSkQuantCache* skc;
-    if( it==d_data.end() ){
-      skc = new CDSkQuantCache( c );
-      d_data[n] = skc;
-    }else{
-      skc = it->second;
-    }
-    return skc->add( c, quants, index+1 );
-  }
-}
-
-QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() {
-  for(std::map< Node, CDSkQuantCache* >::iterator i = d_data.begin(), iend = d_data.end();
-      i != iend; ++i){
-    CDSkQuantCache* current = (*i).second;
-    Assert(current != NULL);
-    delete current;
-  }
-}
-
-QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs)
-    : QuantifiersModule(qs, qe)
-{
-  d_sqc = new CDSkQuantCache(qs.getUserContext());
-}
-
-QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; }
-
-/* Call during quantifier engine's check */
-void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
-{
-  if (quant_e == QEFFORT_STANDARD)
-  {
-    d_sqtc.clear();
-    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( d_quant_processed.find( q )==d_quant_processed.end() ){
-        d_quant_processed[q] = true;
-        Trace("anti-sk") << "Process quantified formula : " << q << std::endl;
-        bool success = false;
-        if( d_quant_sip[q].init( q[1] ) ){
-          Trace("anti-sk") << "- Partitioned to single invocation parts : " << std::endl;
-          d_quant_sip[q].debugPrint( "anti-sk" );
-          //check if it is single invocation
-          if( d_quant_sip[q].isPurelySingleInvocation() ){
-            //for now, only do purely single invocation
-            success = true;
-          }
-        }else{
-          Trace("anti-sk") << "- Failed to initialize." << std::endl;
-        }
-        if( success ){
-          //sort the argument variables
-          std::vector<Node> sivars;
-          d_quant_sip[q].getSingleInvocationVariables(sivars);
-          for (const Node& v : sivars)
-          {
-            d_ask_types[q].push_back(v.getType());
-          }
-          std::map< TypeNode, std::vector< unsigned > > indices;
-          for (unsigned j = 0, size = d_ask_types[q].size(); j < size; j++)
-          {
-            indices[d_ask_types[q][j]].push_back( j );
-          }
-          sortTypeOrder sto;
-          sto.d_tu = d_quantEngine->getTermCanonize();
-          std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto );
-          //increment j on inner loop
-          for( unsigned j=0; j<d_ask_types[q].size();  ){
-            TypeNode curr = d_ask_types[q][j];
-            for( unsigned k=0; k<indices[curr].size(); k++ ){
-              Assert(d_ask_types[q][j] == curr);
-              d_ask_types_index[q].push_back( indices[curr][k] );
-              j++;
-            }
-          }
-          Assert(d_ask_types_index[q].size() == d_ask_types[q].size());
-        }else{
-          d_quant_sip.erase( q );
-        }
-      }
-      //now, activate the quantified formula
-      std::map< Node, std::vector< TypeNode > >::iterator it = d_ask_types.find( q );
-      if( it!=d_ask_types.end() ){
-        d_sqtc.add( it->second, q );        
-      }
-    }
-    Trace("anti-sk-debug") << "Process lemmas..." << std::endl;
-    //send out lemmas for each anti-skolemizable group of quantified formulas
-    d_sqtc.sendLemmas( this );
-    Trace("anti-sk-debug") << "...Finished process lemmas" << std::endl;
-  }
-}
-
-bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) {
-  Assert(!quants.empty());
-  std::sort( quants.begin(), quants.end() );
-  if (d_sqc->add(d_qstate.getUserContext(), quants))
-  {
-    //partition into connected components
-    if( pconnected && quants.size()>1 ){
-      Trace("anti-sk-debug") << "Partition into connected components..." << std::endl;
-      int eqc_count = 0;
-      std::map< Node, int > func_to_eqc;
-      std::map< int, std::vector< Node > > eqc_to_func;
-      std::map< int, std::vector< Node > > eqc_to_quant;
-      for( unsigned i=0; i<quants.size(); i++ ){
-        Node q = quants[i];
-        std::vector< int > eqcs;
-        std::vector<Node> funcs;
-        d_quant_sip[q].getFunctions(funcs);
-        for (const Node& f : funcs)
-        {
-          std::map< Node, int >::iterator itf = func_to_eqc.find( f );
-          if( itf == func_to_eqc.end() ){
-            if( eqcs.empty() ){
-              func_to_eqc[f] = eqc_count;
-              eqc_to_func[eqc_count].push_back( f );
-              eqc_count++;
-            }else{
-              func_to_eqc[f] = eqcs[0];
-              eqc_to_func[eqcs[0]].push_back( f );
-            }
-          }
-          if( std::find( eqcs.begin(), eqcs.end(), func_to_eqc[f] )==eqcs.end() ){
-            eqcs.push_back( func_to_eqc[f] );
-          }
-        }
-        Assert(!eqcs.empty());
-        //merge equivalence classes
-        int id = eqcs[0];
-        eqc_to_quant[id].push_back( q );
-        for( unsigned j=1; j<eqcs.size(); j++ ){
-          int id2 = eqcs[j];
-          std::map< int, std::vector< Node > >::iterator itef = eqc_to_func.find( id2 );
-          if( itef!=eqc_to_func.end() ){
-            for( unsigned k=0; k<itef->second.size(); k++ ){
-              func_to_eqc[itef->second[k]] = id;
-              eqc_to_func[id].push_back( itef->second[k] );
-            }
-            eqc_to_func.erase( id2 );
-          }
-          itef = eqc_to_quant.find( id2 );
-          if( itef!=eqc_to_quant.end() ){
-            eqc_to_quant[id].insert( eqc_to_quant[id].end(), itef->second.begin(), itef->second.end() );
-            eqc_to_quant.erase( id2 );
-          }
-        }
-      }
-      if( eqc_to_quant.size()>1 ){
-        bool addedLemma = false;
-        for( std::map< int, std::vector< Node > >::iterator it = eqc_to_quant.begin(); it != eqc_to_quant.end(); ++it ){
-          Assert(it->second.size() < quants.size());
-          bool ret = sendAntiSkolemizeLemma( it->second, false );
-          addedLemma = addedLemma || ret;
-        }
-        return addedLemma;
-      }
-    }    
-    
-    Trace("anti-sk") << "Anti-skolemize group : " << std::endl;
-    for( unsigned i=0; i<quants.size(); i++ ){
-      Trace("anti-sk") << "   " << quants[i] << std::endl;
-    }
-
-    std::vector< Node > outer_vars;
-    std::vector< Node > inner_vars;
-    Node q0 = quants[0];
-    for (unsigned i = 0, size = d_ask_types[q0].size(); i < size; i++)
-    {
-      Node v = NodeManager::currentNM()->mkBoundVar(d_ask_types[q0][i]);
-      Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl;
-      outer_vars.push_back( v );
-    }
-
-    std::map< Node, Node > func_to_var;
-    std::vector< Node > conj;
-    for( unsigned i=0; i<quants.size(); i++ ){
-      Node q = quants[i];
-      Trace("anti-sk-debug") << "Process " << q << std::endl;
-      std::vector< Node > subs_lhs;
-      std::vector< Node > subs_rhs;
-      //get outer variable substitution
-      Assert(d_ask_types_index[q].size() == d_ask_types[q].size());
-      std::vector<Node> sivars;
-      d_quant_sip[q].getSingleInvocationVariables(sivars);
-      for (unsigned j = 0, size = d_ask_types_index[q].size(); j < size; j++)
-      {
-        Trace("anti-sk-debug")
-            << " o_subs : " << sivars[d_ask_types_index[q][j]] << " -> "
-            << outer_vars[j] << std::endl;
-        subs_lhs.push_back(sivars[d_ask_types_index[q][j]]);
-        subs_rhs.push_back( outer_vars[j] );
-      }
-      //get function substitution
-      std::vector<Node> funcs;
-      d_quant_sip[q].getFunctions(funcs);
-      for (const Node& f : funcs)
-      {
-        Node fv = d_quant_sip[q].getFirstOrderVariableForFunction(f);
-        if( func_to_var.find( f )==func_to_var.end() ){
-          Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() );
-          Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl;
-          inner_vars.push_back( v );
-          func_to_var[f] = v;
-        }
-        subs_lhs.push_back( fv );
-        subs_rhs.push_back( func_to_var[f] );
-        Trace("anti-sk-debug") << " i_subs : " << fv << " -> " << func_to_var[f] << std::endl;
-      }
-      Node c = d_quant_sip[q].getSingleInvocation();
-      if( !subs_lhs.empty() ){
-        c = c.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-      }
-      conj.push_back( c );
-    }
-    Node body = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::AND, conj );
-    if( !inner_vars.empty() ){
-      Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, inner_vars );
-      body = NodeManager::currentNM()->mkNode( kind::EXISTS, bvl, body );
-    }
-    if( !outer_vars.empty() ){
-      Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, outer_vars );
-      body = NodeManager::currentNM()->mkNode( kind::FORALL, bvl, body );
-    }
-    Trace("anti-sk") << "Produced : " << body << std::endl;
-    quants.push_back( body.negate() );
-    Node lem = NodeManager::currentNM()->mkNode( kind::AND, quants ).negate();
-    Trace("anti-sk-lemma") << "Anti-skolemize lemma : " << lem << std::endl;
-    quants.pop_back();
-    return d_quantEngine->addLemma( lem ); 
-  }else{
-    return false;
-  }
-}
-
-}/* namespace CVC4::theory::quantifiers */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
deleted file mode 100644
index 21faa0361..000000000
--- a/src/theory/quantifiers/anti_skolem.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*********************                                                        */
-/*! \file anti_skolem.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 anti-skolemization
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__QUANT_ANTI_SKOLEM_H
-#define CVC4__THEORY__QUANT_ANTI_SKOLEM_H
-
-#include <map>
-#include <vector>
-
-#include "context/cdhashset.h"
-#include "context/cdo.h"
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/single_inv_partition.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class QuantAntiSkolem : public QuantifiersModule {
- public:
-  QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs);
-  virtual ~QuantAntiSkolem();
-
-  bool sendAntiSkolemizeLemma( std::vector< Node >& quants,
-                               bool pconnected = true );
-
-  /* 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 "QuantAntiSkolem"; }
-
- private:
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-
-  std::map< Node, bool > d_quant_processed;
-  std::map< Node, SingleInvocationPartition > d_quant_sip;
-  std::map< Node, std::vector< TypeNode > > d_ask_types;
-  std::map< Node, std::vector< unsigned > > d_ask_types_index;
-  
-  class SkQuantTypeCache {
-  public:
-    std::map< TypeNode, SkQuantTypeCache > d_children;
-    std::vector< Node > d_quants;
-    void add( std::vector< TypeNode >& typs, Node q, unsigned index = 0 );
-    void clear() { 
-      d_children.clear();
-      d_quants.clear(); 
-    }
-    void sendLemmas( QuantAntiSkolem * ask );
-  }; 
-  SkQuantTypeCache d_sqtc;
-  
-  class CDSkQuantCache {
-  public:
-    CDSkQuantCache( context::Context* c ) : d_valid( c, false ){}
-    ~CDSkQuantCache();
-    std::map< Node, CDSkQuantCache* > d_data;
-    context::CDO< bool > d_valid;
-    bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 );
-  };
-  CDSkQuantCache * d_sqc;
-}; /* class QuantAntiSkolem */
-
-}/* namespace CVC4::theory::quantifiers */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
-
-#endif
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
deleted file mode 100644
index 63fecdd9e..000000000
--- a/src/theory/quantifiers/equality_infer.cpp
+++ /dev/null
@@ -1,440 +0,0 @@
-/*********************                                                        */
-/*! \file equality_infer.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Tianyi Liang
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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  Method for inferring equalities between arithmetic equivalence classes, 
- **         inspired by "A generalization of Shostak's method for combining decision procedures" Barrett et al. Figure 1.
- **
- **/
-
-#include "theory/quantifiers/equality_infer.h"
-
-#include "context/context_mm.h"
-#include "theory/rewriter.h"
-#include "theory/arith/arith_msum.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace std;
-
-namespace CVC4 {
-
-EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_solved( c, false ), d_master(c)
-//, d_rep_exp(c), d_uselist(c) 
-{
-
-}
-
-EqualityInference::EqualityInference( context::Context* c, bool trackExp ) : 
-d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), 
-d_rep_to_eqc( c ), d_rep_exp( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){
-  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-  d_true = NodeManager::currentNM()->mkConst( true );
-}
-
-EqualityInference::~EqualityInference(){
-  for( std::map< Node, EqcInfo * >::iterator it = d_eqci.begin(); it != d_eqci.end(); ++it ){
-    delete it->second;
-  }
-}
-
-void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) {
-  if( std::find( exp.begin(), exp.end(), e )==exp.end() ){
-    Trace("eq-infer-debug2") << "......add to explanation " << e << std::endl;
-    exp.push_back( e );
-  }
-}
-
-void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) {
-  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
-  if( re_i!=d_rep_exp.end() ){
-    for( int i=0; i<(*re_i).second; i++ ){
-      addToExplanation( exp, d_rep_exp_data[eqc][i] );
-    }
-  }
-  //for( unsigned i=0; i<d_eqci[n]->d_rep_exp.size(); i++ ){
-  //  addToExplanation( exp, d_eqci[n]->d_rep_exp[i] );
-  //}
-}
-
-void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) {
-  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
-  int n_re = 0;
-  if( re_i != d_rep_exp.end() ){
-    n_re = (*re_i).second;
-  }
-  d_rep_exp[eqc] = n_re + exp_to_add.size();
-  for( unsigned i=0; i<exp_to_add.size(); i++ ){
-    if( n_re<(int)d_rep_exp_data[eqc].size() ){
-      d_rep_exp_data[eqc][n_re] = exp_to_add[i];
-    }else{
-      d_rep_exp_data[eqc].push_back( exp_to_add[i] );
-    }
-    n_re++;
-  }
-  //for( unsigned i=0; i<exp_to_add.size(); i++ ){
-  //  eqci->d_rep_exp.push_back( exp_to_add[i] );
-  //}
-}
-
-Node EqualityInference::getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m ) {
-  if( !eqc->d_master.get().isNull() ){
-    if( eqc->d_master.get()==t ){
-      if( !new_m.isNull() && t!=new_m ){
-        eqc->d_master = new_m;
-        updated = true;
-        return new_m;
-      }else{
-        return t;
-      }
-    }else{
-      Assert(d_eqci.find(eqc->d_master.get()) != d_eqci.end());
-      EqcInfo * eqc_m = d_eqci[eqc->d_master.get()];
-      Node m = getMaster( eqc->d_master.get(), eqc_m, updated, new_m );
-      eqc->d_master = m;
-      return m;
-    }
-  }else{
-    return Node::null();
-  }
-}
-
-//update the internal "master" representative of the equivalence class, return true if the merge was non-redundant
-bool EqualityInference::updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 ) {
-  bool updated = false;
-  Node m1 = getMaster( t1, eqc1, updated );
-  if( m1.isNull() ){
-    eqc1->d_master = t2;
-    if( eqc2->d_master.get().isNull() ){
-      eqc2->d_master = t2;
-    }
-    return true;
-  }else{
-    updated = false;
-    Node m2 = getMaster( t2, eqc2, updated, m1);
-    if( m2.isNull() ){
-      eqc2->d_master = m1;
-      return true;
-    }else{
-      return updated;
-    }
-  }
-}
-
-void EqualityInference::eqNotifyNewClass(TNode t) {
-  if( t.getType().isReal() ){
-    Trace("eq-infer") << "Notify equivalence class : " << t << std::endl;
-    EqcInfo * eqci;
-    std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( t );
-    if( itec==d_eqci.end() ){
-      eqci = new EqcInfo( d_c );
-      d_eqci[t] = eqci;
-    }else{
-      eqci = itec->second;
-    }
-    Assert(!eqci->d_valid.get());
-    if( !eqci->d_solved.get() ){
-      //somewhat strange: t may not be in rewritten form    
-      Node r = Rewriter::rewrite( t );
-      std::map< Node, Node > msum;
-      if (ArithMSum::getMonomialSum(r, msum))
-      {
-        Trace("eq-infer-debug2") << "...process monomial sum, size = " << msum.size() << std::endl;
-        eqci->d_valid = true;
-        bool changed = false;
-        std::vector< Node > exp;
-        std::vector< Node > children;
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
-          Trace("eq-infer-debug2") << "...process child " << it->first << ", " << it->second << std::endl;
-          if( !it->first.isNull() ){
-            Node n = it->first;
-            BoolMap::const_iterator itv = d_elim_vars.find( n );
-            if( itv!=d_elim_vars.end() ){
-              changed = true;
-              Assert(d_eqci.find(n) != d_eqci.end());
-              Assert(n != t);
-              Assert(d_eqci[n]->d_solved.get());
-              Trace("eq-infer-debug2") << "......its solved form is " << d_eqci[n]->d_rep.get() << std::endl;
-              if( d_trackExplain ){
-                //track the explanation: justified by explanation for each substitution
-                addToExplanationEqc( exp, n );
-              }
-              n = d_eqci[n]->d_rep;
-              Assert(!n.isNull());
-            }
-            if( it->second.isNull() ){
-              children.push_back( n );
-            }else{
-              children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) );
-            }
-          }else{
-            Assert(!it->second.isNull());
-            children.push_back( it->second );
-          }
-        }
-        Trace("eq-infer-debug2") << "...children size = " << children.size() << std::endl;
-        bool mvalid = true;
-        if( changed ){
-          r = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
-          Trace("eq-infer-debug2") << "...pre-rewrite : " << r << std::endl;
-          r = Rewriter::rewrite( r );
-          msum.clear();
-          if (!ArithMSum::getMonomialSum(r, msum))
-          {
-            mvalid = false;
-          }
-        }
-        Trace("eq-infer") << "...value is " << r << std::endl;
-        setEqcRep( t, r, exp, eqci );
-        if( mvalid ){
-          for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-            if( !it->first.isNull() ){
-              addToUseList( it->first, t );
-            }
-          }        
-        }
-      }else{
-        eqci->d_valid = false;
-      }
-    }
-  }
-}
-
-void EqualityInference::addToUseList( Node used, Node eqc ) {
-#if 1
-  NodeIntMap::iterator ul_i = d_uselist.find( used );
-  int n_ul = 0;
-  if( ul_i != d_uselist.end() ){
-    n_ul = (*ul_i).second;
-  }
-  d_uselist[ used ] = n_ul + 1;
-  Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
-  if( n_ul<(int)d_uselist_data[used].size() ){
-    d_uselist_data[used][n_ul] = eqc;
-  }else{
-    d_uselist_data[used].push_back( eqc );  
-  }
-#else
-  std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used );
-  EqcInfo * eqci_used;
-  if( itu==d_eqci.end() ){
-    eqci_used = new EqcInfo( d_c );
-    d_eqci[used] = eqci_used;
-  }else{
-    eqci_used = itu->second;
-  }
-  Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
-  eqci_used->d_uselist.push_back( eqc );
-#endif
-}
-
-void EqualityInference::setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ) {
-  eqci->d_rep = r;
-  if( d_trackExplain ){
-    addToExplanationEqc( t, exp_to_add );
-  }
-  //if this is an active equivalence class
-  if( eqci->d_valid.get() ){
-    Trace("eq-infer-debug") << "Set eqc rep " << t << " -> " << r << std::endl;
-    NodeMap::const_iterator itr = d_rep_to_eqc.find( r );
-    if( itr==d_rep_to_eqc.end() ){
-      d_rep_to_eqc[r] = t;
-    }else{
-      //merge two equivalence classes
-      Node t2 = (*itr).second;
-      //check if it is valid
-      std::map< Node, EqcInfo * >::iterator itc = d_eqci.find( t2 );
-      if( itc!=d_eqci.end() && itc->second->d_valid.get() ){
-        //if we haven't already determined they should be merged
-        if( updateMaster( t, t2, eqci, itc->second ) ){
-          Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl;
-          Trace("eq-infer") << "  since they both normalize to : " << r << std::endl;
-          d_pending_merges.push_back( t.eqNode( t2 ) );
-          if( d_trackExplain ){
-            std::vector< Node > exp;
-            for( unsigned j=0; j<2; j++ ){
-              addToExplanationEqc( exp, j==0 ? t : t2 );
-            }
-            Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( AND, exp ) );
-            Trace("eq-infer") << "  explanation : " << exp_n << std::endl;
-            d_pending_merge_exp.push_back( exp_n );
-          }
-        }
-      }
-    }
-  }
-}
-
-void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
-  Assert(!t1.isNull());
-  Assert(!t2.isNull());
-  std::map< Node, EqcInfo * >::iterator itv1 = d_eqci.find( t1 );
-  if( itv1!=d_eqci.end() ){
-    std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 );
-    if( itv2!=d_eqci.end() ){
-      Trace("eq-infer") << "Merge equivalence classes : " << t2 << " into " << t1 << std::endl;
-      Node tr1 = itv1->second->d_rep;
-      Node tr2 = itv2->second->d_rep;
-      itv2->second->d_valid = false;
-      Trace("eq-infer") << "Representatives : " << tr2 << " into " << tr1 << std::endl;
-      if( tr1!=tr2 ){
-        Node eq = tr1.eqNode( tr2 );
-        std::map< Node, Node > msum;
-        if (ArithMSum::getMonomialSumLit(eq, msum))
-        {
-          Node v_solve;
-          //solve for variables with no coefficient
-          if( Trace.isOn("eq-infer-debug2") ){
-            Trace("eq-infer-debug2") << "Monomial sum : " << std::endl;
-            for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
-              Trace("eq-infer-debug2") << "  " << it->first << " * " << it->second << std::endl;
-            }
-          }
-          for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
-            Node n = it->first;
-            if( !n.isNull() ){
-              bool canSolve = false;
-              if( it->second.isNull() ){
-                canSolve = true;
-              }else{
-                //Assert( it->second.isConst() );
-                Rational r = it->second.getConst<Rational>(); 
-                canSolve = r.isOne() || r.isNegativeOne();
-              }
-              if( canSolve ){
-                v_solve = n;
-                break;
-              }
-            }
-          }
-          Trace("eq-infer-debug") << "solve for variable : " << v_solve << std::endl;
-          if( !v_solve.isNull() ){
-            //solve for v_solve
-            Node veq;
-            if (ArithMSum::isolate(v_solve, msum, veq, kind::EQUAL, true) == 1)
-            {
-              Node v_value = veq[1];
-              Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl;
-              Assert(d_elim_vars.find(v_solve) == d_elim_vars.end());
-              d_elim_vars[v_solve] = true;
-              //store value in eqc info
-              EqcInfo * eqci_solved;
-              std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( v_solve );
-              if( itec==d_eqci.end() ){
-                eqci_solved = new EqcInfo( d_c );
-                d_eqci[v_solve] =  eqci_solved;
-              }else{
-                eqci_solved = itec->second;
-              }
-              eqci_solved->d_solved = true;
-              eqci_solved->d_rep = v_value;
-              //track the explanation
-              std::vector< Node > exp;
-              if( d_trackExplain ){
-                //explanation is t1 = t2 + their explanations
-                exp.push_back( t1.eqNode( t2 ) );
-                for( unsigned i=0; i<2; i++ ){
-                  addToExplanationEqc( exp, i==0 ? t1 : t2 );
-                }
-                if( Trace.isOn("eq-infer-debug") ){
-                  Trace("eq-infer-debug") << "      explanation for solving " << v_solve << " is ";
-                  for( unsigned i=0; i<exp.size(); i++ ){
-                    Trace("eq-infer-debug") << exp[i] << " ";
-                  }
-                  Trace("eq-infer-debug") << std::endl;
-                }
-                addToExplanationEqc( v_solve, exp );
-              }
-             
-              std::vector< Node > new_use;
-              for( std::map< Node, Node >::iterator itmm = msum.begin(); itmm != msum.end(); ++itmm ){
-                Node n = itmm->first;
-                if( !n.isNull() && n!=v_solve ){
-                  new_use.push_back( n );
-                  addToUseList( n, v_solve );
-                }
-              }
-              
-              //go through all equivalence classes that may refer to v_solve
-              std::map< Node, bool > processed;
-              processed[v_solve] = true;
-              NodeIntMap::iterator ul_i = d_uselist.find( v_solve );
-              if( ul_i != d_uselist.end() ){
-                int n_ul = (*ul_i).second;
-                Trace("eq-infer-debug") << "      use list size = " << n_ul << std::endl;
-                for( int j=0; j<n_ul; j++ ){
-                  Node r = d_uselist_data[v_solve][j];
-                //Trace("eq-infer-debug") << "      use list size = " << eqci_solved->d_uselist.size() << std::endl;
-                //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){
-                //  Node r = eqci_solved->d_uselist[j];
-                  if( processed.find( r )==processed.end() ){
-                    processed[r] = true;
-                    std::map< Node, EqcInfo * >::iterator itt = d_eqci.find( r );
-                    if( itt!=d_eqci.end() && ( itt->second->d_valid || itt->second->d_solved ) ){
-                      std::map< Node, Node > msum2;
-                      if (ArithMSum::getMonomialSum(itt->second->d_rep.get(),
-                                                    msum2))
-                      {
-                        std::map< Node, Node >::iterator itm = msum2.find( v_solve );
-                        if( itm!=msum2.end() ){
-                          //substitute in solved form
-                          std::map< Node, Node >::iterator itm2 = msum2.find( v_value );
-                          if( itm2 == msum2.end() ){
-                            msum2[v_value] = itm->second;
-                          }else{
-                            msum2[v_value] = NodeManager::currentNM()->mkNode( PLUS, itm2->second.isNull() ? d_one : itm2->second, 
-                                                                                    itm->second.isNull() ? d_one : itm->second );
-                          }
-                          msum2.erase( itm );
-                          Node rr = ArithMSum::mkNode(msum2);
-                          rr = Rewriter::rewrite( rr );
-                          Trace("eq-infer") << "......update " << itt->first << " => " << rr << std::endl;
-                          setEqcRep( itt->first, rr, exp, itt->second );
-                          //update use list
-                          for( unsigned i=0; i<new_use.size(); i++ ){
-                            addToUseList( new_use[i], r );
-                          }
-                        }
-                      }else{
-                        itt->second->d_valid = false;
-                      }
-                    }
-                  }
-                }
-              }
-              Trace("eq-infer") << "...finished solved." << std::endl;
-            }
-          }
-        }
-      }
-    }else{
-      //no information to merge
-    }
-  }else{
-    //carry information (this might happen for non-linear t1 and linear t2?)
-    std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 );
-    if( itv2!=d_eqci.end() ){
-      d_eqci[t1] = d_eqci[t2];
-      d_eqci[t2] = NULL;
-    }
-  }
-}
-
-Node EqualityInference::getPendingMergeExplanation( unsigned i ) { 
-  if( d_trackExplain ){
-    return d_pending_merge_exp[i]; 
-  }else{
-    return d_pending_merges[i];
-  }
-}  
-
-}
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
deleted file mode 100644
index fed458ade..000000000
--- a/src/theory/quantifiers/equality_infer.h
+++ /dev/null
@@ -1,103 +0,0 @@
-/*********************                                                        */
-/*! \file equality_infer.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 additional inference for equalities
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
-#define CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
-
-#include <iostream>
-#include <map>
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "context/cdhashset.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "theory/theory.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class EqualityInference
-{
-  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDList<Node> NodeList;
-  typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap;
-private:
-  context::Context * d_c;
-  Node d_one;
-  Node d_true;
-  class EqcInfo {
-  public:
-    EqcInfo(context::Context* c);
-    ~EqcInfo(){}
-    context::CDO< Node > d_rep;
-    //whether the eqc of this info is a representative and d_rep can been computed successfully
-    context::CDO< bool > d_valid;
-    //whether the eqc of this info is a solved variable
-    context::CDO< bool > d_solved;
-    //master equivalence class (a union find)
-    context::CDO< Node > d_master;
-    //a vector of equalities t1=t2 for which eqNotifyMerge(t1,t2) was called that explains d_rep
-    //NodeList d_rep_exp;
-    //the list of other eqc where this variable may be appear
-    //NodeList d_uselist;
-  };
-
-  /** track explanations */
-  bool d_trackExplain;
-  /** information necessary for equivalence classes */
-  BoolMap d_elim_vars;
-  std::map< Node, EqcInfo * > d_eqci;
-  NodeMap d_rep_to_eqc;
-  NodeIntMap d_rep_exp;
-  std::map< Node, std::vector< Node > > d_rep_exp_data;
-  /** set eqc rep */
-  void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci );
-  /** use list */
-  NodeIntMap d_uselist;
-  std::map< Node, std::vector< Node > > d_uselist_data;
-  void addToUseList( Node used, Node eqc );
-  /** pending merges */
-  NodeList d_pending_merges;
-  NodeList d_pending_merge_exp;
-  /** add to explanation */
-  void addToExplanation( std::vector< Node >& exp, Node e );
-  void addToExplanationEqc( std::vector< Node >& exp, Node eqc );
-  void addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add );
-  /** for setting master/slave */
-  Node getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m = Node::null() );
-  bool updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 );
-public:
-  //second argument is whether explanations should be tracked
-  EqualityInference(context::Context* c, bool trackExp = false);
-  virtual ~EqualityInference();
-  /** input : notification when equality engine is updated */
-  void eqNotifyNewClass(TNode t);
-  void eqNotifyMerge(TNode t1, TNode t2);
-  /** output : inferred equalities */
-  unsigned getNumPendingMerges() { return d_pending_merges.size(); }
-  Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; }  
-  Node getPendingMergeExplanation( unsigned i );
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 3887c583b..b8515df91 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/equality_query.h"
 
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/equality_infer.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index d8b4062fc..719cc3de1 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -33,7 +33,6 @@ QuantifiersModules::QuantifiersModules()
       d_fs(nullptr),
       d_i_cbqi(nullptr),
       d_qsplit(nullptr),
-      d_anti_skolem(nullptr),
       d_sygus_inst(nullptr)
 {
 }
@@ -85,11 +84,6 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
     d_qsplit.reset(new QuantDSplit(qe, qs));
     modules.push_back(d_qsplit.get());
   }
-  if (options::quantAntiSkolem())
-  {
-    d_anti_skolem.reset(new QuantAntiSkolem(qe, qs));
-    modules.push_back(d_anti_skolem.get());
-  }
   if (options::quantAlphaEquiv())
   {
     d_alpha_equiv.reset(new AlphaEquivalence(qe));
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index e83a13ea7..5aa8cf1d5 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
 
 #include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/anti_skolem.h"
 #include "theory/quantifiers/conjecture_generator.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
@@ -81,8 +80,6 @@ class QuantifiersModules
   std::unique_ptr<InstStrategyCegqi> d_i_cbqi;
   /** quantifiers splitting */
   std::unique_ptr<QuantDSplit> d_qsplit;
-  /** quantifiers anti-skolemization */
-  std::unique_ptr<QuantAntiSkolem> d_anti_skolem;
   /** SyGuS instantiation engine */
   std::unique_ptr<SygusInst> d_sygus_inst;
 };