Allow multiple functions in sygus unif approaches (#1831)

10 files changed, 240 insertions, 102 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 7794ec912..256955bbd 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -44,7 +44,7 @@ bool CegisUnif::initialize(Node n,
   d_candidate = candidates[0];
   Trace("cegis-unif") << "Initialize unif utility for " << d_candidate
                       << "...\n";
-  d_sygus_unif.initialize(d_qe, d_candidate, d_enums, lemmas);
+  d_sygus_unif.initialize(d_qe, candidates, d_enums, lemmas);
   Assert(!d_enums.empty());
   Trace("cegis-unif") << "Initialize " << d_enums.size() << " enumerators for "
                       << d_candidate << "...\n";
@@ -129,14 +129,13 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
   }
   /* build candidate solution */
   Assert(candidates.size() == 1);
-  Node vc = d_sygus_unif.constructSolution();
-  Trace("cegis-unif-enum") << "... candidate solution :" << vc << "\n";
-  if (vc.isNull())
+  if (d_sygus_unif.constructSolution(candidate_values))
   {
-    return false;
+    Node vc = candidate_values[0];
+    Trace("cegis-unif-enum") << "... candidate solution :" << vc << "\n";
+    return true;
   }
-  candidate_values.push_back(vc);
-  return true;
+  return false;
 }
 
 Node CegisUnif::purifyLemma(Node n,
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 65b8ba133..472cfbd89 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -143,45 +143,53 @@ bool CegConjecturePbe::initialize(Node n,
       }
     }
   }
-  
-  //register candidates
-  if( options::sygusUnifCondSol() ){
-    if( candidates.size()==1 ){// conditional solutions for multiple function conjectures TODO?
-      // collect a pool of types over which we will enumerate terms 
-      Node c = candidates[0];
-      // specification must have at least one example, and must be in PBE form
-      if (!d_examples[c].empty()
-          && d_examples_out_invalid.find(c) == d_examples_out_invalid.end())
-      {
-        Assert( d_examples.find( c )!=d_examples.end() );
-        Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
-                           << std::endl;
-        d_sygus_unif[c].initialize(d_qe, c, d_candidate_to_enum[c], lemmas);
-        Assert(!d_candidate_to_enum[c].empty());
-        Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
-                           << " enumerators for " << c << "..." << std::endl;
-        // initialize the enumerators
-        for (unsigned i = 0, size = d_candidate_to_enum[c].size(); i < size;
-             i++)
-        {
-          Node e = d_candidate_to_enum[c][i];
-          d_tds->registerEnumerator(e, c, d_parent, true);
-          Node g = d_tds->getActiveGuardForEnumerator(e);
-          d_enum_to_active_guard[e] = g;
-          d_enum_to_candidate[e] = c;
-        }
-        Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
-                           << " example points for " << c << "..." << std::endl;
-        // initialize the examples
-        for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
-        {
-          d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
-        }
-        d_is_pbe = true;
-      }
+
+  if (!options::sygusUnifCondSol())
+  {
+    // we are not doing unification
+    return false;
+  }
+
+  // check if all candidates are valid examples
+  d_is_pbe = true;
+  for (const Node& c : candidates)
+  {
+    if (d_examples[c].empty()
+        || d_examples_out_invalid.find(c) != d_examples_out_invalid.end())
+    {
+      d_is_pbe = false;
+      return false;
+    }
+  }
+  for (const Node& c : candidates)
+  {
+    Assert(d_examples.find(c) != d_examples.end());
+    Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
+                       << std::endl;
+    std::vector<Node> singleton_c;
+    singleton_c.push_back(c);
+    d_sygus_unif[c].initialize(
+        d_qe, singleton_c, d_candidate_to_enum[c], lemmas);
+    Assert(!d_candidate_to_enum[c].empty());
+    Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
+                       << " enumerators for " << c << "..." << std::endl;
+    // initialize the enumerators
+    for (const Node& e : d_candidate_to_enum[c])
+    {
+      d_tds->registerEnumerator(e, c, d_parent, true);
+      Node g = d_tds->getActiveGuardForEnumerator(e);
+      d_enum_to_active_guard[e] = g;
+      d_enum_to_candidate[e] = c;
+    }
+    Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
+                       << " example points for " << c << "..." << std::endl;
+    // initialize the examples
+    for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
+    {
+      d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
     }
   }
-  return d_is_pbe;
+  return true;
 }
 
 Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
@@ -384,11 +392,15 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
   for( unsigned i=0; i<candidates.size(); i++ ){
     Node c = candidates[i];
     //build decision tree for candidate
-    Node vc = d_sygus_unif[c].constructSolution();
-    if( vc.isNull() ){     
+    std::vector<Node> sol;
+    if (d_sygus_unif[c].constructSolution(sol))
+    {
+      Assert(sol.size() == 1);
+      candidate_values.push_back(sol[0]);
+    }
+    else
+    {
       return false;
-    }else{
-      candidate_values.push_back( vc );
     }
   }
   return true;
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 9a017d21b..dc927388e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -29,27 +29,40 @@ namespace quantifiers {
 SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
 
 SygusUnif::~SygusUnif() {}
-
 void SygusUnif::initialize(QuantifiersEngine* qe,
-                           Node f,
+                           const std::vector<Node>& funs,
                            std::vector<Node>& enums,
                            std::vector<Node>& lemmas)
 {
-  Assert(d_candidate.isNull());
-  d_candidate = f;
+  Assert(d_candidates.empty());
   d_qe = qe;
   d_tds = qe->getTermDatabaseSygus();
-  // initialize the strategy
-  d_strategy.initialize(qe, f, enums, lemmas);
+  for (const Node& f : funs)
+  {
+    d_candidates.push_back(f);
+    // initialize the strategy
+    d_strategy[f].initialize(qe, f, enums, lemmas);
+  }
 }
 
-Node SygusUnif::constructSolution()
+bool SygusUnif::constructSolution(std::vector<Node>& sols)
 {
   // initialize a call to construct solution
   initializeConstructSol();
-  // call the virtual construct solution method
-  Node e = d_strategy.getRootEnumerator();
-  return constructSol(e, role_equal, 1);
+  for (const Node& f : d_candidates)
+  {
+    // initialize a call to construct solution for function f
+    initializeConstructSolFor(f);
+    // call the virtual construct solution method
+    Node e = d_strategy[f].getRootEnumerator();
+    Node sol = constructSol(f, e, role_equal, 1);
+    if (sol.isNull())
+    {
+      return false;
+    }
+    sols.push_back(sol);
+  }
+  return true;
 }
 
 Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index beb2023f9..e55f7e6ff 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -29,18 +29,13 @@ namespace quantifiers {
 /** Sygus unification utility
  *
  * This utility implements synthesis-by-unification style approaches for a
- * single function to synthesize f.
- * These approaches include a combination of:
+ * set of functions-to-synthesize. These approaches include a combination of:
  * (1) Decision tree learning, inspired by Alur et al TACAS 2017,
  * (2) Divide-and-conquer via string concatenation.
  *
- * This class maintains:
+ * This class maintains, for each function-to-synthesize f:
  * (1) A "strategy tree" based on the syntactic restrictions for f that is
  * constructed during initialize (d_strategy),
- * (2) A set of input/output examples that are the specification for f. This
- * can be updated via calls to resetExmaples/addExamples,
- * (3) A set of terms that have been enumerated for enumerators (d_ecache). This
- * can be updated via calls to notifyEnumeration.
  *
  * Based on the above, solutions can be constructed via calls to
  * constructSolution.
@@ -53,8 +48,8 @@ class SygusUnif
 
   /** initialize
    *
-   * This initializes this class with function-to-synthesize f. We also call
-   * f the candidate variable.
+   * This initializes this class with functions-to-synthesize funs. We also call
+   * these "candidate variables".
    *
    * This call constructs a set of enumerators for the relevant subfields of
    * the grammar of f and adds them to enums. These enumerators are those that
@@ -66,7 +61,7 @@ class SygusUnif
    * strategy is ITE_strat).
    */
   virtual void initialize(QuantifiersEngine* qe,
-                          Node f,
+                          const std::vector<Node>& funs,
                           std::vector<Node>& enums,
                           std::vector<Node>& lemmas);
 
@@ -78,12 +73,12 @@ class SygusUnif
   virtual void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) = 0;
   /** construct solution
    *
-   * This attempts to construct a solution based on the current set of
-   * enumerated values. Returns null if it cannot (for example, if the
-   * set of enumerated values is insufficient, or if a non-deterministic
-   * strategy aborts).
+   * This attempts to construct a solution for each function-to-synthesize
+   * based on the current set of enumerated values. Returns null if it cannot
+   * for some function (for example, if the set of enumerated values is
+   * insufficient, or if a non-deterministic strategy aborts).
    */
-  virtual Node constructSolution();
+  virtual bool constructSolution(std::vector<Node>& sols);
 
  protected:
   /** reference to quantifier engine */
@@ -99,10 +94,10 @@ class SygusUnif
                         std::vector<Node>& vals,
                         bool pol = true);
   //-----------------------end debug printing
-  /** the candidate for this class */
-  Node d_candidate;
+  /** the candidates for this class */
+  std::vector<Node> d_candidates;
   /** maps a function-to-synthesize to the above information */
-  SygusUnifStrategy d_strategy;
+  std::map<Node, SygusUnifStrategy> d_strategy;
 
   /** domain-specific enumerator exclusion techniques
    *
@@ -139,6 +134,12 @@ class SygusUnif
    * Called once before each attempt to construct solutions.
    */
   virtual void initializeConstructSol() = 0;
+  /** implementation-dependent initialize construct solution
+   *
+   * Called once before each attempt to construct solution for a
+   * function-to-synthesize f.
+   */
+  virtual void initializeConstructSolFor(Node f) = 0;
   /** implementation-dependent function for construct solution.
    *
    * Construct a solution based on enumerator e for function-to-synthesize of
@@ -146,7 +147,7 @@ class SygusUnif
    *
    * ind is the term depth of the context (for debugging).
    */
-  virtual Node constructSol(Node e, NodeRole nrole, int ind) = 0;
+  virtual Node constructSol(Node f, Node e, NodeRole nrole, int ind) = 0;
   /** Heuristically choose the best solved term from solved in context x,
    * currently return the first. */
   virtual Node constructBestSolvedTerm(const std::vector<Node>& solved);
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 7a134b1c0..eb607d2c3 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -466,16 +466,17 @@ SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0)
 }
 
 SygusUnifIo::~SygusUnifIo() {}
