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-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 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 : 40493 : InstantiationEngine::InstantiationEngine(Env& env,
36 : : QuantifiersState& qs,
37 : : QuantifiersInferenceManager& qim,
38 : : QuantifiersRegistry& qr,
39 : 40493 : 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 : 40493 : d_quant_rel(nullptr)
47 : : {
48 [ + + ]: 40493 : if (options().quantifiers.relevantTriggers)
49 : : {
50 : 5 : d_quant_rel.reset(new quantifiers::QuantRelevance(env));
51 : : }
52 [ + - ]: 40493 : if (options().quantifiers.eMatching)
53 : : {
54 : : // these are the instantiation strategies for E-matching
55 : : // user-provided patterns
56 [ + - ]: 40493 : if (options().quantifiers.userPatternsQuant != options::UserPatMode::IGNORE)
57 : : {
58 : 40493 : d_isup.reset(
59 : 40493 : new InstStrategyUserPatterns(d_env, d_trdb, qs, qim, qr, tr));
60 : 40493 : d_instStrategies.push_back(d_isup.get());
61 : : }
62 : :
63 : : // auto-generated patterns
64 : 40493 : d_i_ag.reset(new InstStrategyAutoGenTriggers(
65 : 40493 : d_env, d_trdb, qs, qim, qr, tr, d_quant_rel.get()));
66 : 40493 : d_instStrategies.push_back(d_i_ag.get());
67 : : }
68 : 40493 : }
69 : :
70 : 80494 : InstantiationEngine::~InstantiationEngine() {}
71 : :
72 : 0 : std::string InstantiationEngine::identify() const { return "ematching"; }
73 : :
74 : 35932 : void InstantiationEngine::presolve() {
75 [ + + ]: 107796 : for( unsigned i=0; i<d_instStrategies.size(); ++i ){
76 : 71864 : d_instStrategies[i]->presolve();
77 : : }
78 : 35932 : }
79 : :
80 : 5117 : void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
81 : 5117 : size_t lastWaiting = d_qim.numPendingLemmas();
82 : : //iterate over an internal effort level e
83 : 5117 : int e = 0;
84 [ + + ]: 5117 : int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
85 : 5117 : bool finished = false;
86 : : //while unfinished, try effort level=0,1,2....
87 [ + + ][ + - ]: 15353 : while( !finished && e<=eLimit ){
88 [ + - ]: 10241 : Trace("inst-engine-debug") << "IE: Prepare instantiation (" << e << ")." << std::endl;
89 : 10241 : finished = true;
90 : : //instantiate each quantifier
91 [ + + ]: 184904 : for( unsigned i=0; i<d_quants.size(); i++ ){
92 : 174668 : Node q = d_quants[i];
93 [ + - ]: 174668 : Trace("inst-engine-debug") << "IE: Instantiate " << q << "..." << std::endl;
94 : : //int e_use = d_quantEngine->getRelevance( q )==-1 ? e - 1 : e;
95 : 174668 : int e_use = e;
96 [ + - ]: 174668 : if( e_use>=0 ){
97 [ + - ]: 174668 : Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
98 : : //check each instantiation strategy
99 [ + + ]: 523999 : for( unsigned j=0; j<d_instStrategies.size(); j++ ){
100 : 349336 : InstStrategy* is = d_instStrategies[j];
101 [ + - ][ - + ]: 349336 : Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
[ - - ]
102 : 349336 : InstStrategyStatus quantStatus = is->process(q, effort, e_use);
103 [ + - ]: 698672 : Trace("inst-engine-debug")
104 : 0 : << " -> unfinished= "
105 : 0 : << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
106 : 349336 : << ", conflict=" << d_qstate.isInConflict() << std::endl;
107 [ + + ]: 349336 : if (d_qstate.isInConflict())
108 : : {
109 : 5 : return;
110 : : }
111 [ + + ]: 349331 : else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
112 : : {
113 : 146016 : finished = false;
114 : : }
115 : : }
116 : : }
117 : : }
118 : : //do not consider another level if already added lemma at this level
119 [ + + ]: 10236 : if (d_qim.numPendingLemmas() > lastWaiting)
120 : : {
121 : 2879 : finished = true;
122 : : }
123 : 10236 : e++;
124 : : }
125 : : }
126 : :
127 : 112214 : bool InstantiationEngine::needsCheck( Theory::Effort e ){
128 : 112214 : return d_qstate.getInstWhenNeedsCheck(e);
129 : : }
130 : :
131 : 45016 : void InstantiationEngine::reset_round( Theory::Effort e ){
132 : : //if not, proceed to instantiation round
133 : : //reset the instantiation strategies
134 [ + + ]: 135048 : for( unsigned i=0; i<d_instStrategies.size(); ++i ){
135 : 90032 : InstStrategy* is = d_instStrategies[i];
136 : 90032 : is->processResetInstantiationRound( e );
137 : : }
138 : 45016 : }
139 : :
140 : 87815 : void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
141 : : {
142 : 87815 : CodeTimer codeTimer(d_qstate.getStats().d_ematching_time);
143 [ + + ]: 87815 : if (quant_e != QEFFORT_STANDARD)
144 : : {
145 : 59454 : return;
146 : : }
147 : 28361 : beginCallDebug();
148 : : // collect all active quantified formulas belonging to this
149 : 28361 : bool quantActive = false;
150 : 28361 : d_quants.clear();
151 : 28361 : FirstOrderModel* m = d_treg.getModel();
152 : 28361 : size_t nquant = m->getNumAssertedQuantifiers();
153 [ + + ]: 144226 : for (size_t i = 0; i < nquant; i++)
154 : : {
155 : 231730 : Node q = m->getAssertedQuantifier(i, true);
156 : 115865 : if (shouldProcess(q) && m->isQuantifierActive(q))
157 : : {
158 : 87333 : quantActive = true;
159 : 87333 : d_quants.push_back(q);
160 : : }
161 : : }
162 [ + - ]: 56722 : Trace("inst-engine-debug")
163 : 28361 : << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
164 [ + - ]: 28361 : Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
165 [ + + ]: 28361 : if (quantActive)
166 : : {
167 : 5117 : doInstantiationRound(e);
168 : : }
169 : : else
170 : : {
171 : 23244 : d_quants.clear();
172 : : }
173 : 28361 : endCallDebug();
174 : : }
175 : :
176 : 1257 : bool InstantiationEngine::checkCompleteFor( Node q ) {
177 : : //TODO?
178 : 1257 : return false;
179 : : }
180 : :
181 : 48163 : void InstantiationEngine::checkOwnership(Node q)
182 : : {
183 : 48163 : if (options().quantifiers.userPatternsQuant == options::UserPatMode::STRICT
184 [ + + ][ + - ]: 48163 : && q.getNumChildren() == 3)
[ + + ]
185 : : {
186 : : //if strict triggers, take ownership of this quantified formula
187 [ + + ]: 35 : if (QuantAttributes::hasPattern(q))
188 : : {
189 : 5 : d_qreg.setOwner(q, this, 1);
190 : : }
191 : : }
192 : 48163 : }
193 : :
194 : 48163 : void InstantiationEngine::registerQuantifier(Node q)
195 : : {
196 [ + + ]: 48163 : if (!shouldProcess(q))
197 : : {
198 : 6157 : return;
199 : : }
200 [ + + ]: 42006 : if (d_quant_rel)
201 : : {
202 : 458 : d_quant_rel->registerQuantifier(q);
203 : : }
204 : : // take into account user patterns
205 [ + + ]: 42006 : if (q.getNumChildren() == 3)
206 : : {
207 : 23703 : Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
208 : : // add patterns
209 [ + + ]: 16318 : for (const Node& p : subsPat)
210 : : {
211 [ + + ]: 8417 : if (p.getKind() == Kind::INST_PATTERN)
212 : : {
213 : 7329 : addUserPattern(q, p);
214 : : }
215 [ + + ]: 1088 : else if (p.getKind() == Kind::INST_NO_PATTERN)
216 : : {
217 : 10 : addUserNoPattern(q, p);
218 : : }
219 : : }
220 : : }
221 : : }
222 : :
223 : 7329 : void InstantiationEngine::addUserPattern(Node q, Node pat) {
224 [ + - ]: 7329 : if (d_isup) {
225 : 7329 : d_isup->addUserPattern(q, pat);
226 : : }
227 : 7329 : }
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 : 164028 : bool InstantiationEngine::shouldProcess(Node q)
236 : : {
237 [ + + ]: 164028 : if (!d_qreg.hasOwnership(q, this))
238 : : {
239 : 30479 : return false;
240 : : }
241 : : // also ignore internal quantifiers
242 : 133549 : QuantAttributes& qattr = d_qreg.getQuantAttributes();
243 [ + + ]: 133549 : if (qattr.isQuantBounded(q))
244 : : {
245 : 4158 : return false;
246 : : }
247 : 129391 : return true;
248 : : }
249 : :
250 : : } // namespace quantifiers
251 : : } // namespace theory
252 : : } // namespace cvc5::internal
|
