Minor cleanup and reorganization related to last commit.

20 files changed, 16 insertions, 235 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 2ee777afe..c05065c35 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -117,16 +117,14 @@ libcvc4_la_SOURCES = \
 	prop/cryptominisat.cpp \
 	prop/theory_proxy.cpp \
 	prop/theory_proxy.h \
-	smt/boolean_terms.cpp \
-	smt/boolean_terms.h \
 	smt/command.cpp \
 	smt/command.h \
 	smt/command_list.cpp \
 	smt/command_list.h \
 	smt/dump.cpp \
 	smt/dump.h \
-	smt/ite_removal.cpp \
-	smt/ite_removal.h \
+	smt/term_formula_removal.cpp \
+	smt/term_formula_removal.h \
 	smt/logic_exception.h \
 	smt/logic_request.cpp \
 	smt/logic_request.h \
@@ -134,8 +132,6 @@ libcvc4_la_SOURCES = \
 	smt/managed_ostreams.h \
 	smt/model.cpp \
 	smt/model.h \
-	smt/model_postprocessor.cpp \
-	smt/model_postprocessor.h \
 	smt/smt_engine.cpp \
 	smt/smt_engine.h \
 	smt/smt_engine_check_proof.cpp \
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 92d203cb3..66293d7ad 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -27,7 +27,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/sat_solver_types.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 #include "smt/smt_engine_scope.h"
 
 using namespace std;
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 591f018d8..5c3b01bef 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -20,7 +20,7 @@
 #define __CVC4__DECISION__DECISION_STRATEGY_H
 
 #include "prop/sat_solver_types.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 
 namespace CVC4 {
 
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index c0d65cbe6..ded2cad15 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -22,7 +22,7 @@
 #include "expr/node_manager.h"
 #include "options/decision_options.h"
 #include "theory/rewriter.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 #include "smt/smt_statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 1eb84b45f..31330a97c 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -216,8 +216,6 @@ liboptions_la_SOURCES = \
 	argument_extender_implementation.h \
 	argument_extender.h \
 	base_handlers.h \
-	boolean_term_conversion_mode.cpp \
-	boolean_term_conversion_mode.h \
 	bv_bitblast_mode.cpp \
 	bv_bitblast_mode.h \
 	decision_mode.cpp \
diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp
deleted file mode 100644
index 4fc9b1f8d..000000000
--- a/src/options/boolean_term_conversion_mode.cpp
+++ /dev/null
@@ -1,24 +0,0 @@
-/*********************                                                        */
-/*! \file boolean_term_conversion_mode.cpp
- ** \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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-#include "options/boolean_term_conversion_mode.h"
-
-#include <iostream>
-
-namespace CVC4 {
-
-
-}/* CVC4 namespace */
diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h
deleted file mode 100644
index 57e2ccaf4..000000000
--- a/src/options/boolean_term_conversion_mode.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*********************                                                        */
-/*! \file boolean_term_conversion_mode.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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
-#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
-
-#include <iosfwd>
-
-namespace CVC4 {
-namespace theory {
-namespace booleans {
-
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index c0aa67cd4..94bf15540 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -32,7 +32,6 @@
 #include "options/arith_propagation_mode.h"
 #include "options/arith_unate_lemma_mode.h"
 #include "options/base_options.h"
-#include "options/boolean_term_conversion_mode.h"
 #include "options/bv_bitblast_mode.h"
 #include "options/bv_options.h"
 #include "options/decision_mode.h"
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 248f15c98..6721eaa2b 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -27,7 +27,6 @@
 #include "options/arith_propagation_mode.h"
 #include "options/arith_unate_lemma_mode.h"
 #include "options/base_handlers.h"
-#include "options/boolean_term_conversion_mode.h"
 #include "options/bv_bitblast_mode.h"
 #include "options/decision_mode.h"
 #include "options/language.h"
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"
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8d2e5618f..b66cb15ff 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -23,7 +23,6 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
-#include "smt/boolean_terms.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 3dacfca3a..adce94b5c 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -16,7 +16,7 @@
 #include "theory/quantifiers/ceg_t_instantiator.h"
 
 #include "options/quantifiers_options.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 0023f7d0f..1f1837740 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -14,7 +14,7 @@
 #include "theory/quantifiers/inst_strategy_cbqi.h"
 
 #include "options/quantifiers_options.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7c1b02f47..4054350aa 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -31,7 +31,7 @@
 #include "proof/lemma_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
-#include "smt/ite_removal.h"
+#include "smt/term_formula_removal.h"
 #include "smt/logic_exception.h"
 #include "smt_util/lemma_output_channel.h"
 #include "smt_util/node_visitor.h"