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 | |
parent | 793361d81f0766c6a28ff699ed5447d9b8f8c123 (diff) |
Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options_handler.cpp | 29 | ||||
-rw-r--r-- | src/options/options_handler.h | 4 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 10 | ||||
-rw-r--r-- | src/options/quantifiers_options | 2 |
4 files changed, 44 insertions, 1 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1c48f4bb1..f214b032c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -441,6 +441,20 @@ ground-uf \n\ \n\ "; +const std::string OptionsHandler::s_quantDSplitHelp = "\ +Template modes for quantifiers splitting, supported by --quant-split:\n\ +\n\ +none \n\ ++ Never split quantified formulas.\n\ +\n\ +default \n\ ++ Split quantified formulas over some finite datatypes when finite model finding is enabled.\n\ +\n\ +agg \n\ ++ Aggressively split quantified formulas.\n\ +\n\ +"; + theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "pre-full") { return theory::quantifiers::INST_WHEN_PRE_FULL; @@ -686,6 +700,21 @@ theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std } } +theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::QUANT_DSPLIT_MODE_NONE; + } else if(optarg == "default") { + return theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT; + } else if(optarg == "agg") { + return theory::quantifiers::QUANT_DSPLIT_MODE_AGG; + } else if(optarg == "help") { + puts(s_quantDSplitHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") + + optarg + "'. Try --quant-dsplit-mode help."); + } +} // theory/bv/options_handlers.h void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) { 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; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 540db38ec..7395a9a30 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -163,6 +163,16 @@ enum MacrosQuantMode { MACROS_QUANT_MODE_GROUND_UF, }; +enum QuantDSplitMode { + /** never do quantifiers splitting */ + QUANT_DSPLIT_MODE_NONE, + /** default */ + QUANT_DSPLIT_MODE_DEFAULT, + /** do quantifiers splitting aggressively */ + QUANT_DSPLIT_MODE_AGG, +}; + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index f5a6ee843..cba1423a0 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -283,6 +283,8 @@ option macrosQuant --macros-quant bool :read-write :default false perform quantifiers macro expansion option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler stringToMacrosQuantMode mode for quantifiers macro expansion +option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode + mode for dynamic quantifiers splitting ### recursive function options |