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.
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
[[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."
name = "auto"
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"
#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"
{
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
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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
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
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff