summaryrefslogtreecommitdiff
path: root/src/include/prop_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/include/prop_engine.h')
-rw-r--r--src/include/prop_engine.h43
1 files changed, 0 insertions, 43 deletions
diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h
deleted file mode 100644
index de25c5594..000000000
--- a/src/include/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 "expr.h"
-#include "decision_engine.h"
-#include "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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback