diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-18 19:37:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-18 19:37:11 -0500 |
commit | 547bd91e189b28da9950e12037d1e88079157479 (patch) | |
tree | 7f225e6df081071028c9e6102c902a6224179edf /src/options | |
parent | 10707e3ec6f2cab793919f2d1a159e13cdd032a9 (diff) |
Non-implied mode for model cores (#2653)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/options/Makefile.am | 4 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 47 | ||||
-rw-r--r-- | src/options/options_handler.h | 4 | ||||
-rw-r--r-- | src/options/smt_modes.cpp (renamed from src/options/simplification_mode.cpp) | 23 | ||||
-rw-r--r-- | src/options/smt_modes.h (renamed from src/options/simplification_mode.h) | 41 | ||||
-rw-r--r-- | src/options/smt_options.toml | 15 |
7 files changed, 100 insertions, 38 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 457fd23cd..dd0e34578 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -32,8 +32,8 @@ libcvc4_add_sources( quantifiers_modes.h set_language.cpp set_language.h - simplification_mode.cpp - simplification_mode.h + smt_modes.cpp + smt_modes.h sygus_out_mode.h theoryof_mode.cpp theoryof_mode.h diff --git a/src/options/Makefile.am b/src/options/Makefile.am index c311e04d8..54047efcc 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -96,8 +96,8 @@ liboptions_la_SOURCES = \ quantifiers_modes.h \ set_language.cpp \ set_language.h \ - simplification_mode.cpp \ - simplification_mode.h \ + smt_modes.cpp \ + smt_modes.h \ sygus_out_mode.h \ theoryof_mode.cpp \ theoryof_mode.h \ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index be2d7883d..46663ce7c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -42,8 +42,6 @@ #include "options/language.h" #include "options/option_exception.h" #include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "options/theoryof_mode.h" @@ -1472,6 +1470,51 @@ SimplificationMode OptionsHandler::stringToSimplificationMode( } } +const std::string OptionsHandler::s_modelCoresHelp = + "\ +Model cores modes currently supported by the --simplification option:\n\ +\n\ +none (default) \n\ ++ do not compute model cores\n\ +\n\ +simple\n\ ++ only include a subset of variables whose values are sufficient to show the\n\ +input formula is satisfied by the given model\n\ +\n\ +non-implied\n\ ++ only include a subset of variables whose values, in addition to the values\n\ +of variables whose values are implied, are sufficient to show the input\n\ +formula is satisfied by the given model\n\ +\n\ +"; + +ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return MODEL_CORES_NONE; + } + else if (optarg == "simple") + { + return MODEL_CORES_SIMPLE; + } + else if (optarg == "non-implied") + { + return MODEL_CORES_NON_IMPLIED; + } + else if (optarg == "help") + { + puts(s_modelCoresHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --model-cores: `") + + optarg + "'. Try --model-cores help."); + } +} + const std::string OptionsHandler::s_sygusSolutionOutModeHelp = "\ Modes for finite model finding bound minimization, supported by --sygus-out:\n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 0205b0b73..3078db0f8 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -35,7 +35,7 @@ #include "options/options.h" #include "options/printer_modes.h" #include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" +#include "options/smt_modes.h" #include "options/sygus_out_mode.h" #include "options/theoryof_mode.h" #include "options/ufss_mode.h" @@ -171,6 +171,7 @@ public: void notifyDumpMode(std::string option); SimplificationMode stringToSimplificationMode(std::string option, std::string optarg); + ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg); SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option, std::string optarg); void setProduceAssertions(std::string option, bool value); @@ -241,6 +242,7 @@ public: 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_sygusSolutionOutModeHelp; static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; diff --git a/src/options/simplification_mode.cpp b/src/options/smt_modes.cpp index 6b6fc842d..4a2fd404c 100644 --- a/src/options/simplification_mode.cpp +++ b/src/options/smt_modes.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file simplification_mode.cpp +/*! \file smt_modes.cpp ** \verbatim ** Top contributors (to current version): ** Morgan Deters, Tim King @@ -15,25 +15,22 @@ ** \todo document this file **/ -#include "options/simplification_mode.h" +#include "options/smt_modes.h" #include <iostream> namespace CVC4 { -std::ostream& operator<<(std::ostream& out, SimplificationMode mode) { - switch(mode) { - case SIMPLIFICATION_MODE_BATCH: - out << "SIMPLIFICATION_MODE_BATCH"; - break; - case SIMPLIFICATION_MODE_NONE: - out << "SIMPLIFICATION_MODE_NONE"; - break; - default: - out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; +std::ostream& operator<<(std::ostream& out, SimplificationMode mode) +{ + switch (mode) + { + case SIMPLIFICATION_MODE_BATCH: out << "SIMPLIFICATION_MODE_BATCH"; break; + case SIMPLIFICATION_MODE_NONE: out << "SIMPLIFICATION_MODE_NONE"; break; + default: out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; } return out; } -}/* CVC4 namespace */ +} // namespace CVC4 diff --git a/src/options/simplification_mode.h b/src/options/smt_modes.h index 52bf25fa1..761f3be01 100644 --- a/src/options/simplification_mode.h +++ b/src/options/smt_modes.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file simplification_mode.h +/*! \file smt_modes.h ** \verbatim ** Top contributors (to current version): ** Morgan Deters, Tim King @@ -17,23 +17,42 @@ #include "cvc4_public.h" -#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H -#define __CVC4__SMT__SIMPLIFICATION_MODE_H +#ifndef __CVC4__SMT__MODES_H +#define __CVC4__SMT__MODES_H #include <iosfwd> namespace CVC4 { /** Enumeration of simplification modes (when to simplify). */ -typedef enum { +enum SimplificationMode +{ /** Simplify the assertions all together once a check is requested */ SIMPLIFICATION_MODE_BATCH, /** Don't do simplification */ SIMPLIFICATION_MODE_NONE -} SimplificationMode; - -std::ostream& operator<<(std::ostream& out, SimplificationMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__SIMPLIFICATION_MODE_H */ +}; + +std::ostream& operator<<(std::ostream& out, + SimplificationMode mode) CVC4_PUBLIC; + +/** Enumeration of model core modes. */ +enum ModelCoresMode +{ + /** Do not compute model cores */ + MODEL_CORES_NONE, + /** + * Compute "simple" model cores that exclude variables that do not + * contribute to satisfying the input. + */ + MODEL_CORES_SIMPLE, + /** + * Compute model cores that also exclude variables whose variables are implied + * by others. + */ + MODEL_CORES_NON_IMPLIED +}; + +} // namespace CVC4 + +#endif /* __CVC4__SMT__MODES_H */ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 8af1000ba..e0041774a 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -40,7 +40,7 @@ header = "options/smt_options.h" type = "SimplificationMode" default = "SIMPLIFICATION_MODE_BATCH" handler = "stringToSimplificationMode" - includes = ["options/simplification_mode.h"] + includes = ["options/smt_modes.h"] help = "choose simplification mode, see --simplification=help" [[alias]] @@ -99,13 +99,14 @@ header = "options/smt_options.h" help = "output models after every SAT/INVALID/UNKNOWN response" [[option]] - name = "produceModelCores" + name = "modelCoresMode" category = "regular" - long = "produce-model-cores" - type = "bool" - default = "false" - read_only = true - help = "when printing models, compute a minimal core of relevant definitions" + long = "model-cores=MODE" + type = "ModelCoresMode" + default = "MODEL_CORES_NONE" + handler = "stringToModelCoresMode" + includes = ["options/smt_modes.h"] + help = "mode for producing model cores" [[option]] name = "proof" |