Improvements to sygus sampling (#1621)

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index e97f11db9bcb445602053bf965d61c3a1f426d7c..6552b9157d9f73c09ee19c7e46ccedc23bed99c2 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -306,7 +306,7 @@ option sygusRewSynth --sygus-rr-synth bool :read-write :default false
   use sygus to enumerate candidate rewrite rules via sampling
 option sygusRewVerify --sygus-rr-verify bool :read-write :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
+option sygusSamples --sygus-samples=N int :read-write :default 1000 :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

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 556b07f7f4b4b84da142d739901778f561b919e7..728cd81351a4eae826d8a30db367cf441a860b8a 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -790,60 +790,63 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
       if (options::sygusRewVerify())
       {
         // add to the sampler database object
-        std::map<Node, quantifiers::SygusSampler>::iterator its =
-            d_sampler.find(a);
-        if (its == d_sampler.end())
+        std::map<TypeNode, quantifiers::SygusSampler>::iterator its =
+            d_sampler[a].find(tn);
+        if (its == d_sampler[a].end())
         {
-          d_sampler[a].initializeSygus(d_tds, a, options::sygusSamples());
-          its = d_sampler.find(a);
+          d_sampler[a][tn].initializeSygus(d_tds, nv, options::sygusSamples());
+          its = d_sampler[a].find(tn);
         }
+        Node bvr_sample_ret;
+        std::map<Node, Node>::iterator itsv =
+            d_cache[a].d_search_val_sample[tn].find(bvr);
+        if (itsv == d_cache[a].d_search_val_sample[tn].end())
+        {
+          // initialize the sampler for the rewritten form of this node
+          bvr_sample_ret = its->second.registerTerm(bvr);
+          d_cache[a].d_search_val_sample[tn][bvr] = bvr_sample_ret;
+        }
+        else
+        {
+          bvr_sample_ret = itsv->second;
+        }
+
+        // register the current node with the sampler
         Node sample_ret = its->second.registerTerm(bv);
-        d_cache[a].d_search_val_sample[nv] = sample_ret;
-        if (itsv != d_cache[a].d_search_val[tn].end())
+
+        // bv and bvr should be equivalent under examples
+        if (sample_ret != bvr_sample_ret)
         {
-          // if the analog of this term and another term were rewritten to the
-          // same term, then they should be equivalent under examples.
-          Node prev = itsv->second;
-          Node prev_sample_ret = d_cache[a].d_search_val_sample[prev];
-          if (sample_ret != prev_sample_ret)
+          // we have detected unsoundness in the rewriter
+          Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
+          std::ostream* out = nodeManagerOptions.getOut();
+          (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
+          // debugging information
+          if (Trace.isOn("sygus-rr-debug"))
           {
-            Node prev_bv = d_tds->sygusToBuiltin(prev, tn);
-            // we have detected unsoundness in the rewriter
-            Options& nodeManagerOptions =
-                NodeManager::currentNM()->getOptions();
-            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, bvr);
+            if (pt_index >= 0)
             {
-              int pt_index = its->second.getDiffSamplePointIndex(bv, prev_bv);
-              if (pt_index >= 0)
+              Trace("sygus-rr-debug")
+                  << "; unsound: 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")
-                    << "; unsound: both ext-rewrite to : " << bvr << std::endl;
-                Trace("sygus-rr-debug")
-                    << "; unsound: 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") << "; unsound:    " << 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") << "; unsound: where they evaluate to "
-                                        << pbv_e << " and " << bv_e
-                                        << std::endl;
-              }
-              else
-              {
-                Assert(false);
+                Trace("sygus-rr-debug") << "; unsound:    " << vars[i] << " -> "
+                                        << pt[i] << std::endl;
               }
+              Node bv_e = its->second.evaluate(bv, pt_index);
+              Node pbv_e = its->second.evaluate(bvr, pt_index);
+              Assert(bv_e != pbv_e);
+              Trace("sygus-rr-debug") << "; unsound: where they evaluate to "
+                                      << pbv_e << " and " << bv_e << std::endl;
+            }
+            else
+            {
+              Assert(false);
             }
           }
         }

diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 2c1f85deb2c60cc373a1529b959cc51ca4829082..fa3918270c28d5fb388081bd3e3a0ecea62ab791 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -54,10 +54,37 @@ private:
   NodeSet d_active_terms;
   IntMap d_currTermSize;
   Node d_zero;
-private:
+
+ private:
+  /**
+   * Map from terms (selector chains) to their anchors. The anchor of a
+   * selector chain S1( ... Sn( x ) ... ) is x.
+   */
   std::map< Node, Node > d_term_to_anchor;
+  /**
+   * Map from terms (selector chains) to the conjecture that their anchor is
+   * associated with.
+   */
   std::map<Node, quantifiers::CegConjecture*> d_term_to_anchor_conj;
+  /**
+   * Map from terms (selector chains) to their depth. The depth of a selector
+   * chain S1( ... Sn( x ) ... ) is:
+   *   weight( S1 ) + ... + weight( Sn ),
+   * where weight is the selector weight of Si
+   * (see SygusTermDatabase::getSelectorWeight).
+   */
   std::map< Node, unsigned > d_term_to_depth;
+  /**
+   * Map from terms (selector chains) to whether they are the topmost term
+   * of their type. For example, if:
+   *   S1 : T1 -> T2
+   *   S2 : T2 -> T2
+   *   S3 : T2 -> T1
+   *   S4 : T1 -> T3
+   * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms,
+   * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not.
+   *
+   */
   std::map< Node, bool > d_is_top_level;
   void registerTerm( Node n, std::vector< Node >& lemmas );
   bool computeTopLevel( TypeNode tn, Node n );
@@ -80,22 +107,24 @@ private:
     std::map< TypeNode, std::map< Node, unsigned > > d_search_val_sz;
     /** search value sample
      *
-     * This is used for the sygusRewVerify() option. For each sygus term we
-     * register in this cache, this stores the value returned by calling
-     * SygusSample::registerTerm(...) on its analog.
+     * This is used for the sygusRewVerify() option. For each sygus term t
+     * of type tn with anchor a that we register with this cache, we set:
+     *   d_search_val_sample[tn][r] = r'
+     * where r is the rewritten form of the builtin equivalent of t, and r'
+     * is the term returned by d_sampler[a][tn].registerTerm( r ).
      */
-    std::map<Node, Node> d_search_val_sample;
+    std::map<TypeNode, std::map<Node, Node>> d_search_val_sample;
     /** For each term, whether this cache has processed that term */
     std::map< Node, bool > d_search_val_proc;
   };
   // anchor -> cache
   std::map< Node, SearchCache > d_cache;
-  /** a sygus sampler object for each anchor
+  /** a sygus sampler object for each (anchor, sygus type) pair
    *
    * This is used for the sygusRewVerify() option to verify the correctness of
    * the rewriter.
    */
-  std::map<Node, quantifiers::SygusSampler> d_sampler;
+  std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> d_sampler;
   Node d_null;
   void assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas );
   // register search term

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index aa0a4b77882c6919ed4fdefcd7323ecb4d21bd3e..fa0478ac7395bf5780a66a324dc8be6b79dc0f21 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -100,6 +100,7 @@ void SygusSampler::initialize(TypeNode tn,
         << "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_type_ids[sv] = tnid;
   }
   initializeSamples(nsamples);
 }
@@ -176,6 +177,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples)
         << "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_type_ids[sv] = tnid;
   }
 
   initializeSamples(nsamples);
@@ -666,6 +668,8 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
   // one of eq_n or n must be ordered
   bool eqor = isOrdered(eq_n);
   bool nor = isOrdered(n);
+  Trace("sygus-synth-rr-debug")
+      << "Ordered? : " << nor << " " << eqor << std::endl;
   bool isUnique = false;
   if (eqor || nor)
   {