Remove miscellaneous unused code (#2333)

10 files changed, 1 insertions, 289 deletions

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index ac07e13fb..ae560c5e5 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -210,79 +210,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
   }
 }
 
-void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
-  //make sure internal representatives currently exist
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
-    if( it->first.isSort() ){
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
-      }
-    }
-  }
-  Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
-  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
-    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
-      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
-    }
-  }
-  //store representatives for newly created terms
-  std::map< Node, Node > temp_rep_map;
-
-  bool success;
-  do {
-    success = false;
-    for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
-      for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
-        if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
-          Node ni = it->second;
-          std::vector< Node > cc;
-          cc.push_back( it->second.getOperator() );
-          bool changed = false;
-          for( unsigned j=0; j<ni.getNumChildren(); j++ ){
-            if( ni[j].getType().isSort() ){
-              Node r = getRepresentative( ni[j] );
-              if( itt->second.find( r )==itt->second.end() ){
-                Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
-                r = temp_rep_map[r];
-              }
-              if( r==ni ){
-                //found sub-term as instance
-                Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
-                itt->second[it->first] = ni[j];
-                changed = false;
-                success = true;
-                break;
-              }else{
-                Node ir = itt->second[r];
-                cc.push_back( ir );
-                if( ni[j]!=ir ){
-                  changed = true;
-                }
-              }
-            }else{
-              changed = false;
-              break;
-            }
-          }
-          if( changed ){
-            Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
-            Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
-            success = true;
-            itt->second[it->first] = n;
-            temp_rep_map[n] = it->first;
-          }
-        }
-      }
-    }
-  }while( success );
-  Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
-  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
-    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
-      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
-    }
-  }
-}
-
 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
   return d_qe->getActiveEqualityEngine();
 }
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index a9a3cb185..8f836f9c6 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -114,8 +114,6 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
   Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
