From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Mar 2018 19:13:38 +0000 (-0500)
Subject: Remove unused code (#1700)
X-Git-Tag: cvc5-1.0.0~5217
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f3d010e07f30dd658d4532a43b3813654376162d;p=cvc5.git

Remove unused code (#1700)
---

diff --git a/src/Makefile.am b/src/Makefile.am
index 6395a70bc..53fc3b8bd 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -406,8 +406,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/fmf/model_builder.h \
 	theory/quantifiers/fmf/model_engine.cpp \
 	theory/quantifiers/fmf/model_engine.h \
-	theory/quantifiers/fun_def_engine.cpp \
-	theory/quantifiers/fun_def_engine.h \
 	theory/quantifiers/fun_def_process.cpp \
 	theory/quantifiers/fun_def_process.h \
 	theory/quantifiers/global_negate.cpp \
@@ -430,8 +428,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/quant_conflict_find.h \
 	theory/quantifiers/quant_epr.cpp \
 	theory/quantifiers/quant_epr.h \
-	theory/quantifiers/quant_equality_engine.cpp \
-	theory/quantifiers/quant_equality_engine.h \
 	theory/quantifiers/quant_relevance.cpp \
 	theory/quantifiers/quant_relevance.h \
 	theory/quantifiers/quant_split.cpp \
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index ab74fbc79..1437e9992 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -438,15 +438,6 @@ header = "options/quantifiers_options.h"
   includes   = ["options/quantifiers_modes.h"]
   help       = "selection mode for representatives in quantifiers engine"
 
-[[option]]
-  name       = "instRelevantCond"
-  category   = "regular"
-  long       = "inst-rlv-cond"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "add relevancy conditions for instantiations"
-
 [[option]]
   name       = "fullSaturateQuant"
   category   = "regular"
@@ -1450,17 +1441,6 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "perform anti-skolemization for quantified formulas"
 
-### e-unification options
-
-[[option]]
-  name       = "quantEqualityEngine"
-  category   = "regular"
-  long       = "quant-ee"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "maintain congrunce closure over universal equalities"
-
 ### Higher-order options
 
 [[option]]
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index 34d4eeefc..06f58cca3 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -74,33 +74,6 @@ header = "options/uf_options.h"
   read_only  = true
   help       = "tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
 
-[[option]]
-  name       = "ufssExplainedCliques"
-  category   = "regular"
-  long       = "uf-ss-explained-cliques"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "use explained clique lemmas for uf strong solver"
-
-[[option]]
-  name       = "ufssSimpleCliques"
-  category   = "regular"
-  long       = "uf-ss-simple-cliques"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "always use simple clique lemmas for uf strong solver"
-
-[[option]]
-  name       = "ufssDiseqPropagation"
-  category   = "regular"
-  long       = "uf-ss-deq-prop"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "eagerly propagate disequalities for uf strong solver"
-
 [[option]]
   name       = "ufssMode"
   category   = "regular"
diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp
deleted file mode 100644
index 650a68aa0..000000000
--- a/src/theory/quantifiers/fun_def_engine.cpp
+++ /dev/null
@@ -1,55 +0,0 @@
-/*********************                                                        */
-/*! \file fun_def_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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
- **
- ** This class implements specialized techniques for (recursively) defined functions
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/fun_def_engine.h"
-#include "theory/rewriter.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
-  
-}
-
-/* whether this module needs to check this round */
-bool FunDefEngine::needsCheck( Theory::Effort e ) { 
-  return e>=Theory::EFFORT_LAST_CALL; 
-}
-
-/* reset at a round */
-void FunDefEngine::reset_round( Theory::Effort e ){
-  //TODO
-}
-
-/* Call during quantifier engine's check */
-void FunDefEngine::check(Theory::Effort e, QEffort quant_e)
-{
-  //TODO
-}
-
-/* Called for new quantifiers */
-void FunDefEngine::registerQuantifier( Node q ) {
-  //TODO
-}
-
-/** called for everything that gets asserted */
-void FunDefEngine::assertNode( Node n ) {
-  //TODO
-}
diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h
deleted file mode 100644
index 157eb57fd..000000000
--- a/src/theory/quantifiers/fun_def_engine.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/*********************                                                        */
-/*! \file fun_def_engine.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 Specialized techniques for (recursively) defined functions
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
-#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-//module for handling (recursively) defined functions
-class FunDefEngine : public QuantifiersModule {
-private:
-
-public:
-  FunDefEngine( QuantifiersEngine * qe, context::Context* c );
-  ~FunDefEngine(){}
-
-  /* whether this module needs to check this round */
-  bool needsCheck(Theory::Effort e) override;
-  /* reset at a round */
-  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;
-  /** called for everything that gets asserted */
-  void assertNode(Node n) override;
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const override { return "FunDefEngine"; }
-};
-
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 810ceee4f..323776ddb 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -269,22 +269,6 @@ bool Instantiate::addInstantiation(
   }
 
   Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
-
-  // get relevancy conditions
-  if (options::instRelevantCond())
-  {
-    std::vector<Node> rlv_cond;
-    for (Node& t : terms)
-    {
-      quantifiers::TermUtil::getRelevancyCondition(t, rlv_cond);
-    }
-    if (!rlv_cond.empty())
-    {
-      rlv_cond.push_back(lem);
-      lem = NodeManager::currentNM()->mkNode(kind::OR, rlv_cond);
-    }
-  }
-
   lem = Rewriter::rewrite(lem);
 
   // check for lemma duplication
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
deleted file mode 100644
index 859c4f3ea..000000000
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ /dev/null
@@ -1,219 +0,0 @@
-/*********************                                                        */
-/*! \file quant_equality_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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
- **
- ** Congruence closure with free variables
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/quant_equality_engine.h"
-#include "theory/rewriter.h"
-#include "theory/quantifiers/term_util.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-QuantEqualityEngine::QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ),
-d_notify( *this ),
-d_uequalityEngine(d_notify, c, "theory::quantifiers::QuantEqualityEngine", true),
-d_conflict(c, false),
-d_quant_red(c),
-d_quant_unproc(c){
-  d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
-  d_intType = NodeManager::currentNM()->integerType();
-}
-
-void QuantEqualityEngine::conflict(TNode t1, TNode t2) {
-  //report conflict through quantifiers engine output channel
-  std::vector<TNode> assumptions;
-  d_uequalityEngine.explainEquality(t1, t2, true, assumptions, NULL);
-  Node conflict;
-  if( assumptions.size()==1 ){
-    conflict = assumptions[0];
-  }else{
-    conflict = NodeManager::currentNM()->mkNode( AND, assumptions );
-  }
-  d_conflict = true;
-  Trace("qee-conflict") << "Quantifier equality engine conflict : " << conflict << std::endl;
-  d_quantEngine->getOutputChannel().conflict( conflict );
-}
-
-void QuantEqualityEngine::eqNotifyNewClass(TNode t){
-
-}
-void QuantEqualityEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-
-}
-void QuantEqualityEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-
-}
-void QuantEqualityEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-
-}
-
-/* whether this module needs to check this round */
-bool QuantEqualityEngine::needsCheck( Theory::Effort e ) {
-  return e>=Theory::EFFORT_LAST_CALL;
-}
-
-/* reset at a round */
-void QuantEqualityEngine::reset_round( Theory::Effort e ){
-  //TODO
-}
-
-/* Call during quantifier engine's check */
-void QuantEqualityEngine::check(Theory::Effort e, QEffort quant_e)
-{
-  //TODO
-}
-
-/* Called for new quantifiers */
-void QuantEqualityEngine::registerQuantifier( Node q ) {
-  //TODO
-}
-
-/** called for everything that gets asserted */
-void QuantEqualityEngine::assertNode( Node n ) {
-  Assert( n.getKind()==FORALL );
-  Trace("qee-debug") << "QEE assert : " << n << std::endl;
-  if( !d_conflict ){
-    Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
-    bool pol = n[1].getKind()!=NOT;
-    bool success = true;
-    Node t1;
-    Node t2;
-    if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
-      lit = getTermUtil()->getCanonicalTerm( lit );
-      Trace("qee-debug") << "Canonical :  " << lit << ", pol = " << pol << std::endl;
-      if( lit.getKind()==APPLY_UF ){
-        t1 = getFunctionAppForPredicateApp( lit );
-        t2 = pol ? getTermUtil()->d_one : getTermUtil()->d_zero;
-        pol = true;
-        lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
-      }else if( lit.getKind()==EQUAL ){
-        if( lit[0].getType().isBoolean() ){
-          if( lit[0].getKind()==NOT ){
-            t1 = lit[0][0];
-            pol = !pol;
-          }else{
-            t1 = lit[0];
-          }
-          if( lit[1].getKind()==NOT ){
-            t2 = lit[1][0];
-            pol = !pol;
-          }else{
-            t2 = lit[1];
-          }
-          if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
-            t1 = getFunctionAppForPredicateApp( t1 );
-            t2 = getFunctionAppForPredicateApp( t2 );
-            lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
-          }else{
-            success = false;
-          }
-        }else{
-          t1 = lit[0];
-          t2 = lit[1];
-        }
-      }
-    }else{
-      success = false;
-    }
-    if( success ){
-      bool alreadyHolds = false;
-      if( pol && areUnivEqualInternal( t1, t2 ) ){
-        alreadyHolds = true;
-      }else if( !pol && areUnivDisequalInternal( t1, t2 ) ){
-        alreadyHolds = true;
-      }
-
-      if( alreadyHolds ){
-        d_quant_red.push_back( n );
-        Trace("qee-debug") << "...add to redundant" << std::endl;
-      }else{
-        Trace("qee-debug") << "...assert" << std::endl;
-        Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl;
-        if( lit.getKind()==APPLY_UF ){
-          d_uequalityEngine.assertPredicate(lit, pol, n);
-        }else{
-          d_uequalityEngine.assertEquality(lit, pol, n);
-        }
-      }
-    }else{
-      d_quant_unproc[n] = true;
-      Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
-    }
-  }
-}
-
-bool QuantEqualityEngine::areUnivDisequalInternal( TNode n1, TNode n2 ) {
-  return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
-}
-
-bool QuantEqualityEngine::areUnivEqualInternal( TNode n1, TNode n2 ) {
-  return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
-}
-
-TNode QuantEqualityEngine::getUnivRepresentativeInternal( TNode n ) {
-  if( d_uequalityEngine.hasTerm( n ) ){
-    return d_uequalityEngine.getRepresentative( n );
-  }else{
-    return n;
-  }
-}
-bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
-  //TODO: must convert to internal representation
-  return areUnivDisequalInternal( n1, n2 );
-}
-
-bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
-  //TODO: must convert to internal representation
-  return areUnivEqualInternal( n1, n2 );
-}
-
-TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
-  //TODO: must convert to internal representation
-  return getUnivRepresentativeInternal( n );
-}
-
-Node QuantEqualityEngine::getFunctionForPredicate( Node f ) {
-  std::map< Node, Node >::iterator it = d_pred_to_func.find( f );
-  if( it==d_pred_to_func.end() ){
-    std::vector< TypeNode > argTypes;
-    TypeNode tn = f.getType();
-    for( unsigned i=0; i<(tn.getNumChildren()-1); i++ ){
-      argTypes.push_back( tn[i] );
-    }
-    TypeNode ftn = NodeManager::currentNM()->mkFunctionType( argTypes, d_intType  );
-    std::stringstream ss;
-    ss << "ee_" << f;
-    Node op = NodeManager::currentNM()->mkSkolem( ss.str(), ftn, "op created for internal ee" );
-    d_pred_to_func[f] = op;
-    return op;
-  }else{
-    return it->second;
-  }
-}
-
-Node QuantEqualityEngine::getFunctionAppForPredicateApp( Node n ) {
-  Assert( n.getKind()==APPLY_UF );
-  std::vector< Node > children;
-  children.push_back( getFunctionForPredicate( n.getOperator() ) );
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    children.push_back( n[i] );
-  }
-  return NodeManager::currentNM()->mkNode( APPLY_UF, children );
-}
-
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
deleted file mode 100644
index aa201bbc3..000000000
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ /dev/null
@@ -1,124 +0,0 @@
-/*********************                                                        */
-/*! \file quant_equality_engine.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 Congruence closure with free variables
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
-#define __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class QuantEqualityEngine : public QuantifiersModule {
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-private:
-  //notification class for equality engine
-  class NotifyClass : public eq::EqualityEngineNotify {
-    QuantEqualityEngine& d_qee;
-  public:
-    NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) override
-    {
-      return true;
-    }
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
-    {
-      return true;
-    }
-    bool eqNotifyTriggerTermEquality(TheoryId tag,
-                                     TNode t1,
-                                     TNode t2,
-                                     bool value) override
-    {
-      return true;
-    }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
-    {
-      d_qee.conflict(t1, t2);
-    }
-    void eqNotifyNewClass(TNode t) override { d_qee.eqNotifyNewClass(t); }
-    void eqNotifyPreMerge(TNode t1, TNode t2) override
-    {
-      d_qee.eqNotifyPreMerge(t1, t2);
-    }
-    void eqNotifyPostMerge(TNode t1, TNode t2) override
-    {
-      d_qee.eqNotifyPostMerge(t1, t2);
-    }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
-    {
-      d_qee.eqNotifyDisequal(t1, t2, reason);
-    }
-  };/* class ConjectureGenerator::NotifyClass */
-  /** The notify class */
-  NotifyClass d_notify;
-  /** (universal) equaltity engine */
-  eq::EqualityEngine d_uequalityEngine;
-  /** Are we in conflict */
-  context::CDO<bool> d_conflict;
-  /** list of redundant quantifiers in current context */
-  context::CDList<Node> d_quant_red;
-  /** unprocessed quantifiers in current context */
-  NodeBoolMap d_quant_unproc;
-  // map predicates to functions over int
-  TypeNode d_intType;
-  std::map< Node, Node > d_pred_to_func;
-  Node getFunctionForPredicate( Node f );
-  Node getFunctionAppForPredicateApp( Node n );
-private:
-  void conflict(TNode t1, TNode t2);
-  void eqNotifyNewClass(TNode t);
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-  void eqNotifyPostMerge(TNode t1, TNode t2);
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
-  //queries
-  bool areUnivDisequalInternal( TNode n1, TNode n2 );
-  bool areUnivEqualInternal( TNode n1, TNode n2 );  
-  TNode getUnivRepresentativeInternal( TNode n );
-public:
-  QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
-
-  /* whether this module needs to check this round */
-  bool needsCheck(Theory::Effort e) override;
-  /* reset at a round */
-  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;
-  /** called for everything that gets asserted */
-  void assertNode(Node n) override;
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const override { return "QuantEqualityEngine"; }
-  /** queries */
-  bool areUnivDisequal( TNode n1, TNode n2 );
-  bool areUnivEqual( TNode n1, TNode n2 );
-  TNode getUnivRepresentative( TNode n );
-};
-
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 25e5bbb5f..d1a420e3d 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -16,7 +16,6 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/fun_def_engine.h"
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/term_util.h"
@@ -221,7 +220,6 @@ void QuantAttributes::computeAttributes( Node q ) {
       AlwaysAssert(false);
     }
     d_fun_defs[f] = true;
