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