-
 void SygusUnifIo::initialize(QuantifiersEngine* qe,
-                             Node f,
+                             const std::vector<Node>& funs,
                              std::vector<Node>& enums,
                              std::vector<Node>& lemmas)
 {
+  Assert(funs.size() == 1);
   d_examples.clear();
   d_examples_out.clear();
   d_ecache.clear();
-  SygusUnif::initialize(qe, f, enums, lemmas);
+  d_candidate = funs[0];
+  SygusUnif::initialize(qe, funs, enums, lemmas);
 }
 
 void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
@@ -492,7 +493,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   Assert(!d_examples.empty());
   Assert(d_examples.size() == d_examples_out.size());
 
-  EnumInfo& ei = d_strategy.getEnumInfo(e);
+  EnumInfo& ei = d_strategy[c].getEnumInfo(e);
   // The explanation for why the current value should be excluded in future
   // iterations.
   Node exp_exc;
@@ -528,7 +529,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
     {
       Node xs = ei.d_enum_slave[s];
 
-      EnumInfo& eiv = d_strategy.getEnumInfo(xs);
+      EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
 
       EnumCache& ecv = d_ecache[xs];
 
@@ -677,7 +678,18 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   lemmas.push_back(exp_exc);
 }
 
-Node SygusUnifIo::constructSolution()
+bool SygusUnifIo::constructSolution(std::vector<Node>& sols)
+{
+  Node sol = constructSolutionNode();
+  if (!sol.isNull())
+  {
+    sols.push_back(sol);
+    return true;
+  }
+  return false;
+}
+
+Node SygusUnifIo::constructSolutionNode()
 {
   Node c = d_candidate;
   if (!d_solution.isNull())
@@ -699,9 +711,10 @@ Node SygusUnifIo::constructSolution()
       Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
       // initialize a call to construct solution
       initializeConstructSol();
+      initializeConstructSolFor(c);
       // call the virtual construct solution method
-      Node e = d_strategy.getRootEnumerator();
-      Node vcc = constructSol(e, role_equal, 1);
+      Node e = d_strategy[c].getRootEnumerator();
+      Node vcc = constructSol(c, e, role_equal, 1);
       // if we constructed the solution, and we either did not previously have
       // a solution, or the new solution is better (smaller).
       if (!vcc.isNull()
@@ -740,10 +753,11 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
     Trace("sygus-sui-enum-debug")
         << "Is " << e << " is str.contains exclusion?" << std::endl;
     d_use_str_contains_eexc[e] = true;
-    EnumInfo& ei = d_strategy.getEnumInfo(e);
+    Node c = d_candidate;
+    EnumInfo& ei = d_strategy[c].getEnumInfo(e);
     for (const Node& sn : ei.d_enum_slave)
     {
-      EnumInfo& eis = d_strategy.getEnumInfo(sn);
+      EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
       EnumRole er = eis.getRole();
       if (er != enum_io && er != enum_concat_term)
       {
@@ -833,9 +847,14 @@ void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
 }
 
 void SygusUnifIo::initializeConstructSol() { d_context.initialize(this); }
+void SygusUnifIo::initializeConstructSolFor(Node f)
+{
+  Assert(d_candidate == f);
+}
 
-Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind)
+Node SygusUnifIo::constructSol(Node f, Node e, NodeRole nrole, int ind)
 {
+  Assert(d_candidate == f);
   UnifContextIo& x = d_context;
   TypeNode etn = e.getType();
   if (Trace.isOn("sygus-sui-dt-debug"))
@@ -858,10 +877,10 @@ Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind)
     Trace("sygus-sui-dt-debug") << std::endl;
   }
   // enumerator type info
-  EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn);
+  EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
 
   // get the enumerator information
