Combine sygus stream with PBE (#2726)

5 files changed, 88 insertions, 17 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1de3e3756..a0939f4db 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1938,13 +1938,14 @@ void SmtEngine::setDefaults() {
       // Streaming is incompatible with techniques that focus the search towards
       // finding a single solution. This currently includes the PBE solver and
       // static template inference for invariant synthesis.
-      if (!options::sygusSymBreakPbe.wasSetByUser())
-      {
-        options::sygusSymBreakPbe.set(false);
-      }
       if (!options::sygusUnifPbe.wasSetByUser())
       {
         options::sygusUnifPbe.set(false);
+        // also disable PBE-specific symmetry breaking unless PBE was enabled
+        if (!options::sygusSymBreakPbe.wasSetByUser())
+        {
+          options::sygusSymBreakPbe.set(false);
+        }
       }
       if (!options::sygusInvTemplMode.wasSetByUser())
       {
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index a4f276792..5d7017a1c 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -26,7 +26,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
+SygusUnif::SygusUnif()
+    : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false)
+{
+}
 SygusUnif::~SygusUnif() {}
 
 void SygusUnif::initializeCandidate(
@@ -42,9 +45,40 @@ void SygusUnif::initializeCandidate(
   d_strategy[f].initialize(qe, f, enums);
 }
 
+Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
+{
+  unsigned minSize = 0;
+  Node minTerm;
+  std::map<Node, unsigned>::iterator it;
+  for (const Node& n : terms)
+  {
+    it = d_termToSize.find(n);
+    unsigned ssize = 0;
+    if (it == d_termToSize.end())
+    {
+      ssize = d_tds->getSygusTermSize(n);
+      d_termToSize[n] = ssize;
+    }
+    else
+    {
+      ssize = it->second;
+    }
+    if (minTerm.isNull() || ssize < minSize)
+    {
+      minTerm = n;
+      minSize = ssize;
+    }
+  }
+  return minTerm;
+}
+
 Node SygusUnif::constructBestSolvedTerm(Node e, const std::vector<Node>& solved)
 {
   Assert(!solved.empty());
+  if (d_enableMinimality)
+  {
+    return getMinimalTerm(solved);
+  }
   return solved[0];
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 67e798854..0784644f8 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -181,6 +181,15 @@ class SygusUnif
       const std::map<Node, unsigned>& total_inc,
       const std::map<Node, std::vector<unsigned> >& incr);
   //------------------------------ end constructing solutions
+  /** map terms to their sygus size */
+  std::map<Node, unsigned> d_termToSize;
+  /**
+   * Whether to ensure terms selected by the above methods lead to minimal
+   * solutions.
+   */
+  bool d_enableMinimality;
+  /** returns the term whose sygus size is minimal among those in terms */
+  Node getMinimalTerm(const std::vector<Node>& terms);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 6daeb1706..89619639d 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -238,11 +238,14 @@ Node SubsumeTrie::addTermInternal(Node t,
       if (!d_term.isNull())
       {
         subsumed.push_back(d_term);
-        if (!checkExistsOnly)
-        {
-          // remove it if checkExistsOnly = false
-          d_term = Node::null();
-        }
+        // If we are only interested in feasibility, we could set d_term to null
+        // here. However, d_term still could be useful, since it may be
+        // smaller than t and suffice as a solution under some condition.
+        // As a simple example, consider predicate synthesis and a case where we
+        // enumerate a C that is correct for all I/O points whose output is
+        // true. Then, C subsumes true. However, true may be preferred, e.g.
+        // to generate a solution ite( C, true, D ) instead of ite( C, C, D ),
+        // since true is conditionally correct under C, and is smaller than C.
       }
     }
     else
@@ -470,6 +473,7 @@ void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
 SygusUnifIo::SygusUnifIo()
     : d_check_sol(false),
       d_cond_count(0),
+      d_sol_term_size(0),
       d_sol_cons_nondet(false),
       d_solConsUsingInfoGain(false)
 {
@@ -771,7 +775,7 @@ bool SygusUnifIo::constructSolution(std::vector<Node>& sols,
 Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
 {
   Node c = d_candidate;
-  if (!d_solution.isNull())
+  if (!d_solution.isNull() && !options::sygusStream())
   {
     // already has a solution
     return d_solution;
@@ -782,10 +786,10 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
     Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
                        << std::endl;
     d_check_sol = false;
+    Node newSolution;
     d_solConsUsingInfoGain = false;
     // try multiple times if we have done multiple conditions, due to
     // non-determinism
-    unsigned sol_term_size = 0;
     for (unsigned i = 0; i <= d_cond_count; i++)
     {
       Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
@@ -800,19 +804,24 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
       if (!vcc.isNull()
           && (d_solution.isNull()
               || (!d_solution.isNull()
-                  && d_tds->getSygusTermSize(vcc) < sol_term_size)))
+                  && d_tds->getSygusTermSize(vcc) < d_sol_term_size)))
       {
         Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
                            << std::endl;
         Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
         d_solution = vcc;
-        sol_term_size = d_tds->getSygusTermSize(vcc);
+        newSolution = vcc;
+        d_sol_term_size = d_tds->getSygusTermSize(vcc);
+        Trace("sygus-pbe-sol")
+            << "PBE solution size: " << d_sol_term_size << std::endl;
         // We've determined its feasible, now, enable information gain and
         // retry. We do this since information gain comes with an overhead,
         // and we want testing feasibility to be fast.
         if (!d_solConsUsingInfoGain)
         {
+          // we permanently enable information gain and minimality now
           d_solConsUsingInfoGain = true;
+          d_enableMinimality = true;
           i = 0;
         }
       }
@@ -821,9 +830,9 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
         break;
       }
     }
-    if (!d_solution.isNull())
+    if (!newSolution.isNull())
     {
-      return d_solution;
+      return newSolution;
     }
     Trace("sygus-pbe") << "...failed to solve." << std::endl;
   }
@@ -1427,6 +1436,7 @@ Node SygusUnifIo::constructBestConditional(Node ce,
   // initially set minEntropy to > 1.0.
   double minEntropy = 2.0;
   unsigned bestIndex = 0;
+  int numEqual = 1;
   for (unsigned j = 0; j < nconds; j++)
   {
     // To compute the entropy for a condition C, for pair of terms (s, t), let
@@ -1460,7 +1470,22 @@ Node SygusUnifIo::constructBestConditional(Node ce,
       }
     }
     Trace("sygus-sui-dt-igain") << "..." << entropySum << std::endl;
-    if (entropySum < minEntropy)
+    // either less, or equal and coin flip passes
+    bool doSet = false;
+    if (entropySum == minEntropy)
+    {
+      numEqual++;
+      if (Random::getRandom().pickWithProb(double(1) / double(numEqual)))
+      {
+        doSet = true;
+      }
+    }
+    else if (entropySum < minEntropy)
+    {
+      doSet = true;
+      numEqual = 1;
+    }
+    if (doSet)
     {
       minEntropy = entropySum;
       bestIndex = j;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index 8fa8b95e1..2f87c0552 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -298,6 +298,8 @@ class SygusUnifIo : public SygusUnif
   unsigned d_cond_count;
   /** The solution for the function of this class, if one has been found */
   Node d_solution;
+  /** the term size of the above solution */
+  unsigned d_sol_term_size;
   /**
    * This flag is set to true if the solution construction was
    * non-deterministic with respect to failure/success.