4 files changed, 81 insertions, 21 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index faf358573..35827d3b0 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -569,6 +569,27 @@ auto (default) \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_sygusUnifPiHelp =
+    "\
+Modes for piecewise-independent unification supported by --sygus-unif-pi:\n\
+\n\
+none  \n\
++ Do not use piecewise-independent unification.\n\
+\n\
+complete \n\
++ Use complete approach for piecewise-independent unification (see Section 3\n\
+of Barbosa et al FMCAD 2019).\n\
+\n\
+cond-enum  \n\
++ Use unconstrained condition enumeration for piecewise-independent\n\
+unification (see Section 4 of Barbosa et al FMCAD 2019).\n\
+\n\
+cond-enum-igain \n\
++ Same as cond-enum, but additionally uses an information gain heuristic\n\
+when doing decision tree learning.\n\
+\n\
+";
+
 const std::string OptionsHandler::s_sygusGrammarConsHelp =
     "\
 Modes for default SyGuS grammars, supported by --sygus-grammar-cons:\n\
@@ -1141,6 +1162,37 @@ OptionsHandler::stringToSygusGrammarConsMode(std::string option,
   }
 }
 
+theory::quantifiers::SygusUnifPiMode OptionsHandler::stringToSygusUnifPiMode(
+    std::string option, std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return theory::quantifiers::SYGUS_UNIF_PI_NONE;
+  }
+  else if (optarg == "complete")
+  {
+    return theory::quantifiers::SYGUS_UNIF_PI_COMPLETE;
+  }
+  else if (optarg == "cond-enum")
+  {
+    return theory::quantifiers::SYGUS_UNIF_PI_CENUM;
+  }
+  else if (optarg == "cond-enum-igain")
+  {
+    return theory::quantifiers::SYGUS_UNIF_PI_CENUM_IGAIN;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_sygusUnifPiHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --sygus-unif-pi: `")
+                          + optarg + "'.  Try --sygus-unif-pi help.");
+  }
+}
+
 theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
     std::string option, std::string optarg)
 {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index eae61c5b2..2e372a00c 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -122,6 +122,8 @@ public:
       std::string option, std::string optarg);
   theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode(
       std::string option, std::string optarg);
+  theory::quantifiers::SygusUnifPiMode stringToSygusUnifPiMode(
+      std::string option, std::string optarg);
   theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode(
       std::string option, std::string optarg);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
@@ -277,6 +279,7 @@ public:
   static const std::string s_sygusFilterSolHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_sygusActiveGenHelp;
+  static const std::string s_sygusUnifPiHelp;
   static const std::string s_sygusGrammarConsHelp;
   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 9ff2ac196..1a256b0bc 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -342,6 +342,24 @@ enum QuantRepMode {
   QUANT_REP_MODE_DEPTH,
 };
 
+/**
+ * Modes for piecewise-independent unification for synthesis (see Barbosa et al
+ * FMCAD 2019).
+ */
+enum SygusUnifPiMode
+{
+  /** do not do piecewise-independent unification for synthesis */
+  SYGUS_UNIF_PI_NONE,
+  /** use (finite-model) complete piecewise-independent unification */
+  SYGUS_UNIF_PI_COMPLETE,
+  /** use approach based on condition enumeration for piecewise-independent
+     unification */
+  SYGUS_UNIF_PI_CENUM,
+  /** use approach based on condition enumeration with information gain
+     heuristics for piecewise-independent unification */
+  SYGUS_UNIF_PI_CENUM_IGAIN,
+};
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 171af1e47..e7a24cf3e 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -950,20 +950,15 @@ header = "options/quantifiers_options.h"
   help       = "abort if constant repair techniques are not applicable"
 
 [[option]]
-  name       = "sygusUnif"
+  name       = "sygusUnifPi"
   category   = "regular"
-  long       = "sygus-unif"
-  type       = "bool"
-  default    = "false"
-  help       = "Unification-based function synthesis"
-
-[[option]]
-  name       = "sygusUnifCondIndependent"
-  category   = "regular"
-  long       = "sygus-unif-cond-independent"
-  type       = "bool"
-  default    = "false"
-  help       = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
+  long       = "sygus-unif-pi=MODE"
+  type       = "CVC4::theory::quantifiers::SygusUnifPiMode"
+  default    = "CVC4::theory::quantifiers::SYGUS_UNIF_PI_NONE"
+  handler    = "stringToSygusUnifPiMode"
+  includes   = ["options/quantifiers_modes.h"]
+  read_only  = true
+  help       = "mode for synthesis via piecewise-indepedent unification"
 
 [[option]]
   name       = "sygusUnifShuffleCond"
@@ -974,14 +969,6 @@ header = "options/quantifiers_options.h"
   help       = "Shuffle condition pool when building solutions (may change solutions sizes)"
 
 [[option]]
-  name       = "sygusUnifBooleanHeuristicDt"
-  category   = "regular"
-  long       = "sygus-unif-boolean-heuristic-dt"
-  type       = "bool"
-  default    = "false"
-  help       = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
-
-[[option]]
   name       = "sygusUnifCondIndNoRepeatSol"
   category   = "regular"
   long       = "sygus-unif-cond-independent-no-repeat-sol"