-  /** flatten representatives */
-  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
 }; /* EqualityQueryQuantifiersEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 6763a0ad3..81ecf9e77 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -166,11 +166,6 @@ bool ModelEngine::optOneQuantPerRound(){
 int ModelEngine::checkModel(){
   FirstOrderModel* fm = d_quantEngine->getModel();
 
-  //flatten the representatives
-  //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
-  // d_quantEngine->getEqualityQuery()->flattenRepresentatives(
-  // fm->getRepSet()->d_type_reps );
-
   //for debugging, setup
   for (std::map<TypeNode, std::vector<Node> >::iterator it =
            fm->getRepSetPtr()->d_type_reps.begin();
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 3006a07bf..02c9aedf5 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1870,33 +1870,6 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
   //}
 }
 
-//-------------------------------------------------- handling assertions / eqc
-
-void QuantConflictFind::assertNode( Node q ) {
-  /*
-  if( d_quantEngine->hasOwnership( q, this ) ){
-    Trace("qcf-proc") << "QCF : assertQuantifier : ";
-    debugPrintQuant("qcf-proc", q);
-    Trace("qcf-proc") << std::endl;
-  }
-  */
-}
-
-/** new node */
-void QuantConflictFind::newEqClass( Node n ) {
-
-}
-
-/** merge */
-void QuantConflictFind::merge( Node a, Node b ) {
-
-}
-
-/** assert disequal */
-void QuantConflictFind::assertDisequal( Node a, Node b ) {
-
-}
-
 //-------------------------------------------------- check function
 
 bool QuantConflictFind::needsCheck( Theory::Effort level ) {
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index e4eefe9ad..d76495b52 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -236,14 +236,6 @@ public:
   void registerQuantifier(Node q) override;
 
  public:
-  /** assert quantifier */
-  void assertNode(Node q) override;
-  /** new node */
-  void newEqClass( Node n );
-  /** merge */
-  void merge( Node a, Node b );
-  /** assert disequal */
-  void assertDisequal( Node a, Node b );
   /** needs check */
   bool needsCheck(Theory::Effort level) override;
   /** reset round */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 37451b776..cff14e0c3 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -32,25 +32,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-bool QuantifiersRewriter::isClause( Node n ){
-  if( isLiteral( n ) ){
-    return true;
-  }else if( n.getKind()==NOT ){
-    return isCube( n[0] );
-  }else if( n.getKind()==OR ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( !isClause( n[i] ) ){
-        return false;
-      }
-    }
-    return true;
-  }else if( n.getKind()==IMPLIES ){
-    return isCube( n[0] ) && isClause( n[1] );
-  }else{
-    return false;
-  }
-}
-
 bool QuantifiersRewriter::isLiteral( Node n ){
   switch( n.getKind() ){
   case NOT:
@@ -73,23 +54,6 @@ bool QuantifiersRewriter::isLiteral( Node n ){
   return true;
 }
 
-bool QuantifiersRewriter::isCube( Node n ){
-  if( isLiteral( n ) ){
-    return true;
-  }else if( n.getKind()==NOT ){
-    return isClause( n[0] );
-  }else if( n.getKind()==AND ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( !isCube( n[i] ) ){
-        return false;
-      }
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
 void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
   if( n.getKind()==OR ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index bd0192d9e..963e73701 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -32,9 +32,7 @@ class QuantifiersRewriter {
 private:
   static int getPurifyIdLit2( Node n, std::map< Node, int >& visited );
 public:
-  static bool isClause( Node n );
   static bool isLiteral( Node n );
-  static bool isCube( Node n );
 private:
   static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 29cd492c7..ebfa6f8bb 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1670,41 +1670,6 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     }
   }
 
-
-  Node TheorySetsRels::mkAnd( std::vector<TNode>& conjunctions ) {
-    Assert(conjunctions.size() > 0);
-    std::set<TNode> all;
-
-    for (unsigned i = 0; i < conjunctions.size(); ++i) {
-      TNode t = conjunctions[i];
-      if (t.getKind() == kind::AND) {
-        for(TNode::iterator child_it = t.begin();
-            child_it != t.end(); ++child_it) {
-          Assert((*child_it).getKind() != kind::AND);
-          all.insert(*child_it);
-        }
-      }
-      else {
-        all.insert(t);
-      }
-    }
-    Assert(all.size() > 0);
-    if (all.size() == 1) {
-      // All the same, or just one
-      return conjunctions[0];
-    }
-
-    NodeBuilder<> conjunction(kind::AND);
-    std::set<TNode>::const_iterator it = all.begin();
-    std::set<TNode>::const_iterator it_end = all.end();
-    while (it != it_end) {
-      conjunction << *it;
-      ++ it;
-    }
-
-    return conjunction;
-  }/* mkAnd() */
-
   void TheorySetsRels::printNodeMap(const char* fst,
                                     const char* snd,
                                     const NodeMap& map)
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index a95948bc7..161b5195e 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -185,7 +185,6 @@ private:
   bool areEqual( Node a, Node b );
   Node getRepresentative( Node t );
   bool exists( std::vector<Node>&, Node );
-  Node mkAnd( std::vector< TNode >& assumptions );
   inline void addToMembershipDB( Node, Node, Node  );
   static void printNodeMap(const char* fst,
                            const char* snd,
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 17f001a55..a3f1f9893 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -25,104 +25,6 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-typedef std::set<TNode> Elements;
-typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
-
-struct FlattenedNodeTag {};
-typedef expr::Attribute<FlattenedNodeTag, bool> flattened;
-
-
-/**
- * flattenNode looks for children of same kind, and if found merges
- * them into the parent.
- *
- * It simultaneously handles a couple of other optimizations: 
- * - trivialNode - if found during exploration, return that node itself
- *    (like in case of OR, if "true" is found, makes sense to replace
- *     whole formula with "true")
- * - skipNode - as name suggests, skip them
- *    (like in case of OR, you may want to skip any "false" nodes found)
- *
- * Use a null node if you want to ignore any of the optimizations.
- */
-RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
-{
-  if(n.hasAttribute(flattened()) && n.getAttribute(flattened())) {
-    return RewriteResponse(REWRITE_DONE, n);
-  }
-
-  typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
-
-  node_set visited;
-  visited.insert(skipNode);
-
-  std::vector<TNode> toProcess;
-  toProcess.push_back(n);
-
-  Kind k = n.getKind();
-  typedef std::vector<TNode> ChildList;
-  ChildList childList;   //TNode should be fine, since 'n' is still there
-
-  Debug("sets-rewrite-flatten") << "[sets-rewrite-flatten] " << n << std::endl;
-  for (unsigned i = 0; i < toProcess.size(); ++ i) {
-    TNode current = toProcess[i];
-    Debug("sets-rewrite-flatten") << "[sets-rewrite-flatten]   > Processing " << current << std::endl;
-    for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) {
-      TNode child = current[j];
-      if(visited.find(child) != visited.end()) {
-        continue;
-      } else if(child == trivialNode) {
-        return RewriteResponse(REWRITE_DONE, trivialNode);
-      } else {
-        visited.insert(child);
-        if(child.getKind() == k) {
-          toProcess.push_back(child);
-        } else {
-          childList.push_back(child);
-        }
-      }
-    }
-  }
-  if (childList.size() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
-  if (childList.size() == 1) return RewriteResponse(REWRITE_AGAIN, childList[0]);
-
-  sort(childList.begin(), childList.end());
-
-  /* Make sure we are under number of children possible in a node */
-  NodeManager* nodeManager = NodeManager::currentNM();
-  static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1;
-  AlwaysAssert(childList.size() < MAX_CHILDREN, "do not support formulas this big");
-
-  ChildList::iterator cur = childList.begin(), en = childList.end();
-  Node ret = (*cur);
-  ++cur;
-  while( cur != en ) {
-    ret = nodeManager->mkNode(k, ret, *cur);
-    ret.setAttribute(flattened(), true);
-    ++cur;
-  }
-  Trace("sets-postrewrite") << "flatten Sets::postRewrite returning " << ret << std::endl;
-  if(ret != n) {
-    return RewriteResponse(REWRITE_AGAIN, ret); // again for constants
-  } else {
-    return RewriteResponse(REWRITE_DONE, ret);
-  }
-  // if (childList.size() < MAX_CHILDREN) {
-  //   Node retNode = nodeManager->mkNode(k, childList);
-  //   return RewriteResponse(REWRITE_DONE, retNode);
-  // } else {
-  //   Assert(childList.size() < size_t(MAX_CHILDREN) * size_t(MAX_CHILDREN) );
-  //   NodeBuilder<> nb(k);
-  //   ChildList::iterator cur = childList.begin(), next, en = childList.end();
-  //   while( cur != en ) {
-  //     next = min(cur + MAX_CHILDREN, en);
-  //     nb << (nodeManager->mkNode(k, ChildList(cur, next) ));
-  //     cur = next;
-  //   }
-  //   return RewriteResponse(REWRITE_DONE, nb.constructNode());
-  // }
-}
-
 bool checkConstantMembership(TNode elementTerm, TNode setTerm)
 {
   if(setTerm.getKind() == kind::EMPTYSET) {
@@ -543,9 +445,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
 
   default:
     break;
-  }//switch(node.getKind())
+  }
 
-  // This default implementation
   return RewriteResponse(REWRITE_DONE, node);
 }