Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.

1 files changed, 20 insertions, 161 deletions

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 2e372a00c..a395bb453 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -23,24 +23,14 @@
 #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/base_handlers.h"
-#include "options/bool_to_bv_mode.h"
-#include "options/bv_bitblast_mode.h"
-#include "options/datatypes_modes.h"
-#include "options/decision_mode.h"
+#include "options/bv_options.h"
+#include "options/decision_options.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
 #include "options/printer_modes.h"
-#include "options/quantifiers_modes.h"
-#include "options/smt_modes.h"
-#include "options/strings_modes.h"
-#include "options/sygus_out_mode.h"
-#include "options/theoryof_mode.h"
-#include "options/ufss_mode.h"
+#include "options/quantifiers_options.h"
 
 namespace CVC4 {
 namespace options {
@@ -70,117 +60,29 @@ public:
     options::less_equal(1.0)(option, value);
   }
 
-  // theory/arith/options_handlers.h
-  ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option,
-                                                  std::string optarg);
-  ArithPropagationMode stringToArithPropagationMode(std::string option,
-                                                    std::string optarg);
-  ErrorSelectionRule stringToErrorSelectionRule(std::string option,
-                                                std::string optarg);
-
   // theory/quantifiers/options_handlers.h
-  theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option,
-                                                         std::string optarg);
-  void checkInstWhenMode(std::string option,
-                         theory::quantifiers::InstWhenMode mode);
-  theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(
-      std::string option, std::string optarg);
-  void checkLiteralMatchMode(std::string option,
-                             theory::quantifiers::LiteralMatchMode mode);
-  theory::quantifiers::MbqiMode stringToMbqiMode(std::string option,
-                                                 std::string optarg);
-  void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode);
-  theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option,
-                                                       std::string optarg);
-  theory::quantifiers::QcfMode stringToQcfMode(std::string option,
-                                               std::string optarg);
-  theory::quantifiers::UserPatMode stringToUserPatMode(std::string option,
-                                                       std::string optarg);
-  theory::quantifiers::TriggerSelMode stringToTriggerSelMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::TermDbMode stringToTermDbMode(std::string option,
-                                                     std::string optarg);
-  theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::CbqiBvIneqMode stringToCbqiBvIneqMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::CegisSampleMode stringToCegisSampleMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::SygusUnifPiMode stringToSygusUnifPiMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(
-      std::string option, std::string optarg);
-  theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option,
-                                                         std::string optarg);
-  theory::SygusFairMode stringToSygusFairMode(std::string option,
-                                              std::string optarg);
+  void checkInstWhenMode(std::string option, InstWhenMode mode);
 
   // theory/bv/options_handlers.h
   void abcEnabledBuild(std::string option, bool value);
   void abcEnabledBuild(std::string option, std::string value);
-  void satSolverEnabledBuild(std::string option, bool value);
-  void satSolverEnabledBuild(std::string option, std::string optarg);
-
-  theory::bv::BitblastMode stringToBitblastMode(std::string option,
-                                                std::string optarg);
-  theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option,
-                                                std::string optarg);
-  preprocessing::passes::BoolToBVMode stringToBoolToBVMode(std::string option,
-                                                           std::string optarg);
-  void setBitblastAig(std::string option, bool arg);
-
-  theory::bv::SatSolverMode stringToSatSolver(std::string option,
-                                              std::string optarg);
 
-  theory::bv::BvProofFormat stringToBvProofFormat(std::string option,
-                                                  std::string optarg);
-  theory::bv::BvOptimizeSatProof stringToBvOptimizeSatProof(std::string option,
-                                                            std::string optarg);
+  template<class T> void checkSatSolverEnabled(std::string option, T m);
 
-  theory::strings::ProcessLoopMode stringToStringsProcessLoopMode(
-      std::string option, std::string optarg);
-  theory::strings::RegExpInterMode stringToRegExpInterMode(std::string option,
-                                                           std::string optarg);
+  void checkBvSatSolver(std::string option, SatSolverMode m);
+  void checkBitblastMode(std::string option, BitblastMode m);
 