-    d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
   }
   if( d_qattr[q].d_sygus ){
     if( d_quantEngine->getCegInstantiation()==NULL ){
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index bccf6829c..3b8d03399 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -690,21 +690,6 @@ Node TermUtil::ensureType( Node n, TypeNode tn ) {
   }
 }
 
-void TermUtil::getRelevancyCondition( Node n, std::vector< Node >& cond ) {
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
-    // don't worry about relevancy conditions if using shared selectors
-    if( !options::dtSharedSelectors() ){
-      unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr());
-      const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
-      Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate();
-      if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){
-        cond.push_back( rc );
-      }
-      getRelevancyCondition( n[0], cond );
-    }
-  }
-}
-
 bool TermUtil::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
   if( n==t ){
     return true;
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index bb02b1d6a..8ec2fc8e2 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -249,8 +249,6 @@ public:
   bool containsVtsInfinity( Node n, bool isFree = false );
   /** ensure type */
   static Node ensureType( Node n, TypeNode tn );
-  /** get relevancy condition */
-  static void getRelevancyCondition( Node n, std::vector< Node >& cond );
   
 //general utilities
   // TODO #1216 : promote these?
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index be0cf9fc9..b5f179822 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,7 +30,6 @@
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
-#include "theory/quantifiers/fun_def_engine.h"
 #include "theory/quantifiers/inst_propagator.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
@@ -41,7 +40,6 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_epr.h"
-#include "theory/quantifiers/quant_equality_engine.h"
 #include "theory/quantifiers/quant_relevance.h"
 #include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -162,8 +160,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_ceg_inst = NULL;
   d_lte_part_inst = NULL;
   d_alpha_equiv = NULL;
-  d_fun_def_engine = NULL;
-  d_uee = NULL;
   d_fs = NULL;
   d_rel_dom = NULL;
   d_bv_invert = NULL;
@@ -234,14 +230,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   if( options::quantAlphaEquiv() ){
     d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
   }
-  //if( options::funDefs() ){
-  //  d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
-  //  d_modules.push_back( d_fun_def_engine );
-  //}
-  if( options::quantEqualityEngine() ){
-    d_uee = new quantifiers::QuantEqualityEngine( this, c );
-    d_modules.push_back( d_uee );
-  }
   //full saturation : instantiate from relevant domain, then arbitrary terms
   if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
     d_fs = new quantifiers::InstStrategyEnum(this);
@@ -299,8 +287,6 @@ QuantifiersEngine::~QuantifiersEngine()
   delete d_sg_gen;
   delete d_ceg_inst;
   delete d_lte_part_inst;
-  delete d_fun_def_engine;
-  delete d_uee;
   delete d_fs;
   delete d_i_cbqi;
   delete d_qsplit;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 3fb250d4a..e031bb64b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -70,8 +70,6 @@ namespace quantifiers {
   class CegInstantiation;
   class LtePartialInst;
   class AlphaEquivalence;
-  class FunDefEngine;
-  class QuantEqualityEngine;
   class InstStrategyEnum;
   class InstStrategyCbqi;
   class InstStrategyCegqi;
@@ -151,10 +149,6 @@ private:
   quantifiers::CegInstantiation * d_ceg_inst;
   /** lte partial instantiation */
   quantifiers::LtePartialInst * d_lte_part_inst;
-  /** function definitions engine */
-  quantifiers::FunDefEngine * d_fun_def_engine;
-  /** quantifiers equality engine */
-  quantifiers::QuantEqualityEngine * d_uee;
   /** full saturation */
   quantifiers::InstStrategyEnum* d_fs;
   /** counterexample-based quantifier instantiation */
@@ -251,10 +245,6 @@ public:
   quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
   /** local theory ext partial inst */
   quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
-  /** function definition engine */
-  quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
-  /** quantifiers equality engine */
-  quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
   /** get full saturation */
   quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; }
   /** get inst strategy cbqi */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b5a4370d4..8827959ea 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4103,164 +4103,6 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
   }
 }
 
