Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Morgan Deters, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 instantiation engine class
14 : : */
15 : :
16 : : #include "theory/quantifiers/ematching/instantiation_engine.h"
17 : :
18 : : #include "options/quantifiers_options.h"
19 : : #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
20 : : #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
21 : : #include "theory/quantifiers/ematching/trigger.h"
22 : : #include "theory/quantifiers/first_order_model.h"
23 : : #include "theory/quantifiers/quantifiers_attributes.h"
24 : : #include "theory/quantifiers/term_database.h"
25 : : #include "theory/quantifiers/term_util.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : : using namespace cvc5::context;
29 : : using namespace cvc5::internal::theory::quantifiers::inst;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace quantifiers {
34 : :
35 : 42907 : InstantiationEngine::InstantiationEngine(Env& env,
36 : : QuantifiersState& qs,
37 : : QuantifiersInferenceManager& qim,
38 : : QuantifiersRegistry& qr,
39 : 42907 : TermRegistry& tr)
40 : : : QuantifiersModule(env, qs, qim, qr, tr),
41 : : d_instStrategies(),
42 : : d_isup(),
43 : : d_i_ag(),
44 : : d_quants(),
45 : : d_trdb(d_env, qs, qim, qr, tr),
46 : 42907 : d_quant_rel(nullptr)
47 : : {
48 [ + + ]: 42907 : if (options().quantifiers.relevantTriggers)
49 : : {
50 : 5 : d_quant_rel.reset(new quantifiers::QuantRelevance(env));
51 : : }
52 [ + - ]: 42907 : if (options().quantifiers.eMatching)
53 : : {
54 : : // these are the instantiation strategies for E-matching
55 : : // user-provided patterns
56 [ + - ]: 42907 : if (options().quantifiers.userPatternsQuant != options::UserPatMode::IGNORE)
57 : : {
58 : 42907 : d_isup.reset(
59 : 42907 : new InstStrategyUserPatterns(d_env, d_trdb, qs, qim, qr, tr));
60 : 42907 : d_instStrategies.push_back(d_isup.get());
61 : : }
62 : :
63 : : // auto-generated patterns
64 : 42907 : d_i_ag.reset(new InstStrategyAutoGenTriggers(
65 : 42907 : d_env, d_trdb, qs, qim, qr, tr, d_quant_rel.get()));
66 : 42907 : d_instStrategies.push_back(d_i_ag.get());
67 : : }
68 : 42907 : }
69 : :
70 : 85322 : InstantiationEngine::~InstantiationEngine() {}
71 : :
72 : 0 : std::string InstantiationEngine::identify() const { return "ematching"; }
73 : :
74 : 38272 : void InstantiationEngine::presolve() {
75 [ + + ]: 114816 : for( unsigned i=0; i<d_instStrategies.size(); ++i ){
76 : 76544 : d_instStrategies[i]->presolve();
77 : : }
78 : 38272 : }
79 : :
80 : 6544 : void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
81 : 6544 : size_t lastWaiting = d_qim.numPendingLemmas();
82 : : //iterate over an internal effort level e
83 : 6544 : int e = 0;
84 [ + + ]: 6544 : int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
85 : 6544 : bool finished = false;
86 : : //while unfinished, try effort level=0,1,2....
87 [ + + ][ + - ]: 19633 : while( !finished && e<=eLimit ){
88 [ + - ]: 13096 : Trace("inst-engine-debug") << "IE: Prepare instantiation (" << e << ")." << std::endl;
89 : 13096 : finished = true;
90 : : //instantiate each quantifier
91 [ + + ]: 219006 : for( unsigned i=0; i<d_quants.size(); i++ ){
92 : 205917 : Node q = d_quants[i];
93 [ + - ]: 205917 : Trace("inst-engine-debug") << "IE: Instantiate " << q << "..." << std::endl;
94 : : //int e_use = d_quantEngine->getRelevance( q )==-1 ? e - 1 : e;
95 : 205917 : int e_use = e;
96 [ + - ]: 205917 : if( e_use>=0 ){
97 [ + - ]: 205917 : Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
98 : : //check each instantiation strategy
99 [ + + ]: 617744 : for( unsigned j=0; j<d_instStrategies.size(); j++ ){
100 : 411834 : InstStrategy* is = d_instStrategies[j];
101 [ + - ][ - + ]: 411834 : Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
[ - - ]
102 : 411834 : InstStrategyStatus quantStatus = is->process(q, effort, e_use);
103 [ + - ]: 823668 : Trace("inst-engine-debug")
104 : 0 : << " -> unfinished= "
105 : 0 : << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
106 : 411834 : << ", conflict=" << d_qstate.isInConflict() << std::endl;
107 [ + + ]: 411834 : if (d_qstate.isInConflict())
108 : : {
109 : 7 : return;
110 : : }
111 [ + + ]: 411827 : else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
112 : : {
113 : 174063 : finished = false;
114 : : }
115 : : }
116 : : }
117 : : }
118 : : //do not consider another level if already added lemma at this level
119 [ + + ]: 13089 : if (d_qim.numPendingLemmas() > lastWaiting)
120 : : {
121 : 3744 : finished = true;
122 : : }
123 : 13089 : e++;
124 : : }
125 : : }
126 : :
127 : 126889 : bool InstantiationEngine::needsCheck( Theory::Effort e ){
128 : 126889 : return d_qstate.getInstWhenNeedsCheck(e);
129 : : }
130 : :
131 : 53206 : void InstantiationEngine::reset_round( Theory::Effort e ){
132 : : //if not, proceed to instantiation round
133 : : //reset the instantiation strategies
134 [ + + ]: 159618 : for( unsigned i=0; i<d_instStrategies.size(); ++i ){
135 : 106412 : InstStrategy* is = d_instStrategies[i];
136 : 106412 : is->processResetInstantiationRound( e );
137 : : }
138 : 53206 : }
139 : :
140 : 98739 : void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
141 : : {
142 : 98739 : CodeTimer codeTimer(d_qstate.getStats().d_ematching_time);
143 [ + + ]: 98739 : if (quant_e != QEFFORT_STANDARD)
144 : : {
145 : 66518 : return;
146 : : }
147 : 32221 : beginCallDebug();
148 : : // collect all active quantified formulas belonging to this
149 : 32221 : bool quantActive = false;
150 : 32221 : d_quants.clear();
151 : 32221 : FirstOrderModel* m = d_treg.getModel();
152 : 32221 : size_t nquant = m->getNumAssertedQuantifiers();
153 [ + + ]: 166578 : for (size_t i = 0; i < nquant; i++)
154 : : {
155 : 268714 : Node q = m->getAssertedQuantifier(i, true);
156 : 134357 : if (shouldProcess(q) && m->isQuantifierActive(q))
157 : : {
158 : 102959 : quantActive = true;
159 : 102959 : d_quants.push_back(q);
160 : : }
161 : : }
162 [ + - ]: 64442 : Trace("inst-engine-debug")
163 : 32221 : << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
164 [ + - ]: 32221 : Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
165 [ + + ]: 32221 : if (quantActive)
166 : : {
167 : 6544 : doInstantiationRound(e);
168 : : }
169 : : else
170 : : {
171 : 25677 : d_quants.clear();
172 : : }
173 : 32221 : endCallDebug();
174 : : }
175 : :
176 : 1461 : bool InstantiationEngine::checkCompleteFor( Node q ) {
177 : : //TODO?
178 : 1461 : return false;
179 : : }
180 : :
181 : 55608 : void InstantiationEngine::checkOwnership(Node q)
182 : : {
183 : 55608 : if (options().quantifiers.userPatternsQuant == options::UserPatMode::STRICT
184 [ + + ][ + - ]: 55608 : && q.getNumChildren() == 3)
[ + + ]
185 : : {
186 : : //if strict triggers, take ownership of this quantified formula
187 [ + + ]: 42 : if (QuantAttributes::hasPattern(q))
188 : : {
189 : 6 : d_qreg.setOwner(q, this, 1);
190 : : }
191 : : }
192 : 55608 : }
193 : :
194 : 55608 : void InstantiationEngine::registerQuantifier(Node q)
195 : : {
196 [ + + ]: 55608 : if (!shouldProcess(q))
197 : : {
198 : 6345 : return;
199 : : }
200 [ + + ]: 49263 : if (d_quant_rel)
201 : : {
202 : 458 : d_quant_rel->registerQuantifier(q);
203 : : }
204 : : // take into account user patterns
205 [ + + ]: 49263 : if (q.getNumChildren() == 3)
206 : : {
207 : 26013 : Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
208 : : // add patterns
209 [ + + ]: 17833 : for (const Node& p : subsPat)
210 : : {
211 [ + + ]: 9162 : if (p.getKind() == Kind::INST_PATTERN)
212 : : {
213 : 7819 : addUserPattern(q, p);
214 : : }
215 [ + + ]: 1343 : else if (p.getKind() == Kind::INST_NO_PATTERN)
216 : : {
217 : 10 : addUserNoPattern(q, p);
218 : : }
219 : : }
220 : : }
221 : : }
222 : :
223 : 7819 : void InstantiationEngine::addUserPattern(Node q, Node pat) {
224 [ + - ]: 7819 : if (d_isup) {
225 : 7819 : d_isup->addUserPattern(q, pat);
226 : : }
227 : 7819 : }
228 : :
229 : 10 : void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
230 [ + - ]: 10 : if (d_i_ag) {
231 : 10 : d_i_ag->addUserNoPattern(q, pat);
232 : : }
233 : 10 : }
234 : :
235 : 189965 : bool InstantiationEngine::shouldProcess(Node q)
236 : : {
237 [ + + ]: 189965 : if (!d_qreg.hasOwnership(q, this))
238 : : {
239 : 33262 : return false;
240 : : }
241 : : // also ignore internal quantifiers
242 : 156703 : QuantAttributes& qattr = d_qreg.getQuantAttributes();
243 [ + + ]: 156703 : if (qattr.isQuantBounded(q))
244 : : {
245 : 4429 : return false;
246 : : }
247 : 152274 : return true;
248 : : }
249 : :
250 : : } // namespace quantifiers
251 : : } // namespace theory
252 : : } // namespace cvc5::internal
|
