Add sygus enumerator callback (#6923)

This class will make the uses of the fast enumerator customizable.

3 files changed, 219 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 796de9b4a..445d38896 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -879,6 +879,8 @@ libcvc5_add_sources(
   theory/quantifiers/sygus/sygus_enumerator.h
   theory/quantifiers/sygus/sygus_enumerator_basic.cpp
   theory/quantifiers/sygus/sygus_enumerator_basic.h
+  theory/quantifiers/sygus/sygus_enumerator_callback.cpp
+  theory/quantifiers/sygus/sygus_enumerator_callback.h
   theory/quantifiers/sygus/sygus_eval_unfold.cpp
   theory/quantifiers/sygus/sygus_eval_unfold.h
   theory/quantifiers/sygus/sygus_explain.cpp
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
new file mode 100644
index 000000000..7b3236832
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
@@ -0,0 +1,107 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * sygus_enumerator
+ */
+
+#include "theory/quantifiers/sygus/sygus_enumerator_callback.h"
+
+#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/sygus/example_eval_cache.h"
+#include "theory/quantifiers/sygus/sygus_stats.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+SygusEnumeratorCallback::SygusEnumeratorCallback(Node e, SygusStatistics* s)
+    : d_enum(e), d_stats(s)
+{
+  d_tn = e.getType();
+}
+
+bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
+{
+  Node bn = datatypes::utils::sygusToBuiltin(n);
+  Node bnr = d_extr.extendedRewrite(bn);
+  if (d_stats != nullptr)
+  {
+    ++(d_stats->d_enumTermsRewrite);
+  }
+  // call the solver-specific notify term
+  notifyTermInternal(n, bn, bnr);
+  // check whether we should keep the term, which is based on the callback,
+  // and the builtin terms
+  // First, must be unique up to rewriting
+  if (bterms.find(bnr) != bterms.end())
+  {
+    Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+    return false;
+  }
+  // insert to builtin term cache, regardless of whether it is redundant
+  // based on the callback
+  bterms.insert(bnr);
+  // callback-specific add term
+  if (!addTermInternal(n, bn, bnr))
+  {
+    Trace("sygus-enum-exc")
+        << "Exclude: " << bn << " due to callback" << std::endl;
+    return false;
+  }
+  Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
+  return true;
+}
+
+SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault(
+    Node e, SygusStatistics* s, ExampleEvalCache* eec, SygusSampler* ssrv)
+    : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv)
+{
+}
+void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n,
+                                                        Node bn,
+                                                        Node bnr)
+{
+  if (d_samplerRrV != nullptr)
+  {
+    d_samplerRrV->checkEquivalent(bn, bnr);
+  }
+}
+
+bool SygusEnumeratorCallbackDefault::addTermInternal(Node n, Node bn, Node bnr)
+{
+  // if we are doing PBE symmetry breaking
+  if (d_eec != nullptr)
+  {
+    if (d_stats != nullptr)
+    {
+      ++(d_stats->d_enumTermsExampleEval);
+    }
+    // Is it equivalent under examples?
+    Node bne = d_eec->addSearchVal(d_tn, bnr);
+    if (!bne.isNull())
+    {
+      if (bnr != bne)
+      {
+        Trace("sygus-enum-exc")
+            << "Exclude (by examples): " << bn << ", since we already have "
+            << bne << std::endl;
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
new file mode 100644
index 000000000..545440eef
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
@@ -0,0 +1,110 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * sygus_enumerator
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
+
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "theory/quantifiers/extended_rewrite.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class ExampleEvalCache;
+class SygusStatistics;
+class SygusSampler;
+
+/**
+ * Base class for callbacks in the fast enumerator. This allows a user to
+ * provide custom criteria for whether or not enumerated values should be
+ * considered.
+ */
+class SygusEnumeratorCallback
+{
+ public:
+  SygusEnumeratorCallback(Node e, SygusStatistics* s = nullptr);
+  virtual ~SygusEnumeratorCallback() {}
+  /**
+   * Add term, return true if the term should be considered in the enumeration.
+   * Notice that returning false indicates that n should not be considered as a
+   * subterm of any other term in the enumeration.
+   *
+   * @param n The SyGuS term
+   * @param bterms The (rewritten, builtin) terms we have already enumerated
+   * @return true if n should be considered in the enumeration.
+   */
+  virtual bool addTerm(Node n, std::unordered_set<Node>& bterms) = 0;
+
+ protected:
+  /**
+   * Callback-specific notification of the above
+   *
+   * @param n The SyGuS term
+   * @param bn The builtin version of the enumerated term
+   * @param bnr The (extended) rewritten form of bn
+   */
+  virtual void notifyTermInternal(Node n, Node bn, Node bnr) = 0;
+  /**
+   * Callback-specific add term
+   *
+   * @param n The SyGuS term
+   * @param bn The builtin version of the enumerated term
+   * @param bnr The (extended) rewritten form of bn
+   * @return true if the term should be considered in the enumeration.
+   */
+  virtual bool addTermInternal(Node n, Node bn, Node bnr) = 0;
+  /** The enumerator */
+  Node d_enum;
+  /** The type of enum */
+  TypeNode d_tn;
+  /** extended rewriter */
+  ExtendedRewriter d_extr;
+  /** pointer to the statistics */
+  SygusStatistics* d_stats;
+};
+
+class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
+{
+ public:
+  SygusEnumeratorCallbackDefault(Node e,
+                                 SygusStatistics* s = nullptr,
+                                 ExampleEvalCache* eec = nullptr,
+                                 SygusSampler* ssrv = nullptr);
+  virtual ~SygusEnumeratorCallbackDefault() {}
+
+ protected:
+  /** Notify that bn / bnr is an enumerated builtin, rewritten form of a term */
+  void notifyTermInternal(Node n, Node bn, Node bnr) override;
+  /** Add term, return true if n should be considered in the enumeration */
+  bool addTermInternal(Node n, Node bn, Node bnr) override;
+  /**
+   * Pointer to the example evaluation cache utility (used for symmetry
+   * breaking).
+   */
+  ExampleEvalCache* d_eec;
+  /** sampler (for --sygus-rr-verify) */
+  SygusSampler* d_samplerRrV;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H */