-  // theory/uf/options_handlers.h
-  theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg);
+  void setBitblastAig(std::string option, bool arg);
 
   // theory/options_handlers.h
-  theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg);
   void notifyUseTheoryList(std::string option);
   std::string handleUseTheoryList(std::string option, std::string optarg);
 
-
   // printer/options_handlers.h
-  ModelFormatMode stringToModelFormatMode(std::string option,
-                                          std::string optarg);
   InstFormatMode stringToInstFormatMode(std::string option, std::string optarg);
 
   // decision/options_handlers.h
-  decision::DecisionMode stringToDecisionMode(std::string option,
-                                              std::string optarg);
-  decision::DecisionWeightInternal stringToDecisionWeightInternal(
-      std::string option, std::string optarg);
+  void setDecisionModeStopOnly(std::string option, DecisionMode m);
 
   /**
    * Throws a ModalException if this option is being set after final
@@ -188,13 +90,6 @@ public:
    */
   void notifyBeforeSearch(const std::string& option);
   void notifyDumpMode(std::string option);
-  SimplificationMode stringToSimplificationMode(std::string option,
-                                                std::string optarg);
-  ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg);
-  BlockModelsMode stringToBlockModelsMode(std::string option,
-                                          std::string optarg);
-  SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option,
-                                                    std::string optarg);
   void setProduceAssertions(std::string option, bool value);
   void proofEnabledBuild(std::string option, bool value);
   void LFSCEnabledBuild(std::string option, bool value);
@@ -244,56 +139,20 @@ public:
   Options* d_options;
 
   /* Help strings */
-  static const std::string s_bitblastingModeHelp;
-  static const std::string s_bvSatSolverHelp;
-  static const std::string s_bvProofFormatHelp;
-  static const std::string s_bvOptimizeSatProofHelp;
-  static const std::string s_booleanTermConversionModeHelp;
-  static const std::string s_bvSlicerModeHelp;
-  static const std::string s_stringsProcessLoopModeHelp;
-  static const std::string s_regExpInterModeHelp;
-  static const std::string s_boolToBVModeHelp;
-  static const std::string s_cegqiFairModeHelp;
-  static const std::string s_decisionModeHelp;
-  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_quantDSplitHelp;
-  static const std::string s_quantRepHelp;
-  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_modelCoresHelp;
-  static const std::string s_blockModelsHelp;
-  static const std::string s_sygusSolutionOutModeHelp;
-  static const std::string s_cbqiBvIneqModeHelp;
-  static const std::string s_cegqiSingleInvHelp;
-  static const std::string s_cegqiSingleInvRconsHelp;
-  static const std::string s_cegisSampleHelp;
-  static const std::string s_sygusQueryDumpFileHelp;
-  static const std::string s_sygusFilterSolHelp;
-  static const std::string s_sygusInvTemplHelp;
-  static const std::string s_sygusActiveGenHelp;
-  static const std::string s_sygusUnifPiHelp;
-  static const std::string s_sygusGrammarConsHelp;
-  static const std::string s_termDbModeHelp;
-  static const std::string s_theoryOfModeHelp;
-  static const std::string s_triggerSelModeHelp;
-  static const std::string s_triggerActiveSelModeHelp;
-  static const std::string s_ufssModeHelp;
-  static const std::string s_userPatModeHelp;
-  static const std::string s_fmfBoundMinModeModeHelp;
-  static const std::string s_errorSelectionRulesHelp;
-  static const std::string s_arithPropagationModeHelp;
-  static const std::string s_arithUnateLemmasHelp;
+  static const std::string s_instFormatHelp;
 
 }; /* class OptionHandler */
 
+template<class T>
+void OptionsHandler::checkSatSolverEnabled(std::string option, T m)
+{
+#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
+  std::stringstream ss;
+  ss << "option `" << option
+     << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL";
+  throw OptionException(ss.str());
+#endif
+}
 
 }/* CVC4::options namespace */
 }/* CVC4 namespace */