GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/nonlinear_extension.cpp Lines: 269 323 83.3 %
Date: 2021-03-22 Branches: 454 978 46.4 %

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