removing unecessary files

7 files changed, 1 insertions, 607 deletions

diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am
index 0e6197ac1..8b5fbe979 100644
--- a/src/theory/datatypes/Makefile.am
+++ b/src/theory/datatypes/Makefile.am
@@ -11,10 +11,6 @@ libdatatypes_la_SOURCES = \
 	theory_datatypes.h \
 	datatypes_rewriter.h \
 	theory_datatypes.cpp \
-	union_find.h \
-	union_find.cpp \
-	explanation_manager.h \
-	explanation_manager.cpp \
 	theory_datatypes_instantiator.h \
 	theory_datatypes_instantiator.cpp
 	
diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp
deleted file mode 100644
index be0bf6805..000000000
--- a/src/theory/datatypes/explanation_manager.cpp
+++ /dev/null
@@ -1,104 +0,0 @@
-/*********************                                                        */
-/*! \file explanation_manager.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/datatypes/explanation_manager.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::datatypes;
-
-void ProofManager::setExplanation( Node n, Node jn, unsigned r ) 
-{ 
-  Assert( n!=jn );
-  d_exp[n] = std::pair< Node, unsigned >( jn, r ); 
-}
-
-//std::ostream& operator<<(std::ostream& os, Reason::Rule r)
-//{
-//  switch( r ){
-//    
-//  }
-//}
-
-void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm )
-{
-  if( n.getKind()==kind::AND ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-      process( n[i], nb, pm );
-    }
-  }else{
-    if( !pm->hasExplained( n ) ){
-      context::CDHashMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n );
-      Reason r;
-      Node exp;
-      if( it!=d_drv_map.end() ){
-        r = (*it).second;
-        if( !r.d_isInput ){
-          if( r.d_e ){
-
-            Debug("emanager") << "Em::process: Consult externally for " << n << std::endl;
-            exp = r.d_e->explain( n, pm );
-            //trivial case, explainer says that n is an input
-            if( exp==n ){
-              r.d_isInput = true;
-            }
-          }else{
-            exp = r.d_node;
-            pm->setExplanation( n, exp, r.d_reason );
-            if( exp.isNull() ) Debug("emanager") << "Em::process: " << n << " is an axiom, reason = " << r.d_reason << endl;
-          }
-        }
-      }
-
-      if( r.d_isInput ){
-        Debug("emanager") << "Em::process: " << n << " is an input " << endl;
-        nb << n;
-        pm->setExplanation( n, Node::null(), Reason::input );
-      }else if( !exp.isNull() ){
-        Debug("emanager") << "Em::process: " << exp << " is the explanation for " << n << " " 
-                          << ", reason = " << pm->getReason( n ) << endl;
-        if( exp.getKind()==kind::AND ){
-          for( int i=0; i<(int)exp.getNumChildren(); i++ ) {
-            process( exp[i], nb, pm );
-          }
-        }else{
-          process( exp, nb, pm );
-        }
-      }
-    }else{
-      Debug("emanager") << "Em::process: proof manager has already explained " << n << endl;
-    }
-  }
-}
-
-Node ExplanationManager::explain( Node n, ProofManager* pm )
-{
-  NodeBuilder<> nb(kind::AND);
-  if( pm ){
-    pm->clear();
-    process( n, nb, pm );
-  }else{
-    ProofManager pm;
-    process( n, nb, &pm );
-  }
-  return ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
-}
diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h
deleted file mode 100644
index 174b90ff5..000000000
--- a/src/theory/datatypes/explanation_manager.h
+++ /dev/null
@@ -1,222 +0,0 @@
-/*********************                                                        */
-/*! \file explanation_manager.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Theory of datatypes.
- **
- ** Theory of datatypes.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H
-#define __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H
-
-#include "theory/theory.h"
-#include "util/congruence_closure.h"
-#include "util/datatype.h"
-#include "util/hash.h"
-#include "util/trans_closure.h"
-
-#include <ext/hash_set>
-#include <iostream>
-#include <map>
-
-namespace CVC4 {
-namespace theory {
-namespace datatypes {
-
-
-class Explainer;
-
-/** reason class */
-class Reason { 
-public:
-  enum Rule {
-    unspecified = 0,
-    contradiction = 1,
-
-    cc_coarse,
-
-    //coarse rules for idt
-    idt_cycle_coarse,
-    idt_inst_coarse,
-    //unification rules
-    idt_unify,
-    idt_clash,
-    //tester rules
-    idt_taxiom,
-    idt_tcong,
-    idt_tclash,
-    idt_texhaust,
-    //other rules
-    idt_inst,
-    idt_collapse,
-    idt_collapse2,
-
-    input,
-  };
-public:
-  Reason() : d_e( NULL ), d_isInput( true ){}
-  Reason( Node n, unsigned r ) : d_node( n ), d_reason( r ), d_e( NULL ), d_isInput( false ) {}
-  Reason( Explainer* e ) : d_reason( 0 ), d_e( e ), d_isInput( false ){}
-  virtual ~Reason(){}
-  Node d_node;
-  unsigned d_reason;
-  Explainer* d_e;
-  bool d_isInput;
-};
-
-/** proof manager for theory lemmas */
-class ProofManager {
-protected:
-  enum Effort {
-    MIN_EFFORT = 0,
-    STANDARD = 50,
-    FULL_EFFORT = 100
-  };/* enum Effort */
-  /** map from nodes to a description of how they are explained */
-  std::map< Node, std::pair< Node, unsigned > > d_exp;
-  /** whether to produce proofs */
-  Effort d_effort;
-public:
-  ProofManager( Effort effort = STANDARD ) : d_effort( effort ){}
-  ~ProofManager(){}
-  void setExplanation( Node n, Node jn, unsigned r = 0 );
-  bool hasExplained( Node n ) { return d_exp.find( n )!=d_exp.end(); }
-  Effort getEffort() { return d_effort; }
-  void clear() { d_exp.clear(); }
-  /** for debugging */
-  Node getJustification( Node n ) { return d_exp[n].first; }
-  unsigned getReason( Node n ) { return d_exp[n].second; }
-};
-
-class Explainer 
-{
-public:
-  /** assert that n is true */
-  virtual void assertTrue( Node n ) = 0;
-  /** get the explanation for n.  
-      This should call pm->setExplanation( n1, jn1, r1 ) ... pm->setExplanation( nk, jnk, rk )
-        for some set of Nodes n1...nk.
-      Satisfies post conditions:
-      - If pm->getEffort() = MAX_EFFORT, then each ( ni, jni, ri ) should be a precise
-          application or rule ri, i.e. applying proof rule ri to jni derives ni.
-      - If pm->getEffort() = STANDARD, then for each ( ni, jni, ri ), 
-          jni is the (at least informal) justification for ni.
-      - Return value should be a (possibly empty) conjunction of nodes n'1...n'k, where each n'i occurs 
-          (as a conjunct) in jn1...jnk, but not in n1...nk.  
-          For each of these literals n'i, assertTrue( n'i ) was called.
-      - either pm->setExplanation( n, ... ) is called, or n is the return value.
-  */
-  virtual Node explain( Node n, ProofManager* pm ) = 0;
-};
-
-template <class OutputChannel, class CongruenceOperatorList>
-class CongruenceClosureExplainer : public Explainer
-{
-protected:
-  //pointer to the congruence closure module
-  CongruenceClosure<OutputChannel, CongruenceOperatorList>* d_cc;
-public:
-  CongruenceClosureExplainer(CongruenceClosure<OutputChannel, CongruenceOperatorList>* cc) :
-    Explainer(),
-    d_cc( cc ){
-   }
-  ~CongruenceClosureExplainer(){}
-  /** assert that n is true */
-  void assertTrue( Node n ){
-    Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF );
-    d_cc->addEquality( n );
-  }
-  /** get the explanation for n */
-  Node explain( Node n, ProofManager* pm ){
-    Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF );
-    if( pm->getEffort()==ProofManager::FULL_EFFORT ){
-      //unsupported
-      Assert( false );
-      return Node::null();
-    }else{
-      Node exp = d_cc->explain( n[0], n[1] );
-      if( exp!=n ){
-        pm->setExplanation( n, exp, Reason::cc_coarse );
-      }
-      return exp;
-    }
-  }
-};
-
-
-class ExplanationManager : public Explainer
-{
-private:
-  /** map from nodes and the reason for them */
-  context::CDHashMap< Node, Reason, NodeHashFunction > d_drv_map;
-  /** has conflict */
-  context::CDO< bool > d_hasConflict;
-  /** process the reason for node n */
-  void process( Node n, NodeBuilder<>& nb, ProofManager* pm );
-public:
-  ExplanationManager(context::Context* c) : Explainer(), d_drv_map(c), d_hasConflict( c, false ){}
-  ~ExplanationManager(){}
-
-  /** assert that n is true (n is an input) */
-  void assertTrue( Node n ) { 
-    //TODO: this can be optimized: 
-    //  if the previous explanation for n was empty (n is a tautology), 
-    //  then we should not claim it to be an input.
-    Reason r = d_drv_map[n];
-    r.d_isInput = true; 
-  }
-  /** n is explained */
-  bool hasNode( Node n ) { return d_drv_map.find( n )!=d_drv_map.end(); }
-  /** n is explained */
-  bool hasConflict() { return d_hasConflict.get() || hasNode( NodeManager::currentNM()->mkConst(false) ); }
-  /** jn is why n is true, by rule r */
-  void addNode( Node n, Node jn, unsigned r = 0 ) { 
-    if( !hasNode( n ) ){
-      Assert( n!=jn );
-      Debug("emanager") << "em::addNode: (" << jn << ", " << r << ") -> " << n << std::endl;
-      d_drv_map[n] = Reason( jn, r ); 
-    }
-  }
-  /** Explainer e can tell you why n is true in the current state.  */
-  void addNode( Node n, Explainer* e ) {
-    if( !hasNode( n ) ){
-      Debug("emanager") << "em::addNodeEx: (" << e << ") -> " << n << std::endl;
-      d_drv_map[n] = Reason( e ); 
-    }
-  }
-  /** n is true by reason (axiom) r */
-  void addNodeAxiom( Node n, unsigned r = 0 ) { addNode( n, Node::null(), r ); }
-  /** conclude a contradiction by jn and reason r */
-  void addNodeConflict( Node jn, unsigned r = 0 ){
-    addNode( NodeManager::currentNM()->mkConst(false), jn, r );
-    d_hasConflict.set( true );
-  }
-  /** get explanation for n 
-      Requires pre conditions: TBD
-      Satisfies post conditions:  TBD
-  */
-  Node explain( Node n, ProofManager* pm = NULL );
-  /** get conflict */
-  Node getConflict( ProofManager* pm = NULL ){
-    return explain( NodeManager::currentNM()->mkConst(false), pm );
-  }
-};
-
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 6d9672f95..725f9a5e6 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -22,17 +22,15 @@
 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
 
 #include "theory/theory.h"
-#include "util/congruence_closure.h"
 #include "util/datatype.h"
-#include "theory/datatypes/union_find.h"
 #include "util/hash.h"
 #include "util/trans_closure.h"
-#include "theory/datatypes/explanation_manager.h"
 #include "theory/uf/equality_engine.h"
 
 #include <ext/hash_set>
 #include <iostream>
 #include <map>
+#include "context/cdchunk_list.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/datatypes/theory_datatypes_candidate_generator.h b/src/theory/datatypes/theory_datatypes_candidate_generator.h
deleted file mode 100644
index 46c7ce7fb..000000000
--- a/src/theory/datatypes/theory_datatypes_candidate_generator.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/*********************                                                        */
-/*! \file theory_uf_candidate generator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Theory datatypes candidate generator
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H
-#define __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/datatypes/theory_datatypes.h"
-#include "theory/rr_inst_match.h"
-
-namespace CVC4 {
-namespace theory {
-namespace datatypes {
-
-namespace rrinst {
-typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
-
-// Just iterate amoung the equivalence class of the given node
-// node::Null() *can't* be given to reset
-class CandidateGeneratorTheoryClass : public CandidateGenerator{
-private:
-  //instantiator pointer
-  TheoryDatatypes* d_th;
-  //the equality class iterator
-  TheoryDatatypes::EqListN::const_iterator d_eqc_i;
-  TheoryDatatypes::EqListN* d_eqc;
-public:
-  CandidateGeneratorTheoryClass( TheoryDatatypes* th): d_th( th ), d_eqc(NULL){}
-  ~CandidateGeneratorTheoryClass(){}
-  void resetInstantiationRound(){};
-  void reset( TNode n ){
-    TheoryDatatypes::EqListsN::const_iterator i = d_th->d_equivalence_class.find(n);
-    if(i == d_th->d_equivalence_class.end()){
-      d_eqc = NULL;
-    } else {
-      d_eqc = (*i).second;
-      d_eqc_i = d_eqc->begin();
-    }
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if( d_eqc == NULL || d_eqc_i == d_eqc->end() ) return Node::null();
-    return *(d_eqc_i++);
-  };
-};
-
-
-}
-}
-}
-}
-
-#endif /* __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H */
diff --git a/src/theory/datatypes/union_find.cpp b/src/theory/datatypes/union_find.cpp
deleted file mode 100644
index 34706719e..000000000
--- a/src/theory/datatypes/union_find.cpp
+++ /dev/null
@@ -1,59 +0,0 @@
-/*********************                                                        */
-/*! \file union_find.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include <iostream>
-
-#include "theory/datatypes/union_find.h"
-#include "util/Assert.h"
-#include "expr/node.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace datatypes {
-
-template <class NodeType, class NodeHash>
-void UnionFind<NodeType, NodeHash>::contextNotifyPop() {
-  Trace("datatypesuf") << "datatypesUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl;
-  while(d_offset < d_trace.size()) {
-    pair<TNode, TNode> p = d_trace.back();
-    if(p.second.isNull()) {
-      d_map.erase(p.first);
-      Trace("datatypesuf") << "datatypesUF   " << d_trace.size() << " erasing " << p.first << endl;
-    } else {
-      d_map[p.first] = p.second;
-      Trace("datatypesuf") << "datatypesUF   " << d_trace.size() << " replacing " << p << endl;
-    }
-    d_trace.pop_back();
-  }
-  Trace("datatypesuf") << "datatypesUF cancelling finished." << endl;
-}
-
-// The following declarations allow us to put functions in the .cpp file
-// instead of the header, since we know which instantiations are needed.
-
-template void UnionFind<Node, NodeHashFunction>::contextNotifyPop();
-
-template void UnionFind<TNode, TNodeHashFunction>::contextNotifyPop();
-
-}/* CVC4::theory::datatypes namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/datatypes/union_find.h b/src/theory/datatypes/union_find.h
deleted file mode 100644
index 4893c3502..000000000
--- a/src/theory/datatypes/union_find.h
+++ /dev/null
@@ -1,148 +0,0 @@
-/*********************                                                        */
-/*! \file union_find.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__DATATYPES__UNION_FIND_H
-#define __CVC4__THEORY__DATATYPES__UNION_FIND_H
-
-#include <utility>
-#include <vector>
-#include <ext/hash_map>
-
-#include "expr/node.h"
-#include "context/cdo.h"
-
-namespace CVC4 {
-
-namespace context {
-  class Context;
-}/* CVC4::context namespace */
-
-namespace theory {
-namespace datatypes {
-
-// NodeType \in { Node, TNode }
-template <class NodeType, class NodeHash>
-class UnionFind : context::ContextNotifyObj {
-  /** Our underlying map type. */
-  typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
-
-  /**
-   * Our map of Nodes to their canonical representatives.
-   * If a Node is not present in the map, it is its own
-   * representative.
-   */
-  MapType d_map;
-
-  /** Our undo stack for changes made to d_map. */
-  std::vector<std::pair<TNode, TNode> > d_trace;
-
-  /** Our current offset in the d_trace stack (context-dependent). */
-  context::CDO<size_t> d_offset;
-
-public:
-  UnionFind(context::Context* ctxt) :
-    context::ContextNotifyObj(ctxt),
-    d_offset(ctxt, 0) {
-  }
-
-  ~UnionFind() throw() { }
-
-  /**
-   * Return a Node's union-find representative, doing path compression.
-   */
-  inline TNode find(TNode n);
-
-  /**
-   * Return a Node's union-find representative, NOT doing path compression.
-   * This is useful for Assert() statements, debug checking, and similar
-   * things that you do NOT want to mutate the structure.
-   */
-  inline TNode debugFind(TNode n) const;
-
-  /**
-   * Set the canonical representative of n to newParent.  They should BOTH
-   * be their own canonical representatives on entry to this funciton.
-   */
-  inline void setCanon(TNode n, TNode newParent);
-
-protected:
-
-  /**
-   * Called by the Context when a pop occurs.  Cancels everything to the
-   * current context level.  Overrides ContextNotifyObj::contextNotifyPop().
-   */
-  void contextNotifyPop();
-
-};/* class UnionFind<> */
-
-template <class NodeType, class NodeHash>
-inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
-  typename MapType::const_iterator i = d_map.find(n);
-  if(i == d_map.end()) {
-    return n;
-  } else {
-    return debugFind((*i).second);
-  }
-}
-
-template <class NodeType, class NodeHash>
-inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) {
-  Trace("datatypesuf") << "datatypesUF find of " << n << std::endl;
-  typename MapType::iterator i = d_map.find(n);
-  if(i == d_map.end()) {
-    Trace("datatypesuf") << "datatypesUF   it is rep" << std::endl;
-    return n;
-  } else {
-    Trace("datatypesuf") << "datatypesUF   not rep: par is " << (*i).second << std::endl;
-    std::pair<TNode, TNode> pr = *i;
-    // our iterator is invalidated by the recursive call to find(),
-    // since it mutates the map
-    TNode p = find(pr.second);
-    if(p == pr.second) {
-      return p;
-    }
-    d_trace.push_back(std::make_pair(n, pr.second));
-    d_offset = d_trace.size();
-    Trace("datatypesuf") << "datatypesUF   setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl;
-    pr.second = p;
-    d_map.insert(pr);
-    return p;
-  }
-}
-
-template <class NodeType, class NodeHash>
-inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
-  Assert(d_map.find(n) == d_map.end());
-  Assert(d_map.find(newParent) == d_map.end());
-  if(n != newParent) {
-    Trace("datatypesuf") << "datatypesUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl;
-    d_map[n] = newParent;
-    d_trace.push_back(std::make_pair(n, TNode::null()));
-    d_offset = d_trace.size();
-  }
-}
-
-}/* CVC4::theory::datatypes namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /*__CVC4__THEORY__DATATYPES__UNION_FIND_H */