Refactor symmetry breaking in datatypes sygus (#1640)

6 files changed, 154 insertions, 46 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 1dd4dcbeb..2273db5ea 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -547,9 +547,8 @@ void CegConjecture::printAndContinueStream()
     {
       sol = d_cinfo[cprog].d_inst.back();
       // add to explanation of exclusion
-      d_qe->getTermDatabaseSygus()
-          ->getExplain()
-          ->getExplanationForConstantEquality(cprog, sol, exp);
+      d_qe->getTermDatabaseSygus()->getExplain()->getExplanationForEquality(
+          cprog, sol, exp);
     }
   }
   Assert(!exp.empty());
@@ -612,6 +611,8 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         if (eq_sol != sol)
         {
           ++(cei->d_statistics.d_candidate_rewrites);
+          // if eq_sol is null, then we have an uninteresting candidate rewrite,
+          // e.g. one that is alpha-equivalent to another.
           if (!eq_sol.isNull())
           {
             // The analog of terms sol and eq_sol are equivalent under sample
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index aafaa07e1..f76edb1c3 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -110,19 +110,25 @@ Node TermRecBuild::build(unsigned d)
   return NodeManager::currentNM()->mkNode(d_kind[d], children);
 }
 
-void SygusExplain::getExplanationForConstantEquality(Node n,
-                                                     Node vn,
-                                                     std::vector<Node>& exp)
+void SygusExplain::getExplanationForEquality(Node n,
+                                             Node vn,
+                                             std::vector<Node>& exp)
 {
   std::map<unsigned, bool> cexc;
-  getExplanationForConstantEquality(n, vn, exp, cexc);
+  getExplanationForEquality(n, vn, exp, cexc);
 }
 
-void SygusExplain::getExplanationForConstantEquality(
-    Node n, Node vn, std::vector<Node>& exp, std::map<unsigned, bool>& cexc)
+void SygusExplain::getExplanationForEquality(Node n,
+                                             Node vn,
+                                             std::vector<Node>& exp,
+                                             std::map<unsigned, bool>& cexc)
 {
-  Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
   Assert(n.getType() == vn.getType());
+  if (n == vn)
+  {
+    return;
+  }
+  Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
   TypeNode tn = n.getType();
   Assert(tn.isDatatype());
   const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
@@ -137,22 +143,23 @@ void SygusExplain::getExplanationForConstantEquality(
           kind::APPLY_SELECTOR_TOTAL,
           Node::fromExpr(dt[i].getSelectorInternal(tn.toType(), j)),
           n);
-      getExplanationForConstantEquality(sel, vn[j], exp);
+      getExplanationForEquality(sel, vn[j], exp);
     }
   }
 }
 
-Node SygusExplain::getExplanationForConstantEquality(Node n, Node vn)
+Node SygusExplain::getExplanationForEquality(Node n, Node vn)
 {
   std::map<unsigned, bool> cexc;
-  return getExplanationForConstantEquality(n, vn, cexc);
+  return getExplanationForEquality(n, vn, cexc);
 }
 
-Node SygusExplain::getExplanationForConstantEquality(
-    Node n, Node vn, std::map<unsigned, bool>& cexc)
+Node SygusExplain::getExplanationForEquality(Node n,
+                                             Node vn,
+                                             std::map<unsigned, bool>& cexc)
 {
   std::vector<Node> exp;
-  getExplanationForConstantEquality(n, vn, exp, cexc);
+  getExplanationForEquality(n, vn, exp, cexc);
   Assert(!exp.empty());
   return exp.size() == 1 ? exp[0]
                          : NodeManager::currentNM()->mkNode(kind::AND, exp);
@@ -250,7 +257,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
       // if excluded, we may need to add the explanation for this
       if (vnr_exp.isNull() && !vnr_c.isNull())
       {
-        vnr_exp = getExplanationForConstantEquality(sel, vnr[i]);
+        vnr_exp = getExplanationForEquality(sel, vnr[i]);
       }
     }
   }
