Add a random Sygus enumerator. (#7782)

This PR adds a Sygus enumerator that generates random terms from a grammar. The size of the terms generated by the enumerator approximates a geometric distribution and can be configured with an option.

9 files changed, 395 insertions, 2 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1d57dfeb4..fde0088e8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -912,10 +912,12 @@ libcvc5_add_sources(
   theory/quantifiers/sygus/sygus_pbe.h
   theory/quantifiers/sygus/sygus_process_conj.cpp
   theory/quantifiers/sygus/sygus_process_conj.h
-  theory/quantifiers/sygus/sygus_reconstruct.cpp
-  theory/quantifiers/sygus/sygus_reconstruct.h
   theory/quantifiers/sygus/sygus_qe_preproc.cpp
   theory/quantifiers/sygus/sygus_qe_preproc.h
+  theory/quantifiers/sygus/sygus_random_enumerator.cpp
+  theory/quantifiers/sygus/sygus_random_enumerator.h
+  theory/quantifiers/sygus/sygus_reconstruct.cpp
+  theory/quantifiers/sygus/sygus_reconstruct.h
   theory/quantifiers/sygus/sygus_repair_const.cpp
   theory/quantifiers/sygus/sygus_repair_const.h
   theory/quantifiers/sygus/sygus_stats.cpp
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 80692055f..4021ac2aa 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1092,6 +1092,9 @@ name   = "Quantifiers"
 [[option.mode.ENUM]]
   name = "enum"
   help = "Use optimized enumerator for actively-generated sygus enumerators."
+[[option.mode.RANDOM]]
+  name = "random"
+  help = "Use basic random enumerator for actively-generated sygus enumerators."
 [[option.mode.VAR_AGNOSTIC]]
   name = "var-agnostic"
   help = "Use sygus solver to enumerate terms that are agnostic to variables."
@@ -1100,6 +1103,16 @@ name   = "Quantifiers"
   help = "Internally decide the best policy for each enumerator."
 
 [[option]]
+  name       = "sygusActiveGenRandomP"
+  category   = "regular"
+  long       = "sygus-active-gen-random-p=P"
+  type       = "double"
+  default    = "0.5"
+  minimum    = "0.0"
+  maximum    = "1.0"
+  help       = "the parameter of the geometric distribution used to determine the size of terms generated by --sygus-active-gen=random"
+
+[[option]]
   name       = "sygusActiveGenEnumConsts"
   category   = "regular"
   long       = "sygus-active-gen-cfactor=N"
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index f91127dbe..7fbe1c3cd 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
+#include "theory/quantifiers/sygus/sygus_random_enumerator.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_registry.h"
 
@@ -94,6 +95,11 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
       {
         d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType()));
       }
+      else if (options().quantifiers.sygusActiveGenMode
+               == options::SygusActiveGenMode::RANDOM)
+      {
+        d_evg.reset(new SygusRandomEnumerator(d_tds));
+      }
       else
       {
         Assert(options().quantifiers.sygusActiveGenMode
diff --git a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp
new file mode 100644
index 000000000..bf051a897
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp
@@ -0,0 +1,199 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of sygus random enumerator.
+ */
+
+#include "theory/quantifiers/sygus/sygus_random_enumerator.h"
+
+#include "expr/dtype_cons.h"
+#include "expr/skolem_manager.h"
+#include "options/quantifiers_options.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
+#include "util/random.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+void SygusRandomEnumerator::initialize(Node e)
+{
+  d_tn = e.getType();
+  Assert(d_tn.isDatatype());
+  Assert(d_tn.getDType().isSygus());
+  SygusTypeInfo sti;
+  sti.initialize(d_tds, d_tn);
+  std::vector<TypeNode> stns;
+  sti.getSubfieldTypes(stns);
+  // We will be using the datatype constructors a lot, so we cache them here.
+  for (const TypeNode& stn : stns)
+  {
+    for (const std::shared_ptr<DTypeConstructor>& cons :
+         stn.getDType().getConstructors())
+    {
+      if (cons->getNumArgs() == 0)
+      {
+        d_noArgCons[stn].push_back(cons);
+      }
+      else
+      {
+        d_argCons[stn].push_back(cons);
+      }
+    }
+  }
+}
+
+bool SygusRandomEnumerator::increment()
+{
+  Node n, bn;
+  do
+  {
+    // Generate the next sygus term.
+    n = incrementH();
+    bn = d_tds->sygusToBuiltin(n);
+    bn = Rewriter::callExtendedRewrite(bn);
+    // Ensure that the builtin counterpart is unique (up to rewriting).
+  } while (d_cache.find(bn) != d_cache.cend());
+  d_cache.insert(bn);
+  d_currTerm = n;
+  return true;
+}
+
+Node SygusRandomEnumerator::incrementH()
+{
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Random& rnd = Random::getRandom();
+  double p = options::sygusActiveGenRandomP();
+
+  Node mainSkolem = sm->mkDummySkolem("sygus_rand", d_tn);
+  // List of skolems with no corresponding constructor.
+  std::vector<Node> remainingSkolems;
+  remainingSkolems.push_back(mainSkolem);
+  // List of terms with corresponding constructors. We do not immediately
+  // construct sygus terms (possibly containing holes) for those skolems.
+  // Instead, we wait until we are done picking constructors for all skolems. We
+  // do so to immediately construct ground terms for all of them following their
+  // order in this stack.
+  std::vector<Node> stack;
+  // Constructors corresponding to each skolem.
+  std::unordered_map<Node, std::shared_ptr<DTypeConstructor>> skolemCons;
+  // Ground terms corresponding to each skolem.
+  std::unordered_map<Node, Node> groundTerm;
+  // Sub-skolems needed for skolems with constructors that take arguments.
+  std::unordered_map<Node, std::vector<Node>> subSkolems;
+
+  // We stop when we get a tails or there are no more skolems to process.
+  while (rnd.pickWithProb(p) && !remainingSkolems.empty())
+  {
+    // Pick a random skolem from the remaining ones and remove it from the list.
+    size_t r = rnd() % remainingSkolems.size();
+    Node currSkolem = remainingSkolems[r];
+    remainingSkolems.erase(remainingSkolems.cbegin() + r);
+    // Add the picked skolem to stack for later processing.
+    TypeNode currSkolemType = currSkolem.getType();
+    // If the type current skolem is not a subfield type of `d_tn`, we replace
+    // it with a ground value of its type.
+    if (d_argCons[currSkolemType].empty()
+        && d_noArgCons[currSkolemType].empty())
+    {
+      groundTerm[currSkolem] = nm->mkGroundValue(currSkolemType);
+      continue;
+    }
+    stack.push_back(currSkolem);
+    // Pick a random constructor that takes arguments for this skolem. If there
+    // is none, pick a random no-argument constructor.
+    skolemCons[currSkolem] =
+        d_argCons[currSkolemType].empty()
+            ? d_noArgCons[currSkolemType]
+                         [rnd() % d_noArgCons[currSkolemType].size()]
+            : d_argCons[currSkolemType]
+                       [rnd() % d_argCons[currSkolemType].size()];
+    // Create a sub-skolem for each constructor argument and add them to the
+    // list of remaining skolems.
+    for (size_t i = 0, n = skolemCons[currSkolem]->getNumArgs(); i < n; ++i)
+    {
+      TypeNode subSkolemType = skolemCons[currSkolem]->getArgType(i);
+      Node subSkolem = sm->mkDummySkolem("sygus_rand", subSkolemType);
+      remainingSkolems.push_back(subSkolem);
+      subSkolems[currSkolem].push_back(subSkolem);
+    }
+  }
+
+  // If we get a tail, we need to pick no-argument constructors for the
+  // remaining skolems. If all constructors take arguments, we use the ground
+  // value for the skolems' sygus datatype type.
+  for (Node skolem : remainingSkolems)
+  {
+    TypeNode skolemType = skolem.getType();
+    if (d_noArgCons[skolemType].empty())
+    {
+      groundTerm[skolem] = nm->mkGroundValue(skolemType);
+    }
+    else
+    {
+      skolemCons[skolem] =
+          d_noArgCons[skolemType][rnd() % d_noArgCons[skolemType].size()];
+      stack.push_back(skolem);
+    }
+  }
+
+  // Build up ground values starting from leaf skolems up to the root/main
+  // skolem.
+  while (!stack.empty())
+  {
+    Node currSkolem = stack.back();
+    stack.pop_back();
+    std::vector<Node> args;
+    args.push_back(skolemCons[currSkolem]->getConstructor());
+    for (Node subSkolem : subSkolems[currSkolem])
+    {
+      args.push_back(groundTerm[subSkolem]);
+    }
+    // We may have already generated a sygus term equivalent to the one we are
+    // generating now. In that case, pick the smaller term of the two. This
+    // operation allows us to generate more refined terms over time.
+    groundTerm[currSkolem] = getMin(nm->mkNode(kind::APPLY_CONSTRUCTOR, args));
+  }
+
+  return groundTerm[mainSkolem];
+}
+
+Node SygusRandomEnumerator::getMin(Node n)
+{
+  TypeNode tn = n.getType();
+  Node bn = d_tds->sygusToBuiltin(n);
+  bn = Rewriter::callExtendedRewrite(bn);
+  // Did we calculate the size of `n` before?
+  if (d_size.find(n) == d_size.cend())
+  {
+    // If not, calculate its size and cache it.
+    d_size[n] = datatypes::utils::getSygusTermSize(n);
+  }
+  // Did we come across an equivalent term before? If so, is the equivalent term
+  // smaller than `n`?
+  if (d_minSygus[tn][bn].isNull() || d_size[n] < d_size[d_minSygus[tn][bn]])
+  {
+    d_minSygus[tn][bn] = n;
+  }
+  else
+  {
+    n = d_minSygus[tn][bn];
+  }
+  return n;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_random_enumerator.h b/src/theory/quantifiers/sygus/sygus_random_enumerator.h
new file mode 100644
index 000000000..b70fe9490
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_random_enumerator.h
@@ -0,0 +1,129 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Random sygus enumerator class.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RANDOM_ENUMERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_RANDOM_ENUMERATOR_H
+
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
+
+namespace cvc5 {
+
+class DTypeConstructor;
+
+namespace theory {
+namespace quantifiers {
+
+class TermDbSygus;
+
+using TypeConsMap =
+    std::unordered_map<TypeNode,
+                       std::vector<std::shared_ptr<DTypeConstructor>>>;
+
+/** A random sygus value generator.
+ *
+ * This class is a random term generator for sygus conjectures. The sizes of the
+ * generated terms approximate a geometric distribution with an expected size of
+ * 1 / p, where p is a parameter specified by the user (defaults to 0.5).
+ */
+class SygusRandomEnumerator : public EnumValGenerator
+{
+ public:
+  /** Constructor. Initializes the enumerator.
+   *
+   * @param tds pointer to term database sygus.
+   */
+  SygusRandomEnumerator(TermDbSygus* tds) : d_tds(tds){};
+
+  /** Initialize this class with enumerator `e`. */
+  void initialize(Node e) override;
+
+  /** Inform this generator that abstract value `v` was enumerated. */
+  void addValue(Node v) override { d_cache.insert(v); }
+
+  /**
+   * Get next the next random (T-rewriter-unique) value.
+   *
+   * @return true if a new value is found and loop otherwise.
+   */
+  bool increment() override;
+
+  /** @return the current term. */
+  Node getCurrent() override { return d_currTerm; }
+
+ private:
+  /** Generates a random sygus term.
+   *
+   * S ::= 0 | x | (+ S S)
+   *
+   * Assuming we are provided the above grammar, we generate random terms by
+   * starting with a skolem, `z0`, of the given sygus datatype type (grammar
+   * non-terminal). We then flip a coin to determine whether or not we should
+   * replace the skolem with a random constructor that takes arguments (`(+ S
+   * S)` above). For example, if the first 2 coin flips are heads, then we will
+   * replace `z0` with `(+ z1 z2)` and either `z1` or `z2` (randomly chosen)
+   * with `(+ z3 z4)`. So, we will end up with either `(+ (+ z3 z4) z2)` or `(+
+   * z1 (+ z3 z4))`. We keep doing so until we get a tails. At which point, we
+   * replace all remaining skolems with random no-argument constructors (`0` and
+   * `x` above) and return the resulting sygus term. So, if we get a tails at
+   * the third flip in the previous example, then `incrementH` may return `(+ 1
+   * (+ x x))`, `(+ (+ 1 1) 1)`, or any of the other 14 possible terms.
+   *
+   * \note If a skolem's datatype type does not have a no-argument constructor,
+   * it is replaced with a ground value using `mkGroundValue` utility.
+   * \note If a skolem's datatype type does not have a constructor that takes an
+   * argument (e.g., `S ::= 0 | 1 | x | (+ 2 y)`), it is replaced with a random
+   * no-argument constructor. So `incrementH` may return a term before getting a
+   * tails.
+   *
+   * @return a randomly generated sygus term.
+   */
+  Node incrementH();
+
+  /**
+   * Returns smallest (in terms of size) term equivalent (up to rewriting) to
+   * the given sygus term.
+   */
+  Node getMin(Node n);
+
+  /** Pointer to term database sygus. */
+  TermDbSygus* d_tds;
+  /** The type to enumerate. */
+  TypeNode d_tn;
+  /** The current term. */
+  Node d_currTerm;
+  /** Cache of no-argument constructors for each sygus datatype type. */
+  TypeConsMap d_noArgCons;
+  /** Cache of argument constructors for each sygus datatype type. */
+  TypeConsMap d_argCons;
+  /** Cache of builtin terms we have enumerated so far. */
+  std::unordered_set<Node> d_cache;
+  /** Cache of smallest (in terms of size) term equivalent (up to rewriting)
+   * to the given sygus term, per sygus datatatype type. */
+  std::unordered_map<TypeNode, std::unordered_map<Node, Node>> d_minSygus;
+  /** Cache of the size of a sygus term. */
+  std::unordered_map<Node, unsigned> d_size;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif  // CVC5__THEORY__QUANTIFIERS__SYGUS_RANDOM_ENUMERATOR_H
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 20722a1da..ffff25520 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2531,6 +2531,9 @@ set(regress_1_tests
   regress1/sygus/pLTL_5_trace.sy
   regress1/sygus/qe.sy
   regress1/sygus/qf_abv.smt2
+  regress1/sygus/rand_const.sy
+  regress1/sygus/rand_p_0.sy
+  regress1/sygus/rand_p_1.sy
   regress1/sygus/real-any-const.sy
   regress1/sygus/real-grammar.sy
   regress1/sygus/rec-fun-swap.sy
diff --git a/test/regress/regress1/sygus/rand_const.sy b/test/regress/regress1/sygus/rand_const.sy
new file mode 100644
index 000000000..e920a9cc0
--- /dev/null
+++ b/test/regress/regress1/sygus/rand_const.sy
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status
+; EXPECT: unsat
+
+(set-logic BV)
+
+; Ensures random enumerator correctly handles non-sygus types.
+
+(synth-fun f () (_ BitVec 7)
+  ((Start (_ BitVec 7)))
+  ((Start (_ BitVec 7) ((Constant (_ BitVec 7))))))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/rand_p_0.sy b/test/regress/regress1/sygus/rand_p_0.sy
new file mode 100644
index 000000000..a7b3c9f41
--- /dev/null
+++ b/test/regress/regress1/sygus/rand_p_0.sy
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status
+; EXPECT: unsat
+
+(set-logic BV)
+(set-option :sygus-active-gen-random-p 0)
+
+; Ensures random enumerator correctly handles cases where the coin flips to
+; tails but there is no no-argument constructor to pick.
+
+(synth-fun f () Bool
+  ((Start Bool) (Const Bool))
+  ((Start Bool ((not Const)))
+   (Const Bool (false))))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/rand_p_1.sy b/test/regress/regress1/sygus/rand_p_1.sy
new file mode 100644
index 000000000..412e55f73
--- /dev/null
+++ b/test/regress/regress1/sygus/rand_p_1.sy
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status
+; EXPECT: unsat
+
+(set-logic BV)
+(set-option :sygus-active-gen-random-p 1)
+
+; Ensures random enumerator correctly handles cases where the coin flips to
+; heads but there is no constructor that takes arguments to pick.
+
+(synth-fun f () Bool
+  ((Start Bool))
+  ((Start Bool (false))))
+
+(check-synth)