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 : : * Implementation of trigger class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/ematching/trigger.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "options/base_options.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "smt/env.h"
19 : : #include "theory/quantifiers/ematching/candidate_generator.h"
20 : : #include "theory/quantifiers/ematching/inst_match_generator.h"
21 : : #include "theory/quantifiers/ematching/inst_match_generator_multi.h"
22 : : #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
23 : : #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
24 : : #include "theory/quantifiers/ematching/pattern_term_selector.h"
25 : : #include "theory/quantifiers/ematching/trigger_trie.h"
26 : : #include "theory/quantifiers/inst_match.h"
27 : : #include "theory/quantifiers/instantiate.h"
28 : : #include "theory/quantifiers/quantifiers_attributes.h"
29 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
30 : : #include "theory/quantifiers/quantifiers_registry.h"
31 : : #include "theory/quantifiers/quantifiers_state.h"
32 : : #include "theory/quantifiers/term_util.h"
33 : : #include "theory/valuation.h"
34 : :
35 : : using namespace cvc5::internal::kind;
36 : :
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : : namespace quantifiers {
40 : : namespace inst {
41 : :
42 : : /** trigger class constructor */
43 : 37370 : Trigger::Trigger(Env& env,
44 : : QuantifiersState& qs,
45 : : QuantifiersInferenceManager& qim,
46 : : QuantifiersRegistry& qr,
47 : : TermRegistry& tr,
48 : : Node q,
49 : : std::vector<Node>& nodes,
50 : 37370 : bool isUser)
51 : : : EnvObj(env),
52 : 37370 : d_qstate(qs),
53 : 37370 : d_qim(qim),
54 : 37370 : d_qreg(qr),
55 : 37370 : d_treg(tr),
56 : 37370 : d_quant(q),
57 : 74740 : d_instMatch(env, qs, tr, q)
58 : : {
59 : : // set evaluator mode to "no entail"
60 : 37370 : d_instMatch.setEvaluatorMode(ieval::TermEvaluatorMode::NO_ENTAIL);
61 : : // We must ensure that the ground subterms of the trigger have been
62 : : // preprocessed.
63 : 37370 : Valuation& val = d_qstate.getValuation();
64 [ + + ]: 78113 : for (const Node& n : nodes)
65 : : {
66 : 40743 : Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms);
67 : 40743 : d_nodes.push_back(np);
68 : 40743 : }
69 [ - + ]: 37370 : if (TraceIsOn("trigger"))
70 : : {
71 : 0 : QuantAttributes& qa = d_qreg.getQuantAttributes();
72 : 0 : Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": "
73 : 0 : << std::endl;
74 [ - - ]: 0 : for (const Node& n : d_nodes)
75 : : {
76 [ - - ]: 0 : Trace("trigger") << " " << n << std::endl;
77 : : }
78 : : }
79 : 37370 : std::vector<Node> extNodes;
80 [ + + ]: 78113 : for (const Node& nt : d_nodes)
81 : : {
82 : : // note we must display the original form, so we go back to bound vars
83 : 81486 : Node ns = d_qreg.substituteInstConstantsToBoundVariables(nt, q);
84 : 40743 : extNodes.push_back(ns);
85 : 40743 : }
86 : 37370 : d_trNode = nodeManager()->mkNode(Kind::SEXPR, extNodes);
87 [ - + ]: 37370 : if (isOutputOn(OutputTag::TRIGGER))
88 : : {
89 [ - - ]: 0 : output(OutputTag::TRIGGER) << (isUser ? "(user-trigger " : "(trigger ");
90 : 0 : QuantAttributes& qa = d_qreg.getQuantAttributes();
91 : 0 : output(OutputTag::TRIGGER) << qa.quantToString(q) << " " << d_trNode;
92 : : }
93 : 37370 : QuantifiersStatistics& stats = qs.getStats();
94 [ + + ]: 37370 : if (d_nodes.size() == 1)
95 : : {
96 [ + + ]: 34641 : if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
97 : : {
98 : 17432 : d_mg = new InstMatchGeneratorSimple(env, this, q, d_nodes[0]);
99 : 17432 : ++(stats.d_simple_triggers);
100 : 17432 : output(OutputTag::TRIGGER) << " :simple";
101 : : }
102 : : else
103 : : {
104 : 17209 : d_mg = InstMatchGenerator::mkInstMatchGenerator(env, this, q, d_nodes[0]);
105 : 17209 : ++(stats.d_triggers);
106 : : }
107 : : }
108 : : else
109 : : {
110 [ - + ]: 2729 : if (options().quantifiers.multiTriggerCache)
111 : : {
112 : 0 : d_mg = new InstMatchGeneratorMulti(env, this, q, d_nodes);
113 : 0 : output(OutputTag::TRIGGER) << " :multi-cache";
114 : : }
115 : : else
116 : : {
117 : 2729 : d_mg =
118 : 2729 : InstMatchGenerator::mkInstMatchGeneratorMulti(env, this, q, d_nodes);
119 : 2729 : output(OutputTag::TRIGGER) << " :multi";
120 : : }
121 [ - + ]: 2729 : if (TraceIsOn("multi-trigger"))
122 : : {
123 [ - - ]: 0 : Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
124 [ - - ]: 0 : for (const Node& nc : d_nodes)
125 : : {
126 [ - - ]: 0 : Trace("multi-trigger") << " " << nc << std::endl;
127 : : }
128 : : }
129 : 2729 : ++(stats.d_multi_triggers);
130 : : }
131 [ - + ]: 37370 : if (isOutputOn(OutputTag::TRIGGER))
132 : : {
133 : 0 : output(OutputTag::TRIGGER) << ")" << std::endl;
134 : : }
135 : :
136 [ + - ]: 37370 : Trace("trigger-debug") << "Finished making trigger." << std::endl;
137 : 37370 : }
138 : :
139 [ + - ]: 74448 : Trigger::~Trigger() { delete d_mg; }
140 : :
141 : 325295 : void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); }
142 : :
143 : 325295 : void Trigger::reset(Node eqc) { d_mg->reset(eqc); }
144 : :
145 : 30943 : bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; }
146 : :
147 : 0 : Node Trigger::getInstPattern() const
148 : : {
149 : 0 : return nodeManager()->mkNode(Kind::INST_PATTERN, d_nodes);
150 : : }
151 : :
152 : 108149 : uint64_t Trigger::addInstantiations()
153 : : {
154 : 108149 : uint64_t gtAddedLemmas = 0;
155 [ + + ]: 108149 : if (!d_groundTerms.empty())
156 : : {
157 : : // for each ground term t that does not exist in the equality engine, we
158 : : // add a purification lemma of the form (k = t).
159 : 8083 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
160 [ + + ]: 16480 : for (const Node& gt : d_groundTerms)
161 : : {
162 : 8397 : if (!ee->hasTerm(gt) && !gt.getType().isBoolean())
163 : : {
164 : 1009 : Node k = SkolemManager::mkPurifySkolem(gt);
165 : 1009 : Node eq = k.eqNode(gt);
166 [ + - ]: 2018 : Trace("trigger-gt-lemma")
167 : 1009 : << "Trigger: ground term purify lemma: " << eq << std::endl;
168 : 1009 : d_qim.addPendingLemma(eq, InferenceId::QUANTIFIERS_GT_PURIFY);
169 : 1009 : gtAddedLemmas++;
170 : 1009 : }
171 : : }
172 : : }
173 : 108149 : uint64_t addedLemmas = d_mg->addInstantiations(d_instMatch);
174 [ - + ]: 108149 : if (TraceIsOn("inst-trigger"))
175 : : {
176 [ - - ]: 0 : if (addedLemmas > 0)
177 : : {
178 [ - - ]: 0 : Trace("inst-trigger") << "Added " << addedLemmas
179 : 0 : << " lemmas, trigger was " << d_nodes << std::endl;
180 : : }
181 : : }
182 : 108149 : return gtAddedLemmas + addedLemmas;
183 : : }
184 : :
185 : 144486 : bool Trigger::sendInstantiation(std::vector<Node>& m)
186 : : {
187 : 144486 : InferenceId id = d_mg->getInferenceId();
188 : 144486 : return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode);
189 : : }
190 : :
191 : 0 : int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
192 : :
193 : 40743 : Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
194 : : Node n,
195 : : std::vector<Node>& gts)
196 : : {
197 : 40743 : NodeManager* nm = n.getNodeManager();
198 : 40743 : std::unordered_map<TNode, Node> visited;
199 : 40743 : std::unordered_map<TNode, Node>::iterator it;
200 : 40743 : std::vector<TNode> visit;
201 : 40743 : TNode cur;
202 : 40743 : visit.push_back(n);
203 : : do
204 : : {
205 : 329923 : cur = visit.back();
206 : 329923 : visit.pop_back();
207 : 329923 : it = visited.find(cur);
208 [ + + ]: 329923 : if (it == visited.end())
209 : : {
210 [ + + ][ + + ]: 224677 : if (cur.getNumChildren() == 0 || cur.getKind() == Kind::BOUND_VAR_LIST)
[ + + ]
211 : : {
212 : 120811 : visited[cur] = cur;
213 : : }
214 [ + + ]: 103866 : else if (!TermUtil::hasInstConstAttr(cur))
215 : : {
216 : : // cur has no INST_CONSTANT, thus is ground.
217 : 3366 : Node vcur = val.getPreprocessedTerm(cur);
218 : 3366 : gts.push_back(vcur);
219 : 3366 : visited[cur] = vcur;
220 : 3366 : }
221 : : else
222 : : {
223 : 100500 : visited[cur] = Node::null();
224 : 100500 : visit.push_back(cur);
225 : 100500 : visit.insert(visit.end(), cur.begin(), cur.end());
226 : : }
227 : : }
228 [ + + ]: 105246 : else if (it->second.isNull())
229 : : {
230 : 100500 : Node ret = cur;
231 : 100500 : bool childChanged = false;
232 : 100500 : std::vector<Node> children;
233 [ + + ]: 100500 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
234 : : {
235 : 82978 : children.push_back(cur.getOperator());
236 : : }
237 [ + + ]: 289180 : for (const Node& cn : cur)
238 : : {
239 : 188680 : it = visited.find(cn);
240 [ - + ][ - + ]: 188680 : Assert(it != visited.end());
[ - - ]
241 [ - + ][ - + ]: 188680 : Assert(!it->second.isNull());
[ - - ]
242 [ + + ][ + + ]: 188680 : childChanged = childChanged || cn != it->second;
243 : 188680 : children.push_back(it->second);
244 : 188680 : }
245 [ + + ]: 100500 : if (childChanged)
246 : : {
247 : 221 : ret = nm->mkNode(cur.getKind(), children);
248 : : }
249 : 100500 : visited[cur] = ret;
250 : 100500 : }
251 [ + + ]: 329923 : } while (!visit.empty());
252 [ - + ][ - + ]: 40743 : Assert(visited.find(n) != visited.end());
[ - - ]
253 [ - + ][ - + ]: 40743 : Assert(!visited.find(n)->second.isNull());
[ - - ]
254 : 81486 : return visited[n];
255 : 40743 : }
256 : :
257 : 80454 : void Trigger::debugPrint(CVC5_UNUSED const char* c) const
258 : : {
259 [ + - ]: 80454 : Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl;
260 : 80454 : }
261 : :
262 : : } // namespace inst
263 : : } // namespace quantifiers
264 : : } // namespace theory
265 : : } // namespace cvc5::internal
|
