1 files changed, 0 insertions, 115 deletions
diff --git a/src/include/cvc4.h b/src/include/cvc4.h
deleted file mode 100644
index bbaffabb0..000000000
--- a/src/include/cvc4.h
+++ /dev/null
@@ -1,115 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** cvc4.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_H
-#define __CVC4_H
-
-#include <vector>
-#include "cvc4_expr.h"
-#include "util/command.h"
-#include "util/result.h"
-#include "util/model.h"
-
-namespace CVC4 {
-
-class SmtEngine {
-  /** Current set of assertions. */
-  // TODO: make context-aware to handle user-level push/pop.
-  std::vector<Expr> d_assertList;
-
-  /** Our expression manager */
-  ExprManager *d_em;
-
-  /** User-level options */
-  Options *opts;
-
-  /**
-   * Pre-process an Expr.  This is expected to be highly-variable,
-   * with a lot of "source-level configurability" to add multiple
-   * passes over the Expr.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
-   */
-  void preprocess(Expr);
-
-  /**
-   * Adds a formula to the current context.
-   */
-  void addFormula(Expr);
-
-  /**
-   * Full check of consistency in current context.  Returns true iff
-   * consistent.
-   */
-  Result check();
-
-  /**
-   * Quick check of consistency in current context: calls
-   * processAssertionList() then look for inconsistency (based only on
-   * that).
-   */
-  Result quickCheck();
-
-  /**
-   * Process the assertion list: for literals and conjunctions of
-   * literals, assert to T-solver.
-   */
-  void processAssertionList();
-
-public:
-  /*
-   * Construct an SmtEngine with the given expression manager and user options.
-   */
-  SmtEngine(ExprManager*, Options*) throw();
-
-  /**
-   * Execute a command.
-   */
-  void doCommand(Command*);
-
-  /**
-   * Add a formula to the current context: preprocess, do per-theory
-   * setup, use processAssertionList(), asserting to T-solver for
-   * literals and conjunction of literals.  Returns false iff
-   * inconsistent.
-   */
-  Result assert(Expr);
-
-  /**
-   * Add a formula to the current context and call check().  Returns
-   * true iff consistent.
-   */
-  Result query(Expr);
-
-  /**
-   * Simplify a formula without doing "much" work.  Requires assist
-   * from the SAT Engine.
-   */
-  Expr simplify(Expr);
-
-  /**
-   * Get a (counter)model (only if preceded by a SAT or INVALID query.
-   */
-  Model getModel();
-
-  /**
-   * Push a user-level context.
-   */
-  void push();
-
-  /**
-   * Pop a user-level context.  Throws an exception if nothing to pop.
-   */
-  void pop();
-};/* class SmtEngine */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_H */