-Node TheoryStrings::normalizeRegexp(Node r) {
-  if (d_nf_regexps.find(r) != d_nf_regexps.end()) {
-    return d_nf_regexps[r];
-  }
-  Assert(d_nf_regexps.count(r) == 0);
-  Node nf_r = r;
-  std::vector<Node> nf_exp;
-  if (!d_regexp_opr.checkConstRegExp(r)) {
-    switch (r.getKind()) {
-      case kind::REGEXP_EMPTY:
-      case kind::REGEXP_SIGMA: {
-        break;
-      }
-      case kind::STRING_TO_REGEXP: {
-        if (!r[0].isConst() &&
-            d_normal_forms.find(r[0]) != d_normal_forms.end()) {
-          nf_r = mkConcat(d_normal_forms[r[0]]);
-          Debug("regexp-nf")
-              << "Term: " << r[0] << " has a normal form " << nf_r << std::endl;
-          const std::vector<Node>& r0_exp = d_normal_forms_exp[r[0]];
-          nf_exp.insert(nf_exp.end(), r0_exp.begin(), r0_exp.end());
-          nf_r = Rewriter::rewrite(
-              NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r));
-       }
-        break;
-      }
-      case kind::REGEXP_CONCAT:
-      case kind::REGEXP_UNION:
-      case kind::REGEXP_INTER: {
-        bool flag = false;
-        std::vector<Node> vec_nodes;
-        for (unsigned i = 0; i < r.getNumChildren(); ++i) {
-          Node rtmp = normalizeRegexp(r[i]);
-          vec_nodes.push_back(rtmp);
-          if (rtmp != r[i]) {
-            flag = true;
-          }
-        }
-        if (flag) {
-          Node rtmp = vec_nodes.size() == 1 ? vec_nodes[0]
-                                            : NodeManager::currentNM()->mkNode(
-                                                  r.getKind(), vec_nodes);
-          nf_r = Rewriter::rewrite(rtmp);
-        }
-        break;
-      }
-      case kind::REGEXP_STAR: {
-        Node rtmp = normalizeRegexp(r[0]);
-        if (rtmp != r[0]) {
-          rtmp = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, rtmp);
-          nf_r = Rewriter::rewrite(rtmp);
-        }
-        break;
-      }
-      default: { Unreachable(); }
-    }
-  }
-  d_nf_regexps[r] = nf_r;
-  d_nf_regexps_exp[r] = nf_exp;
-  return nf_r;
-}
-
-bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps) {
-  std::map< Node, std::vector< Node > > unprocessed_x_exps;
-  std::map< Node, std::vector< Node > > unprocessed_memberships;
-  std::map< Node, std::vector< Node > > unprocessed_memberships_bases;
-  bool addLemma = false;
-
-  Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl;
-
-  for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){
-    Node x = (*itr_xr).first;
-    Node nf_x = x;
-    std::vector< Node > nf_x_exp;
-    if(d_normal_forms.find( x ) != d_normal_forms.end()) {
-      //nf_x = mkConcat( d_normal_forms[x] );
-      nf_x_exp.insert(nf_x_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end());
-      //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl;
-    } else {
-      Assert(false);
-    }
-    Trace("regexp-nf") << "Checking Memberships for N(" << x << ") = " << nf_x << " :" << std::endl;
-
-    std::vector< Node > vec_x;
-    std::vector< Node > vec_r;
-    unsigned n_pmem = (*itr_xr).second;
-    Assert( getNumMemberships( x, true )==n_pmem );
-    for( unsigned k=0; k<n_pmem; k++ ){
-      Node r = getMembership( x, true, k );
-      Node nf_r = normalizeRegexp( r );  //AJR: fixed (was normalizing mem #0 always)
-      Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r);
-      if(d_processed_memberships.find(memb) == d_processed_memberships.end()) {
-        if(d_regexp_opr.checkConstRegExp(nf_r)) {
-          vec_x.push_back(x);
-          vec_r.push_back(r);
-        } else {
-          Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r << ") = " << nf_r << std::endl;
-          //TODO: handle symbolic ones
-          addLemma = true;
-        }
-        d_processed_memberships.insert(memb);
-      }
-    }
-    if(!vec_x.empty()) {
-      if(unprocessed_x_exps.find(nf_x) == unprocessed_x_exps.end()) {
-        unprocessed_x_exps[nf_x] = nf_x_exp;
-        unprocessed_memberships[nf_x] = vec_r;
-        unprocessed_memberships_bases[nf_x] = vec_x;
-      } else {
-        unprocessed_x_exps[nf_x].insert(unprocessed_x_exps[nf_x].end(), nf_x_exp.begin(), nf_x_exp.end());
-        unprocessed_memberships[nf_x].insert(unprocessed_memberships[nf_x].end(), vec_r.begin(), vec_r.end());
-        unprocessed_memberships_bases[nf_x].insert(unprocessed_memberships_bases[nf_x].end(), vec_x.begin(), vec_x.end());
-      }
-    }
-  }
-  //Intersection
-  for(std::map< Node, std::vector< Node > >::const_iterator itr = unprocessed_memberships.begin();
-      itr != unprocessed_memberships.end(); ++itr) {
-    Node nf_x = itr->first;
-    std::vector< Node > exp( unprocessed_x_exps[nf_x] );
-    Node r = itr->second[0];
-    //get nf_r
-    Node inter_r = d_nf_regexps[r];
-    exp.insert(exp.end(), d_nf_regexps_exp[r].begin(), d_nf_regexps_exp[r].end());
-    Node x = unprocessed_memberships_bases[itr->first][0];
-    Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r);
-    exp.push_back(memb);
-    for(std::size_t i=1; i < itr->second.size(); i++) {
-      //exps
-      Node r2 = itr->second[i];
-      Node inter_r2 = d_nf_regexps[r2];
-      exp.insert(exp.end(), d_nf_regexps_exp[r2].begin(), d_nf_regexps_exp[r2].end());
-      Node x2 = unprocessed_memberships_bases[itr->first][i];
-      memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x2, r2);
-      exp.push_back(memb);
-      //intersection
-      bool spflag = false;
-      inter_r = d_regexp_opr.intersect(inter_r, inter_r2, spflag);
-      if(inter_r == d_emptyRegexp) {
-        //conflict
-        Node conc;
-        sendInference( d_empty_vec, exp, conc, "INTERSECT CONFLICT", true );
-        addLemma = true;
-        break;
-      }
-    }
-    //infer
-    if(!d_conflict) {
-      memb = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, inter_r) );
-      memb_with_exps[memb] = exp;
-    } else {
-      break;
-    }
-  }
-
-  return addLemma;
-}
-
 bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) {
   Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl;
   Assert( d_regexp_opr.checkConstRegExp(r) );
@@ -4312,107 +4154,6 @@ bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_e
   }
 }
 
