Non-implied mode for model cores (#2653)

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"