From 96b699bc6cccd1ade32e2d5ef73ce004063b8201 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 2 Mar 2017 15:24:07 -0600 Subject: [PATCH] Minor cleanup and reorganization related to last commit. --- src/Makefile.am | 8 +--- src/decision/decision_engine.h | 2 +- src/decision/decision_strategy.h | 2 +- src/decision/justification_heuristic.cpp | 2 +- src/options/Makefile.am | 2 - src/options/boolean_term_conversion_mode.cpp | 24 ----------- src/options/boolean_term_conversion_mode.h | 34 --------------- src/options/options_handler.cpp | 1 - src/options/options_handler.h | 1 - src/smt/boolean_terms.cpp | 42 ------------------- src/smt/boolean_terms.h | 32 -------------- src/smt/model_postprocessor.cpp | 30 ------------- src/smt/model_postprocessor.h | 31 -------------- src/smt/smt_engine.cpp | 19 +-------- ...e_removal.cpp => term_formula_removal.cpp} | 8 ++-- .../{ite_removal.h => term_formula_removal.h} | 6 +-- src/theory/datatypes/theory_datatypes.cpp | 1 - src/theory/quantifiers/ceg_instantiator.cpp | 2 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 2 +- src/theory/theory_engine.cpp | 2 +- 20 files changed, 16 insertions(+), 235 deletions(-) delete mode 100644 src/options/boolean_term_conversion_mode.cpp delete mode 100644 src/options/boolean_term_conversion_mode.h delete mode 100644 src/smt/boolean_terms.cpp delete mode 100644 src/smt/boolean_terms.h delete mode 100644 src/smt/model_postprocessor.cpp delete mode 100644 src/smt/model_postprocessor.h rename src/smt/{ite_removal.cpp => term_formula_removal.cpp} (98%) rename src/smt/{ite_removal.h => term_formula_removal.h} (96%) 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 - -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 - -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 -#include -#include -#include -#include - -#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 -#include - -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 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 similarity index 98% rename from src/smt/ite_removal.cpp rename to 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 diff --git a/src/smt/ite_removal.h b/src/smt/term_formula_removal.h similarity index 96% rename from src/smt/ite_removal.h rename to 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" -- 2.30.2