Sample based on sygus grammar by default (#1558)

5 files changed, 307 insertions, 25 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 34af81033..c58313390 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -308,6 +308,8 @@ option sygusRewVerify --sygus-rr-verify bool :default false
   use sygus to verify the correctness of rewrite rules via sampling
 option sygusSamples --sygus-samples=N int :read-write :default 100 :read-write
   number of points to consider when doing sygus rewriter sample testing
+option sygusSampleGrammar --sygus-sample-grammar bool :default true
+  when applicable, use grammar for choosing sample points
 
 # CEGQI applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 0b8f390f3..82720dd5e 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus_sampler.h"
 
+#include "options/quantifiers_options.h"
 #include "util/bitvector.h"
 #include "util/random.h"
 
@@ -80,6 +81,9 @@ void SygusSampler::initialize(TypeNode tn,
     d_var_index[sv] = d_type_vars[svt].size();
     d_type_vars[svt].push_back(sv);
   }
+  d_rvalue_cindices.clear();
+  d_rvalue_null_cindices.clear();
+  d_var_sygus_types.clear();
   initializeSamples(nsamples);
 }
 
@@ -109,6 +113,10 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples)
       d_type_vars[svt].push_back(sv);
     }
   }
+  d_rvalue_cindices.clear();
+  d_rvalue_null_cindices.clear();
+  d_var_sygus_types.clear();
+  registerSygusType(d_ftn);
   initializeSamples(nsamples);
 }
 
@@ -123,28 +131,90 @@ void SygusSampler::initializeSamples(unsigned nsamples)
     Trace("sygus-sample") << "  var #" << types.size() << " : " << v << " : "
                           << vt << std::endl;
   }
+  std::map<unsigned, std::map<Node, std::vector<TypeNode> >::iterator> sts;
+  if (options::sygusSampleGrammar())
+  {
+    for (unsigned j = 0, size = types.size(); j < size; j++)
+    {
+      sts[j] = d_var_sygus_types.find(d_vars[j]);
+    }
+  }
+
+  unsigned nduplicates = 0;
   for (unsigned i = 0; i < nsamples; i++)
   {
     std::vector<Node> sample_pt;
-    Trace("sygus-sample") << "Sample point #" << i << " : ";
     for (unsigned j = 0, size = types.size(); j < size; j++)
     {
-      Node r = getRandomValue(types[j]);
+      Node v = d_vars[j];
+      Node r;
+      if (options::sygusSampleGrammar())
+      {
+        // choose a random start sygus type, if possible
+        if (sts[j] != d_var_sygus_types.end())
+        {
+          unsigned ntypes = sts[j]->second.size();
+          Assert(ntypes > 0);
+          unsigned index = Random::getRandom().pick(0, ntypes - 1);
+          if (index < ntypes)
+          {
+            // currently hard coded to 0.0, 0.5
+            r = getSygusRandomValue(sts[j]->second[index], 0.0, 0.5);
+          }
+        }
+      }
       if (r.isNull())
       {
-        Trace("sygus-sample") << "INVALID";
-        d_is_valid = false;
+        r = getRandomValue(types[j]);
+        if (r.isNull())
+        {
+          d_is_valid = false;
+        }
       }
-      Trace("sygus-sample") << r << " ";
       sample_pt.push_back(r);
     }
-    Trace("sygus-sample") << std::endl;
-    d_samples.push_back(sample_pt);
+    if (d_samples_trie.add(sample_pt))
+    {
+      if (Trace.isOn("sygus-sample"))
+      {
+        Trace("sygus-sample") << "Sample point #" << i << " : ";
+        for (const Node& r : sample_pt)
+        {
+          Trace("sygus-sample") << r << " ";
+        }
+        Trace("sygus-sample") << std::endl;
+      }
+      d_samples.push_back(sample_pt);
+    }
+    else
+    {
+      i--;
+      nduplicates++;
+      if (nduplicates == nsamples * 10)
+      {
+        Trace("sygus-sample")
+            << "...WARNING: excessive duplicates, cut off sampling at " << i
+            << "/" << nsamples << " points." << std::endl;
+        break;
+      }
+    }
   }
 
   d_trie.clear();
 }
 
+bool SygusSampler::PtTrie::add(std::vector<Node>& pt)
+{
+  PtTrie* curr = this;
+  for (unsigned i = 0, size = pt.size(); i < size; i++)
+  {
+    curr = &(curr->d_children[pt[i]]);
+  }
+  bool retVal = curr->d_children.empty();
+  curr = &(curr->d_children[Node::null()]);
+  return retVal;
+}
+
 Node SygusSampler::registerTerm(Node n, bool forceKeep)
 {
   if (d_is_valid)
@@ -389,6 +459,109 @@ Node SygusSampler::getRandomValue(TypeNode tn)
   return Node::null();
 }
 
+Node SygusSampler::getSygusRandomValue(TypeNode tn,
+                                       double rchance,
+                                       double rinc,
+                                       unsigned depth)
+{
+  Assert(tn.isDatatype());
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
+  Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
+  Trace("sygus-sample-grammar") << "Sygus random value " << tn
+                                << ", depth = " << depth
+                                << ", rchance = " << rchance << std::endl;
+  // check if we terminate on this call
+  // we refuse to enumerate terms of 10+ depth as a hard limit
+  bool terminate = Random::getRandom().pickWithProb(rchance) || depth >= 10;
+  // if we terminate, only nullary constructors can be chosen
+  std::vector<unsigned>& cindices =
+      terminate ? d_rvalue_null_cindices[tn] : d_rvalue_cindices[tn];
+  unsigned ncons = cindices.size();
+  // select a random constructor, or random value when index=ncons.
+  unsigned index = Random::getRandom().pick(0, ncons);
+  Trace("sygus-sample-grammar") << "Random index 0..." << ncons
+                                << " was : " << index << std::endl;
+  if (index < ncons)
+  {
+    Trace("sygus-sample-grammar") << "Recurse constructor index #" << index
+                                  << std::endl;
+    unsigned cindex = cindices[index];
+    Assert(cindex < dt.getNumConstructors());
+    const DatatypeConstructor& dtc = dt[cindex];
+    // more likely to terminate in recursive calls
+    double rchance_new = rchance + (1.0 - rchance) * rinc;
+    std::map<int, Node> pre;
+    bool success = true;
+    // generate random values for all arguments
+    for (unsigned i = 0, nargs = dtc.getNumArgs(); i < nargs; i++)
+    {
+      TypeNode tnc = d_tds->getArgType(dtc, i);
+      Node c = getSygusRandomValue(tnc, rchance_new, rinc, depth + 1);
+      if (c.isNull())
+      {
+        success = false;
+        Trace("sygus-sample-grammar") << "...fail." << std::endl;
+        break;
+      }
+      Trace("sygus-sample-grammar") << "  child #" << i << " : " << c
+                                    << std::endl;
+      pre[i] = c;
+    }
+    if (success)
+    {
+      Trace("sygus-sample-grammar") << "mkGeneric" << std::endl;
+      Node ret = d_tds->mkGeneric(dt, cindex, pre);
+      Trace("sygus-sample-grammar") << "...returned " << ret << std::endl;
+      ret = Rewriter::rewrite(ret);
+      Trace("sygus-sample-grammar") << "...after rewrite " << ret << std::endl;
+      Assert(ret.isConst());
+      return ret;
+    }
+  }
+  Trace("sygus-sample-grammar") << "...resort to random value" << std::endl;
+  // if we did not generate based on the grammar, pick a random value
+  return getRandomValue(TypeNode::fromType(dt.getSygusType()));
+}
+
+// recursion depth bounded by number of types in grammar (small)
+void SygusSampler::registerSygusType(TypeNode tn)
+{
+  if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end())
+  {
+    d_rvalue_cindices[tn].clear();
+    Assert(tn.isDatatype());
+    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    Assert(dt.isSygus());
+    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+    {
+      const DatatypeConstructor& dtc = dt[i];
+      Node sop = Node::fromExpr(dtc.getSygusOp());
+      bool isVar = std::find(d_vars.begin(), d_vars.end(), sop) != d_vars.end();
+      if (isVar)
+      {
+        // if it is a variable, add it to the list of sygus types for that var
+        d_var_sygus_types[sop].push_back(tn);
+      }
+      else
+      {
+        // otherwise, it is a constructor for sygus random value
+        d_rvalue_cindices[tn].push_back(i);
+        if (dtc.getNumArgs() == 0)
+        {
+          d_rvalue_null_cindices[tn].push_back(i);
+        }
+      }
+      // recurse on all subfields
+      for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
+      {
+        TypeNode tnc = d_tds->getArgType(dtc, j);
+        registerSygusType(tnc);
+      }
+    }
+  }
+}
+
 } /* 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 09f4124fe..02b60d155 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -194,6 +194,19 @@ class SygusSampler : public LazyTrieEvaluator
   TermDbSygus* d_tds;
   /** samples */
   std::vector<std::vector<Node> > d_samples;
+  /** data structure to check duplication of sample points */
+  class PtTrie
+  {
+   public:
+    /** add pt to this trie, returns true if pt is not a duplicate. */
+    bool add(std::vector<Node>& pt);
+
+   private:
+    /** the children of this node */
+    std::map<Node, PtTrie> d_children;
+  };
+  /** a trie for samples */
+  PtTrie d_samples_trie;
   /** type of nodes we will be registering with this class */
   TypeNode d_tn;
   /** the sygus type for this sampler (if applicable). */
@@ -246,11 +259,45 @@ class SygusSampler : public LazyTrieEvaluator
    * length, currently by a repeated coin flip.
    * Real : returns the division of two random integers, where the denominator
    * is omitted if it is zero.
-   *
-   * TODO (#1549): improve this function. Can use the grammar to generate
-   * interesting sample points.
    */
   Node getRandomValue(TypeNode tn);
+  /** get sygus random value
+   *
+   * Returns a random value based on the sygus type tn. The return value is
+   * a constant in the analog type of tn. This function chooses either to
+   * return a random value, or otherwise will construct a constant based on
+   * a random constructor of tn whose builtin operator is not a variable.
+   *
+   * rchance: the chance that the call to this function will be forbidden
+   * from making recursive calls and instead must return a value based on
+   * a nullary constructor of tn or based on getRandomValue above.
+   * rinc: the percentage to increment rchance on recursive calls.
+   *
+   * For example, consider the grammar:
+   *   A -> x | y | 0 | 1 | +( A, A ) | ite( B, A, A )
+   *   B -> A = A
+   * If we call this function on A and rchance is 0.0, there are five evenly
+   * chosen possibilities, either we return a random value via getRandomValue
+   * above, or we choose one of the four non-variable constructors of A.
+   * Say we choose ite, then we recursively call this function for
+   * B, A, and A, which return constants c1, c2, and c3. Then, this function
+   * returns the rewritten form of ite( c1, c2, c3 ).
+   * If on the other hand, rchance was 0.5 and rand() < 0.5. Then, we force
+   * this call to terminate by either selecting a random value via
+   * getRandomValue, 0 or 1.
+   */
+  Node getSygusRandomValue(TypeNode tn,
+                           double rchance,
+                           double rinc,
+                           unsigned depth = 0);
+  /** map from sygus types to non-variable constructors */
+  std::map<TypeNode, std::vector<unsigned> > d_rvalue_cindices;
+  /** map from sygus types to non-variable nullary constructors */
+  std::map<TypeNode, std::vector<unsigned> > d_rvalue_null_cindices;
+  /** map from variables to sygus types that include them */
+  std::map<Node, std::vector<TypeNode> > d_var_sygus_types;
+  /** register sygus type, intializes the above two data structures */
+  void registerSygusType(TypeNode tn);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index 87bfa1901..7d7cc624e 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -147,6 +147,12 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
   return ret;
 }
 
+Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
+{
+  std::map<TypeNode, int> var_count;
+  return mkGeneric(dt, c, var_count, pre);
+}
+
 Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
   Assert( n.getType()==tn );
   Assert( tn.isDatatype() );
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 586ef0777..af1ef50b6 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -68,6 +68,56 @@ class TermDbSygus {
   SygusExplain* getExplain() { return d_syexp.get(); }
   /** get the extended rewrite utility */
   ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
+  //-----------------------------conversion from sygus to builtin
+  /** get free variable
+   *
+   * This class caches a list of free variables for each type, which are
+   * used, for instance, for constructing canonical forms of terms with free
+   * variables. This function returns the i^th free variable for type tn.
+   * If useSygusType is true, then this function returns a variable of the
+   * analog type for sygus type tn (see d_fv for details).
+   */
+  TNode getFreeVar(TypeNode tn, int i, bool useSygusType = false);
+  /** get free variable and increment
+   *
+   * This function returns the next free variable for type tn, and increments
+   * the counter in var_count for that type.
+   */
+  TNode getFreeVarInc(TypeNode tn,
+                      std::map<TypeNode, int>& var_count,
+                      bool useSygusType = false);
+  /** returns true if n is a cached free variable (in d_fv). */
+  bool isFreeVar(Node n) { return d_fv_stype.find(n) != d_fv_stype.end(); }
+  /** returns the index of n in the free variable cache (d_fv). */
+  int getVarNum(Node n) { return d_fv_num[n]; }
+  /** returns true if n has a cached free variable (in d_fv). */
+  bool hasFreeVar(Node n);
+  /** make generic
+   *
+   * This function returns a builtin term f( t1, ..., tn ) where f is the
+   * builtin op of the sygus datatype constructor specified by arguments
+   * dt and c. The mapping pre maps child indices to the term for that index
+   * in the term we are constructing. That is, for each i = 1,...,n:
+   *   If i is in the domain of pre, then ti = pre[i].
+   *   If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ],
+   *     and var_count[Ti] is incremented.
+   */
+  Node mkGeneric(const Datatype& dt,
+                 int c,
+                 std::map<TypeNode, int>& var_count,
+                 std::map<int, Node>& pre);
+  /** same as above, but with empty var_count */
+  Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
+  /** sygus to builtin
+   *
+   * Given a sygus datatype term n of type tn, this function returns its analog,
+   * that is, the term that n encodes.
+   */
+  Node sygusToBuiltin(Node n, TypeNode tn);
+  /** same as above, but without tn */
+  Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
+  //-----------------------------end conversion from sygus to builtin
+
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -88,23 +138,31 @@ class TermDbSygus {
    */
   std::map<Node, Node> d_enum_to_active_guard;
 
+  //-----------------------------conversion from sygus to builtin
+  /** cache for sygusToBuiltin */
+  std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
+  /** a cache of fresh variables for each type
+   *
+   * We store two versions of this list:
+   *   index 0: mapping from builtin types to fresh variables of that type,
+   *   index 1: mapping from sygus types to fresh varaibles of the type they
+   *            encode.
+   */
+  std::map<TypeNode, std::vector<Node> > d_fv[2];
+  /** Maps free variables to the domain type they are associated with in d_fv */
+  std::map<Node, TypeNode> d_fv_stype;
+  /** Maps free variables to their index in d_fv. */
+  std::map<Node, int> d_fv_num;
+  /** recursive helper for hasFreeVar, visited stores nodes we have visited. */
+  bool hasFreeVar(Node n, std::map<Node, bool>& visited);
+  //-----------------------------end conversion from sygus to builtin
+
   // TODO :issue #1235 : below here needs refactor
 
  public:
   Node d_true;
   Node d_false;
 
- private:
-  std::map< TypeNode, std::vector< Node > > d_fv[2];
-  std::map< Node, TypeNode > d_fv_stype;
-  std::map< Node, int > d_fv_num;
-  bool hasFreeVar( Node n, std::map< Node, bool >& visited );
-public:
-  TNode getFreeVar( TypeNode tn, int i, bool useSygusType = false );
-  TNode getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType = false );
-  bool isFreeVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); }
-  int getVarNum( Node n ) { return d_fv_num[n]; }
-  bool hasFreeVar( Node n );
 private:
   void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
   bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
@@ -122,7 +180,6 @@ private:
   std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
   // normalized map
   std::map<TypeNode, std::map<Node, Node> > d_normalized;
-  std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
   // grammar information
   // root -> type -> _
   std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
@@ -165,9 +222,6 @@ private:
   bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
 
   TypeNode getSygusTypeForVar( Node v );
-  Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
-  Node sygusToBuiltin( Node n, TypeNode tn );
-  Node sygusToBuiltin( Node n ) { return sygusToBuiltin( n, n.getType() ); }
   Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized(TypeNode t, Node prog);