-bool TheoryStrings::checkMembershipsWithoutLength(
-  std::map< Node, std::vector< Node > > &memb_with_exps,
-  std::map< Node, std::vector< Node > > &XinR_with_exps) {
-  for(std::map< Node, std::vector< Node > >::iterator itr = memb_with_exps.begin(); itr != memb_with_exps.end(); ++itr) {
-    Node memb = itr->first;
-    Node s = memb[0];
-    Node r = memb[1];
-    if(s.isConst()) {
-      memb = Rewriter::rewrite( memb );
-      if(memb == d_false) {
-        Node conc;
-        sendInference(d_empty_vec, itr->second, conc, "MEMBERSHIP CONFLICT", true);
-        //addLemma = true;
-        return true;
-      } else {
-        Assert(memb == d_true);
-      }
-    } else if(s.getKind() == kind::VARIABLE) {
-      //add to XinR
-      XinR_with_exps[itr->first] = itr->second;
-    } else {
-      Assert(s.getKind() == kind::STRING_CONCAT);
-      Node conc;
-      for( unsigned i=0; i<s.getNumChildren(); i++ ) {
-        if(s[i].isConst()) {
-          CVC4::String str( s[0].getConst< String >() );
-          //R-Consume, see Tianyi's thesis
-          if(!applyRConsume(str, r)) {
-            sendInference(d_empty_vec, itr->second, conc, "R-Consume CONFLICT", true);
-            //addLemma = true;
-            return true;
-          }
-        } else {
-          //R-Split, see Tianyi's thesis
-          if(i == s.getNumChildren() - 1) {
-            //add to XinR
-            Node memb2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s[i], r);
-            XinR_with_exps[itr->first] = itr->second;
-          } else {
-            Node s1 = s[i];
-            std::vector< Node > vec_s2;
-            for( unsigned j=i+1; j<s.getNumChildren(); j++ ) {
-              vec_s2.push_back(s[j]);
-            }
-            Node s2 = mkConcat(vec_s2);
-            conc = applyRSplit(s1, s2, r);
-            if(conc == d_true) {
-              break;
-            } else if(conc.isNull() || conc == d_false) {
-              conc = Node::null();
-              sendInference(d_empty_vec, itr->second, conc, "R-Split Conflict", true);
-              //addLemma = true;
-              return true;
-            } else {
-              sendInference(d_empty_vec, itr->second, conc, "R-Split", true);
-              //addLemma = true;
-              return true;
-            }
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
-bool TheoryStrings::checkMemberships2() {
-  bool addedLemma = false;
-  d_nf_regexps.clear();
-  d_nf_regexps_exp.clear();
-  std::map< Node, std::vector< Node > > memb_with_exps;
-  std::map< Node, std::vector< Node > > XinR_with_exps;
-
-  addedLemma = normalizePosMemberships( memb_with_exps );
-  if(!d_conflict) {
-    // main procedure
-    addedLemma |= checkMembershipsWithoutLength( memb_with_exps, XinR_with_exps );
-    //TODO: check addlemma
-    if (!addedLemma && !d_conflict) {
-      for(std::map< Node, std::vector< Node > >::const_iterator itr = XinR_with_exps.begin();
-          itr != XinR_with_exps.end(); ++itr) {
-        std::vector<Node> vec_or;
-        d_regexp_opr.disjunctRegExp( itr->first, vec_or );
-        Node tmp = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_or);
-        Trace("regexp-process") << "Got r: " << itr->first << " to " << tmp << std::endl;
-        /*
-        if(r.getKind() == kind::REGEXP_STAR) {
-          //TODO: apply R-Len
-          addedLemma = applyRLen(XinR_with_exps);
-        } else {
-          //TODO: split
-        }
-        */ 
-      }
-      Assert(false); //TODO:tmp
-    }
-  }
-
-  return addedLemma;
-}
-
 void TheoryStrings::checkMemberships() {
   //add the memberships
   std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP);
@@ -4585,146 +4326,50 @@ void TheoryStrings::checkMemberships() {
           Node xr = getRepresentative( x );
           //Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
           //Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
-          //TODO
-          if( true || r.getKind()!=kind::REGEXP_STAR || ( d_normal_forms[xr].size()==1 && x.getKind()!=kind::STRING_CONCAT ) ){
-            Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr << std::endl;
-            //if so, do simple unrolling
-            std::vector< Node > nvec;
-
-            /*if(xr.isConst()) {
-              Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r) );
-              if(tmp==d_true || tmp==d_false) {
-                if(!polarity) {
-                  tmp = tmp==d_true? d_false : d_true;
-                }
-                nvec.push_back( tmp );
-              }
-            }*/
-
-            if(nvec.empty()) {
-              d_regexp_opr.simplify(atom, nvec, polarity);
-            }
-            Node antec = assertion;
-            if(d_regexp_ant.find(assertion) != d_regexp_ant.end()) {
-              antec = d_regexp_ant[assertion];
-              for(std::vector< Node >::const_iterator itr=nvec.begin(); itr<nvec.end(); itr++) {
-                if(itr->getKind() == kind::STRING_IN_REGEXP) {
-                  if(d_regexp_ant.find( *itr ) == d_regexp_ant.end()) {
-                    d_regexp_ant[ *itr ] = antec;
-                  }
+          Trace("strings-regexp")
+              << "Unroll/simplify membership of atomic term " << xr
+              << std::endl;
+          // if so, do simple unrolling
+          std::vector<Node> nvec;
+
+          if (nvec.empty())
+          {
+            d_regexp_opr.simplify(atom, nvec, polarity);
+          }
+          Node antec = assertion;
+          if (d_regexp_ant.find(assertion) != d_regexp_ant.end())
+          {
+            antec = d_regexp_ant[assertion];
+            for (std::vector<Node>::const_iterator itr = nvec.begin();
+                 itr < nvec.end();
+                 itr++)
+            {
+              if (itr->getKind() == kind::STRING_IN_REGEXP)
+              {
+                if (d_regexp_ant.find(*itr) == d_regexp_ant.end())
+                {
+                  d_regexp_ant[*itr] = antec;
                 }
               }
             }
-            antec = NodeManager::currentNM()->mkNode(kind::AND, antec, mkExplain(rnfexp));
-            Node conc = nvec.size()==1 ? nvec[0] : NodeManager::currentNM()->mkNode(kind::AND, nvec);
-            conc = Rewriter::rewrite(conc);
-            sendLemma( antec, conc, "REGEXP_Unfold" );
-            addedLemma = true;
-            if(changed) {
-              cprocessed.push_back( assertion );
-            } else {
-              processed.push_back( assertion );
-            }
-            //d_regexp_ucached[assertion] = true;
-          }else{
-            Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr << " = ";
-            for( unsigned j=0; j<d_normal_forms[xr].size(); j++ ){
-              Trace("strings-regexp") << d_normal_forms[xr][j] << " ";
-            }
-            Trace("strings-regexp") << ", polarity = " << polarity << std::endl;
-            //otherwise, distribute unrolling over parts
-            Node p1;
-            Node p2;
-            if( d_normal_forms[xr].size()>1 ){
-              p1 = d_normal_forms[xr][0];
-              std::vector< Node > cc;
-              cc.insert( cc.begin(), d_normal_forms[xr].begin() + 1, d_normal_forms[xr].end() );
-              p2 = mkConcat( cc );
-            }
-
-            Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl;
-            std::vector< Node > antec;
-            std::vector< Node > antecn;
-            antec.insert( antec.begin(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
-            if( x!=xr ){
-              antec.push_back( x.eqNode( xr ) );
-            }
-            antecn.push_back( assertion );
-            Node ant = mkExplain( antec, antecn );
-            Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl;
-            Node conc;
-            if( polarity ){
-              if( d_normal_forms[xr].size()==0 ){
-                conc = d_true;
-              }else if( d_normal_forms[xr].size()==1 ){
-                Trace("strings-regexp-debug") << "Case 1\n";
-                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r);
-              }else{
-                Trace("strings-regexp-debug") << "Case 2\n";
-                std::vector< Node > conc_c;
-                Node s11 = mkSkolemS( "s11" );
-                Node s12 = mkSkolemS( "s12" );
-                Node s21 = mkSkolemS( "s21" );
-                Node s22 = mkSkolemS( "s22" );
-                conc = p1.eqNode( mkConcat(s11, s12) );
-                conc_c.push_back(conc);
-                conc = p2.eqNode( mkConcat(s21, s22) );
-                conc_c.push_back(conc);
-                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r);
-                conc_c.push_back(conc);
-                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP,  mkConcat(s12, s21), r[0]);
-                conc_c.push_back(conc);
-                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r);
-                conc_c.push_back(conc);
-                conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc_c));
-                Node eqz = Rewriter::rewrite(x.eqNode(d_emptyString));
-                conc = NodeManager::currentNM()->mkNode(kind::OR, eqz, conc);
-                d_pending_req_phase[eqz] = true;
-              }
-            }else{
-              if( d_normal_forms[xr].size()==0 ){
-                conc = d_false;
-              }else if( d_normal_forms[xr].size()==1 ){
-                Trace("strings-regexp-debug") << "Case 3\n";
-                conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r).negate();
-              }else{
-                Trace("strings-regexp-debug") << "Case 4\n";
-                Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p1);
-                Node len2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p2);
-                Node bi = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-                Node bj = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-                Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, bi, bj);
-                Node g1 = NodeManager::currentNM()->mkNode(kind::AND,
-                      NodeManager::currentNM()->mkNode(kind::GEQ, bi, d_zero),
-                      NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
-                      NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
-                      NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
-                Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, d_zero, bi);
-                Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
-                Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, d_zero, bj);
-                Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
-                Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
-                Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP,  mkConcat(s12, s21), r[0]).negate();
-                Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
-                conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
-                conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
-                conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
-                conc = NodeManager::currentNM()->mkNode(kind::AND, x.eqNode(d_emptyString).negate(), conc);
-              }
-            }
-            if( conc!=d_true ){
-              ant = mkRegExpAntec(assertion, ant);
-              sendLemma(ant, conc, "REGEXP CSTAR");
-              addedLemma = true;
-              if( conc==d_false ){
-                d_regexp_ccached.insert( assertion );
-              }else{
-                cprocessed.push_back( assertion );
-              }
-            }else{
-              d_regexp_ccached.insert(assertion);
-            }
           }
