From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 14 Dec 2021 22:03:36 +0000 (-0600) Subject: Add a random Sygus enumerator. (#7782) X-Git-Tag: cvc5-1.0.0~664 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bbbe2f3ebbd7175930054cca12c3e5e32cd0cbd9;p=cvc5.git 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. --- 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." @@ -1099,6 +1102,16 @@ name = "Quantifiers" 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" 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 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& 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 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 stack; + // Constructors corresponding to each skolem. + std::unordered_map> skolemCons; + // Ground terms corresponding to each skolem. + std::unordered_map groundTerm; + // Sub-skolems needed for skolems with constructors that take arguments. + std::unordered_map> 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 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 + +#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>>; + +/** 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 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> d_minSygus; + /** Cache of the size of a sygus term. */ + std::unordered_map 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)