1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Mathias Preiner
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
19 #define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
21 #include <unordered_set>
23 #include "expr/node.h"
24 #include "theory/quantifiers/extended_rewrite.h"
28 namespace quantifiers
{
30 class ExampleEvalCache
;
31 class SygusStatistics
;
35 * Base class for callbacks in the fast enumerator. This allows a user to
36 * provide custom criteria for whether or not enumerated values should be
39 class SygusEnumeratorCallback
42 SygusEnumeratorCallback(Node e
, SygusStatistics
* s
= nullptr);
43 virtual ~SygusEnumeratorCallback() {}
45 * Add term, return true if the term should be considered in the enumeration.
46 * Notice that returning false indicates that n should not be considered as a
47 * subterm of any other term in the enumeration.
49 * @param n The SyGuS term
50 * @param bterms The (rewritten, builtin) terms we have already enumerated
51 * @return true if n should be considered in the enumeration.
53 virtual bool addTerm(Node n
, std::unordered_set
<Node
>& bterms
);
57 * Callback-specific notification of the above
59 * @param n The SyGuS term
60 * @param bn The builtin version of the enumerated term
61 * @param bnr The (extended) rewritten form of bn
63 virtual void notifyTermInternal(Node n
, Node bn
, Node bnr
) {}
65 * Callback-specific add term
67 * @param n The SyGuS term
68 * @param bn The builtin version of the enumerated term
69 * @param bnr The (extended) rewritten form of bn
70 * @return true if the term should be considered in the enumeration.
72 virtual bool addTermInternal(Node n
, Node bn
, Node bnr
) { return true; }
75 /** The type of enum */
77 /** extended rewriter */
78 ExtendedRewriter d_extr
;
79 /** pointer to the statistics */
80 SygusStatistics
* d_stats
;
83 class SygusEnumeratorCallbackDefault
: public SygusEnumeratorCallback
86 SygusEnumeratorCallbackDefault(Node e
,
87 SygusStatistics
* s
= nullptr,
88 ExampleEvalCache
* eec
= nullptr,
89 SygusSampler
* ssrv
= nullptr,
90 std::ostream
* out
= nullptr);
91 virtual ~SygusEnumeratorCallbackDefault() {}
94 /** Notify that bn / bnr is an enumerated builtin, rewritten form of a term */
95 void notifyTermInternal(Node n
, Node bn
, Node bnr
) override
;
96 /** Add term, return true if n should be considered in the enumeration */
97 bool addTermInternal(Node n
, Node bn
, Node bnr
) override
;
99 * Pointer to the example evaluation cache utility (used for symmetry
102 ExampleEvalCache
* d_eec
;
103 /** sampler (for --sygus-rr-verify) */
104 SygusSampler
* d_samplerRrV
;
105 /** The output stream to print unsound rewrites for above */
109 } // namespace quantifiers
110 } // namespace theory
113 #endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H */