-  EnumInfo& einfo = d_strategy.getEnumInfo(e);
+  EnumInfo& einfo = d_strategy[f].getEnumInfo(e);
 
   EnumCache& ecache = d_ecache[e];
 
@@ -1264,7 +1283,7 @@ Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind)
           }
           else
           {
-            rec_c = constructSol(cenum.first, cenum.second, ind + 2);
+            rec_c = constructSol(f, cenum.first, cenum.second, ind + 2);
           }
 
           // undo update the context
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index 276cc9da2..b0d6ce3ce 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -252,6 +252,16 @@ class SubsumeTrie
  * This class implement synthesis-by-unification, where the specification is
  * I/O examples. With respect to SygusUnif, it's main interface function is
  * addExample, which adds an I/O example to the specification.
+ *
+ * Since I/O specifications for multiple functions can be fully separated, we
+ * assume that this class is used only for a single function to synthesize.
+ *
+ * In addition to the base class which maintains a strategy tree, this class
+ * maintains:
+ * (1) A set of input/output examples that are the specification for f. This
+ * can be updated via calls to resetExmaples/addExamples,
+ * (2) A set of terms that have been enumerated for enumerators (d_ecache). This
+ * can be updated via calls to notifyEnumeration.
  */
 class SygusUnifIo : public SygusUnif
 {
@@ -261,9 +271,13 @@ class SygusUnifIo : public SygusUnif
   SygusUnifIo();
   ~SygusUnifIo();
 
-  /** initialize */
+  /** initialize
+   *
+   * The vector funs should be of length one, since I/O specifications across
+   * multiple functions can be separated.
+   */
   virtual void initialize(QuantifiersEngine* qe,
-                          Node f,
+                          const std::vector<Node>& funs,
                           std::vector<Node>& enums,
                           std::vector<Node>& lemmas) override;
   /** Notify enumeration */
@@ -272,7 +286,7 @@ class SygusUnifIo : public SygusUnif
                                  std::vector<Node>& lemmas) override;
 
   /** Construct solution */
