From: Andrew Reynolds Date: Tue, 27 Jul 2021 00:20:40 +0000 (-0500) Subject: Add sygus enumerator callback (#6923) X-Git-Tag: cvc5-1.0.0~1452 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4640dd5d09d65761ab96ea7f6848d823a3a43278;p=cvc5.git Add sygus enumerator callback (#6923) This class will make the uses of the fast enumerator customizable. --- 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& 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 + +#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& 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 */