Allow partial models for multiple sygus enumerators (#2499)

1 files changed, 21 insertions, 8 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 9a6645560..647b16637 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -415,6 +415,8 @@ void SygusPbe::getTermList(const std::vector<Node>& candidates,
   }
 }
 
+bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }
+
 bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
                                    const std::vector<Node>& enum_values,
                                    const std::vector<Node>& candidates,
@@ -431,10 +433,18 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
       Trace("sygus-pbe-enum") << "  " << enums[i] << " -> ";
       TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
       Trace("sygus-pbe-enum") << std::endl;
-      unsigned sz = d_tds->getSygusTermSize( enum_values[i] );
-      szs.push_back(sz);
-      if( i==0 || sz<min_term_size ){
-        min_term_size = sz;
+      if (!enum_values[i].isNull())
+      {
+        unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
+        szs.push_back(sz);
+        if (i == 0 || sz < min_term_size)
+        {
+          min_term_size = sz;
+        }
+      }
+      else
+      {
+        szs.push_back(0);
       }
     }
     // Assume two enumerators of types T1 and T2.
@@ -448,11 +458,14 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
     std::vector<unsigned> enum_consider;
     for (unsigned i = 0, esize = enums.size(); i < esize; i++)
     {
-      Assert(szs[i] >= min_term_size);
-      int diff = szs[i] - min_term_size;
-      if (!options::sygusPbeMultiFair() || diff <= diffAllow)
+      if (!enum_values[i].isNull())
       {
-        enum_consider.push_back( i );
+        Assert(szs[i] >= min_term_size);
+        int diff = szs[i] - min_term_size;
+        if (!options::sygusPbeMultiFair() || diff <= diffAllow)
+        {
+          enum_consider.push_back(i);
+        }
       }
     }