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 model engine class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/fmf/model_engine.h"
14 : :
15 : : #include "options/quantifiers_options.h"
16 : : #include "theory/quantifiers/first_order_model.h"
17 : : #include "theory/quantifiers/fmf/full_model_check.h"
18 : : #include "theory/quantifiers/instantiate.h"
19 : : #include "theory/quantifiers/quant_rep_bound_ext.h"
20 : : #include "theory/quantifiers/quantifiers_attributes.h"
21 : : #include "theory/quantifiers/term_database.h"
22 : : #include "theory/rep_set_iterator.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : : using namespace cvc5::context;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace quantifiers {
30 : :
31 : : //Model Engine constructor
32 : 32084 : ModelEngine::ModelEngine(Env& env,
33 : : QuantifiersState& qs,
34 : : QuantifiersInferenceManager& qim,
35 : : QuantifiersRegistry& qr,
36 : : TermRegistry& tr,
37 : 32084 : QModelBuilder* builder)
38 : : : QuantifiersModule(env, qs, qim, qr, tr),
39 : 32084 : d_incomplete_check(true),
40 : 32084 : d_addedLemmas(0),
41 : 32084 : d_triedLemmas(0),
42 : 32084 : d_totalLemmas(0),
43 : 32084 : d_builder(builder)
44 : : {
45 : :
46 : 32084 : }
47 : :
48 : 63610 : ModelEngine::~ModelEngine() {
49 : :
50 : 63610 : }
51 : :
52 : 0 : std::string ModelEngine::identify() const { return "fmf-inst"; }
53 : :
54 : 80728 : bool ModelEngine::needsCheck( Theory::Effort e ) {
55 : 80728 : return e==Theory::EFFORT_LAST_CALL;
56 : : }
57 : :
58 : 9734 : QuantifiersModule::QEffort ModelEngine::needsModel(CVC5_UNUSED Theory::Effort e)
59 : : {
60 [ - + ]: 9734 : if (options().quantifiers.mbqiInterleave)
61 : : {
62 : 0 : return QEFFORT_STANDARD;
63 : : }
64 : : else
65 : : {
66 : 9734 : return QEFFORT_MODEL;
67 : : }
68 : : }
69 : :
70 : 36296 : void ModelEngine::reset_round(CVC5_UNUSED Theory::Effort e)
71 : : {
72 : 36296 : d_incomplete_check = true;
73 : 36296 : }
74 : 28143 : void ModelEngine::check(CVC5_UNUSED Theory::Effort e, QEffort quant_e)
75 : : {
76 : 28143 : bool doCheck = false;
77 [ - + ]: 28143 : if (options().quantifiers.mbqiInterleave)
78 : : {
79 [ - - ][ - - ]: 0 : doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
80 : : }
81 [ + - ]: 28143 : if( !doCheck ){
82 : 28143 : doCheck = quant_e == QEFFORT_MODEL;
83 : : }
84 [ + + ]: 28143 : if( doCheck ){
85 [ - + ][ - + ]: 6703 : Assert(!d_qstate.isInConflict());
[ - - ]
86 : 6703 : int addedLemmas = 0;
87 : :
88 : : //the following will test that the model satisfies all asserted universal quantifiers by
89 : : // (model-based) exhaustive instantiation.
90 : 6703 : beginCallDebug();
91 [ + - ]: 6703 : Trace("model-engine-debug") << "Check model..." << std::endl;
92 : 6703 : d_incomplete_check = false;
93 : : // print debug
94 [ - + ]: 6703 : if (TraceIsOn("fmf-model-complete"))
95 : : {
96 [ - - ]: 0 : Trace("fmf-model-complete") << std::endl;
97 : 0 : debugPrint("fmf-model-complete");
98 : : }
99 : : // successfully built an acceptable model, now check it
100 : 6703 : addedLemmas += checkModel();
101 : :
102 : 6703 : endCallDebug();
103 : :
104 [ + + ]: 6703 : if( addedLemmas==0 ){
105 [ + - ]: 10164 : Trace("model-engine-debug")
106 : 0 : << "No lemmas added, incomplete = "
107 [ - - ][ - - ]: 5082 : << (d_incomplete_check || !d_incompleteQuants.empty()) << std::endl;
108 : : // cvc5 will answer SAT or unknown
109 [ - + ]: 5082 : if( TraceIsOn("fmf-consistent") ){
110 [ - - ]: 0 : Trace("fmf-consistent") << std::endl;
111 : 0 : debugPrint("fmf-consistent");
112 : : }
113 : : }
114 : : }
115 : 28143 : }
116 : :
117 : 2870 : bool ModelEngine::checkComplete(IncompleteId& incId)
118 : : {
119 [ - + ]: 2870 : if (d_incomplete_check)
120 : : {
121 : 0 : incId = IncompleteId::QUANTIFIERS_FMF;
122 : 0 : return false;
123 : : }
124 : 2870 : return true;
125 : : }
126 : :
127 : 1978 : bool ModelEngine::checkCompleteFor( Node q ) {
128 : 1978 : return d_incompleteQuants.find(q) == d_incompleteQuants.end();
129 : : }
130 : :
131 : 26039 : void ModelEngine::registerQuantifier( Node f ){
132 [ - + ]: 26039 : if( TraceIsOn("fmf-warn") ){
133 : 0 : bool canHandle = true;
134 [ - - ]: 0 : for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
135 : 0 : TypeNode tn = f[0][i].getType();
136 [ - - ]: 0 : if (!tn.isUninterpretedSort())
137 : : {
138 [ - - ]: 0 : if (!d_env.isFiniteType(tn))
139 : : {
140 [ - - ]: 0 : if( tn.isInteger() ){
141 [ - - ]: 0 : if (!options().quantifiers.fmfBound)
142 : : {
143 : 0 : canHandle = false;
144 : : }
145 : : }else{
146 : 0 : canHandle = false;
147 : : }
148 : : }
149 : : }
150 : 0 : }
151 [ - - ]: 0 : if( !canHandle ){
152 [ - - ]: 0 : Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
153 : : }
154 : : }
155 : 26039 : }
156 : :
157 : 6703 : int ModelEngine::checkModel(){
158 : 6703 : FirstOrderModel* fm = d_treg.getModel();
159 : :
160 : : //for debugging, setup
161 : 6703 : for (std::map<TypeNode, std::vector<Node> >::iterator it =
162 : 6703 : fm->getRepSetPtr()->d_type_reps.begin();
163 [ + + ]: 33187 : it != fm->getRepSetPtr()->d_type_reps.end();
164 : 26484 : ++it)
165 : : {
166 [ + + ]: 26484 : if (it->first.isUninterpretedSort())
167 : : {
168 [ + - ]: 6248 : Trace("model-engine") << "Cardinality( " << it->first << " )"
169 : 3124 : << " = " << it->second.size() << std::endl;
170 [ + - ]: 3124 : Trace("model-engine-debug") << " Reps : ";
171 [ + + ]: 11342 : for( size_t i=0; i<it->second.size(); i++ ){
172 [ + - ]: 8218 : Trace("model-engine-debug") << it->second[i] << " ";
173 : : }
174 [ + - ]: 3124 : Trace("model-engine-debug") << std::endl;
175 [ + - ]: 3124 : Trace("model-engine-debug") << " Term reps : ";
176 [ + + ]: 11342 : for( size_t i=0; i<it->second.size(); i++ ){
177 : 16436 : Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0);
178 [ - + ]: 8218 : if (r.isNull())
179 : : {
180 : : // there was an invalid equivalence class
181 : 0 : d_incomplete_check = true;
182 : : }
183 [ + - ]: 8218 : Trace("model-engine-debug") << r << " ";
184 : 8218 : }
185 [ + - ]: 3124 : Trace("model-engine-debug") << std::endl;
186 : 3124 : Node mbt = fm->getModelBasisTerm(it->first);
187 [ + - ]: 3124 : Trace("model-engine-debug") << " Basis term : " << mbt << std::endl;
188 : 3124 : }
189 : : }
190 : :
191 : 6703 : d_triedLemmas = 0;
192 : 6703 : d_addedLemmas = 0;
193 : 6703 : d_totalLemmas = 0;
194 : : //for statistics
195 [ - + ]: 6703 : if( TraceIsOn("model-engine") ){
196 [ - - ]: 0 : for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
197 : 0 : Node f = fm->getAssertedQuantifier( i );
198 : 0 : if (fm->isQuantifierActive(f) && shouldProcess(f))
199 : : {
200 : 0 : int totalInst = 1;
201 [ - - ]: 0 : for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
202 : 0 : TypeNode tn = f[0][j].getType();
203 [ - - ]: 0 : if (fm->getRepSet()->hasType(tn))
204 : : {
205 : 0 : totalInst =
206 : 0 : totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
207 : : }
208 : 0 : }
209 : 0 : d_totalLemmas += totalInst;
210 : : }
211 : 0 : }
212 : : }
213 : :
214 [ + - ]: 6703 : Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
215 : : // FMC uses two sub-effort levels
216 : 6703 : options::FmfMbqiMode mode = options().quantifiers.fmfMbqiMode;
217 : 6703 : int e_max = mode == options::FmfMbqiMode::FMC
218 [ + + ]: 6703 : ? 2
219 : 1013 : : (mode == options::FmfMbqiMode::TRUST ? 0 : 1);
220 [ + + ]: 16749 : for( int e=0; e<e_max; e++) {
221 : 11667 : d_incompleteQuants.clear();
222 [ + + ]: 38794 : for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
223 : 27127 : Node q = fm->getAssertedQuantifier( i, true );
224 [ + - ]: 27127 : Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
225 : : //determine if we should check this quantifier
226 [ + + ]: 27127 : if (!fm->isQuantifierActive(q))
227 : : {
228 [ + - ]: 176 : Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
229 : 176 : continue;
230 : : }
231 [ + + ]: 26951 : if (!shouldProcess(q))
232 : : {
233 [ + - ]: 12802 : Trace("fmf-exh-inst") << "-> Not processed : " << q << std::endl;
234 : 12802 : d_incompleteQuants.insert(q);
235 : 12802 : continue;
236 : : }
237 : 14149 : exhaustiveInstantiate(q, e);
238 [ - + ]: 14149 : if (d_qstate.isInConflict())
239 : : {
240 : 0 : break;
241 : : }
242 [ + + ][ - ]: 27127 : }
243 [ + + ]: 11667 : if( d_addedLemmas>0 ){
244 : 1621 : break;
245 : : }else{
246 [ - + ][ - + ]: 10046 : Assert(!d_qstate.isInConflict());
[ - - ]
247 : : }
248 : : }
249 : :
250 : : //print debug information
251 [ - + ]: 6703 : if (d_qstate.isInConflict())
252 : : {
253 [ - - ]: 0 : Trace("model-engine") << "Conflict, added lemmas = ";
254 : : }else{
255 [ + - ]: 6703 : Trace("model-engine") << "Added Lemmas = ";
256 : : }
257 [ + - ]: 6703 : Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
258 [ + - ]: 6703 : Trace("model-engine") << d_totalLemmas << std::endl;
259 : 6703 : return d_addedLemmas;
260 : : }
261 : :
262 : 14149 : void ModelEngine::exhaustiveInstantiate(Node q, int effort)
263 : : {
264 : : //first check if the builder can do the exhaustive instantiation
265 : 14149 : unsigned prev_alem = d_builder->getNumAddedLemmas();
266 : 14149 : unsigned prev_tlem = d_builder->getNumTriedLemmas();
267 : 14149 : FirstOrderModel* fm = d_treg.getModel();
268 : 14149 : int retEi = d_builder->doExhaustiveInstantiation(fm, q, effort);
269 [ + + ]: 14149 : if( retEi!=0 ){
270 [ - + ]: 13979 : if( retEi<0 ){
271 [ - - ]: 0 : Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
272 : 0 : d_incompleteQuants.insert(q);
273 : : }else{
274 [ + - ]: 13979 : Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
275 : : }
276 : 13979 : d_triedLemmas += d_builder->getNumTriedLemmas() - prev_tlem;
277 : 13979 : d_addedLemmas += d_builder->getNumAddedLemmas() - prev_alem;
278 : : }else{
279 [ - + ]: 170 : if( TraceIsOn("fmf-exh-inst-debug") ){
280 [ - - ]: 0 : Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
281 [ - - ]: 0 : for (size_t i = 0, nchild = q[0].getNumChildren(); i < nchild; i++)
282 : : {
283 [ - - ]: 0 : Trace("fmf-exh-inst-debug")
284 : 0 : << d_qreg.getInstantiationConstant(q, i) << " ";
285 : : }
286 [ - - ]: 0 : Trace("fmf-exh-inst-debug") << std::endl;
287 : : }
288 : 170 : QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
289 : : //create a rep set iterator and iterate over the (relevant) domain of the quantifier
290 : 170 : QRepBoundExt qrbe(d_env, qbi, d_qstate, d_treg, q);
291 : 170 : RepSetIterator riter(fm->getRepSet(), &qrbe);
292 [ + - ]: 170 : if (riter.setQuantifier(q))
293 : : {
294 [ + - ]: 170 : Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
295 [ + + ]: 170 : if( !riter.isIncomplete() ){
296 : 72 : int triedLemmas = 0;
297 : 72 : int addedLemmas = 0;
298 : 72 : Instantiate* inst = d_qim.getInstantiate();
299 : 72 : while (
300 : 278 : !riter.isFinished()
301 [ + + ][ + + ]: 278 : && (addedLemmas == 0 || !options().quantifiers.fmfOneInstPerRound))
[ + - ][ + + ]
302 : : {
303 : : // instantiation was not shown to be true, construct the term vector
304 : 206 : std::vector<Node> terms;
305 : 206 : riter.getCurrentTerms(terms);
306 [ + - ]: 412 : Trace("fmf-model-eval")
307 : 206 : << "* Add instantiation " << terms << std::endl;
308 : 206 : triedLemmas++;
309 : : //add as instantiation
310 : 206 : inst->processInstantiationRep(q, terms);
311 : 206 : if (inst->addInstantiation(q,
312 : : terms,
313 : : InferenceId::QUANTIFIERS_INST_FMF_EXH,
314 [ + + ]: 412 : Node::null()))
315 : : {
316 : 172 : addedLemmas++;
317 [ - + ]: 172 : if (d_qstate.isInConflict())
318 : : {
319 : 0 : break;
320 : : }
321 : : }else{
322 [ + - ]: 68 : Trace("fmf-model-eval")
323 : 34 : << "* Failed Add instantiation " << terms << std::endl;
324 : : }
325 : 206 : riter.increment();
326 [ + - ]: 206 : }
327 : 72 : d_addedLemmas += addedLemmas;
328 : 72 : d_triedLemmas += triedLemmas;
329 : : }
330 : : }
331 : : else
332 : : {
333 [ - - ]: 0 : Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
334 : : }
335 : : //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
336 [ + + ]: 170 : if (riter.isIncomplete())
337 : : {
338 : 106 : d_incompleteQuants.insert(q);
339 : : }
340 : 170 : }
341 : 14149 : }
342 : :
343 : 0 : void ModelEngine::debugPrint( const char* c ){
344 [ - - ]: 0 : if (TraceIsOn(c))
345 : : {
346 [ - - ]: 0 : Trace(c) << "Quantifiers: " << std::endl;
347 : 0 : FirstOrderModel* m = d_treg.getModel();
348 [ - - ]: 0 : for (size_t i = 0, nquant = m->getNumAssertedQuantifiers(); i < nquant; i++)
349 : : {
350 : 0 : Node q = m->getAssertedQuantifier(i);
351 [ - - ]: 0 : if (d_qreg.hasOwnership(q, this))
352 : : {
353 [ - - ]: 0 : Trace(c) << " ";
354 [ - - ]: 0 : if (!m->isQuantifierActive(q))
355 : : {
356 [ - - ]: 0 : Trace(c) << "*Inactive* ";
357 : : }
358 : : else
359 : : {
360 [ - - ]: 0 : Trace(c) << " ";
361 : : }
362 [ - - ]: 0 : Trace(c) << q << std::endl;
363 : : }
364 : 0 : }
365 : : }
366 : 0 : }
367 : :
368 : 26951 : bool ModelEngine::shouldProcess(Node q)
369 : : {
370 [ + + ]: 26951 : if (!d_qreg.hasOwnership(q, this))
371 : : {
372 : : // if we don't have ownership, another module has taken responsibility
373 : : // for processing q.
374 : 7881 : return false;
375 : : }
376 : : // if finite model finding or fmf bound is on, we process everything
377 [ + + ][ + + ]: 19070 : if (options().quantifiers.finiteModelFind || options().quantifiers.fmfBound)
[ + + ]
378 : : {
379 : 11824 : return true;
380 : : }
381 : : // otherwise, we are only using model-based instantiation for internally
382 : : // generated bounded quantified formulas
383 : 7246 : QuantAttributes& qattr = d_qreg.getQuantAttributes();
384 : 7246 : return qattr.isQuantBounded(q);
385 : : }
386 : :
387 : : } // namespace quantifiers
388 : : } // namespace theory
389 : : } // namespace cvc5::internal
|