+          antec = NodeManager::currentNM()->mkNode(
+              kind::AND, antec, mkExplain(rnfexp));
+          Node conc = nvec.size() == 1
+                          ? nvec[0]
+                          : NodeManager::currentNM()->mkNode(kind::AND, nvec);
+          conc = Rewriter::rewrite(conc);
+          sendLemma(antec, conc, "REGEXP_Unfold");
+          addedLemma = true;
+          if (changed)
+          {
+            cprocessed.push_back(assertion);
+          }
+          else
+          {
+            processed.push_back(assertion);
+          }
+          // d_regexp_ucached[assertion] = true;
         }
       }
       if(d_conflict) {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 2dcb3ebc8..cff49ccb8 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -398,15 +398,10 @@ private:
 
   //check membership constraints
   Node mkRegExpAntec(Node atom, Node ant);
-  Node normalizeRegexp(Node r);
-  bool normalizePosMemberships( std::map< Node, std::vector< Node > > &memb_with_exps );
   bool applyRConsume( CVC4::String &s, Node &r );
   Node applyRSplit( Node s1, Node s2, Node r );
   bool applyRLen( std::map< Node, std::vector< Node > > &XinR_with_exps );
-  bool checkMembershipsWithoutLength( std::map< Node, std::vector< Node > > &memb_with_exps, 
-                                      std::map< Node, std::vector< Node > > &XinR_with_exps);
   void checkMemberships();
-  bool checkMemberships2();
   bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp);
   //check contains
   void checkPosContains( std::vector< Node >& posContains );
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index eb9e5e987..b32a50eb4 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -144,10 +144,6 @@ void Region::setEqual( Node a, Node b ){
         if( !isDisequal( a, n, t ) ){
           setDisequal( a, n, t, true );
           nr->setDisequal( n, a, t, true );
-          //notify the disequality propagator
-          if( options::ufssDiseqPropagation() ){
-            d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null());
-          }
           if( options::ufssSymBreak() ){
             d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
           }
@@ -614,10 +610,6 @@ void SortModel::merge( Node a, Node b ){
       d_reps = d_reps - 1;
 
       if( !d_conflict ){
-        if( options::ufssDiseqPropagation() ){
-          //notify the disequality propagator
-          d_thss->getDisequalityPropagator()->merge(a, b);
-        }
         if( options::ufssSymBreak() ){
           d_thss->getSymmetryBreaker()->merge(a, b);
         }
@@ -669,10 +661,6 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){
         }
 
         if( !d_conflict ){
-          if( options::ufssDiseqPropagation() ){
-            //notify the disequality propagator
-            d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null());
-          }
           if( options::ufssSymBreak() ){
             d_thss->getSymmetryBreaker()->assertDisequal(a, b);
           }
@@ -1284,144 +1272,21 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out
     clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
     addClique( d_cardinality, clique_vec );
   }
-  if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){
-    //add as lemma
-    std::vector< Node > eqs;
-    for( int i=0; i<(int)clique.size(); i++ ){
-      for( int j=0; j<i; j++ ){
-        Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[i]);
-        Node r2 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[j]);
-        eqs.push_back( clique[i].eqNode( clique[j] ) );
-      }
-    }
-    eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
-    Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
-    if( doSendLemma( lem ) ){
-      Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
-      ++( d_thss->d_statistics.d_clique_lemmas );
-    }
-  }else{
-    //found a clique
-    Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
-    Debug("uf-ss-cliques") << "   ";
-    for( int i=0; i<(int)clique.size(); i++ ){
-      Debug("uf-ss-cliques") << clique[i] << " ";
-    }
-    Debug("uf-ss-cliques") << std::endl;
-    Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
-
-    //we will scan through each of the disequaltities
-    bool isSatConflict = true;
-    std::vector< Node > conflict;
-    //collect disequalities, and nodes that must be equal within representatives
-    std::map< Node, std::map< Node, bool > > explained;
-    std::map< Node, std::map< Node, bool > > nodesWithinRep;
-    //map from the reprorted clique members to those reported in the lemma
-    std::map< Node, Node > cliqueRepMap;
-    for( int i=0; i<(int)d_disequalities_index; i++ ){
-      //if both sides of disequality exist in clique
-      Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
-      Node r2 = d_thss->getTheory()->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
-      if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
-          std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
-          std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
-        explained[r1][r2] = true;
-        explained[r2][r1] = true;
-        if( options::ufssExplainedCliques() ){
-          conflict.push_back( d_disequalities[i] );
-          Debug("uf-ss-cliques") << "   -> disequality : " << d_disequalities[i] << std::endl;
-          nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
-          nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
-        }else{
-          //get the terms we report in the lemma
-          Node ru1 = r1;
-          if( cliqueRepMap.find( r1 )==cliqueRepMap.end() ){
-            ru1 = d_disequalities[i][0][0];
-            cliqueRepMap[r1] = ru1;
-          }else{
-            ru1 = cliqueRepMap[r1];
-          }
-          Node ru2 = r2;
-          if( cliqueRepMap.find( r2 )==cliqueRepMap.end() ){
-            ru2 = d_disequalities[i][0][1];
-            cliqueRepMap[r2] = ru2;
-          }else{
-            ru2 = cliqueRepMap[r2];
-          }
-          if( ru1!=d_disequalities[i][0][0] || ru2!=d_disequalities[i][0][1] ){
-            //disequalities have endpoints that are not connected within an equivalence class
-            // we will be producing a lemma, introducing a new literal ru1 != ru2
-            conflict.push_back( ru1.eqNode( ru2 ).notNode() );
-            isSatConflict = false;
-          }else{
-            conflict.push_back( d_disequalities[i] );
-          }
-        }
-        if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
-          break;
-        }
-      }
+  // add as lemma
+  std::vector<Node> eqs;
+  for (unsigned i = 0, size = clique.size(); i < size; i++)
+  {
+    for (unsigned j = 0; j < i; j++)
+    {
+      eqs.push_back(clique[i].eqNode(clique[j]));
     }
-    if( options::ufssExplainedCliques() ){
-      //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
-      Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
-      //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
-      Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
-      //now, we must explain equalities within each equivalence class
-      for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
-        if( it->second.size()>1 ){
-          Node prev;
-          //add explanation of t1 = t2 = ... = tn
-          Debug("uf-ss-cliques") << "Explain ";
-          for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-            if( prev!=Node::null() ){
-              Debug("uf-ss-cliques") << " = ";
-              //explain it2->first and prev
-              std::vector< TNode > expl;
-              d_thss->getTheory()->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
-              for( int i=0; i<(int)expl.size(); i++ ){
-                if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
-                  conflict.push_back( expl[i] );
-                }
-              }
-            }
-            prev = it2->first;
-            Debug("uf-ss-cliques") << prev;
-          }
-          Debug("uf-ss-cliques") << std::endl;
-        }
-      }
-      Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
-      for( int i=0; i<(int)conflict.size(); i++ ){
-        Debug("uf-ss-cliques") << conflict[i] << " ";
-      }
-      Debug("uf-ss-cliques") << std::endl;
-    }
-    //now, make the conflict
-    if( isSatConflict ){
-      conflict.push_back( d_cardinality_literal[ d_cardinality ] );
-      Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
-      Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
-      //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
-      out->conflict( conflictNode );
-      d_conflict = true;
-      ++( d_thss->d_statistics.d_clique_conflicts );
-    }else{
-      Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
-      //add cardinality constraint
-      Node cardNode = d_cardinality_literal[ d_cardinality ];
-      //bool value;
-      //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
-      //Assert( hasValue );
-      //Assert( value );
-      conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
-      if( doSendLemma( conflictNode ) ){
-        Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
-        ++( d_thss->d_statistics.d_clique_lemmas );
-      }
-    }
-
-    //DO_THIS: ensure that the same clique is not reported???  Check standard effort after assertDisequal can produce same clique.
+  }
+  eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
+  Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
+  if (doSendLemma(lem))
+  {
+    Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
+    ++(d_thss->d_statistics.d_clique_lemmas);
   }
 }
 