@@ -264,7 +271,7 @@ void SygusExplain::getExplanationFor(Node n,
                                      unsigned& sz)
 {
   // naive :
-  // return getExplanationForConstantEquality( n, vn, exp );
+  // return getExplanationForEquality( n, vn, exp );
 
   // set up the recursion object
   std::map<TypeNode, int> var_count;
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index ad26f29e4..818f51438 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -100,7 +100,7 @@ class TermRecBuild
  * (datatype) sygus term n is:
  *  (if (gt x 0) 0 0)
  * where if, gt, x, 0 are datatype constructors.
- * The explanation returned by getExplanationForConstantEquality
+ * The explanation returned by getExplanationForEquality
  * below for n and the above term is:
  *   { ((_ is if) n), ((_ is geq) n.0),
  *     ((_ is x) n.0.0), ((_ is 0) n.0.1),
@@ -142,20 +142,19 @@ class SygusExplain
  public:
   SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {}
   ~SygusExplain() {}
-  /** get explanation for constant equality
+  /** get explanation for equality
    *
    * This function constructs an explanation, stored in exp, such that:
    * - All formulas in exp are of the form ((_ is C) ns), where ns
    *   is a chain of selectors applied to n, and
    * - exp => ( n = vn )
    */
-  void getExplanationForConstantEquality(Node n,
-                                         Node vn,
-                                         std::vector<Node>& exp);
+  void getExplanationForEquality(Node n, Node vn, std::vector<Node>& exp);
   /** returns the conjunction of exp computed in the above function */
-  Node getExplanationForConstantEquality(Node n, Node vn);
+  Node getExplanationForEquality(Node n, Node vn);
 
-  /** get explanation for constant equality
+  /** get explanation for equality
+   *
    * This is identical to the above function except that we
    * take an additional argument cexc, which says which
    * children of vn should be excluded from the explanation.
@@ -165,14 +164,14 @@ class SygusExplain
    *   { ((_ is plus) n), ((_ is y) n.1) }
    * where notice that the 0^th argument of vn is excluded.
    */
-  void getExplanationForConstantEquality(Node n,
-                                         Node vn,
-                                         std::vector<Node>& exp,
-                                         std::map<unsigned, bool>& cexc);
+  void getExplanationForEquality(Node n,
+                                 Node vn,
+                                 std::vector<Node>& exp,
+                                 std::map<unsigned, bool>& cexc);
   /** returns the conjunction of exp computed in the above function */
-  Node getExplanationForConstantEquality(Node n,
-                                         Node vn,
-                                         std::map<unsigned, bool>& cexc);
+  Node getExplanationForEquality(Node n,
+                                 Node vn,
+                                 std::map<unsigned, bool>& cexc);
 
   /** get explanation for
    *
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 36e883848..1c61544e1 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -1303,7 +1303,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
   if (exp_exc.isNull())
   {
     // if we did not already explain why this should be excluded, use default
-    exp_exc = d_tds->getExplain()->getExplanationForConstantEquality(x, v);
+    exp_exc = d_tds->getExplain()->getExplanationForEquality(x, v);
   }
   Node exlem =
       NodeManager::currentNM()->mkNode(OR, g.negate(), exp_exc.negate());
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index b12a23c83..e8bdf2083 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -733,6 +733,59 @@ void TermDbSygus::getEnumerators(std::vector<Node>& mts)
   }
 }
 
+void TermDbSygus::registerSymBreakLemma(Node e,
+                                        Node lem,
+                                        TypeNode tn,
+                                        unsigned sz)
+{
+  d_enum_to_sb_lemmas[e].push_back(lem);
+  d_sb_lemma_to_type[lem] = tn;
+  d_sb_lemma_to_size[lem] = sz;
+}
+
+bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const
+{
+  if (!d_enum_to_sb_lemmas.empty())
+  {
+    for (std::pair<const Node, std::vector<Node> > sb : d_enum_to_sb_lemmas)
+    {
+      enums.push_back(sb.first);
+    }
+    return true;
+  }
+  return false;
+}
+
+void TermDbSygus::getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator itsb =
+      d_enum_to_sb_lemmas.find(e);
+  if (itsb != d_enum_to_sb_lemmas.end())
+  {
+    lemmas.insert(lemmas.end(), itsb->second.begin(), itsb->second.end());
+  }
+}
+
+TypeNode TermDbSygus::getTypeForSymBreakLemma(Node lem) const
+{
+  std::map<Node, TypeNode>::const_iterator it = d_sb_lemma_to_type.find(lem);
+  Assert(it != d_sb_lemma_to_type.end());
+  return it->second;
+}
+unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const
+{
+  std::map<Node, unsigned>::const_iterator it = d_sb_lemma_to_size.find(lem);
+  Assert(it != d_sb_lemma_to_size.end());
+  return it->second;
+}
+
+void TermDbSygus::clearSymBreakLemmas()
+{
+  d_enum_to_sb_lemmas.clear();
+  d_sb_lemma_to_type.clear();
+  d_sb_lemma_to_size.clear();
+}
+
 bool TermDbSygus::isRegistered( TypeNode tn ) {
   return d_register.find( tn )!=d_register.end();
 }
@@ -1202,7 +1255,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms
         unsigned start = d_node_mv_args_proc[n][vn];
         // get explanation in terms of testers
         std::vector< Node > antec_exp;
-        d_syexp->getExplanationForConstantEquality(n, vn, antec_exp);
+        d_syexp->getExplanationForEquality(n, vn, antec_exp);
         Node antec = antec_exp.size()==1 ? antec_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
         //Node antec = n.eqNode( vn );
         TypeNode tn = n.getType();
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index e796a3adc..7ef9e6151 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -40,21 +40,31 @@ class TermDbSygus {
   std::string identify() const { return "TermDbSygus"; }
   /** register the sygus type */
   void registerSygusType(TypeNode tn);
-  /** register a variable e that we will do enumerative search on
-   * conj is the conjecture that the enumeration of e is for.
-   * f is the synth-fun that the enumeration of e is for.
-   * mkActiveGuard is whether we want to make an active guard for e 
+
+  //------------------------------utilities
+  /** get the explanation utility */
+  SygusExplain* getExplain() { return d_syexp.get(); }
+  /** get the extended rewrite utility */
+  ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
+  //------------------------------end utilities
+
+  //------------------------------enumerators
+  /**
+   * Register a variable e that we will do enumerative search on.
+   * conj : the conjecture that the enumeration of e is for.
+   * f : the synth-fun that the enumeration of e is for.
+   * mkActiveGuard : whether we want to make an active guard for e
    * (see d_enum_to_active_guard).
    *
-   * Notice that enumerator e may not be equivalent
-   * to f in synthesis-through-unification approaches
-   * (e.g. decision tree construction for PBE synthesis).
+   * Notice that enumerator e may not be one-to-one with f in
+   * synthesis-through-unification approaches (e.g. decision tree construction
+   * for PBE synthesis).
    */
   void registerEnumerator(Node e,
                           Node f,
                           CegConjecture* conj,
                           bool mkActiveGuard = false);
-  /** is e an enumerator? */
+  /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
   CegConjecture* getConjectureForEnumerator(Node e);
@@ -64,10 +74,36 @@ class TermDbSygus {
   Node getActiveGuardForEnumerator(Node e);
   /** get all registered enumerators */
   void getEnumerators(std::vector<Node>& mts);
-  /** get the explanation utility */
-  SygusExplain* getExplain() { return d_syexp.get(); }
-  /** get the extended rewrite utility */
-  ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
+  /** Register symmetry breaking lemma
+   *
+   * This function registers lem as a symmetry breaking lemma template for
+   * subterms of enumerator e. For more information on symmetry breaking
+   * lemma templates, see datatypes/datatypes_sygus.h.
+   *
+   * tn : the (sygus datatype) type that lem applies to, i.e. the
+   * type of terms that lem blocks models for,
+   * sz : the minimum size of terms that the lem blocks.
+   *
+   * Notice that the symmetry breaking lemma template should be relative to x,
+   * where x is returned by the call to getFreeVar( tn, 0 ) in this class.
+   */
+  void registerSymBreakLemma(Node e, Node lem, TypeNode tn, unsigned sz);
+  /** Has symmetry breaking lemmas been added for any enumerator? */
+  bool hasSymBreakLemmas(std::vector<Node>& enums) const;
+  /** Get symmetry breaking lemmas
+   *
+   * Returns the set of symmetry breaking lemmas that have been registered
+   * for enumerator e. It adds these to lemmas.
+   */
+  void getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const;
+  /** Get the type of term symmetry breaking lemma lem applies to */
+  TypeNode getTypeForSymBreakLemma(Node lem) const;
+  /** Get the minimum size of terms symmetry breaking lemma lem applies to */
+  unsigned getSizeForSymBreakLemma(Node lem) const;
+  /** Clear information about symmetry breaking lemmas */
+  void clearSymBreakLemmas();
+  //------------------------------end enumerators
+
   //-----------------------------conversion from sygus to builtin
   /** get free variable
    *
@@ -121,10 +157,15 @@ class TermDbSygus {
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
+
+  //------------------------------utilities
   /** sygus explanation */
   std::unique_ptr<SygusExplain> d_syexp;
   /** sygus explanation */
   std::unique_ptr<ExtendedRewriter> d_ext_rw;
+  //------------------------------end utilities
+
+  //------------------------------enumerators
   /** mapping from enumerator terms to the conjecture they are associated with
    */
   std::map<Node, CegConjecture*> d_enum_to_conjecture;
@@ -137,6 +178,13 @@ class TermDbSygus {
    *   if G is true, then there are more values of e to enumerate".
    */
   std::map<Node, Node> d_enum_to_active_guard;
+  /** mapping from enumerators to symmetry breaking clauses for them */
+  std::map<Node, std::vector<Node> > d_enum_to_sb_lemmas;
+  /** mapping from symmetry breaking lemmas to type */
+  std::map<Node, TypeNode> d_sb_lemma_to_type;
+  /** mapping from symmetry breaking lemmas to size */
+  std::map<Node, unsigned> d_sb_lemma_to_size;
+  //------------------------------end enumerators
 
   //-----------------------------conversion from sygus to builtin
   /** cache for sygusToBuiltin */