/*********************                                                        */
/*! \file theory_uf.h
 ** \verbatim
 ** Original author: mdeters
 ** Major contributors: none
 ** Minor contributors (to current version): none
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009, 2010  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 This is the interface to TheoryUF implementations
 **
 ** This is the interface to TheoryUF implementations.  All
 ** implementations of TheoryUF should inherit from this class.
 **/

#include "cvc4_private.h"

#ifndef __CVC4__THEORY__UF__THEORY_UF_H
#define __CVC4__THEORY__UF__THEORY_UF_H

#include "expr/node.h"
#include "expr/attribute.h"

#include "theory/theory.h"

#include "context/context.h"

namespace CVC4 {
namespace theory {
namespace uf {

class TheoryUF : public Theory {
public:

  /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
  TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation)
    : Theory(THEORY_UF, ctxt, out, valuation) { }

  // We declare these here (even though it's not terribly useful) for
  // documentation reasons, and to keep mktheorytraits from issuing a
  // spurious warning.
  virtual void check(Effort) = 0;
  virtual void propagate(Effort) {}
  virtual void staticLearning(TNode in, NodeBuilder<>& learned) {}
  virtual void notifyRestart() {}
  virtual void presolve() {}

};/* class TheoryUF */

}/* CVC4::theory::uf namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */

#endif /* __CVC4__THEORY__UF__THEORY_UF_H */