summaryrefslogtreecommitdiff
path: root/src/options/options_handler.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-02-18 22:50:05 -0600
committerajreynol <andrew.j.reynolds@gmail.com>2016-02-18 22:50:05 -0600
commitf47f24528f5d19ac0affd572f3d34c090e97f9f9 (patch)
tree6a21c1964d862f99d9137f968881a0da33c59d1d /src/options/options_handler.h
parent793361d81f0766c6a28ff699ed5447d9b8f8c123 (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.h4
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback