This class will make the uses of the fast enumerator customizable.
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
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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 */
projects / cvc5.git / commitdiff