GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_relevance.h Lines: 2 4 50.0 %
Date: 2021-03-22 Branches: 0 2 0.0 %

Line Exec Source
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
4
  QuantRelevance() {}
43
8
  ~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 */