src/theory/quantifiers/sygus/sygus_enumerator_callback.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Mathias Preiner
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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  * ****************************************************************************
  12  *
  13  * sygus_enumerator
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
  19 #define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
  20
  21 #include <unordered_set>
  22
  23 #include "expr/node.h"
  24 #include "theory/quantifiers/extended_rewrite.h"
  25
  26 namespace cvc5 {
  27 namespace theory {
  28 namespace quantifiers {
  29
  30 class ExampleEvalCache;
  31 class SygusStatistics;
  32 class SygusSampler;
  33
  34 /**
  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
  37  * considered.
  38  */
  39 class SygusEnumeratorCallback
  40 {
  41  public:
  42   SygusEnumeratorCallback(Node e, SygusStatistics* s = nullptr);
  43   virtual ~SygusEnumeratorCallback() {}
  44   /**
  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.
  48    *
  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.
  52    */
  53   virtual bool addTerm(Node n, std::unordered_set<Node>& bterms);
  54
  55  protected:
  56   /**
  57    * Callback-specific notification of the above
  58    *
  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
  62    */
  63   virtual void notifyTermInternal(Node n, Node bn, Node bnr) {}
  64   /**
  65    * Callback-specific add term
  66    *
  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.
  71    */
  72   virtual bool addTermInternal(Node n, Node bn, Node bnr) { return true; }
  73   /** The enumerator */
  74   Node d_enum;
  75   /** The type of enum */
  76   TypeNode d_tn;
  77   /** extended rewriter */
  78   ExtendedRewriter d_extr;
  79   /** pointer to the statistics */
  80   SygusStatistics* d_stats;
  81 };
  82
  83 class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
  84 {
  85  public:
  86   SygusEnumeratorCallbackDefault(Node e,
  87                                  SygusStatistics* s = nullptr,
  88                                  ExampleEvalCache* eec = nullptr,
  89                                  SygusSampler* ssrv = nullptr,
  90                                  std::ostream* out = nullptr);
  91   virtual ~SygusEnumeratorCallbackDefault() {}
  92
  93  protected:
  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;
  98   /**
  99    * Pointer to the example evaluation cache utility (used for symmetry
 100    * breaking).
 101    */
 102   ExampleEvalCache* d_eec;
 103   /** sampler (for --sygus-rr-verify) */
 104   SygusSampler* d_samplerRrV;
 105   /** The output stream to print unsound rewrites for above */
 106   std::ostream* d_out;
 107 };
 108
 109 }  // namespace quantifiers
 110 }  // namespace theory
 111 }  // namespace cvc5
 112
 113 #endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H */