1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
/********************* */
/*! \file trigger_database.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief trigger trie class
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
#define CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
#include <vector>
#include "expr/node.h"
#include "theory/quantifiers/ematching/trigger_trie.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
class QuantifiersInferenceManager;
class QuantifiersState;
class QuantifiersRegistry;
class TermRegistry;
namespace inst {
/**
* A database of triggers, which manages how triggers are constructed.
*/
class TriggerDatabase
{
public:
TriggerDatabase(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr);
~TriggerDatabase();
/** mkTrigger method
*
* This makes an instance of a trigger object.
* qe : pointer to the quantifier engine;
* q : the quantified formula we are making a trigger for
* nodes : the nodes comprising the (multi-)trigger
* keepAll: don't remove unneeded patterns;
* trOption : policy for dealing with triggers that already exist
* (see below)
* useNVars : number of variables that should be bound by the trigger
* typically, the number of quantified variables in q.
*/
enum
{
TR_MAKE_NEW, // make new trigger even if it already may exist
TR_GET_OLD, // return a previous trigger if it had already been created
TR_RETURN_NULL // return null if a duplicate is found
};
Trigger* mkTrigger(Node q,
const std::vector<Node>& nodes,
bool keepAll = true,
int trOption = TR_MAKE_NEW,
size_t useNVars = 0);
/** single trigger version that calls the above function */
Trigger* mkTrigger(Node q,
Node n,
bool keepAll = true,
int trOption = TR_MAKE_NEW,
size_t useNVars = 0);
/** make trigger terms
*
* This takes a set of eligible trigger terms and stores a subset of them in
* trNodes, such that :
* (1) the terms in trNodes contain at least n_vars of the quantified
* variables in quantified formula q, and
* (2) the set trNodes is minimal, i.e. removing one term from trNodes
* always violates (1).
*/
static bool mkTriggerTerms(Node q,
const std::vector<Node>& nodes,
size_t nvars,
std::vector<Node>& trNodes);
private:
/** The trigger trie, containing the triggers */
TriggerTrie d_trie;
/** Reference to the quantifiers state */
QuantifiersState& d_qs;
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
/** The quantifiers registry */
QuantifiersRegistry& d_qreg;
/** Reference to the term registry */
TermRegistry& d_treg;
};
} // namespace inst
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
|
