4 files changed, 44 insertions, 4 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index f214b032c..152e22f14 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -428,7 +428,7 @@ post \n\
 ";
 
 const std::string OptionsHandler::s_macrosQuantHelp = "\
-Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
+Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
 \n\
 all \n\
 + Infer definitions for functions, including those containing quantified formulas.\n\
@@ -442,7 +442,7 @@ ground-uf \n\
 ";
 
 const std::string OptionsHandler::s_quantDSplitHelp = "\
-Template modes for quantifiers splitting, supported by --quant-split:\n\
+Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\
 \n\
 none \n\
 + Never split quantified formulas.\n\
@@ -455,6 +455,20 @@ agg \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_quantRepHelp = "\
+Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\
+\n\
+ee \n\
++ Let equality engine choose representatives.\n\
+\n\
+first (default) \n\
++ Choose terms that appear first.\n\
+\n\
+depth \n\
++ Choose terms that are of minimal depth.\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;
@@ -716,6 +730,22 @@ theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std
   }
 }
 
+theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none" ) {
+    return theory::quantifiers::QUANT_REP_MODE_EE;
+  } else if(optarg == "first" || optarg == "default") {
+    return theory::quantifiers::QUANT_REP_MODE_FIRST;
+  } else if(optarg == "depth") {
+    return theory::quantifiers::QUANT_REP_MODE_DEPTH;
+  } else if(optarg ==  "help") {
+    puts(s_quantRepHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
+                          optarg + "'.  Try --quant-rep-mode help.");
+  }
+}
+
 // theory/bv/options_handlers.h
 void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) {
 #ifndef CVC4_USE_ABC
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index a2d67be60..720889ca2 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -101,6 +101,7 @@ public:
   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::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException);
 
   // theory/bv/options_handlers.h
   void abcEnabledBuild(std::string option, bool value) throw(OptionException);
@@ -201,6 +202,7 @@ public:
   static const std::string s_literalMatchHelp;
   static const std::string s_macrosQuantHelp;
   static const std::string s_quantDSplitHelp;
+  static const std::string s_quantRepHelp;
   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 7395a9a30..8aa3756cc 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -172,6 +172,14 @@ enum QuantDSplitMode {
   QUANT_DSPLIT_MODE_AGG,
 };
 
+enum QuantRepMode {
+  /** let equality engine choose representatives */
+  QUANT_REP_MODE_EE,
+  /** default, choose representatives that appear first */
+  QUANT_REP_MODE_FIRST,
+  /** choose representatives that have minimal depth */
+  QUANT_REP_MODE_DEPTH,
+};
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cba1423a0..58367f2e2 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -100,8 +100,8 @@ option instMaxLevel --inst-max-level=N int :read-write :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
 option instLevelInputOnly --inst-level-input-only bool :default true
  only input terms are assigned instantiation level zero
-option internalReps --quant-internal-reps bool :default true
- instantiate with representatives chosen by quantifiers engine
+option quantRepMode --quant-rep-mode=MODE  CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode
+ selection mode for representatives in quantifiers engine
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly