summaryrefslogtreecommitdiff
path: root/src/options/options_handler.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-10-18 19:37:11 -0500
committerGitHub <noreply@github.com>2018-10-18 19:37:11 -0500
commit547bd91e189b28da9950e12037d1e88079157479 (patch)
tree7f225e6df081071028c9e6102c902a6224179edf /src/options/options_handler.h
parent10707e3ec6f2cab793919f2d1a159e13cdd032a9 (diff)
Non-implied mode for model cores (#2653)
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 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback