1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* [[ Add one-line brief description here ]] |
14 |
|
* |
15 |
|
* [[ Add lengthier description here ]] |
16 |
|
* \todo document this file |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "theory/arith/nl/nonlinear_extension.h" |
20 |
|
|
21 |
|
#include "options/arith_options.h" |
22 |
|
#include "options/smt_options.h" |
23 |
|
#include "theory/arith/arith_state.h" |
24 |
|
#include "theory/arith/bound_inference.h" |
25 |
|
#include "theory/arith/inference_manager.h" |
26 |
|
#include "theory/arith/nl/nl_lemma_utils.h" |
27 |
|
#include "theory/arith/theory_arith.h" |
28 |
|
#include "theory/ext_theory.h" |
29 |
|
#include "theory/rewriter.h" |
30 |
|
#include "theory/theory_model.h" |
31 |
|
#include "util/rational.h" |
32 |
|
|
33 |
|
using namespace cvc5::kind; |
34 |
|
|
35 |
|
namespace cvc5 { |
36 |
|
namespace theory { |
37 |
|
namespace arith { |
38 |
|
namespace nl { |
39 |
|
|
40 |
3429 |
NonlinearExtension::NonlinearExtension(Env& env, |
41 |
|
TheoryArith& containing, |
42 |
3429 |
ArithState& state) |
43 |
|
: EnvObj(env), |
44 |
|
d_containing(containing), |
45 |
|
d_astate(state), |
46 |
3429 |
d_im(containing.getInferenceManager()), |
47 |
|
d_hasNlTerms(false), |
48 |
|
d_checkCounter(0), |
49 |
|
d_extTheoryCb(state.getEqualityEngine()), |
50 |
3429 |
d_extTheory(d_extTheoryCb, context(), userContext(), d_im), |
51 |
|
d_model(), |
52 |
|
d_trSlv(d_im, d_model, d_env), |
53 |
|
d_extState(d_im, d_model, d_env), |
54 |
|
d_factoringSlv(&d_extState), |
55 |
|
d_monomialBoundsSlv(&d_extState), |
56 |
|
d_monomialSlv(&d_extState), |
57 |
|
d_splitZeroSlv(&d_extState), |
58 |
|
d_tangentPlaneSlv(&d_extState), |
59 |
|
d_cadSlv(d_env, d_im, d_model), |
60 |
|
d_icpSlv(d_im), |
61 |
|
d_iandSlv(env, d_im, state, d_model), |
62 |
10287 |
d_pow2Slv(env, d_im, state, d_model) |
63 |
|
{ |
64 |
3429 |
d_extTheory.addFunctionKind(kind::NONLINEAR_MULT); |
65 |
3429 |
d_extTheory.addFunctionKind(kind::EXPONENTIAL); |
66 |
3429 |
d_extTheory.addFunctionKind(kind::SINE); |
67 |
3429 |
d_extTheory.addFunctionKind(kind::PI); |
68 |
3429 |
d_extTheory.addFunctionKind(kind::IAND); |
69 |
3429 |
d_extTheory.addFunctionKind(kind::POW2); |
70 |
3429 |
d_true = NodeManager::currentNM()->mkConst(true); |
71 |
3429 |
d_zero = NodeManager::currentNM()->mkConst(Rational(0)); |
72 |
3429 |
d_one = NodeManager::currentNM()->mkConst(Rational(1)); |
73 |
3429 |
d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); |
74 |
|
|
75 |
3429 |
if (d_env.isTheoryProofProducing()) |
76 |
|
{ |
77 |
3 |
ProofChecker* pc = d_env.getProofNodeManager()->getChecker(); |
78 |
3 |
d_proofChecker.registerTo(pc); |
79 |
|
} |
80 |
3429 |
} |
81 |
|
|
82 |
6854 |
NonlinearExtension::~NonlinearExtension() {} |
83 |
|
|
84 |
212306 |
void NonlinearExtension::preRegisterTerm(TNode n) |
85 |
|
{ |
86 |
|
// register terms with extended theory, to find extended terms that can be |
87 |
|
// eliminated by context-depedendent simplification. |
88 |
212306 |
d_extTheory.registerTerm(n); |
89 |
212306 |
} |
90 |
|
|
91 |
|
void NonlinearExtension::processSideEffect(const NlLemma& se) |
92 |
|
{ |
93 |
|
d_trSlv.processSideEffect(se); |
94 |
|
} |
95 |
|
|
96 |
|
void NonlinearExtension::computeRelevantAssertions( |
97 |
|
const std::vector<Node>& assertions, std::vector<Node>& keep) |
98 |
|
{ |
99 |
|
Trace("nl-ext-rlv") << "Compute relevant assertions..." << std::endl; |
100 |
|
Valuation v = d_containing.getValuation(); |
101 |
|
for (const Node& a : assertions) |
102 |
|
{ |
103 |
|
if (v.isRelevant(a)) |
104 |
|
{ |
105 |
|
keep.push_back(a); |
106 |
|
} |
107 |
|
} |
108 |
|
Trace("nl-ext-rlv") << "...keep " << keep.size() << "/" << assertions.size() |
109 |
|
<< " assertions" << std::endl; |
110 |
|
} |
111 |
|
|
112 |
2110 |
void NonlinearExtension::getAssertions(std::vector<Node>& assertions) |
113 |
|
{ |
114 |
2110 |
Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl; |
115 |
2110 |
bool useRelevance = false; |
116 |
2110 |
if (options().arith.nlRlvMode == options::NlRlvMode::INTERLEAVE) |
117 |
|
{ |
118 |
317 |
useRelevance = (d_checkCounter % 2); |
119 |
|
} |
120 |
1793 |
else if (options().arith.nlRlvMode == options::NlRlvMode::ALWAYS) |
121 |
|
{ |
122 |
31 |
useRelevance = true; |
123 |
|
} |
124 |
2110 |
Valuation v = d_containing.getValuation(); |
125 |
|
|
126 |
4220 |
BoundInference bounds; |
127 |
|
|
128 |
4220 |
std::unordered_set<Node> init_assertions; |
129 |
|
|
130 |
229435 |
for (Theory::assertions_iterator it = d_containing.facts_begin(); |
131 |
229435 |
it != d_containing.facts_end(); |
132 |
|
++it) |
133 |
|
{ |
134 |
227325 |
const Assertion& assertion = *it; |
135 |
454650 |
Trace("nl-ext-assert-debug") |
136 |
227325 |
<< "Loaded " << assertion.d_assertion << " from theory" << std::endl; |
137 |
385970 |
Node lit = assertion.d_assertion; |
138 |
227325 |
if (useRelevance && !v.isRelevant(lit)) |
139 |
|
{ |
140 |
|
// not relevant, skip |
141 |
884 |
continue; |
142 |
|
} |
143 |
|
// if using the bound inference utility |
144 |
226441 |
if (options().arith.nlRlvAssertBounds && bounds.add(lit, false)) |
145 |
|
{ |
146 |
67796 |
continue; |
147 |
|
} |
148 |
158645 |
init_assertions.insert(lit); |
149 |
|
} |
150 |
|
|
151 |
36823 |
for (const auto& vb : bounds.get()) |
152 |
|
{ |
153 |
34713 |
const Bounds& b = vb.second; |
154 |
34713 |
if (!b.lower_bound.isNull()) |
155 |
|
{ |
156 |
23457 |
init_assertions.insert(b.lower_bound); |
157 |
|
} |
158 |
34713 |
if (!b.upper_bound.isNull()) |
159 |
|
{ |
160 |
19255 |
init_assertions.insert(b.upper_bound); |
161 |
|
} |
162 |
|
} |
163 |
|
|
164 |
|
// Try to be "more deterministic" by adding assertions in the order they were |
165 |
|
// given |
166 |
229435 |
for (auto it = d_containing.facts_begin(); it != d_containing.facts_end(); |
167 |
|
++it) |
168 |
|
{ |
169 |
454650 |
Node lit = (*it).d_assertion; |
170 |
227325 |
auto iait = init_assertions.find(lit); |
171 |
227325 |
if (iait != init_assertions.end()) |
172 |
|
{ |
173 |
194271 |
Trace("nl-ext-assert-debug") << "Adding " << lit << std::endl; |
174 |
194271 |
assertions.push_back(lit); |
175 |
194271 |
init_assertions.erase(iait); |
176 |
|
} |
177 |
|
} |
178 |
|
// Now add left over assertions that have been newly created within this |
179 |
|
// function by the code above. |
180 |
2533 |
for (const Node& a : init_assertions) |
181 |
|
{ |
182 |
423 |
Trace("nl-ext-assert-debug") << "Adding " << a << std::endl; |
183 |
423 |
assertions.push_back(a); |
184 |
|
} |
185 |
4220 |
Trace("nl-ext") << "...keep " << assertions.size() << " / " |
186 |
4220 |
<< d_containing.numAssertions() << " assertions." |
187 |
2110 |
<< std::endl; |
188 |
2110 |
} |
189 |
|
|
190 |
2110 |
std::vector<Node> NonlinearExtension::getUnsatisfiedAssertions( |
191 |
|
const std::vector<Node>& assertions) |
192 |
|
{ |
193 |
2110 |
std::vector<Node> false_asserts; |
194 |
196804 |
for (const auto& lit : assertions) |
195 |
|
{ |
196 |
389388 |
Node litv = d_model.computeConcreteModelValue(lit); |
197 |
194694 |
Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv; |
198 |
194694 |
if (litv != d_true) |
199 |
|
{ |
200 |
13265 |
Trace("nl-ext-mv-assert") << " [model-false]"; |
201 |
13265 |
false_asserts.push_back(lit); |
202 |
|
} |
203 |
194694 |
Trace("nl-ext-mv-assert") << std::endl; |
204 |
|
} |
205 |
2110 |
return false_asserts; |
206 |
|
} |
207 |
|
|
208 |
151 |
bool NonlinearExtension::checkModel(const std::vector<Node>& assertions) |
209 |
|
{ |
210 |
151 |
Trace("nl-ext-cm") << "--- check-model ---" << std::endl; |
211 |
|
|
212 |
|
// get the presubstitution |
213 |
151 |
Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; |
214 |
|
// Notice that we do not consider relevance here, since assertions were |
215 |
|
// already filtered based on relevance. It is incorrect to filter based on |
216 |
|
// relevance here, since we may have discarded literals that are relevant |
217 |
|
// that are entailed based on the techniques in getAssertions. |
218 |
302 |
std::vector<Node> passertions = assertions; |
219 |
151 |
if (options().arith.nlExt == options::NlExtMode::FULL) |
220 |
|
{ |
221 |
|
// preprocess the assertions with the trancendental solver |
222 |
135 |
if (!d_trSlv.preprocessAssertionsCheckModel(passertions)) |
223 |
|
{ |
224 |
|
return false; |
225 |
|
} |
226 |
|
} |
227 |
151 |
if (options().arith.nlCad) |
228 |
|
{ |
229 |
16 |
d_cadSlv.constructModelIfAvailable(passertions); |
230 |
|
} |
231 |
|
|
232 |
151 |
Trace("nl-ext-cm") << "-----" << std::endl; |
233 |
151 |
unsigned tdegree = d_trSlv.getTaylorDegree(); |
234 |
302 |
std::vector<NlLemma> lemmas; |
235 |
151 |
bool ret = d_model.checkModel(passertions, tdegree, lemmas); |
236 |
151 |
for (const auto& al: lemmas) |
237 |
|
{ |
238 |
|
d_im.addPendingLemma(al); |
239 |
|
} |
240 |
151 |
return ret; |
241 |
|
} |
242 |
|
|
243 |
23489 |
void NonlinearExtension::checkFullEffort(std::map<Node, Node>& arithModel, |
244 |
|
const std::set<Node>& termSet) |
245 |
|
{ |
246 |
23489 |
Trace("nl-ext") << "NonlinearExtension::checkFullEffort" << std::endl; |
247 |
|
|
248 |
23489 |
d_hasNlTerms = true; |
249 |
23489 |
if (options().arith.nlExtRewrites) |
250 |
|
{ |
251 |
46978 |
std::vector<Node> nred; |
252 |
23489 |
if (!d_extTheory.doInferences(0, nred)) |
253 |
|
{ |
254 |
46338 |
Trace("nl-ext") << "...sent no lemmas, # extf to reduce = " << nred.size() |
255 |
23169 |
<< std::endl; |
256 |
23169 |
if (nred.empty()) |
257 |
|
{ |
258 |
21379 |
d_hasNlTerms = false; |
259 |
|
} |
260 |
|
} |
261 |
|
else |
262 |
|
{ |
263 |
320 |
Trace("nl-ext") << "...sent lemmas." << std::endl; |
264 |
|
} |
265 |
|
} |
266 |
|
|
267 |
23489 |
if (!hasNlTerms()) |
268 |
|
{ |
269 |
|
// no non-linear constraints, we are done |
270 |
21379 |
return; |
271 |
|
} |
272 |
2110 |
Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl; |
273 |
2110 |
d_model.reset(d_containing.getValuation().getModel(), arithModel); |
274 |
|
// run a last call effort check |
275 |
2110 |
Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; |
276 |
2110 |
Result::Sat res = modelBasedRefinement(termSet); |
277 |
2110 |
if (res == Result::Sat::SAT) |
278 |
|
{ |
279 |
360 |
Trace("nl-ext") << "interceptModel: do model repair" << std::endl; |
280 |
360 |
d_approximations.clear(); |
281 |
360 |
d_witnesses.clear(); |
282 |
|
// modify the model values |
283 |
720 |
d_model.getModelValueRepair(arithModel, |
284 |
|
d_approximations, |
285 |
|
d_witnesses, |
286 |
360 |
options().smt.modelWitnessValue); |
287 |
|
} |
288 |
|
} |
289 |
|
|
290 |
214 |
void NonlinearExtension::finalizeModel(TheoryModel* tm) |
291 |
|
{ |
292 |
214 |
Trace("nl-ext") << "NonlinearExtension::finalizeModel" << std::endl; |
293 |
|
|
294 |
236 |
for (std::pair<const Node, std::pair<Node, Node>>& a : d_approximations) |
295 |
|
{ |
296 |
22 |
if (a.second.second.isNull()) |
297 |
|
{ |
298 |
22 |
tm->recordApproximation(a.first, a.second.first); |
299 |
|
} |
300 |
|
else |
301 |
|
{ |
302 |
|
tm->recordApproximation(a.first, a.second.first, a.second.second); |
303 |
|
} |
304 |
|
} |
305 |
221 |
for (const auto& vw : d_witnesses) |
306 |
|
{ |
307 |
7 |
tm->recordApproximation(vw.first, vw.second); |
308 |
|
} |
309 |
214 |
} |
310 |
|
|
311 |
2110 |
Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) |
312 |
|
{ |
313 |
2110 |
++(d_stats.d_mbrRuns); |
314 |
2110 |
d_checkCounter++; |
315 |
|
|
316 |
|
// get the assertions |
317 |
4220 |
std::vector<Node> assertions; |
318 |
2110 |
getAssertions(assertions); |
319 |
|
|
320 |
4220 |
Trace("nl-ext-mv-assert") |
321 |
2110 |
<< "Getting model values... check for [model-false]" << std::endl; |
322 |
|
// get the assertions that are false in the model |
323 |
4220 |
const std::vector<Node> false_asserts = getUnsatisfiedAssertions(assertions); |
324 |
2110 |
Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl; |
325 |
|
|
326 |
|
// get the extended terms belonging to this theory |
327 |
4220 |
std::vector<Node> xtsAll; |
328 |
2110 |
d_extTheory.getTerms(xtsAll); |
329 |
|
// only consider those that are currently relevant based on the current |
330 |
|
// assertions, i.e. those contained in termSet |
331 |
4220 |
std::vector<Node> xts; |
332 |
14818 |
for (const Node& x : xtsAll) |
333 |
|
{ |
334 |
12708 |
if (termSet.find(x) != termSet.end()) |
335 |
|
{ |
336 |
12281 |
xts.push_back(x); |
337 |
|
} |
338 |
|
} |
339 |
|
|
340 |
2110 |
if (Trace.isOn("nl-ext-debug")) |
341 |
|
{ |
342 |
|
Trace("nl-ext-debug") << " processing NonlinearExtension::check : " |
343 |
|
<< std::endl; |
344 |
|
Trace("nl-ext-debug") << " " << false_asserts.size() |
345 |
|
<< " false assertions" << std::endl; |
346 |
|
Trace("nl-ext-debug") << " " << xts.size() |
347 |
|
<< " extended terms: " << std::endl; |
348 |
|
Trace("nl-ext-debug") << " "; |
349 |
|
for (unsigned j = 0; j < xts.size(); j++) |
350 |
|
{ |
351 |
|
Trace("nl-ext-debug") << xts[j] << " "; |
352 |
|
} |
353 |
|
Trace("nl-ext-debug") << std::endl; |
354 |
|
} |
355 |
|
|
356 |
|
// compute whether shared terms have correct values |
357 |
2110 |
unsigned num_shared_wrong_value = 0; |
358 |
4220 |
std::vector<Node> shared_term_value_splits; |
359 |
|
// must ensure that shared terms are equal to their concrete value |
360 |
2110 |
Trace("nl-ext-mv") << "Shared terms : " << std::endl; |
361 |
32183 |
for (context::CDList<TNode>::const_iterator its = |
362 |
2110 |
d_containing.shared_terms_begin(); |
363 |
34293 |
its != d_containing.shared_terms_end(); |
364 |
|
++its) |
365 |
|
{ |
366 |
64366 |
TNode shared_term = *its; |
367 |
|
// compute its value in the model, and its evaluation in the model |
368 |
64366 |
Node stv0 = d_model.computeConcreteModelValue(shared_term); |
369 |
64366 |
Node stv1 = d_model.computeAbstractModelValue(shared_term); |
370 |
32183 |
d_model.printModelValue("nl-ext-mv", shared_term); |
371 |
32183 |
if (stv0 != stv1) |
372 |
|
{ |
373 |
3701 |
num_shared_wrong_value++; |
374 |
7402 |
Trace("nl-ext-mv") << "Bad shared term value : " << shared_term |
375 |
3701 |
<< std::endl; |
376 |
3701 |
if (shared_term != stv0) |
377 |
|
{ |
378 |
|
// split on the value, this is non-terminating in general, TODO : |
379 |
|
// improve this |
380 |
7370 |
Node eq = shared_term.eqNode(stv0); |
381 |
3685 |
shared_term_value_splits.push_back(eq); |
382 |
|
} |
383 |
|
else |
384 |
|
{ |
385 |
|
// this can happen for transcendental functions |
386 |
|
// the problem is that we cannot evaluate transcendental functions |
387 |
|
// (they don't have a rewriter that returns constants) |
388 |
|
// thus, the actual value in their model can be themselves, hence we |
389 |
|
// have no reference point to rule out the current model. In this |
390 |
|
// case, we may set incomplete below. |
391 |
|
} |
392 |
|
} |
393 |
|
} |
394 |
4220 |
Trace("nl-ext-debug") << " " << num_shared_wrong_value |
395 |
2110 |
<< " shared terms with wrong model value." << std::endl; |
396 |
|
bool needsRecheck; |
397 |
392 |
do |
398 |
|
{ |
399 |
2126 |
d_model.resetCheck(); |
400 |
2126 |
needsRecheck = false; |
401 |
|
// complete_status: |
402 |
|
// 1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown |
403 |
2126 |
int complete_status = 1; |
404 |
|
// We require a check either if an assertion is false or a shared term has |
405 |
|
// a wrong value |
406 |
2126 |
if (!false_asserts.empty() || num_shared_wrong_value > 0) |
407 |
|
{ |
408 |
1818 |
complete_status = num_shared_wrong_value > 0 ? -1 : 0; |
409 |
1818 |
runStrategy(Theory::Effort::EFFORT_FULL, assertions, false_asserts, xts); |
410 |
1818 |
if (d_im.hasSentLemma() || d_im.hasPendingLemma()) |
411 |
|
{ |
412 |
1563 |
d_im.clearWaitingLemmas(); |
413 |
3313 |
return Result::Sat::UNSAT; |
414 |
|
} |
415 |
|
} |
416 |
1126 |
Trace("nl-ext") << "Finished check with status : " << complete_status |
417 |
563 |
<< std::endl; |
418 |
|
|
419 |
|
// if we did not add a lemma during check and there is a chance for SAT |
420 |
563 |
if (complete_status == 0) |
421 |
|
{ |
422 |
302 |
Trace("nl-ext") |
423 |
151 |
<< "Check model based on bounds for irrational-valued functions..." |
424 |
151 |
<< std::endl; |
425 |
|
// check the model based on simple solving of equalities and using |
426 |
|
// error bounds on the Taylor approximation of transcendental functions. |
427 |
151 |
if (checkModel(assertions)) |
428 |
|
{ |
429 |
52 |
complete_status = 1; |
430 |
|
} |
431 |
151 |
if (d_im.hasUsed()) |
432 |
|
{ |
433 |
|
d_im.clearWaitingLemmas(); |
434 |
|
return Result::Sat::UNSAT; |
435 |
|
} |
436 |
|
} |
437 |
|
|
438 |
|
// if we have not concluded SAT |
439 |
563 |
if (complete_status != 1) |
440 |
|
{ |
441 |
|
// flush the waiting lemmas |
442 |
203 |
if (d_im.hasWaitingLemma()) |
443 |
|
{ |
444 |
169 |
std::size_t count = d_im.numWaitingLemmas(); |
445 |
169 |
d_im.flushWaitingLemmas(); |
446 |
338 |
Trace("nl-ext") << "...added " << count << " waiting lemmas." |
447 |
169 |
<< std::endl; |
448 |
169 |
return Result::Sat::UNSAT; |
449 |
|
} |
450 |
|
// resort to splitting on shared terms with their model value |
451 |
|
// if we did not add any lemmas |
452 |
34 |
if (num_shared_wrong_value > 0) |
453 |
|
{ |
454 |
18 |
complete_status = -1; |
455 |
18 |
if (!shared_term_value_splits.empty()) |
456 |
|
{ |
457 |
88 |
for (const Node& eq : shared_term_value_splits) |
458 |
|
{ |
459 |
144 |
Node req = Rewriter::rewrite(eq); |
460 |
144 |
Node literal = d_containing.getValuation().ensureLiteral(req); |
461 |
72 |
d_containing.getOutputChannel().requirePhase(literal, true); |
462 |
72 |
Trace("nl-ext-debug") << "Split on : " << literal << std::endl; |
463 |
144 |
Node split = literal.orNode(literal.negate()); |
464 |
72 |
d_im.addPendingLemma(split, |
465 |
|
InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT, |
466 |
|
nullptr, |
467 |
|
true); |
468 |
|
} |
469 |
16 |
if (d_im.hasWaitingLemma()) |
470 |
|
{ |
471 |
14 |
d_im.flushWaitingLemmas(); |
472 |
28 |
Trace("nl-ext") << "...added " << d_im.numPendingLemmas() |
473 |
14 |
<< " shared term value split lemmas." << std::endl; |
474 |
14 |
return Result::Sat::UNSAT; |
475 |
|
} |
476 |
|
} |
477 |
|
else |
478 |
|
{ |
479 |
|
// this can happen if we are trying to do theory combination with |
480 |
|
// trancendental functions |
481 |
|
// since their model value cannot even be computed exactly |
482 |
|
} |
483 |
|
} |
484 |
|
|
485 |
|
// we are incomplete |
486 |
40 |
if (options().arith.nlExt == options::NlExtMode::FULL |
487 |
20 |
&& options().arith.nlExtIncPrecision && d_model.usedApproximate()) |
488 |
|
{ |
489 |
16 |
d_trSlv.incrementTaylorDegree(); |
490 |
16 |
needsRecheck = true; |
491 |
|
// increase precision for PI? |
492 |
|
// Difficult since Taylor series is very slow to converge |
493 |
32 |
Trace("nl-ext") << "...increment Taylor degree to " |
494 |
16 |
<< d_trSlv.getTaylorDegree() << std::endl; |
495 |
|
} |
496 |
|
else |
497 |
|
{ |
498 |
8 |
Trace("nl-ext") << "...failed to send lemma in " |
499 |
4 |
"NonLinearExtension, set incomplete" |
500 |
4 |
<< std::endl; |
501 |
4 |
d_containing.getOutputChannel().setIncomplete(IncompleteId::ARITH_NL); |
502 |
4 |
return Result::Sat::SAT_UNKNOWN; |
503 |
|
} |
504 |
|
} |
505 |
376 |
d_im.clearWaitingLemmas(); |
506 |
|
} while (needsRecheck); |
507 |
|
|
508 |
|
// did not add lemmas |
509 |
360 |
return Result::Sat::SAT; |
510 |
|
} |
511 |
|
|
512 |
1818 |
void NonlinearExtension::runStrategy(Theory::Effort effort, |
513 |
|
const std::vector<Node>& assertions, |
514 |
|
const std::vector<Node>& false_asserts, |
515 |
|
const std::vector<Node>& xts) |
516 |
|
{ |
517 |
1818 |
++(d_stats.d_checkRuns); |
518 |
|
|
519 |
1818 |
if (Trace.isOn("nl-strategy")) |
520 |
|
{ |
521 |
|
for (const auto& a : assertions) |
522 |
|
{ |
523 |
|
Trace("nl-strategy") << "Input assertion: " << a << std::endl; |
524 |
|
} |
525 |
|
} |
526 |
1818 |
if (!d_strategy.isStrategyInit()) |
527 |
|
{ |
528 |
234 |
d_strategy.initializeStrategy(options()); |
529 |
|
} |
530 |
|
|
531 |
1818 |
auto steps = d_strategy.getStrategy(); |
532 |
1818 |
bool stop = false; |
533 |
63954 |
while (!stop && steps.hasNext()) |
534 |
|
{ |
535 |
31068 |
InferStep step = steps.next(); |
536 |
31068 |
Trace("nl-strategy") << "Step " << step << std::endl; |
537 |
31068 |
switch (step) |
538 |
|
{ |
539 |
14001 |
case InferStep::BREAK: stop = d_im.hasPendingLemma(); break; |
540 |
317 |
case InferStep::FLUSH_WAITING_LEMMAS: d_im.flushWaitingLemmas(); break; |
541 |
53 |
case InferStep::CAD_FULL: d_cadSlv.checkFull(); break; |
542 |
53 |
case InferStep::CAD_INIT: d_cadSlv.initLastCall(assertions); break; |
543 |
272 |
case InferStep::NL_FACTORING: |
544 |
272 |
d_factoringSlv.check(assertions, false_asserts); |
545 |
272 |
break; |
546 |
1520 |
case InferStep::IAND_INIT: |
547 |
1520 |
d_iandSlv.initLastCall(assertions, false_asserts, xts); |
548 |
1520 |
break; |
549 |
312 |
case InferStep::IAND_FULL: d_iandSlv.checkFullRefine(); break; |
550 |
1520 |
case InferStep::IAND_INITIAL: d_iandSlv.checkInitialRefine(); break; |
551 |
1486 |
case InferStep::POW2_INIT: |
552 |
1486 |
d_pow2Slv.initLastCall(assertions, false_asserts, xts); |
553 |
1486 |
break; |
554 |
312 |
case InferStep::POW2_FULL: d_pow2Slv.checkFullRefine(); break; |
555 |
1486 |
case InferStep::POW2_INITIAL: d_pow2Slv.checkInitialRefine(); break; |
556 |
48 |
case InferStep::ICP: |
557 |
48 |
d_icpSlv.reset(assertions); |
558 |
48 |
d_icpSlv.check(); |
559 |
48 |
break; |
560 |
1802 |
case InferStep::NL_INIT: |
561 |
1802 |
d_extState.init(xts); |
562 |
1802 |
d_monomialBoundsSlv.init(); |
563 |
1802 |
d_monomialSlv.init(xts); |
564 |
1802 |
break; |
565 |
398 |
case InferStep::NL_MONOMIAL_INFER_BOUNDS: |
566 |
398 |
d_monomialBoundsSlv.checkBounds(assertions, false_asserts); |
567 |
398 |
break; |
568 |
960 |
case InferStep::NL_MONOMIAL_MAGNITUDE0: |
569 |
960 |
d_monomialSlv.checkMagnitude(0); |
570 |
960 |
break; |
571 |
656 |
case InferStep::NL_MONOMIAL_MAGNITUDE1: |
572 |
656 |
d_monomialSlv.checkMagnitude(1); |
573 |
656 |
break; |
574 |
507 |
case InferStep::NL_MONOMIAL_MAGNITUDE2: |
575 |
507 |
d_monomialSlv.checkMagnitude(2); |
576 |
507 |
break; |
577 |
1477 |
case InferStep::NL_MONOMIAL_SIGN: d_monomialSlv.checkSign(); break; |
578 |
|
case InferStep::NL_RESOLUTION_BOUNDS: |
579 |
|
d_monomialBoundsSlv.checkResBounds(); |
580 |
|
break; |
581 |
|
case InferStep::NL_SPLIT_ZERO: d_splitZeroSlv.check(); break; |
582 |
|
case InferStep::NL_TANGENT_PLANES: d_tangentPlaneSlv.check(false); break; |
583 |
9 |
case InferStep::NL_TANGENT_PLANES_WAITING: |
584 |
9 |
d_tangentPlaneSlv.check(true); |
585 |
9 |
break; |
586 |
1506 |
case InferStep::TRANS_INIT: |
587 |
1506 |
d_trSlv.initLastCall(xts); |
588 |
1506 |
break; |
589 |
1455 |
case InferStep::TRANS_INITIAL: |
590 |
1455 |
d_trSlv.checkTranscendentalInitialRefine(); |
591 |
1455 |
break; |
592 |
661 |
case InferStep::TRANS_MONOTONIC: |
593 |
661 |
d_trSlv.checkTranscendentalMonotonic(); |
594 |
661 |
break; |
595 |
257 |
case InferStep::TRANS_TANGENT_PLANES: |
596 |
257 |
d_trSlv.checkTranscendentalTangentPlanes(); |
597 |
257 |
break; |
598 |
|
} |
599 |
|
} |
600 |
|
|
601 |
1818 |
Trace("nl-ext") << "finished strategy" << std::endl; |
602 |
3636 |
Trace("nl-ext") << " ...finished with " << d_im.numWaitingLemmas() |
603 |
1818 |
<< " waiting lemmas." << std::endl; |
604 |
3636 |
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() |
605 |
1818 |
<< " pending lemmas." << std::endl; |
606 |
1818 |
} |
607 |
|
|
608 |
|
} // namespace nl |
609 |
|
} // namespace arith |
610 |
|
} // namespace theory |
611 |
22746 |
} // namespace cvc5 |