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