From 105503064be6a198dd864d1e95d6d79e1af51d25 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 17 Nov 2009 17:09:13 +0000
Subject: [PATCH] from meeting

---
 src/{core => prop}/prop_engine.h        | 0
 src/{core => prop}/sat.h                | 0
 src/{core/prover.h => smt/smt_engine.h} | 6 +++---
 src/{core => util}/assert.h             | 0
 src/{core => util}/command.h            | 0
 src/{core => util}/debug.h              | 0
 src/{core => util}/decision_engine.h    | 0
 src/{core => util}/exception.h          | 0
 src/{core => util}/literal.h            | 0
 src/{core => util}/model.h              | 0
 src/{core => util}/result.h             | 0
 src/{core => util}/unique_id.h          | 0
 12 files changed, 3 insertions(+), 3 deletions(-)
 rename src/{core => prop}/prop_engine.h (100%)
 rename src/{core => prop}/sat.h (100%)
 rename src/{core/prover.h => smt/smt_engine.h} (97%)
 rename src/{core => util}/assert.h (100%)
 rename src/{core => util}/command.h (100%)
 rename src/{core => util}/debug.h (100%)
 rename src/{core => util}/decision_engine.h (100%)
 rename src/{core => util}/exception.h (100%)
 rename src/{core => util}/literal.h (100%)
 rename src/{core => util}/model.h (100%)
 rename src/{core => util}/result.h (100%)
 rename src/{core => util}/unique_id.h (100%)

diff --git a/src/core/prop_engine.h b/src/prop/prop_engine.h
similarity index 100%
rename from src/core/prop_engine.h
rename to src/prop/prop_engine.h
diff --git a/src/core/sat.h b/src/prop/sat.h
similarity index 100%
rename from src/core/sat.h
rename to src/prop/sat.h
diff --git a/src/core/prover.h b/src/smt/smt_engine.h
similarity index 97%
rename from src/core/prover.h
rename to src/smt/smt_engine.h
index 14eab7c03..6f6fb355a 100644
--- a/src/core/prover.h
+++ b/src/smt/smt_engine.h
@@ -25,7 +25,7 @@ namespace CVC4 {
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
-// Prover and override check()?
+// SmtEngine and override check()?
 //
 // Probably better than that is to have a configuration object that
 // indicates which passes are desired.  The configuration occurs
@@ -34,7 +34,7 @@ namespace CVC4 {
 //
 // The CNF conversion can go on in PropEngine.
 
-class Prover {
+class SmtEngine {
   /** Current set of assertions. */
   // TODO: make context-aware to handle user-level push/pop.
   std::vector<Expr> d_assertList;
@@ -107,7 +107,7 @@ public:
    * Pop a user-level context.  Throws an exception if nothing to pop.
    */
   void pop();
-};/* class Prover */
+};/* class SmtEngine */
 
 } /* CVC4 namespace */
 
diff --git a/src/core/assert.h b/src/util/assert.h
similarity index 100%
rename from src/core/assert.h
rename to src/util/assert.h
diff --git a/src/core/command.h b/src/util/command.h
similarity index 100%
rename from src/core/command.h
rename to src/util/command.h
diff --git a/src/core/debug.h b/src/util/debug.h
similarity index 100%
rename from src/core/debug.h
rename to src/util/debug.h
diff --git a/src/core/decision_engine.h b/src/util/decision_engine.h
similarity index 100%
rename from src/core/decision_engine.h
rename to src/util/decision_engine.h
diff --git a/src/core/exception.h b/src/util/exception.h
similarity index 100%
rename from src/core/exception.h
rename to src/util/exception.h
diff --git a/src/core/literal.h b/src/util/literal.h
similarity index 100%
rename from src/core/literal.h
rename to src/util/literal.h
diff --git a/src/core/model.h b/src/util/model.h
similarity index 100%
rename from src/core/model.h
rename to src/util/model.h
diff --git a/src/core/result.h b/src/util/result.h
similarity index 100%
rename from src/core/result.h
rename to src/util/result.h
diff --git a/src/core/unique_id.h b/src/util/unique_id.h
similarity index 100%
rename from src/core/unique_id.h
rename to src/util/unique_id.h
-- 
2.30.2