-  virtual Node constructSolution() override;
+  virtual bool constructSolution(std::vector<Node>& sols) override;
 
   /** add example
    *
@@ -284,6 +298,8 @@ class SygusUnifIo : public SygusUnif
   void addExample(const std::vector<Node>& input, Node output);
 
  protected:
+  /** the candidate */
+  Node d_candidate;
   /**
    * Whether we will try to construct solution on the next call to
    * constructSolution. This flag is set to true when we successfully
@@ -356,7 +372,13 @@ class SygusUnifIo : public SygusUnif
   };
   /** maps enumerators to the information above */
   std::map<Node, EnumCache> d_ecache;
-
+  /** Construct solution node
+   *
+   * This is called for the (single) function-to-synthesize during a call to
+   * constructSolution. If this returns a non-null node, then that term is a
+   * solution for the function-to-synthesize in the overall conjecture.
+   */
+  Node constructSolutionNode();
   /** domain-specific enumerator exclusion techniques
    *
    * Returns true if the value v for e can be excluded based on a
@@ -390,8 +412,10 @@ class SygusUnifIo : public SygusUnif
   UnifContextIo d_context;
   /** initialize construct solution */
   void initializeConstructSol() override;
+  /** initialize construct solution for */
+  void initializeConstructSolFor(Node f) override;
   /** construct solution */
-  Node constructSol(Node e, NodeRole nrole, int ind) override;
+  Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 723210ca1..bf23cd0d1 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -25,9 +25,8 @@ namespace quantifiers {
 SygusUnifRl::SygusUnifRl() {}
 
 SygusUnifRl::~SygusUnifRl() {}
-
 void SygusUnifRl::initialize(QuantifiersEngine* qe,
-                             Node f,
+                             const std::vector<Node>& funs,
                              std::vector<Node>& enums,
                              std::vector<Node>& lemmas)
 {
@@ -37,7 +36,7 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe,
   d_rlemmas = d_true;
   d_hasRLemmas = false;
   d_ecache.clear();
-  SygusUnif::initialize(qe, f, enums, lemmas);
+  SygusUnif::initialize(qe, funs, enums, lemmas);
 }
 
 void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
@@ -120,7 +119,8 @@ void SygusUnifRl::initializeConstructSol()
   }
 }
 
