Allow partial models for multiple sygus enumerators (#2499)

9 files changed, 106 insertions, 25 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index a6c95b893..05f1a9960 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -39,6 +39,17 @@ struct SygusAnyConstAttributeId
 };
 typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
 
+/**
+ * Attribute true for enumerators whose current model values have been excluded
+ * by sygus symmetry breaking. This is set by the datatypes sygus solver during
+ * LAST_CALL effort checks for each active sygus enumerator.
+ */
+struct SygusSymBreakExcAttributeId
+{
+};
+typedef expr::Attribute<SygusSymBreakExcAttributeId, bool>
+    SygusSymBreakExcAttribute;
+
 namespace datatypes {
 
 class DatatypesRewriter {
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index db1ce1c05..a6a3ffc9d 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1317,6 +1317,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
         // register the search value ( prog -> progv ), this may invoke symmetry breaking 
         if( options::sygusSymBreakDynamic() ){
           Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas);
+          SygusSymBreakExcAttribute ssbea;
+          prog.setAttribute(ssbea, rsv.isNull());
           if (rsv.isNull())
           {
             Trace("sygus-sb") << "  SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
@@ -1474,6 +1476,8 @@ Node SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
   }
   Assert(!d_this.isNull());
   NodeManager* nm = NodeManager::currentNM();
+  Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s
+                        << " for " << d_this << std::endl;
   return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
 }
 
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 456f44019..d4926311d 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -166,6 +166,13 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
                 ->toStreamSygus(ss, m_eu);
             Trace("cegis") << ss.str() << std::endl;
           }
+          if (m_eu.isNull())
+          {
+            // A condition enumerator was excluded by symmetry breaking, fail.
+            // TODO (#2498): either move conditions to getTermList or handle
+            // partial models in this module.
+            return false;
+          }
           unif_values[index][e].push_back(m_eu);
         }
         // inter-enumerator symmetry breaking for return values
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index c1b12dfd0..02cf1cdf2 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -71,6 +71,16 @@ class SygusModule
    */
   virtual void getTermList(const std::vector<Node>& candidates,
                            std::vector<Node>& terms) = 0;
+  /** allow partial model
+   *
+   * This method returns true if this module does not require that all
+   * terms returned by getTermList have "proper" model values when calling
+   * constructCandidates. A term may have a model value that is not proper
+   * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model
+   * values that are not proper are replaced by "null" when calling
+   * constructCandidates.
+   */
+  virtual bool allowPartialModel() { return false; }
   /** construct candidate
    *
    * This function takes as input:
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);
+        }
       }
     }
 
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 66e19b6c9..b2ad5f63a 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -117,6 +117,11 @@ class SygusPbe : public SygusModule
   */
   void getTermList(const std::vector<Node>& candidates,
                    std::vector<Node>& terms) override;
+  /**
+   * PBE allows partial models to handle multiple enumerators if we are not
+   * using a strictly fair enumeration strategy.
+   */
+  bool allowPartialModel() override;
   /** construct candidates
    *
    * This function attempts to use unification-based approaches for constructing
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index fde69d196..a29fdcc9f 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -338,7 +339,14 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
 
   // get the model value of the relevant terms from the master module
   std::vector<Node> enum_values;
-  getModelValues(terms, enum_values);
+  bool fullModel = getModelValues(terms, enum_values);
+
+  // if the master requires a full model and the model is partial, we fail
+  if (!d_master->allowPartialModel() && !fullModel)
+  {
+    Trace("cegqi-check") << "...partial model, fail." << std::endl;
+    return;
+  }
 
   if (!constructed_cand)
   {
@@ -586,36 +594,54 @@ void SynthConjecture::preregisterConjecture(Node q)
   d_ceg_si->preregisterConjecture(q);
 }
 
-void SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v)
+bool SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v)
 {
+  bool ret = true;
   Trace("cegqi-engine") << "  * Value is : ";
   for (unsigned i = 0; i < n.size(); i++)
   {
     Node nv = getModelValue(n[i]);
     v.push_back(nv);
+    ret = ret && !nv.isNull();
     if (Trace.isOn("cegqi-engine"))
     {
-      TypeNode tn = nv.getType();
-      Trace("cegqi-engine") << n[i] << " -> ";
+      Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv;
+      TypeNode tn = onv.getType();
       std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv);
-      Trace("cegqi-engine") << ss.str() << " ";
-      if (Trace.isOn("cegqi-engine-rr"))
+      Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
+      Trace("cegqi-engine") << n[i] << " -> ";
+      if (nv.isNull())
+      {
+        Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
+      }
+      else
       {
-        Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn);
-        bv = Rewriter::rewrite(bv);
-        Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+        Trace("cegqi-engine") << ss.str() << " ";
+        if (Trace.isOn("cegqi-engine-rr"))
+        {
+          Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn);
+          bv = Rewriter::rewrite(bv);
+          Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+        }
       }
     }
-    Assert(!nv.isNull());
   }
   Trace("cegqi-engine") << std::endl;
+  return ret;
 }
 
 Node SynthConjecture::getModelValue(Node n)
 {
   Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
-  return d_qe->getModel()->getValue(n);
+  if (n.getAttribute(SygusSymBreakExcAttribute()))
+  {
+    // if the current model value of n was excluded by symmetry breaking, then
+    // it does not have a proper model value that we should consider, thus we
+    // return null.
+    return Node::null();
+  }
+  Node mv = d_qe->getModel()->getValue(n);
+  return mv;
 }
 
 void SynthConjecture::debugPrint(const char* c)
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 1cbd4e949..53bc829cf 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -112,9 +112,15 @@ class SynthConjecture
   void assign(Node q);
   /** has a conjecture been assigned to this class */
   bool isAssigned() { return !d_embed_quant.isNull(); }
-  /** get model values for terms n, store in vector v */
-  void getModelValues(std::vector<Node>& n, std::vector<Node>& v);
-  /** get model value for term n */
+  /**
+   * Get model values for terms n, store in vector v. This method returns true
+   * if and only if all values added to v are non-null.
+   */
+  bool getModelValues(std::vector<Node>& n, std::vector<Node>& v);
+  /**
+   * Get model value for term n. If n has a value that was excluded by
+   * datatypes sygus symmetry breaking, this method returns null.
+   */
   Node getModelValue(Node n);
 
   /** get utility for static preprocessing and analysis of conjectures */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 56844ec1f..296c10ff6 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -42,8 +42,7 @@ SynthEngine::~SynthEngine() { delete d_conj; }
 
 bool SynthEngine::needsCheck(Theory::Effort e)
 {
-  return !d_quantEngine->getTheoryEngine()->needCheck()
-         && e >= Theory::EFFORT_LAST_CALL;
+  return e >= Theory::EFFORT_LAST_CALL;
 }
 
 QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)