diff options
Diffstat (limited to 'src/options/options_handler.h')
| -rw-r--r-- | src/options/options_handler.h | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 16ddbce4d..84b7002e3 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__OPTIONS__OPTIONS_HANDLER_H -#define __CVC4__OPTIONS__OPTIONS_HANDLER_H +#ifndef CVC4__OPTIONS__OPTIONS_HANDLER_H +#define CVC4__OPTIONS__OPTIONS_HANDLER_H #include <ostream> #include <string> @@ -37,7 +37,7 @@ #include "options/printer_modes.h" #include "options/quantifiers_modes.h" #include "options/smt_modes.h" -#include "options/strings_process_loop_mode.h" +#include "options/strings_modes.h" #include "options/sygus_out_mode.h" #include "options/theoryof_mode.h" #include "options/ufss_mode.h" @@ -114,6 +114,8 @@ public: 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( @@ -148,9 +150,13 @@ public: theory::bv::BvProofFormat stringToBvProofFormat(std::string option, std::string optarg); + theory::bv::BvOptimizeSatProof stringToBvOptimizeSatProof(std::string option, + std::string optarg); theory::strings::ProcessLoopMode stringToStringsProcessLoopMode( std::string option, std::string optarg); + theory::strings::RegExpInterMode stringToRegExpInterMode(std::string option, + std::string optarg); // theory/uf/options_handlers.h theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg); @@ -172,9 +178,6 @@ public: decision::DecisionWeightInternal stringToDecisionWeightInternal( std::string option, std::string optarg); - /* smt/options_handlers.h */ - void notifyForceLogic(const std::string& option); - /** * Throws a ModalException if this option is being set after final * initialization. @@ -184,6 +187,8 @@ public: 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); @@ -238,9 +243,11 @@ public: 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_stringToStringsProcessLoopModeHelp; + 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; @@ -258,11 +265,13 @@ public: 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; @@ -283,4 +292,4 @@ public: }/* CVC4::options namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__OPTIONS_HANDLER_H */ +#endif /* CVC4__OPTIONS__OPTIONS_HANDLER_H */ |