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 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : :
16 : : #include "theory/arith/nl/nonlinear_extension.h"
17 : :
18 : : #include "options/arith_options.h"
19 : : #include "options/smt_options.h"
20 : : #include "theory/arith/arith_utilities.h"
21 : : #include "theory/arith/bound_inference.h"
22 : : #include "theory/arith/inference_manager.h"
23 : : #include "theory/arith/nl/nl_lemma_utils.h"
24 : : #include "theory/arith/theory_arith.h"
25 : : #include "theory/ext_theory.h"
26 : : #include "theory/rewriter.h"
27 : : #include "theory/theory_model.h"
28 : : #include "util/rational.h"
29 : :
30 : : using namespace cvc5::internal::kind;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace arith {
35 : : namespace nl {
36 : :
37 : 33863 : NonlinearExtension::NonlinearExtension(Env& env, TheoryArith& containing)
38 : : : EnvObj(env),
39 : 33863 : d_containing(containing),
40 : 33863 : d_astate(*containing.getTheoryState()),
41 : 33863 : d_im(containing.getInferenceManager()),
42 : 33863 : d_stats(statisticsRegistry()),
43 : 33863 : d_hasNlTerms(context(), false),
44 : 33863 : d_checkCounter(0),
45 : 33863 : d_extTheoryCb(d_astate.getEqualityEngine()),
46 : 33863 : d_extTheory(env, d_extTheoryCb, d_im),
47 : 33863 : d_model(env),
48 : 33863 : d_trSlv(d_env, d_astate, d_im, d_model),
49 : 33863 : d_extState(d_env, d_im, d_model),
50 : 33863 : d_factoringSlv(d_env, &d_extState),
51 : 33863 : d_monomialBoundsSlv(d_env, &d_extState),
52 : 33863 : d_monomialSlv(d_env, &d_extState),
53 : 33863 : d_fmSlv(d_env, d_astate, d_im),
54 : 33863 : d_splitZeroSlv(d_env, &d_extState),
55 : 33863 : d_tangentPlaneSlv(d_env, &d_extState),
56 : 33863 : d_covSlv(d_env, d_im, d_model),
57 : 33863 : d_icpSlv(d_env, d_im),
58 : 33863 : d_iandSlv(env, d_im, d_model),
59 : 33863 : d_piandSlv(env, d_im, d_model),
60 : 67726 : d_pow2Slv(env, d_im, d_model)
61 : : {
62 : 33863 : d_extTheory.addFunctionKind(Kind::NONLINEAR_MULT);
63 : 33863 : d_extTheory.addFunctionKind(Kind::EXPONENTIAL);
64 : 33863 : d_extTheory.addFunctionKind(Kind::SINE);
65 : 33863 : d_extTheory.addFunctionKind(Kind::PI);
66 : 33863 : d_extTheory.addFunctionKind(Kind::IAND);
67 : 33863 : d_extTheory.addFunctionKind(Kind::PIAND);
68 : 33863 : d_extTheory.addFunctionKind(Kind::POW2);
69 : 33863 : d_true = nodeManager()->mkConst(true);
70 : 33863 : }
71 : :
72 : 67152 : NonlinearExtension::~NonlinearExtension() {}
73 : :
74 : 1003489 : void NonlinearExtension::preRegisterTerm(TNode n)
75 : : {
76 : : // register terms with extended theory, to find extended terms that can be
77 : : // eliminated by context-depedendent simplification.
78 [ + + ]: 1003489 : if (d_extTheory.hasFunctionKind(n.getKind()))
79 : : {
80 : 11960 : d_hasNlTerms = true;
81 : 11960 : d_extTheory.registerTerm(n);
82 : : }
83 : 1003489 : }
84 : :
85 : 0 : void NonlinearExtension::processSideEffect(const NlLemma& se)
86 : : {
87 : 0 : d_trSlv.processSideEffect(se);
88 : 0 : }
89 : :
90 : 0 : void NonlinearExtension::computeRelevantAssertions(
91 : : const std::vector<Node>& assertions, std::vector<Node>& keep)
92 : : {
93 : 0 : const Valuation& v = d_containing.getValuation();
94 [ - - ]: 0 : for (const Node& a : assertions)
95 : : {
96 [ - - ]: 0 : if (v.isRelevant(a))
97 : : {
98 : 0 : keep.emplace_back(a);
99 : : }
100 : : }
101 [ - - ]: 0 : Trace("nl-ext-rlv") << "...relevant assertions: " << keep.size() << "/"
102 : 0 : << assertions.size() << std::endl;
103 : 0 : }
104 : :
105 : 13527 : void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
106 : : {
107 [ + - ]: 13527 : Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl;
108 : 13527 : bool useRelevance = false;
109 [ - + ]: 13527 : if (options().arith.nlRlvMode == options::NlRlvMode::INTERLEAVE)
110 : : {
111 : 0 : useRelevance = (d_checkCounter % 2);
112 : : }
113 [ + + ]: 13527 : else if (options().arith.nlRlvMode == options::NlRlvMode::ALWAYS)
114 : : {
115 : 114 : useRelevance = true;
116 : : }
117 : 13527 : Valuation v = d_containing.getValuation();
118 : :
119 : 13527 : BoundInference bounds(d_env);
120 : :
121 : 13527 : std::unordered_set<Node> init_assertions;
122 : :
123 : 13527 : for (Theory::assertions_iterator it = d_containing.facts_begin();
124 [ + + ]: 1171816 : it != d_containing.facts_end();
125 : 1158289 : ++it)
126 : : {
127 : 1158289 : const Assertion& assertion = *it;
128 [ + - ]: 2316578 : Trace("nl-ext-assert-debug")
129 : 1158289 : << "Loaded " << assertion.d_assertion << " from theory" << std::endl;
130 : 1158289 : Node lit = assertion.d_assertion;
131 [ + + ][ + + ]: 1158289 : if (useRelevance && !v.isRelevant(lit))
[ + + ][ + + ]
[ - - ]
132 : : {
133 : : // not relevant, skip
134 : 1464 : continue;
135 : : }
136 : : // if using the bound inference utility
137 [ + + ][ + + ]: 1156825 : if (options().arith.nlRlvAssertBounds && bounds.add(lit, false))
[ + + ]
138 : : {
139 : 542100 : continue;
140 : : }
141 : 614725 : init_assertions.insert(lit);
142 [ + + ]: 1158289 : }
143 : :
144 [ + + ]: 289860 : for (const auto& vb : bounds.get())
145 : : {
146 : 276333 : const Bounds& b = vb.second;
147 [ + + ]: 276333 : if (!b.lower_bound.isNull())
148 : : {
149 : 188382 : init_assertions.insert(b.lower_bound);
150 : : }
151 [ + + ]: 276333 : if (!b.upper_bound.isNull())
152 : : {
153 : 143581 : init_assertions.insert(b.upper_bound);
154 : : }
155 : : }
156 : :
157 : : // Try to be "more deterministic" by adding assertions in the order they were
158 : : // given
159 [ + + ]: 1171816 : for (auto it = d_containing.facts_begin(); it != d_containing.facts_end();
160 : 1158289 : ++it)
161 : : {
162 : 1158289 : Node lit = (*it).d_assertion;
163 : 1158289 : auto iait = init_assertions.find(lit);
164 [ + + ]: 1158289 : if (iait != init_assertions.end())
165 : : {
166 [ + - ]: 892180 : Trace("nl-ext-assert-debug") << "Adding " << lit << std::endl;
167 : 892180 : assertions.push_back(lit);
168 : 892180 : init_assertions.erase(iait);
169 : : }
170 : 1158289 : }
171 : : // Now add left over assertions that have been newly created within this
172 : : // function by the code above.
173 [ + + ]: 18217 : for (const Node& a : init_assertions)
174 : : {
175 [ + - ]: 4690 : Trace("nl-ext-assert-debug") << "Adding " << a << std::endl;
176 : 4690 : assertions.push_back(a);
177 : : }
178 [ + - ]: 27054 : Trace("nl-ext") << "...keep " << assertions.size() << " / "
179 : 13527 : << d_containing.numAssertions() << " assertions."
180 : 13527 : << std::endl;
181 : 13527 : }
182 : :
183 : 13527 : std::vector<Node> NonlinearExtension::getUnsatisfiedAssertions(
184 : : const std::vector<Node>& assertions)
185 : : {
186 : 13527 : std::vector<Node> false_asserts;
187 [ + + ]: 910397 : for (const auto& lit : assertions)
188 : : {
189 : 896870 : Node litv = d_model.computeConcreteModelValue(lit);
190 [ + - ]: 896870 : Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv;
191 [ + + ]: 896870 : if (litv != d_true)
192 : : {
193 [ + - ]: 73123 : Trace("nl-ext-mv-assert") << " [model-false]";
194 : 73123 : false_asserts.push_back(lit);
195 : : }
196 [ + - ]: 896870 : Trace("nl-ext-mv-assert") << std::endl;
197 : 896870 : }
198 : 13527 : return false_asserts;
199 : 0 : }
200 : :
201 : 900 : bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
202 : : {
203 [ + - ]: 900 : Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
204 : :
205 : : // get the presubstitution
206 [ + - ]: 900 : Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl;
207 : : // Notice that we do not consider relevance here, since assertions were
208 : : // already filtered based on relevance. It is incorrect to filter based on
209 : : // relevance here, since we may have discarded literals that are relevant
210 : : // that are entailed based on the techniques in getAssertions.
211 : 900 : std::vector<Node> passertions = assertions;
212 [ + + ]: 900 : if (options().arith.nlExt == options::NlExtMode::FULL)
213 : : {
214 : : // preprocess the assertions with the trancendental solver
215 [ - + ]: 802 : if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
216 : : {
217 : 0 : return false;
218 : : }
219 : : }
220 [ + + ]: 900 : if (options().arith.nlCov)
221 : : {
222 : 128 : d_covSlv.constructModelIfAvailable(passertions);
223 : : }
224 : :
225 [ + - ]: 900 : Trace("nl-ext-cm") << "-----" << std::endl;
226 : 900 : unsigned tdegree = d_trSlv.getTaylorDegree();
227 : 900 : std::vector<NlLemma> lemmas;
228 : 900 : bool ret = d_model.checkModel(passertions, tdegree, lemmas);
229 [ - + ]: 900 : for (const auto& al : lemmas)
230 : : {
231 : 0 : d_im.addPendingLemma(al);
232 : : }
233 : 900 : return ret;
234 : 900 : }
235 : :
236 : 83761 : void NonlinearExtension::checkFullEffort(std::map<Node, Node>& arithModel,
237 : : const std::set<Node>& termSet)
238 : : {
239 [ + - ]: 83761 : Trace("nl-ext") << "NonlinearExtension::checkFullEffort" << std::endl;
240 [ - + ]: 83761 : if (TraceIsOn("nl-arith-model"))
241 : : {
242 [ - - ]: 0 : Trace("nl-arith-model") << " arith model is:" << std::endl;
243 [ - - ]: 0 : for (std::pair<const Node, Node>& m : arithModel)
244 : : {
245 [ - - ]: 0 : Trace("nl-arith-model")
246 : 0 : << " " << m.first << " -> " << m.second << ", rep "
247 : 0 : << d_astate.getRepresentative(m.first) << std::endl;
248 : : }
249 : : }
250 : :
251 [ + - ]: 83761 : if (options().arith.nlExtRewrites)
252 : : {
253 : 83761 : std::vector<Node> nred;
254 [ + + ]: 83761 : if (!d_extTheory.doInferences(0, nred))
255 : : {
256 [ + - ]: 163898 : Trace("nl-ext") << "...sent no lemmas, # extf to reduce = " << nred.size()
257 : 81949 : << std::endl;
258 : : // note that even if the extended theory thinks there are no terms left
259 : : // to reduce (nred.empty()), we still have to check with the non-linear
260 : : // extension, since the substitutions ExtTheory uses come from the
261 : : // equality engine, which may disagree with the arithmetic model
262 : : // (arithModel), since the equality engine does congruence over extended
263 : : // operators, and the linear solver does not take this into account.
264 : : }
265 : : else
266 : : {
267 [ + - ]: 1812 : Trace("nl-ext") << "...sent lemmas." << std::endl;
268 : : }
269 : 83761 : }
270 : :
271 [ + + ]: 83761 : if (!hasNlTerms())
272 : : {
273 : : // no non-linear constraints, we are done
274 : 70234 : return;
275 : : }
276 [ + - ]: 13527 : Trace("nl-ext-mv") << "Shared terms : " << std::endl;
277 : : // For the purposes of ensuring we do not introduce inconsistencies for
278 : : // theory combination, we first record the model values for all shared
279 : : // terms, if they exist.
280 : 13527 : const context::CDList<TNode>& sts = d_astate.getSharedTerms();
281 : : // Reset the model now, as it is used to compute model values for shared
282 : : // terms in the loop below.
283 : 13527 : d_model.reset(arithModel);
284 : : // A mapping from shared terms to their model value, prior to
285 : : // processing the model below.
286 : 13527 : std::unordered_map<TNode, Node> revSharedTermsPre;
287 [ + + ]: 105116 : for (TNode st : sts)
288 : : {
289 : 91589 : Node stv = d_model.computeAbstractModelValue(st);
290 [ + - ]: 183178 : Trace("nl-model-final")
291 : 91589 : << "- shared term value " << st << " = " << stv << std::endl;
292 : 91589 : revSharedTermsPre[st] = stv;
293 : 91589 : }
294 [ - + ]: 13527 : if (TraceIsOn("nl-model-final"))
295 : : {
296 [ - - ]: 0 : Trace("nl-model-final") << "MODEL INPUT:" << std::endl;
297 [ - - ]: 0 : for (std::pair<const Node, Node>& m : arithModel)
298 : : {
299 [ - - ]: 0 : Trace("nl-model-final")
300 : 0 : << " " << m.first << " -> " << m.second << std::endl;
301 : : }
302 [ - - ]: 0 : Trace("nl-model-final") << "END" << std::endl;
303 : : }
304 [ + - ]: 13527 : Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl;
305 : : // run a last call effort check
306 [ + - ]: 13527 : Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
307 : 13527 : Result::Status res = modelBasedRefinement(termSet);
308 [ + + ]: 13527 : if (res == Result::SAT)
309 : : {
310 [ + - ]: 1463 : Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
311 : : // modify the model values
312 : 1463 : d_model.getModelValueRepair(arithModel);
313 : : }
314 : : // must post-process model with transcendental solver, to ensure we don't
315 : : // assign values for equivalence classes with transcendental function
316 : : // applications
317 : 13527 : d_trSlv.postProcessModel(arithModel, termSet);
318 [ - + ]: 13527 : if (TraceIsOn("nl-model-final"))
319 : : {
320 [ - - ]: 0 : Trace("nl-model-final") << "MODEL OUTPUT:" << std::endl;
321 [ - - ]: 0 : for (std::pair<const Node, Node>& m : arithModel)
322 : : {
323 [ - - ]: 0 : Trace("nl-model-final")
324 : 0 : << " " << m.first << " -> " << m.second << std::endl;
325 : : }
326 [ - - ]: 0 : Trace("nl-model-final") << "END" << std::endl;
327 : : }
328 [ + + ]: 13527 : if (res == Result::SAT)
329 : : {
330 : 1463 : d_model.reset(arithModel);
331 : : // Go back and see if we made two shared terms equal that were disequal
332 : : // prior to modifying the model. If we did so for two terms t and s, then we
333 : : // must split on t = s.
334 : 1463 : std::unordered_map<TNode, std::vector<Node>> sharedTermsPost;
335 : 1463 : std::unordered_set<Node> factorsSplit;
336 [ + + ]: 16550 : for (TNode st : sts)
337 : : {
338 : 15087 : Node stv = d_model.computeAbstractModelValue(st);
339 [ + - ]: 30174 : Trace("nl-model-final")
340 : 15087 : << "- shared term value (post) " << st << " = " << stv << std::endl;
341 : 15087 : sharedTermsPost[stv].emplace_back(st);
342 : : // Corner case: if a multiplication term, need to ensure that each of
343 : : // our variables are assigned in the model. If not, to force this to be
344 : : // the case, we split on that variable and zero.
345 [ + + ]: 15087 : if (st.getKind() == Kind::NONLINEAR_MULT)
346 : : {
347 [ + + ]: 1476 : for (const Node& stf : st)
348 : : {
349 : 984 : if (arithModel.find(stf) == arithModel.end()
350 [ + + ][ + + ]: 984 : && factorsSplit.insert(stf).second)
[ + + ]
351 : : {
352 [ + - ]: 8 : Trace("nl-model-final") << "*** Identified multiplication term "
353 : 0 : "with factor that is not preregistered: "
354 : 4 : << st << " " << stf << std::endl;
355 : : Node zero =
356 : 8 : nodeManager()->mkConstRealOrInt(stf.getType(), Rational(0));
357 : 4 : Node eq = stf.eqNode(zero);
358 : 4 : Node split = eq.orNode(eq.negate());
359 : 4 : NlLemma nlem(InferenceId::ARITH_NL_SHARED_TERM_FACTOR_SPLIT, split);
360 : 4 : d_im.addPendingLemma(nlem);
361 : 4 : }
362 : 984 : }
363 : : }
364 : 15087 : }
365 : 1463 : std::unordered_map<TNode, Node>::iterator itrs;
366 [ + + ]: 4761 : for (const std::pair<const TNode, std::vector<Node>>& stp : sharedTermsPost)
367 : : {
368 : 3298 : Node cv;
369 [ + + ]: 18385 : for (TNode st : stp.second)
370 : : {
371 : 15087 : itrs = revSharedTermsPre.find(st);
372 [ - + ][ - + ]: 15087 : Assert(itrs != revSharedTermsPre.end());
[ - - ]
373 : 15087 : Node stv = itrs->second;
374 [ + + ]: 15087 : if (cv.isNull())
375 : : {
376 : 3298 : cv = stv;
377 : : }
378 [ + + ]: 11789 : else if (stv != cv)
379 : : {
380 [ + - ]: 146 : Trace("nl-model-final")
381 : 0 : << "*** Identified two shared terms that were disequal: " << st
382 : 73 : << " " << stp.second[0] << std::endl;
383 : 73 : Node eq = st.eqNode(stp.second[0]);
384 : 73 : Node split = eq.orNode(eq.negate());
385 : 73 : NlLemma nlem(InferenceId::ARITH_NL_SHARED_TERM_SPLIT, split);
386 : 73 : d_im.addPendingLemma(nlem);
387 : 73 : }
388 : 15087 : }
389 : 3298 : }
390 : 1463 : }
391 : 13527 : }
392 : :
393 : 13527 : Result::Status NonlinearExtension::modelBasedRefinement(
394 : : const std::set<Node>& termSet)
395 : : {
396 : 13527 : ++(d_stats.d_mbrRuns);
397 : 13527 : d_checkCounter++;
398 : :
399 : : // get the assertions
400 : 13527 : std::vector<Node> assertions;
401 : 13527 : getAssertions(assertions);
402 : :
403 [ + - ]: 27054 : Trace("nl-ext-mv-assert")
404 : 13527 : << "Getting model values... check for [model-false]" << std::endl;
405 : : // get the assertions that are false in the model
406 : 13527 : const std::vector<Node> false_asserts = getUnsatisfiedAssertions(assertions);
407 [ + - ]: 13527 : Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl;
408 : :
409 : : // get the extended terms belonging to this theory
410 : 13527 : std::vector<Node> xtsAll;
411 : 13527 : d_extTheory.getTerms(xtsAll);
412 : : // only consider those that are currently relevant based on the current
413 : : // assertions, i.e. those contained in termSet
414 : 13527 : std::vector<Node> xts;
415 [ + + ]: 86648 : for (const Node& x : xtsAll)
416 : : {
417 [ + + ]: 73121 : if (termSet.find(x) != termSet.end())
418 : : {
419 : 68765 : xts.push_back(x);
420 : : }
421 : : }
422 : :
423 [ - + ]: 13527 : if (TraceIsOn("nl-ext-debug"))
424 : : {
425 [ - - ]: 0 : Trace("nl-ext-debug") << " processing NonlinearExtension::check : "
426 : 0 : << std::endl;
427 [ - - ]: 0 : Trace("nl-ext-debug") << " " << false_asserts.size()
428 : 0 : << " false assertions" << std::endl;
429 [ - - ]: 0 : Trace("nl-ext-debug") << " " << xts.size()
430 : 0 : << " extended terms: " << std::endl;
431 [ - - ]: 0 : Trace("nl-ext-debug") << " ";
432 [ - - ]: 0 : for (unsigned j = 0; j < xts.size(); j++)
433 : : {
434 [ - - ]: 0 : Trace("nl-ext-debug") << xts[j] << " ";
435 : : }
436 [ - - ]: 0 : Trace("nl-ext-debug") << std::endl;
437 : : }
438 : :
439 : : // compute whether shared terms have correct values
440 : : bool needsRecheck;
441 [ + + ]: 1521 : do
442 : : {
443 : 13585 : d_model.resetCheck();
444 : 13585 : needsRecheck = false;
445 : : // complete_status:
446 : : // 1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
447 : 13585 : int complete_status = 1;
448 : : // We require a check either if an assertion is false or a shared term has
449 : : // a wrong value
450 [ + + ]: 13585 : if (!false_asserts.empty())
451 : : {
452 : 12364 : complete_status = 0;
453 : 12364 : runStrategy(assertions, false_asserts, xts);
454 [ + + ][ + + ]: 12364 : if (d_im.hasSentLemma() || d_im.hasPendingLemma())
[ + + ]
455 : : {
456 : 11464 : d_im.clearWaitingLemmas();
457 : 12064 : return Result::UNSAT;
458 : : }
459 : : }
460 [ + - ]: 4242 : Trace("nl-ext") << "Finished check with status : " << complete_status
461 : 2121 : << std::endl;
462 : :
463 : : // if we did not add a lemma during check and there is a chance for SAT
464 [ + + ]: 2121 : if (complete_status == 0)
465 : : {
466 [ + - ]: 1800 : Trace("nl-ext")
467 : 0 : << "Check model based on bounds for irrational-valued functions..."
468 : 900 : << std::endl;
469 : : // check the model based on simple solving of equalities and using
470 : : // error bounds on the Taylor approximation of transcendental functions.
471 [ + + ]: 900 : if (checkModel(assertions))
472 : : {
473 : 242 : complete_status = 1;
474 : : }
475 [ - + ]: 900 : if (d_im.hasUsed())
476 : : {
477 : 0 : d_im.clearWaitingLemmas();
478 : 0 : return Result::UNSAT;
479 : : }
480 : : }
481 : :
482 : : // if we have not concluded SAT
483 [ + + ]: 2121 : if (complete_status != 1)
484 : : {
485 : : // flush the waiting lemmas
486 [ + + ]: 658 : if (d_im.hasWaitingLemma())
487 : : {
488 : 593 : std::size_t count = d_im.numWaitingLemmas();
489 : 593 : d_im.flushWaitingLemmas();
490 [ + - ]: 1186 : Trace("nl-ext") << "...added " << count << " waiting lemmas."
491 : 593 : << std::endl;
492 : 593 : return Result::UNSAT;
493 : : }
494 : :
495 : : // we are incomplete
496 : 65 : if (options().arith.nlExt == options::NlExtMode::FULL
497 [ + - ][ + - ]: 65 : && options().arith.nlExtIncPrecision && d_model.usedApproximate())
[ + + ][ + + ]
498 : : {
499 : 58 : d_trSlv.incrementTaylorDegree();
500 : 58 : needsRecheck = true;
501 : : // increase precision for PI?
502 : : // Difficult since Taylor series is very slow to converge
503 [ + - ]: 116 : Trace("nl-ext") << "...increment Taylor degree to "
504 : 58 : << d_trSlv.getTaylorDegree() << std::endl;
505 : : }
506 : : else
507 : : {
508 [ + - ]: 14 : Trace("nl-ext") << "...failed to send lemma in "
509 : 0 : "NonLinearExtension, set incomplete"
510 : 7 : << std::endl;
511 : 7 : d_containing.getOutputChannel().setModelUnsound(IncompleteId::ARITH_NL);
512 : 7 : return Result::UNKNOWN;
513 : : }
514 : : }
515 : 1521 : d_im.clearWaitingLemmas();
516 : : } while (needsRecheck);
517 : :
518 : : // did not add lemmas
519 : 1463 : return Result::SAT;
520 : 13527 : }
521 : :
522 : 12364 : void NonlinearExtension::runStrategy(const std::vector<Node>& assertions,
523 : : const std::vector<Node>& false_asserts,
524 : : const std::vector<Node>& xts)
525 : : {
526 : 12364 : ++(d_stats.d_checkRuns);
527 : :
528 [ - + ]: 12364 : if (TraceIsOn("nl-strategy"))
529 : : {
530 [ - - ]: 0 : for (const auto& a : assertions)
531 : : {
532 [ - - ]: 0 : Trace("nl-strategy") << "Input assertion: " << a << std::endl;
533 : : }
534 : : }
535 [ + + ]: 12364 : if (!d_strategy.isStrategyInit())
536 : : {
537 : 1687 : d_strategy.initializeStrategy(options());
538 : : }
539 : :
540 : 12364 : auto steps = d_strategy.getStrategy();
541 : 12364 : bool stop = false;
542 [ + + ][ + + ]: 285289 : while (!stop && steps.hasNext())
[ + + ]
543 : : {
544 : 272925 : InferStep step = steps.next();
545 [ + - ]: 272925 : Trace("nl-strategy") << "Step " << step << std::endl;
546 [ + + ][ + + ]: 272925 : switch (step)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ - + ]
[ - + ][ + + ]
[ + + ][ - ]
547 : : {
548 : 119138 : case InferStep::BREAK: stop = d_im.hasPendingLemma(); break;
549 : 1898 : case InferStep::FLUSH_WAITING_LEMMAS: d_im.flushWaitingLemmas(); break;
550 : 272 : case InferStep::COVERINGS_FULL: d_covSlv.checkFull(); break;
551 : 284 : case InferStep::COVERINGS_INIT: d_covSlv.initLastCall(assertions); break;
552 : 962 : case InferStep::NL_FACTORING:
553 : 962 : d_factoringSlv.check(assertions, false_asserts);
554 : 962 : break;
555 : 11372 : case InferStep::IAND_INIT: d_iandSlv.initLastCall(xts); break;
556 : 2182 : case InferStep::IAND_FULL: d_iandSlv.checkFullRefine(); break;
557 : 11372 : case InferStep::IAND_INITIAL: d_iandSlv.checkInitialRefine(); break;
558 : 11256 : case InferStep::PIAND_INIT: d_piandSlv.initLastCall(xts); break;
559 : 2182 : case InferStep::PIAND_FULL: d_piandSlv.checkFullRefine(); break;
560 : 11256 : case InferStep::PIAND_INITIAL: d_piandSlv.checkInitialRefine(); break;
561 : 11207 : case InferStep::POW2_INIT: d_pow2Slv.initLastCall(xts); break;
562 : 2182 : case InferStep::POW2_FULL: d_pow2Slv.checkFullRefine(); break;
563 : 11207 : case InferStep::POW2_INITIAL: d_pow2Slv.checkInitialRefine(); break;
564 : 10 : case InferStep::ICP:
565 : 10 : d_icpSlv.reset(assertions);
566 : 10 : d_icpSlv.check();
567 : 10 : break;
568 : 12350 : case InferStep::NL_INIT:
569 : 12350 : d_extState.init(xts);
570 : 12350 : d_monomialBoundsSlv.init();
571 : 12350 : d_monomialSlv.init(xts);
572 : 12350 : break;
573 : 5227 : case InferStep::NL_FLATTEN_MON:
574 : : {
575 : 5227 : std::vector<Node>& mvec = d_extState.d_ms_vars;
576 : 5227 : d_fmSlv.check(mvec);
577 : : }
578 : 5227 : break;
579 : 2779 : case InferStep::NL_MONOMIAL_INFER_BOUNDS:
580 : 2779 : d_monomialBoundsSlv.checkBounds(assertions, false_asserts);
581 : 2779 : break;
582 : 7235 : case InferStep::NL_MONOMIAL_MAGNITUDE0:
583 : 7235 : d_monomialSlv.checkMagnitude(0);
584 : 7235 : break;
585 : 4874 : case InferStep::NL_MONOMIAL_MAGNITUDE1:
586 : 4874 : d_monomialSlv.checkMagnitude(1);
587 : 4874 : break;
588 : 3454 : case InferStep::NL_MONOMIAL_MAGNITUDE2:
589 : 3454 : d_monomialSlv.checkMagnitude(2);
590 : 3454 : break;
591 : 11061 : case InferStep::NL_MONOMIAL_SIGN: d_monomialSlv.checkSign(); break;
592 : 0 : case InferStep::NL_RESOLUTION_BOUNDS:
593 : 0 : d_monomialBoundsSlv.checkResBounds();
594 : 0 : break;
595 : 6 : case InferStep::NL_SPLIT_ZERO: d_splitZeroSlv.check(); break;
596 : 0 : case InferStep::NL_TANGENT_PLANES: d_tangentPlaneSlv.check(false); break;
597 : 814 : case InferStep::NL_TANGENT_PLANES_WAITING:
598 : 814 : d_tangentPlaneSlv.check(true);
599 : 814 : break;
600 : 11652 : case InferStep::TRANS_INIT: d_trSlv.initLastCall(xts); break;
601 : 10944 : case InferStep::TRANS_INITIAL:
602 : 10944 : d_trSlv.checkTranscendentalInitialRefine();
603 : 10944 : break;
604 : 4935 : case InferStep::TRANS_MONOTONIC:
605 : 4935 : d_trSlv.checkTranscendentalMonotonic();
606 : 4935 : break;
607 : 814 : case InferStep::TRANS_TANGENT_PLANES:
608 : 814 : d_trSlv.checkTranscendentalTangentPlanes();
609 : 814 : break;
610 : 0 : default: break;
611 : : }
612 : : }
613 : :
614 [ + - ]: 12364 : Trace("nl-ext") << "finished strategy" << std::endl;
615 [ + - ]: 24728 : Trace("nl-ext") << " ...finished with " << d_im.numWaitingLemmas()
616 : 12364 : << " waiting lemmas." << std::endl;
617 [ + - ]: 24728 : Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas()
618 : 12364 : << " pending lemmas." << std::endl;
619 : 12364 : }
620 : :
621 : : } // namespace nl
622 : : } // namespace arith
623 : : } // namespace theory
624 : : } // namespace cvc5::internal
|
