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