4 files changed, 54 insertions, 4 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index cbef7109f..867feef6e 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -425,6 +425,24 @@ all \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_cegqiSingleInvHelp = "\
+Modes for single invocation techniques, supported by --cegqi-si:\n\
+\n\
+none  \n\
++ Do not use single invocation techniques.\n\
+\n\
+use (default) \n\
++ Use single invocation techniques only if grammar is not restrictive.\n\
+\n\
+all-abort  \n\
++ Always use single invocation techniques, abort if solution reconstruction will likely fail,\
+  for instance, when the grammar does not have ITE and solution requires it.\n\
+\n\
+all \n\
++ Always use single invocation techniques. \n\
+\n\
+";
+
 const std::string OptionsHandler::s_sygusInvTemplHelp = "\
 Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
 \n\
@@ -700,6 +718,24 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s
   }
 }
 
+theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none" ) {
+    return theory::quantifiers::CEGQI_SI_MODE_NONE;
+  } else if(optarg == "use" || optarg == "default") {
+    return theory::quantifiers::CEGQI_SI_MODE_USE;
+  } else if(optarg == "all-abort") {
+    return theory::quantifiers::CEGQI_SI_MODE_ALL_ABORT;
+  } else if(optarg == "all") {
+    return theory::quantifiers::CEGQI_SI_MODE_ALL;
+  } else if(optarg ==  "help") {
+    puts(s_cegqiSingleInvHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --cegqi-si: `") +
+                          optarg + "'.  Try --cegqi-si help.");
+  }
+}
+
 theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "none" ) {
     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index baa6cea96..8f23219eb 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -98,6 +98,7 @@ public:
   theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(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);
@@ -209,6 +210,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_cegqiSingleInvHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_termDbModeHelp;
   static const std::string s_theoryOfModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 38308c9dc..65445be17 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -153,6 +153,17 @@ enum IteLiftQuantMode {
   ITE_LIFT_QUANT_MODE_ALL,
 };
 
+enum CegqiSingleInvMode {
+  /** do not use single invocation techniques */
+  CEGQI_SI_MODE_NONE,
+  /** use single invocation techniques */
+  CEGQI_SI_MODE_USE,
+  /** always use single invocation techniques, abort if solution reconstruction will fail */
+  CEGQI_SI_MODE_ALL_ABORT,
+  /** always use single invocation techniques */
+  CEGQI_SI_MODE_ALL,
+};
+
 enum SygusInvTemplMode {
   /** synthesize I( x ) */
   SYGUS_INV_TEMPL_MODE_NONE,
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 227540f45..456ab04c2 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -109,6 +109,9 @@ option instLevelInputOnly --inst-level-input-only bool :default true
  only input terms are assigned instantiation level zero
 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 instRelevantCond --inst-rlv-cond bool :default false
+ add relevancy conditions for instantiations
+
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
@@ -229,8 +232,8 @@ option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler stringToCegqiFairMode
   if and how to apply fairness for cegqi
-option cegqiSingleInv --cegqi-si bool :default false :read-write
-  process single invocation synthesis conjectures
+option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write
+  mode for processing single invocation synthesis conjectures
 option cegqiSingleInvPartial --cegqi-si-partial bool :default false
   combined techniques for synthesis conjectures that are partially single invocation 
 option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
@@ -239,8 +242,6 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
-option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
-  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form