from meeting

1 files changed, 0 insertions, 43 deletions

diff --git a/src/core/prop_engine.h b/src/core/prop_engine.h
deleted file mode 100644
index 0febd2927..000000000
--- a/src/core/prop_engine.h
+++ /dev/null
@@ -1,43 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** prop_engine.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_PROP_ENGINE_H
-#define __CVC4_PROP_ENGINE_H
-
-#include "core/cvc4_expr.h"
-#include "core/decision_engine.h"
-#include "core/theory_engine.h"
-
-namespace CVC4 {
-
-// In terms of abstraction, this is below (and provides services to)
-// Prover and above (and requires the services of) a specific
-// propositional solver, DPLL or otherwise.
-
-class PropEngine {
-  DecisionEngine* d_de;
-
-public:
-  /**
-   * Create a PropEngine with a particular decision and theory engine.
-   */
-  PropEngine(DecisionEngine*, TheoryEngine*);
-
-  /**
-   * Converts to CNF if necessary.
-   */
-  void solve(Expr);
-
-};/* class PropEngine */
-
-}
-
-#endif /* __CVC4_PROP_ENGINE_H */