diff options
author | Tim King <taking@google.com> | 2015-12-30 11:45:37 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-30 11:45:37 -0800 |
commit | fa7f30a4ba08afe066604daee87006b4fb5f21f7 (patch) | |
tree | 6eecac7cce64fa00f4ac5c18f023f1bc234435a3 /src/smt | |
parent | 1ce397129214a427a10ff3e33069e315fe13eec1 (diff) |
Shuffling around public vs. private headers
- Adding a script contrib/test_install_headers.h that tests whether one can include all cvc4_public headers. CVC4 can pass this test after this commit.
- Making lib/{clock_gettime.h,ffs.h,strtok_r.h} cvc4_private.
- Making prop/sat_solver_factory.h cvc4_private.
- Moving the expr iostream manipulators into their own files: expr_iomanip.{h,cpp}.
- Setting the generated *_options.h files back to being cvc4_private.
-- Removing the usage of options/expr_options.h from expr.h.
-- Removing the include of base_options.h from options.h.
- Cleaning up CPP macros in cvc4_public headers.
-- Changing the ROLL macro in floatingpoint.h into an inline function.
-- Removing the now unused flag -D__BUILDING_STATISTICS_FOR_EXPORT.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 11 | ||||
-rw-r--r-- | src/smt/smt_options_handler.cpp | 46 |
2 files changed, 30 insertions, 27 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f2c45eab9..c1d49d8c8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -26,11 +26,8 @@ #include <utility> #include <vector> -#include "options/boolean_term_conversion_mode.h" -#include "options/decision_mode.h" #include "base/exception.h" #include "base/modal_exception.h" -#include "options/option_exception.h" #include "base/output.h" #include "context/cdhashset.h" #include "context/cdlist.h" @@ -46,12 +43,16 @@ #include "expr/resource_manager.h" #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" +#include "options/decision_mode.h" #include "options/decision_options.h" #include "options/main_options.h" +#include "options/option_exception.h" #include "options/options_handler_interface.h" #include "options/printer_options.h" #include "options/prop_options.h" @@ -65,8 +66,8 @@ #include "proof/proof.h" #include "proof/proof_manager.h" #include "proof/proof_manager.h" -#include "proof/unsat_core.h" #include "proof/theory_proof.h" +#include "proof/unsat_core.h" #include "prop/prop_engine.h" #include "smt/boolean_terms.h" #include "smt/command_list.h" @@ -74,8 +75,8 @@ #include "smt/model_postprocessor.h" #include "smt/smt_engine_scope.h" #include "smt/smt_options_handler.h" -#include "smt_util/command.h" #include "smt_util/boolean_simplification.h" +#include "smt_util/command.h" #include "smt_util/ite_removal.h" #include "smt_util/nary_builder.h" #include "smt_util/node_visitor.h" diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp index 371cdcddd..e1a19d48b 100644 --- a/src/smt/smt_options_handler.cpp +++ b/src/smt/smt_options_handler.cpp @@ -25,6 +25,7 @@ #include "base/modal_exception.h" #include "base/output.h" #include "cvc4autoconfig.h" +#include "expr/expr_iomanip.h" #include "expr/metakind.h" #include "expr/node_manager.h" #include "expr/resource_manager.h" @@ -32,6 +33,7 @@ #include "options/arith_heuristic_pivot_rule.h" #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" @@ -1219,9 +1221,9 @@ void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw( bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \ OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \ __channel_set; \ - __channel_get << Expr::dag(dagSetting); \ - __channel_get << Expr::setdepth(exprDepthSetting); \ - __channel_get << Expr::printtypes(printtypesSetting); \ + __channel_get << expr::ExprDag(dagSetting); \ + __channel_get << expr::ExprSetDepth(exprDepthSetting); \ + __channel_get << expr::ExprPrintTypes(printtypesSetting); \ __channel_get << language::SetLanguage(languageSetting); \ } @@ -1418,12 +1420,12 @@ void SmtOptionsHandler::setDefaultExprDepth(std::string option, int depth) { throw OptionException("--default-expr-depth requires a positive argument, or -1."); } - Debug.getStream() << Expr::setdepth(depth); - Trace.getStream() << Expr::setdepth(depth); - Notice.getStream() << Expr::setdepth(depth); - Chat.getStream() << Expr::setdepth(depth); - Message.getStream() << Expr::setdepth(depth); - Warning.getStream() << Expr::setdepth(depth); + Debug.getStream() << expr::ExprSetDepth(depth); + Trace.getStream() << expr::ExprSetDepth(depth); + Notice.getStream() << expr::ExprSetDepth(depth); + Chat.getStream() << expr::ExprSetDepth(depth); + Message.getStream() << expr::ExprSetDepth(depth); + Warning.getStream() << expr::ExprSetDepth(depth); // intentionally exclude Dump stream from this list } @@ -1432,22 +1434,22 @@ void SmtOptionsHandler::setDefaultDagThresh(std::string option, int dag) { throw OptionException("--default-dag-thresh requires a nonnegative argument."); } - Debug.getStream() << Expr::dag(dag); - Trace.getStream() << Expr::dag(dag); - Notice.getStream() << Expr::dag(dag); - Chat.getStream() << Expr::dag(dag); - Message.getStream() << Expr::dag(dag); - Warning.getStream() << Expr::dag(dag); - Dump.getStream() << Expr::dag(dag); + Debug.getStream() << expr::ExprDag(dag); + Trace.getStream() << expr::ExprDag(dag); + Notice.getStream() << expr::ExprDag(dag); + Chat.getStream() << expr::ExprDag(dag); + Message.getStream() << expr::ExprDag(dag); + Warning.getStream() << expr::ExprDag(dag); + Dump.getStream() << expr::ExprDag(dag); } void SmtOptionsHandler::setPrintExprTypes(std::string option) { - Debug.getStream() << Expr::printtypes(true); - Trace.getStream() << Expr::printtypes(true); - Notice.getStream() << Expr::printtypes(true); - Chat.getStream() << Expr::printtypes(true); - Message.getStream() << Expr::printtypes(true); - Warning.getStream() << Expr::printtypes(true); + Debug.getStream() << expr::ExprPrintTypes(true); + Trace.getStream() << expr::ExprPrintTypes(true); + Notice.getStream() << expr::ExprPrintTypes(true); + Chat.getStream() << expr::ExprPrintTypes(true); + Message.getStream() << expr::ExprPrintTypes(true); + Warning.getStream() << expr::ExprPrintTypes(true); // intentionally exclude Dump stream from this list } |