Minor cleanup and reorganization related to last commit.

7 files changed, 8 insertions, 160 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
deleted file mode 100644
index 442355580..000000000
--- a/src/smt/boolean_terms.cpp
+++ /dev/null
@@ -1,42 +0,0 @@
-/*********************                                                        */
-/*! \file boolean_terms.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-#include "smt/boolean_terms.h"
-
-#include <algorithm>
-#include <map>
-#include <set>
-#include <stack>
-#include <string>
-
-#include "expr/kind.h"
-#include "expr/node_manager_attributes.h"
-#include "options/boolean_term_conversion_mode.h"
-#include "options/booleans_options.h"
-#include "smt/smt_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/theory_model.h"
-#include "util/ntuple.h"
-
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::booleans;
-
-namespace CVC4 {
-namespace smt {
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
deleted file mode 100644
index 0fb82aafe..000000000
--- a/src/smt/boolean_terms.h
+++ /dev/null
@@ -1,32 +0,0 @@
-/*********************                                                        */
-/*! \file boolean_terms.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include "expr/attribute.h"
-#include "expr/node.h"
-#include "util/hash.h"
-#include <map>
-#include <utility>
-
-namespace CVC4 {
-namespace smt {
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
deleted file mode 100644
index 0076b9de9..000000000
--- a/src/smt/model_postprocessor.cpp
+++ /dev/null
@@ -1,30 +0,0 @@
-/*********************                                                        */
-/*! \file model_postprocessor.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief
- **
- **
- **/
-
-#include "smt/model_postprocessor.h"
-
-#include "expr/node_manager_attributes.h"
-#include "expr/record.h"
-#include "smt/boolean_terms.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace smt {
-
-
-} /* namespace smt */
-} /* namespace CVC4 */
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
deleted file mode 100644
index a354315ef..000000000
--- a/src/smt/model_postprocessor.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*********************                                                        */
-/*! \file model_postprocessor.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief 
- **
- ** 
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__MODEL_POSTPROCESSOR_H
-#define __CVC4__MODEL_POSTPROCESSOR_H
-
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace smt {
-
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__MODEL_POSTPROCESSOR_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cefef9345..b94e08fad 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -46,8 +46,6 @@
 #include "options/arith_options.h"
 #include "options/arrays_options.h"
 #include "options/base_options.h"
-#include "options/boolean_term_conversion_mode.h"
-#include "options/booleans_options.h"
 #include "options/booleans_options.h"
 #include "options/bv_options.h"
 #include "options/datatypes_options.h"
@@ -72,13 +70,11 @@
 #include "proof/theory_proof.h"
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
-#include "smt/boolean_terms.h"
 #include "smt/command.h"
 #include "smt/command_list.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 #include "smt/logic_request.h"
 #include "smt/managed_ostreams.h"
-#include "smt/model_postprocessor.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/update_ostream.h"
 #include "smt_util/boolean_simplification.h"
@@ -4469,19 +4465,6 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
 }/* SmtEngine::assertFormula() */
 
 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
-/*
-  ModelPostprocessor mpost;
-  NodeVisitor<ModelPostprocessor> visitor;
-  Node value = visitor.run(mpost, node);
-  Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
-  Node realValue = mpost.rewriteAs(value, expectedType);
-  Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl;
-  if(options::condenseFunctionValues()) {
-    realValue = Rewriter::rewrite(realValue);
-    Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl;
-  }
-  return realValue;
-  */
   return node;
 }
 
diff --git a/src/smt/ite_removal.cpp b/src/smt/term_formula_removal.cpp
index 0202a5a2d..3fd333cc5 100644
--- a/src/smt/ite_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file ite_removal.cpp
+/*! \file term_formula_removal.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Morgan Deters, Dejan Jovanovic, Tim King
@@ -9,11 +9,11 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Removal of term ITEs
+ ** \brief Removal of term formulas
  **
- ** Removal of term ITEs.
+ ** Removal of term formulas.
  **/
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 
 #include <vector>
 
diff --git a/src/smt/ite_removal.h b/src/smt/term_formula_removal.h
index e629c93d7..09991c571 100644
--- a/src/smt/ite_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file ite_removal.h
+/*! \file term_formula_removal.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Morgan Deters, Dejan Jovanovic, Tim King
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Removal of term ITEs
+ ** \brief Removal of term formulas
  **
- ** Removal of term ITEs.
+ ** Removal of term formulas.
  **/
 
 #include "cvc4_private.h"