summaryrefslogtreecommitdiff
path: root/src/smt/smt_options_handler.h
diff options
context:
space:
mode:
authorTim King <taking@google.com>2015-12-14 18:51:40 -0800
committerTim King <taking@google.com>2015-12-14 18:51:40 -0800
commit90e3b73fbd1b2eb262a7a7e2e72d701c8f9e3600 (patch)
tree77af58f4233d766d31e8e032e16cc0b4833d8de2 /src/smt/smt_options_handler.h
parent157a2ed349418611302476dce79fced1d95a4ecc (diff)
Refactoring Options Handler & Library Cycle Breaking
What to Know As a User: A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems. The Problem: The build order of CVC4 used to be [roughly] specified as: options < expr < util < libcvc4 < parsers < main Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable. The Solution: To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen: 1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file. 2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options. 3. All of the old options_handlers.h files have been refactored. 4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary. 5. I am removing the libstatistics library. The constraints that the CVC4 build system will eventually satisfy are: - The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files. - The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases. - The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.) - One library per Makefile.am. - No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.) The build order of CVC4 can now be [roughly] specified as base < options < util < expr < smt_util < libcvc4 < parsers < main The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean. More details about the directories: base/ The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere. options/ The options/ directory is self contained. - It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h . - There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options. - Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done. - The */options_handlers.h files have been removed. - The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp. - All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h . util/ The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean. expr/ The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/. - An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h. - Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h. - The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/. - Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes. - Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources. - This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC. smt_util/ The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel. What is up next: - A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed. - The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.
Diffstat (limited to 'src/smt/smt_options_handler.h')
-rw-r--r--src/smt/smt_options_handler.h198
1 files changed, 198 insertions, 0 deletions
diff --git a/src/smt/smt_options_handler.h b/src/smt/smt_options_handler.h
new file mode 100644
index 000000000..c4d27a722
--- /dev/null
+++ b/src/smt/smt_options_handler.h
@@ -0,0 +1,198 @@
+/********************* */
+/*! \file options_handler_interface.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Interface for custom handlers and predicates options.
+ **
+ ** Interface for custom handlers and predicates options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__SMT__SMT_OPTIONS_HANDLER_H
+#define __CVC4__SMT__SMT_OPTIONS_HANDLER_H
+
+#include <ostream>
+#include <string>
+
+#include "base/modal_exception.h"
+#include "options/arith_heuristic_pivot_rule.h"
+#include "options/arith_propagation_mode.h"
+#include "options/arith_unate_lemma_mode.h"
+#include "options/boolean_term_conversion_mode.h"
+#include "options/bv_bitblast_mode.h"
+#include "options/decision_mode.h"
+#include "options/language.h"
+#include "options/option_exception.h"
+#include "options/options_handler_interface.h"
+#include "options/printer_modes.h"
+#include "options/quantifiers_modes.h"
+#include "options/simplification_mode.h"
+#include "options/theoryof_mode.h"
+#include "options/ufss_mode.h"
+#include "smt/smt_engine.h"
+#include "theory/logic_info.h"
+
+namespace CVC4 {
+namespace smt {
+
+class CVC4_PUBLIC SmtOptionsHandler : public options::OptionsHandler {
+public:
+ SmtOptionsHandler(SmtEngine* smt);
+ ~SmtOptionsHandler();
+
+ // TODO
+ // theory/arith/options_handlers.h
+ // theory/quantifiers/options_handlers.h
+ // theory/bv/options_handlers.h
+ // theory/booleans/options_handlers.h
+ // theory/uf/options_handlers.h
+ // theory/options_handlers.h
+ // printer/options_handlers.h
+ // decision/options_handlers.h
+ // smt/options_handlers.h
+ // expr/options_handlers.h
+ // main/options_handlers.h
+ // options/base_options_handlers.h
+
+ // theory/arith/options_handlers.h
+ virtual ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException);
+ virtual ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException);
+ virtual ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException);
+
+ // theory/quantifiers/options_handlers.h
+ virtual theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException);
+ virtual void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException);
+ virtual theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException);
+ virtual void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException);
+ virtual theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException);
+ virtual void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException);
+ virtual theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
+
+ // theory/bv/options_handlers.h
+ virtual void abcEnabledBuild(std::string option, bool value) throw(OptionException);
+ virtual void abcEnabledBuild(std::string option, std::string value) throw(OptionException);
+ virtual theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException);
+ virtual theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException);
+ virtual void setBitblastAig(std::string option, bool arg) throw(OptionException);
+
+
+ // theory/booleans/options_handlers.h
+ virtual theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException);
+
+ // theory/uf/options_handlers.h
+ virtual theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException);
+
+ // theory/options_handlers.h
+ virtual theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg);
+ virtual void useTheory(std::string option, std::string optarg);
+
+
+ // printer/options_handlers.h
+ virtual ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException);
+ virtual InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException);
+
+ // decision/options_handlers.h
+ virtual decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException);
+ virtual decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException);
+
+
+ // smt/options_handlers.h
+ virtual void dumpMode(std::string option, std::string optarg);
+ virtual LogicInfo* stringToLogicInfo(std::string option, std::string optarg) throw(OptionException);
+ virtual SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
+ virtual void beforeSearch(std::string option, bool value) throw(ModalException);
+ virtual void setProduceAssertions(std::string option, bool value) throw();
+ virtual void proofEnabledBuild(std::string option, bool value) throw(OptionException);
+ virtual void dumpToFile(std::string option, std::string optarg);
+ virtual void setRegularOutputChannel(std::string option, std::string optarg);
+ virtual void setDiagnosticOutputChannel(std::string option, std::string optarg);
+ virtual std::string checkReplayFilename(std::string option, std::string optarg);
+ virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg);
+ virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException);
+ virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException);
+ virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
+ virtual unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException);
+ virtual unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
+
+ /* expr/options_handlers.h */
+ virtual void setDefaultExprDepth(std::string option, int depth);
+ virtual void setDefaultDagThresh(std::string option, int dag);
+ virtual void setPrintExprTypes(std::string option);
+
+ /* main/options_handlers.h */
+ virtual void showConfiguration(std::string option);
+ virtual void showDebugTags(std::string option);
+ virtual void showTraceTags(std::string option);
+ virtual void threadN(std::string option);
+
+ /* options/base_options_handlers.h */
+ virtual void setVerbosity(std::string option, int value) throw(OptionException);
+ virtual void increaseVerbosity(std::string option);
+ virtual void decreaseVerbosity(std::string option);
+ virtual OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException);
+ virtual InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) ;
+ virtual void addTraceTag(std::string option, std::string optarg);
+ virtual void addDebugTag(std::string option, std::string optarg);
+ virtual void setPrintSuccess(std::string option, bool value);
+
+private:
+ SmtEngine* d_smtEngine;
+
+ /* Helper utilities */
+ static std::string suggestTags(char const* const* validTags, std::string inputTag,
+ char const* const* additionalTags = NULL);
+ static std::string __cvc4_errno_failreason();
+
+ /* Help strings */
+ static const std::string s_bitblastingModeHelp;
+ static const std::string s_booleanTermConversionModeHelp;
+ static const std::string s_bvSlicerModeHelp;
+ static const std::string s_cegqiFairModeHelp;
+ static const std::string s_decisionModeHelp;
+ static const std::string s_dumpHelp;
+ static const std::string s_instFormatHelp ;
+ static const std::string s_instWhenHelp;
+ static const std::string s_iteLiftQuantHelp;
+ static const std::string s_literalMatchHelp;
+ static const std::string s_macrosQuantHelp;
+ static const std::string s_mbqiModeHelp;
+ static const std::string s_modelFormatHelp;
+ static const std::string s_prenexQuantModeHelp;
+ static const std::string s_qcfModeHelp;
+ static const std::string s_qcfWhenModeHelp;
+ static const std::string s_simplificationHelp;
+ static const std::string s_sygusInvTemplHelp;
+ static const std::string s_termDbModeHelp;
+ static const std::string s_theoryOfModeHelp;
+ static const std::string s_triggerSelModeHelp;
+ static const std::string s_ufssModeHelp;
+ static const std::string s_userPatModeHelp;
+ static const std::string s_errorSelectionRulesHelp;
+ static const std::string s_arithPropagationModeHelp;
+ static const std::string s_arithUnateLemmasHelp;
+
+
+}; /* class SmtOptionsHandler */
+
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SMT_OPTIONS_HANDLER_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback