Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Trigger database class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/ematching/trigger_database.h"
14 : :
15 : : #include "theory/quantifiers/ematching/ho_trigger.h"
16 : : #include "theory/quantifiers/ematching/trigger.h"
17 : : #include "theory/quantifiers/term_util.h"
18 : :
19 : : namespace cvc5::internal {
20 : : namespace theory {
21 : : namespace quantifiers {
22 : : namespace inst {
23 : :
24 : 43762 : TriggerDatabase::TriggerDatabase(Env& env,
25 : : QuantifiersState& qs,
26 : : QuantifiersInferenceManager& qim,
27 : : QuantifiersRegistry& qr,
28 : 43762 : TermRegistry& tr)
29 : 43762 : : EnvObj(env), d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
30 : : {
31 : 43762 : }
32 : 43427 : TriggerDatabase::~TriggerDatabase() {}
33 : :
34 : 39955 : Trigger* TriggerDatabase::mkTrigger(Node q,
35 : : const std::vector<Node>& nodes,
36 : : bool keepAll,
37 : : int trOption,
38 : : size_t useNVars,
39 : : bool isUser)
40 : : {
41 : 39955 : std::vector<Node> trNodes;
42 [ + + ]: 39955 : if (!keepAll)
43 : : {
44 [ - + ][ - + ]: 33232 : size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars;
[ - - ]
45 [ + + ]: 33232 : if (!mkTriggerTerms(q, nodes, nvars, trNodes))
46 : : {
47 : 2453 : return nullptr;
48 : : }
49 : : }
50 : : else
51 : : {
52 : 6723 : trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end());
53 : : }
54 : :
55 : : // check for duplicate?
56 [ + + ]: 37502 : if (trOption != TR_MAKE_NEW)
57 : : {
58 : 30779 : Trigger* t = d_trie.getTrigger(trNodes);
59 [ + + ]: 30779 : if (t)
60 : : {
61 [ + - ]: 293 : if (trOption == TR_GET_OLD)
62 : : {
63 : : // just return old trigger
64 : 293 : return t;
65 : : }
66 : 0 : return nullptr;
67 : : }
68 : : }
69 : :
70 : : // check if higher-order
71 [ + - ]: 74418 : Trace("trigger-debug") << "Collect higher-order variable triggers..."
72 : 37209 : << std::endl;
73 : 37209 : std::map<Node, std::vector<Node> > hoApps;
74 : 37209 : HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps);
75 [ + - ]: 74418 : Trace("trigger-debug") << "...got " << hoApps.size()
76 : 37209 : << " higher-order applications." << std::endl;
77 : : Trigger* t;
78 [ + + ]: 37209 : if (!hoApps.empty())
79 : : {
80 : 584 : t = new HigherOrderTrigger(
81 : 292 : d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps, isUser);
82 : : }
83 : : else
84 : : {
85 : 36917 : t = new Trigger(d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes, isUser);
86 : : }
87 : 37209 : d_trie.addTrigger(trNodes, t);
88 : 37209 : return t;
89 : 39955 : }
90 : :
91 : 28212 : Trigger* TriggerDatabase::mkTrigger(
92 : : Node q, Node n, bool keepAll, int trOption, size_t useNVars, bool isUser)
93 : : {
94 : 28212 : std::vector<Node> nodes;
95 : 28212 : nodes.push_back(n);
96 : 56424 : return mkTrigger(q, nodes, keepAll, trOption, useNVars, isUser);
97 : 28212 : }
98 : :
99 : 33232 : bool TriggerDatabase::mkTriggerTerms(Node q,
100 : : const std::vector<Node>& nodes,
101 : : size_t nvars,
102 : : std::vector<Node>& trNodes)
103 : : {
104 : : // only take nodes that contribute variables to the trigger when added
105 : 33232 : std::map<Node, bool> vars;
106 : 33232 : std::map<Node, std::vector<Node> > patterns;
107 : 33232 : size_t varCount = 0;
108 : 33232 : std::map<Node, std::vector<Node> > varContains;
109 [ + + ]: 100421 : for (const Node& pat : nodes)
110 : : {
111 : 67189 : TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
112 : : }
113 [ + + ]: 66629 : for (const Node& t : nodes)
114 : : {
115 : 64176 : const std::vector<Node>& vct = varContains[t];
116 : 64176 : bool foundVar = false;
117 [ + + ]: 356731 : for (const Node& v : vct)
118 : : {
119 [ - + ][ - + ]: 292555 : Assert(TermUtil::getInstConstAttr(v) == q);
[ - - ]
120 [ + + ]: 292555 : if (vars.find(v) == vars.end())
121 : : {
122 : 101300 : varCount++;
123 : 101300 : vars[v] = true;
124 : 101300 : foundVar = true;
125 : : }
126 : : }
127 [ + + ]: 64176 : if (foundVar)
128 : : {
129 : 42379 : trNodes.push_back(t);
130 [ + + ]: 183110 : for (const Node& v : vct)
131 : : {
132 : 140731 : patterns[v].push_back(t);
133 : : }
134 : : }
135 [ + + ]: 64176 : if (varCount == nvars)
136 : : {
137 : 30779 : break;
138 : : }
139 : : }
140 [ + + ]: 33232 : if (varCount < nvars)
141 : : {
142 [ + - ]: 4906 : Trace("trigger-debug") << "Don't consider trigger since it does not "
143 : 0 : "contain specified number of variables."
144 : 2453 : << std::endl;
145 [ + - ]: 2453 : Trace("trigger-debug") << nodes << std::endl;
146 : : // do not generate multi-trigger if it does not contain all variables
147 : 2453 : return false;
148 : : }
149 : : // now, minimize the trigger
150 [ + + ]: 66809 : for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
151 : : {
152 : 36030 : bool keepPattern = false;
153 : 36030 : Node n = trNodes[i];
154 : 36030 : const std::vector<Node>& vcn = varContains[n];
155 [ + + ]: 39419 : for (const Node& v : vcn)
156 : : {
157 [ + + ]: 37351 : if (patterns[v].size() == 1)
158 : : {
159 : 33962 : keepPattern = true;
160 : 33962 : break;
161 : : }
162 : : }
163 [ + + ]: 36030 : if (!keepPattern)
164 : : {
165 : : // remove from pattern vector
166 [ + + ]: 4756 : for (const Node& v : vcn)
167 : : {
168 : 2688 : std::vector<Node>& pv = patterns[v];
169 [ + - ]: 2789 : for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
170 : : {
171 [ + + ]: 2789 : if (pv[k] == n)
172 : : {
173 : 2688 : pv.erase(pv.begin() + k, pv.begin() + k + 1);
174 : 2688 : break;
175 : : }
176 : : }
177 : : }
178 : : // remove from trigger nodes
179 : 2068 : trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
180 : 2068 : i--;
181 : 2068 : tsize--;
182 : : }
183 : 36030 : }
184 : 30779 : return true;
185 : 33232 : }
186 : :
187 : : } // namespace inst
188 : : } // namespace quantifiers
189 : : } // namespace theory
190 : : } // namespace cvc5::internal
|