@@ -1653,11 +1518,7 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
       d_card_assertions_eqv_lemma(u),
       d_min_pos_tn_master_card(c, -1),
       d_rel_eqc(c),
-      d_deq_prop(NULL),
       d_sym_break(NULL) {
-  if (options::ufssDiseqPropagation()) {
-    d_deq_prop = new DisequalityPropagator(th->getQuantifiersEngine(), this);
-  }
   if (options::ufssSymBreak()) {
     d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c);
   }
@@ -1671,9 +1532,6 @@ StrongSolverTheoryUF::~StrongSolverTheoryUF() {
   if (d_sym_break) {
     delete d_sym_break;
   }
-  if (d_deq_prop) {
-    delete d_deq_prop;
-  }
 }
 
 SortInference* StrongSolverTheoryUF::getSortInference() {
@@ -1758,10 +1616,6 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
     c->merge( a, b );
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
 #endif
-  }else{
-    if( options::ufssDiseqPropagation() ){
-      d_deq_prop->merge(a, b);
-    }
   }
 }
 
@@ -1778,10 +1632,6 @@ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
     //Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
     c->assertDisequal( a, b, reason );
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl;
-  }else{
-    if( options::ufssDiseqPropagation() ){
-      d_deq_prop->assertDisequal(a, b, reason);
-    }
   }
 }
 
