src/theory/quantifiers/quant_relevance.h

   1 /*********************                                                        */
   2 /*! \file quant_relevance.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
   6  ** This file is part of the CVC4 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.\endverbatim
  11  **
  12  ** \brief quantifier relevance
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANT_RELEVANCE_H
  18 #define CVC4__THEORY__QUANT_RELEVANCE_H
  19
  20 #include <map>
  21
  22 #include "theory/quantifiers/quant_util.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace quantifiers {
  27
  28 /** QuantRelevance
  29  *
  30 * This class is used for implementing SinE-style heuristics
  31 * (e.g. see Hoder et al. CADE 2011)
  32 * This is enabled by the option --relevant-triggers.
  33 */
  34 class QuantRelevance : public QuantifiersUtil
  35 {
  36  public:
  37   /** constructor
  38    * cr is whether relevance is computed by this class.
  39    * if this is false, then all calls to getRelevance
  40    * return -1.
  41    */
  42   QuantRelevance() {}
  43   ~QuantRelevance() {}
  44   /** reset */
  45   bool reset(Theory::Effort e) override { return true; }
  46   /** register quantifier */
  47   void registerQuantifier(Node q) override;
  48   /** identify */
  49   std::string identify() const override { return "QuantRelevance"; }
  50   /** get number of quantifiers for symbol s */
  51   size_t getNumQuantifiersForSymbol(Node s) const;
  52
  53  private:
  54   /** map from quantifiers to symbols they contain */
  55   std::map<Node, std::vector<Node> > d_syms;
  56   /** map from symbols to quantifiers */
  57   std::map<Node, std::vector<Node> > d_syms_quants;
  58   /** relevance for quantifiers and symbols */
  59   std::map<Node, int> d_relevance;
  60   /** compute symbols */
  61   void computeSymbols(Node n, std::vector<Node>& syms);
  62 };
  63
  64 } /* CVC4::theory::quantifiers namespace */
  65 } /* CVC4::theory namespace */
  66 } /* CVC4 namespace */
  67
  68 #endif /* CVC4__THEORY__QUANT_RELEVANCE_H */