-Node SygusUnifRl::constructSol(Node e, NodeRole nrole, int ind)
+void SygusUnifRl::initializeConstructSolFor(Node f) {}
+Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
 {
   Node solution = canCloseBranch(e);
   if (!solution.isNull())
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 0f3871056..13d0d1e56 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -38,7 +38,7 @@ class SygusUnifRl : public SygusUnif
 
   /** initialize */
   void initialize(QuantifiersEngine* qe,
-                  Node f,
+                  const std::vector<Node>& funs,
                   std::vector<Node>& enums,
                   std::vector<Node>& lemmas) override;
   /** Notify enumeration */
@@ -87,6 +87,8 @@ class SygusUnifRl : public SygusUnif
    * from d_rlemmas, in which case we may have added or removed data points
    */
   void initializeConstructSol() override;
+  /** initialize construction solution for function-to-synthesize f */
+  void initializeConstructSolFor(Node f) override;
   /**
    * Returns a term covering all data points in the current branch, on null if
    * none can be found among the currently enumerated values for the respective
@@ -95,7 +97,7 @@ class SygusUnifRl : public SygusUnif
   Node canCloseBranch(Node e);
 
   /** construct solution */
-  Node constructSol(Node e, NodeRole nrole, int ind) override;
+  Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 1ec6323b2..f799c20d5 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1479,6 +1479,7 @@ REG1_TESTS = \
 	regress1/sygus/nia-max-square-ns.sy \
 	regress1/sygus/no-flat-simp.sy \
 	regress1/sygus/no-mention.sy \
+	regress1/sygus/pbe_multi.sy \
 	regress1/sygus/process-10-vars.sy \
 	regress1/sygus/qe.sy \
 	regress1/sygus/real-grammar.sy \
diff --git a/test/regress/regress1/sygus/pbe_multi.sy b/test/regress/regress1/sygus/pbe_multi.sy
new file mode 100644
index 000000000..70cb6b2d2
--- /dev/null
+++ b/test/regress/regress1/sygus/pbe_multi.sy
@@ -0,0 +1,67 @@
+; EXPECT: unsat

+; COMMAND-LINE: --sygus-out=status

+(set-logic BV)

+

+(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))

+(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))

+(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))

+(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))

+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

+

+(synth-fun f ( (x (BitVec 64))) (BitVec 64)

+(

+

+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)

+                    (shl1 Start)

+ 		    (shr1 Start)

+		    (shr4 Start)

+		    (shr16 Start)

+		    (bvand Start Start)

+		    (bvor Start Start)

+		    (bvxor Start Start)

+		    (bvadd Start Start)

+		    (if0 Start Start Start)

+ ))

+)

+)

+

+

+(constraint (= (f #x9db91b67d1eee4b4) #x00009db91b67d1ee))

+(constraint (= (f #x211526232b50ea1d) #xdeead9dcd4af15e2))

+(constraint (= (f #xedcec1de604e94ec) #x0000edcec1de604e))

+(constraint (= (f #xede1841179ee3684) #x0000ede1841179ee))

+(constraint (= (f #x9c623bcc40d252bd) #x639dc433bf2dad42))

+(constraint (= (f #x4601c6d84a50d01b) #xb9fe3927b5af2fe4))

+(constraint (= (f #x0c5ed1e748c4e26c) #x00000c5ed1e748c4))

+(constraint (= (f #x6bb653229e60ee94) #x00006bb653229e60))

+(constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))

+(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))

+

+(synth-fun g ( (x (BitVec 64))) (BitVec 64)

+(

+

+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)

+                    (shl1 Start)

+ 		    (shr1 Start)

+		    (shr4 Start)

+		    (shr16 Start)

+		    (bvand Start Start)

+		    (bvor Start Start)

+		    (bvxor Start Start)

+		    (bvadd Start Start)

+		    (if0 Start Start Start)

+ ))

+)

+)

+

+(constraint (= (g #xd5a6481ee2ba1030) #xfffffffffffffffe))

+(constraint (= (g #x03e887e72dee55cd) #x03e887e72dee55cd))

+(constraint (= (g #xaced92921c8e318d) #xaced92921c8e318d))

+(constraint (= (g #x95e5e4184e40aaec) #xfffffffffffffffe))

+(constraint (= (g #x352367e34d76550b) #x352367e34d76550b))

+(constraint (= (g #x398560eeee7b1b6c) #xfffffffffffffffe))

+(constraint (= (g #x099be4899986c29a) #xfffffffffffffffe))

+(constraint (= (g #xb14b75be2e13445a) #xfffffffffffffffe))

+(constraint (= (g #xb4c680ad7e6b16ce) #xfffffffffffffffe))

+(constraint (= (g #x7e4954872868acb8) #xfffffffffffffffe))

+(check-synth)