@@ -1894,12 +1744,6 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
           }
         }
       }
-      if( lit.getKind()!=EQUAL ){
-        //it is a predicate
-        if( options::ufssDiseqPropagation() ){
-          d_deq_prop->assertPredicate(lit, polarity);
-        }
-      }
     }
   }else{
     if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
@@ -2303,79 +2147,6 @@ StrongSolverTheoryUF::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
 }
 
-
-DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe,
-                                             StrongSolverTheoryUF* ufss)
-  : d_qe(qe), d_ufss(ufss)
-{
-  d_true = NodeManager::currentNM()->mkConst( true );
-  d_false = NodeManager::currentNM()->mkConst( false );
-}
-
-void DisequalityPropagator::checkEquivalenceClass( Node t, Node eqc ) {
-  if( t.getKind()==APPLY_UF ){
-    Node op = t.getOperator();
-    eqc = d_ufss->getTheory()->getEqualityEngine()->getRepresentative( eqc );
-    eq::EqClassIterator eqc_i(eqc, d_ufss->getTheory()->getEqualityEngine());
-    while( !eqc_i.isFinished() ){
-      Node s = *eqc_i;
-      if( s.getKind()==APPLY_UF && s.getOperator()==op ){
-        int unkIndex = -1;
-        for( size_t i=0; i<t.getNumChildren(); i++ ){
-          //should consult strong solver since it knows more disequalities
-          if( d_ufss->areDisequal( t[i], s[i] ) ){
-          //if( d_qe->getEqualityQuery()->areDisequal( t[i], s[i] ) ){
-            unkIndex = -1;
-            break;
-          }else if( !d_qe->getEqualityQuery()->areEqual( t[i], s[i] ) ){
-            if( unkIndex==-1 ){
-              unkIndex = i;
-            }else{
-              unkIndex = -1;
-              break;
-            }
-          }
-        }
-        if( unkIndex!=-1 ){
-          Trace("deq-prop") << "propagate disequality " << t[unkIndex] << " " << s[unkIndex] << std::endl;
-          d_ufss->assertDisequal(t[unkIndex], s[unkIndex], Node::null());
-          ++( d_statistics.d_propagations );
-          if( d_ufss->isConflict() ){
-            return;
-          }
-        }
-      }
-      ++eqc_i;
-    }
-  }
-}
-
-/** merge */
-void DisequalityPropagator::merge( Node a, Node b ){
-
-}
-
-/** assert terms are disequal */
-void DisequalityPropagator::assertDisequal( Node a, Node b, Node reason ){
-  Trace("deq-prop") << "Notify disequal : " << a << " " << b << std::endl;
-}
-
-
-void DisequalityPropagator::assertPredicate( Node p, bool polarity ) {
-  Trace("deq-prop") << "Assert predicate : " << p << " " << polarity << std::endl;
-  checkEquivalenceClass( p, polarity ? d_false : d_true );
-}
-
-DisequalityPropagator::Statistics::Statistics():
-   d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0)
-{
-  smtStatisticsRegistry()->registerStat(& d_propagations);
-}
-
-DisequalityPropagator::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(& d_propagations);
-}
-
 }/* CVC4::theory namespace::uf */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 0166bd947..f634a493c 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -29,7 +29,6 @@ namespace theory {
 class SubsortSymmetryBreaker;
 namespace uf {
 class TheoryUF;
-class DisequalityPropagator;
 } /* namespace CVC4::theory::uf */
 } /* namespace CVC4::theory */
 } /* namespace CVC4 */
