big check-in of various fixes and adjustments

3 files changed, 0 insertions, 296 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 */
diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h
deleted file mode 100644
index 863097123..000000000
--- a/src/include/cvc4_expr.h
+++ /dev/null
@@ -1,100 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** cvc4_expr.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.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **/
-
-#ifndef __CVC4_EXPR_H
-#define __CVC4_EXPR_H
-
-#include <vector>
-#include <stdint.h>
-
-#include "cvc4_config.h"
-#include "expr/kind.h"
-
-namespace CVC4 {
-
-namespace expr {
-  class ExprValue;
-}/* CVC4::expr namespace */
-
-using CVC4::expr::ExprValue;
-
-/**
- * Encapsulation of an ExprValue pointer.  The reference count is
- * maintained in the ExprValue.
- */
-class CVC4_PUBLIC Expr {
-  /** A convenient null-valued encapsulated pointer */
-  static Expr s_null;
-
-  /** The referenced ExprValue */
-  ExprValue* d_ev;
-
-  /** This constructor is reserved for use by the Expr package; one
-   *  must construct an Expr using one of the build mechanisms of the
-   *  Expr package.
-   *
-   *  Increments the reference count. */
-  explicit Expr(ExprValue*);
-
-  typedef Expr* iterator;
-  typedef Expr const* const_iterator;
-
-  friend class ExprBuilder;
-
-public:
-  CVC4_PUBLIC Expr(const Expr&);
-
-  /** Destructor.  Decrements the reference count and, if zero,
-   *  collects the ExprValue. */
-  CVC4_PUBLIC ~Expr();
-
-  Expr& operator=(const Expr&) CVC4_PUBLIC;
-
-  /** Access to the encapsulated expression.
-   *  @return the encapsulated expression. */
-  ExprValue* operator->() const CVC4_PUBLIC;
-
-  uint64_t hash() const;
-
-  Expr eqExpr(const Expr& right) const;
-  Expr notExpr() const;
-  Expr negate() const; // avoid double-negatives
-  Expr andExpr(const Expr& right) const;
-  Expr orExpr(const Expr& right) const;
-  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
-  Expr iffExpr(const Expr& right) const;
-  Expr impExpr(const Expr& right) const;
-  Expr xorExpr(const Expr& right) const;
-
-  Expr plusExpr(const Expr& right) const;
-  Expr uMinusExpr() const;
-  Expr multExpr(const Expr& right) const;
-
-  inline Kind getKind() const;
-
-  static Expr null() { return s_null; }
-
-};/* class Expr */
-
-}/* CVC4 namespace */
-
-#include "expr/expr_value.h"
-
-namespace CVC4 {
-
-inline Kind Expr::getKind() const {
-  return Kind(d_ev->d_kind);
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_EXPR_H */
diff --git a/src/include/theory.h b/src/include/theory.h
deleted file mode 100644
index 47b4a2d92..000000000
--- a/src/include/theory.h
+++ /dev/null
@@ -1,81 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** theory.h
- ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- **/
-
-#ifndef __CVC4_THEORY_H
-#define __CVC4_THEORY_H
-
-#include "expr.h"
-#include "literal.h"
-
-namespace CVC4 {
-
-/**
- * Base class for T-solvers.  Abstract DPLL(T).
- */
-class Theory {
-public:
-  /**
-   * Subclasses of Theory may add additional efforts.  DO NOT CHECK
-   * equality with one of these values (e.g. if STANDARD xxx) but
-   * rather use range checks (or use the helper functions below).
-   * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
-   * with MAX_EFFORT.
-   */
-  enum Effort {
-    MIN_EFFORT = 0,
-    QUICK_CHECK = 10,
-    STANDARD = 50,
-    FULL_EFFORT = 100
-  };/* enum Effort */
-
-  // TODO add compiler annotation "constant function" here
-  static bool minEffortOnly(Effort e)        { return e == MIN_EFFORT; }
-  static bool quickCheckOrMore(Effort e)     { return e >= QUICK_CHECK; }
-  static bool quickCheckOnly(Effort e)       { return e >= QUICK_CHECK && e < STANDARD; }
-  static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
-  static bool standardEffortOnly(Effort e)   { return e >= STANDARD && e < FULL_EFFORT; }
-  static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
-
-  /**
-   * Prepare for an Expr.
-   */
-  virtual void setup(Expr) = 0;
-
-  /**
-   * Assert a literal in the current context.
-   */
-  virtual void assert(Literal) = 0;
-
-  /**
-   * Check the current assignment's consistency.  Return false iff inconsistent.
-   */
-  virtual bool check(Effort level = FULL_EFFORT) = 0;
-
-  /**
-   * T-propagate new literal assignments in the current context.
-   */
-  // TODO design decisoin: instead of returning a set of literals
-  // here, perhaps we have an interface back into the prop engine
-  // where we assert directly.  we might sometimes unknowingly assert
-  // something clearly inconsistent (esp. in a parallel context).
-  // This would allow the PropEngine to cancel our further work since
-  // we're already inconsistent---also could strategize dynamically on
-  // whether enough theory prop work has occurred.
-  virtual void propagate(Callback propagator, Effort level = FULL_EFFORT) = 0;
-
-  /**
-   * Return an explanation for the literal (which was previously propagated by this theory)..
-   */
-  virtual Expr explain(Literal) = 0;
-
-};/* class Theory */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_THEORY_H */