src/theory/arith/nl/nonlinear_extension.cpp

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