@@ -371,8 +370,6 @@ public:
   ~StrongSolverTheoryUF();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
-  /** disequality propagator */
-  DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; }
   /** symmetry breaker */
   SubsortSymmetryBreaker* getSymmetryBreaker() { return d_sym_break; }
   /** get sort inference module */
@@ -471,42 +468,10 @@ public:
   context::CDO<int> d_min_pos_tn_master_card;
   /** relevant eqc */
   NodeBoolMap d_rel_eqc;
-  /** disequality propagator */
-  DisequalityPropagator* d_deq_prop;
   /** symmetry breaking techniques */
   SubsortSymmetryBreaker* d_sym_break;
 }; /* class StrongSolverTheoryUF */
 
-class DisequalityPropagator {
-public:
-  DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss);
-  /** merge */
-  void merge( Node a, Node b );
-  /** assert terms are disequal */
-  void assertDisequal( Node a, Node b, Node reason );
-  /** assert predicate */
-  void assertPredicate( Node p, bool polarity );
-
-  class Statistics {
-  public:
-    IntStat d_propagations;
-    Statistics();
-    ~Statistics();
-  };
-  /** statistics class */
-  Statistics d_statistics;
-
-private:
-  /** quantifiers engine */
-  QuantifiersEngine* d_qe;
-  /** strong solver */
-  StrongSolverTheoryUF* d_ufss;
-  /** true,false */
-  Node d_true;
-  Node d_false;
-  /** check term t against equivalence class that t is disequal from */
-  void checkEquivalenceClass( Node t, Node eqc );
-}; /* class DisequalityPropagator */
 
 }/* CVC4::theory namespace::uf */
 }/* CVC4::theory namespace */