Minor improvements to sygus sampling. (#1577)

5 files changed, 247 insertions, 79 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 5198b44d0..c0f7f0ac2 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -814,6 +814,36 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
             std::ostream* out = nodeManagerOptions.getOut();
             (*out) << "(unsound-rewrite " << prev_bv << " " << bv << ")"
                    << std::endl;
+            // debugging information
+            if (Trace.isOn("sygus-rr-debug"))
+            {
+              int pt_index = its->second.getDiffSamplePointIndex(bv, prev_bv);
+              if (pt_index >= 0)
+              {
+                Trace("sygus-rr-debug")
+                    << "; both ext-rewrite to : " << bvr << std::endl;
+                Trace("sygus-rr-debug")
+                    << "; but are not equivalent for : " << std::endl;
+                std::vector<Node> vars;
+                std::vector<Node> pt;
+                its->second.getSamplePoint(pt_index, vars, pt);
+                Assert(vars.size() == pt.size());
+                for (unsigned i = 0, size = pt.size(); i < size; i++)
+                {
+                  Trace("sygus-rr-debug")
+                      << ";   " << vars[i] << " -> " << pt[i] << std::endl;
+                }
+                Node bv_e = its->second.evaluate(bv, pt_index);
+                Node pbv_e = its->second.evaluate(prev_bv, pt_index);
+                Assert(bv_e != pbv_e);
+                Trace("sygus-rr-debug") << "; where they evaluate to " << pbv_e
+                                        << " and " << bv_e << std::endl;
+              }
+              else
+              {
+                Assert(false);
+              }
+            }
           }
         }
       }
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 889a80879..d325f3f36 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -626,7 +626,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
       if (status != 0 && options::sygusRewSynth())
       {
         TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
-        std::map<Node, SygusSampler>::iterator its = d_sampler.find(prog);
+        std::map<Node, SygusSamplerExt>::iterator its = d_sampler.find(prog);
         if (its == d_sampler.end())
         {
           d_sampler[prog].initializeSygus(
@@ -638,45 +638,21 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         // eq_sol is a candidate solution that is equivalent to sol
         if (eq_sol != solb)
         {
-          // one of eq_sol or solb must be ordered
-          bool eqor = its->second.isOrdered(eq_sol);
-          bool sor = its->second.isOrdered(solb);
-          bool outputRewrite = false;
-          if (eqor || sor)
+          // Terms solb and eq_sol are equivalent under sample points but do
+          // not rewrite to the same term. Hence, this indicates a candidate
+          // rewrite.
+          out << "(candidate-rewrite " << solb << " " << eq_sol << ")"
+              << std::endl;
+          // debugging information
+          if (Trace.isOn("sygus-rr-debug"))
           {
-            outputRewrite = true;
-            // if only one is ordered, then the ordered one must contain the
-            // free variables of the other
-            if (!eqor)
-            {
-              outputRewrite = its->second.containsFreeVariables(solb, eq_sol);
-            }
-            else if (!sor)
-            {
-              outputRewrite = its->second.containsFreeVariables(eq_sol, solb);
-            }
-          }
-
-          if (outputRewrite)
-          {
-            // Terms solb and eq_sol are equivalent under sample points but do
-            // not rewrite to the same term. Hence, this indicates a candidate
-            // rewrite.
-            out << "(candidate-rewrite " << solb << " " << eq_sol << ")"
-                << std::endl;
-            // if the previous value stored was unordered, but this is
-            // ordered, we prefer this one. Thus, we force its addition to the
-            // sampler database.
-            if (!eqor)
-            {
-              its->second.registerTerm(solb, true);
-            }
-          }
-          else
-          {
-            Trace("sygus-synth-rr")
-                << "Alpha equivalent candidate rewrite : " << eq_sol << " "
-                << solb << std::endl;
+            ExtendedRewriter* er = sygusDb->getExtRewriter();
+            Node solbr = er->extendedRewrite(solb);
+            Node eq_solr = er->extendedRewrite(eq_sol);
+            Trace("sygus-rr-debug")
+                << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
+            Trace("sygus-rr-debug")
+                << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
           }
         }
       }
@@ -865,8 +841,9 @@ bool CegConjecture::sampleAddRefinementLemma(std::vector<Node>& vals,
         Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
         // mark this as a CEGIS point (no longer sampled)
         d_cegis_sample_refine.insert(i);
+        std::vector<Node> vars;
         std::vector<Node> pt;
-        d_cegis_sampler.getSamplePoint(i, pt);
+        d_cegis_sampler.getSamplePoint(i, vars, pt);
         Assert(d_base_vars.size() == pt.size());
         Node rlem = d_base_body.substitute(
             d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());
diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
index dae261111..ebcecbe0f 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -261,7 +261,7 @@ private:
    * This is used for the sygusRewSynth() option to synthesize new candidate
    * rewrite rules.
    */
-  std::map<Node, SygusSampler> d_sampler;
+  std::map<Node, SygusSamplerExt> d_sampler;
   /** sampler object for the option cegisSample()
    *
    * This samples points of the type of the inner variables of the synthesis
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index f824cd6f7..c7c322132 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -74,16 +74,33 @@ void SygusSampler::initialize(TypeNode tn,
   d_is_valid = true;
   d_tn = tn;
   d_ftn = TypeNode::null();
+  d_type_vars.clear();
+  d_vars.clear();
+  d_rvalue_cindices.clear();
+  d_rvalue_null_cindices.clear();
+  d_var_sygus_types.clear();
   d_vars.insert(d_vars.end(), vars.begin(), vars.end());
-  for (const Node& sv : vars)
+  std::map<TypeNode, unsigned> type_to_type_id;
+  unsigned type_id_counter = 0;
+  for (const Node& sv : d_vars)
   {
     TypeNode svt = sv.getType();
-    d_var_index[sv] = d_type_vars[svt].size();
-    d_type_vars[svt].push_back(sv);
+    unsigned tnid;
+    std::map<TypeNode, unsigned>::iterator itt = type_to_type_id.find(svt);
+    if (itt == type_to_type_id.end())
+    {
+      type_to_type_id[svt] = type_id_counter;
+      type_id_counter++;
+    }
+    else
+    {
+      tnid = itt->second;
+    }
+    Trace("sygus-sample-debug")
+        << "Type id for " << sv << " is " << tnid << std::endl;
+    d_var_index[sv] = d_type_vars[tnid].size();
+    d_type_vars[tnid].push_back(sv);
   }
-  d_rvalue_cindices.clear();
-  d_rvalue_null_cindices.clear();
-  d_var_sygus_types.clear();
   initializeSamples(nsamples);
 }
 
@@ -99,24 +116,68 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples)
 
   Trace("sygus-sample") << "Register sampler for " << f << std::endl;
 
+  d_vars.clear();
+  d_type_vars.clear();
   d_var_index.clear();
   d_type_vars.clear();
+  d_rvalue_cindices.clear();
+  d_rvalue_null_cindices.clear();
+  d_var_sygus_types.clear();
   // get the sygus variable list
   Node var_list = Node::fromExpr(dt.getSygusVarList());
   if (!var_list.isNull())
   {
     for (const Node& sv : var_list)
     {
-      TypeNode svt = sv.getType();
-      d_var_index[sv] = d_type_vars[svt].size();
       d_vars.push_back(sv);
-      d_type_vars[svt].push_back(sv);
     }
   }
-  d_rvalue_cindices.clear();
-  d_rvalue_null_cindices.clear();
-  d_var_sygus_types.clear();
+  // register sygus type
   registerSygusType(d_ftn);
+  // Variables are associated with type ids based on the set of sygus types they
+  // appear in.
+  std::map<Node, unsigned> var_to_type_id;
+  unsigned type_id_counter = 0;
+  for (const Node& sv : d_vars)
+  {
+    TypeNode svt = sv.getType();
+    // is it equivalent to a previous variable?
+    for (const std::pair<Node, unsigned>& v : var_to_type_id)
+    {
+      Node svc = v.first;
+      if (svc.getType() == svt)
+      {
+        if (d_var_sygus_types[sv].size() == d_var_sygus_types[svc].size())
+        {
+          bool success = true;
+          for (unsigned t = 0, size = d_var_sygus_types[sv].size(); t < size;
+               t++)
+          {
+            if (d_var_sygus_types[sv][t] != d_var_sygus_types[svc][t])
+            {
+              success = false;
+              break;
+            }
+          }
+          if (success)
+          {
+            var_to_type_id[sv] = var_to_type_id[svc];
+          }
+        }
+      }
+    }
+    if (var_to_type_id.find(sv) == var_to_type_id.end())
+    {
+      var_to_type_id[sv] = type_id_counter;
+      type_id_counter++;
+    }
+    unsigned tnid = var_to_type_id[sv];
+    Trace("sygus-sample-debug")
+        << "Type id for " << sv << " is " << tnid << std::endl;
+    d_var_index[sv] = d_type_vars[tnid].size();
+    d_type_vars[tnid].push_back(sv);
+  }
+
   initializeSamples(nsamples);
 }
 
@@ -231,7 +292,7 @@ bool SygusSampler::isContiguous(Node n)
   std::vector<Node> fvs;
   computeFreeVariables(n, fvs);
   // compute contiguous condition
-  for (const std::pair<const TypeNode, std::vector<Node> >& p : d_type_vars)
+  for (const std::pair<const unsigned, std::vector<Node> >& p : d_type_vars)
   {
     bool foundNotFv = false;
     for (const Node& v : p.second)
@@ -282,7 +343,7 @@ void SygusSampler::computeFreeVariables(Node n, std::vector<Node>& fvs)
 bool SygusSampler::isOrdered(Node n)
 {
   // compute free variables in n for each type
-  std::map<TypeNode, std::vector<Node> > fvs;
+  std::map<unsigned, std::vector<Node> > fvs;
 
   std::unordered_set<TNode, TNodeHashFunction> visited;
   std::unordered_set<TNode, TNodeHashFunction>::iterator it;
@@ -301,13 +362,13 @@ bool SygusSampler::isOrdered(Node n)
         std::map<Node, unsigned>::iterator itv = d_var_index.find(cur);
         if (itv != d_var_index.end())
         {
-          TypeNode tn = cur.getType();
+          unsigned tnid = d_type_ids[cur];
           // if this variable is out of order
-          if (itv->second != fvs[tn].size())
+          if (itv->second != fvs[tnid].size())
           {
             return false;
           }
-          fvs[tn].push_back(cur);
+          fvs[tnid].push_back(cur);
         }
       }
       for (unsigned j = 0, nchildren = cur.getNumChildren(); j < nchildren; j++)
@@ -353,9 +414,12 @@ bool SygusSampler::containsFreeVariables(Node a, Node b)
   return true;
 }
 
-void SygusSampler::getSamplePoint(unsigned index, std::vector<Node>& pt)
+void SygusSampler::getSamplePoint(unsigned index,
+                                  std::vector<Node>& vars,
+                                  std::vector<Node>& pt)
 {
   Assert(index < d_samples.size());
+  vars.insert(vars.end(), d_vars.begin(), d_vars.end());
   std::vector<Node>& spt = d_samples[index];
   pt.insert(pt.end(), spt.begin(), spt.end());
 }
@@ -372,6 +436,20 @@ Node SygusSampler::evaluate(Node n, unsigned index)
   return ev;
 }
 
+int SygusSampler::getDiffSamplePointIndex(Node a, Node b)
+{
+  for (unsigned i = 0, nsamp = d_samples.size(); i < nsamp; i++)
+  {
+    Node ae = evaluate(a, i);
+    Node be = evaluate(b, i);
+    if (ae != be)
+    {
+      return i;
+    }
+  }
+  return -1;
+}
+
 Node SygusSampler::getRandomValue(TypeNode tn)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -562,6 +640,51 @@ void SygusSampler::registerSygusType(TypeNode tn)
   }
 }
 
+Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
+{
+  Node eq_n = SygusSampler::registerTerm(n, forceKeep);
+  if (eq_n == n)
+  {
+    return n;
+  }
+  // one of eq_n or n must be ordered
+  bool eqor = isOrdered(eq_n);
+  bool nor = isOrdered(n);
+  bool isUnique = false;
+  if (eqor || nor)
+  {
+    isUnique = true;
+    // if only one is ordered, then the ordered one must contain the
+    // free variables of the other
+    if (!eqor)
+    {
+      isUnique = containsFreeVariables(n, eq_n);
+    }
+    else if (!nor)
+    {
+      isUnique = containsFreeVariables(eq_n, n);
+    }
+  }
+
+  if (isUnique)
+  {
+    // if the previous value stored was unordered, but this is
+    // ordered, we prefer this one. Thus, we force its addition to the
+    // sampler database.
+    if (!eqor)
+    {
+      registerTerm(n, true);
+    }
+    return eq_n;
+  }
+  else
+  {
+    Trace("sygus-synth-rr") << "Alpha equivalent candidate rewrite : " << eq_n
+                            << " " << n << std::endl;
+  }
+  return n;
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 02b60d155..d8f2244c7 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -155,22 +155,40 @@ class SygusSampler : public LazyTrieEvaluator
    * forceKeep is whether we wish to force that n is chosen as a representative
    * value in the trie.
    */
-  Node registerTerm(Node n, bool forceKeep = false);
+  virtual Node registerTerm(Node n, bool forceKeep = false);
+  /** get number of sample points */
+  unsigned getNumSamplePoints() const { return d_samples.size(); }
+  /** get sample point
+   *
+   * Appends sample point #index to the vector pt, d_vars to vars.
+   */
+  void getSamplePoint(unsigned index,
+                      std::vector<Node>& vars,
+                      std::vector<Node>& pt);
+  /** evaluate n on sample point index */
+  Node evaluate(Node n, unsigned index);
+  /**
+   * Returns the index of a sample point such that the evaluation of a and b
+   * diverge, or -1 if no such sample point exists.
+   */
+  int getDiffSamplePointIndex(Node a, Node b);
+
+ protected:
   /** is contiguous
    *
    * This returns whether n's free variables (terms occurring in the range of
    * d_type_vars) are a prefix of the list of variables in d_type_vars for each
-   * type. For instance, if d_type_vars[Int] = { x, y }, then 0, x, x+y, y+x are
-   * contiguous but y is not. This is useful for excluding terms from
-   * consideration that are alpha-equivalent to others.
+   * type id. For instance, if d_type_vars[id] = { x, y } for some id, then
+   * 0, x, x+y, y+x are contiguous but y is not. This is useful for excluding
+   * terms from consideration that are alpha-equivalent to others.
    */
   bool isContiguous(Node n);
   /** is ordered
    *
    * This returns whether n's free variables are in order with respect to
    * variables in d_type_vars for each type. For instance, if
-   * d_type_vars[Int] = { x, y }, then 0, x, x+y are ordered but y and y+x
-   * are not.
+   * d_type_vars[id] = { x, y } for some id, then 0, x, x+y are ordered but
+   * y and y+x are not.
    */
   bool isOrdered(Node n);
   /** contains free variables
@@ -179,16 +197,6 @@ class SygusSampler : public LazyTrieEvaluator
    * are those that occur in the range d_type_vars.
    */
   bool containsFreeVariables(Node a, Node b);
-  /** get number of sample points */
-  unsigned getNumSamplePoints() const { return d_samples.size(); }
-  /** get sample point
-   *
-   * Appends sample point #index to the vector pt.
-   */
-  void getSamplePoint(unsigned index, std::vector<Node>& pt);
-  /** evaluate n on sample point index */
-  Node evaluate(Node n, unsigned index);
-
  private:
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;
@@ -211,20 +219,33 @@ class SygusSampler : public LazyTrieEvaluator
   TypeNode d_tn;
   /** the sygus type for this sampler (if applicable). */
   TypeNode d_ftn;
-  /** all variables */
+  /** all variables we are sampling values for */
   std::vector<Node> d_vars;
   /** type variables
    *
-   * For each type, a list of variables in the grammar we are considering, for
-   * that type. These typically correspond to the arguments of the
+   * We group variables according to "type ids". Two variables have the same
+   * type id if they have indistinguishable status according to this sampler.
+   * This is a finer-grained grouping than types. For example, two variables
+   * of the same type may have different type ids if they occur as constructors
+   * of a different set of sygus types in the grammar we are considering.
+   * For instance, we assign x and y different type ids in this grammar:
+   *   A -> B + C
+   *   B -> x | 0 | 1
+   *   C -> y
+   * Type ids are computed for each variable in d_vars during initialize(...).
+   *
+   * For each type id, a list of variables in the grammar we are considering,
+   * for that type. These typically correspond to the arguments of the
    * function-to-synthesize whose grammar we are considering.
    */
-  std::map<TypeNode, std::vector<Node> > d_type_vars;
+  std::map<unsigned, std::vector<Node> > d_type_vars;
   /**
    * A map all variables in the grammar we are considering to their index in
    * d_type_vars.
    */
   std::map<Node, unsigned> d_var_index;
+  /**  Map from variables to the id (the domain of d_type_vars). */
+  std::map<Node, unsigned> d_type_ids;
   /** constants
    *
    * For each type, a list of constants in the grammar we are considering, for
@@ -300,6 +321,23 @@ class SygusSampler : public LazyTrieEvaluator
   void registerSygusType(TypeNode tn);
 };
 
+/** Version of the above class with some additional features */
+class SygusSamplerExt : public SygusSampler
+{
+ public:
+  /** register term n with this sampler database
+   *
+   * This returns a term ret with the same guarantees as
+   * SygusSampler::registerTerm, with the additional guarantee
+   * that for all ret' returned by a previous call to registerTerm( n' ),
+   * we have that ret = n is not alpha-equivalent to ret' = n,
+   * modulo symmetry of equality. For example,
+   *   (t+0), t and (s+0), s
+   * will not be input/output pairs of this function.
+   */
+  virtual Node registerTerm(Node n, bool forceKeep = false) override;
+};
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */