Refactor mode options for Unif+PI (#3531)

19 files changed, 149 insertions, 56 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"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c47506510..075c8fa00 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1923,16 +1923,6 @@ void SmtEngine::setDefaults() {
         options::cbqi.set(true);
       }
     }
-    // setting unif requirements
-    if (options::sygusUnifBooleanHeuristicDt()
-        && !options::sygusUnifCondIndependent())
-    {
-      options::sygusUnifCondIndependent.set(true);
-    }
-    if (options::sygusUnifCondIndependent() && !options::sygusUnif())
-    {
-      options::sygusUnif.set(true);
-    }
   }
   if (options::sygusInference())
   {
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 399a9576c..8da328eb6 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -151,7 +151,7 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
         // set enums for condition enumerators
         if (index == 1)
         {
-          if (options::sygusUnifCondIndependent())
+          if (usingConditionPool())
           {
             Assert(es.size() == 1);
             // whether valueus exhausted
@@ -228,6 +228,11 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
   return !addedUnifEnumSymBreakLemma;
 }
 
+bool CegisUnif::usingConditionPool() const
+{
+  return d_sygus_unif.usingConditionPool();
+}
+
 void CegisUnif::setConditions(
     const std::map<Node, std::vector<Node>>& unif_cenums,
     const std::map<Node, std::vector<Node>>& unif_cvalues,
@@ -250,7 +255,7 @@ void CegisUnif::setConditions(
       // d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e],
       // unif_cvalues[e]); if condition enumerator had value and it is being
       // passively generated, exclude this value
-      if (options::sygusUnifCondIndependent() && !itc->second.empty())
+      if (usingConditionPool() && !itc->second.empty())
       {
         Node eu = itc->second[0];
         Assert(d_tds->isEnumerator(eu));
@@ -321,7 +326,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
     // if condition values are being indepedently enumerated, they should be
     // communicated to the decision tree strategies indepedently of we
     // proceeding to attempt solution building
-    if (options::sygusUnifCondIndependent())
+    if (usingConditionPool())
     {
       setConditions(unif_cenums, unif_cvalues, lems);
     }
@@ -353,7 +358,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   }
 
   // TODO tie this to the lemma for getting a new condition value
-  Assert(options::sygusUnifCondIndependent() || !lemmas.empty());
+  Assert(usingConditionPool() || !lemmas.empty());
   for (const Node& lem : lemmas)
   {
     Trace("cegis-unif-lemma")
@@ -400,6 +405,9 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
 {
   d_initialized = false;
   d_tds = d_qe->getTermDatabaseSygus();
+  SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool =
+      mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
 }
 
 Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
@@ -415,7 +423,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
     TypeNode ct = c.getType();
     Node eu = nm->mkSkolem("eu", ct);
     Node ceu;
-    if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
+    if (!d_useCondPool && !ci.second.d_enums[0].empty())
     {
       // make a new conditional enumerator as well, starting the
       // second type around
@@ -554,7 +562,7 @@ void CegisUnifEnumDecisionStrategy::initialize(
       DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
 
   // create single condition enumerator for each decision tree strategy
-  if (options::sygusUnifCondIndependent())
+  if (d_useCondPool)
   {
     // allocate a condition enumerator for each candidate
     for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
@@ -576,7 +584,7 @@ void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(
   if (index == 1)
   {
     // we always use (cost-1) conditions, or 1 if in the indepedent case
-    num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1;
+    num_enums = !d_useCondPool ? num_enums - 1 : 1;
   }
   if (num_enums > 0)
   {
@@ -622,7 +630,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   // if we are using a single independent enumerator for conditions, then we
   // allocate an active guard, and are eligible to use variable-agnostic
   // enumeration.
-  if (options::sygusUnifCondIndependent() && index == 1)
+  if (d_useCondPool && index == 1)
   {
     erole = ROLE_ENUM_POOL;
   }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ac859750f..d476d5fb3 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -103,6 +103,11 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
   TermDbSygus* d_tds;
   /** reference to the parent conjecture */
   SynthConjecture* d_parent;
+  /**
+   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+   * FMCAD 2019). This is determined by option::sygusUnifPi().
+   */
+  bool d_useCondPool;
   /** whether this module has been initialized */
   bool d_initialized;
   /** null node */
@@ -294,6 +299,12 @@ class CegisUnif : public Cegis
                      std::map<Node, std::vector<Node>>& unif_cenums,
                      std::map<Node, std::vector<Node>>& unif_cvalues,
                      std::vector<Node>& lems);
+
+  /**
+   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+   * FMCAD 2019). This is determined by option::sygusUnifPi().
+   */
+  bool usingConditionPool() const;
   /**
    * Sygus unif utility. This class implements the core algorithm (e.g. decision
    * tree learning) that this module relies upon.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 5e4513ff3..84b160bb3 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -1187,7 +1187,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // TODO #1935 ITEs are added to Boolean grammars so that we can infer
       // unification strategies. We can do away with this if we can infer
       // unification strategies from and/or/not
-      if (k == ITE && !options::sygusUnif())
+      if (k == ITE && options::sygusUnifPi() == SYGUS_UNIF_PI_NONE)
       {
         continue;
       }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 5d4aaf7ae..1a491394f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -29,7 +29,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnifRl::SygusUnifRl(SynthConjecture* p) : d_parent(p) {}
+SygusUnifRl::SygusUnifRl(SynthConjecture* p)
+    : d_parent(p), d_useCondPool(false), d_useCondPoolIGain(false)
+{
+}
 SygusUnifRl::~SygusUnifRl() {}
 void SygusUnifRl::initializeCandidate(
     QuantifiersEngine* qe,
@@ -57,6 +60,11 @@ void SygusUnifRl::initializeCandidate(
     d_cand_to_eval_hds[f].clear();
     d_cand_to_hd_count[f] = 0;
   }
+  // check whether we are using condition enumeration
+  SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool =
+      mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
+  d_useCondPoolIGain = mode == SYGUS_UNIF_PI_CENUM_IGAIN;
 }
 
 void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
@@ -348,8 +356,7 @@ Node SygusUnifRl::constructSol(
   }
   EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
   Node sol = itd->second.buildSol(etis->d_cons, lemmas);
-  Assert(options::sygusUnifCondIndependent() || !sol.isNull()
-         || !lemmas.empty());
+  Assert(d_useCondPool || !sol.isNull() || !lemmas.empty());
   return sol;
 }
 
@@ -386,6 +393,11 @@ std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
   return it->second;
 }
 
+bool SygusUnifRl::usingConditionPool() const { return d_useCondPool; }
+bool SygusUnifRl::usingConditionPoolInfoGain() const
+{
+  return d_useCondPoolIGain;
+}
 void SygusUnifRl::registerStrategy(
     Node f,
     std::vector<Node>& enums,
@@ -516,7 +528,7 @@ void SygusUnifRl::DecisionTreeInfo::setConditions(
   d_enums.insert(d_enums.end(), enums.begin(), enums.end());
   d_conds.insert(d_conds.end(), conds.begin(), conds.end());
   // add to condition pool
-  if (options::sygusUnifCondIndependent())
+  if (d_unif->usingConditionPool())
   {
     d_cond_mvs.insert(conds.begin(), conds.end());
     if (Trace.isOn("sygus-unif-cond-pool"))
@@ -552,8 +564,8 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
                           << " conditions..." << std::endl;
   // reset the trie
   d_pt_sep.d_trie.clear();
-  return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas)
-                                             : buildSolMinCond(cons, lemmas);
+  return d_unif->usingConditionPool() ? buildSolAllCond(cons, lemmas)
+                                      : buildSolMinCond(cons, lemmas);
 }
 
 Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
@@ -840,7 +852,7 @@ Node SygusUnifRl::DecisionTreeInfo::extractSol(Node cons,
                                                std::map<Node, Node>& hd_mv)
 {
   // rebuild decision tree using heuristic learning
-  if (options::sygusUnifBooleanHeuristicDt())
+  if (d_unif->usingConditionPoolInfoGain())
   {
     recomputeSolHeuristically(hd_mv);
   }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index c5b02a481..827919308 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -103,9 +103,21 @@ class SygusUnifRl : public SygusUnif
   /** retrieve the head of evaluation points for candidate c, if any */
   std::vector<Node> getEvalPointHeads(Node c);
 
+  /**
+   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+   * FMCAD 2019). This is determined by option::sygusUnifPi().
+   */
+  bool usingConditionPool() const;
+  /** Whether we are additionally using information gain.  */
+  bool usingConditionPoolInfoGain() const;
+
  protected:
   /** reference to the parent conjecture */
   SynthConjecture* d_parent;
+  /** Whether we are using condition pool enumeration */
+  bool d_useCondPool;
+  /** Whether we are additionally using information gain heuristics */
+  bool d_useCondPoolIGain;
   /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
   std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
   /** construct sol */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index da4275365..c980e5413 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -65,7 +65,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
   {
     d_modules.push_back(d_ceg_pbe.get());
   }
-  if (options::sygusUnif())
+  if (options::sygusUnifPi() != SYGUS_UNIF_PI_NONE)
   {
     d_modules.push_back(d_ceg_cegisUnif.get());
   }
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index c02d2b31f..1bb85bed9 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --cegqi-si=all --sygus-out=status
-; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z)))))))
diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2
index 6c5039c2b..b851d2e19 100644
--- a/test/regress/regress1/quantifiers/horn-simple.smt2
+++ b/test/regress/regress1/quantifiers/horn-simple.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-unif --sygus-infer
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress1/sygus/car_3.lus.sy b/test/regress/regress1/sygus/car_3.lus.sy
index 088613f21..9432d3131 100755
--- a/test/regress/regress1/sygus/car_3.lus.sy
+++ b/test/regress/regress1/sygus/car_3.lus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-unif --sygus-unif-cond-independent --sygus-unif-boolean-heuristic-dt --decision=justification
+; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification
 
 (set-logic LIA)
 
diff --git a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
index 7d1c35234..df0214316 100644
--- a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
+++ b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-bool-ite-return-const --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status
 (set-logic LIA)
 
 (define-fun
diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress1/sygus/cegisunif-depth1.sy
index 1e810fea3..9f6f65907 100644
--- a/test/regress/regress1/sygus/cegisunif-depth1.sy
+++ b/test/regress/regress1/sygus/cegisunif-depth1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x Int) (y Int)) Int
diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
index 15df2d507..7229dea2e 100644
--- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy
+++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-unif
+; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete
 
 (set-logic SAT)
 (synth-fun u ((x Int)) Int)
diff --git a/test/regress/regress1/sygus/planning-unif.sy b/test/regress/regress1/sygus/planning-unif.sy
index 39c89dc53..3a715501a 100644
--- a/test/regress/regress1/sygus/planning-unif.sy
+++ b/test/regress/regress1/sygus/planning-unif.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
 (set-logic LIA)
 
 (define-fun get-y ((currPoint Int)) Int 
diff --git a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
index 4b0cefcda..6b647b77d 100644
--- a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
+++ b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
 (set-logic BV)
 
 (synth-fun f ((x (BitVec 64)) (y (BitVec 64))) (BitVec 64)