diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
commit | f47f24528f5d19ac0affd572f3d34c090e97f9f9 (patch) | |
tree | 6a21c1964d862f99d9137f968881a0da33c59d1d /src/options/options_handler.h | |
parent | 793361d81f0766c6a28ff699ed5447d9b8f8c123 (diff) |
Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.
Diffstat (limited to 'src/options/options_handler.h')
-rw-r--r-- | src/options/options_handler.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 9aa037004..a2d67be60 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Andrew Reynolds ** 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 @@ -100,6 +100,7 @@ public: theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException); // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value) throw(OptionException); @@ -199,6 +200,7 @@ public: 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_mbqiModeHelp; static const std::string s_modelFormatHelp; static const std::string s_prenexQuantModeHelp; |